-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma IsMatching.sup (hM : M.IsMatching) (hM' : M'.IsMatching)
    (hd : Disjoint M.support M'.support) : (M ⊔ M').IsMatching

Proof state:
case inl
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}, N.IsMatching → Disjoint N.support N'.support → v ∈ N.verts → ∃! w, (N ⊔ N').Adj v w
hmM : v ∈ M.verts
⊢ ∃! w, (M ⊔ M').Adj v w

Tactic:
exact aux hM hd hmM

Result:
no goals

Proof state:
case inr
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}, N.IsMatching → Disjoint N.support N'.support → v ∈ N.verts → ∃! w, (N ⊔ N').Adj v w
hmM' : v ∈ M'.verts
⊢ ∃! w, (M' ⊔ M).Adj v w

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

Result:
no goals

Proof state:
case intro
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
hw : (fun w => N.Adj v w) w ∧ ∀ (y : V), (fun w => N.Adj v w) y → y = w
⊢ ∃! w, (N ⊔ N').Adj v w

Tactic:
use w

Result:
case h
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
hw : (fun w => N.Adj v w) w ∧ ∀ (y : V), (fun w => N.Adj v w) y → y = w
⊢ (fun w => (N ⊔ N').Adj v w) w ∧ ∀ (y : V), (fun w => (N ⊔ N').Adj v w) y → y = w

Proof state:
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}, N.IsMatching → Disjoint N.support N'.support → v ∈ N.verts → ∃! w, (N ⊔ N').Adj v w
⊢ ∃! w, (M ⊔ M').Adj v w

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'

Result:
no goals

Proof state:
case h.inr
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 : ∀ ⦃a : V⦄, a ∈ N.support → a ∉ N'.support
hmN : v ∈ N.verts
w : V
hw : (fun w => N.Adj v w) w ∧ ∀ (y : V), (fun w => 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

Result:
no goals

Proof state:
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
⊢ ∃! w, (M ⊔ M').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

Result:
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}, N.IsMatching → Disjoint N.support N'.support → v ∈ N.verts → ∃! w, (N ⊔ N').Adj v w
⊢ ∃! w, (M ⊔ M').Adj v w

Proof state:
case h
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
hw : (fun w => N.Adj v w) w ∧ ∀ (y : V), (fun w => N.Adj v w) y → y = w
y : V
hy : (N ⊔ N').Adj v y
⊢ 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

Result:
no goals

Proof state:
case h
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
hw : (fun w => N.Adj v w) w ∧ ∀ (y : V), (fun w => N.Adj v w) y → y = w
⊢ ∀ (y : V), (fun w => (N ⊔ N').Adj v w) y → y = w

Tactic:
intro y hy

Result:
case h
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
hw : (fun w => N.Adj v w) w ∧ ∀ (y : V), (fun w => N.Adj v w) y → y = w
y : V
hy : (N ⊔ N').Adj v y
⊢ y = w

Proof state:
case h.inr
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
hw : (fun w => N.Adj v w) w ∧ ∀ (y : V), (fun w => N.Adj v w) y → y = w
y : V
h : N'.Adj v y
⊢ y = w

Tactic:
rw [Set.disjoint_left] at hd

Result:
case h.inr
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 : ∀ ⦃a : V⦄, a ∈ N.support → a ∉ N'.support
hmN : v ∈ N.verts
w : V
hw : (fun w => N.Adj v w) w ∧ ∀ (y : V), (fun w => N.Adj v w) y → y = w
y : V
h : N'.Adj v y
⊢ y = w

Proof state:
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, (N ⊔ N').Adj v w

Tactic:
obtain ⟨w, hw⟩ := hN hmN

Result:
case intro
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
hw : (fun w => N.Adj v w) w ∧ ∀ (y : V), (fun w => N.Adj v w) y → y = w
⊢ ∃! w, (N ⊔ N').Adj v w

Proof state:
case inr
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}, N.IsMatching → Disjoint N.support N'.support → v ∈ N.verts → ∃! w, (N ⊔ N').Adj v w
hmM' : v ∈ M'.verts
⊢ ∃! w, (M ⊔ M').Adj v w

Tactic:
rw [sup_comm]

Result:
case inr
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}, N.IsMatching → Disjoint N.support N'.support → v ∈ N.verts → ∃! w, (N ⊔ N').Adj v w
hmM' : v ∈ M'.verts
⊢ ∃! w, (M' ⊔ M).Adj v w

Proof state:
case h.inl
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
hw : (fun w => N.Adj v w) w ∧ ∀ (y : V), (fun w => N.Adj v w) y → y = w
y : V
h : N.Adj v y
⊢ y = w

Tactic:
exact hw.2 y h

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd : Disjoint M.support M'.support
⊢ (M ⊔ M').IsMatching

Tactic:
intro v hv

Result:
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
⊢ ∃! w, (M ⊔ M').Adj v w