awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommGroup N₂
inst_7 : AddCommGroup N₃
inst_8 : Module R₁ M
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
inst_11 : Module R₂ N₂
inst_12 : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_13 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_14 : Subsingleton M
f : M →ₛₗ[σ₁₂] M₂
x : M
rw : Eq.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) 0 : M₂) ((default : (a : M) → M₂) 0 : M₂)
rw₁ : Eq.{u_10 + 1} (α := M₂) (0 : M₂) ((default : (a : M) → M₂) 0 : M₂)
⊢ Eq.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((default : (a : M) → M₂) x : M₂)
have rw₂ : Eq.{u_10 + 1} (α := M₂) 0 0
Tactic: rw [Subsingleton.elim x 0, map_zero, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
M : Type u_8
M₂ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R₁ M
inst_5 : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
inst_6 : Nontrivial M₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective.{u_8 + 1, u_10 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
⊢ f ≠ 0
have have : ∀ (y : M₂) (ne : y ≠ 0), f ≠ 0
Tactic: have ⟨y, ne⟩ := exists_ne (0 : M₂)
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
M : Type u_8
M₂ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R₁ M
inst_5 : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
inst_6 : Nontrivial M₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective.{u_8 + 1, u_10 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
y : M₂
ne : y ≠ 0
⊢ f ≠ 0
have obtain : ∀ (x : M) (ne : Ne.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) (0 : M₂)), f ≠ 0
Tactic: obtain ⟨x, rfl⟩ := hf y
Cleared hypotheses: y, ne
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommGroup N₂
inst_7 : AddCommGroup N₃
inst_8 : Module R₁ M
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
inst_11 : Module R₂ N₂
inst_12 : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_13 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
⊢ Eq (α := M →+ M₂)
    (toAddMonoidHom.{u_2, u_3, u_8, u_10} (R := R₁) (S := R₂) (modM₁ := inst_8) (modM₂ := inst_9) (σ := σ₁₂) 0) 0
have h : ∀ (x : M),
  Eq.{u_10 + 1} (α := M₂)
    ((toAddMonoidHom.{u_2, u_3, u_8, u_10} (R := R₁) (S := R₂) (modM₁ := inst_8) (modM₂ := inst_9) (σ := σ₁₂) 0 :
          (a : M) → M₂)
        x :
      M₂)
    ((0 : (a : M) → M₂) x : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommGroup N₂
inst_7 : AddCommGroup N₃
inst_8 : Module R₁ M
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
inst_11 : Module R₂ N₂
inst_12 : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_13 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
x y : M →ₛₗ[σ₁₂] M₂
⊢ (x + y).toAddMonoidHom = x.toAddMonoidHom + y.toAddMonoidHom
have h : ∀ (x_1 : M),
  Eq.{u_10 + 1} (α := M₂) (((x + y).toAddMonoidHom : (a : M) → M₂) x_1 : M₂)
    ((x.toAddMonoidHom + y.toAddMonoidHom : (a : M) → M₂) x_1 : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommGroup N₁
inst_3 : Module R M
inst_4 : Module R N₁
inst_5 : Nontrivial M
⊢ Nontrivial.{u_4} (End R M)
have obtain : ∀ (m : M) (ne : m ≠ 0), Nontrivial.{u_4} (End R M)
Tactic: obtain ⟨m, ne⟩ := exists_ne (0 : M)
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
m : M
k l : ℕ
hk : k ≤ l
hm : Eq (α := M) ((f ^ k : (a : M) → M) m : M) (0 : M)
⊢ Eq (α := M) ((f ^ l : (a : M) → M) m : M) (0 : M)
have rw : Eq (α := M) ((f ^ (l - k + k) : (a : M) → M) m : M) (0 : M)
Tactic: rw [← Nat.sub_add_cancel hk, pow_add, mul_apply, hm, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
m : M
k l : ℕ
hk : k ≤ l
hm : Eq (α := M) ((f ^ k : (a : M) → M) m : M) (0 : M)
rw : Eq (α := M) ((f ^ (l - k + k) : (a : M) → M) m : M) (0 : M)
⊢ Eq (α := M) ((f ^ l : (a : M) → M) m : M) (0 : M)
have rw₁ : Eq (α := M) ((f ^ (l - k) * f ^ k : (a : M) → M) m : M) (0 : M)
Tactic: rw [← Nat.sub_add_cancel hk, pow_add, mul_apply, hm, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
m : M
k l : ℕ
hk : k ≤ l
hm : Eq (α := M) ((f ^ k : (a : M) → M) m : M) (0 : M)
rw : Eq (α := M) ((f ^ (l - k + k) : (a : M) → M) m : M) (0 : M)
rw₁ : Eq (α := M) ((f ^ (l - k) * f ^ k : (a : M) → M) m : M) (0 : M)
⊢ Eq (α := M) ((f ^ l : (a : M) → M) m : M) (0 : M)
have rw₂ : Eq (α := M) ((f ^ (l - k) : (a : M) → M) ((f ^ k : (a : M) → M) m : M) : M) (0 : M)
Tactic: rw [← Nat.sub_add_cancel hk, pow_add, mul_apply, hm, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
m : M
k l : ℕ
hk : k ≤ l
hm : Eq (α := M) ((f ^ k : (a : M) → M) m : M) (0 : M)
rw : Eq (α := M) ((f ^ (l - k + k) : (a : M) → M) m : M) (0 : M)
rw₁ : Eq (α := M) ((f ^ (l - k) * f ^ k : (a : M) → M) m : M) (0 : M)
rw₂ : Eq (α := M) ((f ^ (l - k) : (a : M) → M) ((f ^ k : (a : M) → M) m : M) : M) (0 : M)
⊢ Eq (α := M) ((f ^ l : (a : M) → M) m : M) (0 : M)
have rw₃ : Eq (α := M) ((f ^ (l - k) : (a : M) → M) 0 : M) (0 : M)
Tactic: rw [← Nat.sub_add_cancel hk, pow_add, mul_apply, hm, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
m : M
k l : ℕ
hk : k ≤ l
hm : Eq (α := M) ((f ^ k : (a : M) → M) m : M) (0 : M)
rw : Eq (α := M) ((f ^ (l - k + k) : (a : M) → M) m : M) (0 : M)
rw₁ : Eq (α := M) ((f ^ (l - k) * f ^ k : (a : M) → M) m : M) (0 : M)
rw₂ : Eq (α := M) ((f ^ (l - k) : (a : M) → M) ((f ^ k : (a : M) → M) m : M) : M) (0 : M)
rw₃ : Eq (α := M) ((f ^ (l - k) : (a : M) → M) 0 : M) (0 : M)
⊢ Eq (α := M) ((f ^ l : (a : M) → M) m : M) (0 : M)
have rw₄ : Eq.{u_4 + 1} (α := M) 0 0
Tactic: rw [← Nat.sub_add_cancel hk, pow_add, mul_apply, hm, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
k : ℕ
ih : (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)
⊢ (g₂ ^ (k + 1)) ∘ₛₗ f = f ∘ₛₗ (g ^ (k + 1))
have succ : (g₂ * g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ (k + 1))
Tactic: rw [pow_succ', pow_succ', mul_eq_comp, LinearMap.comp_assoc, ih,
    ← LinearMap.comp_assoc, h, LinearMap.comp_assoc, mul_eq_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
k : ℕ
ih : (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)
succ : (g₂ * g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ (k + 1))
⊢ (g₂ ^ (k + 1)) ∘ₛₗ f = f ∘ₛₗ (g ^ (k + 1))
have succ₁ : (g₂ * g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g * g ^ k)
Tactic: rw [pow_succ', pow_succ', mul_eq_comp, LinearMap.comp_assoc, ih,
    ← LinearMap.comp_assoc, h, LinearMap.comp_assoc, mul_eq_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
k : ℕ
ih : (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)
succ : (g₂ * g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ (k + 1))
succ₁ : (g₂ * g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g * g ^ k)
⊢ (g₂ ^ (k + 1)) ∘ₛₗ f = f ∘ₛₗ (g ^ (k + 1))
have succ₂ : (g₂ ∘ₗ g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g * g ^ k)
Tactic: rw [pow_succ', pow_succ', mul_eq_comp, LinearMap.comp_assoc, ih,
    ← LinearMap.comp_assoc, h, LinearMap.comp_assoc, mul_eq_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
k : ℕ
ih : (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)
succ : (g₂ * g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ (k + 1))
succ₁ : (g₂ * g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g * g ^ k)
succ₂ : (g₂ ∘ₗ g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g * g ^ k)
⊢ (g₂ ^ (k + 1)) ∘ₛₗ f = f ∘ₛₗ (g ^ (k + 1))
have succ₃ : g₂ ∘ₛₗ (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g * g ^ k)
Tactic: rw [pow_succ', pow_succ', mul_eq_comp, LinearMap.comp_assoc, ih,
    ← LinearMap.comp_assoc, h, LinearMap.comp_assoc, mul_eq_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
k : ℕ
ih : (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)
succ : (g₂ * g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ (k + 1))
succ₁ : (g₂ * g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g * g ^ k)
succ₂ : (g₂ ∘ₗ g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g * g ^ k)
succ₃ : g₂ ∘ₛₗ (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g * g ^ k)
⊢ (g₂ ^ (k + 1)) ∘ₛₗ f = f ∘ₛₗ (g ^ (k + 1))
have succ₄ : g₂ ∘ₛₗ f ∘ₛₗ (g ^ k) = f ∘ₛₗ (g * g ^ k)
Tactic: rw [pow_succ', pow_succ', mul_eq_comp, LinearMap.comp_assoc, ih,
    ← LinearMap.comp_assoc, h, LinearMap.comp_assoc, mul_eq_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
k : ℕ
ih : (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)
succ : (g₂ * g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ (k + 1))
succ₁ : (g₂ * g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g * g ^ k)
succ₂ : (g₂ ∘ₗ g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g * g ^ k)
succ₃ : g₂ ∘ₛₗ (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g * g ^ k)
succ₄ : g₂ ∘ₛₗ f ∘ₛₗ (g ^ k) = f ∘ₛₗ (g * g ^ k)
⊢ (g₂ ^ (k + 1)) ∘ₛₗ f = f ∘ₛₗ (g ^ (k + 1))
have succ₅ : (g₂ ∘ₛₗ f) ∘ₛₗ (g ^ k) = f ∘ₛₗ (g * g ^ k)
Tactic: rw [pow_succ', pow_succ', mul_eq_comp, LinearMap.comp_assoc, ih,
    ← LinearMap.comp_assoc, h, LinearMap.comp_assoc, mul_eq_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
k : ℕ
ih : (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)
succ : (g₂ * g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ (k + 1))
succ₁ : (g₂ * g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g * g ^ k)
succ₂ : (g₂ ∘ₗ g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g * g ^ k)
succ₃ : g₂ ∘ₛₗ (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g * g ^ k)
succ₄ : g₂ ∘ₛₗ f ∘ₛₗ (g ^ k) = f ∘ₛₗ (g * g ^ k)
succ₅ : (g₂ ∘ₛₗ f) ∘ₛₗ (g ^ k) = f ∘ₛₗ (g * g ^ k)
⊢ (g₂ ^ (k + 1)) ∘ₛₗ f = f ∘ₛₗ (g ^ (k + 1))
have succ₆ : (f ∘ₛₗ g) ∘ₛₗ (g ^ k) = f ∘ₛₗ (g * g ^ k)
Tactic: rw [pow_succ', pow_succ', mul_eq_comp, LinearMap.comp_assoc, ih,
    ← LinearMap.comp_assoc, h, LinearMap.comp_assoc, mul_eq_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
k : ℕ
ih : (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)
succ : (g₂ * g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ (k + 1))
succ₁ : (g₂ * g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g * g ^ k)
succ₂ : (g₂ ∘ₗ g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g * g ^ k)
succ₃ : g₂ ∘ₛₗ (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g * g ^ k)
succ₄ : g₂ ∘ₛₗ f ∘ₛₗ (g ^ k) = f ∘ₛₗ (g * g ^ k)
succ₅ : (g₂ ∘ₛₗ f) ∘ₛₗ (g ^ k) = f ∘ₛₗ (g * g ^ k)
succ₆ : (f ∘ₛₗ g) ∘ₛₗ (g ^ k) = f ∘ₛₗ (g * g ^ k)
⊢ (g₂ ^ (k + 1)) ∘ₛₗ f = f ∘ₛₗ (g ^ (k + 1))
have succ₇ : f ∘ₛₗ (g ∘ₗ g ^ k) = f ∘ₛₗ (g * g ^ k)
Tactic: rw [pow_succ', pow_succ', mul_eq_comp, LinearMap.comp_assoc, ih,
    ← LinearMap.comp_assoc, h, LinearMap.comp_assoc, mul_eq_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
k : ℕ
ih : (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)
succ : (g₂ * g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ (k + 1))
succ₁ : (g₂ * g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g * g ^ k)
succ₂ : (g₂ ∘ₗ g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g * g ^ k)
succ₃ : g₂ ∘ₛₗ (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g * g ^ k)
succ₄ : g₂ ∘ₛₗ f ∘ₛₗ (g ^ k) = f ∘ₛₗ (g * g ^ k)
succ₅ : (g₂ ∘ₛₗ f) ∘ₛₗ (g ^ k) = f ∘ₛₗ (g * g ^ k)
succ₆ : (f ∘ₛₗ g) ∘ₛₗ (g ^ k) = f ∘ₛₗ (g * g ^ k)
succ₇ : f ∘ₛₗ (g ∘ₗ g ^ k) = f ∘ₛₗ (g * g ^ k)
⊢ (g₂ ^ (k + 1)) ∘ₛₗ f = f ∘ₛₗ (g ^ (k + 1))
have succ₈ : f ∘ₛₗ (g ∘ₗ g ^ k) = f ∘ₛₗ (g ∘ₗ g ^ k)
Tactic: rw [pow_succ', pow_succ', mul_eq_comp, LinearMap.comp_assoc, ih,
    ← LinearMap.comp_assoc, h, LinearMap.comp_assoc, mul_eq_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
k : ℕ
⊢ (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)
have zero : HPow.hPow (β := ℕ) g₂ 0 ∘ₛₗ f = f ∘ₛₗ HPow.hPow (β := ℕ) g 0
Tactic: induction k with
  | zero => simp [one_eq_id]
  | succ k ih => rw [pow_succ', pow_succ', mul_eq_comp, LinearMap.comp_assoc, ih,
    ← LinearMap.comp_assoc, h, LinearMap.comp_assoc, mul_eq_comp]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
k : ℕ
zero : HPow.hPow (β := ℕ) g₂ 0 ∘ₛₗ f = f ∘ₛₗ HPow.hPow (β := ℕ) g 0
⊢ (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)
have succ : ∀ (k : ℕ) (ih : (g₂ ^ k) ∘ₛₗ f = f ∘ₛₗ (g ^ k)), (g₂ ^ (k + 1)) ∘ₛₗ f = f ∘ₛₗ (g ^ (k + 1))
Tactic: induction k with
  | zero => simp [one_eq_id]
  | succ k ih => rw [pow_succ', pow_succ', mul_eq_comp, LinearMap.comp_assoc, ih,
    ← LinearMap.comp_assoc, h, LinearMap.comp_assoc, mul_eq_comp]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : End R M
n : ℕ
⊢ f' ^ (n + 1) = (f' ^ n) ∘ₗ f'
have rw : f' ^ n * f' = (f' ^ n) ∘ₗ f'
Tactic: rw [pow_succ, mul_eq_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : End R M
n : ℕ
rw : f' ^ n * f' = (f' ^ n) ∘ₗ f'
⊢ f' ^ (n + 1) = (f' ^ n) ∘ₗ f'
have rw₁ : (f' ^ n) ∘ₗ f' = (f' ^ n) ∘ₗ f'
Tactic: rw [pow_succ, mul_eq_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : End R M
n : ℕ
⊢ f' ^ (n + 1) = f' ∘ₗ f' ^ n
have rw : f' * f' ^ n = f' ∘ₗ f' ^ n
Tactic: rw [pow_succ', mul_eq_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : End R M
n : ℕ
rw : f' * f' ^ n = f' ∘ₗ f' ^ n
⊢ f' ^ (n + 1) = f' ∘ₗ f' ^ n
have rw₁ : f' ∘ₗ f' ^ n = f' ∘ₗ f' ^ n
Tactic: rw [pow_succ', mul_eq_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : End R M
h : Surjective (α := M) (β := M) (⇑f' : (a : M) → M)
n : ℕ
⊢ Surjective (α := M) (β := M) (⇑(f' ^ (n + 1)) : (a : M) → M)
have rw : Surjective (α := M) (β := M) (⇑((f' ^ n) ∘ₗ f') : (a : M) → M)
Tactic: rw [iterate_succ]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : End R M
h : Injective (α := M) (β := M) (⇑f' : (a : M) → M)
n : ℕ
⊢ Injective (α := M) (β := M) (⇑(f' ^ (n + 1)) : (a : M) → M)
have rw : Injective (α := M) (β := M) (⇑((f' ^ n) ∘ₗ f') : (a : M) → M)
Tactic: rw [iterate_succ]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : End R M
h : Bijective (α := M) (β := M) (⇑f' : (a : M) → M)
n : ℕ
⊢ Bijective (α := M) (β := M) (⇑(f' ^ (n + 1)) : (a : M) → M)
have rw : Bijective (α := M) (β := M) (⇑((f' ^ n) ∘ₗ f') : (a : M) → M)
Tactic: rw [iterate_succ]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (hypothesis)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : End R M
n : ℕ
hn : n ≠ 0
h : Injective (α := M) (β := M) (⇑(f' ^ n) : (a : M) → M)
⊢ Injective (α := M) (β := M) (⇑f' : (a : M) → M)
have h₁ : Injective (α := M) (β := M) (Function.comp (β := M) (⇑(f' ^ n.pred) : (a : M) → M) (⇑f' : (a : M) → M))
Tactic: rw [← Nat.succ_pred_eq_of_pos (show 0 < n by lia), iterate_succ, coe_comp] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (hypothesis)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : End R M
n : ℕ
hn : n ≠ 0
h : Surjective (α := M) (β := M) (⇑(f' ^ n) : (a : M) → M)
⊢ Surjective (α := M) (β := M) (⇑f' : (a : M) → M)
have h₁ : Surjective (α := M) (β := M) (Function.comp (β := M) (⇑f' : (a : M) → M) (⇑(f' ^ n.pred) : (a : M) → M))
Tactic: rw [← Nat.succ_pred_eq_of_pos (Nat.pos_iff_ne_zero.mpr hn), pow_succ', coe_mul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : Semiring S
inst_6 : Module R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
f : M₁ →ₗ[R] S
x_1 : M
x y : M₁
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) (x + y) : S) x_1 =
    HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) x : S) x_1 +
      HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) y : S) x_1
have rw : HAdd.hAdd (α := S) (β := S) ((f : (a : M₁) → S) x : S) ((f : (a : M₁) → S) y : S) • x_1 =
  HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) x : S) x_1 +
    HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) y : S) x_1
Tactic: rw [f.map_add, add_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : Semiring S
inst_6 : Module R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
f : M₁ →ₗ[R] S
x_1 : M
x y : M₁
rw :
  HAdd.hAdd (α := S) (β := S) ((f : (a : M₁) → S) x : S) ((f : (a : M₁) → S) y : S) • x_1 =
    HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) x : S) x_1 +
      HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) y : S) x_1
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) (x + y) : S) x_1 =
    HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) x : S) x_1 +
      HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) y : S) x_1
have rw₁ : HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) x : S) x_1 +
    HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) y : S) x_1 =
  HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) x : S) x_1 +
    HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) y : S) x_1
Tactic: rw [f.map_add, add_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : Semiring S
inst_6 : Module R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
f : M₁ →ₗ[R] S
x : M
b : R
y : M₁
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) (b • y) : S) x =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) b : R)
      (HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) y : S) x)
have rw : HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) (b • y) : S) x =
  b • HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) y : S) x
Tactic: rw [RingHom.id_apply, map_smul, smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.End (goal)
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : Semiring S
inst_6 : Module R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
f : M₁ →ₗ[R] S
x : M
b : R
y : M₁
rw :
  HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) (b • y) : S) x =
    b • HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) y : S) x
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) (b • y) : S) x =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) b : R)
      (HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) y : S) x)
have rw₁ : HSMul.hSMul (β := S) b ((f : (a : M₁) → S) y : S) • x =
  b • HSMul.hSMul.{u_3, u_4, u_4} (α := S) ((f : (a : M₁) → S) y : S) x
Tactic: rw [RingHom.id_apply, map_smul, smul_assoc]