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

Goal state before:
pp: case h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ ((fst i₁ i₂ ≫ i₁ ≫ fst f i) ≫ diagonal f) ≫ fst f f =
    (map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) ⋯ ⋯ ≫
        map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst f f

Tactic:
simp [condition_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ ((fst i₁ i₂ ≫ i₁ ≫ fst f i) ≫ diagonal f) ≫ snd f f =
    (map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) ⋯ ⋯ ≫
        map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      snd f f

Tactic:
simp [condition_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g], P g → P (pullback.fst f g)
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
this : HasPullback f g
e : Y' ≅ pullback f g := ⋯.isoPullback
⊢ P g'

Tactic:
← P.cancel_left_of_respectsIso e.inv,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g], P g → P (pullback.fst f g)
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
this : HasPullback f g
e : Y' ≅ pullback f g := ⋯.isoPullback
⊢ P (e.inv ≫ g')
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

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.strictLimitsOfShape J).isoClosure = P.limitsOfShape J

Tactic:
by
  refine le_antisymm ?_ ?_
  · rw [isoClosure_le_iff]
    apply strictLimitsOfShape_le_limitsOfShape
  · intro X ⟨h⟩
    have := h.hasLimit
    exact ⟨limit h.diag, strictLimitsOfShape.limit h.diag h.prop_diag_obj,
      ⟨h.isLimit.conePointUniqueUpToIso (limit.isLimit _)⟩⟩

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

Goal state before:
pp: case refine_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
⊢ (i : Fin n) → f i.succ ⟶ c₂.pt

Tactic:
· intro i
        apply c₁.ι.app ⟨i⟩ ≫ c₂.inr

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

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)
⊢ 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) ⋯) ⋯
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
⊢ ∀ (s : PullbackCone (fst g h) (snd f g)) (m : s.pt ⟶ pullback (fst f g) (fst f h)),
    m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = s.fst →
      m ≫ fst (fst f g) (fst f h) = s.snd → m = lift s.snd (lift (s.snd ≫ fst f g) (s.fst ≫ snd g h) ⋯) ⋯

Tactic:
intro c m hfst hsnd
    refine pullback.hom_ext (by simpa) ?_
    apply pullback.hom_ext <;> simp [← hsnd, pullback.condition, ← hfst]

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
E : Type u₂
inst✝¹ : Category.{v₂, u₂} E
inst✝ : CartesianMonoidalCategory E
G : D ⥤ E
A : C
⊢ prodComparisonNatTrans (F ⋙ G) A =
    Functor.whiskerRight (prodComparisonNatTrans F A) G ≫ F.whiskerLeft (prodComparisonNatTrans G (F.obj A))

Tactic:
ext; simp [prodComparison_comp]

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
E : Type u₂
inst✝¹ : Category.{v₂, u₂} E
inst✝ : CartesianMonoidalCategory E
G : D ⥤ E
⊢ prodComparisonBifunctorNatTrans (F ⋙ G) =
    Functor.whiskerRight (prodComparisonBifunctorNatTrans F) ((Functor.whiskeringRight C D E).obj G) ≫
      F.whiskerLeft (Functor.whiskerRight (prodComparisonBifunctorNatTrans G) ((Functor.whiskeringLeft C D E).obj F))

Tactic:
ext; simp [prodComparison_comp]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : HopfAlgebra R A
inst✝² : HopfAlgebra S B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R S B
⊢ LinearMap.mul' S (B ⊗[R] A) ∘ₗ
      LinearMap.lTensor (B ⊗[R] A) (AlgebraTensorModule.map (antipode S) (antipode R)) ∘ₗ comul =
    Algebra.linearMap S (B ⊗[R] A) ∘ₗ counit

Tactic:
by
    ext x y
    convert! congr($(mul_antipode_lTensor_comul_apply (R := S) x) ⊗ₜ[R]
      $(mul_antipode_lTensor_comul_apply (R := R) y)) using 1
    · dsimp [Algebra.TensorProduct.one_def]
      hopf_tensor_induction comul (R := S) x with x₁ x₂
      hopf_tensor_induction comul (R := R) y with y₁ y₂
      simp
    · dsimp [Algebra.TensorProduct.one_def]
      simp [Algebra.algebraMap_eq_smul_one, smul_tmul']

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
⊢ ∀ (m : s.pt ⟶ (A ⊗ A) ⊗ A),
    m ≫ μ ▷ A = s.fst →
      m ≫ (α_ A A A).hom ≫ A ◁ μ = s.snd →
        m = lift (lift (s.snd ≫ fst A A) (lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ)) (s.fst ≫ snd A A)

Tactic:
m

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
m : s.pt ⟶ (A ⊗ A) ⊗ A
⊢ m ≫ μ ▷ A = s.fst →
    m ≫ (α_ A A A).hom ≫ A ◁ μ = s.snd →
      m = lift (lift (s.snd ≫ fst A A) (lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ)) (s.fst ≫ snd A A)
Module: Mathlib.Logic.Equiv.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : Denumerable α
s : Multiset α
⊢ (fun n ↦ Multiset.map (ofNat α) ↑(raise (ofNat (List ℕ) n) 0))
      ((fun s ↦ encode (lower ((Multiset.map encode s).sort fun a b ↦ a ≤ b) 0)) s) =
    s

Tactic:
have :=
        raise_lower (List.pairwise_cons.2 ⟨fun n _ => Nat.zero_le n,
        (s.map encode).pairwise_sort _⟩).sortedLE
      simp [-Multiset.map_coe, this]

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

Goal state before:
pp: α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
n : ℕ
⊢ ∀ ⦃a₂ : ℕ⦄,
    (fun n ↦
            have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
            this)
          n =
        (fun n ↦
            have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
            this)
          a₂ →
      n = a₂

Tactic:
m

Goal state after:
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
n m : ℕ
⊢ (fun n ↦
          have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
          this)
        n =
      (fun n ↦
          have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
          this)
        m →
    n = m
Module: Mathlib.Data.W.Basic

Goal state before:
pp: α : Type u_1
β : α → Type u_2
inst✝ : (a : α) → Fintype (β a)
t : WType β
⊢ 0 < t.depth

Tactic:
by
  cases t
  apply Nat.succ_pos

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
g : ᘁX ⟶ Z
⊢ 𝟙 ᘁY ⊗≫ η_ (ᘁX) X ▷ ᘁY ⊗≫ ᘁX ◁ f ▷ ᘁY ⊗≫ (g ▷ (Y ⊗ ᘁY) ≫ Z ◁ ε_ (ᘁY) Y) ⊗≫ 𝟙 Z =
    (λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (g ⊗ₘ f) ▷ ᘁY ≫ (α_ Z Y ᘁY).hom ≫ Z ◁ ε_ (ᘁY) Y ≫ (ρ_ Z).hom

Tactic:
tensorHom_def'

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
g : ᘁX ⟶ Z
⊢ 𝟙 ᘁY ⊗≫ η_ (ᘁX) X ▷ ᘁY ⊗≫ ᘁX ◁ f ▷ ᘁY ⊗≫ (g ▷ (Y ⊗ ᘁY) ≫ Z ◁ ε_ (ᘁY) Y) ⊗≫ 𝟙 Z =
    (λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (ᘁX ◁ f ≫ g ▷ Y) ▷ ᘁY ≫ (α_ Z Y ᘁY).hom ≫ Z ◁ ε_ (ᘁY) Y ≫ (ρ_ Z).hom
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ Y Yᘁ ≫ (g ⊗ₘ (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom) =
    𝟙 (𝟙_ C) ⊗≫ (η_ Y Yᘁ ▷ 𝟙_ C ≫ (Y ⊗ Yᘁ) ◁ η_ X Xᘁ) ⊗≫ Y ◁ Yᘁ ◁ f ▷ Xᘁ ⊗≫ Y ◁ ε_ Y Yᘁ ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 (Z ⊗ Xᘁ)

Tactic:
tensorHom_def'

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasRightDual X
inst✝¹ : HasRightDual Y
inst✝ : HasRightDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ Y Yᘁ ≫ Y ◁ ((ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom) ≫ g ▷ Xᘁ =
    𝟙 (𝟙_ C) ⊗≫ (η_ Y Yᘁ ▷ 𝟙_ C ≫ (Y ⊗ Yᘁ) ◁ η_ X Xᘁ) ⊗≫ Y ◁ Yᘁ ◁ f ▷ Xᘁ ⊗≫ Y ◁ ε_ Y Yᘁ ▷ Xᘁ ⊗≫ g ▷ Xᘁ ⊗≫ 𝟙 (Z ⊗ Xᘁ)
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
t : Set M
h₁ : Set.range v ⊆ t
h₂ : #↑t = Module.rank R M
h₃ : LinearIndepOn R _root_.id t
e : Set.range v = t
⊢ ↑n = Module.rank R M

Tactic:
rw [← e, ← lift_injective.eq_iff, mk_range_eq_of_injective hv.injective] at h₂

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₂ : lift.{u, 0} #(Fin n) = lift.{0, u} (Module.rank R M)
h₃ : LinearIndepOn R _root_.id t
e : Set.range v = t
⊢ ↑n = Module.rank R M
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✝ : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
w : V
hw : w ∈ W ⊓ K ∙ v
⊢ w ∈ W ∧ ∃ t, t • v = w

Tactic:
by simpa [mem_span_singleton] using hw

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y ⟶ Z
⊢ (tensorRightHomEquiv (𝟙_ C) Y Y' Z).symm (η_ Y Y' ≫ f ▷ Y') = η_ Y Y' ▷ Y ⊗≫ (f ▷ (Y' ⊗ Y) ≫ Z ◁ ε_ Y Y') ⊗≫ 𝟙 Z

Tactic:
by
      dsimp [tensorRightHomEquiv]; monoidal

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : HasRightDual X
f : Y ⟶ Xᘁ
⊢ (tensorRightHomEquiv Y X Xᘁ (𝟙_ C)) (f ▷ X ≫ ε_ X Xᘁ) = 𝟙 Y ⊗≫ (Y ◁ η_ X Xᘁ ≫ f ▷ (X ⊗ Xᘁ)) ⊗≫ ε_ X Xᘁ ▷ Xᘁ

Tactic:
by
      dsimp [tensorRightHomEquiv]; monoidal

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

Goal state before:
pp: R : Type u_1
M : Type u_5
Mₗ₁ : Type u_9
Mₗ₁' : Type u_10
Mₗ₂ : Type u_11
Mₗ₂' : Type u_12
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid Mₗ₁
inst✝⁶ : AddCommMonoid Mₗ₂
inst✝⁵ : AddCommMonoid Mₗ₁'
inst✝⁴ : AddCommMonoid Mₗ₂'
inst✝³ : Module R Mₗ₁
inst✝² : Module R Mₗ₂
inst✝¹ : Module R Mₗ₁'
inst✝ : Module R Mₗ₂'
B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M
e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁'
e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'
h : ((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M))) B).SeparatingLeft
⊢ B.SeparatingLeft

Tactic:
by
    convert! h.congr e₁.symm e₂.symm
    ext x y
    simp

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W B.ker
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ y ∈ W, (B x) y = 0
u : M
hu : u ∈ W
v : M
hv : v ∈ B.ker
this : (B x) u = 0
⊢ (B x) (u + v) = 0 (u + v)

Tactic:
rw [mem_ker] at hv; simpa [← hB.eq v, hv]

Goal state after:
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
c : Cocone F
⊢ ∀ (m : (coequalizerCocone F).pt ⟶ c.pt),
    (∀ (j : WalkingParallelPair), (coequalizerCocone F).ι.app j ≫ m = c.ι.app j) →
      m = pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯

Tactic:
m

Goal state after:
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
c : Cocone F
m : (coequalizerCocone F).pt ⟶ c.pt
⊢ (∀ (j : WalkingParallelPair), (coequalizerCocone F).ι.app j ≫ m = c.ι.app j) →
    m = pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: case h₀
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
c : Cocone F
m : (coequalizerCocone F).pt ⟶ c.pt
J : ∀ (j : WalkingParallelPair), (coequalizerCocone F).ι.app j ≫ m = c.ι.app j
J1 : pushoutInl F ≫ m = c.ι.app WalkingParallelPair.one
⊢ pushout.inl (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
        (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)) ≫
      m =
    (PushoutCocone.mk (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯).ι.app WalkingSpan.left

Tactic:
exact J1

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

Goal state before:
pp: case h₁
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
c : Cocone F
m : (coequalizerCocone F).pt ⟶ c.pt
J : ∀ (j : WalkingParallelPair), (coequalizerCocone F).ι.app j ≫ m = c.ι.app j
J1 : pushoutInl F ≫ m = c.ι.app WalkingParallelPair.one
⊢ pushoutInl F ≫ m =
    (PushoutCocone.mk (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯).ι.app WalkingSpan.right

Tactic:
exact J1

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

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R M
φ : Dual R M
⊢ (∃ y, W.mkQ.dualMap y = φ) → φ ∈ W.dualAnnihilator

Tactic:
rintro ⟨ψ, rfl⟩
    have := LinearMap.mem_range_self W.mkQ.dualMap ψ
    simpa only [ker_mkQ] using W.mkQ.range_dualMap_le_dualAnnihilator_ker this

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

Goal state before:
pp: case e'_3
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑f.range.subtype.dualMap
rr_surj : Function.Surjective ⇑f.rangeRestrict
this : f.rangeRestrict.dualMap.range = f.rangeRestrict.ker.dualAnnihilator
⊢ f.ker.dualAnnihilator = f.rangeRestrict.ker.dualAnnihilator

Tactic:
apply congr_arg
    exact (ker_rangeRestrict f).symm

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Kernels

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

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

Tactic:
· simpa using! (Function.Exact.apply_apply_eq_zero H x).symm

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

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

Tactic:
← forall_dual_apply_eq_zero_iff K x

Goal state after:
case right
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
x : ↥W
h : ∀ (x_1 : Dual K V₁ ⧸ dualAnnihilator W), ((Submodule.dualPairing W) x_1) x = 0
⊢ ∀ (φ : Dual K ↥W), φ 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 W' : Subspace K V₁
h : IsCompl W W'
⊢ IsCompl (dualAnnihilator W) (dualAnnihilator W')

Tactic:
rw [isCompl_iff, disjoint_iff, codisjoint_iff] at h ⊢

Goal state after:
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
h : W ⊓ W' = ⊥ ∧ W ⊔ W' = ⊤
⊢ dualAnnihilator W ⊓ dualAnnihilator W' = ⊥ ∧ dualAnnihilator W ⊔ dualAnnihilator W' = ⊤
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₂
f : V₁ →ₗ[K] V₂
⊢ Function.Bijective ⇑f.dualMap ↔ Function.Bijective ⇑f

Tactic:
Function.Bijective,

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₂
f : V₁ →ₗ[K] V₂
⊢ Function.Injective ⇑f.dualMap ∧ Function.Surjective ⇑f.dualMap ↔ Function.Injective ⇑f ∧ Function.Surjective ⇑f
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

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

Tactic:
by
  -- Since C is abelian, u := ker g ≫ i is the kernel of some morphism h.
  let u := kernel.ι g ≫ i
  have hu := normalMonoOfMono u
  let h := hu.g
  -- By hypothesis, p factors through the kernel of g via some t.
  obtain ⟨t, ht⟩ := kernel.lift' g p hpg
  have fh : f ≫ h = 0 :=
    calc
      f ≫ h = (p ≫ i) ≫ h := (Abelian.image.fac f).symm ▸ rfl
      _ = ((t ≫ kernel.ι g) ≫ i) ≫ h := ht ▸ rfl
      _ = t ≫ u ≫ h := by simp only [u, Category.assoc]
      _ = t ≫ 0 := hu.w ▸ rfl
      _ = 0 := HasZeroMorphisms.comp_zero _ _
  -- h factors through the cokernel of f via some l.
  obtain ⟨l, hl⟩ := cokernel.desc' f h fh
  have hih : i ≫ h = 0 :=
    calc
      i ≫ h = i ≫ cokernel.π f ≫ l := hl ▸ rfl
      _ = 0 ≫ l := by rw [← Category.assoc, kernel.condition]
      _ = 0 := zero_comp
  -- i factors through u = ker h via some s.
  obtain ⟨s, hs⟩ := NormalMono.lift' u i hih
  have hs' : (s ≫ kernel.ι g) ≫ i = 𝟙 I ≫ i := by rw [Category.assoc, hs, Category.id_comp]
  have : Epi (kernel.ι g) := epi_of_epi_fac ((cancel_mono _).1 hs')
  -- ker g is an epimorphism, but ker g ≫ g = 0 = ker g ≫ 0, so g = 0 as required.
  exact zero_of_epi_comp _ (kernel.condition g)

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

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
s : Fork prod.snd 0
⊢ ∀ (m : s.pt ⟶ (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp).pt),
    m ≫ Fork.ι (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) = s.ι → m = s.ι ≫ prod.fst

Tactic:
m

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
s : Fork prod.snd 0
m : s.pt ⟶ (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp).pt
⊢ m ≫ Fork.ι (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) = s.ι → m = s.ι ≫ prod.fst
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

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

Tactic:
rw [neg_def, neg_def]

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

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

Tactic:
by rw [add_neg, sub_self]

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 : X ⟶ Y
⊢ -(a - b) = -a + b

Tactic:
rw [neg_def, neg_def]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ 0 - (a - b) = 0 - a + b
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f✝ : A ⟶ B
X✝ Y✝ : GrpCat
f : X✝ ⟶ Y✝
e : Mono f
⊢ Mono ((forget GrpCat).map f)

Tactic:
mono_iff_injective,

Goal state after:
A B : GrpCat
f✝ : A ⟶ B
X✝ Y✝ : GrpCat
f : X✝ ⟶ Y✝
e : Function.Injective ⇑(ConcreteCategory.hom f)
⊢ Mono ((forget GrpCat).map f)
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : CommGrpCat
f✝ : A ⟶ B
X✝ Y✝ : CommGrpCat
f : X✝ ⟶ Y✝
e : Mono f
⊢ Mono ((forget CommGrpCat).map f)

Tactic:
mono_iff_injective,

Goal state after:
A B : CommGrpCat
f✝ : A ⟶ B
X✝ Y✝ : CommGrpCat
f : X✝ ⟶ Y✝
e : Function.Injective ⇑(ConcreteCategory.hom f)
⊢ Mono ((forget CommGrpCat).map f)