-- Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean
theorem hom_eq_iff_not_disjoint (C : G.ComponentCompl L) (h : K ⊆ L) (D : G.ComponentCompl K) :
    C.hom h = D ↔ ¬Disjoint (C : Set V) (D : Set V)

Proof state:
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
D : G.ComponentCompl K
⊢ hom h C = D ↔ ¬Disjoint ↑C ↑D

Tactic:
rw [Set.not_disjoint_iff]

Result:
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
D : G.ComponentCompl K
⊢ hom h C = D ↔ ∃ x ∈ ↑C, x ∈ ↑D

Proof state:
case mpr.intro.intro.intro.intro
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
x✝ : V
xnL : x✝ ∉ L
x : V
w✝¹ : x ∉ L
e₁ : G.componentComplMk w✝¹ = G.componentComplMk xnL
w✝ : x ∉ K
⊢ hom h (G.componentComplMk w✝¹) = G.componentComplMk w✝

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
D : G.ComponentCompl K
⊢ hom h C = D ↔ ∃ x ∈ ↑C, x ∈ ↑D

Tactic:
constructor

Result:
case mp
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
D : G.ComponentCompl K
⊢ hom h C = D → ∃ x ∈ ↑C, x ∈ ↑D

case mpr
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
D : G.ComponentCompl K
⊢ (∃ x ∈ ↑C, x ∈ ↑D) → hom h C = D

Proof state:
case mpr
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
D : G.ComponentCompl K
⊢ (∃ x ∈ ↑C, x ∈ ↑D) → hom h C = D

Tactic:
refine C.ind fun x xnL => ?_

Result:
case mpr
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
D : G.ComponentCompl K
x : V
xnL : x ∉ L
⊢ (∃ x_1 ∈ ↑(G.componentComplMk xnL), x_1 ∈ ↑D) → hom h (G.componentComplMk xnL) = D

Proof state:
case mp
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
⊢ ∃ x ∈ ↑C, x ∈ ↑(hom h C)

Tactic:
refine C.ind fun x xnL => ?_

Result:
case mp
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
x : V
xnL : x ∉ L
⊢ ∃ x_1 ∈ ↑(G.componentComplMk xnL), x_1 ∈ ↑(hom h (G.componentComplMk xnL))

Proof state:
case mp
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
D : G.ComponentCompl K
⊢ hom h C = D → ∃ x ∈ ↑C, x ∈ ↑D

Tactic:
rintro rfl

Result:
case mp
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
⊢ ∃ x ∈ ↑C, x ∈ ↑(hom h C)

Proof state:
case mpr
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
D : G.ComponentCompl K
x : V
xnL : x ∉ L
⊢ (∃ x_1 ∈ ↑(G.componentComplMk xnL), x_1 ∈ ↑D) → hom h (G.componentComplMk xnL) = D

Tactic:
rintro ⟨x, ⟨_, e₁⟩, _, rfl⟩

Result:
case mpr.intro.intro.intro.intro
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
x✝ : V
xnL : x✝ ∉ L
x : V
w✝¹ : x ∉ L
e₁ : G.componentComplMk w✝¹ = G.componentComplMk xnL
w✝ : x ∉ K
⊢ hom h (G.componentComplMk xnL) = G.componentComplMk w✝

Proof state:
case mpr.intro.intro.intro.intro
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
x✝ : V
xnL : x✝ ∉ L
x : V
w✝¹ : x ∉ L
e₁ : G.componentComplMk w✝¹ = G.componentComplMk xnL
w✝ : x ∉ K
⊢ hom h (G.componentComplMk xnL) = G.componentComplMk w✝

Tactic:
rw [← e₁]

Result:
case mpr.intro.intro.intro.intro
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
x✝ : V
xnL : x✝ ∉ L
x : V
w✝¹ : x ∉ L
e₁ : G.componentComplMk w✝¹ = G.componentComplMk xnL
w✝ : x ∉ K
⊢ hom h (G.componentComplMk w✝¹) = G.componentComplMk w✝

Proof state:
case mp
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
x : V
xnL : x ∉ L
⊢ ∃ x_1 ∈ ↑(G.componentComplMk xnL), x_1 ∈ ↑(hom h (G.componentComplMk xnL))

Tactic:
exact ⟨x, ⟨xnL, rfl⟩, ⟨fun xK => xnL (h xK), rfl⟩⟩

Result:
no goals