awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
R' : Type u'
inst_2 : CommRing R'
inst_3 : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat.{v, u} R
N : ModuleCat.{v', u'} R'
e' : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑M : Type v) (↑N : Type v')
n : ℕ
inst_4 : HasProjectiveDimensionLE M n
zero :
  ∀ {M : ModuleCat.{v, u} R} {N : ModuleCat.{v', u'} R'}
    (e' : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑M : Type v) (↑N : Type v')) [HasProjectiveDimensionLE M 0],
    HasProjectiveDimensionLE N 0
⊢ HasProjectiveDimensionLE N n
have succ : ∀ (n : ℕ)
  (ih :
    ∀ {M : ModuleCat.{v, u} R} {N : ModuleCat.{v', u'} R'}
      (e' : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑M : Type v) (↑N : Type v')) [HasProjectiveDimensionLE M n],
      HasProjectiveDimensionLE N n)
  {M : ModuleCat.{v, u} R} {N : ModuleCat.{v', u'} R'}
  (e' : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑M : Type v) (↑N : Type v')) [HasProjectiveDimensionLE M (n + 1)],
  HasProjectiveDimensionLE N (n + 1)
Tactic: induction n generalizing M N e' with
  | zero =>
    have : HasProjectiveDimensionLE M 0 := ‹_›
    simp only [HasProjectiveDimensionLE, zero_add] at this ⊢
    rw [← projective_iff_hasProjectiveDimensionLT_one, ← IsProjective.iff_projective] at this ⊢
    exact Projective.of_equiv e'
  | succ n ih =>
    let S := M.projectiveShortComplex
    let S' := N.projectiveShortComplex
    have S_exact := M.shortExact_projectiveShortComplex
    have S'_exact := N.shortExact_projectiveShortComplex
    let eR : Shrink.{v} R ≃ₛₗ[RingHomClass.toRingHom e] Shrink.{v'} R' :=
      ((Shrink.linearEquiv R R).trans e.toSemilinearEquiv).trans (Shrink.linearEquiv R' R').symm
    let e2 : S.X₂ ≃ₛₗ[RingHomClass.toRingHom e] S'.X₂ :=
      (Finsupp.mapDomain.linearEquiv (Shrink R) R e').trans (Finsupp.mapRange.linearEquiv eR)
    have comm : S'.g.hom.comp e2.toLinearMap = e'.toLinearMap.comp S.g.hom := by
      ext m r
      simp [S, S', e2, eR, Basis.constr_apply, map_smulₛₗ]
    have : S.g.hom.ker = Submodule.comap e2.toLinearMap S'.g.hom.ker := by
      rw [← LinearMap.ker_comp, comm, LinearEquiv.ker_comp]
    rw [Submodule.comap_equiv_eq_map_symm] at this
    let eker : S.X₁ ≃ₛₗ[RingHomClass.toRingHom e] S'.X₁ :=
      (LinearEquiv.ofEq _ _ this).trans (e2.symm.submoduleMap S'.g.hom.ker).symm
    have := (S_exact.hasProjectiveDimensionLT_X₃_iff n inferInstance).mp ‹_›
    exact (S'_exact.hasProjectiveDimensionLT_X₃_iff n inferInstance).mpr (ih eker)
Cleared hypotheses: M, N, e', n, inst_4
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
R' : Type u'
inst_2 : CommRing R'
inst_3 : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat.{v, u} R
N : ModuleCat.{v', u'} R'
e' : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑M : Type v) (↑N : Type v')
⊢ projectiveDimension M = projectiveDimension N
have refine : ∀ (N_1 : WithBot ℕ∞), projectiveDimension M ≤ N_1 ↔ projectiveDimension N ≤ N_1
Tactic: refine eq_of_forall_ge_iff (fun N ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
R' : Type u'
inst_2 : CommRing R'
inst_3 : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat.{v, u} R
N : ModuleCat.{v', u'} R'
e' : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑M : Type v) (↑N : Type v')
n : ℕ
⊢ projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔ projectiveDimension N ≤ (↑n : WithBot ℕ∞)
have coe : HasProjectiveDimensionLE M n ↔ HasProjectiveDimensionLE N n
Tactic: simp only [projectiveDimension_le_iff]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
R' : Type u'
inst_2 : CommRing R'
inst_3 : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat.{v, u} R
N : ModuleCat.{v', u'} R'
e' : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑M : Type v) (↑N : Type v')
n : ℕ∞
⊢ projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔ projectiveDimension N ≤ (↑n : WithBot ℕ∞)
have coe : projectiveDimension M ≤ (↑⊤ : WithBot ℕ∞) ↔ projectiveDimension N ≤ (↑⊤ : WithBot ℕ∞)
Tactic: induction n with
    | top => simp
    | coe n =>
      norm_cast
      simp only [projectiveDimension_le_iff]
      exact ⟨fun h ↦ hasProjectiveDimensionLE_of_semiLinearEquiv e e' n,
        fun h ↦ hasProjectiveDimensionLE_of_semiLinearEquiv e.symm e'.symm n⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
R' : Type u'
inst_2 : CommRing R'
inst_3 : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat.{v, u} R
N : ModuleCat.{v', u'} R'
e' : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑M : Type v) (↑N : Type v')
n : ℕ∞
coe : projectiveDimension M ≤ (↑⊤ : WithBot ℕ∞) ↔ projectiveDimension N ≤ (↑⊤ : WithBot ℕ∞)
⊢ projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔ projectiveDimension N ≤ (↑n : WithBot ℕ∞)
have coe₁ : ∀ (n : ℕ), projectiveDimension M ≤ (↑(↑n : ℕ∞) : WithBot ℕ∞) ↔ projectiveDimension N ≤ (↑(↑n : ℕ∞) : WithBot ℕ∞)
Tactic: induction n with
    | top => simp
    | coe n =>
      norm_cast
      simp only [projectiveDimension_le_iff]
      exact ⟨fun h ↦ hasProjectiveDimensionLE_of_semiLinearEquiv e e' n,
        fun h ↦ hasProjectiveDimensionLE_of_semiLinearEquiv e.symm e'.symm n⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
R' : Type u'
inst_2 : CommRing R'
inst_3 : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat.{v, u} R
N_1 : ModuleCat.{v', u'} R'
e' : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑M : Type v) (↑N_1 : Type v')
N : WithBot ℕ∞
⊢ projectiveDimension M ≤ N ↔ projectiveDimension N_1 ≤ N
have bot : projectiveDimension M ≤ ⊥ ↔ projectiveDimension N_1 ≤ ⊥
Tactic: induction N with
  | bot => simpa [projectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton] using
      e'.subsingleton_congr
  | coe n =>
    induction n with
    | top => simp
    | coe n =>
      norm_cast
      simp only [projectiveDimension_le_iff]
      exact ⟨fun h ↦ hasProjectiveDimensionLE_of_semiLinearEquiv e e' n,
        fun h ↦ hasProjectiveDimensionLE_of_semiLinearEquiv e.symm e'.symm n⟩
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
R' : Type u'
inst_2 : CommRing R'
inst_3 : Small.{v', u'} R'
e : R ≃+* R'
M : ModuleCat.{v, u} R
N_1 : ModuleCat.{v', u'} R'
e' : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑M : Type v) (↑N_1 : Type v')
N : WithBot ℕ∞
bot : projectiveDimension M ≤ ⊥ ↔ projectiveDimension N_1 ≤ ⊥
⊢ projectiveDimension M ≤ N ↔ projectiveDimension N_1 ≤ N
have coe : ∀ (n : ℕ∞), projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔ projectiveDimension N_1 ≤ (↑n : WithBot ℕ∞)
Tactic: induction N with
  | bot => simpa [projectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton] using
      e'.subsingleton_congr
  | coe n =>
    induction n with
    | top => simp
    | coe n =>
      norm_cast
      simp only [projectiveDimension_le_iff]
      exact ⟨fun h ↦ hasProjectiveDimensionLE_of_semiLinearEquiv e e' n,
        fun h ↦ hasProjectiveDimensionLE_of_semiLinearEquiv e.symm e'.symm n⟩
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Semi (goal)
Goal:
R : Type u
inst : Semiring R
M N : SemimoduleCat.{v, u} R
f g : M.Hom N
h : f.hom = g.hom
⊢ f = g
have mk : ∀ (hom' : (↑M : Type v) →ₗ[R] (↑N : Type v)) (h : { hom' := hom' : M.Hom N }.hom = g.hom),
  { hom' := hom' : M.Hom N } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Semi (goal)
Goal:
R : Type u
inst : Semiring R
M N : SemimoduleCat.{v, u} R
g : M.Hom N
hom' : (↑M : Type v) →ₗ[R] (↑N : Type v)
h : { hom' := hom' : M.Hom N }.hom = g.hom
⊢ { hom' := hom' : M.Hom N } = g
have mk : ∀ (hom'_1 : (↑M : Type v) →ₗ[R] (↑N : Type v)) (h : { hom' := hom' : M.Hom N }.hom = { hom' := hom'_1 }.hom),
  { hom' := hom' : M.Hom N } = { hom' := hom'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Semi (goal)
Goal:
R : Type u
inst : Semiring R
M : SemimoduleCat.{u_1, u} R
inst_1 : Subsingleton.{u_1 + 1} (↑M : Type u_1)
X : SemimoduleCat.{u_1, u} R
f : M ⟶ X
⊢ f = default
have hf : ∀ (x : (↑M : Type u_1)),
  Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑M : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑M : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Semi (goal)
Goal:
R : Type u
inst : Semiring R
M : SemimoduleCat.{u_1, u} R
inst_1 : Subsingleton.{u_1 + 1} (↑M : Type u_1)
X : SemimoduleCat.{u_1, u} R
f : M ⟶ X
x : (↑M : Type u_1)
⊢ Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑M : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑M : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
have hf : Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑M : Type u_1)) → (↑X : Type u_1)) 0 : (↑X : Type u_1))
  ((Hom.hom default : (a : (↑M : Type u_1)) → (↑X : Type u_1)) 0 : (↑X : Type u_1))
Tactic: rw [Subsingleton.elim x (0 : M)]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Semi (goal)
Goal:
R : Type u
inst : Semiring R
M : SemimoduleCat.{u_1, u} R
inst_1 : Subsingleton.{u_1 + 1} (↑M : Type u_1)
X : SemimoduleCat.{u_1, u} R
f : X ⟶ M
⊢ f = default
have hf : ∀ (x : (↑X : Type u_1)),
  Eq (α := (↑M : Type u_1)) ((Hom.hom f : (a : (↑X : Type u_1)) → (↑M : Type u_1)) x : (↑M : Type u_1))
    ((Hom.hom default : (a : (↑X : Type u_1)) → (↑M : Type u_1)) x : (↑M : Type u_1))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Semi (goal)
Goal:
R : Type u
inst : Semiring R
X₁ X₂ : Type v
g₁ : AddCommMonoid X₁
g₂ : AddCommMonoid X₂
m₁ : Module R X₁
m₂ : Module R X₂
e : X₁ ≃ₗ[R] X₂
⊢ ↟(↑e : X₁ →ₗ[R] X₂) ≫ ↟(↑e.symm : X₂ →ₗ[R] X₁) = 𝟙 (of R X₁)
have hf : ∀ (x : (↑(of R X₁) : Type v)),
  Eq (α := (↑(of R X₁) : Type v))
    ((Hom.hom (↟(↑e : X₁ →ₗ[R] X₂) ≫ ↟(↑e.symm : X₂ →ₗ[R] X₁)) : (a : (↑(of R X₁) : Type v)) → (↑(of R X₁) : Type v))
        x :
      (↑(of R X₁) : Type v))
    ((Hom.hom (𝟙 (of R X₁)) : (a : (↑(of R X₁) : Type v)) → (↑(of R X₁) : Type v)) x : (↑(of R X₁) : Type v))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Semi (goal)
Goal:
R : Type u
inst : Semiring R
X₁ X₂ : Type v
g₁ : AddCommMonoid X₁
g₂ : AddCommMonoid X₂
m₁ : Module R X₁
m₂ : Module R X₂
e : X₁ ≃ₗ[R] X₂
⊢ ↟(↑e.symm : X₂ →ₗ[R] X₁) ≫ ↟(↑e : X₁ →ₗ[R] X₂) = 𝟙 (of R X₂)
have hf : ∀ (x : (↑(of R X₂) : Type v)),
  Eq (α := (↑(of R X₂) : Type v))
    ((Hom.hom (↟(↑e.symm : X₂ →ₗ[R] X₁) ≫ ↟(↑e : X₁ →ₗ[R] X₂)) : (a : (↑(of R X₂) : Type v)) → (↑(of R X₂) : Type v))
        x :
      (↑(of R X₂) : Type v))
    ((Hom.hom (𝟙 (of R X₂)) : (a : (↑(of R X₂) : Type v)) → (↑(of R X₂) : Type v)) x : (↑(of R X₂) : Type v))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Semi (goal)
Goal:
R : Type u
inst : Semiring R
M : SemimoduleCat.{v, u} R
h : IsZero M
⊢ Subsingleton.{v + 1} (↑M : Type v)
have refine : ∀ (x : (↑M : Type v)), x = 0
Tactic: refine subsingleton_of_forall_eq 0 (fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Semi (goal)
Goal:
R : Type u
inst : Semiring R
M : SemimoduleCat.{v, u} R
h : IsZero M
x : (↑M : Type v)
⊢ x = 0
have rw : Eq (α := (↑M : Type v)) ((Hom.hom (𝟙 M) : (a : (↑M : Type v)) → (↑M : Type v)) x : (↑M : Type v)) (0 : (↑M : Type v))
Tactic: rw [← LinearMap.id_apply (R := R) x, ← SemimoduleCat.hom_id]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Semi (goal)
Goal:
R : Type u
inst : Semiring R
X₁ X₂ : Type v
S₀ : Type u₀
inst_1 : CommSemiring S₀
S : Type u
inst_2 : Semiring S
inst_3 : Algebra S₀ S
M N : SemimoduleCat.{v, u} S
x : S₀
x_1 : S
x_2 : (↑M : Type v)
⊢ (x • x_1) • x_2 = x • x_1 • x_2
have rw : HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) x : S) (x_1 • x_2) = x • x_1 • x_2
Tactic: rw [Algebra.smul_def, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Semi (goal)
Goal:
R : Type u
inst : Semiring R
X₁ X₂ : Type v
S₀ : Type u₀
inst_1 : CommSemiring S₀
S : Type u
inst_2 : Semiring S
inst_3 : Algebra S₀ S
M N : SemimoduleCat.{v, u} S
s : S
s₀ : S₀
n : (↑M : Type v)
⊢ s • HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) n =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
have rw : HSMul.hSMul (β := S) s ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) • n =
  HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
Tactic: rw [← smul_assoc, smul_eq_mul, ← Algebra.commutes, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Semi (goal)
Goal:
R : Type u
inst : Semiring R
X₁ X₂ : Type v
S₀ : Type u₀
inst_1 : CommSemiring S₀
S : Type u
inst_2 : Semiring S
inst_3 : Algebra S₀ S
M N : SemimoduleCat.{v, u} S
s : S
s₀ : S₀
n : (↑M : Type v)
rw :
  HSMul.hSMul (β := S) s ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) • n =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
⊢ s • HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) n =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
have rw₁ : HMul.hMul (β := S) s ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) • n =
  HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
Tactic: rw [← smul_assoc, smul_eq_mul, ← Algebra.commutes, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Semi (goal)
Goal:
R : Type u
inst : Semiring R
X₁ X₂ : Type v
S₀ : Type u₀
inst_1 : CommSemiring S₀
S : Type u
inst_2 : Semiring S
inst_3 : Algebra S₀ S
M N : SemimoduleCat.{v, u} S
s : S
s₀ : S₀
n : (↑M : Type v)
rw :
  HSMul.hSMul (β := S) s ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) • n =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
rw₁ :
  HMul.hMul (β := S) s ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) • n =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
⊢ s • HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) n =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
have rw₂ : HMul.hMul (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) s • n =
  HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
Tactic: rw [← smul_assoc, smul_eq_mul, ← Algebra.commutes, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Semi (goal)
Goal:
R : Type u
inst : Semiring R
X₁ X₂ : Type v
S₀ : Type u₀
inst_1 : CommSemiring S₀
S : Type u
inst_2 : Semiring S
inst_3 : Algebra S₀ S
M N : SemimoduleCat.{v, u} S
s : S
s₀ : S₀
n : (↑M : Type v)
rw :
  HSMul.hSMul (β := S) s ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) • n =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
rw₁ :
  HMul.hMul (β := S) s ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) • n =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
rw₂ :
  HMul.hMul (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) s • n =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
⊢ s • HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) n =
    HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
have rw₃ : HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n) =
  HSMul.hSMul.{u, v, v} (α := S) ((algebraMap S₀ S : (a : S₀) → S) s₀ : S) (s • n)
Tactic: rw [← smul_assoc, smul_eq_mul, ← Algebra.commutes, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Semi (goal)
Goal:
R : Type u
inst : Semiring R
X₁ X₂ : Type v
A B : SemimoduleCat.{v, u} R
f : A ⟶ B
h :
  IsIso (X :=
    Functor.obj
      (forget₂ (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
        (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat.{v}) ↦
        (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommMonCat.carrier))
      A)
    (CategoryTheory.Functor.map
      (forget₂ (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
        (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat.{v}) ↦
        (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommMonCat.carrier))
      f)
⊢ IsIso (X :=
    Functor.obj
      (forget (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
        (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier))
      A)
    (CategoryTheory.Functor.map
      (forget (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
        (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier))
      f)
have change : IsIso (X :=
  Functor.obj
    (forget AddCommMonCat (FC := fun (x1 x2 : AddCommMonCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
      AddCommMonCat.carrier))
    (Functor.obj
      (forget₂ (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
        (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat.{v}) ↦
        (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommMonCat.carrier))
      A))
  (CategoryTheory.Functor.map
    (forget AddCommMonCat (FC := fun (x1 x2 : AddCommMonCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
      AddCommMonCat.carrier))
    (CategoryTheory.Functor.map
      (forget₂ (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
        (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat.{v}) ↦
        (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommMonCat.carrier))
      f))
Tactic: change IsIso ((forget _).map ((forget₂ _ AddCommMonCat).map f))
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Semi (hypothesis)
Goal:
R : Type u
inst : Semiring R
X₁ X₂ : Type v
A B : SemimoduleCat.{v, u} R
f : A ⟶ B
h :
  IsIso (X :=
    Functor.obj
      (forget₂ (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
        (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat.{v}) ↦
        (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommMonCat.carrier))
      A)
    (CategoryTheory.Functor.map
      (forget₂ (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦
        (↑x1 : Type v) →ₗ[R] (↑x2 : Type v)) (CC := carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat.{v}) ↦
        (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommMonCat.carrier))
      f)
⊢ IsIso f
have this : IsIso (X :=
  Functor.obj
    (forget (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
      (CC := carrier))
    A)
  (CategoryTheory.Functor.map
    (forget (SemimoduleCat.{v, u} R) (FC := fun (x1 x2 : SemimoduleCat.{v, u} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
      (CC := carrier))
    f)
Tactic: have : IsIso ((forget _).map f) := by
      change IsIso ((forget _).map ((forget₂ _ AddCommMonCat).map f))
      infer_instance
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings (goal)
Goal:
C : Type u'
inst : Category.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R R' : CategoryTheory.Functor.{v', u, u', u + 1} Cᵒᵖ RingCat
α : R ⟶ R'
M₁ M₂ : PresheafOfModules.{v, v', u', u} R'
hM₂ : Presheaf.IsSheaf J M₂.presheaf
inst_1 :
  Presheaf.IsLocallySurjective J (FA := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CA :=
    RingCat.carrier) α
g : (restrictScalars α).obj M₁ ⟶ (restrictScalars α).obj M₂
X : Cᵒᵖ
r' : (↑(R'.obj X) : Type u)
m : (↑(M₁.obj X) : Type v)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
          AddCommGrpCat.carrier) (((toPresheaf R).map g).app X) :
        (a : (↑(M₁.presheaf.obj X) : Type v)) → (↑(M₂.presheaf.obj X) : Type v))
      (r' • m) =
    HSMul.hSMul (β := (↑(M₂.presheaf.obj X) : Type v)) r'
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
              AddCommGrpCat.carrier) (((toPresheaf R).map g).app X) :
            (a : (↑(M₁.presheaf.obj X) : Type v)) → (↑(M₂.presheaf.obj X) : Type v))
          m :
        (↑(M₂.presheaf.obj X) : Type v))
have a : ∀ (Y : C) (f : Y ⟶ Opposite.unop X),
  (Presheaf.imageSieve (FA := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CA := RingCat.carrier) α
          r').arrows
      f →
    Eq (α := (↑(M₂.presheaf.obj (Opposite.op Y)) : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
              AddCommGrpCat.carrier) (M₂.presheaf.map f.op) :
            (a : (↑(M₂.presheaf.obj (Opposite.op (Opposite.unop X))) : Type v)) →
              (↑(M₂.presheaf.obj (Opposite.op Y)) : Type v))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                  AddCommGrpCat.carrier) (((toPresheaf R).map g).app X) :
                (a : (↑(M₁.presheaf.obj X) : Type v)) → (↑(M₂.presheaf.obj X) : Type v))
              (r' • m) :
            (↑(M₂.presheaf.obj X) : Type v)) :
        (↑(M₂.presheaf.obj (Opposite.op Y)) : Type v))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
              AddCommGrpCat.carrier) (M₂.presheaf.map f.op) :
            (a : (↑(M₂.presheaf.obj (Opposite.op (Opposite.unop X))) : Type v)) →
              (↑(M₂.presheaf.obj (Opposite.op Y)) : Type v))
          (HSMul.hSMul (β := (↑(M₂.presheaf.obj X) : Type v)) r'
            ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
                    AddCommGrpCat.carrier) (((toPresheaf R).map g).app X) :
                  (a : (↑(M₁.presheaf.obj X) : Type v)) → (↑(M₂.presheaf.obj X) : Type v))
                m :
              (↑(M₂.presheaf.obj X) : Type v))) :
        (↑(M₂.presheaf.obj (Opposite.op Y)) : Type v))
Tactic: apply hM₂.isSeparated _ _ (Presheaf.imageSieve_mem J α r')
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.Free (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_1 : HasWeakSheafify J AddCommGrpCat
inst_2 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_3 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
M : SheafOfModules R
I : Type u
f : I → M.sections
⊢ (fun (f : free I ⟶ M) (i : I) ↦ ((M.unitHomEquiv : (a : unit R ⟶ M) → M.sections) (ιFree i ≫ f) : M.sections))
      ((fun (s : I → M.sections) ↦
          (Cofan.IsColimit.desc (isColimitFreeCofan I) fun (i : I) ↦
              (Equiv.symm M.unitHomEquiv : (a : M.sections) → unit R ⟶ M) (s i) :
            Cocone.pt (F := Discrete.functor fun (x : I) ↦ unit R) (freeCofan I) ⟶ M))
        f) =
    f
have h : ∀ (i : I),
  (fun (f : free I ⟶ M) (i : I) ↦ ((M.unitHomEquiv : (a : unit R ⟶ M) → M.sections) (ιFree i ≫ f) : M.sections))
      ((fun (s : I → M.sections) ↦
          (Cofan.IsColimit.desc (isColimitFreeCofan I) fun (i : I) ↦
              (Equiv.symm M.unitHomEquiv : (a : M.sections) → unit R ⟶ M) (s i) :
            Cocone.pt (F := Discrete.functor fun (x : I) ↦ unit R) (freeCofan I) ⟶ M))
        f)
      i =
    f i
Tactic: ext1 i