awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
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
inst_1 : DecidablePred (α := Subgroup G) FiniteIndex
D : Subgroup G := ⨅ k ∈ {i ∈ s | (H i).FiniteIndex}, H k
hD : D.FiniteIndex
hD_le : ∀ {i : ι} (hi : i ∈ s) (hfi : (H i).FiniteIndex), D ≤ H i
t : (i : ι) → (hi : i ∈ s) → (hfi : (H i).FiniteIndex) → Finset ↥(H i)
ht :
  ∀ (i : ι) (hi : i ∈ s) (hfi : (H i).FiniteIndex),
    IsComplement (↑(t i hi hfi) : Set ↥(H i)) (↑(D.subgroupOf (H i)) : Set ↥(H i)) ∧
      ⋃ g ∈ t i hi hfi, (↑g : G) • (↑D : Set G) = (↑(H i) : Set G)
κ : Type (max u_2 u_1) := (i : ↥s) × ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1})
f : (k : κ) → G :=
  fun (k : κ) ↦
    g (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι) *
      (↑(↑(k.snd (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) :
            ↥(H (↑k.fst : ι))) :
        G)
K : (k : κ) → Subgroup G :=
  fun (k : κ) ↦
    if
        (H
            (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) :
              ι)).FiniteIndex then
      D
    else H (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι)
k : κ
hkfi :
  (H (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι)).FiniteIndex
hk : K k = D
hcovers' :
  Eq.{u_1 + 1} (α := Set G) (⋃ (i : κ), ⋃ (_ : Membership.mem (γ := Finset κ) {x : κ | K x = D} i), f i • (↑D : Set G))
    Set.univ
hHD : ∀ (i : ι), ¬(H i).FiniteIndex → H i ≠ D
hdensity :
  ∑ i ∈ s, (↑(H i).index : ℚ)⁻¹ = HMul.hMul (α := ℚ) (↑(Finset.card (α := κ) {x : κ | K x = D}) : ℚ) (↑D.index : ℚ)⁻¹
h : Finset.card (α := κ) {x : κ | K x = D} = D.index
i : ι
hi : i ∈ s ∧ (H i).FiniteIndex
j : ι
hj : j ∈ s ∧ (H j).FiniteIndex
hij : i ≠ j
c : Set G
hi' : c ≤ (fun (i : ι) ↦ g i • (↑(H i) : Set G)) i
hj' : c ≤ (fun (i : ι) ↦ g i • (↑(H i) : Set G)) j
x : G
hx : x ∈ c
hdisjoint : (↑{x : κ | K x = D} : Set κ).PairwiseDisjoint (α := Set G) fun (x : κ) ↦ f x • (↑D : Set G)
hk' :
  ∀ (i : ι) (hi : i ∈ s ∧ (H i).FiniteIndex) (hi' : c ≤ g i • (↑(H i) : Set G)),
    ∃ (k : κ),
      (↑(k.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι) = i ∧
        K k = D ∧ x ∈ f k • (↑D : Set G)
k₁ : κ
hik₁ : (↑(k₁.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) ⋯ h else {1}))) : ι) = i
hk₁ : K k₁ = D
hxk₁ : x ∈ f k₁ • (↑D : Set G)
⊢ Membership.mem (γ := Set G) ⊥ x
have refine_3 : ∀ (k₂ : κ)
  (hjk₂ : (↑(k₂.fst (β := fun (i : ↥s) ↦ ↥(if h : (H (↑i : ι)).FiniteIndex then t (↑i : ι) sorry h else {1}))) : ι) = j)
  (hk₂ : K k₂ = D) (hxk₂ : x ∈ f k₂ • (↑D : Set G)), Membership.mem (γ := Set G) ⊥ x
Tactic: have ⟨k₂, hjk₂, hk₂, hxk₂⟩ := hk' j hj hj'
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
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
⊢ ∃ i ∈ s, (H i).FiniteIndex ∧ (H i).index ≤ s.card
have by_contra! : ∀ (h : ∀ (i : ι) (_ : i ∈ s) (_ : (H i).FiniteIndex), s.card < (H i).index), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
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
⊢ False
have apply : LT.lt (α := ℚ) (∑ i ∈ s, (↑(H i).index : ℚ)⁻¹) 1
Tactic: apply (one_le_sum_inv_index_of_leftCoset_cover hcovers).not_gt
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (hypothesis)
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
⊢ LT.lt (α := ℚ) (∑ i ∈ s, (↑(H i).index : ℚ)⁻¹) 1
have hs' : 0 < s.card
Tactic: have hs' : 0 < s.card := hs.card_pos
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
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 : ℚ)⁻¹
have inl : LT.lt (α := ℚ) (↑0 : ℚ)⁻¹ (↑s.card : ℚ)⁻¹
Tactic: rwa [hindex, Nat.cast_zero, inv_zero, inv_pos, Nat.cast_pos]
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
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 : ℚ)⁻¹
⊢ LT.lt (α := ℚ) (↑(H i).index : ℚ)⁻¹ (↑s.card : ℚ)⁻¹
have inl₁ : LT.lt (α := ℚ) 0⁻¹ (↑s.card : ℚ)⁻¹
Tactic: rwa [hindex, Nat.cast_zero, inv_zero, inv_pos, Nat.cast_pos]
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
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 : ℚ)⁻¹
⊢ LT.lt (α := ℚ) (↑(H i).index : ℚ)⁻¹ (↑s.card : ℚ)⁻¹
have inl₂ : LT.lt (α := ℚ) 0 (↑s.card : ℚ)⁻¹
Tactic: rwa [hindex, Nat.cast_zero, inv_zero, inv_pos, Nat.cast_pos]
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
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 : ℚ)⁻¹
⊢ LT.lt (α := ℚ) (↑(H i).index : ℚ)⁻¹ (↑s.card : ℚ)⁻¹
have inl₃ : LT.lt (α := ℚ) 0 (↑s.card : ℚ)
Tactic: rwa [hindex, Nat.cast_zero, inv_zero, inv_pos, Nat.cast_pos]
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (hypothesis)
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
⊢ LT.lt (α := ℚ) (↑(H i).index : ℚ)⁻¹ (↑s.card : ℚ)⁻¹
have x : (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⟩)
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (hypothesis)
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
⊢ LT.lt (α := ℚ) (∑ i ∈ s, (↑(H i).index : ℚ)⁻¹) 1
have hlt : ∀ 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⟩)
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
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 : ℚ)⁻¹
⊢ LT.lt (α := ℚ) (∑ i ∈ s, (↑(H i).index : ℚ)⁻¹) 1
have inr : Eq (α := ℚ) (∑ i ∈ s, (↑s.card : ℚ)⁻¹) 1
Tactic: apply (Finset.sum_lt_sum_of_nonempty hs hlt).trans_eq
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
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 : ℚ)⁻¹
⊢ Eq (α := ℚ) (∑ i ∈ s, (↑s.card : ℚ)⁻¹) 1
have inr : HSMul.hSMul (β := ℚ) s.card (↑s.card : ℚ)⁻¹ = 1
Tactic: rw [Finset.sum_const, nsmul_eq_mul, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr hs'.ne')]
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
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
⊢ Eq (α := ℚ) (∑ i ∈ s, (↑s.card : ℚ)⁻¹) 1
have inr₁ : HMul.hMul (α := ℚ) (↑s.card : ℚ) (↑s.card : ℚ)⁻¹ = 1
Tactic: rw [Finset.sum_const, nsmul_eq_mul, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr hs'.ne')]
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
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
⊢ Eq (α := ℚ) (∑ i ∈ s, (↑s.card : ℚ)⁻¹) 1
have inr₂ : Eq (α := ℚ) 1 1
Tactic: rw [Finset.sum_const, nsmul_eq_mul, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr hs'.ne')]
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (hypothesis)
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
⊢ LT.lt (α := ℚ) (∑ i ∈ s, (↑(H i).index : ℚ)⁻¹) 1
have x : 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')]
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
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
⊢ False
have have : ∀ (p : Subspace k E) (hp : p ∈ s) (hfi : (Submodule.toAddSubgroup p).FiniteIndex), False
Tactic: have ⟨p, hp, hfi⟩ := Submodule.exists_finiteIndex_of_cover hcovers
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (hypothesis)
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
⊢ False
have this : Finite.{u_2 + 1} (E ⧸ p)
Tactic: have : Finite (E ⧸ p) := AddSubgroup.finite_quotient_of_finiteIndex
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (hypothesis)
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)
⊢ False
have this₁ : Nontrivial.{u_2} (E ⧸ p)
Tactic: have : Nontrivial (E ⧸ p) := Submodule.Quotient.nontrivial_iff.mpr (ne_of_mem_of_not_mem hp hs)
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (hypothesis)
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)
⊢ False
have this₁ : Infinite.{u_2 + 1} (E ⧸ p)
Tactic: have : Infinite (E ⧸ p) := Module.Free.infinite k (E ⧸ p)
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
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
⊢ ⊤ ∈ s
have contrapose! : ∀ (hcovers : ⊤ ∉ s), Ne.{u_2 + 1} (α := Set E) (⋃ p ∈ s, (↑p : Set E)) Set.univ
Tactic: contrapose! hcovers
Cleared hypotheses: hcovers
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (goal)
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
⊢ ∃ (i : ι), p i = ⊤
have have : ∀ (this : Fintype (↑(Set.range p) : Type u_2)), ∃ (i : ι), p i = ⊤
Tactic: have := Fintype.ofFinite (Set.range p)
-- Lean 4 proof step from Mathlib.GroupTheory.CosetCover (hypothesis)
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)
⊢ ∃ (i : ι), p i = ⊤
have hcovers₁ : 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
Cleared hypotheses: hcovers
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
M' : CoxeterMatrix B' := CoxeterMatrix.reindex e M
⊢ 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)
have 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
Tactic: apply congrArg Set.range
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
M' : CoxeterMatrix B' := CoxeterMatrix.reindex e M
⊢ uncurry M'.relation ∘ Prod.map (⇑e : (a : B) → B') (⇑e : (a : B) → B') =
    (⇑(FreeGroup.freeGroupCongr e) : (a : FreeGroup B) → FreeGroup B') ∘ uncurry M.relation
have 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')
Tactic: ext ⟨i, i'⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
Goal:
B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
⊢ Eq (α := Subgroup (FreeGroup B'))
    (Subgroup.map (↑(FreeGroup.freeGroupCongr e) : FreeGroup B →* FreeGroup B') (Subgroup.normalClosure M.relationsSet))
    (Subgroup.normalClosure (CoxeterMatrix.reindex e M).relationsSet)
have 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))
Tactic: rw [reindex_relationsSet,
        Subgroup.map_normalClosure _ _ (by simpa using (FreeGroup.freeGroupCongr e).surjective),
        MonoidHom.coe_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
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))
⊢ Eq (α := Subgroup (FreeGroup B'))
    (Subgroup.map (↑(FreeGroup.freeGroupCongr e) : FreeGroup B →* FreeGroup B') (Subgroup.normalClosure M.relationsSet))
    (Subgroup.normalClosure (CoxeterMatrix.reindex e M).relationsSet)
have 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))
Tactic: rw [reindex_relationsSet,
        Subgroup.map_normalClosure _ _ (by simpa using (FreeGroup.freeGroupCongr e).surjective),
        MonoidHom.coe_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
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))
⊢ Eq (α := Subgroup (FreeGroup B'))
    (Subgroup.map (↑(FreeGroup.freeGroupCongr e) : FreeGroup B →* FreeGroup B') (Subgroup.normalClosure M.relationsSet))
    (Subgroup.normalClosure (CoxeterMatrix.reindex e M).relationsSet)
have 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))
Tactic: rw [reindex_relationsSet,
        Subgroup.map_normalClosure _ _ (by simpa using (FreeGroup.freeGroupCongr e).surjective),
        MonoidHom.coe_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (hypothesis)
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ cs.simple i * cs.simple i = 1
have this : FreeGroup.of i * FreeGroup.of i ∈ M.relationsSet
Tactic: have : (FreeGroup.of i) * (FreeGroup.of i) ∈ M.relationsSet := ⟨(i, i), by simp [relation]⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (hypothesis)
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
⊢ cs.simple i * cs.simple i = 1
have 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)
Tactic: have : (PresentedGroup.mk _ (FreeGroup.of i * FreeGroup.of i) : M.Group) = 1 :=
    (QuotientGroup.eq_one_iff _).mpr (Subgroup.subset_normalClosure this)
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
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)
⊢ cs.simple i * cs.simple i = 1
have 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
Tactic: unfold simple
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (goal)
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.of (rels := M.relationsSet) i) : W)
      ((cs.mulEquiv.symm : (a : M.Group) → W) (PresentedGroup.of (rels := M.relationsSet) i) : W) =
    1
have 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
Tactic: rw [← map_mul, PresentedGroup.of, map_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (hypothesis)
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
⊢ (cs.simple i * cs.simple i') ^ M.M i i' = 1
have this : (FreeGroup.of i * FreeGroup.of i') ^ M.M i i' ∈ M.relationsSet
Tactic: have : (FreeGroup.of i * FreeGroup.of i') ^ M i i' ∈ M.relationsSet := ⟨(i, i'), rfl⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Basic (hypothesis)
Goal:
B : Type u_1
W : Type u_3
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
this : (FreeGroup.of i * FreeGroup.of i') ^ M.M i i' ∈ M.relationsSet
⊢ (cs.simple i * cs.simple i') ^ M.M i i' = 1
have this₁ : Eq (α := PresentedGroup M.relationsSet)
  ((PresentedGroup.mk M.relationsSet : (a : FreeGroup B) → PresentedGroup M.relationsSet)
      ((FreeGroup.of i * FreeGroup.of i') ^ M.M i i') :
    PresentedGroup M.relationsSet)
  (1 : PresentedGroup M.relationsSet)
Tactic: have : (PresentedGroup.mk _ ((FreeGroup.of i * FreeGroup.of i') ^ M i i') : M.Group) = 1 :=
    (QuotientGroup.eq_one_iff _).mpr (Subgroup.subset_normalClosure this)