-- Mathlib/Combinatorics/HalesJewett.lean
theorem exists_mono_in_high_dimension_fin (α κ η) [Finite α] [Finite κ] [Finite η] :
    ∃ n, ∀ C : (Fin n → α) → κ, ∃ l : Subspace η α (Fin n), l.IsMono C

Proof state:
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
⊢ ∃ n, ∀ (C : (Fin n → α) → κ), ∃ l, IsMono C l

Tactic:
obtain ⟨ι, ιfin, hι⟩ := exists_mono_in_high_dimension α κ η

Result:
case intro.intro
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
⊢ ∃ n, ∀ (C : (Fin n → α) → κ), ∃ l, IsMono C l

Proof state:
case intro.intro.intro.intro.intro
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
C : (Fin (Fintype.card ι) → α) → κ
l : Subspace η α ι
c : κ
cl : ∀ (x : η → α), (fun v => C (v ∘ ⇑(Fintype.equivFin ι).symm)) (↑l x) = c
e : η
i : ι
hi : l.idxFun i = Sum.inr e
⊢ ∃ i, (l.idxFun ∘ ⇑(Fintype.equivFin ι).symm) i = Sum.inr e

Tactic:
use Fintype.equivFin _ i

Result:
case h
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
C : (Fin (Fintype.card ι) → α) → κ
l : Subspace η α ι
c : κ
cl : ∀ (x : η → α), (fun v => C (v ∘ ⇑(Fintype.equivFin ι).symm)) (↑l x) = c
e : η
i : ι
hi : l.idxFun i = Sum.inr e
⊢ (l.idxFun ∘ ⇑(Fintype.equivFin ι).symm) ((Fintype.equivFin ι) i) = Sum.inr e

Proof state:
case intro.intro.intro.intro
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
C : (Fin (Fintype.card ι) → α) → κ
l : Subspace η α ι
c : κ
cl : ∀ (x : η → α), (fun v => C (v ∘ ⇑(Fintype.equivFin ι).symm)) (↑l x) = c
⊢ ∃ l, IsMono C l

Tactic:
refine ⟨⟨l.idxFun ∘ (Fintype.equivFin _).symm, fun e ↦ ?_⟩, c, cl⟩

Result:
case intro.intro.intro.intro
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
C : (Fin (Fintype.card ι) → α) → κ
l : Subspace η α ι
c : κ
cl : ∀ (x : η → α), (fun v => C (v ∘ ⇑(Fintype.equivFin ι).symm)) (↑l x) = c
e : η
⊢ ∃ i, (l.idxFun ∘ ⇑(Fintype.equivFin ι).symm) i = Sum.inr e

Proof state:
case h
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
C : (Fin (Fintype.card ι) → α) → κ
l : Subspace η α ι
c : κ
cl : ∀ (x : η → α), (fun v => C (v ∘ ⇑(Fintype.equivFin ι).symm)) (↑l x) = c
e : η
i : ι
hi : l.idxFun i = Sum.inr e
⊢ (l.idxFun ∘ ⇑(Fintype.equivFin ι).symm) ((Fintype.equivFin ι) i) = Sum.inr e

Tactic:
simpa using hi

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
C : (Fin (Fintype.card ι) → α) → κ
l : Subspace η α ι
c : κ
cl : ∀ (x : η → α), (fun v => C (v ∘ ⇑(Fintype.equivFin ι).symm)) (↑l x) = c
e : η
⊢ ∃ i, (l.idxFun ∘ ⇑(Fintype.equivFin ι).symm) i = Sum.inr e

Tactic:
obtain ⟨i, hi⟩ := l.proper e

Result:
case intro.intro.intro.intro.intro
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
C : (Fin (Fintype.card ι) → α) → κ
l : Subspace η α ι
c : κ
cl : ∀ (x : η → α), (fun v => C (v ∘ ⇑(Fintype.equivFin ι).symm)) (↑l x) = c
e : η
i : ι
hi : l.idxFun i = Sum.inr e
⊢ ∃ i, (l.idxFun ∘ ⇑(Fintype.equivFin ι).symm) i = Sum.inr e

Proof state:
case intro.intro
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
⊢ ∃ n, ∀ (C : (Fin n → α) → κ), ∃ l, IsMono C l

Tactic:
refine ⟨Fintype.card ι, fun C ↦ ?_⟩

Result:
case intro.intro
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
C : (Fin (Fintype.card ι) → α) → κ
⊢ ∃ l, IsMono C l

Proof state:
case intro.intro
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
C : (Fin (Fintype.card ι) → α) → κ
⊢ ∃ l, IsMono C l

Tactic:
obtain ⟨l, c, cl⟩ := hι fun v ↦ C (v ∘ (Fintype.equivFin _).symm)

Result:
case intro.intro.intro.intro
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
ι : Type
ιfin : Fintype ι
hι : ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
C : (Fin (Fintype.card ι) → α) → κ
l : Subspace η α ι
c : κ
cl : ∀ (x : η → α), (fun v => C (v ∘ ⇑(Fintype.equivFin ι).symm)) (↑l x) = c
⊢ ∃ l, IsMono C l