awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Projective
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) }
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))
⊢ 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))

Tactic:
rw [epi_iff_range_eq_top, LinearMap.range_eq_top]

Premises used: LinearMap.range_eq_top, ModuleCat.epi_iff_range_eq_top
-- Module: Mathlib.Algebra.Category.ModuleCat.Projective
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))

Tactic:
fun m ↦ ⟨Finsupp.single m 1, ?_⟩

Premises used: Exists.intro, OfNat.ofNat, Function.Surjective, Finsupp.single
-- Module: Mathlib.Algebra.Category.ModuleCat.Projective
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) }
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
⊢ 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:
refine fun m ↦ ⟨Finsupp.single m 1, ?_⟩
-- Module: Mathlib.Algebra.Category.ModuleCat.Projective
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) }
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:
simp [e, Basis.constr_apply]

Premises used: Module.Basis.constr_apply
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
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
⊢ HasProjectiveDimensionLE M 0

Tactic:
have : HasProjectiveDimensionLE M 0 := ‹_›
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
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
⊢ HasProjectiveDimensionLT M 1

Tactic:
simp only [HasProjectiveDimensionLE, zero_add] at this ⊢

Premises used: CategoryTheory.HasProjectiveDimensionLE, zero_add
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
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
zero : ∀ (this : Module.Projective.{u, v} R (↑M : Type v)), Module.Projective.{u', v'} R' (↑N : Type v')
⊢ HasProjectiveDimensionLT N 1

Tactic:
rw [← projective_iff_hasProjectiveDimensionLT_one, ← IsProjective.iff_projective] at this ⊢

Premises used: IsProjective.iff_projective, CategoryTheory.projective_iff_hasProjectiveDimensionLT_one
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
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 : Module.Projective.{u, v} R (↑M : Type v)
⊢ Module.Projective.{u', v'} R' (↑N : Type v')

Tactic:
Projective.of_equiv e'

Premises used: Module.Projective.of_equiv
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
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 : Module.Projective.{u, v} R (↑M : Type v)
⊢ Module.Projective.{u', v'} R' (↑N : Type v')

Tactic:
exact Projective.of_equiv e'

Premises used: Module.Projective.of_equiv
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
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
⊢ M.projectiveShortComplex.ShortExact

Tactic:
have S_exact := M.shortExact_projectiveShortComplex
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
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
⊢ N.projectiveShortComplex.ShortExact

Tactic:
have S'_exact := N.shortExact_projectiveShortComplex
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
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)
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'))
⊢ 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:
ext m r
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
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)
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:
simp [S, S', e2, eR, Basis.constr_apply, map_smulₛₗ]

Premises used: MulActionSemiHomClass.map_smulₛₗ, Module.Basis.constr_apply
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
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

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ₛₗ]
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
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
rw₂ rw₃ : (Hom.hom S.g).ker = (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

Tactic:
rw [← LinearMap.ker_comp, comm, LinearEquiv.ker_comp]

Premises used: LinearMap.ker_comp, LinearEquiv.ker_comp
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
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

Tactic:
have : S.g.hom.ker = Submodule.comap e2.toLinearMap S'.g.hom.ker := by
      rw [← LinearMap.ker_comp, comm, LinearEquiv.ker_comp]
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
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
⊢ (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

Premises used: Submodule.comap_equiv_eq_map_symm
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
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))
⊢ HasProjectiveDimensionLT M.projectiveShortComplex.X₁ (n + 1)

Tactic:
have := (S_exact.hasProjectiveDimensionLT_X₃_iff n inferInstance).mp ‹_›
-- Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
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_1 :
  (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_1).trans
    (LinearEquiv.symm (e2.symm.submoduleMap (Hom.hom S'.g).ker))
this : HasProjectiveDimensionLT M.projectiveShortComplex.X₁ (n + 1)
⊢ HasProjectiveDimensionLE N (n + 1)

Tactic:
(S'_exact.hasProjectiveDimensionLT_X₃_iff n inferInstance).mpr (ih eker)

Premises used: Iff.mpr, CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃_iff, inferInstance