awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Projective (goal)
Goal:
R : Type u
inst : Ring R
P : ModuleCat.{v, u} R
inst_1 : Small.{v, u} R
inst_2 : CategoryTheory.Projective P
⊢ Module.Projective.{u, v} R (↑P : Type v)
have refine : ∀ {M N : Type v} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
  (f : M →ₗ[R] N) (g : (↑P : Type v) →ₗ[R] N),
  Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N) → ∃ (h : (↑P : Type v) →ₗ[R] M), f ∘ₗ h = g
Tactic: refine Module.Projective.of_lifting_property ?_
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Projective (hypothesis)
Goal:
R : Type u
inst : Ring R
P : ModuleCat.{v, u} R
inst_1 : Small.{v, u} R
inst_2 : CategoryTheory.Projective P
M N : Type v
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
f : M →ₗ[R] N
g : (↑P : Type v) →ₗ[R] N
s : Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N)
⊢ ∃ (h : (↑P : Type v) →ₗ[R] M), f ∘ₗ h = g
have this : Epi (↟f)
Tactic: have : Epi (↟f) := (ModuleCat.epi_iff_surjective (↟f)).mpr s
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Projective (goal)
Goal:
R : Type u
inst : Ring R
P M_1 : ModuleCat.{v, u} R
inst_1 : Small.{v, u} R
M : ModuleCat.{v, u} R
e : Basis.{v, u, v} (↑M : Type v) R ((↑M : Type v) →₀ Shrink.{v, u} R) :=
  { repr := Finsupp.mapRange.linearEquiv (Shrink.linearEquiv R R) }
⊢ Epi (C := ModuleCat.{v, u} R) (X := of R ((↑M : Type v) →₀ Shrink.{v, u} R)) (Y := M)
    (↟((e.constr ℕ : (a : (↑M : Type v) → (↑M : Type v)) → ((↑M : Type v) →₀ Shrink.{v, u} R) →ₗ[R] (↑M : Type v)) id))
have rw : Function.Surjective.{v + 1, v + 1} (α := (↑(of R ((↑M : Type v) →₀ Shrink.{v, u} R)) : Type v)) (β := (↑M : Type v))
  (⇑(Hom.hom
        (↟((e.constr ℕ : (a : (↑M : Type v) → (↑M : Type v)) → ((↑M : Type v) →₀ Shrink.{v, u} R) →ₗ[R] (↑M : Type v))
            id))) :
    (a : (↑(of R ((↑M : Type v) →₀ Shrink.{v, u} R)) : Type v)) → (↑M : Type v))
Tactic: rw [epi_iff_range_eq_top, LinearMap.range_eq_top]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Projective (goal)
Goal:
R : Type u
inst : Ring R
P M_1 : ModuleCat.{v, u} R
inst_1 : Small.{v, u} R
M : ModuleCat.{v, u} R
e : Basis.{v, u, v} (↑M : Type v) R ((↑M : Type v) →₀ Shrink.{v, u} R) :=
  { repr := Finsupp.mapRange.linearEquiv (Shrink.linearEquiv R R) }
⊢ Function.Surjective.{v + 1, v + 1} (α := (↑(of R ((↑M : Type v) →₀ Shrink.{v, u} R)) : Type v)) (β := (↑M : Type v))
    (⇑(Hom.hom
          (↟((e.constr ℕ : (a : (↑M : Type v) → (↑M : Type v)) → ((↑M : Type v) →₀ Shrink.{v, u} R) →ₗ[R] (↑M : Type v))
              id))) :
      (a : (↑(of R ((↑M : Type v) →₀ Shrink.{v, u} R)) : Type v)) → (↑M : Type v))
have refine : ∀ (m : (↑M : Type v)),
  (Hom.hom
          (↟((e.constr ℕ : (a : (↑M : Type v) → (↑M : Type v)) → ((↑M : Type v) →₀ Shrink.{v, u} R) →ₗ[R] (↑M : Type v))
              id)) :
        (a : (↑(of R ((↑M : Type v) →₀ Shrink.{v, u} R)) : Type v)) → (↑M : Type v))
      (Finsupp.single m 1) =
    m
Tactic: refine fun m ↦ ⟨Finsupp.single m 1, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension (hypothesis)
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')
inst_4 this : HasProjectiveDimensionLE M 0
⊢ HasProjectiveDimensionLE N 0
have this₁ : HasProjectiveDimensionLT M 1
Tactic: simp only [HasProjectiveDimensionLE, zero_add] at this ⊢
Cleared hypotheses: this
-- 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')
inst_4 : HasProjectiveDimensionLE M 0
this : HasProjectiveDimensionLT M 1
⊢ HasProjectiveDimensionLT N 1
have zero : ∀ (this : Module.Projective.{u, v} R (↑M : Type v)), Module.Projective.{u', v'} R' (↑N : Type v')
Tactic: rw [← projective_iff_hasProjectiveDimensionLT_one, ← IsProjective.iff_projective] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension (hypothesis)
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'
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')
inst_4 : HasProjectiveDimensionLE M (n + 1)
S : ShortComplex (ModuleCat.{v, u} R) := M.projectiveShortComplex
S' : ShortComplex (ModuleCat.{v', u'} R') := N.projectiveShortComplex
⊢ HasProjectiveDimensionLE N (n + 1)
have S_exact : M.projectiveShortComplex.ShortExact
Tactic: have S_exact := M.shortExact_projectiveShortComplex
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension (hypothesis)
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'
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')
inst_4 : HasProjectiveDimensionLE M (n + 1)
S : ShortComplex (ModuleCat.{v, u} R) := M.projectiveShortComplex
S' : ShortComplex (ModuleCat.{v', u'} R') := N.projectiveShortComplex
S_exact : M.projectiveShortComplex.ShortExact
⊢ HasProjectiveDimensionLE N (n + 1)
have S'_exact : N.projectiveShortComplex.ShortExact
Tactic: have S'_exact := N.shortExact_projectiveShortComplex
-- 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'
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')
inst_4 : HasProjectiveDimensionLE M (n + 1)
S : ShortComplex (ModuleCat.{v, u} R) := M.projectiveShortComplex
S' : ShortComplex (ModuleCat.{v', u'} R') := N.projectiveShortComplex
S_exact : M.projectiveShortComplex.ShortExact
S'_exact : N.projectiveShortComplex.ShortExact
eR : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (Shrink.{v, u} R) (Shrink.{v', u'} R') :=
  LinearEquiv.trans (re₁₂ := ⋯) (re₂₁ := ⋯) (LinearEquiv.trans (Shrink.linearEquiv R R) e.toSemilinearEquiv)
    (LinearEquiv.symm (Shrink.linearEquiv R' R'))
e2 : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑S.X₂ : Type v) (↑S'.X₂ : Type v') :=
  LinearEquiv.trans (Finsupp.mapDomain.linearEquiv (Shrink.{v, u} R) R (↑e' : (↑M : Type v) ≃ (↑N : Type v')))
    (Finsupp.mapRange.linearEquiv eR)
⊢ Hom.hom S'.g ∘ₛₗ (↑e2 : (↑S.X₂ : Type v) →ₛₗ[(↑e : R →+* R')] (↑S'.X₂ : Type v')) =
    (↑e' : (↑M : Type v) →ₛₗ[(↑e : R →+* R')] (↑N : Type v')) ∘ₛₗ Hom.hom S.g
have h : ∀ (m : (↑M : Type v)) (r : Shrink.{v, u} R),
  Eq.{v' + 1} (α := (↑S'.X₃ : Type v'))
    ((((Hom.hom S'.g ∘ₛₗ (↑e2 : (↑S.X₂ : Type v) →ₛₗ[(↑e : R →+* R')] (↑S'.X₂ : Type v'))).comp (σ₁₂ := RingHom.id R)
              (Finsupp.lsingle m) :
            LinearMap.{u, u', v, v'} (↑e : R →+* R') (Shrink.{v, u} R) (↑S'.X₃ : Type v')) :
          (a : Shrink.{v, u} R) → (↑S'.X₃ : Type v'))
        r :
      (↑S'.X₃ : Type v'))
    (((((↑e' : (↑M : Type v) →ₛₗ[(↑e : R →+* R')] (↑N : Type v')) ∘ₛₗ Hom.hom S.g).comp (σ₁₂ := RingHom.id R)
              (Finsupp.lsingle m) :
            LinearMap.{u, u', v, v'} (↑e : R →+* R') (Shrink.{v, u} R) (↑S'.X₃ : Type v')) :
          (a : Shrink.{v, u} R) → (↑S'.X₃ : Type v'))
        r :
      (↑S'.X₃ : Type v'))
Tactic: ext m r
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension (hypothesis)
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'
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')
inst_4 : HasProjectiveDimensionLE M (n + 1)
S : ShortComplex (ModuleCat.{v, u} R) := M.projectiveShortComplex
S' : ShortComplex (ModuleCat.{v', u'} R') := N.projectiveShortComplex
S_exact : M.projectiveShortComplex.ShortExact
S'_exact : N.projectiveShortComplex.ShortExact
eR : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (Shrink.{v, u} R) (Shrink.{v', u'} R') :=
  LinearEquiv.trans (re₁₂ := ⋯) (re₂₁ := ⋯) (LinearEquiv.trans (Shrink.linearEquiv R R) e.toSemilinearEquiv)
    (LinearEquiv.symm (Shrink.linearEquiv R' R'))
e2 : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑S.X₂ : Type v) (↑S'.X₂ : Type v') :=
  LinearEquiv.trans (Finsupp.mapDomain.linearEquiv (Shrink.{v, u} R) R (↑e' : (↑M : Type v) ≃ (↑N : Type v')))
    (Finsupp.mapRange.linearEquiv eR)
⊢ HasProjectiveDimensionLE N (n + 1)
have comm : Hom.hom S'.g ∘ₛₗ (↑e2 : (↑S.X₂ : Type v) →ₛₗ[(↑e : R →+* R')] (↑S'.X₂ : Type v')) =
  (↑e' : (↑M : Type v) →ₛₗ[(↑e : R →+* R')] (↑N : Type v')) ∘ₛₗ Hom.hom S.g
Tactic: 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ₛₗ]
-- 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'
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')
inst_4 : HasProjectiveDimensionLE M (n + 1)
S : ShortComplex (ModuleCat.{v, u} R) := M.projectiveShortComplex
S' : ShortComplex (ModuleCat.{v', u'} R') := N.projectiveShortComplex
S_exact : M.projectiveShortComplex.ShortExact
S'_exact : N.projectiveShortComplex.ShortExact
eR : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (Shrink.{v, u} R) (Shrink.{v', u'} R') :=
  LinearEquiv.trans (re₁₂ := ⋯) (re₂₁ := ⋯) (LinearEquiv.trans (Shrink.linearEquiv R R) e.toSemilinearEquiv)
    (LinearEquiv.symm (Shrink.linearEquiv R' R'))
e2 : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑S.X₂ : Type v) (↑S'.X₂ : Type v') :=
  LinearEquiv.trans (Finsupp.mapDomain.linearEquiv (Shrink.{v, u} R) R (↑e' : (↑M : Type v) ≃ (↑N : Type v')))
    (Finsupp.mapRange.linearEquiv eR)
comm :
  Hom.hom S'.g ∘ₛₗ (↑e2 : (↑S.X₂ : Type v) →ₛₗ[(↑e : R →+* R')] (↑S'.X₂ : Type v')) =
    (↑e' : (↑M : Type v) →ₛₗ[(↑e : R →+* R')] (↑N : Type v')) ∘ₛₗ Hom.hom S.g
⊢ (Hom.hom S.g).ker =
    Submodule.comap (↑e2 : (↑S.X₂ : Type v) →ₛₗ[(↑e : R →+* R')] (↑S'.X₂ : Type v')) (Hom.hom S'.g).ker
have rw : (Hom.hom S.g).ker = (Hom.hom S'.g ∘ₛₗ (↑e2 : (↑S.X₂ : Type v) →ₛₗ[(↑e : R →+* R')] (↑S'.X₂ : Type v'))).ker
Tactic: rw [← LinearMap.ker_comp, comm, LinearEquiv.ker_comp]
-- 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'
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')
inst_4 : HasProjectiveDimensionLE M (n + 1)
S : ShortComplex (ModuleCat.{v, u} R) := M.projectiveShortComplex
S' : ShortComplex (ModuleCat.{v', u'} R') := N.projectiveShortComplex
S_exact : M.projectiveShortComplex.ShortExact
S'_exact : N.projectiveShortComplex.ShortExact
eR : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (Shrink.{v, u} R) (Shrink.{v', u'} R') :=
  LinearEquiv.trans (re₁₂ := ⋯) (re₂₁ := ⋯) (LinearEquiv.trans (Shrink.linearEquiv R R) e.toSemilinearEquiv)
    (LinearEquiv.symm (Shrink.linearEquiv R' R'))
e2 : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑S.X₂ : Type v) (↑S'.X₂ : Type v') :=
  LinearEquiv.trans (Finsupp.mapDomain.linearEquiv (Shrink.{v, u} R) R (↑e' : (↑M : Type v) ≃ (↑N : Type v')))
    (Finsupp.mapRange.linearEquiv eR)
comm :
  Hom.hom S'.g ∘ₛₗ (↑e2 : (↑S.X₂ : Type v) →ₛₗ[(↑e : R →+* R')] (↑S'.X₂ : Type v')) =
    (↑e' : (↑M : Type v) →ₛₗ[(↑e : R →+* R')] (↑N : Type v')) ∘ₛₗ Hom.hom S.g
rw : (Hom.hom S.g).ker = (Hom.hom S'.g ∘ₛₗ (↑e2 : (↑S.X₂ : Type v) →ₛₗ[(↑e : R →+* R')] (↑S'.X₂ : Type v'))).ker
⊢ (Hom.hom S.g).ker =
    Submodule.comap (↑e2 : (↑S.X₂ : Type v) →ₛₗ[(↑e : R →+* R')] (↑S'.X₂ : Type v')) (Hom.hom S'.g).ker
have rw₁ : (Hom.hom S.g).ker = ((↑e' : (↑M : Type v) →ₛₗ[(↑e : R →+* R')] (↑N : Type v')) ∘ₛₗ Hom.hom S.g).ker
Tactic: rw [← LinearMap.ker_comp, comm, LinearEquiv.ker_comp]
-- 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'
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')
inst_4 : HasProjectiveDimensionLE M (n + 1)
S : ShortComplex (ModuleCat.{v, u} R) := M.projectiveShortComplex
S' : ShortComplex (ModuleCat.{v', u'} R') := N.projectiveShortComplex
S_exact : M.projectiveShortComplex.ShortExact
S'_exact : N.projectiveShortComplex.ShortExact
eR : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (Shrink.{v, u} R) (Shrink.{v', u'} R') :=
  LinearEquiv.trans (re₁₂ := ⋯) (re₂₁ := ⋯) (LinearEquiv.trans (Shrink.linearEquiv R R) e.toSemilinearEquiv)
    (LinearEquiv.symm (Shrink.linearEquiv R' R'))
e2 : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑S.X₂ : Type v) (↑S'.X₂ : Type v') :=
  LinearEquiv.trans (Finsupp.mapDomain.linearEquiv (Shrink.{v, u} R) R (↑e' : (↑M : Type v) ≃ (↑N : Type v')))
    (Finsupp.mapRange.linearEquiv eR)
comm :
  Hom.hom S'.g ∘ₛₗ (↑e2 : (↑S.X₂ : Type v) →ₛₗ[(↑e : R →+* R')] (↑S'.X₂ : Type v')) =
    (↑e' : (↑M : Type v) →ₛₗ[(↑e : R →+* R')] (↑N : Type v')) ∘ₛₗ Hom.hom S.g
rw : (Hom.hom S.g).ker = (Hom.hom S'.g ∘ₛₗ (↑e2 : (↑S.X₂ : Type v) →ₛₗ[(↑e : R →+* R')] (↑S'.X₂ : Type v'))).ker
rw₁ : (Hom.hom S.g).ker = ((↑e' : (↑M : Type v) →ₛₗ[(↑e : R →+* R')] (↑N : Type v')) ∘ₛₗ Hom.hom S.g).ker
⊢ (Hom.hom S.g).ker =
    Submodule.comap (↑e2 : (↑S.X₂ : Type v) →ₛₗ[(↑e : R →+* R')] (↑S'.X₂ : Type v')) (Hom.hom S'.g).ker
have rw₂ : (Hom.hom S.g).ker = (Hom.hom S.g).ker
Tactic: rw [← LinearMap.ker_comp, comm, LinearEquiv.ker_comp]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension (hypothesis)
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'
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')
inst_4 : HasProjectiveDimensionLE M (n + 1)
S : ShortComplex (ModuleCat.{v, u} R) := M.projectiveShortComplex
S' : ShortComplex (ModuleCat.{v', u'} R') := N.projectiveShortComplex
S_exact : M.projectiveShortComplex.ShortExact
S'_exact : N.projectiveShortComplex.ShortExact
eR : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (Shrink.{v, u} R) (Shrink.{v', u'} R') :=
  LinearEquiv.trans (re₁₂ := ⋯) (re₂₁ := ⋯) (LinearEquiv.trans (Shrink.linearEquiv R R) e.toSemilinearEquiv)
    (LinearEquiv.symm (Shrink.linearEquiv R' R'))
e2 : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑S.X₂ : Type v) (↑S'.X₂ : Type v') :=
  LinearEquiv.trans (Finsupp.mapDomain.linearEquiv (Shrink.{v, u} R) R (↑e' : (↑M : Type v) ≃ (↑N : Type v')))
    (Finsupp.mapRange.linearEquiv eR)
comm :
  Hom.hom S'.g ∘ₛₗ (↑e2 : (↑S.X₂ : Type v) →ₛₗ[(↑e : R →+* R')] (↑S'.X₂ : Type v')) =
    (↑e' : (↑M : Type v) →ₛₗ[(↑e : R →+* R')] (↑N : Type v')) ∘ₛₗ Hom.hom S.g
⊢ HasProjectiveDimensionLE N (n + 1)
have this : (Hom.hom S.g).ker = Submodule.comap (↑e2 : (↑S.X₂ : Type v) →ₛₗ[(↑e : R →+* R')] (↑S'.X₂ : Type v')) (Hom.hom S'.g).ker
Tactic: have : S.g.hom.ker = Submodule.comap e2.toLinearMap S'.g.hom.ker := by
      rw [← LinearMap.ker_comp, comm, LinearEquiv.ker_comp]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension (hypothesis)
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'
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')
inst_4 : HasProjectiveDimensionLE M (n + 1)
S : ShortComplex (ModuleCat.{v, u} R) := M.projectiveShortComplex
S' : ShortComplex (ModuleCat.{v', u'} R') := N.projectiveShortComplex
S_exact : M.projectiveShortComplex.ShortExact
S'_exact : N.projectiveShortComplex.ShortExact
eR : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (Shrink.{v, u} R) (Shrink.{v', u'} R') :=
  LinearEquiv.trans (re₁₂ := ⋯) (re₂₁ := ⋯) (LinearEquiv.trans (Shrink.linearEquiv R R) e.toSemilinearEquiv)
    (LinearEquiv.symm (Shrink.linearEquiv R' R'))
e2 : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑S.X₂ : Type v) (↑S'.X₂ : Type v') :=
  LinearEquiv.trans (Finsupp.mapDomain.linearEquiv (Shrink.{v, u} R) R (↑e' : (↑M : Type v) ≃ (↑N : Type v')))
    (Finsupp.mapRange.linearEquiv eR)
comm :
  Hom.hom S'.g ∘ₛₗ (↑e2 : (↑S.X₂ : Type v) →ₛₗ[(↑e : R →+* R')] (↑S'.X₂ : Type v')) =
    (↑e' : (↑M : Type v) →ₛₗ[(↑e : R →+* R')] (↑N : Type v')) ∘ₛₗ Hom.hom S.g
this :
  (Hom.hom S.g).ker =
    Submodule.comap (↑e2 : (↑S.X₂ : Type v) →ₛₗ[(↑e : R →+* R')] (↑S'.X₂ : Type v')) (Hom.hom S'.g).ker
⊢ HasProjectiveDimensionLE N (n + 1)
have this₁ : (Hom.hom S.g).ker =
  Submodule.map (↑e2.symm : (↑S'.X₂ : Type v') →ₛₗ[(↑e.symm : R' →+* R)] (↑S.X₂ : Type v)) (Hom.hom S'.g).ker
Tactic: rw [Submodule.comap_equiv_eq_map_symm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension (hypothesis)
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'
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')
inst_4 : HasProjectiveDimensionLE M (n + 1)
S : ShortComplex (ModuleCat.{v, u} R) := M.projectiveShortComplex
S' : ShortComplex (ModuleCat.{v', u'} R') := N.projectiveShortComplex
S_exact : M.projectiveShortComplex.ShortExact
S'_exact : N.projectiveShortComplex.ShortExact
eR : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (Shrink.{v, u} R) (Shrink.{v', u'} R') :=
  LinearEquiv.trans (re₁₂ := ⋯) (re₂₁ := ⋯) (LinearEquiv.trans (Shrink.linearEquiv R R) e.toSemilinearEquiv)
    (LinearEquiv.symm (Shrink.linearEquiv R' R'))
e2 : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑S.X₂ : Type v) (↑S'.X₂ : Type v') :=
  LinearEquiv.trans (Finsupp.mapDomain.linearEquiv (Shrink.{v, u} R) R (↑e' : (↑M : Type v) ≃ (↑N : Type v')))
    (Finsupp.mapRange.linearEquiv eR)
comm :
  Hom.hom S'.g ∘ₛₗ (↑e2 : (↑S.X₂ : Type v) →ₛₗ[(↑e : R →+* R')] (↑S'.X₂ : Type v')) =
    (↑e' : (↑M : Type v) →ₛₗ[(↑e : R →+* R')] (↑N : Type v')) ∘ₛₗ Hom.hom S.g
this :
  (Hom.hom S.g).ker =
    Submodule.map (↑e2.symm : (↑S'.X₂ : Type v') →ₛₗ[(↑e.symm : R' →+* R)] (↑S.X₂ : Type v)) (Hom.hom S'.g).ker
eker : LinearEquiv.{u, u', v, v'} (↑e : R →+* R') (↑S.X₁ : Type v) (↑S'.X₁ : Type v') :=
  (LinearEquiv.ofEq (Hom.hom S.g).ker
        (Submodule.map (↑e2.symm : (↑S'.X₂ : Type v') →ₛₗ[(↑e.symm : R' →+* R)] (↑S.X₂ : Type v)) (Hom.hom S'.g).ker)
        this).trans
    (LinearEquiv.symm (e2.symm.submoduleMap (Hom.hom S'.g).ker))
⊢ HasProjectiveDimensionLE N (n + 1)
have this₁ : HasProjectiveDimensionLT M.projectiveShortComplex.X₁ (n + 1)
Tactic: have := (S_exact.hasProjectiveDimensionLT_X₃_iff n inferInstance).mp ‹_›
-- 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
⊢ HasProjectiveDimensionLE N n
have 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
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