awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
val : Sym2 V
x y : V
he : Quot.mk (Sym2.Rel V) (x, y) ∈ M.edgeSet
⊢ ∃ (a : (↑M.verts : Type u_1)),
    h.toEdge a = Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) (Quot.mk (Sym2.Rel V) (x, y)) he

Tactic:
⟨⟨x, M.edge_vert he⟩, h.toEdge_eq_of_adj he⟩

Premises used: SimpleGraph.Subgraph.edge_vert, SimpleGraph.Subgraph.IsMatching.toEdge_eq_of_adj, Subtype.mk, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
val : Sym2 V
x y : V
he : Quot.mk (Sym2.Rel V) (x, y) ∈ M.edgeSet
⊢ ∃ (a : (↑M.verts : Type u_1)),
    h.toEdge a = Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) (Quot.mk (Sym2.Rel V) (x, y)) he

Tactic:
exact ⟨⟨x, M.edge_vert he⟩, h.toEdge_eq_of_adj he⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
v w : V
h : M.IsMatching
ha : M.Adj v w
rw :
  Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(v, w) ha =
    h.toEdge (Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) w ⋯)
rw₁ :
  Eq (α := (↑M.edgeSet : Type u_1)) (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(v, w) ha)
    (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(w, v) ⋯)
rw₂ : s(v, w) = s(w, v)
rw₃ rw₄ : s(w, v) = s(w, v)
⊢ h.toEdge (Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯) =
    h.toEdge (Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) w ⋯)

Tactic:
rw [h.toEdge_eq_of_adj ha, h.toEdge_eq_of_adj ha.symm, Subtype.mk_eq_mk, Sym2.eq_swap]

Premises used: SimpleGraph.Subgraph.Adj.symm, SimpleGraph.Subgraph.IsMatching.toEdge_eq_of_adj, Sym2.eq_swap, Subtype.mk_eq_mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
hv : v ∈ M.verts
⊢ v ∈ (↑(h.toEdge (Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v hv)) : Sym2 V)

Tactic:
⟨h hv |>.choose, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Exists.choose, Sym2.Mem, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v : V
h : M.IsMatching
huv : M.Adj u v
⊢ h.toEdge ⁻¹' {Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(u, v) huv} =
    {Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) u ⋯, Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯}

Tactic:
Set.ext fun w ↦ ⟨fun hw ↦ ?_, fun hw ↦ ?_⟩

Premises used: Set.ext, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v : V
h : M.IsMatching
huv : M.Adj u v
refine_1 :
  ∀ (w : (↑M.verts : Type u_1))
    (hw : w ∈ h.toEdge ⁻¹' {Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(u, v) huv}),
    Membership.mem (γ := Set (↑M.verts : Type u_1))
      {Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) u ⋯, Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯} w
refine_2 :
  ∀ (w : (↑M.verts : Type u_1))
    (hw :
      Membership.mem (γ := Set (↑M.verts : Type u_1))
        {Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) u ⋯, Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯} w),
    w ∈ h.toEdge ⁻¹' {Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(u, v) huv}
⊢ h.toEdge ⁻¹' {Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(u, v) huv} =
    {Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) u ⋯, Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯}

Tactic:
refine Set.ext fun w ↦ ⟨fun hw ↦ ?_, fun hw ↦ ?_⟩

Premises used: Set.ext, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v : V
h : M.IsMatching
huv : M.Adj u v
w : (↑M.verts : Type u_1)
hw : w ∈ h.toEdge ⁻¹' {Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(u, v) huv}
⊢ Membership.mem (γ := Set (↑M.verts : Type u_1))
    {Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) u ⋯, Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯} w

Tactic:
grind [h.mem_coe_toEdge w.property]

Premises used: SimpleGraph.Subgraph.IsMatching.mem_coe_toEdge, Subtype.property
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v : V
h : M.IsMatching
huv : M.Adj u v
w : (↑M.verts : Type u_1)
hw :
  Membership.mem (γ := Set (↑M.verts : Type u_1))
    {Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) u ⋯, Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯} w
refine_2 :
  Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) u ⋯ ∈
    h.toEdge ⁻¹' {Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(u, v) huv}
refine_2₁ :
  Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯ ∈
    h.toEdge ⁻¹' {Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(u, v) huv}
⊢ w ∈ h.toEdge ⁻¹' {Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(u, v) huv}

Tactic:
rcases hw with rfl | rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v : V
h : M.IsMatching
huv : M.Adj u v
⊢ Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) u ⋯ ∈
    h.toEdge ⁻¹' {Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(u, v) huv}

Tactic:
simp [h.toEdge_eq_of_adj huv]

Premises used: SimpleGraph.Subgraph.IsMatching.toEdge_eq_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v : V
h : M.IsMatching
huv : M.Adj u v
⊢ Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯ ∈
    h.toEdge ⁻¹' {Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(u, v) huv}

Tactic:
simp [h.toEdge_eq_of_adj huv.symm]

Premises used: SimpleGraph.Subgraph.Adj.symm, SimpleGraph.Subgraph.IsMatching.toEdge_eq_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
hGG' : G ≤ G'
v : V
hv : v ∈ (Subgraph.map (Hom.ofLE hGG') M).verts
obtain :
  ∀ (w : V) (hv : w ∈ M.verts) (hv' : (Hom.ofLE hGG' : (a : V) → V) w = v),
    ∃! w : V, (Subgraph.map (Hom.ofLE hGG') M).Adj v w
⊢ ∃! w : V, (Subgraph.map (Hom.ofLE hGG') M).Adj v w

Tactic:
obtain ⟨_, hv, hv'⟩ := Set.mem_image _ _ _ |>.mp hv

Premises used: Set.mem_image, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
hGG' : G ≤ G'
v : V
hv_1 : v ∈ (Subgraph.map (Hom.ofLE hGG') M).verts
w : V
hv : w ∈ M.verts
hv' : (Hom.ofLE hGG' : (a : V) → V) w = v
obtain :
  ∀ (w_1 : V) (hw : (fun (w_2 : V) ↦ M.Adj w w_2) w_1 ∧ ∀ (y : V), (fun (w_2 : V) ↦ M.Adj w w_2) y → y = w_1),
    ∃! w : V, (Subgraph.map (Hom.ofLE hGG') M).Adj v w
⊢ ∃! w : V, (Subgraph.map (Hom.ofLE hGG') M).Adj v w

Tactic:
obtain ⟨w, hw⟩ := h hv
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
hGG' : G ≤ G'
v : V
hv_1 : v ∈ (Subgraph.map (Hom.ofLE hGG') M).verts
w_1 : V
hv : w_1 ∈ M.verts
hv' : (Hom.ofLE hGG' : (a : V) → V) w_1 = v
w : V
hw : (fun (w : V) ↦ M.Adj w_1 w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj w_1 w) y → y = w
h₁ :
  (fun (w : V) ↦ (Subgraph.map (Hom.ofLE hGG') M).Adj v w) w ∧
    ∀ (y : V), (fun (w : V) ↦ (Subgraph.map (Hom.ofLE hGG') M).Adj v w) y → y = w
⊢ ∃! w : V, (Subgraph.map (Hom.ofLE hGG') M).Adj v w

Tactic:
use w
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
hGG' : G ≤ G'
v : V
hv_1 : v ∈ (Subgraph.map (Hom.ofLE hGG') M).verts
w_1 : V
hv : w_1 ∈ M.verts
hv' : (Hom.ofLE hGG' : (a : V) → V) w_1 = v
w : V
hw : (fun (w : V) ↦ M.Adj w_1 w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj w_1 w) y → y = w
⊢ (fun (w : V) ↦ (Subgraph.map (Hom.ofLE hGG') M).Adj v w) w ∧
    ∀ (y : V), (fun (w : V) ↦ (Subgraph.map (Hom.ofLE hGG') M).Adj v w) y → y = w

Tactic:
simpa using hv' ▸ hw
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v w : V
hM : M.IsMatching
huv : M.Adj u v
huw : M.Adj u w
⊢ v = w

Tactic:
(hM <| M.edge_vert huv).unique huv huw

Premises used: SimpleGraph.Subgraph.edge_vert, ExistsUnique.unique
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v w : V
hM : M.IsMatching
huw : M.Adj u w
hvw : M.Adj v w
⊢ u = v

Tactic:
hM.eq_of_adj_left huw.symm hvw.symm

Premises used: SimpleGraph.Subgraph.Adj.symm, SimpleGraph.Subgraph.IsMatching.eq_of_adj_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v w : V
hM : M.IsMatching
hvw : v ≠ w
huv : M.Adj u v
⊢ ¬M.Adj u w

Tactic:
fun huw ↦ hvw <| hM.eq_of_adj_left huv huw

Premises used: SimpleGraph.Subgraph.IsMatching.eq_of_adj_left, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v w : V
hM : M.IsMatching
huv : u ≠ v
huw : M.Adj u w
⊢ ¬M.Adj v w

Tactic:
fun hvw ↦ huv <| hM.eq_of_adj_right huw hvw

Premises used: SimpleGraph.Subgraph.IsMatching.eq_of_adj_right, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd_1 : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
N N' : G.Subgraph
hN : N.IsMatching
hd : Disjoint N.support N'.support
hmN : v ∈ N.verts
obtain :
  ∀ (w : V) (hw : (fun (w : V) ↦ N.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ N.Adj v w) y → y = w),
    ∃! w : V, (N ⊔ N').Adj v w
⊢ ∃! w : V, (N ⊔ N').Adj v w

Tactic:
obtain ⟨w, hw⟩ := hN hmN
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd_1 : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
N N' : G.Subgraph
hN : N.IsMatching
hd : Disjoint N.support N'.support
hmN : v ∈ N.verts
w : V
hw : (fun (w : V) ↦ N.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ N.Adj v w) y → y = w
h : (fun (w : V) ↦ (N ⊔ N').Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ (N ⊔ N').Adj v w) y → y = w
⊢ ∃! w : V, (N ⊔ N').Adj v w

Tactic:
use w
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd_1 : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
N N' : G.Subgraph
hN : N.IsMatching
hd : Disjoint N.support N'.support
hmN : v ∈ N.verts
w : V
hw : (fun (w : V) ↦ N.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ N.Adj v w) y → y = w
⊢ (fun (w : V) ↦ (N ⊔ N').Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ (N ⊔ N').Adj v w) y → y = w

Tactic:
⟨sup_adj.mpr (.inl hw.1), ?_⟩

Premises used: Iff.mpr, SimpleGraph.Subgraph.sup_adj, And.left, And.intro, Or.inl
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd_1 : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
N N' : G.Subgraph
hN : N.IsMatching
hd : Disjoint N.support N'.support
hmN : v ∈ N.verts
w : V
hw : (fun (w : V) ↦ N.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ N.Adj v w) y → y = w
h : ∀ (y : V), (fun (w : V) ↦ (N ⊔ N').Adj v w) y → y = w
⊢ (fun (w : V) ↦ (N ⊔ N').Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ (N ⊔ N').Adj v w) y → y = w

Tactic:
refine ⟨sup_adj.mpr (.inl hw.1), ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd_1 : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
N N' : G.Subgraph
hN : N.IsMatching
hd : Disjoint N.support N'.support
hmN : v ∈ N.verts
w : V
hw : (fun (w : V) ↦ N.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ N.Adj v w) y → y = w
y : V
h : N.Adj v y
⊢ y = w

Tactic:
hw.2 y h

Premises used: And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd_1 : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
N N' : G.Subgraph
hN : N.IsMatching
hd : Disjoint N.support N'.support
hmN : v ∈ N.verts
w : V
hw : (fun (w : V) ↦ N.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ N.Adj v w) y → y = w
y : V
h : N.Adj v y
⊢ y = w

Tactic:
exact hw.2 y h

Premises used: And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd_1 : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
N N' : G.Subgraph
hN : N.IsMatching
hd : Disjoint N.support N'.support
hmN : v ∈ N.verts
w : V
hw : (fun (w : V) ↦ N.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ N.Adj v w) y → y = w
y : V
h : N'.Adj v y
h₁ :
  ∀ (hd : ∀ ⦃a : V⦄, a ∈ N.support → a ∉ N'.support) (hmN : v ∈ N.verts) (w : V)
    (hw : (fun (w : V) ↦ N.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ N.Adj v w) y → y = w) (y : V) (h : N'.Adj v y), y = w
⊢ y = w

Tactic:
rw [Set.disjoint_left] at hd

Premises used: Set.disjoint_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd_1 : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
N N' : G.Subgraph
hN : N.IsMatching
hd : ∀ ⦃a : V⦄, a ∈ N.support → a ∉ N'.support
hmN : v ∈ N.verts
w : V
hw : (fun (w : V) ↦ N.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ N.Adj v w) y → y = w
y : V
h : N'.Adj v y
⊢ y = w

Tactic:
simpa [(mem_support _).mpr ⟨w, hw.1⟩, (mem_support _).mpr ⟨y, h⟩] using @hd v

Premises used: Iff.mpr, And.left, Exists.intro, SimpleGraph.Subgraph.mem_support
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd_1 : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
N N' : G.Subgraph
hN : N.IsMatching
hd : Disjoint N.support N'.support
hmN : v ∈ N.verts
w : V
hw : (fun (w : V) ↦ N.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ N.Adj v w) y → y = w
y : V
hy : (N ⊔ N').Adj v y
h : ∀ (h : N.Adj v y), y = w
h₁ : ∀ (h : N'.Adj v y), y = w
⊢ y = w

Tactic:
cases hy with
    | inl h => exact hw.2 y h
    | inr h =>
      rw [Set.disjoint_left] at hd
      simpa [(mem_support _).mpr ⟨w, hw.1⟩, (mem_support _).mpr ⟨y, h⟩] using @hd v

Premises used: Iff.mpr, Set.disjoint_left, And.left, Exists.intro, SimpleGraph.Subgraph.mem_support
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
⊢ ∀ {N N' : G.Subgraph} (hN : N.IsMatching) (hd : Disjoint N.support N'.support) (hmN : v ∈ N.verts),
    ∃! w : V, (N ⊔ N').Adj v w

Tactic:
have aux {N N' : Subgraph G} (hN : N.IsMatching) (hd : Disjoint N.support N'.support)
    (hmN : v ∈ N.verts) : ∃! w, (N ⊔ N').Adj v w := by
    obtain ⟨w, hw⟩ := hN hmN
    use w
    refine ⟨sup_adj.mpr (.inl hw.1), ?_⟩
    intro y hy
    cases hy with
    | inl h => exact hw.2 y h
    | inr h =>
      rw [Set.disjoint_left] at hd
      simpa [(mem_support _).mpr ⟨w, hw.1⟩, (mem_support _).mpr ⟨y, h⟩] using @hd v
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
aux :
  ∀ {N N' : G.Subgraph} (hN : N.IsMatching) (hd : Disjoint N.support N'.support) (hmN : v ∈ N.verts),
    ∃! w : V, (N ⊔ N').Adj v w
hmM : v ∈ M.verts
⊢ ∃! w : V, (M ⊔ M').Adj v w

Tactic:
aux hM hd hmM
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
aux :
  ∀ {N N' : G.Subgraph} (hN : N.IsMatching) (hd : Disjoint N.support N'.support) (hmN : v ∈ N.verts),
    ∃! w : V, (N ⊔ N').Adj v w
hmM : v ∈ M.verts
⊢ ∃! w : V, (M ⊔ M').Adj v w

Tactic:
exact aux hM hd hmM
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
aux :
  ∀ {N N' : G.Subgraph} (hN : N.IsMatching) (hd : Disjoint N.support N'.support) (hmN : v ∈ N.verts),
    ∃! w : V, (N ⊔ N').Adj v w
hmM' : v ∈ M'.verts
inr : ∃! w : V, (M' ⊔ M).Adj v w
⊢ ∃! w : V, (M ⊔ M').Adj v w

Tactic:
rw [sup_comm]

Premises used: sup_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
aux :
  ∀ {N N' : G.Subgraph} (hN : N.IsMatching) (hd : Disjoint N.support N'.support) (hmN : v ∈ N.verts),
    ∃! w : V, (N ⊔ N').Adj v w
hmM' : v ∈ M'.verts
⊢ ∃! w : V, (M' ⊔ M).Adj v w

Tactic:
aux hM' (Disjoint.symm hd) hmM'

Premises used: Disjoint.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
aux :
  ∀ {N N' : G.Subgraph} (hN : N.IsMatching) (hd : Disjoint N.support N'.support) (hmN : v ∈ N.verts),
    ∃! w : V, (N ⊔ N').Adj v w
hmM' : v ∈ M'.verts
⊢ ∃! w : V, (M' ⊔ M).Adj v w

Tactic:
exact aux hM' (Disjoint.symm hd) hmM'

Premises used: Disjoint.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
aux :
  ∀ {N N' : G.Subgraph} (hN : N.IsMatching) (hd : Disjoint N.support N'.support) (hmN : v ∈ N.verts),
    ∃! w : V, (N ⊔ N').Adj v w
⊢ v ∈ M.verts ∨ v ∈ M'.verts

Tactic:
cases Set.mem_or_mem_of_mem_union hv with
  | inl hmM => exact aux hM hd hmM
  | inr hmM' =>
    rw [sup_comm]
    exact aux hM' (Disjoint.symm hd) hmM'

Premises used: Set.mem_or_mem_of_mem_union, sup_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun (i j : ι) ↦ Disjoint (f i).support (f j).support
v : V
hv : Membership.mem (γ := Set V) (verts (G := G) (⨆ (i : ι), f i)) v
obtain : ∀ (i : ι) (hi : v ∈ (f i).verts), ∃! w : V, Adj (G := G) (⨆ (i : ι), f i) v w
⊢ ∃! w : V, Adj (G := G) (⨆ (i : ι), f i) v w

Tactic:
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp (verts_iSup ▸ hv)

Premises used: Set.mem_iUnion, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun (i j : ι) ↦ Disjoint (f i).support (f j).support
v : V
hv : Membership.mem (γ := Set V) (verts (G := G) (⨆ (i : ι), f i)) v
i : ι
hi : v ∈ (f i).verts
obtain :
  ∀ (w : V) (hw : (fun (w : V) ↦ (f i).Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ (f i).Adj v w) y → y = w),
    ∃! w : V, Adj (G := G) (⨆ (i : ι), f i) v w
⊢ ∃! w : V, Adj (G := G) (⨆ (i : ι), f i) v w

Tactic:
obtain ⟨w, hw⟩ := hM i hi
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun (i j : ι) ↦ Disjoint (f i).support (f j).support
v : V
hv : Membership.mem (γ := Set V) (verts (G := G) (⨆ (i : ι), f i)) v
i : ι
hi : v ∈ (f i).verts
w : V
hw : (fun (w : V) ↦ (f i).Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ (f i).Adj v w) y → y = w
h :
  (fun (w : V) ↦ Adj (G := G) (⨆ (i : ι), f i) v w) w ∧
    ∀ (y : V), (fun (w : V) ↦ Adj (G := G) (⨆ (i : ι), f i) v w) y → y = w
⊢ ∃! w : V, Adj (G := G) (⨆ (i : ι), f i) v w

Tactic:
use w
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun (i j : ι) ↦ Disjoint (f i).support (f j).support
v : V
hv : Membership.mem (γ := Set V) (verts (G := G) (⨆ (i : ι), f i)) v
i : ι
hi : v ∈ (f i).verts
w : V
hw : (fun (w : V) ↦ (f i).Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ (f i).Adj v w) y → y = w
⊢ (fun (w : V) ↦ Adj (G := G) (⨆ (i : ι), f i) v w) w ∧
    ∀ (y : V), (fun (w : V) ↦ Adj (G := G) (⨆ (i : ι), f i) v w) y → y = w

Tactic:
⟨iSup_adj.mpr ⟨i, hw.1⟩, ?_⟩

Premises used: Iff.mpr, And.left, And.intro, Exists.intro, SimpleGraph.Subgraph.iSup_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun (i j : ι) ↦ Disjoint (f i).support (f j).support
v : V
hv : Membership.mem (γ := Set V) (verts (G := G) (⨆ (i : ι), f i)) v
i : ι
hi : v ∈ (f i).verts
w : V
hw : (fun (w : V) ↦ (f i).Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ (f i).Adj v w) y → y = w
h : ∀ (y : V), (fun (w : V) ↦ Adj (G := G) (⨆ (i : ι), f i) v w) y → y = w
⊢ (fun (w : V) ↦ Adj (G := G) (⨆ (i : ι), f i) v w) w ∧
    ∀ (y : V), (fun (w : V) ↦ Adj (G := G) (⨆ (i : ι), f i) v w) y → y = w

Tactic:
refine ⟨iSup_adj.mpr ⟨i, hw.1⟩, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun (i j : ι) ↦ Disjoint (f i).support (f j).support
v : V
hv : Membership.mem (γ := Set V) (verts (G := G) (⨆ (i : ι), f i)) v
i : ι
hi : v ∈ (f i).verts
w : V
hw : (fun (w : V) ↦ (f i).Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ (f i).Adj v w) y → y = w
y : V
hy : Adj (G := G) (⨆ (i : ι), f i) v y
h : ∀ (i' : ι) (hi' : (f i').Adj v y), y = w
⊢ y = w

Tactic:
obtain ⟨i', hi'⟩ := iSup_adj.mp hy

Premises used: Iff.mp, SimpleGraph.Subgraph.iSup_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun (i j : ι) ↦ Disjoint (f i).support (f j).support
v : V
hv : Membership.mem (γ := Set V) (verts (G := G) (⨆ (i : ι), f i)) v
i : ι
hi : v ∈ (f i).verts
w : V
hw : (fun (w : V) ↦ (f i).Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ (f i).Adj v w) y → y = w
y : V
hy : Adj (G := G) (⨆ (i : ι), f i) v y
i' : ι
hi' : (f i').Adj v y
pos : ∀ (heq : i = i'), y = w
neg : ∀ (heq : ¬i = i'), y = w
⊢ y = w

Tactic:
by_cases heq : i = i'
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun (i j : ι) ↦ Disjoint (f i).support (f j).support
v : V
hv : Membership.mem (γ := Set V) (verts (G := G) (⨆ (i : ι), f i)) v
i : ι
hi : v ∈ (f i).verts
w : V
hw : (fun (w : V) ↦ (f i).Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ (f i).Adj v w) y → y = w
y : V
hy : Adj (G := G) (⨆ (i : ι), f i) v y
i' : ι
hi' : (f i').Adj v y
heq : i = i'
⊢ y = w

Tactic:
hw.2 y (heq.symm ▸ hi')

Premises used: Eq.rec, And.right, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun (i j : ι) ↦ Disjoint (f i).support (f j).support
v : V
hv : Membership.mem (γ := Set V) (verts (G := G) (⨆ (i : ι), f i)) v
i : ι
hi : v ∈ (f i).verts
w : V
hw : (fun (w : V) ↦ (f i).Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ (f i).Adj v w) y → y = w
y : V
hy : Adj (G := G) (⨆ (i : ι), f i) v y
i' : ι
hi' : (f i').Adj v y
heq : i = i'
⊢ y = w

Tactic:
exact hw.2 y (heq.symm ▸ hi')

Premises used: Eq.rec, And.right, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun (i j : ι) ↦ Disjoint (f i).support (f j).support
v : V
hv : Membership.mem (γ := Set V) (verts (G := G) (⨆ (i : ι), f i)) v
i : ι
hi : v ∈ (f i).verts
w : V
hw : (fun (w : V) ↦ (f i).Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ (f i).Adj v w) y → y = w
y : V
hy : Adj (G := G) (⨆ (i : ι), f i) v y
i' : ι
hi' : (f i').Adj v y
heq : ¬i = i'
⊢ (fun (i j : ι) ↦ Disjoint (f i).support (f j).support) i i'

Tactic:
have := hd heq