awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
Goal:
R : Type u_1
S : Type u_5
M₃ : Type u_11
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M₃
inst_3 : Module S M₃
σ : R →+* S
f g : R →ₛₗ[σ] M₃
h : Eq.{u_11 + 1} (α := M₃) ((f : (a : R) → M₃) 1 : M₃) ((g : (a : R) → M₃) 1 : M₃)
x : R
rw : Eq.{u_11 + 1} (α := M₃) ((f : (a : R) → M₃) (x * 1) : M₃) ((g : (a : R) → M₃) (x * 1) : M₃)
rw₁ :
  Eq.{u_11 + 1} (α := M₃) ((f : (a : R) → M₃) (HSMul.hSMul (β := R) x 1) : M₃)
    ((g : (a : R) → M₃) (HSMul.hSMul (β := R) x 1) : M₃)
rw₂ :
  HSMul.hSMul.{u_5, u_11, u_11} (α := S) (β := M₃) ((σ : (a : R) → S) x : S) ((f : (a : R) → M₃) 1 : M₃) =
    (g : (a : R) → M₃) (HSMul.hSMul (β := R) x 1)
rw₃ :
  HSMul.hSMul.{u_5, u_11, u_11} (α := S) (β := M₃) ((σ : (a : R) → S) x : S) ((f : (a : R) → M₃) 1 : M₃) =
    HSMul.hSMul.{u_5, u_11, u_11} (α := S) (β := M₃) ((σ : (a : R) → S) x : S) ((g : (a : R) → M₃) 1 : M₃)
⊢ Eq.{u_11 + 1} (α := M₃) ((f : (a : R) → M₃) x : M₃) ((g : (a : R) → M₃) x : M₃)
have rw₄ : HSMul.hSMul.{u_5, u_11, u_11} (α := S) (β := M₃) ((σ : (a : R) → S) x : S) ((g : (a : R) → M₃) 1 : M₃) =
  HSMul.hSMul.{u_5, u_11, u_11} (α := S) (β := M₃) ((σ : (a : R) → S) x : S) ((g : (a : R) → M₃) 1 : M₃)
Tactic: rw [← mul_one x, ← smul_eq_mul, f.map_smulₛₗ, g.map_smulₛₗ, h]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₂ →ₛₗ[σ₂₃] M₃
hf : Injective.{u_10 + 1, u_11 + 1} (α := M₂) (β := M₃) (⇑f : (a : M₂) → M₃)
g₁ g₂ : M₁ →ₛₗ[σ₁₂] M₂
h : f ∘ₛₗ g₁ = f ∘ₛₗ g₂
x : M₁
⊢ Eq.{u_11 + 1} (α := M₃) ((f : (a : M₂) → M₃) ((g₁ : (a : M₁) → M₂) x : M₂) : M₃)
    ((f : (a : M₂) → M₃) ((g₂ : (a : M₁) → M₂) x : M₂) : M₃)
have rw : Eq.{u_11 + 1} (α := M₃) ((f ∘ₛₗ g₁ : (a : M₁) → M₃) x : M₃) ((f : (a : M₂) → M₃) ((g₂ : (a : M₁) → M₂) x : M₂) : M₃)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₂ →ₛₗ[σ₂₃] M₃
hf : Injective.{u_10 + 1, u_11 + 1} (α := M₂) (β := M₃) (⇑f : (a : M₂) → M₃)
g₁ g₂ : M₁ →ₛₗ[σ₁₂] M₂
h : f ∘ₛₗ g₁ = f ∘ₛₗ g₂
x : M₁
rw :
  Eq.{u_11 + 1} (α := M₃) ((f ∘ₛₗ g₁ : (a : M₁) → M₃) x : M₃) ((f : (a : M₂) → M₃) ((g₂ : (a : M₁) → M₂) x : M₂) : M₃)
⊢ Eq.{u_11 + 1} (α := M₃) ((f : (a : M₂) → M₃) ((g₁ : (a : M₁) → M₂) x : M₂) : M₃)
    ((f : (a : M₂) → M₃) ((g₂ : (a : M₁) → M₂) x : M₂) : M₃)
have rw₁ : Eq.{u_11 + 1} (α := M₃) ((f ∘ₛₗ g₂ : (a : M₁) → M₃) x : M₃) ((f : (a : M₂) → M₃) ((g₂ : (a : M₁) → M₂) x : M₂) : M₃)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₂ →ₛₗ[σ₂₃] M₃
hf : Injective.{u_10 + 1, u_11 + 1} (α := M₂) (β := M₃) (⇑f : (a : M₂) → M₃)
g₁ g₂ : M₁ →ₛₗ[σ₁₂] M₂
h : f ∘ₛₗ g₁ = f ∘ₛₗ g₂
x : M₁
rw :
  Eq.{u_11 + 1} (α := M₃) ((f ∘ₛₗ g₁ : (a : M₁) → M₃) x : M₃) ((f : (a : M₂) → M₃) ((g₂ : (a : M₁) → M₂) x : M₂) : M₃)
rw₁ :
  Eq.{u_11 + 1} (α := M₃) ((f ∘ₛₗ g₂ : (a : M₁) → M₃) x : M₃) ((f : (a : M₂) → M₃) ((g₂ : (a : M₁) → M₂) x : M₂) : M₃)
⊢ Eq.{u_11 + 1} (α := M₃) ((f : (a : M₂) → M₃) ((g₁ : (a : M₁) → M₂) x : M₂) : M₃)
    ((f : (a : M₂) → M₃) ((g₂ : (a : M₁) → M₂) x : M₂) : M₃)
have rw₂ : Eq.{u_11 + 1} (α := M₃) ((f : (a : M₂) → M₃) ((g₂ : (a : M₁) → M₂) x : M₂) : M₃)
  ((f : (a : M₂) → M₃) ((g₂ : (a : M₁) → M₂) x : M₂) : M₃)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₂ →ₛₗ[σ₂₃] M₃
σ₃₂ : R₃ →+* R₂
inst_7 : RingHomInvPair σ₂₃ σ₃₂
inst_8 : RingHomCompTriple σ₁₃ σ₃₂ σ₁₂
hf : ∃ (f' : M₃ →ₛₗ[σ₃₂] M₂), f ∘ₛₗ f' = id
h : M₁ →ₛₗ[σ₁₃] M₃
⊢ ∃ (a : M₁ →ₛₗ[σ₁₂] M₂), (fun (g : M₁ →ₛₗ[σ₁₂] M₂) ↦ f ∘ₛₗ g) a = h
have obtain : ∀ (f' : M₃ →ₛₗ[σ₃₂] M₂) (hf' : f ∘ₛₗ f' = id), ∃ (a : M₁ →ₛₗ[σ₁₂] M₂), (fun (g : M₁ →ₛₗ[σ₁₂] M₂) ↦ f ∘ₛₗ g) a = h
Tactic: obtain ⟨f', hf'⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₂ →ₛₗ[σ₂₃] M₃
σ₃₂ : R₃ →+* R₂
inst_7 : RingHomInvPair σ₂₃ σ₃₂
inst_8 : RingHomCompTriple σ₁₃ σ₃₂ σ₁₂
h : M₁ →ₛₗ[σ₁₃] M₃
f' : M₃ →ₛₗ[σ₃₂] M₂
hf' : f ∘ₛₗ f' = id
⊢ ∃ (a : M₁ →ₛₗ[σ₁₂] M₂), (fun (g : M₁ →ₛₗ[σ₁₂] M₂) ↦ f ∘ₛₗ g) a = h
have refine : (fun (g : M₁ →ₛₗ[σ₁₂] M₂) ↦ f ∘ₛₗ g) (f' ∘ₛₗ h) = h
Tactic: refine ⟨f'.comp h, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₂ →ₛₗ[σ₂₃] M₃
σ₃₂ : R₃ →+* R₂
inst_7 : RingHomInvPair σ₂₃ σ₃₂
inst_8 : RingHomCompTriple σ₁₃ σ₃₂ σ₁₂
h : M₁ →ₛₗ[σ₁₃] M₃
f' : M₃ →ₛₗ[σ₃₂] M₂
hf' : f ∘ₛₗ f' = id
simp_rw simp_rw₁ : f ∘ₛₗ f' ∘ₛₗ h = h
⊢ (fun (g : M₁ →ₛₗ[σ₁₂] M₂) ↦ f ∘ₛₗ g) (f' ∘ₛₗ h) = h
have simp_rw₂ : (f ∘ₛₗ f') ∘ₛₗ h = h
Tactic: simp_rw [← comp_assoc, hf', id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₂ →ₛₗ[σ₂₃] M₃
σ₃₂ : R₃ →+* R₂
inst_7 : RingHomInvPair σ₂₃ σ₃₂
inst_8 : RingHomCompTriple σ₁₃ σ₃₂ σ₁₂
h : M₁ →ₛₗ[σ₁₃] M₃
f' : M₃ →ₛₗ[σ₃₂] M₂
hf' : f ∘ₛₗ f' = id
simp_rw simp_rw₁ : f ∘ₛₗ f' ∘ₛₗ h = h
simp_rw₂ : (f ∘ₛₗ f') ∘ₛₗ h = h
⊢ (fun (g : M₁ →ₛₗ[σ₁₂] M₂) ↦ f ∘ₛₗ g) (f' ∘ₛₗ h) = h
have simp_rw₃ : id ∘ₛₗ h = h
Tactic: simp_rw [← comp_assoc, hf', id_comp]
-- 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 S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : Module R M
inst_6 : Module S M₂
σ : R →+* S
σ' : S →+* R
inst_7 : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ → M
h₁ : ∀ (x : M), g ((f : (a : M) → M₂) x) = x
h₂ : ∀ (x : M₂), (f : (a : M) → M₂) (g x) = x
x y : M₂
⊢ g (x + y) = g x + g y
have rw : g ((f : (a : M) → M₂) (g (x + y))) = g ((f : (a : M) → M₂) (g x + g y))
Tactic: rw [← h₁ (g (x + y)), ← h₁ (g x + g y)]
-- 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 S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : Module R M
inst_6 : Module S M₂
σ : R →+* S
σ' : S →+* R
inst_7 : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ → M
h₁ : ∀ (x : M), g ((f : (a : M) → M₂) x) = x
h₂ : ∀ (x : M₂), (f : (a : M) → M₂) (g x) = x
a : S
b : M₂
⊢ g (a • b) = HSMul.hSMul.{u_1, u_8, u_8} (α := R) ((σ' : (a : S) → R) a : R) (g b)
have rw : g ((f : (a : M) → M₂) (g (a • b))) =
  g ((f : (a : M) → M₂) (HSMul.hSMul.{u_1, u_8, u_8} (α := R) ((σ' : (a : S) → R) a : R) (g b)))
Tactic: rw [← h₁ (g (a • b)), ← h₁ (σ' a • g b)]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module S M₂
σ : R →+* S
σ' : S →+* R
inst_6 : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ →ₛₗ[σ'] M
h : g ∘ₛₗ f = id
⊢ Injective.{u_8 + 1, u_8 + 1} (α := M) (β := M)
    (Function.comp.{u_8 + 1, u_10 + 1, u_8 + 1} (β := M₂) (⇑g : (a : M₂) → M) (⇑f : (a : M) → M₂))
have simp_rw : Injective (α := M) (β := M) (⇑(g ∘ₛₗ f) : (a : M) → M)
Tactic: simp_rw [← coe_comp, h, id_coe, bijective_id.1]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module S M₂
σ : R →+* S
σ' : S →+* R
inst_6 : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ →ₛₗ[σ'] M
h : g ∘ₛₗ f = id
simp_rw : Injective (α := M) (β := M) (⇑(g ∘ₛₗ f) : (a : M) → M)
⊢ Injective.{u_8 + 1, u_8 + 1} (α := M) (β := M)
    (Function.comp.{u_8 + 1, u_10 + 1, u_8 + 1} (β := M₂) (⇑g : (a : M₂) → M) (⇑f : (a : M) → M₂))
have simp_rw₁ : Injective.{u_8 + 1, u_8 + 1} (α := M) (β := M) (⇑id : (a : M) → M)
Tactic: simp_rw [← coe_comp, h, id_coe, bijective_id.1]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module S M₂
σ : R →+* S
σ' : S →+* R
inst_6 : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ →ₛₗ[σ'] M
h : g ∘ₛₗ f = id
simp_rw : Injective (α := M) (β := M) (⇑(g ∘ₛₗ f) : (a : M) → M)
simp_rw₁ : Injective.{u_8 + 1, u_8 + 1} (α := M) (β := M) (⇑id : (a : M) → M)
⊢ Injective.{u_8 + 1, u_8 + 1} (α := M) (β := M)
    (Function.comp.{u_8 + 1, u_10 + 1, u_8 + 1} (β := M₂) (⇑g : (a : M₂) → M) (⇑f : (a : M) → M₂))
have simp_rw₂ : Injective.{u_8 + 1, u_8 + 1} (α := M) _root_.id
Tactic: simp_rw [← coe_comp, h, id_coe, bijective_id.1]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module S M₂
σ : R →+* S
σ' : S →+* R
inst_6 : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ →ₛₗ[σ'] M
h : g ∘ₛₗ f = id
⊢ Surjective.{u_8 + 1, u_8 + 1} (α := M) (β := M)
    (Function.comp.{u_8 + 1, u_10 + 1, u_8 + 1} (β := M₂) (⇑g : (a : M₂) → M) (⇑f : (a : M) → M₂))
have simp_rw : Surjective (α := M) (β := M) (⇑(g ∘ₛₗ f) : (a : M) → M)
Tactic: simp_rw [← coe_comp, h, id_coe, bijective_id.2]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module S M₂
σ : R →+* S
σ' : S →+* R
inst_6 : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ →ₛₗ[σ'] M
h : g ∘ₛₗ f = id
simp_rw : Surjective (α := M) (β := M) (⇑(g ∘ₛₗ f) : (a : M) → M)
⊢ Surjective.{u_8 + 1, u_8 + 1} (α := M) (β := M)
    (Function.comp.{u_8 + 1, u_10 + 1, u_8 + 1} (β := M₂) (⇑g : (a : M₂) → M) (⇑f : (a : M) → M₂))
have simp_rw₁ : Surjective.{u_8 + 1, u_8 + 1} (α := M) (β := M) (⇑id : (a : M) → M)
Tactic: simp_rw [← coe_comp, h, id_coe, bijective_id.2]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module S M₂
σ : R →+* S
σ' : S →+* R
inst_6 : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ →ₛₗ[σ'] M
h : g ∘ₛₗ f = id
simp_rw : Surjective (α := M) (β := M) (⇑(g ∘ₛₗ f) : (a : M) → M)
simp_rw₁ : Surjective.{u_8 + 1, u_8 + 1} (α := M) (β := M) (⇑id : (a : M) → M)
⊢ Surjective.{u_8 + 1, u_8 + 1} (α := M) (β := M)
    (Function.comp.{u_8 + 1, u_10 + 1, u_8 + 1} (β := M₂) (⇑g : (a : M₂) → M) (⇑f : (a : M) → M₂))
have simp_rw₂ : Surjective.{u_8 + 1, u_8 + 1} (α := M) _root_.id
Tactic: simp_rw [← coe_comp, h, id_coe, bijective_id.2]
-- 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_1 : 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 S_1
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
module_M : Module R M
module_M₂ : Module S_1 M₂
σ : R →+* S_1
f : M →ₛₗ[σ] M₂
S : Type u_14
inst_4 : Semiring S
inst_5 : Module S M
inst_6 : Module S M₂
fₗ : M →ₗ[S] M₂
c : ℤ
x : M
⊢ (fₗ : (a : M) → M₂) (c • x) = HSMul.hSMul (β := M₂) c ((fₗ : (a : M) → M₂) x : M₂)
have zero : (fₗ : (a : M) → M₂) (HSMul.hSMul (α := ℤ) 0 x) = HSMul.hSMul (α := ℤ) (β := M₂) 0 ((fₗ : (a : M) → M₂) x : M₂)
Tactic: induction c with
    | zero => simp
    | succ n ih => simp [add_smul]
    | pred n ih => simp [sub_smul]
Cleared hypotheses: c
-- 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_1 : 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 S_1
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
module_M : Module R M
module_M₂ : Module S_1 M₂
σ : R →+* S_1
f : M →ₛₗ[σ] M₂
S : Type u_14
inst_4 : Semiring S
inst_5 : Module S M
inst_6 : Module S M₂
fₗ : M →ₗ[S] M₂
c : ℤ
x : M
zero : (fₗ : (a : M) → M₂) (HSMul.hSMul (α := ℤ) 0 x) = HSMul.hSMul (α := ℤ) (β := M₂) 0 ((fₗ : (a : M) → M₂) x : M₂)
⊢ (fₗ : (a : M) → M₂) (c • x) = HSMul.hSMul (β := M₂) c ((fₗ : (a : M) → M₂) x : M₂)
have succ : ∀ (n : ℕ)
  (ih :
    (fₗ : (a : M) → M₂) (HSMul.hSMul (α := ℤ) (↑n : ℤ) x) =
      HSMul.hSMul (α := ℤ) (β := M₂) (↑n : ℤ) ((fₗ : (a : M) → M₂) x : M₂)),
  (fₗ : (a : M) → M₂) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 • x) =
    HSMul.hSMul (β := M₂) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) ((fₗ : (a : M) → M₂) x : M₂)
Tactic: induction c with
    | zero => simp
    | succ n ih => simp [add_smul]
    | pred n ih => simp [sub_smul]
Cleared hypotheses: c
-- 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_1 : 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 S_1
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
module_M : Module R M
module_M₂ : Module S_1 M₂
σ : R →+* S_1
f : M →ₛₗ[σ] M₂
S : Type u_14
inst_4 : Semiring S
inst_5 : Module S M
inst_6 : Module S M₂
fₗ : M →ₗ[S] M₂
c : ℤ
x : M
zero : (fₗ : (a : M) → M₂) (HSMul.hSMul (α := ℤ) 0 x) = HSMul.hSMul (α := ℤ) (β := M₂) 0 ((fₗ : (a : M) → M₂) x : M₂)
succ :
  ∀ (n : ℕ)
    (ih :
      (fₗ : (a : M) → M₂) (HSMul.hSMul (α := ℤ) (↑n : ℤ) x) =
        HSMul.hSMul (α := ℤ) (β := M₂) (↑n : ℤ) ((fₗ : (a : M) → M₂) x : M₂)),
    (fₗ : (a : M) → M₂) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 • x) =
      HSMul.hSMul (β := M₂) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) ((fₗ : (a : M) → M₂) x : M₂)
⊢ (fₗ : (a : M) → M₂) (c • x) = HSMul.hSMul (β := M₂) c ((fₗ : (a : M) → M₂) x : M₂)
have pred : ∀ (n : ℕ)
  (ih :
    (fₗ : (a : M) → M₂) (HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x) =
      HSMul.hSMul (α := ℤ) (β := M₂) (-(↑n : ℤ)) ((fₗ : (a : M) → M₂) x : M₂)),
  (fₗ : (a : M) → M₂) (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1 • x) =
    HSMul.hSMul (β := M₂) (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) ((fₗ : (a : M) → M₂) x : M₂)
Tactic: induction c with
    | zero => simp
    | succ n ih => simp [add_smul]
    | pred n ih => simp [sub_smul]
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
Goal:
R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
inst_2 : Semiring R
inst_3 : Module R M
inst_4 : Semiring S
inst_5 : Module S M₂
σ : R →+* S
f g : M →ₑ+[(↑σ : R →* S)] M₂
h :
  Eq (α := M →ₛₗ[σ] M₂)
    (↑f :
      [inst_6 : FunLike (M →ₑ+[(↑σ : R →* S)] M₂) M M₂] →
        [SemilinearMapClass (M →ₑ+[(↑σ : R →* S)] M₂) σ M M₂] → M →ₛₗ[σ] M₂)
    (↑g :
      [inst_6 : FunLike (M →ₑ+[(↑σ : R →* S)] M₂) M M₂] →
        [SemilinearMapClass (M →ₑ+[(↑σ : R →* S)] M₂) σ M M₂] → M →ₛₗ[σ] M₂)
⊢ f = g
have a : ∀ (m : M), Eq.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) m : M₂) ((g : (a : M) → M₂) m : M₂)
Tactic: ext m
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
Goal:
R : Type u_14
M : Type u_15
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
c : R
⊢ IsLinearMap R (M₂ := M) fun (z : M) ↦ c • z
have refine : ∀ (c_1 : R) (x : M), c • c_1 • x = c_1 • c • x
Tactic: refine IsLinearMap.mk (smul_add c) ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
Goal:
M : Type u_8
M₂ : Type u_10
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
f g : M →+ M₂
h : f.toNatLinearMap = g.toNatLinearMap
⊢ f = g
have h₁ : ∀ (x : M), Eq.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((g : (a : M) → M₂) x : M₂)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
Goal:
M : Type u_8
M₂ : Type u_10
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
f g : M →+ M₂
h : f.toIntLinearMap = g.toIntLinearMap
⊢ f = g
have h₁ : ∀ (x : M), Eq.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((g : (a : M) → M₂) x : M₂)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_8
M₂ : Type u_10
M₃ : Type u_11
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 : Module R₁ M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →ₛₗ[σ₂₃] M₃
c : M
⊢ Eq.{u_11 + 1} (α := M₃) ((g.comp (σ₁₂ := σ₁₂) 0 : (a : M) → M₃) c : M₃) ((0 : (a : M) → M₃) c : M₃)
have rw : Eq.{u_11 + 1} (α := M₃) ((g : (a : M₂) → M₃) ((0 : (a : M) → M₂) c : M₂) : M₃) ((0 : (a : M) → M₃) c : M₃)
Tactic: rw [comp_apply, zero_apply, zero_apply, g.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_8
M₂ : Type u_10
M₃ : Type u_11
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 : Module R₁ M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →ₛₗ[σ₂₃] M₃
c : M
rw : Eq.{u_11 + 1} (α := M₃) ((g : (a : M₂) → M₃) ((0 : (a : M) → M₂) c : M₂) : M₃) ((0 : (a : M) → M₃) c : M₃)
⊢ Eq.{u_11 + 1} (α := M₃) ((g.comp (σ₁₂ := σ₁₂) 0 : (a : M) → M₃) c : M₃) ((0 : (a : M) → M₃) c : M₃)
have rw₁ : Eq.{u_11 + 1} (α := M₃) ((g : (a : M₂) → M₃) 0 : M₃) ((0 : (a : M) → M₃) c : M₃)
Tactic: rw [comp_apply, zero_apply, zero_apply, g.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_8
M₂ : Type u_10
M₃ : Type u_11
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 : Module R₁ M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →ₛₗ[σ₂₃] M₃
c : M
rw : Eq.{u_11 + 1} (α := M₃) ((g : (a : M₂) → M₃) ((0 : (a : M) → M₂) c : M₂) : M₃) ((0 : (a : M) → M₃) c : M₃)
rw₁ : Eq.{u_11 + 1} (α := M₃) ((g : (a : M₂) → M₃) 0 : M₃) ((0 : (a : M) → M₃) c : M₃)
⊢ Eq.{u_11 + 1} (α := M₃) ((g.comp (σ₁₂ := σ₁₂) 0 : (a : M) → M₃) c : M₃) ((0 : (a : M) → M₃) c : M₃)
have rw₂ : Eq.{u_11 + 1} (α := M₃) ((g : (a : M₂) → M₃) 0 : M₃) (0 : M₃)
Tactic: rw [comp_apply, zero_apply, zero_apply, g.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.LinearMap.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_8
M₂ : Type u_10
M₃ : Type u_11
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 : Module R₁ M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →ₛₗ[σ₂₃] M₃
c : M
rw : Eq.{u_11 + 1} (α := M₃) ((g : (a : M₂) → M₃) ((0 : (a : M) → M₂) c : M₂) : M₃) ((0 : (a : M) → M₃) c : M₃)
rw₁ : Eq.{u_11 + 1} (α := M₃) ((g : (a : M₂) → M₃) 0 : M₃) ((0 : (a : M) → M₃) c : M₃)
rw₂ : Eq.{u_11 + 1} (α := M₃) ((g : (a : M₂) → M₃) 0 : M₃) (0 : M₃)
⊢ Eq.{u_11 + 1} (α := M₃) ((g.comp (σ₁₂ := σ₁₂) 0 : (a : M) → M₃) c : M₃) ((0 : (a : M) → M₃) c : M₃)
have rw₃ : Eq.{u_11 + 1} (α := M₃) 0 0
Tactic: rw [comp_apply, zero_apply, zero_apply, g.map_zero]
-- 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
⊢ Eq.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((default : (a : M) → M₂) x : M₂)
have rw : Eq.{u_10 + 1} (α := M₂) ((f : (a : M) → M₂) 0 : M₂) ((default : (a : M) → M₂) 0 : M₂)
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_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₂)
⊢ 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 : M₂) ((default : (a : M) → M₂) 0 : M₂)
Tactic: rw [Subsingleton.elim x 0, map_zero, map_zero]