## Stream: new members

### Topic: term extraction

#### Arthur Paulino (Nov 07 2021 at 20:14):

How do I turn

h: ∀ (w w' : V), M.adj v w ∧ M.adj v w' → w = w'


into

w: V
w': V
h: M.adj v w ∧ M.adj v w' → w = w'


?

#### Kyle Miller (Nov 07 2021 at 20:15):

You can't unless you happen to have two vertices w and w' on hand. If you do have them, you could do specialize h w w'.

#### Alex J. Best (Nov 07 2021 at 20:16):

If h is a hypothesis you can't do this, for instance if V was false you'd be able to turn false -> true into a proof of false.

#### Arthur Paulino (Nov 07 2021 at 20:21):

Can I use hu: rel.dom M.adj = set.univ to make this possible?

#### Ruben Van de Velde (Nov 07 2021 at 20:26):

Can you share a #mwe ?

#### Arthur Paulino (Nov 07 2021 at 20:30):

Sure

import combinatorics.simple_graph.subgraph

open finset
universe u

namespace simple_graph
variables {V : Type u} {G : simple_graph V} (M : subgraph G)

def is_matching : Prop := ∀ (v w w': V), M.adj v w ∧ M.adj v w' → w = w'

def is_perfect : Prop := is_matching M ∧ M.support = set.univ

lemma is_perfect_iff :
is_perfect M ↔ ∀ (v : V), ∃! (w : V), M.adj v w :=
begin
simp only [is_matching, is_perfect, subgraph.support, exists_unique],
split,
{ intros h v,
cases h with h hu,
specialize h v,
sorry,},
{ intro h,
split,
{ intros v w w' hv,
specialize h v,
cases hv with hw hw',
cases h with x h,
cases h with _ hy,
have hxw := hy w hw,
have hxw' := hy w' hw',
simp [hxw, hxw'], },
{ sorry, }, },
end

end simple_graph


I'm trying to clear that first sorry

#### Arthur Paulino (Nov 07 2021 at 20:33):

Both h and hu that I mentioned will be available after the line specialize h v, (right before sorry)

#### Kyle Miller (Nov 07 2021 at 20:49):

Did you define subgraph.support?

#### Kyle Miller (Nov 07 2021 at 20:55):

I'm guessing it's this (for M : G.subgraph):

def subgraph.support : set V := rel.dom M.adj

lemma subgraph.mem_support {v : V} : v ∈ M.support ↔ ∃ w, M.adj v w := iff.rfl


In that case, here's the first sorry:

lemma is_perfect_iff :
is_perfect M ↔ ∀ (v : V), ∃! (w : V), M.adj v w :=
begin
simp only [is_matching, is_perfect, exists_unique],
split,
{ intros h v,
cases h with h hu,
have hu' := set.mem_univ v,
rw [←hu, subgraph.mem_support] at hu',
cases hu' with w hw,
use [w, hw],
intros u hu,
exact h _ _ _ ⟨hu, hw⟩, },
{ sorry },
end


#### Kyle Miller (Nov 07 2021 at 20:56):

and I would suggest this for is_matching:

def is_matching : Prop := ∀ {v w w': V}, M.adj v w → M.adj v w' → w = w'


Last updated: Dec 20 2023 at 11:08 UTC