awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
j : ℕ
h₁ : cs.length (cs.wordProd (take j ω)) ≤ (take j ω).length
h₂ : cs.length (cs.wordProd (drop j ω)) ≤ (drop j ω).length
⊢ cs.length (cs.wordProd ω) = cs.length (cs.wordProd (take j ω) * cs.wordProd (drop j ω))
have rw : cs.length (cs.wordProd ω) = cs.length (cs.wordProd (take j ω ++ drop j ω))
Tactic: rw [← cs.wordProd_append, ω.take_append_drop j]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
j : ℕ
h₁ : cs.length (cs.wordProd (take j ω)) ≤ (take j ω).length
h₂ : cs.length (cs.wordProd (drop j ω)) ≤ (drop j ω).length
rw : cs.length (cs.wordProd ω) = cs.length (cs.wordProd (take j ω ++ drop j ω))
⊢ cs.length (cs.wordProd ω) = cs.length (cs.wordProd (take j ω) * cs.wordProd (drop j ω))
have rw₁ : cs.length (cs.wordProd ω) = cs.length (cs.wordProd ω)
Tactic: rw [← cs.wordProd_append, ω.take_append_drop j]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (hypothesis)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
j : ℕ
h₁ : cs.length (cs.wordProd (take j ω)) ≤ (take j ω).length
h₂ : cs.length (cs.wordProd (drop j ω)) ≤ (drop j ω).length
⊢ cs.IsReduced (take j ω) ∧ cs.IsReduced (drop j ω)
have h₃ : (take j ω).length + (drop j ω).length ≤ cs.length (cs.wordProd (take j ω)) + cs.length (cs.wordProd (drop j ω))
Tactic: have h₃ := calc
    (ω.take j).length + (ω.drop j).length
    _ = ω.length := by rw [← List.length_append, ω.take_append_drop j]
    _ = ℓ (π ω) := hω.symm
    _ = ℓ (π (ω.take j) * π (ω.drop j)) := by rw [← cs.wordProd_append, ω.take_append_drop j]
    _ ≤ ℓ (π (ω.take j)) + ℓ (π (ω.drop j)) := cs.length_mul_le _ _
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
h : cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) < M.M i i' + 1
⊢ ¬cs.length (cs.wordProd (alternatingWord i i' (M.M i i').succ)) = (alternatingWord i i' (M.M i i').succ).length
have rw : ¬cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) = M.M i i' + 1
Tactic: rw [Nat.succ_eq_add_one, length_alternatingWord]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
⊢ ¬cs.IsReduced (alternatingWord i i' (M.M i i').succ)
have refl : cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) < M.M i i' + 1
Tactic: suffices h : ℓ (π (alternatingWord i i' (M i i' + 1))) < M i i' + 1 by
      unfold IsReduced
      rw [Nat.succ_eq_add_one, length_alternatingWord]
      lia
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
⊢ M.M i i' + 1 ≤ M.M i i' * 2
have linarith : M.M i i' * 2 < M.M i i' + 1 →
  -1 + (HMul.hMul (α := ℤ) (↑(M.M i i') : ℤ) 2 + 1 - HAdd.hAdd (α := ℤ) (↑(M.M i i') : ℤ) 1) +
      HSub.hSub (α := ℤ) 1 (↑(M.M i i') : ℤ) =
    0
Tactic: linarith [Nat.one_le_iff_ne_zero.mpr hM]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (hypothesis)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
⊢ cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) < M.M i i' + 1
have this : M.M i i' + 1 ≤ M.M i i' * 2
Tactic: have : M i i' + 1 ≤ M i i' * 2 := by linarith [Nat.one_le_iff_ne_zero.mpr hM]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
this : M.M i i' + 1 ≤ M.M i i' * 2
⊢ cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) < M.M i i' + 1
have refl : cs.length (cs.wordProd (alternatingWord i' i (M.M i i' * 2 - (M.M i i' + 1)))) < M.M i i' + 1
Tactic: rw [cs.prod_alternatingWord_eq_prod_alternatingWord_sub i i' _ this]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (hypothesis)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
this : M.M i i' + 1 ≤ M.M i i' * 2
⊢ cs.length (cs.wordProd (alternatingWord i' i (M.M i i' * 2 - (M.M i i' + 1)))) < M.M i i' + 1
have this₁ : M.M i i' * 2 - (M.M i i' + 1) = M.M i i' - 1
Tactic: have : M i i' * 2 - (M i i' + 1) = M i i' - 1 := by lia
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
this_1 : M.M i i' + 1 ≤ M.M i i' * 2
this : M.M i i' * 2 - (M.M i i' + 1) = M.M i i' - 1
⊢ cs.length (cs.wordProd (alternatingWord i' i (M.M i i' * 2 - (M.M i i' + 1)))) < M.M i i' + 1
have refl : cs.length (cs.wordProd (alternatingWord i' i (M.M i i' - 1))) < M.M i i' + 1
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m_1 : ℕ
hM : M.M i i' ≠ 0
m_2 : ℕ
m : (M.M i i').succ.le m_2
ih : ¬cs.IsReduced (alternatingWord i i' m_2)
⊢ ¬cs.IsReduced (alternatingWord i i' m_2.succ)
have step : ∀ (ih : cs.IsReduced (alternatingWord i i' m_2.succ)), cs.IsReduced (alternatingWord i i' m_2)
Tactic: contrapose ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (hypothesis)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m_1 : ℕ
hM : M.M i i' ≠ 0
m_2 : ℕ
m : (M.M i i').succ.le m_2
ih : cs.IsReduced (alternatingWord i i' m_2.succ)
⊢ cs.IsReduced (alternatingWord i i' m_2)
have ih₁ : cs.IsReduced ((if Even m_2 then i' else i) :: alternatingWord i i' m_2)
Tactic: rw [alternatingWord_succ'] at ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (hypothesis)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m_1 : ℕ
hM : M.M i i' ≠ 0
m_2 : ℕ
m : (M.M i i').succ.le m_2
ih : cs.IsReduced ((if Even m_2 then i' else i) :: alternatingWord i i' m_2)
⊢ cs.IsReduced (alternatingWord i i' m_2)
have ih₁ : cs.IsReduced (drop 1 ((if Even m_2 then i' else i) :: alternatingWord i i' m_2))
Tactic: apply IsReduced.drop (j := 1) at ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
hm : m > M.M i i'
⊢ ¬cs.IsReduced (alternatingWord i i' m)
have refl : ¬cs.IsReduced (alternatingWord i i' (M.M i i').succ)
Tactic: induction hm with
  | refl => -- Base case; m = M i i' + 1
    suffices h : ℓ (π (alternatingWord i i' (M i i' + 1))) < M i i' + 1 by
      unfold IsReduced
      rw [Nat.succ_eq_add_one, length_alternatingWord]
      lia
    have : M i i' + 1 ≤ M i i' * 2 := by linarith [Nat.one_le_iff_ne_zero.mpr hM]
    rw [cs.prod_alternatingWord_eq_prod_alternatingWord_sub i i' _ this]
    have : M i i' * 2 - (M i i' + 1) = M i i' - 1 := by lia
    rw [this]
    calc
      ℓ (π (alternatingWord i' i (M i i' - 1)))
      _ ≤ (alternatingWord i' i (M i i' - 1)).length := cs.length_wordProd_le _
      _ = M i i' - 1 := length_alternatingWord _ _ _
      _ ≤ M i i' := Nat.sub_le _ _
      _ < M i i' + 1 := Nat.lt_succ_self _
  | step m ih => -- Inductive step
    contrapose ih
    rw [alternatingWord_succ'] at ih
    apply IsReduced.drop (j := 1) at ih
    simpa using ih
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
hm : m > M.M i i'
refl : ¬cs.IsReduced (alternatingWord i i' (M.M i i').succ)
⊢ ¬cs.IsReduced (alternatingWord i i' m)
have step : ∀ {m : ℕ} (m_1 : (M.M i i').succ.le m) (ih : ¬cs.IsReduced (alternatingWord i i' m)),
  ¬cs.IsReduced (alternatingWord i i' m.succ)
Tactic: induction hm with
  | refl => -- Base case; m = M i i' + 1
    suffices h : ℓ (π (alternatingWord i i' (M i i' + 1))) < M i i' + 1 by
      unfold IsReduced
      rw [Nat.succ_eq_add_one, length_alternatingWord]
      lia
    have : M i i' + 1 ≤ M i i' * 2 := by linarith [Nat.one_le_iff_ne_zero.mpr hM]
    rw [cs.prod_alternatingWord_eq_prod_alternatingWord_sub i i' _ this]
    have : M i i' * 2 - (M i i' + 1) = M i i' - 1 := by lia
    rw [this]
    calc
      ℓ (π (alternatingWord i' i (M i i' - 1)))
      _ ≤ (alternatingWord i' i (M i i' - 1)).length := cs.length_wordProd_le _
      _ = M i i' - 1 := length_alternatingWord _ _ _
      _ ≤ M i i' := Nat.sub_le _ _
      _ < M i i' + 1 := Nat.lt_succ_self _
  | step m ih => -- Inductive step
    contrapose ih
    rw [alternatingWord_succ'] at ih
    apply IsReduced.drop (j := 1) at ih
    simpa using ih
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w⁻¹) < cs.length w⁻¹ ↔ cs.length (w * cs.simple i) < cs.length w
have nth_rw : cs.length (cs.simple i * w⁻¹)⁻¹ < cs.length w⁻¹ ↔ cs.length (w * cs.simple i) < cs.length w
Tactic: nth_rw 1 [← length_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
hw : w ≠ 1
⊢ ∃ (i : B), cs.IsLeftDescent w i
have rcases : ∀ (ω : List B) (h : cs.IsReduced ω) (hw : cs.wordProd ω ≠ 1), ∃ (i : B), cs.IsLeftDescent (cs.wordProd ω) i
Tactic: rcases cs.exists_isReduced w with ⟨ω, h, rfl⟩
Cleared hypotheses: w, hw
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (hypothesis)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
h : cs.IsReduced ω
hw : cs.wordProd ω ≠ 1
⊢ ∃ (i : B), cs.IsLeftDescent (cs.wordProd ω) i
have h₁ : ω ≠ []
Tactic: have h₁ : ω ≠ [] := by rintro rfl; simp at hw
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
h : cs.IsReduced ω
hw : cs.wordProd ω ≠ 1
h₁ : ω ≠ []
⊢ ∃ (i : B), cs.IsLeftDescent (cs.wordProd ω) i
have rcases : ∀ (i : B) (ω' : List B) (h : cs.IsReduced (i :: ω')) (hw : cs.wordProd (i :: ω') ≠ 1) (h₁ : i :: ω' ≠ []),
  ∃ (i_1 : B), cs.IsLeftDescent (cs.wordProd (i :: ω')) i_1
Tactic: rcases List.exists_cons_of_ne_nil h₁ with ⟨i, ω', rfl⟩
Cleared hypotheses: ω, h, hw, h₁
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω' : List B
h : cs.IsReduced (i :: ω')
hw : cs.wordProd (i :: ω') ≠ 1
h₁ : i :: ω' ≠ []
⊢ ∃ (i_1 : B), cs.IsLeftDescent (cs.wordProd (i :: ω')) i_1
have h₂ : cs.IsLeftDescent (cs.wordProd (i :: ω')) i
Tactic: use i
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω' : List B
h : cs.IsReduced (i :: ω')
hw : cs.wordProd (i :: ω') ≠ 1
h₁ : i :: ω' ≠ []
⊢ cs.IsLeftDescent (cs.wordProd (i :: ω')) i
have h₂ : cs.length (cs.wordProd ω') < (i :: ω').length
Tactic: rw [IsLeftDescent, h, wordProd_cons, simple_mul_simple_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω' : List B
h : cs.IsReduced (i :: ω')
hw : cs.wordProd (i :: ω') ≠ 1
h₁ : i :: ω' ≠ []
⊢ cs.length (cs.wordProd ω') < (i :: ω').length
have ℓ : ω'.length < (i :: ω').length
Tactic: calc
    ℓ (π ω') ≤ ω'.length := cs.length_wordProd_le ω'
    _ < (i :: ω').length := by simp
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
hw : w ≠ 1
⊢ ∃ (i : B), cs.IsRightDescent w i
have simp : ∃ (i : B), cs.IsLeftDescent w⁻¹ i
Tactic: simp only [← isLeftDescent_inv_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
hw : w ≠ 1
⊢ ∃ (i : B), cs.IsLeftDescent w⁻¹ i
have hw₁ : w⁻¹ ≠ 1
Tactic: apply exists_leftDescent_of_ne_one
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w) < cs.length w ↔ cs.length (cs.simple i * w) + 1 = cs.length w
have mp : cs.length (cs.simple i * w) < cs.length w → cs.length (cs.simple i * w) + 1 = cs.length w
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
mp : cs.length (cs.simple i * w) < cs.length w → cs.length (cs.simple i * w) + 1 = cs.length w
⊢ cs.length (cs.simple i * w) < cs.length w ↔ cs.length (cs.simple i * w) + 1 = cs.length w
have mpr : cs.length (cs.simple i * w) + 1 = cs.length w → cs.length (cs.simple i * w) < cs.length w
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ ¬cs.length (cs.simple i * w) < cs.length w ↔ cs.length (cs.simple i * w) = cs.length w + 1
have mp : ¬cs.length (cs.simple i * w) < cs.length w → cs.length (cs.simple i * w) = cs.length w + 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
mp : ¬cs.length (cs.simple i * w) < cs.length w → cs.length (cs.simple i * w) = cs.length w + 1
⊢ ¬cs.length (cs.simple i * w) < cs.length w ↔ cs.length (cs.simple i * w) = cs.length w + 1
have mpr : cs.length (cs.simple i * w) = cs.length w + 1 → ¬cs.length (cs.simple i * w) < cs.length w
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (w * cs.simple i) < cs.length w ↔ cs.length (w * cs.simple i) + 1 = cs.length w
have mp : cs.length (w * cs.simple i) < cs.length w → cs.length (w * cs.simple i) + 1 = cs.length w
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
mp : cs.length (w * cs.simple i) < cs.length w → cs.length (w * cs.simple i) + 1 = cs.length w
⊢ cs.length (w * cs.simple i) < cs.length w ↔ cs.length (w * cs.simple i) + 1 = cs.length w
have mpr : cs.length (w * cs.simple i) + 1 = cs.length w → cs.length (w * cs.simple i) < cs.length w
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ ¬cs.length (w * cs.simple i) < cs.length w ↔ cs.length (w * cs.simple i) = cs.length w + 1
have mp : ¬cs.length (w * cs.simple i) < cs.length w → cs.length (w * cs.simple i) = cs.length w + 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
mp : ¬cs.length (w * cs.simple i) < cs.length w → cs.length (w * cs.simple i) = cs.length w + 1
⊢ ¬cs.length (w * cs.simple i) < cs.length w ↔ cs.length (w * cs.simple i) = cs.length w + 1
have mpr : cs.length (w * cs.simple i) = cs.length w + 1 → ¬cs.length (w * cs.simple i) < cs.length w
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.IsLeftDescent w i ↔ ¬cs.IsLeftDescent (cs.simple i * w) i
have rw : cs.length (cs.simple i * w) + 1 = cs.length w ↔ cs.length w = cs.length (cs.simple i * w) + 1
Tactic: rw [isLeftDescent_iff, not_isLeftDescent_iff, simple_mul_simple_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w) + 1 = cs.length w ↔ cs.length w = cs.length (cs.simple i * w) + 1
have mp : cs.length (cs.simple i * w) + 1 = cs.length w → cs.length w = cs.length (cs.simple i * w) + 1
Tactic: tauto
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
mp : cs.length (cs.simple i * w) + 1 = cs.length w → cs.length w = cs.length (cs.simple i * w) + 1
⊢ cs.length (cs.simple i * w) + 1 = cs.length w ↔ cs.length w = cs.length (cs.simple i * w) + 1
have mpr : cs.length w = cs.length (cs.simple i * w) + 1 → cs.length (cs.simple i * w) + 1 = cs.length w
Tactic: tauto
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.IsRightDescent w i ↔ ¬cs.IsRightDescent (w * cs.simple i) i
have rw : cs.length (w * cs.simple i) + 1 = cs.length w ↔ cs.length w = cs.length (w * cs.simple i) + 1
Tactic: rw [isRightDescent_iff, not_isRightDescent_iff, simple_mul_simple_cancel_right]
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (w * cs.simple i) + 1 = cs.length w ↔ cs.length w = cs.length (w * cs.simple i) + 1
have mp : cs.length (w * cs.simple i) + 1 = cs.length w → cs.length w = cs.length (w * cs.simple i) + 1
Tactic: tauto
-- Lean 4 proof step from Mathlib.GroupTheory.Coxeter.Length (goal)
Goal:
B : Type u_1
W : Type u_2
inst : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
mp : cs.length (w * cs.simple i) + 1 = cs.length w → cs.length w = cs.length (w * cs.simple i) + 1
⊢ cs.length (w * cs.simple i) + 1 = cs.length w ↔ cs.length w = cs.length (w * cs.simple i) + 1
have mpr : cs.length w = cs.length (w * cs.simple i) + 1 → cs.length (w * cs.simple i) + 1 = cs.length w
Tactic: tauto
-- Lean 4 proof step from Mathlib.GroupTheory.DedekindFinite (goal)
Goal:
M : Type u_1
inst : Monoid M
inst_1 : Finite M
a b : M
hab : a * b = 1
⊢ b * a = 1
have have : ∀ (c : M) (hbc : Eq.{u_1 + 1} (α := M) ((fun (x : M) ↦ b * x) c) 1), b * a = 1
Tactic: have ⟨c, hbc⟩ := Finite.surjective_of_injective (isLeftRegular_of_mul_eq_one hab) 1
-- Lean 4 proof step from Mathlib.GroupTheory.Descent (goal)
Goal:
G : Type u_1
inst : Group G
f : G →* G
hf : ∀ (U : Subgroup G), map f U ≤ U
s : Set G
h : G → ℝ
a b c : ℝ
ha : 0 ≤ a
H₀ : a < b
hs : s.Finite
H₁ : s * (↑f.range : Set G) = Set.univ
H₂ : ∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g * x) + c
H₃ : ∀ (x : G), b * h x - c ≤ h ((f : (a : G) → G) x)
inst_1 : Northcott h
q : (a : G) → G ⧸ map f ⊤ := QuotientGroup.mk
S : Set G := s ∪ {x : G | h x ≤ 2 * c / (b - a)}
U : Subgroup G := closure S
⊢ FG G
have suffices : U = ⊤
Tactic: suffices U = ⊤ from Group.fg_iff.mpr ⟨S, this, hs.union <| Northcott.finite_le _⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Descent (goal)
Goal:
G : Type u_1
inst : Group G
f : G →* G
hf : ∀ (U : Subgroup G), map f U ≤ U
s : Set G
h : G → ℝ
a b c : ℝ
ha : 0 ≤ a
H₀ : a < b
hs : s.Finite
H₁ : s * (↑f.range : Set G) = Set.univ
H₂ : ∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g * x) + c
H₃ : ∀ (x : G), b * h x - c ≤ h ((f : (a : G) → G) x)
inst_1 : Northcott h
q : (a : G) → G ⧸ map f ⊤ := QuotientGroup.mk
S : Set G := s ∪ {x : G | h x ≤ 2 * c / (b - a)}
U : Subgroup G := closure S
⊢ U = ⊤
have by_contra! : ∀ (H : U ≠ ⊤), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.GroupTheory.Descent (hypothesis)
Goal:
G : Type u_1
inst : Group G
f : G →* G
hf : ∀ (U : Subgroup G), map f U ≤ U
s : Set G
h : G → ℝ
a b c : ℝ
ha : 0 ≤ a
H₀ : a < b
hs : s.Finite
H₁ : s * (↑f.range : Set G) = Set.univ
H₂ : ∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g * x) + c
H₃ : ∀ (x : G), b * h x - c ≤ h ((f : (a : G) → G) x)
inst_1 : Northcott h
q : (a : G) → G ⧸ map f ⊤ := QuotientGroup.mk
S : Set G := s ∪ {x : G | h x ≤ 2 * c / (b - a)}
U : Subgroup G := closure S
H : U ≠ ⊤
⊢ False
have H₄ : (↑U : Set G)ᶜ.Nonempty
Tactic: rw [← SetLike.coe_ne_coe, coe_top, ← Set.nonempty_compl] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.Descent (goal)
Goal:
G : Type u_1
inst : Group G
f : G →* G
hf : ∀ (U : Subgroup G), map f U ≤ U
s : Set G
h : G → ℝ
a b c : ℝ
ha : 0 ≤ a
H₀ : a < b
hs : s.Finite
H₁ : s * (↑f.range : Set G) = Set.univ
H₂ : ∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g * x) + c
H₃ : ∀ (x : G), b * h x - c ≤ h ((f : (a : G) → G) x)
inst_1 : Northcott h
q : (a : G) → G ⧸ map f ⊤ := QuotientGroup.mk
S : Set G := s ∪ {x : G | h x ≤ 2 * c / (b - a)}
U : Subgroup G := closure S
H : (↑U : Set G)ᶜ.Nonempty
⊢ False
have obtain : ∀ (x : G) (hx₁ : x ∈ (↑U : Set G)ᶜ) (hx₂ : ∀ a' ∈ (↑U : Set G)ᶜ, h x ≤ h a'), False
Tactic: obtain ⟨x, hx₁, hx₂⟩ := Northcott.exists_min_image h Uᶜ H
-- Lean 4 proof step from Mathlib.GroupTheory.Descent (goal)
Goal:
G : Type u_1
inst : Group G
f : G →* G
hf : ∀ (U : Subgroup G), map f U ≤ U
s : Set G
h : G → ℝ
a b c : ℝ
ha : 0 ≤ a
H₀ : a < b
hs : s.Finite
H₁ : s * (↑f.range : Set G) = Set.univ
H₂ : ∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g * x) + c
H₃ : ∀ (x : G), b * h x - c ≤ h ((f : (a : G) → G) x)
inst_1 : Northcott h
q : (a : G) → G ⧸ map f ⊤ := QuotientGroup.mk
S : Set G := s ∪ {x : G | h x ≤ 2 * c / (b - a)}
U : Subgroup G := closure S
H : (↑U : Set G)ᶜ.Nonempty
x : G
hx₁ : x ∈ (↑U : Set G)ᶜ
hx₂ : ∀ a' ∈ (↑U : Set G)ᶜ, h x ≤ h a'
⊢ False
have obtain : ∀ (g : G) (hg : g ∈ s) (y : G) (hx₁ : HMul.hMul (β := G) g ((f : (a : G) → G) y : G) ∈ (↑U : Set G)ᶜ)
  (hx₂ : ∀ a' ∈ (↑U : Set G)ᶜ, h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G)) ≤ h a'), False
Tactic: obtain ⟨g, hg, z, ⟨y, rfl⟩, rfl⟩ := Set.mem_mul.mp <| H₁ ▸ Set.mem_univ x
Cleared hypotheses: x, hx₁, hx₂
-- Lean 4 proof step from Mathlib.GroupTheory.Descent (goal)
Goal:
G : Type u_1
inst : Group G
f : G →* G
hf : ∀ (U : Subgroup G), map f U ≤ U
s : Set G
h : G → ℝ
a b c : ℝ
ha : 0 ≤ a
H₀ : a < b
hs : s.Finite
H₁ : s * (↑f.range : Set G) = Set.univ
H₂ : ∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g * x) + c
H₃ : ∀ (x : G), b * h x - c ≤ h ((f : (a : G) → G) x)
inst_1 : Northcott h
q : (a : G) → G ⧸ map f ⊤ := QuotientGroup.mk
S : Set G := s ∪ {x : G | h x ≤ 2 * c / (b - a)}
U : Subgroup G := closure S
H : (↑U : Set G)ᶜ.Nonempty
g : G
hg : g ∈ s
y : G
hx₁ : HMul.hMul (β := G) g ((f : (a : G) → G) y : G) ∈ (↑U : Set G)ᶜ
hx₂ : ∀ a' ∈ (↑U : Set G)ᶜ, h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G)) ≤ h a'
this :
  a * h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G)) + 2 * c <
    b * h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G))
⊢ h y < h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G))
have nlinarith : h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G)) ≤ h y →
  a * h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G)) + 2 * c -
              b * h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G)) +
            (h ((f : (a : G) → G) y) - (a * h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G)) + c)) +
          (b * h y - c - h ((f : (a : G) → G) y)) +
        (0 - (0 - a) * (h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G)) - h y)) +
      (0 - (a - b) * (h (HMul.hMul (β := G) g ((f : (a : G) → G) y : G)) - h y)) =
    0
Tactic: nlinarith [H₂ g hg (f y), H₃ y]