awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst_2 : AddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₁
inst_5 : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf_1 : Surjective.{u_5 + 1, u_6 + 1} (α := M₁) (β := M₂) (⇑φ : (a : M₁) → M₂)
b : M₁
hy : Membership.mem (α := M₂) (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) ((φ : (a : M₁) → M₂) b : M₂)
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf :
  ((DFinsupp.lsum ℕ (M := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)) :
            (a : (i : HeightOneSpectrum A) → ↥(primaryComponent M₁ i.asIdeal) →ₗ[A] M₁) →
              (Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) →ₗ[A] M₁)
          fun (i : HeightOneSpectrum A) ↦ Submodule.subtype (primaryComponent M₁ i.asIdeal) :
        (a : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) → M₁)
      f =
    b
refine_1 :
  Membership.mem (γ := Submodule A M₂)
    ((fun (P : HeightOneSpectrum A) ↦ (primaryComponent M₂ P.asIdeal : Submodule A M₂)) P)
    (HSub.hSub (α := M₂) (β := M₂) ((φ : (a : M₁) → M₂) b : M₂)
      ((φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) P) : M₁) : M₂))
⊢ HSub.hSub (α := M₂) (β := M₂) ((φ : (a : M₁) → M₂) b : M₂)
      ((φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) P) : M₁) : M₂) =
    0
have refine_2 : Membership.mem (γ := Submodule A M₂)
  (⨆ (j : HeightOneSpectrum A),
    ⨆ (_ : j ≠ P), (fun (P : HeightOneSpectrum A) ↦ (primaryComponent M₂ P.asIdeal : Submodule A M₂)) j)
  (HSub.hSub (α := M₂) (β := M₂) ((φ : (a : M₁) → M₂) b : M₂)
    ((φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) P) : M₁) : M₂))
Tactic: refine (Submodule.disjoint_def.mp (iSupIndep_primaryComponent A M₂ P)) _ ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst_2 : AddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₁
inst_5 : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf_1 : Surjective.{u_5 + 1, u_6 + 1} (α := M₁) (β := M₂) (⇑φ : (a : M₁) → M₂)
b : M₁
hy : Membership.mem (α := M₂) (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) ((φ : (a : M₁) → M₂) b : M₂)
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf :
  ((DFinsupp.lsum ℕ (M := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)) :
            (a : (i : HeightOneSpectrum A) → ↥(primaryComponent M₁ i.asIdeal) →ₗ[A] M₁) →
              (Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) →ₗ[A] M₁)
          fun (i : HeightOneSpectrum A) ↦ Submodule.subtype (primaryComponent M₁ i.asIdeal) :
        (a : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) → M₁)
      f =
    b
⊢ HSub.hSub (α := M₂) (β := M₂) ((φ : (a : M₁) → M₂) b : M₂)
      ((φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) P) : M₁) : M₂) =
    ∑ Q ∈ f.support (β := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)) \ {P},
      (φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) Q) : M₁)
have rw : Eq.{u_6 + 1} (α := M₂) ((φ : (a : M₁) → M₂) b : M₂)
  (∑ x ∈ f.support (β := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)),
      (φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) x) : M₁) :
    M₂)
Tactic: rw [sub_eq_iff_eq_add', ← Finset.sum_eq_add_sum_diff_singleton P (fun P ↦ φ (f P)) (by aesop)]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst_2 : AddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₁
inst_5 : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf_1 : Surjective.{u_5 + 1, u_6 + 1} (α := M₁) (β := M₂) (⇑φ : (a : M₁) → M₂)
b : M₁
hy : Membership.mem (α := M₂) (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) ((φ : (a : M₁) → M₂) b : M₂)
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf :
  ((DFinsupp.lsum ℕ (M := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)) :
            (a : (i : HeightOneSpectrum A) → ↥(primaryComponent M₁ i.asIdeal) →ₗ[A] M₁) →
              (Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) →ₗ[A] M₁)
          fun (i : HeightOneSpectrum A) ↦ Submodule.subtype (primaryComponent M₁ i.asIdeal) :
        (a : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) → M₁)
      f =
    b
⊢ Membership.mem (γ := Submodule A M₂)
    (⨆ (j : HeightOneSpectrum A),
      ⨆ (_ : j ≠ P), (fun (P : HeightOneSpectrum A) ↦ (primaryComponent M₂ P.asIdeal : Submodule A M₂)) j)
    (HSub.hSub (α := M₂) (β := M₂) ((φ : (a : M₁) → M₂) b : M₂)
      ((φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) P) : M₁) : M₂))
have hdiff : HSub.hSub (α := M₂) (β := M₂) ((φ : (a : M₁) → M₂) b : M₂)
    ((φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) P) : M₁) : M₂) =
  ∑ Q ∈ f.support (β := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)) \ {P},
    (φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) Q) : M₁)
Tactic: have hdiff : φ b - φ ↑(f P) = ∑ Q ∈ f.support \ {P}, φ ↑(f Q) := by
      rw [sub_eq_iff_eq_add', ← Finset.sum_eq_add_sum_diff_singleton P (fun P ↦ φ (f P)) (by aesop)]
      simpa [DFinsupp.sumAddHom_apply, DFinsupp.sum] using congr(φ $hf).symm
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst_2 : AddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₁
inst_5 : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf_1 : Surjective.{u_5 + 1, u_6 + 1} (α := M₁) (β := M₂) (⇑φ : (a : M₁) → M₂)
b : M₁
hy : Membership.mem (α := M₂) (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) ((φ : (a : M₁) → M₂) b : M₂)
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf :
  ((DFinsupp.lsum ℕ (M := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)) :
            (a : (i : HeightOneSpectrum A) → ↥(primaryComponent M₁ i.asIdeal) →ₗ[A] M₁) →
              (Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) →ₗ[A] M₁)
          fun (i : HeightOneSpectrum A) ↦ Submodule.subtype (primaryComponent M₁ i.asIdeal) :
        (a : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) → M₁)
      f =
    b
hdiff :
  HSub.hSub (α := M₂) (β := M₂) ((φ : (a : M₁) → M₂) b : M₂)
      ((φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) P) : M₁) : M₂) =
    ∑ Q ∈ f.support (β := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)) \ {P},
      (φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) Q) : M₁)
⊢ Membership.mem (γ := Submodule A M₂)
    (⨆ (j : HeightOneSpectrum A),
      ⨆ (_ : j ≠ P), (fun (P : HeightOneSpectrum A) ↦ (primaryComponent M₂ P.asIdeal : Submodule A M₂)) j)
    (HSub.hSub (α := M₂) (β := M₂) ((φ : (a : M₁) → M₂) b : M₂)
      ((φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) P) : M₁) : M₂))
have refine_2 : Membership.mem (γ := Submodule A M₂)
  (⨆ (j : HeightOneSpectrum A),
    ⨆ (_ : j ≠ P), (fun (P : HeightOneSpectrum A) ↦ (primaryComponent M₂ P.asIdeal : Submodule A M₂)) j)
  (∑ Q ∈ f.support (β := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)) \ {P},
    (φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) Q) : M₁))
Tactic: rw [hdiff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst_2 : AddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₁
inst_5 : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf : Surjective.{u_5 + 1, u_6 + 1} (α := M₁) (β := M₂) (⇑φ : (a : M₁) → M₂)
⊢ Surjective.{u_5 + 1, u_6 + 1} (α := ↥(primaryComponent M₁ P.asIdeal)) (β := ↥(primaryComponent M₂ P.asIdeal))
    (⇑(map P.asIdeal φ) : (a : ↥(primaryComponent M₁ P.asIdeal)) → ↥(primaryComponent M₂ P.asIdeal))
have rintro : ∀ (y : M₂) (hy : Membership.mem (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) y),
  ∃ (a : ↥(primaryComponent M₁ P.asIdeal)),
    (map P.asIdeal φ : (a : ↥(primaryComponent M₁ P.asIdeal)) → ↥(primaryComponent M₂ P.asIdeal)) a =
      Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) x) y hy
Tactic: classical
  rintro ⟨y, hy⟩
  obtain ⟨b, rfl⟩ : ∃ a, φ a = y := hf y
  obtain ⟨f, hf⟩ : ∃ f : Π₀ i : HeightOneSpectrum A, primaryComponent M₁ i.asIdeal,
      (DFinsupp.lsum ℕ fun i : HeightOneSpectrum A ↦
      (primaryComponent M₁ i.asIdeal).subtype) f = b := by
    simp only [← mem_iSup_iff_exists_dfinsupp, iSup_primaryComponent_eq_top hM₁, mem_top]
  refine ⟨f P, Subtype.ext ?_⟩
  simp only [map_apply_coe]
  rw [eq_comm, ← sub_eq_zero]
  refine (Submodule.disjoint_def.mp (iSupIndep_primaryComponent A M₂ P)) _ ?_ ?_
  · exact Submodule.sub_mem _ hy (primaryComponent_map_mem _ _ _)
  · have hdiff : φ b - φ ↑(f P) = ∑ Q ∈ f.support \ {P}, φ ↑(f Q) := by
      rw [sub_eq_iff_eq_add', ← Finset.sum_eq_add_sum_diff_singleton P (fun P ↦ φ (f P)) (by aesop)]
      simpa [DFinsupp.sumAddHom_apply, DFinsupp.sum] using congr(φ $hf).symm
    rw [hdiff]
    exact Submodule.sum_mem _ fun Q hQ ↦ Submodule.mem_iSup_of_mem Q <|
        Submodule.mem_iSup_of_mem (by grind) (primaryComponent_map_mem _ _ _)
-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst_2 : AddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₁
inst_5 : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf : Surjective.{u_5 + 1, u_6 + 1} (α := M₁) (β := M₂) (⇑φ : (a : M₁) → M₂)
rintro :
  ∀ (y : M₂) (hy : Membership.mem (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) y),
    ∃ (a : ↥(primaryComponent M₁ P.asIdeal)),
      (map P.asIdeal φ : (a : ↥(primaryComponent M₁ P.asIdeal)) → ↥(primaryComponent M₂ P.asIdeal)) a =
        Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) x) y hy
⊢ Surjective.{u_5 + 1, u_6 + 1} (α := ↥(primaryComponent M₁ P.asIdeal)) (β := ↥(primaryComponent M₂ P.asIdeal))
    (⇑(map P.asIdeal φ) : (a : ↥(primaryComponent M₁ P.asIdeal)) → ↥(primaryComponent M₂ P.asIdeal))
have rintro₁ : ∀ (b : M₁)
  (hy : Membership.mem (α := M₂) (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) ((φ : (a : M₁) → M₂) b : M₂)),
  ∃ (a : ↥(primaryComponent M₁ P.asIdeal)),
    Eq.{u_6 + 1} (α := ↥(primaryComponent M₂ P.asIdeal))
      ((map P.asIdeal φ : (a : ↥(primaryComponent M₁ P.asIdeal)) → ↥(primaryComponent M₂ P.asIdeal)) a :
        ↥(primaryComponent M₂ P.asIdeal))
      (Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) x)
          ((φ : (a : M₁) → M₂) b) hy :
        ↥(primaryComponent M₂ P.asIdeal))
Tactic: classical
  rintro ⟨y, hy⟩
  obtain ⟨b, rfl⟩ : ∃ a, φ a = y := hf y
  obtain ⟨f, hf⟩ : ∃ f : Π₀ i : HeightOneSpectrum A, primaryComponent M₁ i.asIdeal,
      (DFinsupp.lsum ℕ fun i : HeightOneSpectrum A ↦
      (primaryComponent M₁ i.asIdeal).subtype) f = b := by
    simp only [← mem_iSup_iff_exists_dfinsupp, iSup_primaryComponent_eq_top hM₁, mem_top]
  refine ⟨f P, Subtype.ext ?_⟩
  simp only [map_apply_coe]
  rw [eq_comm, ← sub_eq_zero]
  refine (Submodule.disjoint_def.mp (iSupIndep_primaryComponent A M₂ P)) _ ?_ ?_
  · exact Submodule.sub_mem _ hy (primaryComponent_map_mem _ _ _)
  · have hdiff : φ b - φ ↑(f P) = ∑ Q ∈ f.support \ {P}, φ ↑(f Q) := by
      rw [sub_eq_iff_eq_add', ← Finset.sum_eq_add_sum_diff_singleton P (fun P ↦ φ (f P)) (by aesop)]
      simpa [DFinsupp.sumAddHom_apply, DFinsupp.sum] using congr(φ $hf).symm
    rw [hdiff]
    exact Submodule.sum_mem _ fun Q hQ ↦ Submodule.mem_iSup_of_mem Q <|
        Submodule.mem_iSup_of_mem (by grind) (primaryComponent_map_mem _ _ _)
-- Lean 4 proof step from Mathlib.Algebra.Module.TransferInstance (goal)
Goal:
α : Type u_2
β : Type u_3
e : α ≃ β
R : Type u_4
inst : Zero R
inst_1 : Zero β
inst_2 : SMul R β
inst_3 : NoZeroSMulDivisors R β
this : Zero α := e.zero
this_1 : SMul R α := Equiv.smul R e
⊢ NoZeroSMulDivisors R α
have refine : ∀ {r : R} (m : α), r • m = 0 → r = 0 ∨ m = 0
Tactic: refine ⟨fun {r} m ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.TransferInstance (goal)
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
e_1 e : α ≃ β
inst_1 : AddCommMonoid β
inst_2 : Module R β
this : AddCommMonoid α := e.addCommMonoid
module : Module R α := Equiv.module R e
r : R
x : α
⊢ (AddEquiv.toEquiv e.addEquiv).toFun (r • x) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) ((AddEquiv.toEquiv e.addEquiv).toFun x)
have a : Eq.{u_2 + 1} (α := α) ((e.symm : (a : β) → α) ((AddEquiv.toEquiv e.addEquiv).toFun (r • x)) : α)
  ((e.symm : (a : β) → α)
      (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) ((AddEquiv.toEquiv e.addEquiv).toFun x)) :
    α)
Tactic: apply e.symm.injective
-- Lean 4 proof step from Mathlib.Algebra.Module.TransferInstance (goal)
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
e_1 e : α ≃ β
inst_1 : AddCommMonoid β
inst_2 : Module R β
this : AddCommMonoid α := e.addCommMonoid
module : Module R α := Equiv.module R e
r : R
x : α
⊢ Eq.{u_2 + 1} (α := α) ((e.symm : (a : β) → α) ((AddEquiv.toEquiv e.addEquiv).toFun (r • x)) : α)
    ((e.symm : (a : β) → α)
        (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) ((AddEquiv.toEquiv e.addEquiv).toFun x)) :
      α)
have a : (AddEquiv.toEquiv e.addEquiv : (a : α) → β) (r • x) =
  HSMul.hSMul (β := β) r ((AddEquiv.toEquiv e.addEquiv : (a : α) → β) x : β)
Tactic: simp only [toFun_as_coe, RingHom.id_apply, EmbeddingLike.apply_eq_iff_eq]
-- Lean 4 proof step from Mathlib.Algebra.Module.TransferInstance (goal)
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
A : Type u_4
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : AddCommMonoid α
inst_4 : AddCommMonoid β
inst_5 : Module A β
inst_6 : Module R α
inst_7 : Module R β
inst_8 : IsScalarTower R A β
e : α ≃ₗ[R] β
this : Module A α := AddEquiv.module A e.toAddEquiv
⊢ IsScalarTower R A α
have smul_assoc : ∀ (x : R) (y : A) (z : α), (x • y) • z = x • y • z
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.TransferInstance (goal)
Goal:
R : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring R
A : Type u_4
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : AddCommMonoid α
inst_4 : AddCommMonoid β
inst_5 : Module A β
inst_6 : Module R α
inst_7 : Module R β
inst_8 : IsScalarTower R A β
e : α ≃ₗ[R] β
this : Module A α := AddEquiv.module A e.toAddEquiv
x : R
y : A
z : α
⊢ (x • y) • z = x • y • z
have smul_assoc : ({ toFun := (↑e : α →ₗ[R] β).toFun, invFun := e.invFun, left_inv := sorry, right_inv := sorry : α ≃ β }.symm : (a : β) → α)
    (x •
      HSMul.hSMul (β := β) y
        (({ toFun := (↑e : α →ₗ[R] β).toFun, invFun := e.invFun, left_inv := sorry, right_inv := sorry : α ≃ β } : (a : α) → β)
            z :
          β)) =
  HSMul.hSMul (β := α) x
    (({ toFun := (↑e : α →ₗ[R] β).toFun, invFun := e.invFun, left_inv := sorry, right_inv := sorry : α ≃ β }.symm : (a : β) → α)
        (HSMul.hSMul (β := β) y
          (({ toFun := (↑e : α →ₗ[R] β).toFun, invFun := e.invFun, left_inv := sorry, right_inv := sorry : α ≃ β } :
                (a : α) → β)
              z :
            β)) :
      α)
Tactic: simp only [Equiv.smul_def, smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Module.ULift (goal)
Goal:
R : Type u
M : Type v
N : Type w
inst : SMul R M
inst_1 : SMul M N
inst_2 : SMul R N
inst_3 : IsScalarTower R M N
x : R
y : M
z : ULift.{u_1, w} N
⊢ { down := (x • y) • z.down : ULift.{u_1, w} N } = { down := x • y • z.down }
have rw : { down := x • y • z.down : ULift.{u_1, w} N } = { down := x • y • z.down }
Tactic: rw [smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Module.ULift (goal)
Goal:
R : Type u
M : Type v
N : Type w
inst : Zero M
inst_1 : SMulZeroClass R M
c : R
⊢ HSMul.hSMul (β := ULift.{u_1, v} M) c 0 = 0
have h : down.{u_1, v} (HSMul.hSMul (β := ULift.{u_1, v} M) c 0) = down.{u_1, v} 0
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.ULift (goal)
Goal:
R : Type u
M : Type v
N : Type w
inst : Zero M
inst_1 : SMulZeroClass R M
c : R
⊢ HSMul.hSMul (β := ULift.{u_1, v} M) c 0 = 0
have h : down.{u_1, v} (HSMul.hSMul (β := ULift.{u_1, v} M) c 0) = down.{u_1, v} 0
Tactic: { ext; simp [smul_zero] }
-- Lean 4 proof step from Mathlib.Algebra.Module.ULift (goal)
Goal:
R : Type u
M : Type v
N : Type w
inst : AddZeroClass M
inst_1 : DistribSMul R M
c : R
f g : ULift.{u_1, v} M
⊢ c • (f + g) = c • f + c • g
have h : down.{u_1, v} (c • (f + g)) = down.{u_1, v} (c • f + c • g)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.ULift (goal)
Goal:
R : Type u
M : Type v
N : Type w
inst : Monoid R
inst_1 : Monoid M
inst_2 : MulDistribMulAction R M
x : R
⊢ HSMul.hSMul (β := ULift.{u_1, v} M) x 1 = 1
have h : down.{u_1, v} (HSMul.hSMul (β := ULift.{u_1, v} M) x 1) = down.{u_1, v} 1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.ULift (goal)
Goal:
R : Type u
M : Type v
N : Type w
inst : Monoid R
inst_1 : Monoid M
inst_2 : MulDistribMulAction R M
x : R
x_1 x_2 : ULift.{u_1, v} M
⊢ x • (x_1 * x_2) = x • x_1 * x • x_2
have h : down.{u_1, v} (x • (x_1 * x_2)) = down.{u_1, v} (x • x_1 * x • x_2)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
F : Type u_4
inst_3 : AddCommGroup F
inst_4 : Module K F
f : E ≃ₗ[K] F
⊢ Eq (α := Submodule ℤ F)
    (Submodule.map (↑(LinearEquiv.restrictScalars ℤ f) : E →ₗ[ℤ] F)
      (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    (span ℤ (Set.range.{u_4, u_2 + 1} (ι := ι) (⇑(b.map f) : (a : ι) → F)))
have simp_rw : Eq.{u_4 + 1} (α := Submodule ℤ F)
  (span ℤ
    (Set.image.{u_1, u_4} (α := E) (⇑(↑(LinearEquiv.restrictScalars ℤ f) : E →ₗ[ℤ] F) : (a : E) → F)
      (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))))
  (span ℤ (Set.range.{u_4, u_2 + 1} (ι := ι) (⇑(b.map f) : (a : ι) → F)))
Tactic: simp_rw [Submodule.map_span, LinearEquiv.coe_coe, LinearEquiv.restrictScalars_apply,
    Basis.coe_map, Set.range_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
F : Type u_4
inst_3 : AddCommGroup F
inst_4 : Module K F
f : E ≃ₗ[K] F
simp_rw :
  Eq.{u_4 + 1} (α := Submodule ℤ F)
    (span ℤ
      (Set.image.{u_1, u_4} (α := E) (⇑(↑(LinearEquiv.restrictScalars ℤ f) : E →ₗ[ℤ] F) : (a : E) → F)
        (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    (span ℤ (Set.range.{u_4, u_2 + 1} (ι := ι) (⇑(b.map f) : (a : ι) → F)))
⊢ Eq (α := Submodule ℤ F)
    (Submodule.map (↑(LinearEquiv.restrictScalars ℤ f) : E →ₗ[ℤ] F)
      (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    (span ℤ (Set.range.{u_4, u_2 + 1} (ι := ι) (⇑(b.map f) : (a : ι) → F)))
have simp_rw₁ : Eq.{u_4 + 1} (α := Submodule ℤ F)
  (span ℤ
    ((fun (a : E) ↦ (LinearEquiv.restrictScalars ℤ f : (a : E) → F) a) ''
      Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
  (span ℤ (Set.range.{u_4, u_2 + 1} (ι := ι) (⇑(b.map f) : (a : ι) → F)))
Tactic: simp_rw [Submodule.map_span, LinearEquiv.coe_coe, LinearEquiv.restrictScalars_apply,
    Basis.coe_map, Set.range_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
F : Type u_4
inst_3 : AddCommGroup F
inst_4 : Module K F
f : E ≃ₗ[K] F
simp_rw :
  Eq.{u_4 + 1} (α := Submodule ℤ F)
    (span ℤ
      (Set.image.{u_1, u_4} (α := E) (⇑(↑(LinearEquiv.restrictScalars ℤ f) : E →ₗ[ℤ] F) : (a : E) → F)
        (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    (span ℤ (Set.range.{u_4, u_2 + 1} (ι := ι) (⇑(b.map f) : (a : ι) → F)))
simp_rw₁ :
  Eq.{u_4 + 1} (α := Submodule ℤ F)
    (span ℤ
      ((fun (a : E) ↦ (LinearEquiv.restrictScalars ℤ f : (a : E) → F) a) ''
        Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
    (span ℤ (Set.range.{u_4, u_2 + 1} (ι := ι) (⇑(b.map f) : (a : ι) → F)))
⊢ Eq (α := Submodule ℤ F)
    (Submodule.map (↑(LinearEquiv.restrictScalars ℤ f) : E →ₗ[ℤ] F)
      (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    (span ℤ (Set.range.{u_4, u_2 + 1} (ι := ι) (⇑(b.map f) : (a : ι) → F)))
have simp_rw₂ : Eq.{u_4 + 1} (α := Submodule ℤ F)
  (span ℤ ((fun (a : E) ↦ (f : (a : E) → F) a) '' Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
  (span ℤ (Set.range.{u_4, u_2 + 1} (ι := ι) (⇑(b.map f) : (a : ι) → F)))
Tactic: simp_rw [Submodule.map_span, LinearEquiv.coe_coe, LinearEquiv.restrictScalars_apply,
    Basis.coe_map, Set.range_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
F : Type u_4
inst_3 : AddCommGroup F
inst_4 : Module K F
f : E ≃ₗ[K] F
simp_rw :
  Eq.{u_4 + 1} (α := Submodule ℤ F)
    (span ℤ
      (Set.image.{u_1, u_4} (α := E) (⇑(↑(LinearEquiv.restrictScalars ℤ f) : E →ₗ[ℤ] F) : (a : E) → F)
        (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    (span ℤ (Set.range.{u_4, u_2 + 1} (ι := ι) (⇑(b.map f) : (a : ι) → F)))
simp_rw₁ :
  Eq.{u_4 + 1} (α := Submodule ℤ F)
    (span ℤ
      ((fun (a : E) ↦ (LinearEquiv.restrictScalars ℤ f : (a : E) → F) a) ''
        Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
    (span ℤ (Set.range.{u_4, u_2 + 1} (ι := ι) (⇑(b.map f) : (a : ι) → F)))
simp_rw₂ :
  Eq.{u_4 + 1} (α := Submodule ℤ F)
    (span ℤ ((fun (a : E) ↦ (f : (a : E) → F) a) '' Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
    (span ℤ (Set.range.{u_4, u_2 + 1} (ι := ι) (⇑(b.map f) : (a : ι) → F)))
⊢ Eq (α := Submodule ℤ F)
    (Submodule.map (↑(LinearEquiv.restrictScalars ℤ f) : E →ₗ[ℤ] F)
      (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    (span ℤ (Set.range.{u_4, u_2 + 1} (ι := ι) (⇑(b.map f) : (a : ι) → F)))
have simp_rw₃ : Eq.{u_4 + 1} (α := Submodule ℤ F)
  (span ℤ ((fun (a : E) ↦ (f : (a : E) → F) a) '' Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
  (span ℤ
    (Set.range.{u_4, u_2 + 1} (ι := ι)
      (Function.comp.{u_2 + 1, u_1 + 1, u_4 + 1} (β := E) (⇑f : (a : E) → F) (⇑b : (a : ι) → E))))
Tactic: simp_rw [Submodule.map_span, LinearEquiv.coe_coe, LinearEquiv.restrictScalars_apply,
    Basis.coe_map, Set.range_comp]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
c : K
hc : c ≠ 0
⊢ HSMul.hSMul (β := Submodule ℤ E) c (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) =
    span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑(b.isUnitSMul (w := fun (x : ι) ↦ c) ⋯) : (a : ι) → E))
have rw : Eq.{u_1 + 1} (α := Submodule ℤ E) (span ℤ (Set.range fun (i : ι) ↦ HSMul.hSMul (β := E) c ((b : (a : ι) → E) i : E)))
  (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑(b.isUnitSMul (w := fun (x : ι) ↦ c) sorry) : (a : ι) → E)))
Tactic: rw [smul_span, Set.smul_set_range]