-- Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean
theorem infinite_iff_in_all_ranges {K : Finset V} (C : G.ComponentCompl K) :
    C.supp.Infinite ↔ ∀ (L) (h : K ⊆ L), ∃ D : G.ComponentCompl L, D.hom h = C

Proof state:
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
⊢ C.supp.Infinite ↔ ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C

Tactic:
constructor

Result:
case mp
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
⊢ C.supp.Infinite → ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C

case mpr
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
⊢ (∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C) → C.supp.Infinite

Proof state:
case mpr.intro.intro
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : C.supp.Finite
D : G.ComponentCompl ↑(K ∪ Cfin.toFinset)
e : hom ⋯ D = C
v : V
vD : v ∈ ↑D
Ddis : Disjoint ↑(K ∪ Cfin.toFinset) ↑D := ComponentCompl.disjoint_right D
⊢ False

Tactic:
simp_rw [Finset.coe_union, Set.Finite.coe_toFinset, Set.disjoint_union_left,
  Set.disjoint_iff] at Ddis

Result:
case mpr.intro.intro
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : C.supp.Finite
D : G.ComponentCompl ↑(K ∪ Cfin.toFinset)
e : hom ⋯ D = C
v : V
vD : v ∈ ↑D
Ddis : ↑K ∩ ↑D ⊆ ∅ ∧ C.supp ∩ ↑D ⊆ ∅
⊢ False

Proof state:
case mpr.intro
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : C.supp.Finite
D : G.ComponentCompl ↑(K ∪ Cfin.toFinset)
e : hom ⋯ D = C
⊢ False

Tactic:
obtain ⟨v, vD⟩ := D.nonempty

Result:
case mpr.intro.intro
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : C.supp.Finite
D : G.ComponentCompl ↑(K ∪ Cfin.toFinset)
e : hom ⋯ D = C
v : V
vD : v ∈ ↑D
⊢ False

Proof state:
case mpr
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
⊢ (∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C) → C.supp.Infinite

Tactic:
rintro h Cfin

Result:
case mpr
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : C.supp.Finite
⊢ False

Proof state:
case mp.intro.intro.intro
V : Type u
G : SimpleGraph V
K L : Finset V
h : K ⊆ L
v : V
vL : v ∉ ↑L
vK : v ∉ ↑K
Cinf : (G.componentComplMk vK).supp.Infinite
⊢ ∃ D, hom h D = G.componentComplMk vK

Tactic:
exact ⟨componentComplMk _ vL, rfl⟩

Result:
no goals

Proof state:
case mp
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
Cinf : C.supp.Infinite
L : Finset V
h : K ⊆ L
⊢ ∃ D, hom h D = C

Tactic:
obtain ⟨v, ⟨vK, rfl⟩, vL⟩ := Set.Infinite.nonempty (Set.Infinite.diff Cinf L.finite_toSet)

Result:
case mp.intro.intro.intro
V : Type u
G : SimpleGraph V
K L : Finset V
h : K ⊆ L
v : V
vL : v ∉ ↑L
vK : v ∉ ↑K
Cinf : (G.componentComplMk vK).supp.Infinite
⊢ ∃ D, hom h D = G.componentComplMk vK

Proof state:
case mpr.intro.intro
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : C.supp.Finite
D : G.ComponentCompl ↑(K ∪ Cfin.toFinset)
e : hom ⋯ D = C
v : V
vD : v ∈ ↑D
⊢ False

Tactic:
let Ddis := D.disjoint_right

Result:
case mpr.intro.intro
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : C.supp.Finite
D : G.ComponentCompl ↑(K ∪ Cfin.toFinset)
e : hom ⋯ D = C
v : V
vD : v ∈ ↑D
Ddis : Disjoint ↑(K ∪ Cfin.toFinset) ↑D := ComponentCompl.disjoint_right D
⊢ False

Proof state:
case mpr.intro.intro
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : C.supp.Finite
D : G.ComponentCompl ↑(K ∪ Cfin.toFinset)
e : hom ⋯ D = C
v : V
vD : v ∈ ↑D
Ddis : ↑K ∩ ↑D ⊆ ∅ ∧ C.supp ∩ ↑D ⊆ ∅
⊢ False

Tactic:
exact Ddis.right ⟨(ComponentCompl.hom_eq_iff_le _ _ _).mp e vD, vD⟩

Result:
no goals

Proof state:
case mp
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
⊢ C.supp.Infinite → ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C

Tactic:
rintro Cinf L h

Result:
case mp
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
Cinf : C.supp.Infinite
L : Finset V
h : K ⊆ L
⊢ ∃ D, hom h D = C

Proof state:
case mpr
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : C.supp.Finite
⊢ False

Tactic:
obtain ⟨D, e⟩ := h (K ∪ Cfin.toFinset) Finset.subset_union_left

Result:
case mpr.intro
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : C.supp.Finite
D : G.ComponentCompl ↑(K ∪ Cfin.toFinset)
e : hom ⋯ D = C
⊢ False