awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.AffineMonoid.Irreducible (hypothesis)
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
inst_2 : Monoid.FG M
S : Finset M
hSgen : Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun (S : Finset M) ↦ Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤) y → y ≤ S → S ≤ y
r : M
hrS : r ∈ (↑S : Set M)
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ (x : M) (x_1 : M) (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr_1 : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr' : r = (r ^ (m r + n r) * ∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s
hr : m r + n r = 0
⊢ False
have this : {r} ⊆ (↑(closure ((↑S : Set M) \ {r})) : Set M)
Tactic: have : ({r} : Set M) ⊆ closure (S \ {r}) := by
      simp only [hr, pow_zero, one_mul] at hr'
      rw [hr', Set.singleton_subset_iff]
      refine mul_mem ?_ ?_ <;> refine prod_mem _ fun s hs ↦ pow_mem (subset_closure ?_) _ <;>
        rw [← hr'] <;> simpa using hs
-- Lean 4 proof step from Mathlib.Algebra.AffineMonoid.Irreducible (hypothesis)
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
inst_2 : Monoid.FG M
S : Finset M
hSgen : Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun (S : Finset M) ↦ Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤) y → y ≤ S → S ≤ y
r : M
hrS : r ∈ (↑S : Set M)
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ (x : M) (x_1 : M) (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr_1 : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr' : r = (r ^ (m r + n r) * ∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s
hr : m r + n r = 0
this : {r} ⊆ (↑(closure ((↑S : Set M) \ {r})) : Set M)
⊢ False
have hSmax₁ : S ≤ S \ {r}
Tactic: specialize hSmax (y := S \ {r}) (by simp [Submonoid.closure_sdiff_eq_closure this, hSgen])
      Finset.sdiff_subset
Cleared hypotheses: hSmax
-- Lean 4 proof step from Mathlib.Algebra.AffineMonoid.Irreducible (hypothesis)
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
inst_2 : Monoid.FG M
S : Finset M
hSgen : Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun (S : Finset M) ↦ Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤) y → y ≤ S → S ≤ y
r : M
hrS : r ∈ (↑S : Set M)
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ (x : M) (x_1 : M) (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr_1 : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr' : r = (r ^ (m r + n r) * ∏ s ∈ S \ {r}, s ^ m s) * ∏ s ∈ S \ {r}, s ^ n s
hr : m r + n r = 1
⊢ False
have hr'₁ : (∀ i ∈ S \ {r}, i ^ m i = 1) ∧ ∀ i ∈ S \ {r}, i ^ n i = 1
Tactic: simp only [hr, pow_one, mul_assoc, eq_comm (a := r), mul_eq_left, LeftCancelMonoid.mul_eq_one,
      Finset.prod_eq_one_iff] at hr'
Cleared hypotheses: hr'
-- Lean 4 proof step from Mathlib.Algebra.AffineMonoid.Irreducible (goal)
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
inst_2 : Monoid.FG M
S : Finset M
hSgen : Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun (S : Finset M) ↦ Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤) y → y ≤ S → S ≤ y
r : M
hrS : r ∈ (↑S : Set M)
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ (x : M) (x_1 : M) (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr_1 : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr : m r + n r = 1
hr' : (∀ i ∈ S \ {r}, i ^ m i = 1) ∧ ∀ i ∈ S \ {r}, i ^ n i = 1
⊢ False
have inl : ∀ (h : m r = 0), False
Tactic: obtain h | h : m r = 0 ∨ n r = 0 := by lia
-- Lean 4 proof step from Mathlib.Algebra.AffineMonoid.Irreducible (goal)
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
inst_2 : Monoid.FG M
S : Finset M
hSgen : Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun (S : Finset M) ↦ Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤) y → y ≤ S → S ≤ y
r : M
hrS : r ∈ (↑S : Set M)
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ (x : M) (x_1 : M) (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr_1 : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr : m r + n r = 1
hr' : (∀ i ∈ S \ {r}, i ^ m i = 1) ∧ ∀ i ∈ S \ {r}, i ^ n i = 1
inl : ∀ (h : m r = 0), False
⊢ False
have inr : ∀ (h : n r = 0), False
Tactic: obtain h | h : m r = 0 ∨ n r = 0 := by lia
-- Lean 4 proof step from Mathlib.Algebra.AffineMonoid.Irreducible (hypothesis)
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
inst_2 : Monoid.FG M
S : Finset M
hSgen : Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun (S : Finset M) ↦ Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤) y → y ≤ S → S ≤ y
r : M
hrS : r ∈ (↑S : Set M)
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ (x : M) (x_1 : M) (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr_1 : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr : m r + n r = 1
hr' : (∀ i ∈ S \ {r}, i ^ m i = 1) ∧ ∀ i ∈ S \ {r}, i ^ n i = 1
h : m r = 0
⊢ False
have hr₁ : r = 1 * b
Tactic: obtain rfl : a = 1 := by simpa [h, Finset.prod_eq_one hr'.1] using hm
Cleared hypotheses: a, hr_1, ha, hm
-- Lean 4 proof step from Mathlib.Algebra.AffineMonoid.Irreducible (hypothesis)
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
inst_2 : Monoid.FG M
S : Finset M
hSgen : Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun (S : Finset M) ↦ Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤) y → y ≤ S → S ≤ y
r : M
hrS : r ∈ (↑S : Set M)
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ (x : M) (x_1 : M) (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr_1 : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr : m r + n r = 1
hr' : (∀ i ∈ S \ {r}, i ^ m i = 1) ∧ ∀ i ∈ S \ {r}, i ^ n i = 1
h : m r = 0
hr₁ : r = 1 * b
⊢ False
have ha₁ : ¬IsUnit.{u_1} (M := M) 1
Tactic: obtain rfl : a = 1 := by simpa [h, Finset.prod_eq_one hr'.1] using hm
Cleared hypotheses: a, hr_1, ha, hm
-- Lean 4 proof step from Mathlib.Algebra.AffineMonoid.Irreducible (hypothesis)
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
inst_2 : Monoid.FG M
S : Finset M
hSgen : Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun (S : Finset M) ↦ Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤) y → y ≤ S → S ≤ y
r : M
hrS : r ∈ (↑S : Set M)
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ (x : M) (x_1 : M) (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr_1 : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr : m r + n r = 1
hr' : (∀ i ∈ S \ {r}, i ^ m i = 1) ∧ ∀ i ∈ S \ {r}, i ^ n i = 1
h : m r = 0
hr₁ : r = 1 * b
ha₁ : ¬IsUnit.{u_1} (M := M) 1
⊢ False
have hm₁ : 1 = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
Tactic: obtain rfl : a = 1 := by simpa [h, Finset.prod_eq_one hr'.1] using hm
Cleared hypotheses: a, hr_1, ha, hm
-- Lean 4 proof step from Mathlib.Algebra.AffineMonoid.Irreducible (hypothesis)
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
inst_2 : Monoid.FG M
S : Finset M
hSgen : Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun (S : Finset M) ↦ Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤) y → y ≤ S → S ≤ y
r : M
hrS : r ∈ (↑S : Set M)
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ (x : M) (x_1 : M) (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr_1 : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr : m r + n r = 1
hr' : (∀ i ∈ S \ {r}, i ^ m i = 1) ∧ ∀ i ∈ S \ {r}, i ^ n i = 1
h : n r = 0
⊢ False
have hr₁ : r = a * 1
Tactic: obtain rfl : b = 1 := by simpa [h, Finset.prod_eq_one hr'.2] using hn
Cleared hypotheses: b, hr_1, hb, hn
-- Lean 4 proof step from Mathlib.Algebra.AffineMonoid.Irreducible (hypothesis)
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
inst_2 : Monoid.FG M
S : Finset M
hSgen : Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun (S : Finset M) ↦ Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤) y → y ≤ S → S ≤ y
r : M
hrS : r ∈ (↑S : Set M)
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ (x : M) (x_1 : M) (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr_1 : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr : m r + n r = 1
hr' : (∀ i ∈ S \ {r}, i ^ m i = 1) ∧ ∀ i ∈ S \ {r}, i ^ n i = 1
h : n r = 0
hr₁ : r = a * 1
⊢ False
have hb₁ : ¬IsUnit.{u_1} (M := M) 1
Tactic: obtain rfl : b = 1 := by simpa [h, Finset.prod_eq_one hr'.2] using hn
Cleared hypotheses: b, hr_1, hb, hn
-- Lean 4 proof step from Mathlib.Algebra.AffineMonoid.Irreducible (hypothesis)
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : Subsingleton.{u_1 + 1} Mˣ
inst_2 : Monoid.FG M
S : Finset M
hSgen : Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤
hSmax : ∀ ⦃y : Finset M⦄, (fun (S : Finset M) ↦ Eq (α := Submonoid M) (closure (↑S : Set M)) ⊤) y → y ≤ S → S ≤ y
r : M
hrS : r ∈ (↑S : Set M)
hr₀ : r ≠ 1
hrirred : ¬IsUnit r → ∃ (x : M) (x_1 : M) (_ : r = x * x_1), ¬IsUnit x ∧ ¬IsUnit x_1
a b : M
hr_1 : r = a * b
ha : ¬IsUnit a
hb : ¬IsUnit b
m n : M → ℕ
hm : a = r ^ m r * ∏ s ∈ S \ {r}, s ^ m s
hn : b = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
hr : m r + n r = 1
hr' : (∀ i ∈ S \ {r}, i ^ m i = 1) ∧ ∀ i ∈ S \ {r}, i ^ n i = 1
h : n r = 0
hr₁ : r = a * 1
hb₁ : ¬IsUnit.{u_1} (M := M) 1
⊢ False
have hn₁ : 1 = r ^ n r * ∏ s ∈ S \ {r}, s ^ n s
Tactic: obtain rfl : b = 1 := by simpa [h, Finset.prod_eq_one hr'.2] using hn
Cleared hypotheses: b, hr_1, hb, hn
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
r : R
⊢ x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) * x
have rw : x * x - HMul.hMul (β := A) x ((algebraMap R A : (a : R) → A) r : A) =
  HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) * x
Tactic: rw [mul_sub, ← commutes, sub_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
r : R
rw :
  x * x - HMul.hMul (β := A) x ((algebraMap R A : (a : R) → A) r : A) =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) * x
⊢ x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) * x
have rw₁ : x * x - HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) x =
  HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) * x
Tactic: rw [mul_sub, ← commutes, sub_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
r : R
rw :
  x * x - HMul.hMul (β := A) x ((algebraMap R A : (a : R) → A) r : A) =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) * x
rw₁ :
  x * x - HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) x =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) * x
⊢ x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) * x
have rw₂ : x * x - HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) x =
  x * x - HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) x
Tactic: rw [mul_sub, ← commutes, sub_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
r : R
n : ℕ
ih :
  x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n * x
⊢ x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ (n + 1) =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ (n + 1) * x
have succ : x *
    (HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
      HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n) =
  HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
      HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
    x
Tactic: rw [pow_succ', ← mul_assoc, mul_sub_algebraMap_commutes, mul_assoc, ih, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
r : R
n : ℕ
ih :
  x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n * x
succ :
  x *
      (HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n) =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
      x
⊢ x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ (n + 1) =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ (n + 1) * x
have succ₁ : x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n =
  HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
      HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
    x
Tactic: rw [pow_succ', ← mul_assoc, mul_sub_algebraMap_commutes, mul_assoc, ih, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
r : R
n : ℕ
ih :
  x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n * x
succ :
  x *
      (HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n) =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
      x
succ₁ :
  x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
      HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
      x
⊢ x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ (n + 1) =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ (n + 1) * x
have succ₂ : HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) * x *
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n =
  HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
      HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
    x
Tactic: rw [pow_succ', ← mul_assoc, mul_sub_algebraMap_commutes, mul_assoc, ih, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
r : R
n : ℕ
ih :
  x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n * x
succ :
  x *
      (HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n) =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
      x
succ₁ :
  x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
      HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
      x
succ₂ :
  HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) * x *
      HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
      x
⊢ x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ (n + 1) =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ (n + 1) * x
have succ₃ : HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
    (x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n) =
  HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
      HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
    x
Tactic: rw [pow_succ', ← mul_assoc, mul_sub_algebraMap_commutes, mul_assoc, ih, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
r : R
n : ℕ
ih :
  x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n * x
succ :
  x *
      (HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n) =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
      x
succ₁ :
  x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
      HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
      x
succ₂ :
  HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) * x *
      HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
      x
succ₃ :
  HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
      (x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n) =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
      x
⊢ x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ (n + 1) =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ (n + 1) * x
have succ₄ : HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
    (HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n * x) =
  HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
      HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
    x
Tactic: rw [pow_succ', ← mul_assoc, mul_sub_algebraMap_commutes, mul_assoc, ih, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
r : R
n : ℕ
ih :
  x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n * x
succ :
  x *
      (HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n) =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
      x
succ₁ :
  x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
      HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
      x
succ₂ :
  HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) * x *
      HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
      x
succ₃ :
  HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
      (x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n) =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
      x
succ₄ :
  HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
      (HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n * x) =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
        HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
      x
⊢ x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ (n + 1) =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ (n + 1) * x
have succ₅ : HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
      HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
    x =
  HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) *
      HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n *
    x
Tactic: rw [pow_succ', ← mul_assoc, mul_sub_algebraMap_commutes, mul_assoc, ih, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
r : R
n : ℕ
⊢ x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n * x
have zero : x * HPow.hPow (β := ℕ) (HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A)) 0 =
  HPow.hPow (β := ℕ) (HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A)) 0 * x
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rw [pow_succ', ← mul_assoc, mul_sub_algebraMap_commutes, mul_assoc, ih, ← mul_assoc]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Ring A
inst_2 : Algebra R A
x : A
r : R
n : ℕ
zero :
  x * HPow.hPow (β := ℕ) (HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A)) 0 =
    HPow.hPow (β := ℕ) (HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A)) 0 * x
⊢ x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n * x
have succ : ∀ (n : ℕ)
  (ih :
    x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n =
      HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ n * x),
  x * HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ (n + 1) =
    HSub.hSub (β := A) x ((algebraMap R A : (a : R) → A) r : A) ^ (n + 1) * x
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rw [pow_succ', ← mul_assoc, mul_sub_algebraMap_commutes, mul_assoc, ih, ← mul_assoc]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Basic (goal)
Goal:
R : Type u
S : Type v
M : Type w
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMulCommClass S R M
inst_6 : SMul R S
inst_7 : IsScalarTower R S M
x : R
h : IsUnit.{w} (M := End S M) ((algebraMap R (End S M) : (a : R) → End S M) x : End S M)
m m' : M
H : m = x • m'
⊢ ((↑h.unit⁻¹ : End S M) : (a : M) → M) m = m'
have apply_fun : Eq (α := M) (((↑h.unit : End S M) : (a : M) → M) (((↑h.unit⁻¹ : End S M) : (a : M) → M) m : M) : M)
  (((↑h.unit : End S M) : (a : M) → M) m' : M)
Tactic: apply_fun ⇑h.unit.val using ((isUnit_iff _).mp h).injective