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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X B : C
f : X ⟶ B
inst✝¹ : HasPullback f f
inst✝ : Epi f
h : ∀ ⦃Z : C⦄ ⦃g : X ⟶ Z⦄, pullback.fst f f ≫ g = pullback.snd f f ≫ g → ∃ u, f ≫ u = g
s : Cofork (pullback.fst f f) (pullback.snd f f)
g : B ⟶ s.pt
hg : f ≫ g = s.π
m✝ : (Cofork.ofπ f ⋯).pt ⟶ s.pt
hm : (Cofork.ofπ f ⋯).π ≫ m✝ = s.π
⊢ m✝ = g

Tactic:
← cancel_epi f,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X B : C
f : X ⟶ B
inst✝¹ : HasPullback f f
inst✝ : Epi f
h : ∀ ⦃Z : C⦄ ⦃g : X ⟶ Z⦄, pullback.fst f f ≫ g = pullback.snd f f ≫ g → ∃ u, f ≫ u = g
s : Cofork (pullback.fst f f) (pullback.snd f f)
g : B ⟶ s.pt
hg : f ≫ g = s.π
m✝ : (Cofork.ofπ f ⋯).pt ⟶ s.pt
hm : (Cofork.ofπ f ⋯).π ≫ m✝ = s.π
⊢ f ≫ m✝ = f ≫ g
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case pos
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
h : ∀ (d : C), ¬P d → IsConnected (CostructuredArrow P.ι d)
d : C
hd : P d
⊢ IsConnected (CostructuredArrow P.ι d)

pp: case neg
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
h : ∀ (d : C), ¬P d → IsConnected (CostructuredArrow P.ι d)
d : C
hd : ¬P d
⊢ IsConnected (CostructuredArrow P.ι d)

Tactic:
· have : Nonempty (CostructuredArrow P.ι d) := ⟨⟨d, hd⟩, ⟨⟨⟩⟩, 𝟙 _⟩
    refine zigzag_isConnected (fun j₁ j₂ ↦ Zigzag.trans
      (j₂ := by exact CostructuredArrow.mk (Y := ⟨d, hd⟩) (𝟙 _)) (.of_hom ?_) (.of_inv ?_))
    · exact CostructuredArrow.homMk (InducedCategory.homMk j₁.hom)
    · exact CostructuredArrow.homMk (InducedCategory.homMk j₂.hom)

Goal state after:
case neg
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
h : ∀ (d : C), ¬P d → IsConnected (CostructuredArrow P.ι d)
d : C
hd : ¬P d
⊢ IsConnected (CostructuredArrow P.ι d)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝² : HasPushout g₁ g₂
inst✝¹ : HasPushout g₃ g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ IsColimit
    (PushoutCocone.mk
      (pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯)
      (pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯)

Tactic:
by
  apply rightSquareIsPushout _ rfl (pushoutIsPushout _ _)
  simpa [PushoutCocone.pasteHoriz] using PushoutCocone.mkSelfIsColimit (pushoutIsPushout _ _)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : ∀ (X : C), ∃ A B p, ∃ (_ : P p), ∃ x, IsIso p
⊢ isomorphisms C ≤ P.pushouts

Tactic:
by
  intro X Y f (_ : IsIso f)
  obtain ⟨A, B, p, hp, g, _⟩ := h X
  exact ⟨A, B, p, p ≫ g, g ≫ f, hp, (IsPushout.of_id_snd (f := p ≫ g)).of_iso
    (Iso.refl _) (Iso.refl _) (asIso p) (asIso f) (by simp) (by simp) (by simp) (by simp)⟩

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₁ : Fan fun i ↦ f i.succ
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
x✝ : Discrete (Fin (n + 1))
j : Fin (n + 1)
i : Fin n
⊢ ↑(BinaryFan.IsLimit.lift' t₂ (s.π.app { as := 0 })
          (t₁.lift
            { pt := s.pt,
              π :=
                Discrete.natTrans fun x ↦
                  match x with
                  | { as := i } => s.π.app { as := i.succ } })) ≫
      (extendFan c₁ c₂).π.app { as := i.succ } =
    s.π.app { as := i.succ }

Tactic:
dsimp only [extendFan_π_app]

Goal state after:
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₁ : Fan fun i ↦ f i.succ
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
x✝ : Discrete (Fin (n + 1))
j : Fin (n + 1)
i : Fin n
⊢ ↑(BinaryFan.IsLimit.lift' t₂ (s.π.app { as := 0 })
          (t₁.lift { pt := s.pt, π := Discrete.natTrans fun x ↦ s.π.app { as := x.as.succ } })) ≫
      Fin.cases c₂.fst (fun i ↦ c₂.snd ≫ c₁.π.app { as := i }) i.succ =
    s.π.app { as := i.succ }
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.IsStableUnderCobaseChange
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Epi f
hcomp : P (f ≫ g)
⊢ g ≫ pushout.inl (f ≫ g) f = pushout.inr (f ≫ g) f

Tactic:
← cancel_epi f,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.IsStableUnderCobaseChange
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Epi f
hcomp : P (f ≫ g)
⊢ f ≫ g ≫ pushout.inl (f ≫ g) f = f ≫ pushout.inr (f ≫ g) f
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: case h₂
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₁ : Fan fun i ↦ f i.succ
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
m : s.pt ⟶ (extendFan c₁ c₂).pt
w : ∀ (j : Discrete (Fin (n + 1))), m ≫ (extendFan c₁ c₂).π.app j = s.π.app j
j : Fin n
⊢ m ≫ c₂.snd ≫ c₁.π.app { as := j } = m ≫ (extendFan c₁ c₂).π.app { as := j.succ }

Tactic:
dsimp only [extendFan_π_app]

Goal state after:
case h₂
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₁ : Fan fun i ↦ f i.succ
c₂ : BinaryFan (f 0) c₁.pt
t₁ : IsLimit c₁
t₂ : IsLimit c₂
s : Cone (Discrete.functor f)
m : s.pt ⟶ (extendFan c₁ c₂).pt
w : ∀ (j : Discrete (Fin (n + 1))), m ≫ (extendFan c₁ c₂).π.app j = s.π.app j
j : Fin n
⊢ m ≫ c₂.snd ≫ c₁.π.app { as := j } = m ≫ Fin.cases c₂.fst (fun i ↦ c₂.snd ≫ c₁.π.app { as := i }) j.succ
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

Goal state before:
pp: 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
⊢ (P.strictLimitsOfShape J).isoClosure ≤ P.limitsOfShape J

Tactic:
rw [isoClosure_le_iff]
    apply strictLimitsOfShape_le_limitsOfShape

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

Goal state before:
pp: case w₂.h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := ⋯
e : pullback (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) := ⋯
⊢ ((e ≪≫ pullbackDiagonalMapIdIso g (𝟙 X) f ≪≫ asIso (fst g (𝟙 X))).symm.hom ≫
        snd (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)) ≫
      fst (g ≫ f) f =
    lift (𝟙 Y) g ⋯ ≫ fst (g ≫ f) f

Tactic:
simp [e, i]

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
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := ⋯
e : pullback (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) := ⋯
⊢ ((e ≪≫ pullbackDiagonalMapIdIso g (𝟙 X) f ≪≫ asIso (fst g (𝟙 X))).symm.hom ≫
        snd (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)) ≫
      snd (g ≫ f) f =
    lift (𝟙 Y) g ⋯ ≫ snd (g ≫ f) f

Tactic:
simp [e, i]

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

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
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
inst✝ : P.IsClosedUnderLimitsOfShape J
⊢ P.op.IsClosedUnderColimitsOfShape Jᵒᵖ

Tactic:
by
  rwa [← isClosedUnderLimitsOfShape_iff_op]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : MonObj B
f : A ⟶ 𝟙_ C
g : A ⟶ B
this : lift f g ≫ η ▷ B ≫ μ = lift f g ≫ (λ_ B).hom
⊢ lift (f ≫ η) g ≫ μ = g

Tactic:
rwa [lift_whiskerRight_assoc, lift_leftUnitor_hom] at this

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
A B : C
inst✝ : MonObj B
f : A ⟶ 𝟙_ C
g : A ⟶ B
⊢ lift (f ≫ η) g ≫ μ = g

Tactic:
by
  have := lift f g ≫= one_mul B
  rwa [lift_whiskerRight_assoc, lift_leftUnitor_hom] at this

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f : X ⟶ M
⊢ 1 * f = f

Tactic:
change lift (toUnit _ ≫ η) f ≫ μ = f
    rw [← Category.comp_id f, ← lift_map_assoc, tensorHom_id, MonObj.one_mul,
      Category.comp_id, leftUnitor_hom]
    exact lift_snd _ _

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝² : MonObj M✝
inst✝¹ : MonObj N✝
inst✝ : MonObj O
M N : Mon C
α : yonedaMonObj M.X ⟶ yonedaMonObj N.X
⊢ (ConcreteCategory.hom (α.app (op (𝟙_ C)))) (𝟙 (𝟙_ C) ≫ η) = η

Tactic:
toUnit_unique (𝟙 _) (toUnit _),

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝² : MonObj M✝
inst✝¹ : MonObj N✝
inst✝ : MonObj O
M N : Mon C
α : yonedaMonObj M.X ⟶ yonedaMonObj N.X
⊢ (ConcreteCategory.hom (α.app (op (𝟙_ C)))) (toUnit (𝟙_ C) ≫ η) = η
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

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

Tactic:
by aesop

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
T X Y : C
f : T ⟶ X
g : T ⟶ Y
⊢ lift f g ≫ (β_ Y X).inv = lift g f

Tactic:
by aesop

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

Goal state before:
pp: R : Type u
A : Type v
ι : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
repr : Coalgebra.Repr R a ι
⊢ ∑ i ∈ repr.index, (antipode R) (repr.left i) * repr.right i = counit a • 1

Tactic:
rw [sum_antipode_mul_eq_algebraMap_counit, Algebra.smul_def, mul_one]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
⊢ toConv (antipode R ∘ₗ LinearMap.mul' R A ∘ₗ ↑(TensorProduct.comm R A A)) =
    toConv (LinearMap.mul' R A ∘ₗ (antipode R ⊗ₘ antipode R))

Tactic:
apply left_inv_eq_right_inv (a := toConv <| LinearMap.mul' R A ∘ₗ TensorProduct.comm R A A)

Goal state after:
case hba
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
⊢ toConv (antipode R ∘ₗ LinearMap.mul' R A ∘ₗ ↑(TensorProduct.comm R A A)) *
      toConv (LinearMap.mul' R A ∘ₗ ↑(TensorProduct.comm R A A)) =
    1

case hac
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
⊢ toConv (LinearMap.mul' R A ∘ₗ ↑(TensorProduct.comm R A A)) *
      toConv (LinearMap.mul' R A ∘ₗ (antipode R ⊗ₘ antipode R)) =
    1
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y Z : C
inst✝ : Closed X
f : X ⟶ Y
g : Y ⟶ Z
⊢ curry' f ≫ (ihom X).map g = curry' (f ≫ g)

Tactic:
simp only [curry', ← curry_natural_right, Category.assoc]

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

Goal state before:
pp: case e'_3.h₁
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
i j : ι
⊢ j = i ↔ i = j

Tactic:
@eq_comm _ j i

Goal state after:
case e'_3.h₁
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
i j : ι
⊢ i = j ↔ i = j
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
⊢ False

Tactic:
have := rank_quotient_add_rank (R := R) (M := PUnit) ⊥

Goal state after:
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
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{u, u_1} R
f : M →ₗ[R] M'
p : Submodule R M'
⊢ ∀ x ∈ comap f p, f x ∈ p

Tactic:
by aesop

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

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank K (V →ₗ[K] K) = #(V →ₗ[K] K)

Tactic:
obtain ⟨⟨ι, b⟩⟩ := Module.Free.exists_basis (R := K) (M := V)
  rw [← b.mk_eq_rank'', aleph0_le_mk_iff] at h
  have e := (b.constr K (M' := K)).symm
  rw [e.rank_eq, e.toEquiv.cardinal_eq]
  apply rank_fun_infinite

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : IsStablyFiniteRing R
inst✝ : Nontrivial R
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Surjective ⇑f
lt : n < m
⊢ False

Tactic:
let p : (Fin m → R) →ₗ[R] Fin n → R := funLeft R R (Fin.castLE lt.le)

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : IsStablyFiniteRing R
inst✝ : Nontrivial R
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Surjective ⇑f
lt : n < m
p : (Fin m → R) →ₗ[R] Fin n → R := funLeft R R (Fin.castLE ⋯)
⊢ False
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
⊢ Module.rank R (M ⧸ N) + Module.rank R ↥N = Module.rank R M

Tactic:
exact HasRankNullity.rank_quotient_add_rank _

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
inst✝ : Module.Finite K V
p : Submodule K V
v : V
hv : v ∉ p
⊢ v ≠ 0

Tactic:
by aesop

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
⊢ x ∈ W ⊓ B.ker

Tactic:
refine ⟨hx, ?_⟩

Goal state after:
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
⊢ x ∈ ↑B.ker
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 : ∀ (j : WalkingParallelPair), (coequalizerCocone F).ι.app j ≫ m = c.ι.app j
⊢ pushoutInl F ≫ m = c.ι.app WalkingParallelPair.one

Tactic:
simpa using J WalkingParallelPair.one

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
Z : C
h : Y ⟶ Z
t : IsSplitCoequalizer f g h
s : Cofork f g
⊢ t.asCofork.π ≫ t.rightSection ≫ s.π = s.π

Tactic:
by
      dsimp
      rw [← t.leftSection_top_assoc, s.condition, t.leftSection_bottom_assoc]

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

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
hp : p < ⊤
hp' : Projective R (M ⧸ p)
x : M
hx : x ∉ p
f : Dual R M
hf : f x ≠ 0
hf' : map f p = ⊥
⊢ f ≠ 0

Tactic:
by aesop

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
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
x : M
⊢ B x = 0 → x = 0 ↔ (B x = 0 ↔ x = 0)

Tactic:
by aesop

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
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
x : M
⊢ (B x) x = 0 ∧ x ≠ 0 ∨ (B x) x ≠ 0 ∧ x = 0 → x ≠ 0 ∧ (B x) x ≤ 0

Tactic:
by aesop

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f : M ⟶ N
⊢ ↟(Hom.hom f).ker.subtype ≫ f = 0

Tactic:
by aesop

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

Goal state before:
pp: case of_equiv
K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
α β : Type u_4
h : α ≃ β
hyp : ∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)
W : β → Subspace K V₁
⊢ dualAnnihilator (⨅ i, W i) = ⨆ i, dualAnnihilator (W i)

Tactic:
rw [← h.iInf_comp, hyp _, ← h.iSup_comp]

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₁
⊢ Injective ⇑B.flip ↔ Surjective ⇑B

Tactic:
by
  rw [← dualMap_surjective_iff, ← (evalEquiv K V₁).toEquiv.surjective_comp]; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCokernels C
inst✝² : IsNormalEpiCategory C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst✝¹ : Epi a
inst✝ : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
⊢ (f ≫ a) ≫ s.inl = 0 ≫ s.inl

Tactic:
eq_whisker hfa

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasFiniteCoproducts C
inst✝³ : HasCokernels C
inst✝² : IsNormalEpiCategory C
X Y Z : C
a : X ⟶ Y
b : X ⟶ Z
inst✝¹ : Epi a
inst✝ : Epi b
P : C
f : P ⟶ X
hfa : f ≫ a = 0
i : IsColimit (CokernelCofork.ofπ a hfa)
Q : C
g : Q ⟶ X
hgb : g ≫ b = 0
i' : IsColimit (CokernelCofork.ofπ b hgb)
a' : (CokernelCofork.ofπ a hfa).pt ⟶ cokernel (coprod.desc f g)
ha' : Cofork.π (CokernelCofork.ofπ a hfa) ≫ a' = cokernel.π (coprod.desc f g)
b' : (CokernelCofork.ofπ b hgb).pt ⟶ cokernel (coprod.desc f g)
hb' : Cofork.π (CokernelCofork.ofπ b hgb) ≫ b' = cokernel.π (coprod.desc f g)
s : PushoutCocone a b
⊢ 0 ≫ s.inl = 0 ≫ s.inl
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
⊢ Epi (r A)

Tactic:
let hp1 : IsLimit (KernelFork.ofι (prod.lift (𝟙 A) (0 : A ⟶ A)) hlp) := by
    refine Fork.IsLimit.mk _ (fun s => Fork.ι s ≫ Limits.prod.fst) ?_ ?_
    · intro s
      apply Limits.prod.hom_ext <;> simp
    · intro s m h
      have : Mono (prod.lift (𝟙 A) (0 : A ⟶ A)) := mono_of_mono_fac (prod.lift_fst _ _)
      apply (cancel_mono (prod.lift (𝟙 A) (0 : A ⟶ A))).1
      convert! h
      apply Limits.prod.hom_ext <;> simp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
hp1 : IsLimit (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) :=
  Fork.IsLimit.mk (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) (fun s ↦ s.ι ≫ prod.fst) ⋯ ⋯
⊢ Epi (r A)
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
aux :
  ∀ (s : CokernelCofork (kernel.ι f)),
    Cofork.π (CokernelCofork.ofπ f ⋯) ≫
        inv (imageMonoFactorisation f).m ≫
          inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) s =
      Cofork.π s
A : CokernelCofork (kernel.ι f)
g : (CokernelCofork.ofπ f ⋯).pt ⟶ A.pt
hg : f ≫ g = Cofork.π A
⊢ g = inv (imageMonoFactorisation f).m ≫ inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) A

Tactic:
← cancel_epi f,

Goal state after:
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
aux :
  ∀ (s : CokernelCofork (kernel.ι f)),
    Cofork.π (CokernelCofork.ofπ f ⋯) ≫
        inv (imageMonoFactorisation f).m ≫
          inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) s =
      Cofork.π s
A : CokernelCofork (kernel.ι f)
g : (CokernelCofork.ofπ f ⋯).pt ⟶ A.pt
hg : f ≫ g = Cofork.π A
⊢ f ≫ g =
    f ≫ inv (imageMonoFactorisation f).m ≫ inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) A
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✝ : Epi f
⊢ Nonempty (NormalEpi f)

Tactic:
obtain ⟨hf⟩ := h f
    exact ⟨{
      W := hf.kernelFork.pt
      g := hf.kernelFork.ι
      w := by simp
      isColimit :=
        have : IsIso hf.imageι :=
          KernelFork.IsLimit.isIso_ι _ hf.imageIsKernel (by simp [← cancel_epi f])
        IsColimit.ofIsoColimit hf.imageIsCokernel (Cofork.ext (asIso hf.imageι)) }⟩

Goal state after:
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φ' : QuasiIso φ'
⊢ QuasiIso (φ ≫ φ') ↔ QuasiIso φ

Tactic:
constructor
  · intro
    exact quasiIso_of_comp_right φ φ'
  · intro
    exact quasiIso_comp φ φ'

Goal state after: