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

Goal state before:
pp: case refine_4
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (fst g h) (snd f g)
m : c.pt ⟶ pullback (fst f g) (fst f h)
hfst : m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = c.fst
⊢ m ≫ fst (fst f g) (fst f h) = c.snd → m = lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯

Tactic:
hsnd

Goal state after:
case refine_4
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (fst g h) (snd f g)
m : c.pt ⟶ pullback (fst f g) (fst f h)
hfst : m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = c.fst
hsnd : m ≫ fst (fst f g) (fst f h) = c.snd
⊢ m = lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯
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
X : C
⊢ P.colimitsOfShape J X ↔ (P.op.limitsOfShape Jᵒᵖ).unop X

Tactic:
refine ⟨fun ⟨h⟩ => ⟨?_⟩, fun ⟨h⟩ => ⟨?_⟩⟩

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
X : C
x✝ : P.colimitsOfShape J X
h : P.ColimitOfShape J X
⊢ P.op.LimitOfShape Jᵒᵖ (Opposite.op X)

case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
X : C
x✝ : (P.op.limitsOfShape Jᵒᵖ).unop X
h : P.op.LimitOfShape Jᵒᵖ (Opposite.op X)
⊢ P.ColimitOfShape J X
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
X : C
⊢ P.limitsOfShape J X ↔ (P.op.colimitsOfShape Jᵒᵖ).unop X

Tactic:
refine ⟨fun ⟨h⟩ => ⟨?_⟩, fun ⟨h⟩ => ⟨?_⟩⟩

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
X : C
x✝ : P.limitsOfShape J X
h : P.LimitOfShape J X
⊢ P.op.ColimitOfShape Jᵒᵖ (Opposite.op X)

case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
X : C
x✝ : (P.op.colimitsOfShape Jᵒᵖ).unop X
h : P.op.ColimitOfShape Jᵒᵖ (Opposite.op X)
⊢ P.LimitOfShape J X
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
X Y : C
g : X ⟶ Y
H : ∀ {T : C} (f : T ⟶ Y) [inst : HasPullback f g], P (pullback.fst f g)
X' Y' : C
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ g
this : HasPullback i₂ g
⊢ P f'

Tactic:
rw [← h.isoPullback_hom_fst, P.cancel_left_of_respectsIso]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
X Y : C
g : X ⟶ Y
H : ∀ {T : C} (f : T ⟶ Y) [inst : HasPullback f g], P (pullback.fst f g)
X' Y' : C
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
h : IsPullback f' i₁ i₂ g
this : HasPullback i₂ g
⊢ P (pullback.fst i₂ g)
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
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
E : Type u₂
inst✝² : Category.{v₂, u₂} E
inst✝¹ : CartesianMonoidalCategory E
G : D ⥤ E
inst✝ : PreservesLimit (Functor.empty C) F
⊢ IsIso (terminalComparison F)

Tactic:
rw [← preservesTerminalIso_hom]
  infer_instance

Goal state after:
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
this : lift (𝟙 A) ι ≫ μ ≫ f = (toUnit A ≫ η) ≫ f
⊢ lift f (ι ≫ f) ≫ μ = toUnit A ≫ η

Tactic:
IsMonHom.mul_hom,

Goal state after:
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
this : lift (𝟙 A) ι ≫ (f ⊗ₘ f) ≫ μ = (toUnit A ≫ η) ≫ f
⊢ lift f (ι ≫ f) ≫ μ = toUnit A ≫ η
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
this : lift ι (𝟙 A) ≫ μ ≫ f = (toUnit A ≫ η) ≫ f
⊢ lift (ι ≫ f) f ≫ μ = toUnit A ≫ η

Tactic:
IsMonHom.mul_hom,

Goal state after:
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
this : lift ι (𝟙 A) ≫ (f ⊗ₘ f) ≫ μ = (toUnit A ≫ η) ≫ f
⊢ lift (ι ≫ f) f ≫ μ = toUnit A ≫ η
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
this : mul' R (C ⊗[R] C) ∘ₗ (δ ⊗ₘ δ) = δ ∘ₗ mul' R C
⊢ mul' R (C ⊗[R] C) ∘ₗ (δ ⊗ₘ δ) ∘ₗ (id ⊗ₘ antipode R) ∘ₗ δ = δ ∘ₗ mul' R C ∘ₗ (id ⊗ₘ antipode R) ∘ₗ δ

Tactic:
simp [this, ← comp_assoc]

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

Goal state before:
pp: case inr
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
i j : ι
hne : i ≠ j
⊢ (h.basis.repr (e i)) j = (Finsupp.single i 1) j

Tactic:
· simp [hne, h.eval_of_ne hne.symm]

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
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
x : M ⧸ span R s
hxt : x ∈ t
hxs : sec x ∈ s
⊢ (span R s).mkQ (sec x) = 0

Tactic:
mkQ_apply,

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
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
x : M ⧸ span R s
hxt : x ∈ t
hxs : sec x ∈ s
⊢ Submodule.Quotient.mk (sec x) = 0
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
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
this : Module.rank R (M ⧸ N) ≠ 0
⊢ ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N

Tactic:
rw [ne_eq, rank_eq_zero_iff, (Submodule.Quotient.mk_surjective N).forall] at this

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
N : Submodule R M
h : Module.rank R ↥N < Module.rank R M
this : ¬∀ (x : M), ∃ a, a ≠ 0 ∧ a • Quotient.mk x = 0
⊢ ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N
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) = 1 → m ≤ n) ↔
    ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), g * f = 1 → m ≤ n

Tactic:
Module.End.one_eq_id,

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) = 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
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
inst✝ : Module.Finite R M
N : Submodule R M
⊢ finrank R (M ⧸ N) + finrank R ↥N = finrank R M

Tactic:
rw [← Nat.cast_inj (R := Cardinal), Module.finrank_eq_rank, Nat.cast_add, Module.finrank_eq_rank,
    Submodule.finrank_eq_rank]

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
inst✝ : Module.Finite R M
N : Submodule R M
⊢ Module.rank R (M ⧸ N) + Module.rank R ↥N = Module.rank R M
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
x✝ : ∃ φ, φ (Submodule.Quotient.mk v) ≠ 0
φ : Dual K (V ⧸ W)
hφ : φ (Submodule.Quotient.mk v) ≠ 0
w : V
hw : w ∈ W
⊢ φ ((mkQ W) w) = 0

Tactic:
mkQ_apply,

Goal state after:
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
x✝ : ∃ φ, φ (Submodule.Quotient.mk v) ≠ 0
φ : Dual K (V ⧸ W)
hφ : φ (Submodule.Quotient.mk v) ≠ 0
w : V
hw : w ∈ W
⊢ φ (Submodule.Quotient.mk w) = 0
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case left
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ (Submodule.dualPairing W).SeparatingLeft

Tactic:
LinearMap.separatingLeft_iff_ker_eq_bot,

Goal state after:
case left
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ (Submodule.dualPairing W).ker = ⊥
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: case left
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ (dualCopairing W).SeparatingLeft

Tactic:
LinearMap.separatingLeft_iff_ker_eq_bot,

Goal state after:
case left
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ (dualCopairing W).ker = ⊥
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:
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.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✝ : FiniteDimensional K V₁
⊢ Surjective ⇑B ∧ Surjective ⇑B.flip ↔ Injective ⇑B ∧ Surjective ⇑B

Tactic:
flip_surjective_iff₁,

Goal state after:
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✝ : FiniteDimensional K V₁
⊢ Surjective ⇑B ∧ Injective ⇑B ↔ Injective ⇑B ∧ Surjective ⇑B
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
inst✝ : IsNormalMonoCategory C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
⊢ IsRegularMono f

Tactic:
have := normalMonoOfMono f

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y : C
inst✝¹ : HasZeroMorphisms C
inst✝ : IsNormalMonoCategory C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
this : NormalMono f
⊢ IsRegularMono f
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
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
reassoc' : ∀ {W : C} (h' : R ⟶ W), NormalEpi.g ≫ g ≫ h' = 0 ≫ h'
⊢ NormalEpi.g ≫ f ≫ h = 0

Tactic:
comm,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasZeroMorphisms C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
reassoc' : ∀ {W : C} (h' : R ⟶ W), NormalEpi.g ≫ g ≫ h' = 0 ≫ h'
⊢ NormalEpi.g ≫ g ≫ k = 0
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ pullback.lift (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ pullback.snd f g = s.ι ≫ biprod.snd

Tactic:
pullback.lift_snd

Goal state after:
case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
s : Fork (biprod.desc f (-g)) 0
⊢ s.ι ≫ biprod.snd = s.ι ≫ biprod.snd
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
R : C
e : Y ⟶ R
h : pullback.snd f g ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc 0 e
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this✝¹ : IsColimit (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc 0 e
this✝ : f ≫ d = 0
this : d = 0
⊢ e = biprod.inr ≫ biprod.desc 0 e

Tactic:
by rw [biprod.inr_desc]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst f g ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this : IsColimit (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc e 0
⊢ (-g) ≫ d = (biprod.inr ≫ biprod.desc f (-g)) ≫ d

Tactic:
by rw [biprod.inr_desc]

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

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
b b' : ↑B
x : X'
y : ↑X
⊢ fromCoset ⟨(b * b') • ↑y, ⋯⟩ = fromCoset ⟨b • ↑⟨b' • ↑y, ⋯⟩, ⋯⟩

Tactic:
simp only [leftCoset_assoc]

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

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
x : ↑B
hx : x ∈ (Hom.hom f).range
⊢ τ ((g x) ((Equiv.symm τ) ∞)) = ∞

Tactic:
rw [τ_symm_apply_infinity, g_apply_fromCoset]

Goal state after:
A B : GrpCat
f : A ⟶ B
x : ↑B
hx : x ∈ (Hom.hom f).range
⊢ τ (fromCoset ⟨x • ↑⟨↑(Hom.hom f).range, ⋯⟩, ⋯⟩) = ∞
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: case neg
A B : GrpCat
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∉ (Hom.hom f).range
⊢ fromCoset ⟨((ConcreteCategory.hom f) a * y) • ↑(Hom.hom f).range, ⋯⟩ =
    fromCoset ⟨(ConcreteCategory.hom f) a • ↑⟨(fun x ↦ x • ↑(Hom.hom f).range) y, ⋯⟩, ⋯⟩

Tactic:
simp only [leftCoset_assoc]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl f g = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this : IsLimit (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift e 0
⊢ e = 0

Tactic:
have : d ≫ (-g) = 0 := calc
      d ≫ (-g) = d ≫ biprod.lift f (-g) ≫ biprod.snd := by rw [biprod.lift_snd]
      _ = biprod.lift e (0 : R ⟶ Z) ≫ biprod.snd := by rw [← Category.assoc, hd]
      _ = 0 := biprod.lift_snd _ _

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl f g = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
hu : u ≫ BiproductToPushoutIsCokernel.biproductToPushout f g = 0
this✝ : IsLimit (KernelFork.ofι (biprod.lift f (-g)) ⋯)
d : R ⟶ X
hd : d ≫ biprod.lift f (-g) = biprod.lift e 0
this : d ≫ (-g) = 0
⊢ e = 0
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:
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.RightHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
hg : S.g = 0
⊢ h.p ≫ 𝟙 h.Q ≫ h.g' = h.p ≫ 0

Tactic:
id_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
hg : S.g = 0
⊢ h.p ≫ h.g' = h.p ≫ 0
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
h : S.LeftHomologyData
A : C
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
⊢ 𝟙 S.X₂ ≫ S.g = 0

Tactic:
id_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.LeftHomologyData
A : C
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
⊢ S.g = 0
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
h : S.LeftHomologyData
A : C
hf : S.f = 0
hg : S.g = 0
⊢ 𝟙 S.X₂ ≫ S.g = 0

Tactic:
id_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.LeftHomologyData
A : C
hf : S.f = 0
hg : S.g = 0
⊢ S.g = 0
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₂
⊢ ψ₁.φK ≫ h₂.i = ψ₂.φK ≫ h₂.i

Tactic:
commi,

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₂
⊢ h₁.i ≫ φ.τ₂ = ψ₂.φK ≫ h₂.i
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
⊢ leftHomologyMap φ = leftHomologyMap' (𝟙 S₁ ≫ φ ≫ 𝟙 S₂) S₁.leftHomologyData S₂.leftHomologyData

Tactic:
id_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₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ leftHomologyMap φ = leftHomologyMap' (φ ≫ 𝟙 S₂) S₁.leftHomologyData 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₂) S₁.leftHomologyData S₂.leftHomologyData

Tactic:
id_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₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ cyclesMap φ = cyclesMap' (φ ≫ 𝟙 S₂) S₁.leftHomologyData S₂.leftHomologyData
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₂) S₁.rightHomologyData S₂.rightHomologyData

Tactic:
id_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 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
⊢ opcyclesMap φ = opcyclesMap' (𝟙 S₁ ≫ φ ≫ 𝟙 S₂) S₁.rightHomologyData S₂.rightHomologyData

Tactic:
id_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
⊢ opcyclesMap φ = opcyclesMap' (φ ≫ 𝟙 S₂) S₁.rightHomologyData S₂.rightHomologyData
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h₁ : IsIso (opcyclesMap φ)
h₂ : Mono φ.τ₃
h : (S₂.homologyι ≫ inv (opcyclesMap φ)) ≫ S₁.fromOpcycles = 0
z : S₂.homology ⟶ (KernelFork.ofι S₁.homologyι ⋯).pt
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
⊢ (homologyMap φ ≫ z) ≫ S₁.homologyι = 𝟙 S₁.homology ≫ S₁.homologyι

Tactic:
id_comp,

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h₁ : IsIso (opcyclesMap φ)
h₂ : Mono φ.τ₃
h : (S₂.homologyι ≫ inv (opcyclesMap φ)) ≫ S₁.fromOpcycles = 0
z : S₂.homology ⟶ (KernelFork.ofι S₁.homologyι ⋯).pt
hz : z ≫ S₁.homologyι = S₂.homologyι ≫ inv (opcyclesMap φ)
⊢ (homologyMap φ ≫ z) ≫ S₁.homologyι = S₁.homologyι
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a : S₁ ⟶ S₂
⊢ (0 + a).τ₁ = a.τ₁

Tactic:
apply zero_add

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

Goal state before:
pp: case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a : S₁ ⟶ S₂
⊢ (0 + a).τ₂ = a.τ₂

Tactic:
apply zero_add

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

Goal state before:
pp: case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
a : S₁ ⟶ S₂
⊢ (0 + a).τ₃ = a.τ₃

Tactic:
apply zero_add

Goal state after: