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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : F.IsEquivalence
inst✝ : MonoidalClosed D
X Y Z : C
⊢ ∀ (f : Y ⟶ (ihom X).obj Z),
    uncurry f =
      (Functor.Monoidal.commTensorLeft F X).compInverseIso.inv.app Y ≫
        (adj.toEquivalence.symm.toAdjunction.homEquiv ((F ⋙ tensorLeft (F.obj X)).obj Y) Z).symm
          (uncurry ((adj.homEquiv Y ((ihom (F.obj X)).obj (adj.toEquivalence.symm.inverse.obj Z))).symm f))

Tactic:
intro f
  -- This whole proof used to be `rfl` before https://github.com/leanprover-community/mathlib4/pull/16317.
  change (((adj.comp ((ihom.adjunction (F.obj X)).comp
      adj.toEquivalence.symm.toAdjunction)).ofNatIsoLeft _).homEquiv _ _).symm _ = _
  rw [Adjunction.homEquiv_ofNatIsoLeft_symm_apply]
  dsimp
  rw [Adjunction.comp_homEquiv, Adjunction.comp_homEquiv]
  rfl

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : HasRankNullity.{u, u_1} R
H : Subsingleton R
this : Module.rank R (PUnit.{u + 1} ⧸ ⊥) + Module.rank R ↥⊥ = Module.rank R PUnit.{u + 1}
⊢ False

Tactic:
simp [one_add_one_eq_two] at this

Goal state after:
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
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₂
p : Subspace K V
q : Subspace K V₂
f₁ : ↥p ≃ₗ[K] ↥q
f₂ : V ≃ₗ[K] V₂
⊢ finrank K (V ⧸ p) = finrank K (V₂ ⧸ q)

Tactic:
← @add_right_cancel_iff _ _ _ (finrank K p),

Goal state after:
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₂
p : Subspace K V
q : Subspace K V₂
f₁ : ↥p ≃ₗ[K] ↥q
f₂ : V ≃ₗ[K] V₂
⊢ finrank K (V ⧸ p) + finrank K ↥p = finrank K (V₂ ⧸ q) + finrank K ↥p
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix

Goal state before:
pp: R : Type u
S : Type u'
M : Type v
N : Type w
inst✝¹² : Ring R
inst✝¹¹ : Ring S
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : Free R M
inst✝⁷ : Module.Finite R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : Module S N
inst✝³ : SMulCommClass R S N
inst✝² : StrongRankCondition R
inst✝¹ : StrongRankCondition S
inst✝ : Free S N
⊢ ↑(finrank R M) * lift.{v, w} (Module.rank S N) = lift.{w, v} (Module.rank R M) * lift.{v, w} (Module.rank S N)

Tactic:
← finrank_eq_rank R,

Goal state after:
R : Type u
S : Type u'
M : Type v
N : Type w
inst✝¹² : Ring R
inst✝¹¹ : Ring S
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : Free R M
inst✝⁷ : Module.Finite R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : Module S N
inst✝³ : SMulCommClass R S N
inst✝² : StrongRankCondition R
inst✝¹ : StrongRankCondition S
inst✝ : Free S N
⊢ ↑(finrank R M) * lift.{v, w} (Module.rank S N) = lift.{w, v} ↑(finrank R M) * lift.{v, w} (Module.rank S N)
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid P
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Projective R M
inst✝ : Module.Finite R M
⊢ ↑(rTensorHomEquivHomRTensor R M P Q) = rTensorHomToHomRTensor (RingHom.id R) M P Q

Tactic:
let e := congr (dualTensorHomEquiv R M P) (LinearEquiv.refl R Q)

Goal state after:
R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid P
inst✝⁵ : AddCommMonoid Q
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Projective R M
inst✝ : Module.Finite R M
e : Dual R M ⊗[R] P ⊗[R] Q ≃ₗ[R] (M →ₗ[R] P) ⊗[R] Q :=
  TensorProduct.congr (dualTensorHomEquiv R M P) (LinearEquiv.refl R Q)
⊢ ↑(rTensorHomEquivHomRTensor R M P Q) = rTensorHomToHomRTensor (RingHom.id R) M P Q
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
⊢ F.map WalkingParallelPairHom.left ≫ pushoutInl F = F.map WalkingParallelPairHom.right ≫ pushoutInl F

Tactic:
conv_rhs => rw [pushoutInl_eq_pushout_inr]
        convert!
          (whisker_eq Limits.coprod.inr pushout.condition :
            (_ : F.obj _ ⟶ constructCoequalizer _) = _) using
          1 <;> simp

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_7
M : Type u_8
N : Type u_9
ι : Type u_10
κ : Type u_11
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ∑ x,
      ∑ x_1, (Finsupp.single x_1 1) j * (Finsupp.single x 1) i * ((Finsupp.single i' 1) x * (Finsupp.single j' 1) x_1) =
    (Finsupp.single j' 1) j * (Finsupp.single i' 1) i

Tactic:
rw [Finset.sum_eq_single i, Finset.sum_eq_single j]

Goal state after:
R : Type u_7
M : Type u_8
N : Type u_9
ι : Type u_10
κ : Type u_11
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ (Finsupp.single j 1) j * (Finsupp.single i 1) i * ((Finsupp.single i' 1) i * (Finsupp.single j' 1) j) =
    (Finsupp.single j' 1) j * (Finsupp.single i' 1) i

case h₀
R : Type u_7
M : Type u_8
N : Type u_9
ι : Type u_10
κ : Type u_11
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ∀ b ∈ Finset.univ,
    b ≠ j → (Finsupp.single b 1) j * (Finsupp.single i 1) i * ((Finsupp.single i' 1) i * (Finsupp.single j' 1) b) = 0

case h₁
R : Type u_7
M : Type u_8
N : Type u_9
ι : Type u_10
κ : Type u_11
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ j ∉ Finset.univ →
    (Finsupp.single j 1) j * (Finsupp.single i 1) i * ((Finsupp.single i' 1) i * (Finsupp.single j' 1) j) = 0

case h₀
R : Type u_7
M : Type u_8
N : Type u_9
ι : Type u_10
κ : Type u_11
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ∀ b ∈ Finset.univ,
    b ≠ i →
      ∑ x, (Finsupp.single x 1) j * (Finsupp.single b 1) i * ((Finsupp.single i' 1) b * (Finsupp.single j' 1) x) = 0

case h₁
R : Type u_7
M : Type u_8
N : Type u_9
ι : Type u_10
κ : Type u_11
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ i ∉ Finset.univ →
    ∑ x, (Finsupp.single x 1) j * (Finsupp.single i 1) i * ((Finsupp.single i' 1) i * (Finsupp.single j' 1) x) = 0
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_7
M : Type u_8
N : Type u_9
ι : Type u_10
κ : Type u_11
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ∑ x, ∑ x_1, ((Finsupp.single x 1) i * (Finsupp.single x_1 1) j) • b.coord x ⊗ₜ[R] c.coord x_1 =
    b.coord i ⊗ₜ[R] c.coord j

Tactic:
rw [Finset.sum_eq_single i, Finset.sum_eq_single j]

Goal state after:
R : Type u_7
M : Type u_8
N : Type u_9
ι : Type u_10
κ : Type u_11
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ((Finsupp.single i 1) i * (Finsupp.single j 1) j) • b.coord i ⊗ₜ[R] c.coord j = b.coord i ⊗ₜ[R] c.coord j

case h₀
R : Type u_7
M : Type u_8
N : Type u_9
ι : Type u_10
κ : Type u_11
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ∀ b_1 ∈ Finset.univ, b_1 ≠ j → ((Finsupp.single i 1) i * (Finsupp.single b_1 1) j) • b.coord i ⊗ₜ[R] c.coord b_1 = 0

case h₁
R : Type u_7
M : Type u_8
N : Type u_9
ι : Type u_10
κ : Type u_11
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ j ∉ Finset.univ → ((Finsupp.single i 1) i * (Finsupp.single j 1) j) • b.coord i ⊗ₜ[R] c.coord j = 0

case h₀
R : Type u_7
M : Type u_8
N : Type u_9
ι : Type u_10
κ : Type u_11
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ∀ b_1 ∈ Finset.univ,
    b_1 ≠ i → ∑ x, ((Finsupp.single b_1 1) i * (Finsupp.single x 1) j) • b.coord b_1 ⊗ₜ[R] c.coord x = 0

case h₁
R : Type u_7
M : Type u_8
N : Type u_9
ι : Type u_10
κ : Type u_11
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ i ∉ Finset.univ → ∑ x, ((Finsupp.single i 1) i * (Finsupp.single x 1) j) • b.coord i ⊗ₜ[R] c.coord x = 0
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
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
⊢ Nondegenerate B ↔ ∀ (x : M), (B x) x = 0 ↔ x = 0

Tactic:
hB.isRefl.nondegenerate_iff_separatingLeft,

Goal state after:
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
hB : IsSymm B
⊢ SeparatingLeft B ↔ ∀ (x : M), (B x) x = 0 ↔ x = 0
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:
rw [comp_apply, mkQ_apply, (Quotient.mk_eq_zero W).mpr hw, φ.map_zero]

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

Goal state before:
pp: case neg
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ¬FiniteDimensional K V
⊢ finrank K (Dual K V) = finrank K V

Tactic:
finrank_eq_zero_of_basis_imp_false,

Goal state after:
case neg
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ¬FiniteDimensional K V
⊢ 0 = finrank K V

case neg
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ¬FiniteDimensional K V
⊢ ∀ (s : Finset (Dual K V)) (a : Basis (↑↑s) K (Dual K V)), False
Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
this : HasFiniteLimits C
⊢ PreservesFiniteLimits G

Tactic:
have : PreservesLimitsOfShape (Discrete WalkingPair) G :=
    preservesBinaryProducts_of_preservesTerminal_and_pullbacks G

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
this✝ : HasFiniteLimits C
this : PreservesLimitsOfShape (Discrete WalkingPair) G
⊢ PreservesFiniteLimits G
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 : X ⟶ Y
Z : C
l : IsColimit (CokernelCofork.ofπ 0 ⋯)
Z✝ : C
u v : Y ⟶ Z✝
huv : f ≫ u = f ≫ v
W : C
w : Y ⟶ W
hw : equalizer.ι u v ≫ w = 0
hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)
m : X ⟶ equalizer u v
hm : m ≫ equalizer.ι u v = f
⊢ m ≫ equalizer.ι u v ≫ w = 0

Tactic:
hw,

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 : X ⟶ Y
Z : C
l : IsColimit (CokernelCofork.ofπ 0 ⋯)
Z✝ : C
u v : Y ⟶ Z✝
huv : f ≫ u = f ≫ v
W : C
w : Y ⟶ W
hw : equalizer.ι u v ≫ w = 0
hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)
m : X ⟶ equalizer u v
hm : m ≫ equalizer.ι u v = f
⊢ m ≫ 0 = 0
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hl : IsLimit (KernelFork.ofι (diag A) ⋯) :=
  monoIsKernelOfCokernel (colimit.cocone (parallelPair (diag A) 0)) (colimit.isColimit (parallelPair (diag A) 0))
Z : C
x : Z ⟶ A
hx : x ≫ r A = 0
hxx : (x ≫ prod.lift (𝟙 A) 0) ≫ cokernel.π (diag A) = 0
y : Z ⟶ (KernelFork.ofι (diag A) ⋯).pt
hy : y ≫ diag A = x ≫ prod.lift (𝟙 A) 0
⊢ y = 0

Tactic:
erw [← Category.comp_id y, ← Limits.prod.lift_snd (𝟙 A) (𝟙 A), ← Category.assoc, hy,
      Category.assoc, prod.lift_snd, HasZeroMorphisms.comp_zero]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c : X ⟶ Y
⊢ a - (-b - c) = a + (b + c)

Tactic:
← add_neg,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c : X ⟶ Y
⊢ a + -(-b - c) = a + (b + c)
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
⊢ f ≫ coimage.π g = 0 ↔ f ≫ g = 0

Tactic:
by
  simp [← cancel_mono (Abelian.factorThruCoimage _)]

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

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
a : ↑A
x✝ : X'
⊢ (ConcreteCategory.hom f) a ∈ {b | h b = g b}

Tactic:
rw [← agree]

Goal state after:
A B : GrpCat
f : A ⟶ B
a : ↑A
x✝ : X'
⊢ (ConcreteCategory.hom f) a ∈ ↑(Hom.hom f).range
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u_1
inst✝² : Category.{?u.4, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteProducts C
h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), Nonempty (AbelianStruct f)
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
hf : AbelianStruct f
⊢ Fork.ι hf.kernelFork = 0

Tactic:
simp [← cancel_mono f]

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 S₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁✝ : S₁.HomologyData
h₂✝ : S₂.HomologyData
inst✝ : S.HasHomology
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ IsIso (leftRightHomologyComparison' h₁ h₂)

Tactic:
rw [leftRightHomologyComparison'_compatibility h₁ S.homologyData.left h₂
    S.homologyData.right]
  infer_instance

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₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ rightHomologyMap' φ h₁ h₂ = h₁.homologyIso.inv ≫ homologyMap φ ≫ h₂.homologyIso.hom

Tactic:
← cancel_epi (leftRightHomologyComparison' S₁.leftHomologyData h₁),

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
⊢ leftRightHomologyComparison' S₁.leftHomologyData h₁ ≫ rightHomologyMap' φ h₁ h₂ =
    leftRightHomologyComparison' S₁.leftHomologyData h₁ ≫ h₁.homologyIso.inv ≫ homologyMap φ ≫ h₂.homologyIso.hom
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
S S₁ S₂ : ShortComplex C
h : S.LeftHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
this✝ : PreservesLimit (parallelPair S.g 0) F
this : PreservesColimit (parallelPair h.f' 0) F
wi : F.map h.i ≫ F.map S.g = 0
hi : IsLimit ((KernelFork.ofι h.i ⋯).map F)
f' : F.obj S.X₁ ⟶ F.obj h.K := hi.lift (KernelFork.ofι (S.map F).f ⋯)
hf' : f' = F.map h.f'
wπ : f' ≫ F.map h.π = 0
hπ : IsColimit (CokernelCofork.ofπ (F.map h.π) wπ)
⊢ (S.map F).LeftHomologyData

Tactic:
exact
    { K := F.obj h.K
      H := F.obj h.H
      i := F.map h.i
      π := F.map h.π
      wi := wi
      hi := hi
      wπ := wπ
      hπ := hπ }

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : HasZeroMorphisms C
inst✝⁵ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasRightHomology
inst✝² : S₂.HasRightHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ F.map (opcyclesMap φ) ≫ (S₂.mapOpcyclesIso F).inv = (S₁.mapOpcyclesIso F).inv ≫ opcyclesMap (F.mapShortComplex.map φ)

Tactic:
rw [← cancel_epi (S₁.mapOpcyclesIso F).hom, ← mapOpcyclesIso_hom_naturality_assoc,
    Iso.hom_inv_id, comp_id, Iso.hom_inv_id_assoc]

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
inst✝¹ : IsIso φ.τ₁
inst✝ : IsIso φ.τ₃
this : Mono S₁.f
⊢ IsIso φ.τ₂

Tactic:
have := h₂.mono_f

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
inst✝¹ : IsIso φ.τ₁
inst✝ : IsIso φ.τ₃
this✝ : Mono S₁.f
this : Mono S₂.f
⊢ IsIso φ.τ₂
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hf : S.f = 0
this : S.HasHomology
⊢ Mono S.g

Tactic:
have := hS.epi_toCycles

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hf : S.f = 0
this✝ : S.HasHomology
this : Epi S.toCycles
⊢ Mono S.g
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : IsZero S.X₂
⊢ S.f = 0 ∧ S.g = 0

Tactic:
exact ⟨h.eq_of_tgt _ _, h.eq_of_src _ _⟩

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
B A₁ A₂ : C
f : A₁ ⟶ B
g : A₂ ⟶ B
inst✝¹ : Mono f
inst✝ : Mono g
h : mk f ≤ mk g
⊢ ofMkLEMk f g h ≫ g = f

Tactic:
simp [ofMkLEMk]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝² : Mono f
A✝¹ : C
f✝¹ : A✝¹ ⟶ X
inst✝¹ : Mono f✝¹
A✝ : C
f✝ : A✝ ⟶ X
inst✝ : Mono f✝
h : mk (f✝¹ ≫ f) = mk (f✝ ≫ f)
⊢ (isoOfMkEqMk (f✝¹ ≫ f) (f✝ ≫ f) h).hom ≫ f✝ = f✝¹

Tactic:
simp [← cancel_mono f]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Abelian C
S : ShortComplex C
hS : S.Exact
P : C
f : P ⟶ S.X₂
inst✝ : Projective P
hf : f ≫ S.g = 0
⊢ P ⟶ S.X₁

Tactic:
have := hS.epi_toCycles

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Abelian C
S : ShortComplex C
hS : S.Exact
P : C
f : P ⟶ S.X₂
inst✝ : Projective P
hf : f ≫ S.g = 0
this : Epi S.toCycles
⊢ P ⟶ S.X₁
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X Y Z✝ : C
inst✝³ : HasZeroMorphisms C
f✝ : X ⟶ Y
inst✝² : HasKernel f✝
f : X ⟶ Y
inst✝¹ : HasKernel f
Z : C
h : Y ⟶ Z
inst✝ : Mono h
⊢ IsIso ((kernelSubobject f).ofLE (kernelSubobject (f ≫ h)) ⋯)

Tactic:
rw [ofLE_mk_le_mk_of_comm (kernelCompMono f h).inv]
  · infer_instance
  · simp

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

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesMonomorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
⊢ 𝟙 (L.obj S.X₂) ≫ L.map S.g = L.map (cokernel.π (kernel.ι S.g)) ≫ L.map (Abelian.factorThruCoimage S.g)

Tactic:
rw [Category.id_comp, ← L.map_comp, cokernel.π_desc]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c : Cofan Z
f : Fan fun x ↦ op (Z x)
hc : IsColimit c
hf : IsLimit f
c' : Cofan Z
⊢ (hc.desc c').op ≫ (opCoproductIsoProduct' hc hf).hom = hf.lift c'.op

Tactic:
refine (Iso.eq_comp_inv _).mp (Quiver.Hom.unop_inj (hc.hom_ext (fun ⟨j⟩ ↦ Quiver.Hom.op_inj ?_)))
  simp only [unop_op, Discrete.functor_obj, Quiver.Hom.unop_op, IsColimit.fac,
    Cofan.op, unop_comp, op_comp, op_unop, Quiver.Hom.op_unop, Category.assoc]
  erw [opCoproductIsoProduct'_inv_comp_inj, IsLimit.fac]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
inst✝ : F'.IsLeftKanExtension α
c : Cocone F
hc : IsColimit c
s : Cocone F'
m : (F'.coconeOfIsLeftKanExtension α c).pt ⟶ s.pt
hm : ∀ (j : D), (F'.coconeOfIsLeftKanExtension α c).ι.app j ≫ m = s.ι.app j
j : C
⊢ c.ι.app j ≫ m = c.ι.app j ≫ hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι }

Tactic:
have := hm (L.obj j)

Goal state after:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
inst✝ : F'.IsLeftKanExtension α
c : Cocone F
hc : IsColimit c
s : Cocone F'
m : (F'.coconeOfIsLeftKanExtension α c).pt ⟶ s.pt
hm : ∀ (j : D), (F'.coconeOfIsLeftKanExtension α c).ι.app j ≫ m = s.ι.app j
j : C
this : (F'.coconeOfIsLeftKanExtension α c).ι.app (L.obj j) ≫ m = s.ι.app (L.obj j)
⊢ c.ι.app j ≫ m = c.ι.app j ≫ hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι }