-- Mathlib/Combinatorics/HalesJewett.lean
lemma coe_injective [Nontrivial α] : Injective ((⇑) : Subspace η α ι → (η → α) → ι → α)

Proof state:
case idxFun.h.inr.inl.intro
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
e : η
hl : l.idxFun i = Sum.inr e
a : α
hm : m.idxFun i = Sum.inl a
b : α
hba : b ≠ a
⊢ Sum.inr e = Sum.inl a

Tactic:
simpa [hl, hm, hba, coe_apply] using hlm (const _ b) i

Result:
no goals

Proof state:
case idxFun.h.inl.intro
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
a : α
hl : l.idxFun i = Sum.inl a
b : α
hba : b ≠ a
⊢ Sum.inl a = m.idxFun i

Tactic:
cases hm : idxFun m i <;> simpa [hl, hm, hba.symm, coe_apply] using hlm (const _ b) i

Result:
no goals

Proof state:
case idxFun.h.inr.inl
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
e : η
hl : l.idxFun i = Sum.inr e
a : α
hm : m.idxFun i = Sum.inl a
⊢ Sum.inr e = Sum.inl a

Tactic:
obtain ⟨b, hba⟩ := exists_ne a

Result:
case idxFun.h.inr.inl.intro
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
e : η
hl : l.idxFun i = Sum.inr e
a : α
hm : m.idxFun i = Sum.inl a
b : α
hba : b ≠ a
⊢ Sum.inr e = Sum.inl a

Proof state:
case idxFun.h
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
⊢ l.idxFun i = m.idxFun i

Tactic:
cases hl : idxFun l i with
| inl a =>
  obtain ⟨b, hba⟩ := exists_ne a
  cases hm : idxFun m i <;> simpa [hl, hm, hba.symm, coe_apply] using hlm (const _ b) i
| inr e =>
  cases hm : idxFun m i with
  | inl a =>
    obtain ⟨b, hba⟩ := exists_ne a
    simpa [hl, hm, hba, coe_apply] using hlm (const _ b) i
  | inr f =>
    obtain ⟨a, b, hab⟩ := exists_pair_ne α
    simp only [Sum.inr.injEq]
    by_contra! hef
    simpa [hl, hm, hef, hab, coe_apply] using hlm (Function.update (const _ a) f b) i

Result:
no goals

Proof state:
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
⊢ Injective toFun

Tactic:
classical
rintro l m hlm
ext i
simp only [funext_iff] at hlm
cases hl : idxFun l i with
| inl a =>
  obtain ⟨b, hba⟩ := exists_ne a
  cases hm : idxFun m i <;> simpa [hl, hm, hba.symm, coe_apply] using hlm (const _ b) i
| inr e =>
  cases hm : idxFun m i with
  | inl a =>
    obtain ⟨b, hba⟩ := exists_ne a
    simpa [hl, hm, hba, coe_apply] using hlm (const _ b) i
  | inr f =>
    obtain ⟨a, b, hab⟩ := exists_pair_ne α
    simp only [Sum.inr.injEq]
    by_contra! hef
    simpa [hl, hm, hef, hab, coe_apply] using hlm (Function.update (const _ a) f b) i

Result:
no goals

Proof state:
case idxFun.h.inr.inr.intro.intro
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
e : η
hl : l.idxFun i = Sum.inr e
f : η
hm : m.idxFun i = Sum.inr f
a b : α
hab : a ≠ b
⊢ Sum.inr e = Sum.inr f

Tactic:
simp only [Sum.inr.injEq]

Result:
case idxFun.h.inr.inr.intro.intro
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
e : η
hl : l.idxFun i = Sum.inr e
f : η
hm : m.idxFun i = Sum.inr f
a b : α
hab : a ≠ b
⊢ e = f

Proof state:
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
⊢ Injective toFun

Tactic:
rintro l m hlm

Result:
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
hlm : ↑l = ↑m
⊢ l = m

Proof state:
case idxFun.h.inl
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
a : α
hl : l.idxFun i = Sum.inl a
⊢ Sum.inl a = m.idxFun i

Tactic:
obtain ⟨b, hba⟩ := exists_ne a

Result:
case idxFun.h.inl.intro
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
a : α
hl : l.idxFun i = Sum.inl a
b : α
hba : b ≠ a
⊢ Sum.inl a = m.idxFun i

Proof state:
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
hlm : ↑l = ↑m
⊢ l = m

Tactic:
ext i

Result:
case idxFun.h
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
hlm : ↑l = ↑m
i : ι
⊢ l.idxFun i = m.idxFun i

Proof state:
case idxFun.h.inr
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
e : η
hl : l.idxFun i = Sum.inr e
⊢ Sum.inr e = m.idxFun i

Tactic:
cases hm : idxFun m i with
| inl a =>
  obtain ⟨b, hba⟩ := exists_ne a
  simpa [hl, hm, hba, coe_apply] using hlm (const _ b) i
| inr f =>
  obtain ⟨a, b, hab⟩ := exists_pair_ne α
  simp only [Sum.inr.injEq]
  by_contra! hef
  simpa [hl, hm, hef, hab, coe_apply] using hlm (Function.update (const _ a) f b) i

Result:
no goals

Proof state:
case idxFun.h.inr.inr.intro.intro
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
e : η
hl : l.idxFun i = Sum.inr e
f : η
hm : m.idxFun i = Sum.inr f
a b : α
hab : a ≠ b
hef : e ≠ f
⊢ False

Tactic:
simpa [hl, hm, hef, hab, coe_apply] using hlm (Function.update (const _ a) f b) i

Result:
no goals

Proof state:
case idxFun.h.inr.inr
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
e : η
hl : l.idxFun i = Sum.inr e
f : η
hm : m.idxFun i = Sum.inr f
⊢ Sum.inr e = Sum.inr f

Tactic:
obtain ⟨a, b, hab⟩ := exists_pair_ne α

Result:
case idxFun.h.inr.inr.intro.intro
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
e : η
hl : l.idxFun i = Sum.inr e
f : η
hm : m.idxFun i = Sum.inr f
a b : α
hab : a ≠ b
⊢ Sum.inr e = Sum.inr f

Proof state:
case idxFun.h
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
hlm : ↑l = ↑m
i : ι
⊢ l.idxFun i = m.idxFun i

Tactic:
simp only [funext_iff] at hlm

Result:
case idxFun.h
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
⊢ l.idxFun i = m.idxFun i

Proof state:
case idxFun.h.inr.inr.intro.intro
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
e : η
hl : l.idxFun i = Sum.inr e
f : η
hm : m.idxFun i = Sum.inr f
a b : α
hab : a ≠ b
⊢ e = f

Tactic:
by_contra! hef

Result:
case idxFun.h.inr.inr.intro.intro
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
e : η
hl : l.idxFun i = Sum.inr e
f : η
hm : m.idxFun i = Sum.inr f
a b : α
hab : a ≠ b
hef : e ≠ f
⊢ False