awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
tfae_1_to_2 : ∀ (a : x ∈ V(H)), y ∈ V(H)
tfae_2_to_3 : ∀ (a : y ∈ V(H)), e ∈ E(H)
⊢ ∀ (a : e ∈ E(H)), x ∈ V(H)

Tactic:
tfae_have 3 → 1 := (he.anti_of_mem hHG.le · |>.left_mem)

Premises used: _private.0.Graph.IsLink.anti_of_mem, Graph.IsClosedSubgraph.isInducedSubgraph, Graph.IsLink.left_mem, Graph.IsInducedSubgraph.le
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
tfae_1_to_2 : ∀ (a : x ∈ V(H)), y ∈ V(H)
tfae_2_to_3 : ∀ (a : y ∈ V(H)), e ∈ E(H)
tfae_3_to_1 : ∀ (a : e ∈ E(H)), x ∈ V(H)
⊢ [x ∈ V(H), y ∈ V(H), e ∈ E(H)].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
G H : Graph α β
hx : x ∈ V(H)
hHG : H ≤c G
⊢ H.Adj x y ↔ G.Adj x y

Tactic:
⟨(·.mono hHG.le), fun ⟨_, hxy⟩ ↦ (hHG.isLink_congr hx |>.mpr hxy).adj⟩

Premises used: Iff.mpr, Graph.Adj.mono, Graph.IsClosedSubgraph.isLink_congr, Graph.IsLink.adj, Graph.IsClosedSubgraph.isInducedSubgraph, Graph.Adj, Graph.IsInducedSubgraph.le, Iff.intro, _private.0.Graph.IsInducedSubgraph.adj_congr.match_1
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
G H : Graph α β
hxy : G.Adj x y
hHG : H ≤c G
⊢ x ∈ V(H) ↔ y ∈ V(H)

Tactic:
hHG.mem_iff_of_isLink hxy.choose_spec

Premises used: Exists.choose_spec, Graph.IsClosedSubgraph.mem_iff_of_isLink
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G G₁ H : Graph α β
hHG₁ : H ≤ G₁
hG₁ : G₁ ≤ G
hHG : H ≤c G
⊢ H ≤c G₁

Tactic:
mk' hHG₁ fun _ _ he hx ↦ hHG.inc_congr hx |>.mpr (he.mono hG₁) |>.edge_mem

Premises used: Iff.mpr, Graph.IsClosedSubgraph.mk', Graph.IsClosedSubgraph.inc_congr, Graph.Inc.mono, Graph.Inc.edge_mem
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤i G
contrapose! : H ≤c G ↔ ∀ (x y : α) (_ : G.Adj x y) (_ : x ∈ V(H)), y ∈ V(H)
⊢ ¬H ≤c G ↔ ∃ (x : α) (y : α), G.Adj x y ∧ x ∈ V(H) ∧ y ∉ V(H)

Tactic:
contrapose!
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤i G
symm : (∀ (x y : α) (_ : G.Adj x y) (_ : x ∈ V(H)), y ∈ V(H)) ↔ H ≤c G
⊢ H ≤c G ↔ ∀ (x y : α) (_ : G.Adj x y) (_ : x ∈ V(H)), y ∈ V(H)

Tactic:
symm
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤i G
⊢ (∀ (x y : α) (_ : G.Adj x y) (_ : x ∈ V(H)), y ∈ V(H)) ↔ H ≤c G

Tactic:
⟨fun hncl ↦ ⟨hHG, fun e x ⟨y, hexy⟩ hxH =>
    hHG.isLink_of_mem_mem hexy hxH (hncl x y ⟨e, hexy⟩ hxH) |>.edge_mem⟩,
    fun hcl _ _ hexy ↦ (hcl.mem_iff_of_adj hexy).mp⟩

Premises used: Graph.IsLink.edge_mem, Graph.IsClosedSubgraph.mk, Membership.mem, _private.0.Graph.IsInducedSubgraph.not_isClosedSubgraph_iff_exists_adj.match_1, Graph.IsClosedSubgraph.mem_iff_of_adj, Iff.intro, Graph.edgeSet, Exists.intro, Iff.mp, Graph.IsInducedSubgraph.isLink_of_mem_mem
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤i G
⊢ (∀ (x y : α) (_ : G.Adj x y) (_ : x ∈ V(H)), y ∈ V(H)) ↔ H ≤c G

Tactic:
exact ⟨fun hncl ↦ ⟨hHG, fun e x ⟨y, hexy⟩ hxH =>
    hHG.isLink_of_mem_mem hexy hxH (hncl x y ⟨e, hexy⟩ hxH) |>.edge_mem⟩,
    fun hcl _ _ hexy ↦ (hcl.mem_iff_of_adj hexy).mp⟩
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤i G
rw :
  (∃ (x : α) (y : α), G.Adj x y ∧ x ∈ V(H) ∧ y ∉ V(H)) ↔ ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)
⊢ ¬H ≤c G ↔ ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∉ V(H)

Tactic:
rw [hHG.not_isClosedSubgraph_iff_exists_adj]

Premises used: Graph.IsInducedSubgraph.not_isClosedSubgraph_iff_exists_adj
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G_1 G₁ G₂ H H₁ H₂ K : Graph α β
F F₁ F₂ : Set β
X Y : Set α
G : Graph α β
vertexSet_mono : autoParam (V(noEdge ∅ β) ⊆ V(G)) IsSubgraph.vertexSet_mono._autoParam
isLink_mono :
  autoParam (∀ ⦃e : β⦄ ⦃x y : α⦄, IsLink (noEdge ∅ β) e x y → G.IsLink e x y) IsSubgraph.isLink_mono._autoParam
⊢ noEdge ∅ β ≤ G

Tactic:
constructor
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G_1 G₁ G₂ H H₁ H₂ K : Graph α β
F F₁ F₂ : Set β
X Y : Set α
G : Graph α β
⊢ autoParam (V(noEdge ∅ β) ⊆ V(G)) IsSubgraph.vertexSet_mono._autoParam

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G_1 G₁ G₂ H H₁ H₂ K : Graph α β
F F₁ F₂ : Set β
X Y : Set α
G : Graph α β
⊢ autoParam (∀ ⦃e : β⦄ ⦃x y : α⦄, IsLink (noEdge ∅ β) e x y → G.IsLink e x y) IsSubgraph.isLink_mono._autoParam

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
⊢ Eq (α := Graph α β) (noEdge ∅ β) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
⊢ Eq.{u_1 + 1} (α := Set α) (vertexSet.{u_1, u_2} (β := β) ⊥) ∅

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
⊢ Eq.{u_2 + 1} (α := Set β) (edgeSet.{u_1, u_2} (α := α) ⊥) ∅

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
⊢ ∀ ⦃e : β⦄ ⦃x : α⦄,
    G.Inc e x →
      Membership.mem (γ := Set α) (vertexSet.{u_1, u_2} (β := β) ⊥) x →
        Membership.mem (γ := Set β) (edgeSet.{u_1, u_2} (α := α) ⊥) e

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
⊢ G = ⊥ ∨ V(G).Nonempty

Tactic:
(em (V(G) = ∅)).elim (fun he ↦ .inl (Graph.ext he fun e x y ↦ ?_)) (Or.inr ∘
    nonempty_iff_ne_empty.mpr)

Premises used: Iff.mpr, Function.comp, em, Set.nonempty_iff_ne_empty, Or.inl, EmptyCollection.emptyCollection, Or.elim, Graph.vertexSet, Graph.ext, Eq, Or.inr
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
refine : ∀ (he : V(G) = ∅) (e : β) (x y : α), G.IsLink e x y ↔ IsLink ⊥ e x y
⊢ G = ⊥ ∨ V(G).Nonempty

Tactic:
refine (em (V(G) = ∅)).elim (fun he ↦ .inl (Graph.ext he fun e x y ↦ ?_)) (Or.inr ∘
    nonempty_iff_ne_empty.mpr)

Premises used: Iff.mpr, Function.comp, em, Set.nonempty_iff_ne_empty, EmptyCollection.emptyCollection, Or.elim, Graph.vertexSet, Eq, Or.inr
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
he : V(G) = ∅
e : β
x y : α
simp : ¬G.IsLink e x y
⊢ G.IsLink e x y ↔ IsLink ⊥ e x y

Tactic:
simp only [edgeSet_bot, mem_empty_iff_false, not_false_eq_true, not_isLink_of_notMem_edgeSet,
    iff_false]

Premises used: iff_false, Graph.edgeSet_bot, Graph.not_isLink_of_notMem_edgeSet, Set.mem_empty_iff_false, not_false_eq_true
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
he : V(G) = ∅
e : β
x y : α
h : G.IsLink e x y
⊢ False

Tactic:
simpa [he] using h.left_mem

Premises used: Graph.IsLink.left_mem
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
he : V(G) = ∅
e : β
x y : α
⊢ ¬G.IsLink e x y

Tactic:
exact fun h ↦ by simpa [he] using h.left_mem
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
h : V(G) = ∅
⊢ V(G) ⊆ vertexSet.{u_1, u_2} (β := β) ⊥

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
h : G = ⊥
⊢ V(G) = ∅

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
refine : ∀ (h : V(G) = ∅) (e : β) (x y : α) (he : G.IsLink e x y), IsLink ⊥ e x y
⊢ V(G) = ∅ ↔ G = ⊥

Tactic:
refine ⟨fun h ↦ bot_le.antisymm' ⟨by simp [h], fun e x y he ↦ ?_⟩, fun h ↦ by simp [h]⟩
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
h : V(G) = ∅
e : β
x y : α
he : G.IsLink e x y
⊢ IsLink ⊥ e x y

Tactic:
simpa [h] using he.left_mem

Premises used: Graph.IsLink.left_mem
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
⊢ ¬G ≠ ⊥ ↔ ¬V(G).Nonempty

Tactic:
simp [vertexSet_eq_empty_iff, not_nonempty_iff_eq_empty]

Premises used: Graph.vertexSet_eq_empty_iff, Set.not_nonempty_iff_eq_empty
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
⊢ ¬V(G).Nonempty ↔ G = ⊥

Tactic:
simp [vertexSet_eq_empty_iff, not_nonempty_iff_eq_empty]

Premises used: Graph.vertexSet_eq_empty_iff, Set.not_nonempty_iff_eq_empty
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x : α
G : Graph α β
h : x ∈ V(G)
⊢ G ≠ ⊥

Tactic:
ne_bot_iff.mpr ⟨x, h⟩

Premises used: Iff.mpr, Graph.ne_bot_iff, Exists.intro
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
⊢ G ≤s ⊥ ↔ G = ⊥

Tactic:
⟨fun h => le_bot_iff.mp h.le, fun h => h ▸ .rfl⟩

Premises used: le_bot_iff, Eq.rec, Graph.IsSpanningSubgraph.rfl, Iff.intro, Iff.mp, Graph.IsSpanningSubgraph.le
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
⊢ G ≤i ⊥ ↔ G = ⊥

Tactic:
⟨fun h => le_bot_iff.mp h.le, fun h => h ▸ .rfl⟩

Premises used: le_bot_iff, Eq.rec, Graph.IsInducedSubgraph.le, Iff.intro, Iff.mp, Graph.IsInducedSubgraph.rfl
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
⊢ G ≤c ⊥ ↔ G = ⊥

Tactic:
⟨fun h => le_bot_iff.mp h.le, fun h => h ▸ .rfl⟩

Premises used: le_bot_iff, Graph.IsClosedSubgraph.isInducedSubgraph, Eq.rec, Graph.IsClosedSubgraph.rfl, Graph.IsInducedSubgraph.le, Iff.intro, Iff.mp
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x : α
G H : Graph α β
h : x ∈ V(G)
h' : x ∈ V(H)
simp : ∃ (x : Graph α β) (_ : x ≤ G) (_ : x ≤ H), V(x).Nonempty
⊢ ¬Disjoint G H

Tactic:
simp only [Disjoint, le_bot_iff, not_forall, ne_eq, ne_bot_iff]

Premises used: le_bot_iff, Graph.ne_bot_iff, Disjoint, ne_eq, Classical.not_forall
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x : α
G H : Graph α β
h : x ∈ V(G)
h' : x ∈ V(H)
h₁ : ∃ (_ : noEdge {x} β ≤ G) (_ : noEdge {x} β ≤ H), Set.Nonempty (α := α) V(noEdge {x} β)
⊢ ∃ (x : Graph α β) (_ : x ≤ G) (_ : x ≤ H), V(x).Nonempty

Tactic:
use noEdge {x} β

Premises used: Graph.noEdge, Singleton.singleton
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x : α
G H : Graph α β
h : x ∈ V(G)
h' : x ∈ V(H)
⊢ ∃ (_ : noEdge {x} β ≤ G) (_ : noEdge {x} β ≤ H), Set.Nonempty (α := α) V(noEdge {x} β)

Tactic:
simp [h, h']
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
l : Subspace η α ι
x : η → α
i : ι
⊢ (↑l : (x : η → α) → (i : ι) → α) x i = Sum.elim id x (l.idxFun i)

Tactic:
rfl

Premises used: Combinatorics.Subspace.toFun, rfl
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
l m : Subspace η α ι
hlm : (↑l : (x : η → α) → (i : ι) → α) = (↑m : (x : η → α) → (i : ι) → α)
idxFun : ∀ (i : ι), l.idxFun i = m.idxFun i
⊢ l = m

Tactic:
ext i
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
l m : Subspace η α ι
hlm : (↑l : (x : η → α) → (i : ι) → α) = (↑m : (x : η → α) → (i : ι) → α)
i : ι
⊢ ∀ (x : η → α) (x_1 : ι), (↑l : (x : η → α) → (i : ι) → α) x x_1 = (↑m : (x : η → α) → (i : ι) → α) x x_1

Tactic:
simp only [funext_iff] at hlm

Premises used: funext_iff
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), (↑l : (x : η → α) → (i : ι) → α) x x_1 = (↑m : (x : η → α) → (i : ι) → α) x x_1
a : α
hl : l.idxFun i = Sum.inl a
idxFun : ∀ (b : α) (hba : b ≠ a), Sum.inl a = m.idxFun i
⊢ Sum.inl a = m.idxFun i

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

Premises used: exists_ne
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), (↑l : (x : η → α) → (i : ι) → α) x x_1 = (↑m : (x : η → α) → (i : ι) → α) x x_1
a : α
hl : l.idxFun i = Sum.inl a
b : α
hba : b ≠ a
idxFun : ∀ (val : α) (hm : m.idxFun i = Sum.inl val), Eq (α := α ⊕ η) (Sum.inl a) (Sum.inl val)
idxFun₁ : ∀ (val : η) (hm : m.idxFun i = Sum.inr val), Sum.inl a = Sum.inr val
⊢ Sum.inl a = m.idxFun i

Tactic:
cases hm : idxFun m i

Premises used: Combinatorics.Subspace.idxFun
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), (↑l : (x : η → α) → (i : ι) → α) x x_1 = (↑m : (x : η → α) → (i : ι) → α) x x_1
a : α
hl : l.idxFun i = Sum.inl a
b : α
hba : b ≠ a
val : α
hm : m.idxFun i = Sum.inl val
⊢ Eq (α := α ⊕ η) (Sum.inl a) (Sum.inl val)

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

Premises used: Ne.symm, Function.const, Combinatorics.Subspace.coe_apply
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), (↑l : (x : η → α) → (i : ι) → α) x x_1 = (↑m : (x : η → α) → (i : ι) → α) x x_1
a : α
hl : l.idxFun i = Sum.inl a
b : α
hba : b ≠ a
val : η
hm : m.idxFun i = Sum.inr val
⊢ Sum.inl a = Sum.inr val

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

Premises used: Ne.symm, Function.const, Combinatorics.Subspace.coe_apply
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), (↑l : (x : η → α) → (i : ι) → α) x x_1 = (↑m : (x : η → α) → (i : ι) → α) x x_1
e : η
hl : l.idxFun i = Sum.inr e
a : α
hm : m.idxFun i = Sum.inl a
idxFun : ∀ (b : α) (hba : b ≠ a), Sum.inr e = Sum.inl a
⊢ Sum.inr e = Sum.inl a

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

Premises used: exists_ne
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), (↑l : (x : η → α) → (i : ι) → α) x x_1 = (↑m : (x : η → α) → (i : ι) → α) 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

Premises used: Function.const, Combinatorics.Subspace.coe_apply
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), (↑l : (x : η → α) → (i : ι) → α) x x_1 = (↑m : (x : η → α) → (i : ι) → α) x x_1
e : η
hl : l.idxFun i = Sum.inr e
f : η
hm : m.idxFun i = Sum.inr f
idxFun : ∀ (a b : α) (hab : a ≠ b), Eq (α := α ⊕ η) (Sum.inr e) (Sum.inr f)
⊢ Eq (α := α ⊕ η) (Sum.inr e) (Sum.inr f)

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

Premises used: exists_pair_ne
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), (↑l : (x : η → α) → (i : ι) → α) x x_1 = (↑m : (x : η → α) → (i : ι) → α) x x_1
e : η
hl : l.idxFun i = Sum.inr e
f : η
hm : m.idxFun i = Sum.inr f
a b : α
hab : a ≠ b
idxFun : e = f
⊢ Eq (α := α ⊕ η) (Sum.inr e) (Sum.inr f)

Tactic:
simp only [Sum.inr.injEq]

Premises used: Sum.inr.injEq
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), (↑l : (x : η → α) → (i : ι) → α) x x_1 = (↑m : (x : η → α) → (i : ι) → α) x x_1
e : η
hl : l.idxFun i = Sum.inr e
f : η
hm : m.idxFun i = Sum.inr f
a b : α
hab : a ≠ b
idxFun : ∀ (hef : e ≠ f), False
⊢ e = f

Tactic:
by_contra! hef
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), (↑l : (x : η → α) → (i : ι) → α) x x_1 = (↑m : (x : η → α) → (i : ι) → α) 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

Premises used: Function.update, Function.const, Combinatorics.Subspace.coe_apply
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), (↑l : (x : η → α) → (i : ι) → α) x x_1 = (↑m : (x : η → α) → (i : ι) → α) x x_1
e : η
hl : l.idxFun i = Sum.inr e
idxFun : ∀ (x : α ⊕ η) (hm : m.idxFun i = x), Sum.inr e = x
⊢ 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

Premises used: Combinatorics.Subspace.idxFun, Sum.inr.injEq, Combinatorics.Subspace.coe_apply, exists_pair_ne
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), (↑l : (x : η → α) → (i : ι) → α) x x_1 = (↑m : (x : η → α) → (i : ι) → α) x x_1
idxFun : ∀ (x : α ⊕ η) (hl : l.idxFun i = x), x = m.idxFun i
⊢ 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

Premises used: Combinatorics.Subspace.idxFun, Sum.inr.injEq, Combinatorics.Subspace.coe_apply, exists_pair_ne
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
inst : Nontrivial α
rintro : ∀ ⦃l m : Subspace η α ι⦄ (hlm : (↑l : (x : η → α) → (i : ι) → α) = (↑m : (x : η → α) → (i : ι) → α)), l = m
idxFun :
  ∀ ⦃l m : Subspace η α ι⦄ (hlm : (↑l : (x : η → α) → (i : ι) → α) = (↑m : (x : η → α) → (i : ι) → α)) (i : ι),
    l.idxFun i = m.idxFun i
idxFun₁ :
  ∀ ⦃l m : Subspace η α ι⦄ (i : ι)
    (hlm : ∀ (x : η → α) (x_1 : ι), (↑l : (x : η → α) → (i : ι) → α) x x_1 = (↑m : (x : η → α) → (i : ι) → α) x x_1),
    l.idxFun i = m.idxFun i
⊢ Injective (α := Subspace η α ι) 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

Premises used: Sum.inr.injEq, funext_iff, Combinatorics.Subspace.coe_apply, exists_pair_ne
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
l : Subspace η α ι
x : η → α
i : ι
a : α
h : l.idxFun i = Sum.inl a
⊢ (↑l : (x : η → α) → (i : ι) → α) x i = a

Tactic:
simp [apply_def, h]

Premises used: Combinatorics.Subspace.apply_def
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
l : Subspace η α ι
x : η → α
i : ι
e : η
h : l.idxFun i = Sum.inr e
⊢ (↑l : (x : η → α) → (i : ι) → α) x i = x e

Tactic:
simp [apply_def, h]

Premises used: Combinatorics.Subspace.apply_def
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
η_1 : Type u_1
α_1 : Type u_2
ι_1 : Type u_3
κ_1 : Type u_4
η : Type u_5
α : Type u_6
ι : Type u_7
κ : Type u_8
l_1 : Subspace η α ι
x : η → α
i_1 : ι
a : α
e_1 : η
η' : Type u_9
α' : Type u_10
ι' : Type u_11
l : Subspace η α ι
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
e : η'
i : ι
inl :
  ∀ (val : α) (h : l.idxFun i = Sum.inl val),
    Eq (α := α ⊕ η) (Sum.inl val : α ⊕ η) (Sum.inr ((eη.symm : (a : η') → η) e) : α ⊕ η) ↔
      Eq (α := α' ⊕ η')
        (Sum.map (⇑eα : (a : α) → α') (⇑eη : (a : η) → η')
          (l.idxFun ((eι.symm : (a : ι') → ι) ((eι : (a : ι) → ι') i : ι'))))
        (Sum.inr e)
inr :
  ∀ (val : η) (h : l.idxFun i = Sum.inr val),
    Eq (α := α ⊕ η) (Sum.inr val) (Sum.inr ((eη.symm : (a : η') → η) e)) ↔
      Eq (α := α' ⊕ η')
        (Sum.map (⇑eα : (a : α) → α') (⇑eη : (a : η) → η')
          (l.idxFun ((eι.symm : (a : ι') → ι) ((eι : (a : ι) → ι') i : ι'))))
        (Sum.inr e)
⊢ l.idxFun i = Sum.inr ((eη.symm : (a : η') → η) e) ↔
    Eq (α := α' ⊕ η')
      (Sum.map (⇑eα : (a : α) → α') (⇑eη : (a : η) → η')
        (l.idxFun ((eι.symm : (a : ι') → ι) ((eι : (a : ι) → ι') i : ι'))))
      (Sum.inr e)

Tactic:
cases h : idxFun l i

Premises used: Combinatorics.Subspace.idxFun
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
η_1 : Type u_1
α_1 : Type u_2
ι_1 : Type u_3
κ_1 : Type u_4
η : Type u_5
α : Type u_6
ι : Type u_7
κ : Type u_8
l_1 : Subspace η α ι
x : η → α
i_1 : ι
a : α
e_1 : η
η' : Type u_9
α' : Type u_10
ι' : Type u_11
l : Subspace η α ι
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
e : η'
i : ι
val : α
h : l.idxFun i = Sum.inl val
⊢ Eq (α := α ⊕ η) (Sum.inl val : α ⊕ η) (Sum.inr ((eη.symm : (a : η') → η) e) : α ⊕ η) ↔
    Eq (α := α' ⊕ η')
      (Sum.map (⇑eα : (a : α) → α') (⇑eη : (a : η) → η')
        (l.idxFun ((eι.symm : (a : ι') → ι) ((eι : (a : ι) → ι') i : ι'))))
      (Sum.inr e)

Tactic:
simp [*, Equiv.eq_symm_apply]

Premises used: Equiv.eq_symm_apply
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
η_1 : Type u_1
α_1 : Type u_2
ι_1 : Type u_3
κ_1 : Type u_4
η : Type u_5
α : Type u_6
ι : Type u_7
κ : Type u_8
l_1 : Subspace η α ι
x : η → α
i_1 : ι
a : α
e_1 : η
η' : Type u_9
α' : Type u_10
ι' : Type u_11
l : Subspace η α ι
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
e : η'
i : ι
val : η
h : l.idxFun i = Sum.inr val
⊢ Eq (α := α ⊕ η) (Sum.inr val) (Sum.inr ((eη.symm : (a : η') → η) e)) ↔
    Eq (α := α' ⊕ η')
      (Sum.map (⇑eα : (a : α) → α') (⇑eη : (a : η) → η')
        (l.idxFun ((eι.symm : (a : ι') → ι) ((eι : (a : ι) → ι') i : ι'))))
      (Sum.inr e)

Tactic:
simp [*, Equiv.eq_symm_apply]

Premises used: Equiv.eq_symm_apply
-- Module: Mathlib.Combinatorics.HalesJewett
Goal:
η : Type u_5
α : Type u_6
ι : Type u_7
η' : Type u_9
α' : Type u_10
ι' : Type u_11
l : Subspace η α ι
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
x : η' → α'
i : ι'
inl :
  ∀ (val : α) (h : l.idxFun ((eι.symm : (a : ι') → ι) i) = Sum.inl val),
    (↑(l.reindex eη eα eι) : (x : η' → α') → (i : ι') → α') x i =
      (eα : (a : α) → α')
        ((↑l : (x : η → α) → (i : ι) → α) ((⇑eα.symm : (a : α') → α) ∘ x ∘ (⇑eη : (a : η) → η'))
          ((eι.symm : (a : ι') → ι) i))
inr :
  ∀ (val : η) (h : l.idxFun ((eι.symm : (a : ι') → ι) i) = Sum.inr val),
    (↑(l.reindex eη eα eι) : (x : η' → α') → (i : ι') → α') x i =
      (eα : (a : α) → α')
        ((↑l : (x : η → α) → (i : ι) → α) ((⇑eα.symm : (a : α') → α) ∘ x ∘ (⇑eη : (a : η) → η'))
          ((eι.symm : (a : ι') → ι) i))
⊢ (↑(l.reindex eη eα eι) : (x : η' → α') → (i : ι') → α') x i =
    (eα : (a : α) → α')
      ((↑l : (x : η → α) → (i : ι) → α) ((⇑eα.symm : (a : α') → α) ∘ x ∘ (⇑eη : (a : η) → η'))
        ((eι.symm : (a : ι') → ι) i))

Tactic:
cases h : l.idxFun (eι.symm i)

Premises used: Combinatorics.Subspace.idxFun, Equiv.symm, DFunLike.coe