-- Mathlib/Combinatorics/HalesJewett.lean
theorem exists_mono_in_high_dimension (α κ η) [Finite α] [Finite κ] [Finite η] :
    ∃ (ι : Type) (_ : Fintype ι), ∀ C : (ι → α) → κ, ∃ l : Subspace η α ι, l.IsMono C

Proof state:
case intro.intro.intro.intro
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
val✝ : Fintype η
ι : Type
w✝ : Fintype ι
hι : ∀ (C : (ι → Shrink.{0, u_7} η → α) → κ), ∃ l, Line.IsMono C l
C : (ι × Shrink.{0, u_7} η → α) → κ
l : Line (Shrink.{0, u_7} η → α) ι
hl :
  Line.IsMono
    (fun x =>
      C fun x_1 =>
        match x_1 with
        | (i, e) => x i e)
    l
⊢ ∃ l, IsMono C l

Tactic:
refine ⟨l.toSubspace.reindex (equivShrink.{0} η).symm (Equiv.refl _) (Equiv.refl _), ?_⟩

Result:
case intro.intro.intro.intro
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
val✝ : Fintype η
ι : Type
w✝ : Fintype ι
hι : ∀ (C : (ι → Shrink.{0, u_7} η → α) → κ), ∃ l, Line.IsMono C l
C : (ι × Shrink.{0, u_7} η → α) → κ
l : Line (Shrink.{0, u_7} η → α) ι
hl :
  Line.IsMono
    (fun x =>
      C fun x_1 =>
        match x_1 with
        | (i, e) => x i e)
    l
⊢ IsMono C (l.toSubspace.reindex (equivShrink η).symm (Equiv.refl α) (Equiv.refl (ι × Shrink.{0, u_7} η)))

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

Tactic:
cases nonempty_fintype η

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

Proof state:
case intro.intro.intro.intro
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
val✝ : Fintype η
ι : Type
w✝ : Fintype ι
hι : ∀ (C : (ι → Shrink.{0, u_7} η → α) → κ), ∃ l, Line.IsMono C l
C : (ι × Shrink.{0, u_7} η → α) → κ
l : Line (Shrink.{0, u_7} η → α) ι
hl :
  Line.IsMono
    (fun x =>
      C fun x_1 =>
        match x_1 with
        | (i, e) => x i e)
    l
⊢ IsMono C (l.toSubspace.reindex (equivShrink η).symm (Equiv.refl α) (Equiv.refl (ι × Shrink.{0, u_7} η)))

Tactic:
convert hl.toSubspace.reindex

Result:
case h.e'_5.h.h.e'_1
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
val✝ : Fintype η
ι : Type
w✝ : Fintype ι
hι : ∀ (C : (ι → Shrink.{0, u_7} η → α) → κ), ∃ l, Line.IsMono C l
C : (ι × Shrink.{0, u_7} η → α) → κ
l : Line (Shrink.{0, u_7} η → α) ι
hl :
  Line.IsMono
    (fun x =>
      C fun x_1 =>
        match x_1 with
        | (i, e) => x i e)
    l
x✝ : ι × Shrink.{0, u_7} η → α
⊢ x✝ = ⇑(Equiv.refl α).symm ∘ x✝ ∘ ⇑(Equiv.refl (ι × Shrink.{0, u_7} η))

Proof state:
case intro.intro.intro
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
val✝ : Fintype η
ι : Type
w✝ : Fintype ι
hι : ∀ (C : (ι → Shrink.{0, u_7} η → α) → κ), ∃ l, Line.IsMono C l
⊢ ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l

Tactic:
refine ⟨ι × Shrink η, inferInstance, fun C ↦ ?_⟩

Result:
case intro.intro.intro
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
val✝ : Fintype η
ι : Type
w✝ : Fintype ι
hι : ∀ (C : (ι → Shrink.{0, u_7} η → α) → κ), ∃ l, Line.IsMono C l
C : (ι × Shrink.{0, u_7} η → α) → κ
⊢ ∃ l, IsMono C l

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

Tactic:
obtain ⟨ι, _, hι⟩ := Line.exists_mono_in_high_dimension (Shrink.{0} η → α) κ

Result:
case intro.intro.intro
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
val✝ : Fintype η
ι : Type
w✝ : Fintype ι
hι : ∀ (C : (ι → Shrink.{0, u_7} η → α) → κ), ∃ l, Line.IsMono C l
⊢ ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l

Proof state:
case intro.intro.intro
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
val✝ : Fintype η
ι : Type
w✝ : Fintype ι
hι : ∀ (C : (ι → Shrink.{0, u_7} η → α) → κ), ∃ l, Line.IsMono C l
C : (ι × Shrink.{0, u_7} η → α) → κ
⊢ ∃ l, IsMono C l

Tactic:
obtain ⟨l, hl⟩ := hι fun x ↦ C fun (i, e) ↦ x i e

Result:
case intro.intro.intro.intro
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
val✝ : Fintype η
ι : Type
w✝ : Fintype ι
hι : ∀ (C : (ι → Shrink.{0, u_7} η → α) → κ), ∃ l, Line.IsMono C l
C : (ι × Shrink.{0, u_7} η → α) → κ
l : Line (Shrink.{0, u_7} η → α) ι
hl :
  Line.IsMono
    (fun x =>
      C fun x_1 =>
        match x_1 with
        | (i, e) => x i e)
    l
⊢ ∃ l, IsMono C l

Proof state:
case h.e'_5.h.h.e'_1
α : Type u_5
κ : Type u_6
η : Type u_7
inst✝² : Finite α
inst✝¹ : Finite κ
inst✝ : Finite η
val✝ : Fintype η
ι : Type
w✝ : Fintype ι
hι : ∀ (C : (ι → Shrink.{0, u_7} η → α) → κ), ∃ l, Line.IsMono C l
C : (ι × Shrink.{0, u_7} η → α) → κ
l : Line (Shrink.{0, u_7} η → α) ι
hl :
  Line.IsMono
    (fun x =>
      C fun x_1 =>
        match x_1 with
        | (i, e) => x i e)
    l
x✝ : ι × Shrink.{0, u_7} η → α
⊢ x✝ = ⇑(Equiv.refl α).symm ∘ x✝ ∘ ⇑(Equiv.refl (ι × Shrink.{0, u_7} η))

Tactic:
simp

Result:
no goals