mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderLimitsOfShape (Discrete WalkingPair)
X Y : P.FullSubcategory
⊢ ∀ {T : P.FullSubcategory} (f : T ⟶ X) (g : T ⟶ Y)
    (m : T ⟶ (BinaryFan.mk (ObjectProperty.homMk (fst X.obj Y.obj)) (ObjectProperty.homMk (snd X.obj Y.obj))).pt),
    m ≫ (BinaryFan.mk (ObjectProperty.homMk (fst X.obj Y.obj)) (ObjectProperty.homMk (snd X.obj Y.obj))).fst = f →
      m ≫ (BinaryFan.mk (ObjectProperty.homMk (fst X.obj Y.obj)) (ObjectProperty.homMk (snd X.obj Y.obj))).snd = g →
        m = ObjectProperty.homMk (lift f.hom g.hom)

Tactic:
by aesop_cat

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
antipode : A →ₗ[R] A
antipode_convMul_id : toConv antipode * toConv LinearMap.id = 1
id_convMul_antipode : toConv LinearMap.id * toConv antipode = 1
⊢ mul' R A ∘ₗ lTensor A antipode ∘ₗ comul = Algebra.linearMap R A ∘ₗ counit

Tactic:
simpa using! congr(($id_convMul_antipode).ofConv)

Goal state after:
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
⊢ toConv (antipode R) * toConv id = 1

Tactic:
ext c

Goal state after:
R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
c : C
⊢ (toConv (antipode R) * toConv id).ofConv c = (ofConv 1) c
Module: Mathlib.RingTheory.HopfAlgebra.Convolution

Goal state before:
pp: R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
⊢ toConv id * toConv (antipode R) = 1

Tactic:
ext c

Goal state after:
R : Type u_1
C : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring C
inst✝ : HopfAlgebra R C
c : C
⊢ (toConv id * toConv (antipode R)).ofConv c = (ofConv 1) c
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
⊢ ι ≫ f = f ≫ ι

Tactic:
suffices lift (lift f (ι ≫ f)) f =
      lift (lift f (f ≫ ι)) f by simpa using (this =≫ fst _ _) =≫ snd _ _
  apply (isPullback B).hom_ext <;> apply CartesianMonoidalCategory.hom_ext <;>
    simp [lift_inv_comp_right, lift_inv_comp_left]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
G✝ H✝ H₁ H₂ G H : Grp C
⊢ ∀ {T : Grp C} (f : T ⟶ G) (g : T ⟶ H),
    { hom := lift f.hom g.hom } ≫ (BinaryFan.mk (homMk' (fst G.toMon H.toMon)) (homMk' (snd G.toMon H.toMon))).fst = f

Tactic:
by aesop_cat

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
G✝ H✝ H₁ H₂ G H : Grp C
⊢ ∀ {T : Grp C} (f : T ⟶ G) (g : T ⟶ H),
    { hom := lift f.hom g.hom } ≫ (BinaryFan.mk (homMk' (fst G.toMon H.toMon)) (homMk' (snd G.toMon H.toMon))).snd = g

Tactic:
by aesop_cat

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
G✝ H✝ H₁ H₂ G H : Grp C
⊢ ∀ {T : Grp C} (f : T ⟶ G) (g : T ⟶ H)
    (m : T ⟶ (BinaryFan.mk (homMk' (fst G.toMon H.toMon)) (homMk' (snd G.toMon H.toMon))).pt),
    m ≫ (BinaryFan.mk (homMk' (fst G.toMon H.toMon)) (homMk' (snd G.toMon H.toMon))).fst = f →
      m ≫ (BinaryFan.mk (homMk' (fst G.toMon H.toMon)) (homMk' (snd G.toMon H.toMon))).snd = g →
        m = { hom := lift f.hom g.hom }

Tactic:
by aesop_cat

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
p : Submodule R M'
⊢ lift.{v, u} (Module.rank R ↥(comap f p)) ≤ lift.{u, v} (Module.rank R ↥p) + lift.{v, u} (Module.rank R ↥f.ker)

Tactic:
let f' : comap f p →ₗ[R] p := f.restrict (by aesop)
  have hk : Module.rank R f'.ker ≤ Module.rank R f.ker := by
    rw [← rank_map_eq (injective_subtype (comap f p))]
    exact rank_mono fun x hx ↦ by aesop (add simp Subtype.ext_iff)
  have hr : Module.rank R f'.range ≤ Module.rank R p := by grw [Submodule.rank_le f'.range]
  rw [← f'.lift_rank_range_add_rank_ker]
  gcongr <;> rwa [lift_le]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : ↑n < Module.rank R M
⊢ ∃ x, LinearIndependent R (Fin.cons x v)

Tactic:
obtain ⟨t, h₁, h₂, h₃⟩ := exists_linearIndepOn_of_lt_rank hv.linearIndepOn_id

Goal state after:
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : ↑n < Module.rank R M
t : Set M
h₁ : Set.range v ⊆ t
h₂ : #↑t = Module.rank R M
h₃ : LinearIndepOn R _root_.id t
⊢ ∃ x, LinearIndependent R (Fin.cons x v)
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s t : Submodule K V
hdim : finrank K V ≤ finrank K ↥s + finrank K ↥t
hdisjoint : Disjoint s t
⊢ finrank K ↥(s ⊓ t) = 0

Tactic:
rw [disjoint_iff_inf_le, le_bot_iff] at hdisjoint

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s t : Submodule K V
hdim : finrank K V ≤ finrank K ↥s + finrank K ↥t
hdisjoint : s ⊓ t = ⊥
⊢ finrank K ↥(s ⊓ t) = 0
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: case «2»
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
S : Subalgebra F E
this✝² : FiniteDimensional F E
this✝¹ : FiniteDimensional F ↥S
h : finrank F ↥S = finrank F E
this✝ : 2 ≤ 2
this : 0 < 2
⊢ S = ⊤

Tactic:
rw [← Algebra.toSubmodule_eq_top]

Goal state after:
case «2»
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
S : Subalgebra F E
this✝² : FiniteDimensional F E
this✝¹ : FiniteDimensional F ↥S
h : finrank F ↥S = finrank F E
this✝ : 2 ≤ 2
this : 0 < 2
⊢ toSubmodule S = ⊤
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case left
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module.Finite R M
inst✝ : Projective R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
g : M →ₗ[R] Fin n → R
eq : f ∘ₗ g = LinearMap.id
⊢ Function.Injective (⇑(lcomp R N f) ∘ ⇑(dualTensorHom R M N))

Tactic:
← coe_comp,

Goal state after:
case left
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module.Finite R M
inst✝ : Projective R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
g : M →ₗ[R] Fin n → R
eq : f ∘ₗ g = LinearMap.id
⊢ Function.Injective ⇑(lcomp R N f ∘ₗ dualTensorHom R M N)
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case right
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module.Finite R M
inst✝ : Projective R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
g : M →ₗ[R] Fin n → R
eq : f ∘ₗ g = LinearMap.id
⊢ Function.Surjective (⇑(dualTensorHom R M N) ∘ ⇑(rTensor N g.dualMap))

Tactic:
← coe_comp,

Goal state after:
case right
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module.Finite R M
inst✝ : Projective R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
g : M →ₗ[R] Fin n → R
eq : f ∘ₗ g = LinearMap.id
⊢ Function.Surjective ⇑(dualTensorHom R M N ∘ₗ rTensor N g.dualMap)
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
I : R →+* R
B : M →ₗ[R] M →ₛₗ[I] M₃
B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃
x✝¹ : M
x✝ : M₁
⊢ (B' (0 x✝¹)) x✝ = (B x✝¹) (0 x✝)

Tactic:
by
  simp only [Pi.zero_apply, map_zero, zero_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : DecidableEq ι
⊢ dualTensorHom R M (ι →₀ N) =
    finsuppLinearMap R ∘ₗ Finsupp.mapRange.linearMap (dualTensorHom R M N) ∘ₗ ↑(finsuppRight R R (Dual R M) N ι)

Tactic:
by
  ext; simp [Finsupp.single_apply]; aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
g : P →ₗ[R] N
comp_eq_id : g ∘ₗ f = LinearMap.id
h : Function.Bijective ⇑(dualTensorHom R M P)
⊢ Function.Injective (⇑(compRight R f) ∘ ⇑(dualTensorHom R M N))

Tactic:
← coe_comp,

Goal state after:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
g : P →ₗ[R] N
comp_eq_id : g ∘ₗ f = LinearMap.id
h : Function.Bijective ⇑(dualTensorHom R M P)
⊢ Function.Injective ⇑(compRight R f ∘ₗ dualTensorHom R M N)
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
g : P →ₗ[R] N
comp_eq_id : g ∘ₗ f = LinearMap.id
h : Function.Bijective ⇑(dualTensorHom R M P)
⊢ Function.Surjective (⇑(dualTensorHom R M N) ∘ ⇑(lTensor (Dual R M) g))

Tactic:
← coe_comp,

Goal state after:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
g : P →ₗ[R] N
comp_eq_id : g ∘ₗ f = LinearMap.id
h : Function.Bijective ⇑(dualTensorHom R M P)
⊢ Function.Surjective ⇑(dualTensorHom R M N ∘ₗ lTensor (Dual R M) g)
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case pos
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
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
he : (B x) y * (B y) x = (B x) x * (B y) y
hz : (B x) y • x - (B x) x • y = 0
hL : LinearIndependent R ![x, y]
hx : x = 0
⊢ False

Tactic:
simpa [hx] using LinearIndependent.ne_zero 0 hL

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
F : J ⥤ C
c₁ : Fan F.obj
c₂ : Fan fun f ↦ F.obj f.fst.2
s t : c₁.pt ⟶ c₂.pt
hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), s ≫ c₂.π.app { as := f } = c₁.π.app { as := f.fst.1 } ≫ F.map f.snd
ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), t ≫ c₂.π.app { as := f } = c₁.π.app { as := f.fst.2 }
i : Fork s t
t₁ : IsLimit c₁
t₂ : IsLimit c₂
hi : IsLimit i
q : Cone F
⊢ t₁.lift (Fan.mk q.1 fun j ↦ q.π.app j) ≫ s = t₁.lift (Fan.mk q.1 fun j ↦ q.π.app j) ≫ t

Tactic:
apply t₂.hom_ext
      intro ⟨j⟩
      simp [hs, ht]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := K ∙ x
hp : p ≠ ⊥
⊢ LinearMap.ker f ⊓ p = ⊥

Tactic:
Submodule.eq_bot_iff

Goal state after:
K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
inst✝ : FiniteDimensional K V₁
f g : Dual K V₁
x : V₁
h : LinearMap.ker f = LinearMap.ker g
h' : f x = g x
hx : f x ≠ 0
p : Submodule K V₁ := K ∙ x
hp : p ≠ ⊥
⊢ ∀ x ∈ LinearMap.ker f ⊓ p, x = 0
Module: Mathlib.Algebra.Category.ModuleCat.Kernels

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
y : ↑N
m : ↑M
⊢ (ConcreteCategory.hom (cokernel.π f)) (y + (ConcreteCategory.hom f) m) = (ConcreteCategory.hom (cokernel.π f)) y

Tactic:
simpa only [map_add, add_eq_left] using! cokernel.condition_apply f m

Goal state after:
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✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCokernels C
inst✝² : IsNormalEpiCategory C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst✝¹ : Epi a
inst✝ : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (coprod.desc f g)
hb' : b ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
reassoced' : ∀ {W : C} (h : cokernel (coprod.desc f g) ⟶ W), b ≫ b' ≫ h = cokernel.π (coprod.desc f g) ≫ h
⊢ b ≫ b' ≫ cokernel.desc (coprod.desc f g) (b ≫ s.inr) ⋯ = b ≫ s.inr

Tactic:
simp [reassoced']

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X : C
⊢ diag X ≫ σ = 0

Tactic:
rw [cokernel.condition_assoc, zero_comp]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A : Type u
B : Type v
inst✝¹ : Group A
inst✝ : Group B
f : A →* B
h : ∀ (u v : ↥f.ker →* A), f.comp u = f.comp v → u = v
⊢ f.ker = ⊥

Tactic:
by simpa using congr_arg range (h f.ker.subtype 1 (by cat_disch))

Goal state after:
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
b : ↑B
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [← y.2.choose_spec, leftCoset_assoc]
          let b' : B := y.2.choose
          use b * b'

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₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ cyclesMap φ = h₁.cyclesIso.hom ≫ γ.φK ≫ h₂.cyclesIso.inv

Tactic:
dsimp [LeftHomologyData.cyclesIso, cyclesMapIso']

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ cyclesMap φ = cyclesMap' (𝟙 S₁) S₁.leftHomologyData h₁ ≫ γ.φK ≫ cyclesMap' (𝟙 S₂) h₂ S₂.leftHomologyData
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₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ cyclesMap φ = cyclesMap' (𝟙 S₁) S₁.leftHomologyData h₁ ≫ γ.φK ≫ cyclesMap' (𝟙 S₂) h₂ S₂.leftHomologyData

Tactic:
← γ.cyclesMap'_eq,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ cyclesMap φ = cyclesMap' (𝟙 S₁) S₁.leftHomologyData h₁ ≫ cyclesMap' φ h₁ h₂ ≫ cyclesMap' (𝟙 S₂) h₂ S₂.leftHomologyData
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₁ h₁' : S.LeftHomologyData
h₂ h₂' : S.RightHomologyData
⊢ leftRightHomologyComparison' h₁ h₂ =
    leftRightHomologyComparison' h₁ h₂ ≫ rightHomologyMap' (𝟙 S) h₂ h₂' ≫ rightHomologyMap' (𝟙 S) h₂' h₂

Tactic:
← rightHomologyMap'_comp,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h₁ h₁' : S.LeftHomologyData
h₂ h₂' : S.RightHomologyData
⊢ leftRightHomologyComparison' h₁ h₂ = leftRightHomologyComparison' h₁ h₂ ≫ rightHomologyMap' (𝟙 S ≫ 𝟙 S) h₂ h₂
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ homologyMap φ ≫ S₂.leftHomologyData.homologyIso.hom ≫ leftRightHomologyComparison' S₂.leftHomologyData h₂ =
    S₁.leftHomologyData.homologyIso.hom ≫
      leftRightHomologyComparison' S₁.leftHomologyData h₁ ≫ h₁.homologyIso.inv ≫ homologyMap φ ≫ h₂.homologyIso.hom

Tactic:
leftRightHomologyComparison'_fac,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ homologyMap φ ≫ S₂.leftHomologyData.homologyIso.hom ≫ S₂.leftHomologyData.homologyIso.inv ≫ h₂.homologyIso.hom =
    S₁.leftHomologyData.homologyIso.hom ≫
      leftRightHomologyComparison' S₁.leftHomologyData h₁ ≫ h₁.homologyIso.inv ≫ homologyMap φ ≫ h₂.homologyIso.hom
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ homologyMap φ ≫ S₂.leftHomologyData.homologyIso.hom ≫ S₂.leftHomologyData.homologyIso.inv ≫ h₂.homologyIso.hom =
    S₁.leftHomologyData.homologyIso.hom ≫
      leftRightHomologyComparison' S₁.leftHomologyData h₁ ≫ h₁.homologyIso.inv ≫ homologyMap φ ≫ h₂.homologyIso.hom

Tactic:
leftRightHomologyComparison'_fac,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ homologyMap φ ≫ S₂.leftHomologyData.homologyIso.hom ≫ S₂.leftHomologyData.homologyIso.inv ≫ h₂.homologyIso.hom =
    S₁.leftHomologyData.homologyIso.hom ≫
      (S₁.leftHomologyData.homologyIso.inv ≫ h₁.homologyIso.hom) ≫
        h₁.homologyIso.inv ≫ homologyMap φ ≫ h₂.homologyIso.hom
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₁ S₂ S₃ : ShortComplex C
e : S₁ ≅ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ rightHomologyMap' e.hom h₁ h₂ ≫ rightHomologyMap' e.inv h₂ h₁ = 𝟙 h₁.H

Tactic:
← rightHomologyMap'_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
e : S₁ ≅ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ rightHomologyMap' (e.hom ≫ e.inv) h₁ h₁ = 𝟙 h₁.H
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₁ S₂ S₃ : ShortComplex C
e : S₁ ≅ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ rightHomologyMap' e.inv h₂ h₁ ≫ rightHomologyMap' e.hom h₁ h₂ = 𝟙 h₂.H

Tactic:
← rightHomologyMap'_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
e : S₁ ≅ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ rightHomologyMap' (e.inv ≫ e.hom) h₂ h₂ = 𝟙 h₂.H
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₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ rightHomologyMap φ =
    rightHomologyMap' (𝟙 S₁) S₁.rightHomologyData h₁ ≫
      rightHomologyMap' φ h₁ h₂ ≫ rightHomologyMap' (𝟙 S₂) h₂ S₂.rightHomologyData

Tactic:
← rightHomologyMap'_comp,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ rightHomologyMap φ =
    rightHomologyMap' (𝟙 S₁) S₁.rightHomologyData h₁ ≫ rightHomologyMap' (φ ≫ 𝟙 S₂) h₁ S₂.rightHomologyData
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₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ rightHomologyMap φ =
    rightHomologyMap' (𝟙 S₁) S₁.rightHomologyData h₁ ≫ rightHomologyMap' (φ ≫ 𝟙 S₂) h₁ S₂.rightHomologyData

Tactic:
← rightHomologyMap'_comp,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ rightHomologyMap φ = rightHomologyMap' (𝟙 S₁ ≫ φ ≫ 𝟙 S₂) S₁.rightHomologyData S₂.rightHomologyData
Module: Mathlib.Algebra.Homology.ShortComplex.Limits

Goal state before:
pp: 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 : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
j : J
⊢ (h₁.lift (π₁.mapCone s) ≫ c.pt.f) ≫ (π₂.mapCone c).π.app j =
    (s.pt.f ≫ h₂.lift (π₂.mapCone s)) ≫ (π₂.mapCone c).π.app j

Tactic:
by
        have eq₁ := h₁.fac (π₁.mapCone s)
        have eq₂ := h₂.fac (π₂.mapCone s)
        have eq₁₂ := fun j => (c.π.app j).comm₁₂
        have eq₁₂' := fun j => (s.π.app j).comm₁₂
        dsimp at eq₁ eq₂ eq₁₂ eq₁₂' ⊢
        rw [assoc, assoc, ← eq₁₂, reassoc_of% eq₁, eq₂, eq₁₂']

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

Goal state before:
pp: S : ShortComplex Ab
⊢ S.Exact ↔ Function.Exact ⇑(ConcreteCategory.hom S.f) ⇑(ConcreteCategory.hom S.g)

Tactic:
rw [S.ab_exact_iff]
  apply forall_congr'
  intro x₂
  constructor
  · intro h
    refine ⟨h, ?_⟩
    rintro ⟨x₁, rfl⟩
    simp only [ab_zero_apply]
  · tauto

Goal state after: