awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.LinearMap (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
ι : Type u_9
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 : AddCommMonoid M₃
inst_7 : Module R M
inst_8 : Module R M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_11 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
M₂' : Type u_10
inst_12 : AddCommMonoid M₂'
inst_13 : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective.{u_10 + 1, u_7 + 1} (α := M₂') (β := M₂) (⇑p : (a : M₂') → M₂)
h :
  ∀ (c : M),
    Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_10 + 1} (ι := M₂') (⇑p : (a : M₂') → M₂))
      ((f : (a : M) → M₂) c : M₂)
b c : M
a :
  (p : (a : M₂') → M₂)
      (Exists.choose (p := fun (y : M₂') ↦
        (p : (a : M₂') → M₂) y = HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : M) → M₂) b : M₂) ((f : (a : M) → M₂) c : M₂))
        ⋯) =
    HAdd.hAdd (α := M₂) (β := M₂)
      ((p : (a : M₂') → M₂)
          (Exists.choose (p := fun (y : M₂') ↦
            Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) b : M₂)) ⋯) :
        M₂)
      ((p : (a : M₂') → M₂)
          (Exists.choose (p := fun (y : M₂') ↦
            Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) c : M₂)) ⋯) :
        M₂)
a₁ :
  (p : (a : M₂') → M₂)
      (Exists.choose (p := fun (y : M₂') ↦
        (p : (a : M₂') → M₂) y = HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : M) → M₂) b : M₂) ((f : (a : M) → M₂) c : M₂))
        ⋯) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : M) → M₂) b : M₂) ((f : (a : M) → M₂) c : M₂)
⊢ Eq.{u_7 + 1} (α := M₂)
    ((p : (a : M₂') → M₂)
        (Exists.choose (p := fun (y : M₂') ↦
          Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) (b + c) : M₂)) ⋯) :
      M₂)
    ((p : (a : M₂') → M₂)
        (Exists.choose (p := fun (y : M₂') ↦
            Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) b : M₂)) ⋯ +
          Exists.choose (p := fun (y : M₂') ↦
            Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) c : M₂)) ⋯) :
      M₂)
have a₂ : Eq.{u_7 + 1} (α := M₂)
  ((p : (a : M₂') → M₂)
      (Exists.choose (p := fun (y : M₂') ↦
        Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) (b + c) : M₂)) sorry) :
    M₂)
  ((f : (a : M) → M₂) (b + c) : M₂)
Tactic: simp_rw [map_add, (h _).choose_spec, ← map_add, (h _).choose_spec]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.LinearMap (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
ι : Type u_9
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 : AddCommMonoid M₃
inst_7 : Module R M
inst_8 : Module R M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_11 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
M₂' : Type u_10
inst_12 : AddCommMonoid M₂'
inst_13 : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective.{u_10 + 1, u_7 + 1} (α := M₂') (β := M₂) (⇑p : (a : M₂') → M₂)
h :
  ∀ (c : M),
    Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_10 + 1} (ι := M₂') (⇑p : (a : M₂') → M₂))
      ((f : (a : M) → M₂) c : M₂)
r : R
c : M
⊢ Exists.choose (p := fun (y : M₂') ↦
      Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) (r • c) : M₂)) ⋯ =
    HSMul.hSMul.{u_3, u_10, u_10} (α := R₂) ((σ₁₂ : (a : R) → R₂) r : R₂)
      (Exists.choose (p := fun (y : M₂') ↦
        Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) c : M₂)) ⋯)
have a : Eq.{u_7 + 1} (α := M₂)
  ((p : (a : M₂') → M₂)
      (Exists.choose (p := fun (y : M₂') ↦
        Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) (r • c) : M₂)) sorry) :
    M₂)
  ((p : (a : M₂') → M₂)
      (HSMul.hSMul.{u_3, u_10, u_10} (α := R₂) ((σ₁₂ : (a : R) → R₂) r : R₂)
        (Exists.choose (p := fun (y : M₂') ↦
          Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) c : M₂)) sorry)) :
    M₂)
Tactic: apply hp
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.LinearMap (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
ι : Type u_9
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 : AddCommMonoid M₃
inst_7 : Module R M
inst_8 : Module R M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_11 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
M₂' : Type u_10
inst_12 : AddCommMonoid M₂'
inst_13 : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective.{u_10 + 1, u_7 + 1} (α := M₂') (β := M₂) (⇑p : (a : M₂') → M₂)
h :
  ∀ (c : M),
    Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_10 + 1} (ι := M₂') (⇑p : (a : M₂') → M₂))
      ((f : (a : M) → M₂) c : M₂)
r : R
c : M
⊢ Eq.{u_7 + 1} (α := M₂)
    ((p : (a : M₂') → M₂)
        (Exists.choose (p := fun (y : M₂') ↦
          Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) (r • c) : M₂)) ⋯) :
      M₂)
    ((p : (a : M₂') → M₂)
        (HSMul.hSMul.{u_3, u_10, u_10} (α := R₂) ((σ₁₂ : (a : R) → R₂) r : R₂)
          (Exists.choose (p := fun (y : M₂') ↦
            Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) c : M₂)) ⋯)) :
      M₂)
have a : (p : (a : M₂') → M₂)
    (Exists.choose (p := fun (y : M₂') ↦
      Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) (r • c) : M₂)) sorry) =
  HSMul.hSMul.{u_3, u_7, u_7} (α := R₂) (β := M₂) ((σ₁₂ : (a : R) → R₂) r : R₂)
    ((p : (a : M₂') → M₂)
        (Exists.choose (p := fun (y : M₂') ↦
          Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) c : M₂)) sorry) :
      M₂)
Tactic: simp_rw [map_smul, (h _).choose_spec, map_smulₛₗ]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.LinearMap (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
ι : Type u_9
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 : AddCommMonoid M₃
inst_7 : Module R M
inst_8 : Module R M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst_11 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
M₂' : Type u_10
inst_12 : AddCommMonoid M₂'
inst_13 : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective.{u_10 + 1, u_7 + 1} (α := M₂') (β := M₂) (⇑p : (a : M₂') → M₂)
h :
  ∀ (c : M),
    Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_10 + 1} (ι := M₂') (⇑p : (a : M₂') → M₂))
      ((f : (a : M) → M₂) c : M₂)
r : R
c : M
a :
  (p : (a : M₂') → M₂)
      (Exists.choose (p := fun (y : M₂') ↦
        Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) (r • c) : M₂)) ⋯) =
    HSMul.hSMul.{u_3, u_7, u_7} (α := R₂) (β := M₂) ((σ₁₂ : (a : R) → R₂) r : R₂)
      ((p : (a : M₂') → M₂)
          (Exists.choose (p := fun (y : M₂') ↦
            Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) c : M₂)) ⋯) :
        M₂)
⊢ Eq.{u_7 + 1} (α := M₂)
    ((p : (a : M₂') → M₂)
        (Exists.choose (p := fun (y : M₂') ↦
          Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) (r • c) : M₂)) ⋯) :
      M₂)
    ((p : (a : M₂') → M₂)
        (HSMul.hSMul.{u_3, u_10, u_10} (α := R₂) ((σ₁₂ : (a : R) → R₂) r : R₂)
          (Exists.choose (p := fun (y : M₂') ↦
            Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) c : M₂)) ⋯)) :
      M₂)
have a₁ : (f : (a : M) → M₂) (r • c) =
  HSMul.hSMul.{u_3, u_7, u_7} (α := R₂) (β := M₂) ((σ₁₂ : (a : R) → R₂) r : R₂) ((f : (a : M) → M₂) c : M₂)
Tactic: simp_rw [map_smul, (h _).choose_spec, map_smulₛₗ]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.LinearMap (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
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₂
f : M →ₛₗ[σ₁₂] M₂
M₂' : Type u_10
inst_6 : AddCommMonoid M₂'
inst_7 : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective.{u_10 + 1, u_7 + 1} (α := M₂') (β := M₂) (⇑p : (a : M₂') → M₂)
h :
  ∀ (c : M),
    Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_10 + 1} (ι := M₂') (⇑p : (a : M₂') → M₂))
      ((f : (a : M) → M₂) c : M₂)
⊢ p ∘ₛₗ f.codLift p hp h = f
have h₁ : ∀ (x : M), Eq.{u_7 + 1} (α := M₂) ((p ∘ₛₗ f.codLift p hp h : (a : M) → M₂) x : M₂) ((f : (a : M) → M₂) x : M₂)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.LinearMap (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
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₂
f : M →ₛₗ[σ₁₂] M₂
M₂' : Type u_10
inst_6 : AddCommMonoid M₂'
inst_7 : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective.{u_10 + 1, u_7 + 1} (α := M₂') (β := M₂) (⇑p : (a : M₂') → M₂)
h :
  ∀ (c : M),
    Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_10 + 1} (ι := M₂') (⇑p : (a : M₂') → M₂))
      ((f : (a : M) → M₂) c : M₂)
x : M
⊢ Eq.{u_7 + 1} (α := M₂) ((p ∘ₛₗ f.codLift p hp h : (a : M) → M₂) x : M₂) ((f : (a : M) → M₂) x : M₂)
have h₁ : Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) ((f.codLift p hp h : (a : M) → M₂') x : M₂') : M₂)
  ((f : (a : M) → M₂) x : M₂)
Tactic: rw [comp_apply, codLift_apply, (h x).choose_spec]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.LinearMap (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
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₂
f : M →ₛₗ[σ₁₂] M₂
M₂' : Type u_10
inst_6 : AddCommMonoid M₂'
inst_7 : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective.{u_10 + 1, u_7 + 1} (α := M₂') (β := M₂) (⇑p : (a : M₂') → M₂)
h :
  ∀ (c : M),
    Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_10 + 1} (ι := M₂') (⇑p : (a : M₂') → M₂))
      ((f : (a : M) → M₂) c : M₂)
x : M
h₁ :
  Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) ((f.codLift p hp h : (a : M) → M₂') x : M₂') : M₂)
    ((f : (a : M) → M₂) x : M₂)
⊢ Eq.{u_7 + 1} (α := M₂) ((p ∘ₛₗ f.codLift p hp h : (a : M) → M₂) x : M₂) ((f : (a : M) → M₂) x : M₂)
have h₂ : Eq.{u_7 + 1} (α := M₂)
  ((p : (a : M₂') → M₂)
      (Exists.choose (p := fun (y : M₂') ↦
        Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) x : M₂)) sorry) :
    M₂)
  ((f : (a : M) → M₂) x : M₂)
Tactic: rw [comp_apply, codLift_apply, (h x).choose_spec]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.LinearMap (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
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₂
f : M →ₛₗ[σ₁₂] M₂
M₂' : Type u_10
inst_6 : AddCommMonoid M₂'
inst_7 : Module R₂ M₂'
p : M₂' →ₗ[R₂] M₂
hp : Injective.{u_10 + 1, u_7 + 1} (α := M₂') (β := M₂) (⇑p : (a : M₂') → M₂)
h :
  ∀ (c : M),
    Membership.mem.{u_7, u_7} (α := M₂) (γ := Set M₂) (range.{u_7, u_10 + 1} (ι := M₂') (⇑p : (a : M₂') → M₂))
      ((f : (a : M) → M₂) c : M₂)
x : M
h₁ :
  Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) ((f.codLift p hp h : (a : M) → M₂') x : M₂') : M₂)
    ((f : (a : M) → M₂) x : M₂)
h₂ :
  Eq.{u_7 + 1} (α := M₂)
    ((p : (a : M₂') → M₂)
        (Exists.choose (p := fun (y : M₂') ↦
          Eq.{u_7 + 1} (α := M₂) ((p : (a : M₂') → M₂) y : M₂) ((f : (a : M) → M₂) x : M₂)) ⋯) :
      M₂)
    ((f : (a : M) → M₂) x : M₂)
⊢ Eq.{u_7 + 1} (α := M₂) ((p ∘ₛₗ f.codLift p hp h : (a : M) → M₂) x : M₂) ((f : (a : M) → M₂) x : M₂)
have h₃ : Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) ((f : (a : M) → M₂) x : M₂)
Tactic: rw [comp_apply, codLift_apply, (h x).choose_spec]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.LinearMap (goal)
Goal:
R : Type u_10
R₂ : Type u_11
M : Type u_12
M₂ : Type u_13
inst : Ring R
inst_1 : Ring R₂
σ₁₂ : R →+* R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
p : Submodule R M
q : Submodule R₂ M₂
f g : M →ₛₗ[σ₁₂] M₂
hf : MapsTo (⇑f : (a : M) → M₂) (↑p : Set M) (↑q : Set M₂)
hg : MapsTo (⇑g : (a : M) → M₂) (↑p : Set M) (↑q : Set M₂)
hfg : MapsTo (⇑(f - g) : (a : M) → M₂) (↑p : Set M) (↑q : Set M₂)
⊢ f.restrict hf - g.restrict hg = (f - g).restrict hfg
have h : ∀ (x : ↥p),
  Eq.{u_13 + 1} (α := M₂) (↑((f.restrict hf - g.restrict hg : (a : ↥p) → ↥q) x) : M₂)
    (↑(((f - g).restrict hfg : (a : ↥p) → ↥q) x) : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.LinearMap (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : M →ₗ[R] M
h : Commute f g
p : Submodule R M
hf : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
hg : MapsTo (⇑g : (a : M) → M) (↑p : Set M) (↑p : Set M)
⊢ Commute (f.restrict hf) (g.restrict hg)
have change : (f ∘ₗ g).restrict sorry = (g ∘ₗ f).restrict sorry
Tactic: change (f ∘ₗ g).restrict (hf.comp hg) = (g ∘ₗ f).restrict (hg.comp hf)
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.LinearMap (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
g : Module.End R ↥N
G : Module.End R M
h : G ∘ₗ N.subtype = N.subtype ∘ₗ g
k : ℕ
hG : G ^ k = 0
⊢ g ^ k = 0
have h₁ : ∀ (m : ↥N), Eq.{u_5 + 1} (α := M) (↑((g ^ k : (a : ↥N) → ↥N) m) : M) (↑((0 : (a : ↥N) → ↥N) m) : M)
Tactic: ext m
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.LinearMap (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
g : Module.End R ↥N
G : Module.End R M
h : G ∘ₗ N.subtype = N.subtype ∘ₗ g
k : ℕ
hG : G ^ k = 0
m : ↥N
⊢ Eq (α := M) ((N.subtype ∘ₗ g ^ k : (a : ↥N) → M) m : M) (0 : M)
have rw : Eq (α := M) (((G ^ k) ∘ₗ N.subtype : (a : ↥N) → M) m : M) (0 : M)
Tactic: rw [← Module.End.commute_pow_left_of_commute h, hG, zero_comp, zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.LinearMap (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
g : Module.End R ↥N
G : Module.End R M
h : G ∘ₗ N.subtype = N.subtype ∘ₗ g
k : ℕ
hG : G ^ k = 0
m : ↥N
rw : Eq (α := M) (((G ^ k) ∘ₗ N.subtype : (a : ↥N) → M) m : M) (0 : M)
⊢ Eq (α := M) ((N.subtype ∘ₗ g ^ k : (a : ↥N) → M) m : M) (0 : M)
have rw₁ : Eq (α := M) ((0 ∘ₗ N.subtype : (a : ↥N) → M) m : M) (0 : M)
Tactic: rw [← Module.End.commute_pow_left_of_commute h, hG, zero_comp, zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.LinearMap (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
g : Module.End R ↥N
G : Module.End R M
h : G ∘ₗ N.subtype = N.subtype ∘ₗ g
k : ℕ
hG : G ^ k = 0
m : ↥N
rw : Eq (α := M) (((G ^ k) ∘ₗ N.subtype : (a : ↥N) → M) m : M) (0 : M)
rw₁ : Eq (α := M) ((0 ∘ₗ N.subtype : (a : ↥N) → M) m : M) (0 : M)
⊢ Eq (α := M) ((N.subtype ∘ₗ g ^ k : (a : ↥N) → M) m : M) (0 : M)
have rw₂ : Eq (α := M) ((0 : (a : ↥N) → M) m : M) (0 : M)
Tactic: rw [← Module.End.commute_pow_left_of_commute h, hG, zero_comp, zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.LinearMap (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
g : Module.End R ↥N
G : Module.End R M
h : G ∘ₗ N.subtype = N.subtype ∘ₗ g
k : ℕ
hG : G ^ k = 0
m : ↥N
rw : Eq (α := M) (((G ^ k) ∘ₗ N.subtype : (a : ↥N) → M) m : M) (0 : M)
rw₁ : Eq (α := M) ((0 ∘ₗ N.subtype : (a : ↥N) → M) m : M) (0 : M)
rw₂ : Eq (α := M) ((0 : (a : ↥N) → M) m : M) (0 : M)
⊢ Eq (α := M) ((N.subtype ∘ₗ g ^ k : (a : ↥N) → M) m : M) (0 : M)
have rw₃ : Eq.{u_5 + 1} (α := M) 0 0
Tactic: rw [← Module.End.commute_pow_left_of_commute h, hG, zero_comp, zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.LinearMap (hypothesis)
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
g : Module.End R ↥N
G : Module.End R M
h : G ∘ₗ N.subtype = N.subtype ∘ₗ g
k : ℕ
hG : G ^ k = 0
m : ↥N
⊢ Eq.{u_5 + 1} (α := M) (↑((g ^ k : (a : ↥N) → ↥N) m) : M) (↑((0 : (a : ↥N) → ↥N) m) : M)
have hg : Eq (α := M) ((N.subtype ∘ₗ g ^ k : (a : ↥N) → M) m : M) (0 : M)
Tactic: have hg : N.subtype.comp (g ^ k) m = 0 := by
    rw [← Module.End.commute_pow_left_of_commute h, hG, zero_comp, zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.LinearMap (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : M →ₗ[R] M
p : Submodule R M
n : ℕ
h : ∀ x ∈ p, Membership.mem (α := M) p ((f' : (a : M) → M) x : M)
x : M
hx : x ∈ p
⊢ Membership.mem (α := M) p ((f' ^ n : (a : M) → M) x : M)
have zero : ∀ (x : M) (hx : x ∈ p), Membership.mem (α := M) p ((HPow.hPow (β := ℕ) f' 0 : (a : M) → M) x : M)
Tactic: induction n generalizing x with
  | zero => simpa
  | succ n ih =>
    simpa only [iterate_succ, coe_comp, Function.comp_apply, restrict_apply] using ih _ (h _ hx)
Cleared hypotheses: n, x, hx
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.LinearMap (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : M →ₗ[R] M
p : Submodule R M
n : ℕ
h : ∀ x ∈ p, Membership.mem (α := M) p ((f' : (a : M) → M) x : M)
x : M
hx : x ∈ p
zero : ∀ (x : M) (hx : x ∈ p), Membership.mem (α := M) p ((HPow.hPow (β := ℕ) f' 0 : (a : M) → M) x : M)
⊢ Membership.mem (α := M) p ((f' ^ n : (a : M) → M) x : M)
have succ : ∀ (n : ℕ) (ih : ∀ (x : M) (hx : x ∈ p), Membership.mem (α := M) p ((f' ^ n : (a : M) → M) x : M)) (x : M) (hx : x ∈ p),
  Membership.mem (α := M) p ((f' ^ (n + 1) : (a : M) → M) x : M)
Tactic: induction n generalizing x with
  | zero => simpa
  | succ n ih =>
    simpa only [iterate_succ, coe_comp, Function.comp_apply, restrict_apply] using ih _ (h _ hx)
Cleared hypotheses: n, x, hx
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.LinearMap (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : M →ₗ[R] M
p : Submodule R M
n : ℕ
h : ∀ x ∈ p, Membership.mem (α := M) p ((f' : (a : M) → M) x : M)
h' : ∀ (x : M) (hx : x ∈ p), Membership.mem (α := M) p ((f' ^ n : (a : M) → M) x : M)
⊢ f'.restrict h ^ n = (f' ^ n).restrict h'
have h₁ : ∀ (x : ↥p),
  Eq.{u_5 + 1} (α := M) (↑((f'.restrict h ^ n : (a : ↥p) → ↥p) x) : M) (↑(((f' ^ n).restrict h' : (a : ↥p) → ↥p) x) : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.LinearMap (hypothesis)
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f' : M →ₗ[R] M
p : Submodule R M
n : ℕ
h : ∀ x ∈ p, Membership.mem (α := M) p ((f' : (a : M) → M) x : M)
h' : ∀ (x : M) (hx : x ∈ p), Membership.mem (α := M) p ((f' ^ n : (a : M) → M) x : M)
x : ↥p
⊢ Eq.{u_5 + 1} (α := M) (↑((f'.restrict h ^ n : (a : ↥p) → ↥p) x) : M) (↑(((f' ^ n).restrict h' : (a : ↥p) → ↥p) x) : M)
have this : Semiconj (α := ↥p) (Subtype.val (p := fun (x : M) ↦ x ∈ p)) (⇑(f'.restrict h) : (a : ↥p) → ↥p) (⇑f' : (a : M) → M)
Tactic: have : Semiconj (↑) (f'.restrict h) f' := fun _ ↦ coe_restrict_apply _ _
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
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 σ₁₂ σ₂₃ σ₁₃
p_1 p' : Submodule R M
q q' : Submodule R₂ M₂
x : M
inst_10 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
p : Submodule R M
c : R₂
y : M
hy : y ∈ (↑p : Set M)
⊢ Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M))
    (HSMul.hSMul (β := M₂) c ((f : (a : M) → M₂) y : M₂))
have obtain : ∀ (a : R),
  Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M))
    (HSMul.hSMul.{u_3, u_7, u_7} (α := R₂) (β := M₂) ((σ₁₂ : (a : R) → R₂) a : R₂) ((f : (a : M) → M₂) y : M₂))
Tactic: obtain ⟨a, rfl⟩ := σ₁₂.surjective c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
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 σ₁₂ σ₂₃ σ₁₃
p_1 p' : Submodule R M
q q' : Submodule R₂ M₂
x : M
σ₂₁ : R₂ →+* R
inst_10 : RingHomInvPair σ₁₂ σ₂₁
inst_11 : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
i : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p : Submodule R M
x_1 y : ↥p
⊢ (Equiv.Set.image (⇑f : (a : M) → M₂) (↑p : Set M) i).toFun (x_1 + y) =
    (Equiv.Set.image (⇑f : (a : M) → M₂) (↑p : Set M) i).toFun x_1 +
      (Equiv.Set.image (⇑f : (a : M) → M₂) (↑p : Set M) i).toFun y
have simp : Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M)) x)
    (HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : M) → M₂) (↑x_1 : M) : M₂) ((f : (a : M) → M₂) (↑y : M) : M₂)) sorry =
  HAdd.hAdd (α := ↥(map f p)) (β := ↥(map f p))
    (Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M)) x)
        ((f : (a : M) → M₂) (↑x_1 : M)) sorry :
      { x : M₂ // Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M)) x })
    (Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M)) x)
        ((f : (a : M) → M₂) (↑y : M)) sorry :
      { x : M₂ // Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M)) x })
Tactic: simp only [coe_add, map_add, Equiv.toFun_as_coe, Equiv.Set.image_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
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 σ₁₂ σ₂₃ σ₁₃
p_1 p' : Submodule R M
q q' : Submodule R₂ M₂
x : M
σ₂₁ : R₂ →+* R
inst_10 : RingHomInvPair σ₁₂ σ₂₁
inst_11 : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
i : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p : Submodule R M
m : R
x_1 : ↥p
⊢ (Equiv.Set.image (⇑f : (a : M) → M₂) (↑p : Set M) i).toFun (m • x_1) =
    HSMul.hSMul.{u_3, u_7, u_7} (α := R₂) ((σ₁₂ : (a : R) → R₂) m : R₂)
      ((Equiv.Set.image (⇑f : (a : M) → M₂) (↑p : Set M) i).toFun x_1)
have simp : Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M)) x)
    (HSMul.hSMul.{u_3, u_7, u_7} (α := R₂) (β := M₂) ((σ₁₂ : (a : R) → R₂) m : R₂) ((f : (a : M) → M₂) (↑x_1 : M) : M₂))
    sorry =
  HSMul.hSMul.{u_3, u_7, u_7} (α := R₂) (β := ↥(map f p)) ((σ₁₂ : (a : R) → R₂) m : R₂)
    (Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M)) x)
        ((f : (a : M) → M₂) (↑x_1 : M)) sorry :
      { x : M₂ // Membership.mem (γ := Set M₂) ((⇑f : (a : M) → M₂) '' (↑p : Set M)) x })
Tactic: simp only [coe_smul_of_tower, map_smulₛₗ _, Equiv.toFun_as_coe, Equiv.Set.image_apply]