mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Coevaluation

Goal state before:
pp: K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.lTensor V (contractLeft K V))
      ((TensorProduct.assoc K V (Dual K V) V)
        ((∑ i, (Basis.ofVectorSpace K V) i ⊗ₜ[K] (Basis.ofVectorSpace K V).coord i) ⊗ₜ[K]
          (Basis.ofVectorSpace K V) j)) =
    (Basis.ofVectorSpace K V) j ⊗ₜ[K] 1

Tactic:
TensorProduct.sum_tmul,

Goal state after:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.lTensor V (contractLeft K V))
      ((TensorProduct.assoc K V (Dual K V) V)
        (∑ a, (Basis.ofVectorSpace K V) a ⊗ₜ[K] (Basis.ofVectorSpace K V).coord a ⊗ₜ[K] (Basis.ofVectorSpace K V) j)) =
    (Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
Module: Mathlib.Algebra.Category.FGModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
V W : Type v
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : Module.Finite R W
e : V ≃ₗ[R] W
⊢ ConcreteCategory.ofHom ↑e ≫ ConcreteCategory.ofHom ↑e.symm = 𝟙 (of R V)

Tactic:
ext x

Goal state after:
R : Type u
inst✝⁶ : Ring R
V W : Type v
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : Module.Finite R W
e : V ≃ₗ[R] W
x : ↑(of R V).obj
⊢ (ModuleCat.Hom.hom (ConcreteCategory.ofHom ↑e ≫ ConcreteCategory.ofHom ↑e.symm).hom) x =
    (ModuleCat.Hom.hom (𝟙 (of R V)).hom) x
Module: Mathlib.Algebra.Category.FGModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
V W : Type v
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : Module.Finite R W
e : V ≃ₗ[R] W
⊢ ConcreteCategory.ofHom ↑e.symm ≫ ConcreteCategory.ofHom ↑e = 𝟙 (of R W)

Tactic:
ext x

Goal state after:
R : Type u
inst✝⁶ : Ring R
V W : Type v
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : Module.Finite R V
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : Module.Finite R W
e : V ≃ₗ[R] W
x : ↑(of R W).obj
⊢ (ModuleCat.Hom.hom (ConcreteCategory.ofHom ↑e.symm ≫ ConcreteCategory.ofHom ↑e).hom) x =
    (ModuleCat.Hom.hom (𝟙 (of R W)).hom) x
Module: Mathlib.Algebra.Category.ModuleCat.Products

Goal state before:
pp: R : Type u
inst✝ : Ring R
ι : Type v
Z : ι → ModuleCat R
s : Cone (Discrete.functor Z)
m : s.pt ⟶ (productCone Z).pt
w : ∀ (j : Discrete ι), m ≫ (productCone Z).π.app j = s.π.app j
⊢ m = ↟(LinearMap.pi fun j ↦ Hom.hom (s.π.app { as := j }))

Tactic:
ext x

Goal state after:
R : Type u
inst✝ : Ring R
ι : Type v
Z : ι → ModuleCat R
s : Cone (Discrete.functor Z)
m : s.pt ⟶ (productCone Z).pt
w : ∀ (j : Discrete ι), m ≫ (productCone Z).π.app j = s.π.app j
x : ↑s.pt
⊢ (Hom.hom m) x = (Hom.hom (↟(LinearMap.pi fun j ↦ Hom.hom (s.π.app { as := j })))) x
Module: Mathlib.Algebra.Category.ModuleCat.Products

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
ι : Type v
Z : ι → ModuleCat R
inst✝ : DecidableEq ι
s : Cocone (Discrete.functor Z)
f : (coproductCocone Z).pt ⟶ s.pt
h : ∀ (j : Discrete ι), (coproductCocone Z).ι.app j ≫ f = s.ι.app j
i : ι
⊢ Hom.hom f ∘ₗ lof R ι (fun i ↦ ↑(Z i)) i =
    Hom.hom (↟(toModule R ι ↑s.1 fun i ↦ Hom.hom (s.ι.app { as := i }))) ∘ₗ lof R ι (fun i ↦ ↑(Z i)) i

Tactic:
ext x

Goal state after:
R : Type u
inst✝¹ : Ring R
ι : Type v
Z : ι → ModuleCat R
inst✝ : DecidableEq ι
s : Cocone (Discrete.functor Z)
f : (coproductCocone Z).pt ⟶ s.pt
h : ∀ (j : Discrete ι), (coproductCocone Z).ι.app j ≫ f = s.ι.app j
i : ι
x : ↑(Z i)
⊢ (Hom.hom f ∘ₗ lof R ι (fun i ↦ ↑(Z i)) i) x =
    (Hom.hom (↟(toModule R ι ↑s.1 fun i ↦ Hom.hom (s.ι.app { as := i }))) ∘ₗ lof R ι (fun i ↦ ↑(Z i)) i) x
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
⊢ B.flip.ker = B.ker

Tactic:
ext x

Goal state after:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
x : M₁
⊢ x ∈ B.flip.ker ↔ x ∈ B.ker
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
hp' : Projective R (M ⧸ p)
hp : ∀ (x : M), x ∈ p
x✝ : M
⊢ x✝ ∈ p ↔ x✝ ∈ ⊤

Tactic:
simp [hp]

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case inr.inr
R : Type u_1
M : Type u_5
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x = 0
hy : (B y) y ≤ 0
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y

Tactic:
replace hy : B y y = 0 := le_antisymm hy (hs y)

Goal state after:
case inr.inr
R : Type u_1
M : Type u_5
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x = 0
hy : (B y) y = 0
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, (L i).ker ≤ K.ker
x✝¹ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
p : Submodule 𝕜 E := ⨅ i, (L i).ker
p_eq : p = φ.ker
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := p.liftQ φ ⋯
x✝ : FiniteDimensional 𝕜 (E ⧸ p)
L' : ι → E ⧸ p →ₗ[𝕜] 𝕜 := fun i ↦ p.liftQ (L i) ⋯
K' : E ⧸ p →ₗ[𝕜] 𝕜 := p.liftQ K h
this : ⨅ i, (L' i).ker ≤ K'.ker
c : ι → 𝕜
hK' : ∑ i, c i • L' i = K'
⊢ ∑ i, c i • p.liftQ (L i) ⋯ ∘ₗ p.mkQ = K

Tactic:
← p.liftQ_mkQ K h

Goal state after:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, (L i).ker ≤ K.ker
x✝¹ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
p : Submodule 𝕜 E := ⨅ i, (L i).ker
p_eq : p = φ.ker
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := p.liftQ φ ⋯
x✝ : FiniteDimensional 𝕜 (E ⧸ p)
L' : ι → E ⧸ p →ₗ[𝕜] 𝕜 := fun i ↦ p.liftQ (L i) ⋯
K' : E ⧸ p →ₗ[𝕜] 𝕜 := p.liftQ K h
this : ⨅ i, (L' i).ker ≤ K'.ker
c : ι → 𝕜
hK' : ∑ i, c i • L' i = K'
⊢ ∑ i, c i • p.liftQ (L i) ⋯ ∘ₗ p.mkQ = p.liftQ K h ∘ₗ p.mkQ
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, (L i).ker ≤ K.ker
x✝¹ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
p : Submodule 𝕜 E := ⨅ i, (L i).ker
p_eq : p = φ.ker
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := p.liftQ φ ⋯
x✝ : FiniteDimensional 𝕜 (E ⧸ p)
L' : ι → E ⧸ p →ₗ[𝕜] 𝕜 := fun i ↦ p.liftQ (L i) ⋯
K' : E ⧸ p →ₗ[𝕜] 𝕜 := p.liftQ K h
this : ⨅ i, (L' i).ker ≤ K'.ker
c : ι → 𝕜
hK' : ∑ i, c i • L' i = K'
⊢ ∑ i, c i • p.liftQ (L i) ⋯ ∘ₗ p.mkQ = p.liftQ K h ∘ₗ p.mkQ

Tactic:
ext x

Goal state after:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, (L i).ker ≤ K.ker
x✝¹ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
p : Submodule 𝕜 E := ⨅ i, (L i).ker
p_eq : p = φ.ker
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := p.liftQ φ ⋯
x✝ : FiniteDimensional 𝕜 (E ⧸ p)
L' : ι → E ⧸ p →ₗ[𝕜] 𝕜 := fun i ↦ p.liftQ (L i) ⋯
K' : E ⧸ p →ₗ[𝕜] 𝕜 := p.liftQ K h
this : ⨅ i, (L' i).ker ≤ K'.ker
c : ι → 𝕜
hK' : ∑ i, c i • L' i = K'
x : E
⊢ (∑ i, c i • p.liftQ (L i) ⋯ ∘ₗ p.mkQ) x = (p.liftQ K h ∘ₗ p.mkQ) x
Module: Mathlib.Algebra.Category.ModuleCat.Kernels

Goal state before:
pp: case zero
R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f✝ f : M ⟶ N
g : N ⟶ P
H : Function.Exact ⇑(Hom.hom f) ⇑(Hom.hom g)
H₂ : Function.Injective ⇑(Hom.hom f)
⊢ (kernelCone g).π.app WalkingParallelPair.zero =
    (LinearEquiv.ofInjective (Hom.hom f) H₂ ≪≫ₗ
              LinearEquiv.ofEq (Hom.hom f).range (Hom.hom g).ker ⋯).toModuleIso.symm.hom ≫
      (KernelFork.ofι f ⋯).π.app WalkingParallelPair.zero

Tactic:
ext x

Goal state after:
case zero
R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f✝ f : M ⟶ N
g : N ⟶ P
H : Function.Exact ⇑(Hom.hom f) ⇑(Hom.hom g)
H₂ : Function.Injective ⇑(Hom.hom f)
x : ↑(((Functor.const WalkingParallelPair).obj (kernelCone g).pt).obj WalkingParallelPair.zero)
⊢ (Hom.hom ((kernelCone g).π.app WalkingParallelPair.zero)) x =
    (Hom.hom
        ((LinearEquiv.ofInjective (Hom.hom f) H₂ ≪≫ₗ
                  LinearEquiv.ofEq (Hom.hom f).range (Hom.hom g).ker ⋯).toModuleIso.symm.hom ≫
          (KernelFork.ofι f ⋯).π.app WalkingParallelPair.zero))
      x
Module: Mathlib.Algebra.Category.ModuleCat.Kernels

Goal state before:
pp: case one
R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f✝ f : M ⟶ N
g : N ⟶ P
H : Function.Exact ⇑(Hom.hom f) ⇑(Hom.hom g)
H₂ : Function.Injective ⇑(Hom.hom f)
⊢ (kernelCone g).π.app WalkingParallelPair.one =
    (LinearEquiv.ofInjective (Hom.hom f) H₂ ≪≫ₗ
              LinearEquiv.ofEq (Hom.hom f).range (Hom.hom g).ker ⋯).toModuleIso.symm.hom ≫
      (KernelFork.ofι f ⋯).π.app WalkingParallelPair.one

Tactic:
ext x

Goal state after:
case one
R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f✝ f : M ⟶ N
g : N ⟶ P
H : Function.Exact ⇑(Hom.hom f) ⇑(Hom.hom g)
H₂ : Function.Injective ⇑(Hom.hom f)
x : ↑(((Functor.const WalkingParallelPair).obj (kernelCone g).pt).obj WalkingParallelPair.one)
⊢ (Hom.hom ((kernelCone g).π.app WalkingParallelPair.one)) x =
    (Hom.hom
        ((LinearEquiv.ofInjective (Hom.hom f) H₂ ≪≫ₗ
                  LinearEquiv.ofEq (Hom.hom f).range (Hom.hom g).ker ⋯).toModuleIso.symm.hom ≫
          (KernelFork.ofι f ⋯).π.app WalkingParallelPair.one))
      x
Module: Mathlib.Algebra.Category.ModuleCat.Kernels

Goal state before:
pp: case zero
R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f✝ f : M ⟶ N
g : N ⟶ P
H : Function.Exact ⇑(Hom.hom f) ⇑(Hom.hom g)
H₂ : Function.Surjective ⇑(Hom.hom g)
⊢ (cokernelCocone f).ι.app WalkingParallelPair.zero ≫
      (((Hom.hom g).ker.quotEquivOfEq (Hom.hom f).range ⋯).toModuleIso.symm ≪≫
          ((Hom.hom g).quotKerEquivOfSurjective H₂).toModuleIso).hom =
    (CokernelCofork.ofπ g ⋯).ι.app WalkingParallelPair.zero

Tactic:
ext x

Goal state after:
case zero
R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f✝ f : M ⟶ N
g : N ⟶ P
H : Function.Exact ⇑(Hom.hom f) ⇑(Hom.hom g)
H₂ : Function.Surjective ⇑(Hom.hom g)
x : ↑((parallelPair f 0).obj WalkingParallelPair.zero)
⊢ (Hom.hom
        ((cokernelCocone f).ι.app WalkingParallelPair.zero ≫
          (((Hom.hom g).ker.quotEquivOfEq (Hom.hom f).range ⋯).toModuleIso.symm ≪≫
              ((Hom.hom g).quotKerEquivOfSurjective H₂).toModuleIso).hom))
      x =
    (Hom.hom ((CokernelCofork.ofπ g ⋯).ι.app WalkingParallelPair.zero)) x
Module: Mathlib.Algebra.Category.ModuleCat.Kernels

Goal state before:
pp: case one
R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f✝ f : M ⟶ N
g : N ⟶ P
H : Function.Exact ⇑(Hom.hom f) ⇑(Hom.hom g)
H₂ : Function.Surjective ⇑(Hom.hom g)
⊢ (cokernelCocone f).ι.app WalkingParallelPair.one ≫
      (((Hom.hom g).ker.quotEquivOfEq (Hom.hom f).range ⋯).toModuleIso.symm ≪≫
          ((Hom.hom g).quotKerEquivOfSurjective H₂).toModuleIso).hom =
    (CokernelCofork.ofπ g ⋯).ι.app WalkingParallelPair.one

Tactic:
ext x

Goal state after:
case one
R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f✝ f : M ⟶ N
g : N ⟶ P
H : Function.Exact ⇑(Hom.hom f) ⇑(Hom.hom g)
H₂ : Function.Surjective ⇑(Hom.hom g)
x : ↑((parallelPair f 0).obj WalkingParallelPair.one)
⊢ (Hom.hom
        ((cokernelCocone f).ι.app WalkingParallelPair.one ≫
          (((Hom.hom g).ker.quotEquivOfEq (Hom.hom f).range ⋯).toModuleIso.symm ≪≫
              ((Hom.hom g).quotKerEquivOfSurjective H₂).toModuleIso).hom))
      x =
    (Hom.hom ((CokernelCofork.ofπ g ⋯).ι.app WalkingParallelPair.one)) x
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst✝ : IsReflexive K V₂
⊢ B.ker.dualAnnihilator = B.flip.range

Tactic:
by
  change _ = range (B.dualMap.comp (Module.evalEquiv K V₂).toLinearMap)
  rw [← range_dualMap_eq_dualAnnihilator_ker, range_comp_of_range_eq_top _ (LinearEquiv.range _)]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝² : HasCokernel f
inst✝¹ : HasCokernel (G.map f)
inst✝ : PreservesColimit (parallelPair f 0) G
⊢ (iso G f).inv = cokernelComparison f G

Tactic:
by
  rw [← cancel_epi (cokernel.π _)]
  simp [PreservesCokernel.iso]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
hf : NormalMono f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
⊢ IsLimit (KernelFork.ofι f' ⋯)

Tactic:
refine (IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_).1 hf.isLimit

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
hf : NormalMono f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
⊢ parallelPair g 0 ≅ parallelPair (Arrow.Hom.right e.inv ≫ g) 0

case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
hf : NormalMono f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
⊢ (Cone.postcompose (Iso.hom ?refine_1)).obj (KernelFork.ofι f ⋯) ≅ KernelFork.ofι f' ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasKernels C
inst✝² : IsNormalMonoCategory C
X Y Z : C
a : X ⟶ Z
b : Y ⟶ Z
inst✝¹ : Mono a
inst✝ : Mono b
P : C
f : Z ⟶ P
haf : a ≫ f = 0
i : IsLimit (KernelFork.ofι a haf)
Q : C
g : Z ⟶ Q
hbg : b ≫ g = 0
i' : IsLimit (KernelFork.ofι b hbg)
a' : kernel (prod.lift f g) ⟶ (KernelFork.ofι a haf).pt
ha' : a' ≫ Fork.ι (KernelFork.ofι a haf) = kernel.ι (prod.lift f g)
b' : kernel (prod.lift f g) ⟶ (KernelFork.ofι b hbg).pt
hb' : b' ≫ Fork.ι (KernelFork.ofι b hbg) = kernel.ι (prod.lift f g)
s : PullbackCone a b
m : s.pt ⟶ kernel (prod.lift f g)
h₁ : m ≫ a' = s.fst
x✝ : m ≫ b' = s.snd
⊢ s.snd ≫ b = kernel.lift (prod.lift f g) (s.snd ≫ b) ⋯ ≫ kernel.ι (prod.lift f g)

Tactic:
kernel.lift_ι

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteProducts C
inst✝³ : HasKernels C
inst✝² : IsNormalMonoCategory C
X Y Z : C
a : X ⟶ Z
b : Y ⟶ Z
inst✝¹ : Mono a
inst✝ : Mono b
P : C
f : Z ⟶ P
haf : a ≫ f = 0
i : IsLimit (KernelFork.ofι a haf)
Q : C
g : Z ⟶ Q
hbg : b ≫ g = 0
i' : IsLimit (KernelFork.ofι b hbg)
a' : kernel (prod.lift f g) ⟶ (KernelFork.ofι a haf).pt
ha' : a' ≫ Fork.ι (KernelFork.ofι a haf) = kernel.ι (prod.lift f g)
b' : kernel (prod.lift f g) ⟶ (KernelFork.ofι b hbg).pt
hb' : b' ≫ Fork.ι (KernelFork.ofι b hbg) = kernel.ι (prod.lift f g)
s : PullbackCone a b
m : s.pt ⟶ kernel (prod.lift f g)
h₁ : m ≫ a' = s.fst
x✝ : m ≫ b' = s.snd
⊢ s.snd ≫ b = s.snd ≫ b
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
P Q : C
f : P ⟶ Q
I : C := Abelian.image f
p : P ⟶ Abelian.image f := Abelian.factorThruImage f
i : kernel (cokernel.π f) ⟶ Q := kernel.ι (cokernel.π f)
R : C
g : I ⟶ R
hpg : p ≫ g = 0
u : kernel g ⟶ Q := kernel.ι g ≫ i
hu : NormalMono u
h : Q ⟶ NormalMono.Z u := NormalMono.g
t : P ⟶ kernel g
ht : t ≫ kernel.ι g = p
fh : f ≫ h = 0
⊢ g = 0

Tactic:
obtain ⟨l, hl⟩ := cokernel.desc' f h fh

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
P Q : C
f : P ⟶ Q
I : C := Abelian.image f
p : P ⟶ Abelian.image f := Abelian.factorThruImage f
i : kernel (cokernel.π f) ⟶ Q := kernel.ι (cokernel.π f)
R : C
g : I ⟶ R
hpg : p ≫ g = 0
u : kernel g ⟶ Q := kernel.ι g ≫ i
hu : NormalMono u
h : Q ⟶ NormalMono.Z u := NormalMono.g
t : P ⟶ kernel g
ht : t ≫ kernel.ι g = p
fh : f ≫ h = 0
l : cokernel f ⟶ NormalMono.Z u
hl : cokernel.π f ≫ l = h
⊢ g = 0
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: case e'_2.e'_7
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
s : KernelFork (cokernel.π f)
e_1✝ : (s.pt ⟶ Y✝) = (s.pt ⟶ (parallelPair (cokernel.π f) 0).obj WalkingParallelPair.zero)
e_5✝ : Y✝ = (parallelPair (cokernel.π f) 0).obj WalkingParallelPair.zero
⊢ inv (imageMonoFactorisation f).e ≫ f = limit.π (parallelPair (cokernel.π f) 0) WalkingParallelPair.zero

Tactic:
rw [IsIso.inv_comp_eq, eq_comm]

Goal state after:
case e'_2.e'_7
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
s : KernelFork (cokernel.π f)
e_1✝ : (s.pt ⟶ Y✝) = (s.pt ⟶ (parallelPair (cokernel.π f) 0).obj WalkingParallelPair.zero)
e_5✝ : Y✝ = (parallelPair (cokernel.π f) 0).obj WalkingParallelPair.zero
⊢ (imageMonoFactorisation f).e ≫ limit.π (parallelPair (cokernel.π f) 0) WalkingParallelPair.zero = f
Module: Mathlib.Algebra.Homology.ShortComplex.QuasiIso

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
⊢ QuasiIso φ ↔ IsIso γ.φH

Tactic:
by
  rw [ShortComplex.quasiIso_iff, γ.homologyMap_eq]
  constructor
  · intro h
    have : IsIso (γ.φH ≫ (RightHomologyData.homologyIso h₂).inv) :=
      IsIso.of_isIso_comp_left (RightHomologyData.homologyIso h₁).hom _
    exact IsIso.of_isIso_comp_right _ (RightHomologyData.homologyIso h₂).inv
  · intro h
    infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
hg : S.g = 0
⊢ h.i ≫ h.liftK (𝟙 S.X₂) ⋯ = 𝟙 h.K

Tactic:
simp only [← cancel_mono h.i, id_comp, assoc, liftK_i, comp_id]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ₁ ψ₂ : LeftHomologyMapData φ h₁ h₂
hK : ψ₁.φK = ψ₂.φK
⊢ ψ₁.φH = ψ₂.φH

Tactic:
rw [← cancel_epi h₁.π, commπ, commπ, hK]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ leftRightHomologyComparison' h₁ h₂ = h₁.descH (h₂.liftH (h₁.i ≫ h₂.p) ⋯) ⋯

Tactic:
simp only [← cancel_mono h₂.ι, ← cancel_epi h₁.π, π_leftRightHomologyComparison'_ι,
    LeftHomologyData.π_descH_assoc, RightHomologyData.liftH_ι]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ (leftHomologyMap φ).op = S₂.rightHomologyOpIso.inv ≫ rightHomologyMap (opMap φ) ≫ S₁.rightHomologyOpIso.hom

Tactic:
dsimp [rightHomologyOpIso, RightHomologyData.rightHomologyIso, rightHomologyMap,
    leftHomologyMap]
  simp only [← rightHomologyMap'_comp, comp_id, id_comp, leftHomologyMap'_op]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ (leftHomologyMap φ).op = S₂.rightHomologyOpIso.inv ≫ rightHomologyMap (opMap φ) ≫ S₁.rightHomologyOpIso.hom

Tactic:
by
  dsimp [rightHomologyOpIso, RightHomologyData.rightHomologyIso, rightHomologyMap,
    leftHomologyMap]
  simp only [← rightHomologyMap'_comp, comp_id, id_comp, leftHomologyMap'_op]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Abelian

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
⊢ f' = kernel.lift γ f' ⋯ ≫ kernel.ι γ

Tactic:
kernel.lift_ι

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
⊢ f' = f'
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ (-φ₁).τ₃ = -h.h₃ + (-h.h₂) ≫ S₂.g + (-φ₂).τ₃

Tactic:
neg_τ₃,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ -φ₁.τ₃ = -h.h₃ + (-h.h₂) ≫ S₂.g + (-φ₂).τ₃
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ -φ₁.τ₃ = -h.h₃ + (-h.h₂) ≫ S₂.g + (-φ₂).τ₃

Tactic:
neg_τ₃,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ -φ₁.τ₃ = -h.h₃ + (-h.h₂) ≫ S₂.g + -φ₂.τ₃
Module: Mathlib.Algebra.Homology.ShortComplex.Limits

Goal state before:
pp: case h₂
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
⊢ m.τ₂ =
    { τ₁ := h₁.desc (π₁.mapCocone s), τ₂ := h₂.desc (π₂.mapCocone s), τ₃ := h₃.desc (π₃.mapCocone s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }.τ₂

Tactic:
exact h₂.uniq (π₂.mapCocone s) _ (fun j => π₂.congr_map (hm j))

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X E✝ X✝ : Type u
f : X ⟶ X✝
e : E✝ ⟶ X✝
x✝ : Epi e
he : Function.Surjective ⇑(ConcreteCategory.hom e)
⊢ (↾fun x ↦ ⋯.choose) ≫ e = f

Tactic:
ext x

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X E✝ X✝ : Type u
f : X ⟶ X✝
e : E✝ ⟶ X✝
x✝ : Epi e
he : Function.Surjective ⇑(ConcreteCategory.hom e)
x : X
⊢ (ConcreteCategory.hom ((↾fun x ↦ ⋯.choose) ≫ e)).toFun x = (ConcreteCategory.hom f).toFun x