mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
X₁ X₂ : J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j
⊢ W.colimitsOfShape J φ

Tactic:
obtain rfl : φ = h₁.desc (Cocone.mk _ (f ≫ c₂.ι)) := h₁.hom_ext (fun j ↦ by simp [hφ])

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
X₁ X₂ : J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
hφ : ∀ (j : J), c₁.ι.app j ≫ h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } = f.app j ≫ c₂.ι.app j
⊢ W.colimitsOfShape J (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝² : Category.{v_1, u_1} J
J' : Type u_2
inst✝¹ : Category.{v_2, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X₁ X₂ : J' ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J' f
h₁' : IsColimit (Cocone.whisker F c₁)
h₂' : IsColimit (Cocone.whisker F c₂)
⊢ W.colimitsOfShape J (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })

Tactic:
have : h₁.desc (Cocone.mk c₂.pt (f ≫ c₂.ι)) =
      h₁'.desc (Cocone.mk c₂.pt (Functor.whiskerLeft _ f ≫ (c₂.whisker F).ι)) :=
    h₁'.hom_ext (fun j ↦ by
      have := h₁'.fac (Cocone.mk c₂.pt (Functor.whiskerLeft F f ≫ Functor.whiskerLeft F c₂.ι)) j
      dsimp at this ⊢
      simp [this])

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝² : Category.{v_1, u_1} J
J' : Type u_2
inst✝¹ : Category.{v_2, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X₁ X₂ : J' ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J' f
h₁' : IsColimit (Cocone.whisker F c₁)
h₂' : IsColimit (Cocone.whisker F c₂)
this : h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } = h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ (Cocone.whisker F c₂).ι }
⊢ W.colimitsOfShape J (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : IsStableUnderCoproducts.{w, v, u} W
⊢ coproducts.{w, v, u} W ≤ W

Tactic:
intro X Y f hf
  rw [coproducts_iff] at hf
  obtain ⟨J, hf⟩ := hf
  exact colimitsOfShape_le _ hf

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.isoClosure.colimitsOfShape J = P.colimitsOfShape J

Tactic:
refine le_antisymm ?_ (colimitsOfShape_monotone _ (P.le_isoClosure))

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.isoClosure.colimitsOfShape J ≤ P.colimitsOfShape J
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : HasPushout f f
⊢ (codiagonal f).op = pullback.diagonal f.op ≫ (pullbackIsoOpPushout f.op f.op).hom

Tactic:
rw [← Iso.comp_inv_eq]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : HasPushout f f
⊢ (codiagonal f).op ≫ (pullbackIsoOpPushout f.op f.op).inv = pullback.diagonal f.op
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : HasPushout f f
H : IsIso (codiagonal f)
Z✝ : C
x✝¹ x✝ : Y ⟶ Z✝
e : f ≫ x✝¹ = f ≫ x✝
⊢ x✝¹ = x✝

Tactic:
by rw [← inl_desc _ _ e, (cancel_mono (g := inl f f) (h := inr f f)
    (codiagonal f)).mp (by simp), inr_desc]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y : C
f : X ⟶ 𝟙_ C
g : X ⟶ Y
⊢ lift f g ≫ (λ_ Y).hom = g

Tactic:
by
  rw [← Iso.eq_comp_inv]
  cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y : C
f : X ⟶ Y
g : X ⟶ 𝟙_ C
⊢ lift f g ≫ (ρ_ Y).hom = f

Tactic:
by
  rw [← Iso.eq_comp_inv]
  cat_disch

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A B C D T✝ : CommAlgCat R
f : A ⟶ T✝
g : B ⟶ T✝
⊢ Hom.hom ((A.binaryCofan B).inl ≫ ofHom (Algebra.TensorProduct.lift (Hom.hom f) (Hom.hom g) ⋯)) = Hom.hom f

Tactic:
exact lift_comp_includeLeft _ _ fun _ _ ↦ .all _ _

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
ι : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : Coalgebra R C
f : WithConv (C →ₗ[R] A)
x✝ : C
⊢ (1 * f).ofConv x✝ = f.ofConv x✝

Tactic:
simp [convOne_def, ← map_comp_rTensor]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y : C
⊢ F.map (X ◁ toUnit Y) ≫ F.map (ρ_ X).hom = F.map (fst X Y)

Tactic:
simp [← Functor.map_comp, rightUnitor_hom]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
G X✝ : C
inst✝¹ : GrpObj G
A B G' X : C
inst✝ : AddGrpObj G'
e : G' ≅ X
⊢ lift (e.inv ≫ AddGrpObj.neg ≫ e.hom) (𝟙 X) ≫ AddMonObj.add = toUnit X ≫ AddMonObj.zero

Tactic:
by simp +instances [AddMonObj.ofIso]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
G X✝ : C
inst✝¹ : GrpObj G
A B G' X : C
inst✝ : AddGrpObj G'
e : G' ≅ X
⊢ lift (𝟙 X) (e.inv ≫ AddGrpObj.neg ≫ e.hom) ≫ AddMonObj.add = toUnit X ≫ AddMonObj.zero

Tactic:
by simp +instances [AddMonObj.ofIso]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
A B X✝ X' Y Y' Z : C
inst✝¹ : Closed A
inst✝ : MonoidalClosed C
X : Cᵒᵖ
⊢ (internalHom.obj X).IsRightAdjoint

Tactic:
bdsimp
  infer_instance

Goal state after:
Module: Mathlib.Data.W.Cardinal

Goal state before:
pp: α : Type u
β : α → Type u
⊢ (sum fun a ↦ #(WType β) ^ lift.{u, u} #(β a)) = sum fun a ↦ #(WType β) ^ #(β a)

Tactic:
lift_id

Goal state after:
Module: Mathlib.Data.W.Cardinal

Goal state before:
pp: α : Type u
β : α → Type u
κ : Cardinal.{u}
hκ : (sum fun a ↦ κ ^ #(β a)) ≤ κ
⊢ (sum fun a ↦ κ ^ lift.{u, u} #(β a)) ≤ κ

Tactic:
lift_id

Goal state after:
α : Type u
β : α → Type u
κ : Cardinal.{u}
hκ : (sum fun a ↦ κ ^ #(β a)) ≤ κ
⊢ (sum fun a ↦ κ ^ #(β a)) ≤ κ
Module: Mathlib.Data.W.Cardinal

Goal state before:
pp: α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
⊢ max (lift.{u, u} #α) ℵ₀ = max #α ℵ₀

Tactic:
lift_id

Goal state after:
α : Type u
β : α → Type u
inst✝ : ∀ (a : α), Finite (β a)
⊢ max #α ℵ₀ = max #α ℵ₀
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
inst✝² : DivisionRing K
V : Type u
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank K V = lift.{u, u} (Module.rank K V)

Tactic:
lift_id

Goal state after:
K : Type u
inst✝² : DivisionRing K
V : Type u
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank K V = Module.rank K V
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K V : Type u
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank K V = lift.{u, u} (Module.rank K V)

Tactic:
lift_id

Goal state after:
K V : Type u
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank K V = Module.rank K V
Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ (∀ (n m : ℕ) (a : Matrix (Fin n) (Fin m) R) (a_1 : Matrix (Fin m) (Fin n) R),
      toLinearMapRight' (a_1 * a) = LinearMap.id → m ≤ n) ↔
    ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), g * f = 1 → m ≤ n

Tactic:
← toLinearMapRight'_one,

Goal state after:
R : Type u_1
inst✝ : Semiring R
⊢ (∀ (n m : ℕ) (a : Matrix (Fin n) (Fin m) R) (a_1 : Matrix (Fin m) (Fin n) R),
      toLinearMapRight' (a_1 * a) = toLinearMapRight' 1 → m ≤ n) ↔
    ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), g * f = 1 → m ≤ n
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: case refine_1
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
t : K
hw : t • v ∈ W ⊓ K ∙ v
ht : t • v ∈ W
⊢ t • v = 0

Tactic:
rcases eq_or_ne t 0 with rfl | ht₀

Goal state after:
case refine_1.inl
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
hw : 0 • v ∈ W ⊓ K ∙ v
ht : 0 • v ∈ W
⊢ 0 • v = 0

case refine_1.inr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
t : K
hw : t • v ∈ W ⊓ K ∙ v
ht : t • v ∈ W
ht₀ : t ≠ 0
⊢ t • v = 0
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix

Goal state before:
pp: case e'_3
K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ #(M →ₐ[K] L) = lift.{max u_2 v, max u_2 v} #(M →ₐ[K] L)

Tactic:
lift_id

Goal state after:
case e'_3
K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ #(M →ₐ[K] L) = #(M →ₐ[K] L)
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Field K₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), (B (v i)) (v i) ≠ 0
s : Finset n
w : n → K₁
hs : ∑ i ∈ s, w i • v i = 0
i : n
hi : i ∈ s
this : (B (∑ i ∈ s, w i • v i)) (v i) = 0
j : n
_hj : j ∈ s
hij : j ≠ i
⊢ I₁ (w j) • (B (v j)) (v i) = 0

Tactic:
rw [isOrthoᵢ_def.1 hv₁ _ _ hij, smul_zero]

Goal state after:
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)

Tactic:
· refine .of_comp (g := g.dualMap.rTensor N) ?_
    rw [← coe_comp, dualTensorHom_comp_rTensor_dualMap, coe_comp,
      ← coe_dualTensorHomEquivOfBasis (Pi.basisFun ..)]
    refine (surjective_of_comp_eq_id (f.lcomp R N) _ ?_).comp (EquivLike.surjective _)
    ext φ; exact congr(φ ($eq _))

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

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
hB' : B.SeparatingRight
⊢ B.flip.ker = ⊥

Tactic:
← separatingRight_iff_flip_ker_eq_bot

Goal state after:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
hB : B.IsRefl
hB' : B.SeparatingRight
⊢ B.SeparatingRight
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K✝ : Type uK
V✝ : Type uV
inst✝¹³ : CommSemiring K✝
inst✝¹² : AddCommMonoid V✝
inst✝¹¹ : Module K✝ V✝
inst✝¹⁰ : Projective K✝ V✝
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : IsReflexive R M
K : Type u_4
V : Type u_5
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : IsReflexive K V
contra : ℵ₀ ≤ Module.rank K V
this : lift.{?u.55, u_5} (Module.rank K V) < Module.rank K (Dual K (Dual K V))
⊢ False

Tactic:
by
    have heq := lift_rank_eq_of_equiv_equiv (R := K) (R' := K) (M := V) (M' := Dual K (Dual K V))
      (ZeroHom.id K) (evalEquiv K V) bijective_id (fun r v ↦ (evalEquiv K V).map_smul _ _)
    rw [← lift_umax, heq, lift_id'] at this
    exact lt_irrefl _ this

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

Goal state before:
pp: 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
inst✝ : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
⊢ (B x) y * (B y) x < (B x) x * (B y) y ↔ LinearIndependent R ![x, y]

Tactic:
by
  have hle z : 0 ≤ B z z := by obtain rfl | hz := eq_or_ne z 0 <;> simp [le_of_lt, *]
  constructor
  · contrapose!
    intro h
    rw [LinearIndependent.pair_iff] at h
    push Not at h
    obtain ⟨r, s, hl, h0⟩ := h
    by_cases hr : r = 0; · simp_all
    by_cases hs : s = 0; · simp_all
    suffices
        (B (r • x) (r • x)) * (B (s • y) (s • y)) = (B (r • x) (s • y)) * (B (s • y) (r • x)) by
      simp only [map_smul, smul_apply, smul_eq_mul] at this
      rw [show r * (r * (B x) x) * (s * (s * (B y) y)) = (r * r * s * s) * ((B x) x * (B y) y) by
        ring, show s * (r * (B x) y) * (r * (s * (B y) x)) = (r * r * s * s) * ((B x) y * (B y) x)
        by ring] at this
      have hrs : r * r * s * s ≠ 0 := by simp [hr, hs]
      exact le_of_eq <| mul_right_injective₀ hrs this
    simp [show s • y = - r • x by rwa [neg_smul, ← add_eq_zero_iff_eq_neg']]
  · contrapose!
    intro h
    exact not_linearIndependent_of_apply_mul_apply_eq B hp x y (le_antisymm
      (apply_mul_apply_le_of_forall_zero_le B hle x y) h)

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

Goal state before:
pp: case right.mk
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
y✝ : V₁ ⧸ W
x : V₁
⊢ (∀ (x_1 : ↥(dualAnnihilator W)), x_1 x = 0) → x ∈ W

Tactic:
rw [← forall_mem_dualAnnihilator_apply_eq_zero_iff, SetLike.forall]

Goal state after:
case right.mk
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
y✝ : V₁ ⧸ W
x : V₁
⊢ (∀ (x_1 : Dual K V₁) (h : x_1 ∈ dualAnnihilator W), ⟨x_1, h⟩ x = 0) → ∀ φ ∈ dualAnnihilator W, φ x = 0
Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : SmallCategory J
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : J ⥤ C
c₁ : Cofan fun f ↦ F.obj f.fst.1
c₂ : Cofan F.obj
s t : c₁.pt ⟶ c₂.pt
hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), c₁.ι.app { as := f } ≫ s = F.map f.snd ≫ c₂.ι.app { as := f.fst.2 }
ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), c₁.ι.app { as := f } ≫ t = c₂.ι.app { as := f.fst.1 }
i : Cofork s t
j₁ j₂ : J
f : j₁ ⟶ j₂
reassoced :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)) {W : C} {h : c₂.pt ⟶ W},
    c₁.ι.app { as := f } ≫ s ≫ h = F.map f.snd ≫ c₂.ι.app { as := f.fst.2 } ≫ h
⊢ c₁.ι.app { as := ⟨(j₁, j₂), f⟩ } ≫ s ≫ i.π = c₂.ι.app { as := j₁ } ≫ i.π

Tactic:
i.condition,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : SmallCategory J
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : J ⥤ C
c₁ : Cofan fun f ↦ F.obj f.fst.1
c₂ : Cofan F.obj
s t : c₁.pt ⟶ c₂.pt
hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), c₁.ι.app { as := f } ≫ s = F.map f.snd ≫ c₂.ι.app { as := f.fst.2 }
ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), c₁.ι.app { as := f } ≫ t = c₂.ι.app { as := f.fst.1 }
i : Cofork s t
j₁ j₂ : J
f : j₁ ⟶ j₂
reassoced :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)) {W : C} {h : c₂.pt ⟶ W},
    c₁.ι.app { as := f } ≫ s ≫ h = F.map f.snd ≫ c₂.ι.app { as := f.fst.2 } ≫ h
⊢ c₁.ι.app { as := ⟨(j₁, j₂), f⟩ } ≫ t ≫ i.π = c₂.ι.app { as := j₁ } ≫ i.π
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic

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

pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
hf : NormalEpi f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
⊢ (Cocone.precompose (Iso.inv ?refine_1)).obj (CokernelCofork.ofπ f ⋯) ≅ CokernelCofork.ofπ f' ⋯

Tactic:
· exact parallelPair.ext (Iso.refl _) (Arrow.leftFunc.mapIso e)

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
hf : NormalEpi f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
⊢ (Cocone.precompose
          (parallelPair.ext (Iso.refl ((parallelPair g 0).obj WalkingParallelPair.zero)) (Arrow.leftFunc.mapIso e) ⋯
              ⋯).inv).obj
      (CokernelCofork.ofπ f ⋯) ≅
    CokernelCofork.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)
⊢ kernel.ι (prod.lift f g) ≫ f = kernel.ι (prod.lift f g) ≫ prod.lift f g ≫ prod.fst

Tactic:
prod.lift_fst

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)
⊢ kernel.ι (prod.lift f g) ≫ f = kernel.ι (prod.lift f g) ≫ 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 : C
f g : X ⟶ Y
⊢ pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ 𝟙 X =
    pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ prod.lift (𝟙 X) f ≫ prod.fst

Tactic:
prod.lift_fst

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 : C
f g : X ⟶ Y
⊢ pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ 𝟙 X =
    pullback.fst (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g) ≫ 𝟙 X
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ prod.lift a c ≫ σ = prod.lift (prod.lift a c ≫ σ) (prod.lift b d ≫ σ) ≫ prod.fst

Tactic:
prod.lift_fst

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ prod.lift a c ≫ σ = prod.lift a c ≫ σ
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ (prod.lift f g ≫ prod.map h h) ≫ σ = f ≫ h - g ≫ h

Tactic:
prod.lift_map,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ prod.lift (f ≫ h) (g ≫ h) ≫ σ = f ≫ h - g ≫ h
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₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ : IsIso (homologyMap φ)
hφφ' : IsIso (homologyMap (φ ≫ φ'))
⊢ IsIso (homologyMap φ')

Tactic:
rw [homologyMap_comp] at hφφ'

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ : IsIso (homologyMap φ)
hφφ' : IsIso (homologyMap φ ≫ homologyMap φ')
⊢ IsIso (homologyMap φ')
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₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ' : IsIso (homologyMap φ')
hφφ' : IsIso (homologyMap (φ ≫ φ'))
⊢ IsIso (homologyMap φ)

Tactic:
rw [homologyMap_comp] at hφφ'

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ S₃ : ShortComplex C
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : S₃.HasHomology
φ : S₁ ⟶ S₂
φ' : S₂ ⟶ S₃
hφ' : IsIso (homologyMap φ')
hφφ' : IsIso (homologyMap φ ≫ homologyMap φ')
⊢ IsIso (homologyMap φ)
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
⊢ ψ₁.φK ≫ h₂.π = ψ₂.φK ≫ h₂.π

Tactic:
hK

Goal state after:
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
⊢ ψ₂.φK ≫ h₂.π = ψ₂.φK ≫ h₂.π
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
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
hf' : φ.τ₁ ≫ f' = h.f'
⊢ φ.τ₁ ≫ f' ≫ h.π = 0

Tactic:
reassoc_of% hf',

Goal state after:
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
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
hf' : φ.τ₁ ≫ f' = h.f'
⊢ h.f' ≫ h.π = 0
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
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
φQ : h₁.Q ⟶ h₂.Q := h₁.descQ (φ.τ₂ ≫ h₂.p) ⋯
commg' : φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃
φH : h₁.H ⟶ h₂.H := h₂.liftH (h₁.ι ≫ φQ) ⋯
⊢ h₁.p ≫ φQ = φ.τ₂ ≫ h₂.p

Tactic:
simp [φQ]

Goal state after: