awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b : A
rw : r • a * b = b * r • a
rw₁ : r • a * b = r • (b * a)
⊢ Commute (r • a) b
have rw₂ : r • (a * b) = r • (b * a)
Tactic: rw [commute_iff_eq, mul_smul_comm, smul_mul_assoc, ha.comm]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b : A
rw : r • a * b = b * r • a
rw₁ : r • a * b = r • (b * a)
rw₂ : r • (a * b) = r • (b * a)
⊢ Commute (r • a) b
have rw₃ : r • (b * a) = r • (b * a)
Tactic: rw [commute_iff_eq, mul_smul_comm, smul_mul_assoc, ha.comm]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b c : A
⊢ r • a * (b * c) = r • a * b * c
have rw : r • (a * (b * c)) = r • a * b * c
Tactic: rw [smul_mul_assoc, smul_mul_assoc, smul_mul_assoc, ha.left_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b c : A
rw : r • (a * (b * c)) = r • a * b * c
⊢ r • a * (b * c) = r • a * b * c
have rw₁ : r • (a * (b * c)) = r • (a * b) * c
Tactic: rw [smul_mul_assoc, smul_mul_assoc, smul_mul_assoc, ha.left_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b c : A
rw : r • (a * (b * c)) = r • a * b * c
rw₁ : r • (a * (b * c)) = r • (a * b) * c
⊢ r • a * (b * c) = r • a * b * c
have rw₂ : r • (a * (b * c)) = r • (a * b * c)
Tactic: rw [smul_mul_assoc, smul_mul_assoc, smul_mul_assoc, ha.left_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b c : A
rw : r • (a * (b * c)) = r • a * b * c
rw₁ : r • (a * (b * c)) = r • (a * b) * c
rw₂ : r • (a * (b * c)) = r • (a * b * c)
⊢ r • a * (b * c) = r • a * b * c
have rw₃ : r • (a * b * c) = r • (a * b * c)
Tactic: rw [smul_mul_assoc, smul_mul_assoc, smul_mul_assoc, ha.left_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b c : A
⊢ b * c * r • a = b * (c * r • a)
have rw : r • (b * c * a) = b * (c * r • a)
Tactic: rw [mul_smul_comm, mul_smul_comm, mul_smul_comm, ha.right_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b c : A
rw : r • (b * c * a) = b * (c * r • a)
⊢ b * c * r • a = b * (c * r • a)
have rw₁ : r • (b * c * a) = b * r • (c * a)
Tactic: rw [mul_smul_comm, mul_smul_comm, mul_smul_comm, ha.right_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b c : A
rw : r • (b * c * a) = b * (c * r • a)
rw₁ : r • (b * c * a) = b * r • (c * a)
⊢ b * c * r • a = b * (c * r • a)
have rw₂ : r • (b * c * a) = r • (b * (c * a))
Tactic: rw [mul_smul_comm, mul_smul_comm, mul_smul_comm, ha.right_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
r : R
a : A
ha : a ∈ Set.center A
b c : A
rw : r • (b * c * a) = b * (c * r • a)
rw₁ : r • (b * c * a) = b * r • (c * a)
rw₂ : r • (b * c * a) = r • (b * (c * a))
⊢ b * c * r • a = b * (c * r • a)
have rw₃ : r • (b * (c * a)) = r • (b * (c * a))
Tactic: rw [mul_smul_comm, mul_smul_comm, mul_smul_comm, ha.right_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
r : R
a : A
ha : a ∈ s.centralizer
x : A
hx : x ∈ s
⊢ x * r • a = r • a * x
have rw : r • (x * a) = r • a * x
Tactic: rw [mul_smul_comm, smul_mul_assoc, ha x hx]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
r : R
a : A
ha : a ∈ s.centralizer
x : A
hx : x ∈ s
rw : r • (x * a) = r • a * x
⊢ x * r • a = r • a * x
have rw₁ : r • (x * a) = r • (a * x)
Tactic: rw [mul_smul_comm, smul_mul_assoc, ha x hx]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
s : Set A
r : R
a : A
ha : a ∈ s.centralizer
x : A
hx : x ∈ s
rw : r • (x * a) = r • a * x
rw₁ : r • (x * a) = r • (a * x)
⊢ x * r • a = r • a * x
have rw₂ : r • (a * x) = r • (a * x)
Tactic: rw [mul_smul_comm, smul_mul_assoc, ha x hx]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.NonUnitalSubalgebra (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : SMulCommClass R A A
a b : A
s : Set A
hb : Membership.mem (γ := NonUnitalSubalgebra R A) (adjoin R s) b
h : ∀ b ∈ s, Commute a b
⊢ Commute a b
have this : Membership.mem (γ := NonUnitalSubalgebra R A) (centralizer R s) a
Tactic: have : a ∈ centralizer R s := by simpa only [Commute.symm_iff (a := a)] using h
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
A : Type v
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A
r : R
⊢ (fun (r : R) ↦ HSMul.hSMul (β := A) r 1) r = x ↔ (algebraMap R A : (a : R) → A) r = x
have rw : (fun (r : R) ↦ HSMul.hSMul (β := A) r 1) r = x ↔ HSMul.hSMul (β := A) r 1 = x
Tactic: rw [algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
n : ℕ
⊢ HSMul.hSMul.{u, v, v} (α := R) (β := A) (↑n : R) 1 = (↑n : A)
have rw : HSMul.hSMul (β := A) n 1 = (↑n : A)
Tactic: rw [Nat.cast_smul_eq_nsmul, nsmul_one]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
n : ℕ
rw : HSMul.hSMul (β := A) n 1 = (↑n : A)
⊢ HSMul.hSMul.{u, v, v} (α := R) (β := A) (↑n : R) 1 = (↑n : A)
have rw₁ : Eq.{v + 1} (α := A) (↑n : A) (↑n : A)
Tactic: rw [Nat.cast_smul_eq_nsmul, nsmul_one]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
x : A
⊢ Membership.mem (γ := SubMulAction R A) (toSubMulAction 1) x ↔ Membership.mem (γ := SubMulAction R A) 1 x
have rw : Membership.mem (γ := SubMulAction R A) (toSubMulAction (R ∙ 1)) x ↔ ∃ (r : R), HSMul.hSMul (β := A) r 1 = x
Tactic: rw [one_eq_span, SubMulAction.mem_one]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
A' : Submodule R A
M' : Submodule R M
r : R
m_1 : M
hm_1 : m_1 ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
a : A
ha : a ∈ A'.toAddSubmonoid
m : M
hm : m ∈ M'.toAddSubmonoid
⊢ r • a • m ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
have rw : (r • a) • m ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
Tactic: rw [← smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
A' : Submodule R A
M' : Submodule R M
r : R
m : M
hm : m ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
m₁ m₂ : M
h₁ : r • m₁ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
h₂ : r • m₂ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
⊢ r • (m₁ + m₂) ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
have rw : r • m₁ + r • m₂ ∈ (A'.toAddSubmonoid • M'.toAddSubmonoid).carrier
Tactic: rw [smul_add]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
I : Submodule R A
N : Submodule R M
x : M
hx : x ∈ I • N
p : (x : M) → x ∈ I • N → Prop
smul : ∀ (r : A) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) ⋯
add : ∀ (x : M) (hx : x ∈ I • N) (y : M) (hy : y ∈ I • N), p x hx → p y hy → p (x + y) ⋯
⊢ p x hx
have refine : ∃ (x_1 : x ∈ I • N), p x x_1
Tactic: refine Exists.elim ?_ fun (h : x ∈ I • N) (H : p x h) ↦ H
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Submodule R M
n : M
h : n ∈ N
⊢ Membership.mem (γ := Submodule R M) ⊥ (HSMul.hSMul.{v, u_1, u_1} (α := A) 0 n)
have rw : Membership.mem (γ := Submodule R M) ⊥ 0
Tactic: rw [zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
I J : Submodule R A
N : Submodule R M
mn : A
hmn : mn ∈ I ⊔ J
p : M
hp : p ∈ N
⊢ mn • p ∈ I • N ⊔ J • N
have obtain : ∀ (m : A) (hm : m ∈ I) (n : A) (hn : n ∈ J) (hmn : m + n ∈ I ⊔ J), (m + n) • p ∈ I • N ⊔ J • N
Tactic: obtain ⟨m, hm, n, hn, rfl⟩ := mem_sup.mp hmn
Cleared hypotheses: mn, hmn
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
I J : Submodule R A
N : Submodule R M
p : M
hp : p ∈ N
m : A
hm : m ∈ I
n : A
hn : n ∈ J
hmn : m + n ∈ I ⊔ J
⊢ (m + n) • p ∈ I • N ⊔ J • N
have rw : m • p + n • p ∈ I • N ⊔ J • N
Tactic: rw [add_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
ι : Sort u_2
t_1 : ι → Submodule R A
N : Submodule R M
t : A
ht : Membership.mem (γ := Submodule R A) (⨆ (i : ι), t_1 i) t
s : M
hs : s ∈ N
⊢ (fun (x : A) ↦ Membership.mem (γ := Submodule R M) (⨆ (i : ι), t_1 i • N) (x • s)) 0
have simp_rw : Membership.mem (γ := Submodule R M) (⨆ (i : ι), t_1 i • N) 0
Tactic: simp_rw [zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
ι : Sort u_2
t_1 : ι → Submodule R A
N : Submodule R M
t : A
ht : Membership.mem (γ := Submodule R A) (⨆ (i : ι), t_1 i) t
s : M
hs : s ∈ N
x y : A
⊢ (fun (x : A) ↦ Membership.mem (γ := Submodule R M) (⨆ (i : ι), t_1 i • N) (x • s)) x →
    (fun (x : A) ↦ Membership.mem (γ := Submodule R M) (⨆ (i : ι), t_1 i • N) (x • s)) y →
      (fun (x : A) ↦ Membership.mem (γ := Submodule R M) (⨆ (i : ι), t_1 i • N) (x • s)) (x + y)
have simp_rw : Membership.mem (γ := Submodule R M) (⨆ (i : ι), t_1 i • N) (x • s) →
  Membership.mem (γ := Submodule R M) (⨆ (i : ι), t_1 i • N) (y • s) →
    Membership.mem (γ := Submodule R M) (⨆ (i : ι), t_1 i • N) (x • s + y • s)
Tactic: simp_rw [add_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Submodule R M
⊢ HSMul.hSMul.{v, u_1, u_1} (α := Submodule R A) 1 N = N
have refine_1 : ∀ (r : A) (hr : Membership.mem (γ := Submodule R A) 1 r) (m : M) (hm : m ∈ N), r • m ∈ N
Tactic: refine le_antisymm (smul_le.mpr fun r hr m hm ↦ ?_) fun m hm ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Submodule R M
refine_1 : ∀ (r : A) (hr : Membership.mem (γ := Submodule R A) 1 r) (m : M) (hm : m ∈ N), r • m ∈ N
⊢ HSMul.hSMul.{v, u_1, u_1} (α := Submodule R A) 1 N = N
have refine_2 : ∀ (m : M) (hm : m ∈ N), m ∈ HSMul.hSMul.{v, u_1, u_1} (α := Submodule R A) 1 N
Tactic: refine le_antisymm (smul_le.mpr fun r hr m hm ↦ ?_) fun m hm ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Submodule R M
r : A
hr : Membership.mem (γ := Submodule R A) 1 r
m : M
hm : m ∈ N
⊢ r • m ∈ N
have refine_1 : ∀ (r : R), HSMul.hSMul.{v, u_1, u_1} (α := A) ((LinearMap.toSpanSingleton R A 1 : (a : R) → A) r : A) m ∈ N
Tactic: obtain ⟨r, rfl⟩ := hr
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Submodule R M
m : M
hm : m ∈ N
r : R
⊢ HSMul.hSMul.{v, u_1, u_1} (α := A) ((LinearMap.toSpanSingleton R A 1 : (a : R) → A) r : A) m ∈ N
have refine_1 : r • m ∈ N
Tactic: rw [LinearMap.toSpanSingleton_apply, smul_one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
M : Type u_1
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
N : Submodule R M
m : M
hm : m ∈ N
⊢ m ∈ HSMul.hSMul.{v, u_1, u_1} (α := Submodule R A) 1 N
have refine_2 : HSMul.hSMul.{v, u_1, u_1} (α := A) 1 m ∈ HSMul.hSMul.{v, u_1, u_1} (α := Submodule R A) 1 N
Tactic: rw [← one_smul A m]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : NoZeroDivisors A
M N : Submodule R A
h : M = ⊥ ∨ N = ⊥
⊢ M * N = ⊥
have inl : ⊥ * N = ⊥
Tactic: obtain rfl | rfl := h
Cleared hypotheses: M, h
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
inst_4 : NoZeroDivisors A
M N : Submodule R A
h : M = ⊥ ∨ N = ⊥
inl : ⊥ * N = ⊥
⊢ M * N = ⊥
have inr : M * ⊥ = ⊥
Tactic: obtain rfl | rfl := h
Cleared hypotheses: N, h
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
N P : Submodule R A
h : N * P = 1
| ⊤
have rw : N * (P * ⊤)
Tactic: rw [← Submodule.one_mul ⊤, ← h, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
⊢ HPow.hPow (β := ℕ) M 1 = M
have rw : HPow.hPow (β := ℕ) M 0 * M = M
Tactic: rw [Submodule.pow_succ, Submodule.pow_zero, Submodule.one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
rw : HPow.hPow (β := ℕ) M 0 * M = M
⊢ HPow.hPow (β := ℕ) M 1 = M
have rw₁ : 1 * M = M
Tactic: rw [Submodule.pow_succ, Submodule.pow_zero, Submodule.one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
rw : HPow.hPow (β := ℕ) M 0 * M = M
rw₁ : 1 * M = M
⊢ HPow.hPow (β := ℕ) M 1 = M
have rw₂ : M = M
Tactic: rw [Submodule.pow_succ, Submodule.pow_zero, Submodule.one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
n : ℕ
h : n ≠ 0
⊢ M ^ (n + 1) = M * M ^ n
have rw : M ^ (1 + n) = M * M ^ n
Tactic: rw [add_comm, M.pow_add h, Submodule.pow_one]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
n : ℕ
h : n ≠ 0
rw : M ^ (1 + n) = M * M ^ n
⊢ M ^ (n + 1) = M * M ^ n
have rw₁ : HPow.hPow (β := ℕ) M 1 * M ^ n = M * M ^ n
Tactic: rw [add_comm, M.pow_add h, Submodule.pow_one]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
n : ℕ
h : n ≠ 0
rw : M ^ (1 + n) = M * M ^ n
rw₁ : HPow.hPow (β := ℕ) M 1 * M ^ n = M * M ^ n
⊢ M ^ (n + 1) = M * M ^ n
have rw₂ : M * M ^ n = M * M ^ n
Tactic: rw [add_comm, M.pow_add h, Submodule.pow_one]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
n : ℕ
h : n + 2 ≠ 0
⊢ HPow.hPow (α := Submodule R A) ⊥ (n + 2) = ⊥
have rw : HPow.hPow (α := Submodule R A) ⊥ (n + 1) * ⊥ = ⊥
Tactic: rw [Submodule.pow_succ, bot_pow n.succ_ne_zero, bot_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
n : ℕ
h : n + 2 ≠ 0
rw : HPow.hPow (α := Submodule R A) ⊥ (n + 1) * ⊥ = ⊥
⊢ HPow.hPow (α := Submodule R A) ⊥ (n + 2) = ⊥
have rw₁ : HMul.hMul (α := Submodule R A) ⊥ ⊥ = ⊥
Tactic: rw [Submodule.pow_succ, bot_pow n.succ_ne_zero, bot_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
n : ℕ
h : n + 2 ≠ 0
rw : HPow.hPow (α := Submodule R A) ⊥ (n + 1) * ⊥ = ⊥
rw₁ : HMul.hMul (α := Submodule R A) ⊥ ⊥ = ⊥
⊢ HPow.hPow (α := Submodule R A) ⊥ (n + 2) = ⊥
have rw₂ : Eq.{v + 1} (α := Submodule R A) ⊥ ⊥
Tactic: rw [Submodule.pow_succ, bot_pow n.succ_ne_zero, bot_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
n : ℕ
ih : ∀ (h : n ≠ 0), (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n
h : n + 1 ≠ 0
⊢ (M ^ (n + 1)).toAddSubmonoid = M.toAddSubmonoid ^ (n + 1)
have succ : (M ^ n).toAddSubmonoid * M.toAddSubmonoid = M.toAddSubmonoid ^ n * M.toAddSubmonoid
Tactic: rw [Submodule.pow_succ, pow_succ, mul_toAddSubmonoid]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
ih : ∀ (h : Ne (α := ℕ) 0 0), (HPow.hPow (β := ℕ) M 0).toAddSubmonoid = HPow.hPow (β := ℕ) M.toAddSubmonoid 0
h : HAdd.hAdd (α := ℕ) 0 1 ≠ 0
⊢ (HPow.hPow (β := ℕ) M 0).toAddSubmonoid * M.toAddSubmonoid = HPow.hPow (β := ℕ) M.toAddSubmonoid 0 * M.toAddSubmonoid
have succ : toAddSubmonoid.{u, v} (R := R) 1 * M.toAddSubmonoid = HPow.hPow (β := ℕ) M.toAddSubmonoid 0 * M.toAddSubmonoid
Tactic: rw [Submodule.pow_zero, pow_zero, one_mul, ← mul_toAddSubmonoid, Submodule.one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
ih : ∀ (h : Ne (α := ℕ) 0 0), (HPow.hPow (β := ℕ) M 0).toAddSubmonoid = HPow.hPow (β := ℕ) M.toAddSubmonoid 0
h : HAdd.hAdd (α := ℕ) 0 1 ≠ 0
succ : toAddSubmonoid.{u, v} (R := R) 1 * M.toAddSubmonoid = HPow.hPow (β := ℕ) M.toAddSubmonoid 0 * M.toAddSubmonoid
⊢ (HPow.hPow (β := ℕ) M 0).toAddSubmonoid * M.toAddSubmonoid = HPow.hPow (β := ℕ) M.toAddSubmonoid 0 * M.toAddSubmonoid
have succ₁ : toAddSubmonoid.{u, v} (R := R) 1 * M.toAddSubmonoid = 1 * M.toAddSubmonoid
Tactic: rw [Submodule.pow_zero, pow_zero, one_mul, ← mul_toAddSubmonoid, Submodule.one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
ih : ∀ (h : Ne (α := ℕ) 0 0), (HPow.hPow (β := ℕ) M 0).toAddSubmonoid = HPow.hPow (β := ℕ) M.toAddSubmonoid 0
h : HAdd.hAdd (α := ℕ) 0 1 ≠ 0
succ : toAddSubmonoid.{u, v} (R := R) 1 * M.toAddSubmonoid = HPow.hPow (β := ℕ) M.toAddSubmonoid 0 * M.toAddSubmonoid
succ₁ : toAddSubmonoid.{u, v} (R := R) 1 * M.toAddSubmonoid = 1 * M.toAddSubmonoid
⊢ (HPow.hPow (β := ℕ) M 0).toAddSubmonoid * M.toAddSubmonoid = HPow.hPow (β := ℕ) M.toAddSubmonoid 0 * M.toAddSubmonoid
have succ₂ : toAddSubmonoid.{u, v} (R := R) 1 * M.toAddSubmonoid = M.toAddSubmonoid
Tactic: rw [Submodule.pow_zero, pow_zero, one_mul, ← mul_toAddSubmonoid, Submodule.one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Algebra.Operations (goal)
Goal:
R : Type u
inst : Semiring R
A : Type v
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
M : Submodule R A
ih : ∀ (h : Ne (α := ℕ) 0 0), (HPow.hPow (β := ℕ) M 0).toAddSubmonoid = HPow.hPow (β := ℕ) M.toAddSubmonoid 0
h : HAdd.hAdd (α := ℕ) 0 1 ≠ 0
succ : toAddSubmonoid.{u, v} (R := R) 1 * M.toAddSubmonoid = HPow.hPow (β := ℕ) M.toAddSubmonoid 0 * M.toAddSubmonoid
succ₁ : toAddSubmonoid.{u, v} (R := R) 1 * M.toAddSubmonoid = 1 * M.toAddSubmonoid
succ₂ : toAddSubmonoid.{u, v} (R := R) 1 * M.toAddSubmonoid = M.toAddSubmonoid
⊢ (HPow.hPow (β := ℕ) M 0).toAddSubmonoid * M.toAddSubmonoid = HPow.hPow (β := ℕ) M.toAddSubmonoid 0 * M.toAddSubmonoid
have succ₃ : (1 * M).toAddSubmonoid = M.toAddSubmonoid
Tactic: rw [Submodule.pow_zero, pow_zero, one_mul, ← mul_toAddSubmonoid, Submodule.one_mul]