awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : Module.Finite R M
inst_7 : Module.FinitePresentation R M'
this : IsLocalizedModule.{u_3, u_1, u_1} (M := M') S LinearMap.id
r : R
hrp : r ∈ S
H :
  ∀ (t : R),
    r ∣ t →
      Function.Bijective (α := LocalizedModule (Submonoid.powers t) M) (β := LocalizedModule (Submonoid.powers t) M')
        (⇑((LocalizedModule.map (Submonoid.powers t) :
                  (a : M →ₗ[R] M') →
                    LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                      LocalizedModule (Submonoid.powers t) M')
                f :
              LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
                (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) M')) :
          (a : LocalizedModule (Submonoid.powers t) M) → LocalizedModule (Submonoid.powers t) M')
hrp' : Submonoid.powers r ≤ S
refine_1 : ∀ (y : M'), ∃ (x : Prod.{u_4, u_3} M ↥(Submonoid.powers r)), x.2 • y = (f : (a : M) → M') x.1
⊢ ∃ r ∈ S, IsLocalizedModule.Away r f
have refine_2 : ∀ {x₁ x₂ : M},
  Eq.{u_1 + 1} (α := M') ((f : (a : M) → M') x₁ : M') ((f : (a : M) → M') x₂ : M') →
    ∃ (c : ↥(Submonoid.powers r)), c • x₁ = c • x₂
Tactic: refine ⟨r, hrp, ⟨fun x ↦ IsLocalizedModule.map_units f ⟨x, hrp' x.2⟩, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : Module.Finite R M
inst_7 : Module.FinitePresentation R M'
this : IsLocalizedModule.{u_3, u_1, u_1} (M := M') S LinearMap.id
r : R
hrp : r ∈ S
H :
  ∀ (t : R),
    r ∣ t →
      Function.Bijective (α := LocalizedModule (Submonoid.powers t) M) (β := LocalizedModule (Submonoid.powers t) M')
        (⇑((LocalizedModule.map (Submonoid.powers t) :
                  (a : M →ₗ[R] M') →
                    LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                      LocalizedModule (Submonoid.powers t) M')
                f :
              LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
                (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) M')) :
          (a : LocalizedModule (Submonoid.powers t) M) → LocalizedModule (Submonoid.powers t) M')
hrp' : Submonoid.powers r ≤ S
y : M'
⊢ ∃ (x : Prod.{u_4, u_3} M ↥(Submonoid.powers r)), x.2 • y = (f : (a : M) → M') x.1
have refine_1 : ∀ (x : LocalizedModule (Submonoid.powers r) M)
  (hx :
    Eq (α := LocalizedModule (Submonoid.powers r) M')
      ((((LocalizedModule.map (Submonoid.powers r) :
                  (a : M →ₗ[R] M') →
                    LocalizedModule (Submonoid.powers r) M →ₗ[Localization (Submonoid.powers r)]
                      LocalizedModule (Submonoid.powers r) M')
                f :
              LinearMap (R := Localization (Submonoid.powers r)) (RingHom.id (Localization (Submonoid.powers r)))
                (LocalizedModule (Submonoid.powers r) M) (LocalizedModule (Submonoid.powers r) M')) :
            (a : LocalizedModule (Submonoid.powers r) M) → LocalizedModule (Submonoid.powers r) M')
          x :
        LocalizedModule (Submonoid.powers r) M')
      ((LocalizedModule.mkLinearMap (Submonoid.powers r) M' : (a : M') → LocalizedModule (Submonoid.powers r) M') y :
        LocalizedModule (Submonoid.powers r) M')),
  ∃ (x : Prod.{u_4, u_3} M ↥(Submonoid.powers r)), x.2 • y = (f : (a : M) → M') x.1
Tactic: obtain ⟨x, hx⟩ := (H _ dvd_rfl).2 (LocalizedModule.mkLinearMap _ _ y)
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submonoid R
M' : Type u_1
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M →ₗ[R] M'
inst_5 : IsLocalizedModule S f
inst_6 : Module.Finite R M
inst_7 : Module.FinitePresentation R M'
this : IsLocalizedModule.{u_3, u_1, u_1} (M := M') S LinearMap.id
r : R
hrp : r ∈ S
H :
  ∀ (t : R),
    r ∣ t →
      Function.Bijective (α := LocalizedModule (Submonoid.powers t) M) (β := LocalizedModule (Submonoid.powers t) M')
        (⇑((LocalizedModule.map (Submonoid.powers t) :
                  (a : M →ₗ[R] M') →
                    LocalizedModule (Submonoid.powers t) M →ₗ[Localization (Submonoid.powers t)]
                      LocalizedModule (Submonoid.powers t) M')
                f :
              LinearMap (R := Localization (Submonoid.powers t)) (RingHom.id (Localization (Submonoid.powers t)))
                (LocalizedModule (Submonoid.powers t) M) (LocalizedModule (Submonoid.powers t) M')) :
          (a : LocalizedModule (Submonoid.powers t) M) → LocalizedModule (Submonoid.powers t) M')
hrp' : Submonoid.powers r ≤ S
y : M'
x : M
n : ℕ
hx :
  Eq (α := LocalizedModule (Submonoid.powers r) M')
    ((((LocalizedModule.map (Submonoid.powers r) :
                (a : M →ₗ[R] M') →
                  LocalizedModule (Submonoid.powers r) M →ₗ[Localization (Submonoid.powers r)]
                    LocalizedModule (Submonoid.powers r) M')
              f :
            LinearMap (R := Localization (Submonoid.powers r)) (RingHom.id (Localization (Submonoid.powers r)))
              (LocalizedModule (Submonoid.powers r) M) (LocalizedModule (Submonoid.powers r) M')) :
          (a : LocalizedModule (Submonoid.powers r) M) → LocalizedModule (Submonoid.powers r) M')
        (Function.uncurry (mk' (LocalizedModule.mkLinearMap (Submonoid.powers r) M))
          (x,
            Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r) x)
              ((fun (x : ℕ) ↦ r ^ x) n) ⋯)) :
      LocalizedModule (Submonoid.powers r) M')
    ((LocalizedModule.mkLinearMap (Submonoid.powers r) M' : (a : M') → LocalizedModule (Submonoid.powers r) M') y :
      LocalizedModule (Submonoid.powers r) M')
⊢ ∃ (x : Prod.{u_4, u_3} M ↥(Submonoid.powers r)), x.2 • y = (f : (a : M) → M') x.1
have refine_1 : ∀ (m : ℕ) (hm : r ^ (m + n) • y = (f : (a : M) → M') (r ^ m • x)),
  ∃ (x : Prod.{u_4, u_3} M ↥(Submonoid.powers r)), x.2 • y = (f : (a : M) → M') x.1
Tactic: obtain ⟨m, hm⟩ : ∃ m, r ^ (m + n) • y = f (r ^ m • x) := by
      simpa [LocalizedModule.map, IsLocalizedModule.mk_eq_mk', -IsLocalizedModule.mk'_one,
        pow_add, mul_smul, IsLocalizedModule.mk'_eq_mk'_iff, Submonoid.mem_powers_iff,
        Submonoid.smul_def] using hx
-- Lean 4 proof step from Mathlib.Algebra.Module.GradedModule (goal)
Goal:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst : AddMonoid ιA
inst_1 : VAdd ιA ιB
inst_2 : (i : ιA) → AddCommMonoid (A i)
inst_3 : (i : ιB) → AddCommMonoid (M i)
inst_4 : DecidableEq ιA
inst_5 : DecidableEq ιB
inst_6 : GMonoid A
inst_7 : Gmodule A M
x : ⨁ (i : ιB), M i
⊢ HSMul.hSMul (α := ⨁ (i : ιA), A i) 1 x = x
have suffices : Eq (α := (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
  ((smulAddMonoidHom A M : (a : ⨁ (i : ιA), A i) → (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) 1)
  (AddMonoidHom.id (⨁ (i : ιB), M i))
Tactic: suffices smulAddMonoidHom A M 1 = AddMonoidHom.id (⨁ i, M i) from DFunLike.congr_fun this x
-- Lean 4 proof step from Mathlib.Algebra.Module.GradedModule (goal)
Goal:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst : AddMonoid ιA
inst_1 : VAdd ιA ιB
inst_2 : (i : ιA) → AddCommMonoid (A i)
inst_3 : (i : ιB) → AddCommMonoid (M i)
inst_4 : DecidableEq ιA
inst_5 : DecidableEq ιB
inst_6 : GMonoid A
inst_7 : Gmodule A M
x : ⨁ (i : ιB), M i
⊢ Eq (α := (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
    ((smulAddMonoidHom A M : (a : ⨁ (i : ιA), A i) → (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) 1)
    (AddMonoidHom.id (⨁ (i : ιB), M i))
have H : ∀ (i : ιB) (y : M i),
  Eq (α := ⨁ (i : ιB), M i)
    (((smulAddMonoidHom A M : (a : ⨁ (i : ιA), A i) → (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) 1 :
          (a : ⨁ (i : ιB), M i) → ⨁ (i : ιB), M i)
        ((of M i : (a : M i) → ⨁ (i : ιB), M i) y) :
      ⨁ (i : ιB), M i)
    ((AddMonoidHom.id (⨁ (i : ιB), M i) : (a : ⨁ (i : ιB), M i) → ⨁ (i : ιB), M i)
        ((of M i : (a : M i) → ⨁ (i : ιB), M i) y) :
      ⨁ (i : ιB), M i)
Tactic: apply DirectSum.addHom_ext
-- Lean 4 proof step from Mathlib.Algebra.Module.GradedModule (goal)
Goal:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst : AddMonoid ιA
inst_1 : VAdd ιA ιB
inst_2 : (i : ιA) → AddCommMonoid (A i)
inst_3 : (i : ιB) → AddCommMonoid (M i)
inst_4 : DecidableEq ιA
inst_5 : DecidableEq ιB
inst_6 : GMonoid A
inst_7 : Gmodule A M
x : ⨁ (i : ιB), M i
i : ιB
xi : M i
⊢ Eq (α := ⨁ (i : ιB), M i)
    (((smulAddMonoidHom A M : (a : ⨁ (i : ιA), A i) → (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) 1 :
          (a : ⨁ (i : ιB), M i) → ⨁ (i : ιB), M i)
        ((of M i : (a : M i) → ⨁ (i : ιB), M i) xi) :
      ⨁ (i : ιB), M i)
    ((AddMonoidHom.id (⨁ (i : ιB), M i) : (a : ⨁ (i : ιB), M i) → ⨁ (i : ιB), M i)
        ((of M i : (a : M i) → ⨁ (i : ιB), M i) xi) :
      ⨁ (i : ιB), M i)
have H : Eq (α := ⨁ (i : ιB), M i)
  ((((smulAddMonoidHom A M : (a : ⨁ (i : ιA), A i) → (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
            ((of A 0 : (a : A 0) → ⨁ (i : ιA), A i) (GOne.one (A := A))) :
          (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) :
        (a : ⨁ (i : ιB), M i) → ⨁ (i : ιB), M i)
      ((of M i : (a : M i) → ⨁ (i : ιB), M i) xi) :
    ⨁ (i : ιB), M i)
  ((AddMonoidHom.id (⨁ (i : ιB), M i) : (a : ⨁ (i : ιB), M i) → ⨁ (i : ιB), M i)
      ((of M i : (a : M i) → ⨁ (i : ιB), M i) xi) :
    ⨁ (i : ιB), M i)
Tactic: rw [show (1 : DirectSum ιA fun i => A i) = (of A 0) GOne.one by rfl]
-- Lean 4 proof step from Mathlib.Algebra.Module.GradedModule (goal)
Goal:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst : AddMonoid ιA
inst_1 : VAdd ιA ιB
inst_2 : (i : ιA) → AddCommMonoid (A i)
inst_3 : (i : ιB) → AddCommMonoid (M i)
inst_4 : DecidableEq ιA
inst_5 : DecidableEq ιB
inst_6 : GMonoid A
inst_7 : Gmodule A M
x : ⨁ (i : ιB), M i
i : ιB
xi : M i
⊢ Eq (α := ⨁ (i : ιB), M i)
    ((((smulAddMonoidHom A M : (a : ⨁ (i : ιA), A i) → (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
              ((of A 0 : (a : A 0) → ⨁ (i : ιA), A i) (GOne.one (A := A))) :
            (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) :
          (a : ⨁ (i : ιB), M i) → ⨁ (i : ιB), M i)
        ((of M i : (a : M i) → ⨁ (i : ιB), M i) xi) :
      ⨁ (i : ιB), M i)
    ((AddMonoidHom.id (⨁ (i : ιB), M i) : (a : ⨁ (i : ιB), M i) → ⨁ (i : ιB), M i)
        ((of M i : (a : M i) → ⨁ (i : ιB), M i) xi) :
      ⨁ (i : ιB), M i)
have H : Eq (α := ⨁ (i : ιB), M i)
  ((of M (HVAdd.hVAdd.{u_1, u_2, u_2} (α := ιA) 0 i) : (a : M (0 +ᵥ i)) → ⨁ (i : ιB), M i)
      (GSMul.smul (A := A) (M := M) (GOne.one (A := A)) xi) :
    ⨁ (i : ιB), M i)
  ((AddMonoidHom.id (⨁ (i : ιB), M i) : (a : ⨁ (i : ιB), M i) → ⨁ (i : ιB), M i)
      ((of M i : (a : M i) → ⨁ (i : ιB), M i) xi) :
    ⨁ (i : ιB), M i)
Tactic: rw [smulAddMonoidHom_apply_of_of]
-- Lean 4 proof step from Mathlib.Algebra.Module.GradedModule (goal)
Goal:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst : AddMonoid ιA
inst_1 : VAdd ιA ιB
inst_2 : (i : ιA) → AddCommMonoid (A i)
inst_3 : (i : ιB) → AddCommMonoid (M i)
inst_4 : DecidableEq ιA
inst_5 : DecidableEq ιB
inst_6 : GSemiring A
inst_7 : Gmodule A M
a b : ⨁ (i : ιA), A i
c : ⨁ (i : ιB), M i
⊢ (a * b) • c = a • b • c
have a₁ : Eq (α := (⨁ (i : ιA), A i) →+ (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
  (comp
    ((compHom :
        (a : (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) →
          ((⨁ (i : ιA), A i) →+ ⨁ (i : ιA), A i) →+ (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
      (smulAddMonoidHom A M))
    (mulHom A))
  (AddMonoidHom.flip
    ((((compHom :
              (a :
                  ((⨁ (i : ιB), M i) →+ (⨁ (i : ιA), A i) →+ ⨁ (i : ιB), M i) →+
                    (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) →
                ((⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ (⨁ (i : ιA), A i) →+ ⨁ (i : ιB), M i) →+
                  (⨁ (i : ιA), A i) →+ (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
            flipHom :
          ((⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ (⨁ (i : ιA), A i) →+ ⨁ (i : ιB), M i) →+
            (⨁ (i : ιA), A i) →+ (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) :
        (a : (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ (⨁ (i : ιA), A i) →+ ⨁ (i : ιB), M i) →
          (⨁ (i : ιA), A i) →+ (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
      (comp (N := (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
        ((compHom :
            (a : (⨁ (i : ιB), M i) →+ (⨁ (i : ιA), A i) →+ ⨁ (i : ιB), M i) →
              ((⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) →+ (⨁ (i : ιB), M i) →+ (⨁ (i : ιA), A i) →+ ⨁ (i : ιB), M i)
          (AddMonoidHom.flip (smulAddMonoidHom A M)))
        (smulAddMonoidHom A M))))
Tactic: suffices
    (-- `fun a b c ↦ (a * b) • c` as a bundled hom
              smulAddMonoidHom
              A M).compHom.comp
        (DirectSum.mulHom A) =
      (AddMonoidHom.compHom AddMonoidHom.flipHom <|
          (smulAddMonoidHom A M).flip.compHom.comp <| smulAddMonoidHom A M).flip
    from -- `fun a b c ↦ a • (b • c)` as a bundled hom
      DFunLike.congr_fun (DFunLike.congr_fun (DFunLike.congr_fun this a) b) c
-- Lean 4 proof step from Mathlib.Algebra.Module.GradedModule (goal)
Goal:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst : AddMonoid ιA
inst_1 : VAdd ιA ιB
inst_2 : (i : ιA) → AddCommMonoid (A i)
inst_3 : (i : ιB) → AddCommMonoid (M i)
inst_4 : DecidableEq ιA
inst_5 : DecidableEq ιB
inst_6 : GSemiring A
inst_7 : Gmodule A M
a b : ⨁ (i : ιA), A i
c : ⨁ (i : ιB), M i
ai : ιA
ax : A ai
bi : ιA
bx : A bi
ci : ιB
cx : M ci
⊢ Eq (α := ⨁ (i : ιB), M i)
    ((((smulAddMonoidHom A M : (a : ⨁ (i : ιA), A i) → (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
              ((((mulHom A : (a : ⨁ (i : ιA), A i) → (⨁ (i : ιA), A i) →+ ⨁ (i : ιA), A i)
                      ((of A ai : (a : A ai) → ⨁ (i : ιA), A i) ax) :
                    (⨁ (i : ιA), A i) →+ ⨁ (i : ιA), A i) :
                  (a : ⨁ (i : ιA), A i) → ⨁ (i : ιA), A i)
                ((of A bi : (a : A bi) → ⨁ (i : ιA), A i) bx)) :
            (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) :
          (a : ⨁ (i : ιB), M i) → ⨁ (i : ιB), M i)
        ((of M ci : (a : M ci) → ⨁ (i : ιB), M i) cx) :
      ⨁ (i : ιB), M i)
    ((((smulAddMonoidHom A M : (a : ⨁ (i : ιA), A i) → (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
              ((of A ai : (a : A ai) → ⨁ (i : ιA), A i) ax) :
            (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) :
          (a : ⨁ (i : ιB), M i) → ⨁ (i : ιB), M i)
        ((((smulAddMonoidHom A M : (a : ⨁ (i : ιA), A i) → (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
                ((of A bi : (a : A bi) → ⨁ (i : ιA), A i) bx) :
              (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) :
            (a : ⨁ (i : ιB), M i) → ⨁ (i : ιB), M i)
          ((of M ci : (a : M ci) → ⨁ (i : ιB), M i) cx)) :
      ⨁ (i : ιB), M i)
have H : Eq (α := ⨁ (i : ιB), M i)
  ((of M ((ai + bi) +ᵥ ci) : (a : M ((ai + bi) +ᵥ ci)) → ⨁ (i : ιB), M i)
      (GSMul.smul (A := A) (M := M) (GMul.mul (A := A) ax bx) cx) :
    ⨁ (i : ιB), M i)
  ((of M (ai +ᵥ bi +ᵥ ci) : (a : M (ai +ᵥ bi +ᵥ ci)) → ⨁ (i : ιB), M i)
      (GSMul.smul (A := A) (M := M) ax (GSMul.smul (A := A) (M := M) bx cx)) :
    ⨁ (i : ιB), M i)
Tactic: rw [smulAddMonoidHom_apply_of_of, smulAddMonoidHom_apply_of_of, DirectSum.mulHom_of_of,
    smulAddMonoidHom_apply_of_of]
-- Lean 4 proof step from Mathlib.Algebra.Module.GradedModule (goal)
Goal:
ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst : AddMonoid ιA
inst_1 : AddAction ιA ιM
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
𝓐 : ιA → σ'
inst_5 : SetLike σ' A
𝓜 : ιM → σ
inst_6 : AddCommMonoid M
inst_7 : Module A M
inst_8 : SetLike σ M
inst_9 : AddSubmonoidClass σ' A
inst_10 : AddSubmonoidClass σ M
inst_11 : SetLike.GradedMonoid 𝓐
inst_12 : SetLike.GradedSMul 𝓐 𝓜
inst_13 : DecidableEq ιA
inst_14 : DecidableEq ιM
inst_15 : GradedRing 𝓐
inst_16 : Decomposition 𝓜
h : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
⊢ M ≃ₗ[A] ⨁ (i : ιM), ↥(𝓜 i)
have refine : ∀ (m : A) (x : M),
  AddHom.toFun (AddEquiv.toAddHom (decomposeAddEquiv 𝓜)) (m • x) =
    HSMul.hSMul (α := A) (β := ⨁ (i : ιM), ↥(𝓜 i)) ((RingHom.id A : (a : A) → A) m : A)
      (AddHom.toFun (AddEquiv.toAddHom (decomposeAddEquiv 𝓜)) x)
Tactic: refine ⟨⟨(DirectSum.decomposeAddEquiv 𝓜).toAddHom, ?_⟩,
    (DirectSum.decomposeAddEquiv 𝓜).symm.toFun, (DirectSum.decomposeAddEquiv 𝓜).left_inv,
    (DirectSum.decomposeAddEquiv 𝓜).right_inv⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.GradedModule (goal)
Goal:
ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst : AddMonoid ιA
inst_1 : AddAction ιA ιM
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
𝓐 : ιA → σ'
inst_5 : SetLike σ' A
𝓜 : ιM → σ
inst_6 : AddCommMonoid M
inst_7 : Module A M
inst_8 : SetLike σ M
inst_9 : AddSubmonoidClass σ' A
inst_10 : AddSubmonoidClass σ M
inst_11 : SetLike.GradedMonoid 𝓐
inst_12 : SetLike.GradedSMul 𝓐 𝓜
inst_13 : DecidableEq ιA
inst_14 : DecidableEq ιM
inst_15 : GradedRing 𝓐
inst_16 : Decomposition 𝓜
h : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
x : A
y : M
⊢ AddHom.toFun (AddEquiv.toAddHom (decomposeAddEquiv 𝓜)) (x • y) =
    HSMul.hSMul (α := A) (β := ⨁ (i : ιM), ↥(𝓜 i)) ((RingHom.id A : (a : A) → A) x : A)
      (AddHom.toFun (AddEquiv.toAddHom (decomposeAddEquiv 𝓜)) y)
have rw : Eq (α := ⨁ (i : ιM), ↥(𝓜 i))
  (∑ x_1 ∈ DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x),
    (decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
      ((↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) x_1) : A) • y))
  (∑ i ∈ DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x),
    HSMul.hSMul (α := A) (β := ⨁ (i : ιM), ↥(𝓜 i))
      ((RingHom.id A : (a : A) → A)
          (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) :
        A)
      ((decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)))
Tactic: rw [AddHom.toFun_eq_coe, ← DirectSum.sum_support_decompose 𝓐 x, map_sum, Finset.sum_smul,
    AddEquiv.coe_toAddHom, map_sum, Finset.sum_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.GradedModule (goal)
Goal:
ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst : AddMonoid ιA
inst_1 : AddAction ιA ιM
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
𝓐 : ιA → σ'
inst_5 : SetLike σ' A
𝓜 : ιM → σ
inst_6 : AddCommMonoid M
inst_7 : Module A M
inst_8 : SetLike σ M
inst_9 : AddSubmonoidClass σ' A
inst_10 : AddSubmonoidClass σ M
inst_11 : SetLike.GradedMonoid 𝓐
inst_12 : SetLike.GradedSMul 𝓐 𝓜
inst_13 : DecidableEq ιA
inst_14 : DecidableEq ιM
inst_15 : GradedRing 𝓐
inst_16 : Decomposition 𝓜
h : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
x : A
y : M
⊢ Eq (α := ⨁ (i : ιM), ↥(𝓜 i))
    (∑ x_1 ∈ DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x),
      (decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
        ((↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) x_1) : A) • y))
    (∑ i ∈ DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x),
      HSMul.hSMul (α := A) (β := ⨁ (i : ιM), ↥(𝓜 i))
        ((RingHom.id A : (a : A) → A)
            (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) :
          A)
        ((decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)))
have refine : ∀ (i : ιA)
  (_hi :
    Membership.mem (γ := Finset ιA)
      (DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x)) i),
  (decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
      ((↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) • y) =
    HSMul.hSMul (α := A) (β := ⨁ (i : ιM), ↥(𝓜 i))
      ((RingHom.id A : (a : A) → A)
          (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) :
        A)
      ((decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i))
Tactic: refine Finset.sum_congr rfl (fun i _hi => ?_)
-- Lean 4 proof step from Mathlib.Algebra.Module.GradedModule (goal)
Goal:
ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst : AddMonoid ιA
inst_1 : AddAction ιA ιM
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
𝓐 : ιA → σ'
inst_5 : SetLike σ' A
𝓜 : ιM → σ
inst_6 : AddCommMonoid M
inst_7 : Module A M
inst_8 : SetLike σ M
inst_9 : AddSubmonoidClass σ' A
inst_10 : AddSubmonoidClass σ M
inst_11 : SetLike.GradedMonoid 𝓐
inst_12 : SetLike.GradedSMul 𝓐 𝓜
inst_13 : DecidableEq ιA
inst_14 : DecidableEq ιM
inst_15 : GradedRing 𝓐
inst_16 : Decomposition 𝓜
h : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
x : A
y : M
i : ιA
_hi :
  Membership.mem (γ := Finset ιA)
    (DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x)) i
⊢ (decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
      ((↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) • y) =
    HSMul.hSMul (α := A) (β := ⨁ (i : ιM), ↥(𝓜 i))
      ((RingHom.id A : (a : A) → A)
          (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) :
        A)
      ((decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i))
have rw : Eq (α := ⨁ (i : ιM), ↥(𝓜 i))
  (∑ x_1 ∈ DFinsupp.support (β := fun (i : ιM) ↦ ↥(𝓜 i)) ((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y),
    (decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
      ((↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) •
        (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) x_1) : M)))
  (∑ x_1 ∈ DFinsupp.support (β := fun (i : ιM) ↦ ↥(𝓜 i)) ((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y),
    HSMul.hSMul (β := ⨁ (i : ιM), ↥(𝓜 i))
      (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A)
      ((decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
          (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) x_1) : M) :
        ⨁ (i : ιM), ↥(𝓜 i)))
Tactic: rw [RingHom.id_apply, ← DirectSum.sum_support_decompose 𝓜 y, map_sum, Finset.smul_sum, map_sum,
    Finset.smul_sum]