awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ
h : ∀ (i : ι) (_ : i ∈ s) (_ : (H i).FiniteIndex), s.card < (H i).index
apply : LT.lt (α := ℚ) (∑ i ∈ s, (↑(H i).index : ℚ)⁻¹) 1
⊢ False

Tactic:
apply (one_le_sum_inv_index_of_leftCoset_cover hcovers).not_gt

Premises used: Subgroup.one_le_sum_inv_index_of_leftCoset_cover, LE.le.not_gt
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ
h : ∀ (i : ι) (_ : i ∈ s) (_ : (H i).FiniteIndex), s.card < (H i).index
hs : s = ∅
⊢ LT.lt (α := ℚ) (∑ i ∈ s, (↑(H i).index : ℚ)⁻¹) 1

Tactic:
simp only [hs, Finset.sum_empty, zero_lt_one]

Premises used: zero_lt_one, Finset.sum_empty
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ
h : ∀ (i : ι) (_ : i ∈ s) (_ : (H i).FiniteIndex), s.card < (H i).index
hs : s.Nonempty
⊢ 0 < s.card

Tactic:
have hs' : 0 < s.card := hs.card_pos
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ
h : ∀ (i : ι) (_ : i ∈ s) (_ : (H i).FiniteIndex), s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
i : ι
hi : i ∈ s
hindex : (H i).index = 0
inl : LT.lt (α := ℚ) (↑0 : ℚ)⁻¹ (↑s.card : ℚ)⁻¹
inl₁ : LT.lt (α := ℚ) 0⁻¹ (↑s.card : ℚ)⁻¹
inl₂ : LT.lt (α := ℚ) 0 (↑s.card : ℚ)⁻¹
inl₃ : LT.lt (α := ℚ) 0 (↑s.card : ℚ)
inl₄ inl₅ inl₆ inl₇ : 0 < s.card
⊢ LT.lt (α := ℚ) (↑(H i).index : ℚ)⁻¹ (↑s.card : ℚ)⁻¹

Tactic:
rwa [hindex, Nat.cast_zero, inv_zero, inv_pos, Nat.cast_pos]

Premises used: Nat.cast_pos, inv_zero, inv_pos, Nat.cast_zero
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ
h : ∀ (i : ι) (_ : i ∈ s) (_ : (H i).FiniteIndex), s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
i : ι
hi : i ∈ s
hindex : (H i).index ≠ 0
⊢ LT.lt (α := ℚ) 0 (↑s.card : ℚ)

Tactic:
exact_mod_cast hs'
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ
h : ∀ (i : ι) (_ : i ∈ s) (_ : (H i).FiniteIndex), s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
i : ι
hi : i ∈ s
hindex : (H i).index ≠ 0
⊢ LT.lt (α := ℚ) (↑s.card : ℚ) (↑(H i).index : ℚ)

Tactic:
exact_mod_cast h i hi ⟨hindex⟩

Premises used: Subgroup.FiniteIndex.mk
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ
h : ∀ (i : ι) (_ : i ∈ s) (_ : (H i).FiniteIndex), s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
i : ι
hi : i ∈ s
hindex : (H i).index ≠ 0
⊢ LT.lt (α := ℚ) (↑(H i).index : ℚ)⁻¹ (↑s.card : ℚ)⁻¹

Tactic:
exact inv_strictAnti₀ (by exact_mod_cast hs') (by exact_mod_cast h i hi ⟨hindex⟩)

Premises used: inv_strictAnti₀
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ
h : ∀ (i : ι) (_ : i ∈ s) (_ : (H i).FiniteIndex), s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
i : ι
hi : i ∈ s
⊢ (H i).index = 0 ∨ (H i).index ≠ 0

Tactic:
cases eq_or_ne (H i).index 0 with
    | inl hindex =>
      rwa [hindex, Nat.cast_zero, inv_zero, inv_pos, Nat.cast_pos]
    | inr hindex =>
      exact inv_strictAnti₀ (by exact_mod_cast hs') (by exact_mod_cast h i hi ⟨hindex⟩)

Premises used: Nat.cast_pos, inv_zero, inv_pos, Subgroup.index, inv_strictAnti₀, eq_or_ne, Nat.cast_zero, OfNat.ofNat
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ
h : ∀ (i : ι) (_ : i ∈ s) (_ : (H i).FiniteIndex), s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
⊢ ∀ i ∈ s, LT.lt (α := ℚ) (↑(H i).index : ℚ)⁻¹ (↑s.card : ℚ)⁻¹

Tactic:
have hlt : ∀ i ∈ s, ((H i).index : ℚ)⁻¹ < (s.card : ℚ)⁻¹ := fun i hi ↦ by
    cases eq_or_ne (H i).index 0 with
    | inl hindex =>
      rwa [hindex, Nat.cast_zero, inv_zero, inv_pos, Nat.cast_pos]
    | inr hindex =>
      exact inv_strictAnti₀ (by exact_mod_cast hs') (by exact_mod_cast h i hi ⟨hindex⟩)
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ
h : ∀ (i : ι) (_ : i ∈ s) (_ : (H i).FiniteIndex), s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
hlt : ∀ i ∈ s, LT.lt (α := ℚ) (↑(H i).index : ℚ)⁻¹ (↑s.card : ℚ)⁻¹
inr : Eq (α := ℚ) (∑ i ∈ s, (↑s.card : ℚ)⁻¹) 1
⊢ LT.lt (α := ℚ) (∑ i ∈ s, (↑(H i).index : ℚ)⁻¹) 1

Tactic:
apply (Finset.sum_lt_sum_of_nonempty hs hlt).trans_eq

Premises used: LT.lt.trans_eq, Finset.sum_lt_sum_of_nonempty
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ
h : ∀ (i : ι) (_ : i ∈ s) (_ : (H i).FiniteIndex), s.card < (H i).index
hs : s.Nonempty
hs' : 0 < s.card
hlt : ∀ i ∈ s, LT.lt (α := ℚ) (↑(H i).index : ℚ)⁻¹ (↑s.card : ℚ)⁻¹
inr : HSMul.hSMul (β := ℚ) s.card (↑s.card : ℚ)⁻¹ = 1
inr₁ : HMul.hMul (α := ℚ) (↑s.card : ℚ) (↑s.card : ℚ)⁻¹ = 1
inr₂ inr₃ : Eq (α := ℚ) 1 1
⊢ Eq (α := ℚ) (∑ i ∈ s, (↑s.card : ℚ)⁻¹) 1

Tactic:
rw [Finset.sum_const, nsmul_eq_mul, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr hs'.ne')]

Premises used: mul_inv_cancel₀, nsmul_eq_mul, Finset.sum_const
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ
h : ∀ (i : ι) (_ : i ∈ s) (_ : (H i).FiniteIndex), s.card < (H i).index
⊢ s = ∅ ∨ s.Nonempty

Tactic:
cases s.eq_empty_or_nonempty with
  | inl hs => simp only [hs, Finset.sum_empty, zero_lt_one]
  | inr hs =>
  have hs' : 0 < s.card := hs.card_pos
  have hlt : ∀ i ∈ s, ((H i).index : ℚ)⁻¹ < (s.card : ℚ)⁻¹ := fun i hi ↦ by
    cases eq_or_ne (H i).index 0 with
    | inl hindex =>
      rwa [hindex, Nat.cast_zero, inv_zero, inv_pos, Nat.cast_pos]
    | inr hindex =>
      exact inv_strictAnti₀ (by exact_mod_cast hs') (by exact_mod_cast h i hi ⟨hindex⟩)
  apply (Finset.sum_lt_sum_of_nonempty hs hlt).trans_eq
  rw [Finset.sum_const, nsmul_eq_mul, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr hs'.ne')]

Premises used: zero_lt_one, nsmul_eq_mul, Finset.sum_empty, Finset.eq_empty_or_nonempty, Finset.sum_const
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : ι → Submodule R M
s : Finset ι
hcovers : Eq.{u_2 + 1} (α := Set M) (⋃ i ∈ s, (↑(p i) : Set M)) Set.univ
⊢ Eq.{u_2 + 1} (α := Set M) (⋃ i ∈ s, HVAdd.hVAdd (α := M) 0 (↑(p i).toAddSubgroup : Set M)) Set.univ

Tactic:
simpa only [zero_vadd] using hcovers

Premises used: zero_vadd
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
k : Type u_1
E : Type u_2
inst : DivisionRing k
inst_1 : Infinite k
inst_2 : AddCommGroup E
inst_3 : Module k E
s : Finset (Subspace k E)
hs : ⊤ ∉ s
hcovers : Eq.{u_2 + 1} (α := Set E) (⋃ p ∈ s, (↑p : Set E)) Set.univ
have : ∀ (p : Subspace k E) (hp : p ∈ s) (hfi : (Submodule.toAddSubgroup p).FiniteIndex), False
⊢ False

Tactic:
have ⟨p, hp, hfi⟩ := Submodule.exists_finiteIndex_of_cover hcovers
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
k : Type u_1
E : Type u_2
inst : DivisionRing k
inst_1 : Infinite k
inst_2 : AddCommGroup E
inst_3 : Module k E
s : Finset (Subspace k E)
hs : ⊤ ∉ s
hcovers : Eq.{u_2 + 1} (α := Set E) (⋃ p ∈ s, (↑p : Set E)) Set.univ
p : Subspace k E
hp : p ∈ s
hfi : (Submodule.toAddSubgroup p).FiniteIndex
⊢ Finite.{u_2 + 1} (E ⧸ p)

Tactic:
have : Finite (E ⧸ p) := AddSubgroup.finite_quotient_of_finiteIndex
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
k : Type u_1
E : Type u_2
inst : DivisionRing k
inst_1 : Infinite k
inst_2 : AddCommGroup E
inst_3 : Module k E
s : Finset (Subspace k E)
hs : ⊤ ∉ s
hcovers : Eq.{u_2 + 1} (α := Set E) (⋃ p ∈ s, (↑p : Set E)) Set.univ
p : Subspace k E
hp : p ∈ s
hfi : (Submodule.toAddSubgroup p).FiniteIndex
this : Finite.{u_2 + 1} (E ⧸ p)
⊢ Nontrivial.{u_2} (E ⧸ p)

Tactic:
have : Nontrivial (E ⧸ p) := Submodule.Quotient.nontrivial_iff.mpr (ne_of_mem_of_not_mem hp hs)
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
k : Type u_1
E : Type u_2
inst : DivisionRing k
inst_1 : Infinite k
inst_2 : AddCommGroup E
inst_3 : Module k E
s : Finset (Subspace k E)
hs : ⊤ ∉ s
hcovers : Eq.{u_2 + 1} (α := Set E) (⋃ p ∈ s, (↑p : Set E)) Set.univ
p : Subspace k E
hp : p ∈ s
hfi : (Submodule.toAddSubgroup p).FiniteIndex
this_1 : Finite.{u_2 + 1} (E ⧸ p)
this : Nontrivial.{u_2} (E ⧸ p)
⊢ Infinite.{u_2 + 1} (E ⧸ p)

Tactic:
have : Infinite (E ⧸ p) := Module.Free.infinite k (E ⧸ p)
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
k : Type u_1
E : Type u_2
inst : DivisionRing k
inst_1 : Infinite k
inst_2 : AddCommGroup E
inst_3 : Module k E
s : Finset (Subspace k E)
hs : ⊤ ∉ s
hcovers : Eq.{u_2 + 1} (α := Set E) (⋃ p ∈ s, (↑p : Set E)) Set.univ
p : Subspace k E
hp : p ∈ s
hfi : (Submodule.toAddSubgroup p).FiniteIndex
this_1 : Finite.{u_2 + 1} (E ⧸ p)
this_2 : Nontrivial.{u_2} (E ⧸ p)
this : Infinite.{u_2 + 1} (E ⧸ p)
⊢ False

Tactic:
not_finite (E ⧸ p)

Premises used: HasQuotient.Quotient, not_finite
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
k : Type u_1
E : Type u_2
inst : DivisionRing k
inst_1 : Infinite k
inst_2 : AddCommGroup E
inst_3 : Module k E
s : Finset (Subspace k E)
hs : ⊤ ∉ s
hcovers : Eq.{u_2 + 1} (α := Set E) (⋃ p ∈ s, (↑p : Set E)) Set.univ
p : Subspace k E
hp : p ∈ s
hfi : (Submodule.toAddSubgroup p).FiniteIndex
this_1 : Finite.{u_2 + 1} (E ⧸ p)
this_2 : Nontrivial.{u_2} (E ⧸ p)
this : Infinite.{u_2 + 1} (E ⧸ p)
⊢ False

Tactic:
exact not_finite (E ⧸ p)

Premises used: HasQuotient.Quotient, not_finite
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
k : Type u_1
E : Type u_2
inst : DivisionRing k
inst_1 : Infinite k
inst_2 : AddCommGroup E
inst_3 : Module k E
s : Finset (Subspace k E)
hcovers : Eq.{u_2 + 1} (α := Set E) (⋃ p ∈ s, (↑p : Set E)) Set.univ
contrapose! : ∀ (hcovers : ⊤ ∉ s), Ne.{u_2 + 1} (α := Set E) (⋃ p ∈ s, (↑p : Set E)) Set.univ
⊢ ⊤ ∈ s

Tactic:
contrapose! hcovers
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
k : Type u_1
E : Type u_2
inst : DivisionRing k
inst_1 : Infinite k
inst_2 : AddCommGroup E
inst_3 : Module k E
s : Finset (Subspace k E)
hcovers : ⊤ ∉ s
⊢ Ne.{u_2 + 1} (α := Set E) (⋃ p ∈ s, (↑p : Set E)) Set.univ

Tactic:
Subspace.biUnion_ne_univ_of_top_notMem hcovers

Premises used: Subspace.biUnion_ne_univ_of_top_notMem
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
k : Type u_1
E : Type u_2
inst : DivisionRing k
inst_1 : Infinite k
inst_2 : AddCommGroup E
inst_3 : Module k E
s : Finset (Subspace k E)
hcovers : ⊤ ∉ s
⊢ Ne.{u_2 + 1} (α := Set E) (⋃ p ∈ s, (↑p : Set E)) Set.univ

Tactic:
exact Subspace.biUnion_ne_univ_of_top_notMem hcovers

Premises used: Subspace.biUnion_ne_univ_of_top_notMem
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
k : Type u_1
E : Type u_2
inst : DivisionRing k
inst_1 : Infinite k
inst_2 : AddCommGroup E
inst_3 : Module k E
ι : Sort u_3
inst_4 : Finite ι
p : ι → Subspace k E
hcovers : Eq.{u_2 + 1} (α := Set E) (⋃ (i : ι), (↑(p i) : Set E)) Set.univ
have : ∀ (this : Fintype (↑(Set.range p) : Type u_2)), ∃ (i : ι), p i = ⊤
⊢ ∃ (i : ι), p i = ⊤

Tactic:
have := Fintype.ofFinite (Set.range p)
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
k : Type u_1
E : Type u_2
inst : DivisionRing k
inst_1 : Infinite k
inst_2 : AddCommGroup E
inst_3 : Module k E
ι : Sort u_3
inst_4 : Finite ι
p : ι → Subspace k E
hcovers : Eq.{u_2 + 1} (α := Set E) (⋃ (i : ι), (↑(p i) : Set E)) Set.univ
this : Fintype (↑(Set.range p) : Type u_2)
⊢ Eq.{u_2 + 1} (α := Set E) (⋃ x ∈ (Set.range p).toFinset, (↑x : Set E)) Set.univ

Tactic:
simp_rw [← Set.biUnion_range (f := p), ← Set.mem_toFinset] at hcovers

Premises used: Set.biUnion_range, Set.mem_toFinset
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
k : Type u_1
E : Type u_2
inst : DivisionRing k
inst_1 : Infinite k
inst_2 : AddCommGroup E
inst_3 : Module k E
ι : Sort u_3
inst_4 : Finite ι
p : ι → Subspace k E
this : Fintype (↑(Set.range p) : Type u_2)
hcovers : Eq.{u_2 + 1} (α := Set E) (⋃ x ∈ (Set.range p).toFinset, (↑x : Set E)) Set.univ
⊢ ∃ (i : ι), p i = ⊤

Tactic:
apply Set.mem_toFinset.mp (Subspace.top_mem_of_biUnion_eq_univ hcovers)

Premises used: Iff.mp, Subspace.top_mem_of_biUnion_eq_univ, Set.mem_toFinset
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
M' : CoxeterMatrix B' := CoxeterMatrix.reindex e M
⊢ Set.range (uncurry M'.relation) =
    Set.range.{u_2, u_1 + 1} (ι := B × B) (uncurry M'.relation ∘ Prod.map (⇑e : (a : B) → B') (⇑e : (a : B) → B'))

Tactic:
simp [Set.range_comp]

Premises used: Set.range_comp
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
M' : CoxeterMatrix B' := CoxeterMatrix.reindex e M
apply :
  uncurry M'.relation ∘ Prod.map (⇑e : (a : B) → B') (⇑e : (a : B) → B') =
    (⇑(FreeGroup.freeGroupCongr e) : (a : FreeGroup B) → FreeGroup B') ∘ uncurry M.relation
⊢ Set.range.{u_2, u_1 + 1} (ι := B × B) (uncurry M'.relation ∘ Prod.map (⇑e : (a : B) → B') (⇑e : (a : B) → B')) =
    Set.range ((⇑(FreeGroup.freeGroupCongr e) : (a : FreeGroup B) → FreeGroup B') ∘ uncurry M.relation)

Tactic:
apply congrArg Set.range

Premises used: congrArg, Set.range
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
M' : CoxeterMatrix B' := CoxeterMatrix.reindex e M
h :
  ∀ (i i' : B),
    (uncurry M'.relation ∘ Prod.map (⇑e : (a : B) → B') (⇑e : (a : B) → B')) (i, i') =
      ((⇑(FreeGroup.freeGroupCongr e) : (a : FreeGroup B) → FreeGroup B') ∘ uncurry M.relation) (i, i')
⊢ uncurry M'.relation ∘ Prod.map (⇑e : (a : B) → B') (⇑e : (a : B) → B') =
    (⇑(FreeGroup.freeGroupCongr e) : (a : FreeGroup B) → FreeGroup B') ∘ uncurry M.relation

Tactic:
ext ⟨i, i'⟩
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
M' : CoxeterMatrix B' := CoxeterMatrix.reindex e M
i i' : B
⊢ (uncurry M'.relation ∘ Prod.map (⇑e : (a : B) → B') (⇑e : (a : B) → B')) (i, i') =
    ((⇑(FreeGroup.freeGroupCongr e) : (a : FreeGroup B) → FreeGroup B') ∘ uncurry M.relation) (i, i')

Tactic:
simp [relation, reindex_apply, M']

Premises used: CoxeterMatrix.reindex_apply, CoxeterMatrix.relation
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
M' : CoxeterMatrix B' := CoxeterMatrix.reindex e M
⊢ Eq.{u_2 + 1} (α := Set (FreeGroup B'))
    (Set.range ((⇑(FreeGroup.freeGroupCongr e) : (a : FreeGroup B) → FreeGroup B') ∘ uncurry M.relation))
    ((⇑(FreeGroup.freeGroupCongr e) : (a : FreeGroup B) → FreeGroup B') '' M.relationsSet)

Tactic:
simp [Set.range_comp, relationsSet]

Premises used: Set.range_comp, CoxeterMatrix.relationsSet
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
⊢ Surjective.{u_1 + 1, u_2 + 1} (α := FreeGroup B) (β := FreeGroup B')
    (⇑(↑(FreeGroup.freeGroupCongr e) : FreeGroup B →* FreeGroup B') : (a : FreeGroup B) → FreeGroup B')

Tactic:
simpa using (FreeGroup.freeGroupCongr e).surjective

Premises used: MulEquiv.surjective, FreeGroup.freeGroupCongr
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
rw :
  Eq (α := Subgroup (FreeGroup B'))
    (Subgroup.map (↑(FreeGroup.freeGroupCongr e) : FreeGroup B →* FreeGroup B') (Subgroup.normalClosure M.relationsSet))
    (Subgroup.normalClosure ((⇑(FreeGroup.freeGroupCongr e) : (a : FreeGroup B) → FreeGroup B') '' M.relationsSet))
rw₁ :
  Eq.{u_2 + 1} (α := Subgroup (FreeGroup B'))
    (Subgroup.normalClosure
      ((⇑(↑(FreeGroup.freeGroupCongr e) : FreeGroup B →* FreeGroup B') : (a : FreeGroup B) → FreeGroup B') ''
        M.relationsSet))
    (Subgroup.normalClosure ((⇑(FreeGroup.freeGroupCongr e) : (a : FreeGroup B) → FreeGroup B') '' M.relationsSet))
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := Subgroup (FreeGroup B'))
    (Subgroup.normalClosure ((⇑(FreeGroup.freeGroupCongr e) : (a : FreeGroup B) → FreeGroup B') '' M.relationsSet))
    (Subgroup.normalClosure ((⇑(FreeGroup.freeGroupCongr e) : (a : FreeGroup B) → FreeGroup B') '' M.relationsSet))
⊢ Eq (α := Subgroup (FreeGroup B'))
    (Subgroup.map (↑(FreeGroup.freeGroupCongr e) : FreeGroup B →* FreeGroup B') (Subgroup.normalClosure M.relationsSet))
    (Subgroup.normalClosure (CoxeterMatrix.reindex e M).relationsSet)

Tactic:
rw [reindex_relationsSet,
        Subgroup.map_normalClosure _ _ (by simpa using (FreeGroup.freeGroupCongr e).surjective),
        MonoidHom.coe_coe]

Premises used: CoxeterMatrix.reindex_relationsSet, MonoidHom.coe_coe, Subgroup.map_normalClosure
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
i : B'
⊢ (M.reindexGroupEquiv e : (a : (CoxeterMatrix.reindex e M).Group) → M.Group) ((CoxeterMatrix.reindex e M).simple i) =
    M.simple ((e.symm : (a : B') → B) i)

Tactic:
rfl

Premises used: FreeGroup.of, CoxeterMatrix.simple, Quotient.liftOn', PresentedGroup.of, List.map, Con.liftOn, FreeGroup.mk, Quot.map, rfl
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
i : B
⊢ ((M.reindexGroupEquiv e).symm : (a : M.Group) → (CoxeterMatrix.reindex e M).Group) (M.simple i) =
    (CoxeterMatrix.reindex e M).simple ((e : (a : B) → B') i)

Tactic:
rfl

Premises used: FreeGroup.of, CoxeterMatrix.simple, Quotient.liftOn', PresentedGroup.of, List.map, Con.liftOn, FreeGroup.mk, Quot.map, rfl
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
M : CoxeterMatrix B
⊢ M.toCoxeterSystem.simple = M.simple

Tactic:
rfl

Premises used: CoxeterMatrix.simple, PresentedGroup.of, rfl
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i' : B'
⊢ (cs.reindex e).simple i' = cs.simple ((e.symm : (a : B') → B) i')

Tactic:
rfl

Premises used: FreeGroup.of, Quotient.liftOn', CoxeterMatrix.reindex, PresentedGroup.of, List.map, CoxeterSystem.simple, Con.liftOn, CoxeterSystem.reindex, FreeGroup.mk, Quot.map, rfl
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
H : Type u_4
inst : Group W
inst_1 : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
e : W ≃* H
i : B
⊢ (cs.map e).simple i = (e : (a : W) → H) (cs.simple i)

Tactic:
rfl

Premises used: CoxeterSystem.simple, rfl
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ uncurry M.relation (i, i) = FreeGroup.of i * FreeGroup.of i

Tactic:
simp [relation]

Premises used: CoxeterMatrix.relation
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ FreeGroup.of i * FreeGroup.of i ∈ M.relationsSet

Tactic:
have : (FreeGroup.of i) * (FreeGroup.of i) ∈ M.relationsSet := ⟨(i, i), by simp [relation]⟩
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
this : FreeGroup.of i * FreeGroup.of i ∈ M.relationsSet
⊢ Eq (α := PresentedGroup M.relationsSet)
    ((PresentedGroup.mk M.relationsSet : (a : FreeGroup B) → PresentedGroup M.relationsSet)
        (FreeGroup.of i * FreeGroup.of i) :
      PresentedGroup M.relationsSet)
    (1 : PresentedGroup M.relationsSet)

Tactic:
have : (PresentedGroup.mk _ (FreeGroup.of i * FreeGroup.of i) : M.Group) = 1 :=
    (QuotientGroup.eq_one_iff _).mpr (Subgroup.subset_normalClosure this)
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
this_1 : FreeGroup.of i * FreeGroup.of i ∈ M.relationsSet
this :
  Eq (α := PresentedGroup M.relationsSet)
    ((PresentedGroup.mk M.relationsSet : (a : FreeGroup B) → PresentedGroup M.relationsSet)
        (FreeGroup.of i * FreeGroup.of i) :
      PresentedGroup M.relationsSet)
    (1 : PresentedGroup M.relationsSet)
unfold :
  HMul.hMul (α := W) (β := W)
      ((cs.mulEquiv.symm : (a : M.Group) → W) (PresentedGroup.of (rels := M.relationsSet) i) : W)
      ((cs.mulEquiv.symm : (a : M.Group) → W) (PresentedGroup.of (rels := M.relationsSet) i) : W) =
    1
⊢ cs.simple i * cs.simple i = 1

Tactic:
unfold simple

Premises used: CoxeterSystem.simple
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
this_1 : FreeGroup.of i * FreeGroup.of i ∈ M.relationsSet
this :
  Eq (α := PresentedGroup M.relationsSet)
    ((PresentedGroup.mk M.relationsSet : (a : FreeGroup B) → PresentedGroup M.relationsSet)
        (FreeGroup.of i * FreeGroup.of i) :
      PresentedGroup M.relationsSet)
    (1 : PresentedGroup M.relationsSet)
rw :
  HMul.hMul (α := W) (β := W)
      ((cs.mulEquiv.symm : (a : M.Group) → W)
          ((PresentedGroup.mk M.relationsSet : (a : FreeGroup B) → PresentedGroup M.relationsSet) (FreeGroup.of i) :
            PresentedGroup M.relationsSet) :
        W)
      ((cs.mulEquiv.symm : (a : M.Group) → W)
          ((PresentedGroup.mk M.relationsSet : (a : FreeGroup B) → PresentedGroup M.relationsSet) (FreeGroup.of i) :
            PresentedGroup M.relationsSet) :
        W) =
    1
⊢ HMul.hMul (α := W) (β := W)
      ((cs.mulEquiv.symm : (a : M.Group) → W) (PresentedGroup.of (rels := M.relationsSet) i) : W)
      ((cs.mulEquiv.symm : (a : M.Group) → W) (PresentedGroup.of (rels := M.relationsSet) i) : W) =
    1

Tactic:
rw [← map_mul, PresentedGroup.of, map_mul]

Premises used: PresentedGroup.of, map_mul
-- Module: Mathlib.GroupTheory.Coxeter.Basic
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
this_1 : FreeGroup.of i * FreeGroup.of i ∈ M.relationsSet
this :
  Eq (α := PresentedGroup M.relationsSet)
    ((PresentedGroup.mk M.relationsSet : (a : FreeGroup B) → PresentedGroup M.relationsSet)
        (FreeGroup.of i * FreeGroup.of i) :
      PresentedGroup M.relationsSet)
    (1 : PresentedGroup M.relationsSet)
⊢ HMul.hMul (α := W) (β := W)
      ((cs.mulEquiv.symm : (a : M.Group) → W)
          ((PresentedGroup.mk M.relationsSet : (a : FreeGroup B) → PresentedGroup M.relationsSet) (FreeGroup.of i) :
            PresentedGroup M.relationsSet) :
        W)
      ((cs.mulEquiv.symm : (a : M.Group) → W)
          ((PresentedGroup.mk M.relationsSet : (a : FreeGroup B) → PresentedGroup M.relationsSet) (FreeGroup.of i) :
            PresentedGroup M.relationsSet) :
        W) =
    1

Tactic:
map_mul_eq_one cs.mulEquiv.symm this

Premises used: CoxeterSystem.mulEquiv, map_mul_eq_one, MulEquiv.symm