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

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
comm : a ≫ f₁ = b ≫ f₁
big_k : IsKernelPair (f₁ ≫ f₂) a b
s : PullbackCone f₁ f₁
s' : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂) := PullbackCone.mk s.fst s.snd ⋯
m✝ : s.pt ⟶ (PullbackCone.mk a b comm).pt
m₁ : m✝ ≫ (PullbackCone.mk a b comm).fst = s.fst
m₂ : m✝ ≫ (PullbackCone.mk a b comm).snd = s.snd
⊢ a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
comm : a ≫ f₁ = b ≫ f₁
big_k : IsKernelPair (f₁ ≫ f₂) a b
s : PullbackCone f₁ f₁
s' : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂) := PullbackCone.mk s.fst s.snd ⋯
m✝ : s.pt ⟶ (PullbackCone.mk a b comm).pt
m₁ : m✝ ≫ (PullbackCone.mk a b comm).fst = s.fst
m₂ : m✝ ≫ (PullbackCone.mk a b comm).snd = s.snd
⊢ m✝ ≫ (PullbackCone.mk a b ?refine_1).fst = (IsPullback.isLimit big_k).lift s' ≫ (PullbackCone.mk a b ?refine_1).fst

pp: case refine_3
C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
comm : a ≫ f₁ = b ≫ f₁
big_k : IsKernelPair (f₁ ≫ f₂) a b
s : PullbackCone f₁ f₁
s' : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂) := PullbackCone.mk s.fst s.snd ⋯
m✝ : s.pt ⟶ (PullbackCone.mk a b comm).pt
m₁ : m✝ ≫ (PullbackCone.mk a b comm).fst = s.fst
m₂ : m✝ ≫ (PullbackCone.mk a b comm).snd = s.snd
⊢ m✝ ≫ (PullbackCone.mk a b ?refine_1).snd = (IsPullback.isLimit big_k).lift s' ≫ (PullbackCone.mk a b ?refine_1).snd

Tactic:
· apply reassoc_of% comm

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
comm : a ≫ f₁ = b ≫ f₁
big_k : IsKernelPair (f₁ ≫ f₂) a b
s : PullbackCone f₁ f₁
s' : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂) := PullbackCone.mk s.fst s.snd ⋯
m✝ : s.pt ⟶ (PullbackCone.mk a b comm).pt
m₁ : m✝ ≫ (PullbackCone.mk a b comm).fst = s.fst
m₂ : m✝ ≫ (PullbackCone.mk a b comm).snd = s.snd
⊢ m✝ ≫ (PullbackCone.mk a b ⋯).fst = (IsPullback.isLimit big_k).lift s' ≫ (PullbackCone.mk a b ⋯).fst

case refine_3
C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
comm : a ≫ f₁ = b ≫ f₁
big_k : IsKernelPair (f₁ ≫ f₂) a b
s : PullbackCone f₁ f₁
s' : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂) := PullbackCone.mk s.fst s.snd ⋯
m✝ : s.pt ⟶ (PullbackCone.mk a b comm).pt
m₁ : m✝ ≫ (PullbackCone.mk a b comm).fst = s.fst
m₂ : m✝ ≫ (PullbackCone.mk a b comm).snd = s.snd
⊢ m✝ ≫ (PullbackCone.mk a b ⋯).snd = (IsPullback.isLimit big_k).lift s' ≫ (PullbackCone.mk a b ⋯).snd
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P ≤ P.pushouts

Tactic:
by
  intro X Y p hp
  exact P.pushouts_mk IsPushout.of_id_fst hp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
⊢ P.limitsOfShape J = (P.op.colimitsOfShape Jᵒᵖ).unop

Tactic:
ext X
  refine ⟨fun ⟨h⟩ => ⟨?_⟩, fun ⟨h⟩ => ⟨?_⟩⟩
  · exact
      { diag := h.diag.op
        ι := NatTrans.op h.π
        isColimit := isColimitOfUnop h.isLimit
        prop_diag_obj _ := h.prop_diag_obj _ }
  · exact
      { diag := h.diag.unop
        π := NatTrans.unop h.ι
        isLimit := isLimitOfOp h.isColimit
        prop_diag_obj _ := h.prop_diag_obj _ }

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.IsClosedUnderColimitsOfShape WalkingParallelPair
X Y : C
h : Retract X Y
hY : P Y
c : Cofork (h.r ≫ h.i) (𝟙 Y) := Cofork.ofπ h.r ⋯
s : Cofork (h.r ≫ h.i) (𝟙 Y)
⊢ c.π ≫ h.i ≫ s.π = s.π

Tactic:
by simpa using! s.condition

Goal state after:
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
inst✝ : BraidedCategory C
⊢ ∀ (a b : SymmetricCategory C), a = b

Tactic:
rintro ⟨_⟩ ⟨_⟩

Goal state after:
C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
inst✝ toBraidedCategory✝¹ : BraidedCategory C
symmetry✝¹ : ∀ (X Y : C), (β_ X Y).hom ≫ (β_ Y X).hom = 𝟙 (X ⊗ Y)
toBraidedCategory✝ : BraidedCategory C
symmetry✝ : ∀ (X Y : C), (β_ X Y).hom ≫ (β_ Y X).hom = 𝟙 (X ⊗ Y)
⊢ { toBraidedCategory := toBraidedCategory✝¹, symmetry := symmetry✝¹ } =
    { toBraidedCategory := toBraidedCategory✝, symmetry := symmetry✝ }
Module: Mathlib.RingTheory.Coalgebra.Convolution

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
ι : Type u_6
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalNonAssocSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
inst✝⁶ : AddCommMonoid C
inst✝⁵ : Module R C
inst✝⁴ : CoalgebraStruct R C
inst✝³ : Monoid S
inst✝² : DistribMulAction S A
inst✝¹ : SMulCommClass R S A
inst✝ : SMulCommClass S A A
s : S
f g : WithConv (C →ₗ[R] A)
⊢ s • f • g = f • s • g

Tactic:
by ext c; simp [(ℛ R c).convMul_apply, Finset.smul_sum, mul_smul_comm]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
ι : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsScalarTower R A A
inst✝² : AddCommMonoid C
inst✝¹ : Module R C
inst✝ : Coalgebra R C
f g h : WithConv (C →ₗ[R] A)
⊢ (mul' R A ∘ₗ rTensor A (mul' R A)) ∘ₗ
      (((f.ofConv ⊗ₘ g.ofConv) ⊗ₘ h.ofConv) ∘ₗ ↑(TensorProduct.assoc R C C C).symm) ∘ₗ lTensor C δ ∘ₗ δ =
    (mul' R A ∘ₗ rTensor A (mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A).symm) ∘ₗ
      (f.ofConv ⊗ₘ (g.ofConv ⊗ₘ h.ofConv)) ∘ₗ lTensor C δ ∘ₗ δ

Tactic:
by
      simp only [map_map_comp_assoc_symm_eq, comp_assoc]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
C : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring C
inst✝¹ : Bialgebra R C
inst✝ : Algebra R A
f g : WithConv (C →ₐ[R] A)
c : C
⊢ (f * g).ofConv c = (Algebra.TensorProduct.lift f.ofConv g.ofConv ⋯) (comul c)

Tactic:
simp only [convMul_def, coe_comp, Function.comp_apply, Bialgebra.comulAlgHom_apply]

Goal state after:
R : Type u_1
A : Type u_2
C : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring C
inst✝¹ : Bialgebra R C
inst✝ : Algebra R A
f g : WithConv (C →ₐ[R] A)
c : C
⊢ (lmul' R) ((Algebra.TensorProduct.map f.ofConv g.ofConv) (comul c)) =
    (Algebra.TensorProduct.lift f.ofConv g.ofConv ⋯) (comul c)
Module: Mathlib.RingTheory.HopfAlgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
⊢ counit ∘ₗ antipode R = counit

Tactic:
ext; exact counit_antipode _

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ (ihom.ev M).app N =
    ↟((TensorProduct.uncurry (RingHom.id R) ↑M ↑((ihom M).obj N) ↑N)
        (LinearMap.lcomp R ↑N ↑homLinearEquiv ∘ₗ LinearMap.id.flip))

Tactic:
rw [← MonoidalClosed.uncurry_id_eq_ev]

Goal state after:
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ MonoidalClosed.uncurry (𝟙 ((ihom M).obj N)) =
    ↟((TensorProduct.uncurry (RingHom.id R) ↑M ↑((ihom M).obj N) ↑N)
        (LinearMap.lcomp R ↑N ↑homLinearEquiv ∘ₗ LinearMap.id.flip))
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this✝ : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i ↦ bK i.1 i.2)
hLK : #↥L < #K
this : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
c : ιK →₀ K := bK.repr (⇑bL ∘ ⇑e)
s : Finset ιK := c.support
rep_e : ∑ a ∈ s, c a • bK a = ⇑bL ∘ ⇑e
f : ℕ → ↥s → ↥L := fun i j ↦ ⟨bK (↑j) i, ⋯⟩
h : LinearIndependent (↥L)ᵐᵒᵖ f
⊢ False

Tactic:
have := h.cardinal_lift_le_rank
    rw [lift_uzero, (LinearEquiv.piCongrRight fun _ ↦ MulOpposite.opLinearEquiv Lᵐᵒᵖ).rank_eq,
        rank_fun'] at this
    exact natCast_lt_aleph0.not_ge this

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 : C
inst✝ : HasLeftDual X
⊢ (ᘁ𝟙 X) = 𝟙 ᘁX

Tactic:
by
  simp [leftAdjointMate]

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

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
ιK : Type (max u v)
bK : Module.Basis ιK K (ι → K)
e : ℕ ↪ ι
this : lift.{v, u} (Module.rank K (ℕ → K)) ≤ Module.rank K (ι → K)
key : ℵ₀ ≤ Module.rank K (ι → K) ∧ lift.{v, u} #K ≤ Module.rank K (ι → K)
⊢ ℵ₀ ≤ Module.rank K (ι → K)

Tactic:
exact key.1

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

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
ι : Type v
hι : Infinite ι
⊢ Module.rank K (ι → K) = #(ι → K)

Tactic:
by
  obtain ⟨⟨ιK, bK⟩⟩ := Module.Free.exists_basis (R := K) (M := ι → K)
  obtain ⟨e⟩ := lift_mk_le'.mp ((aleph0_le_mk_iff.mpr hι).trans_eq (lift_uzero #ι).symm)
  have := LinearMap.lift_rank_le_of_injective _ <|
    LinearMap.funLeft_injective_of_surjective K K _ (invFun_surjective e.injective)
  rw [lift_umax.{u, v}, lift_id'.{u, v}] at this
  have key := (lift_le.{v}.mpr <| max_aleph0_card_le_rank_fun_nat K).trans this
  rw [lift_max, lift_aleph0, max_le_iff] at key
  have : Infinite ιK := by
    rw [← aleph0_le_mk_iff, bK.mk_eq_rank'']; exact key.1
  rw [bK.repr.toEquiv.cardinal_eq, mk_finsupp_lift_of_infinite,
      lift_umax.{u, v}, lift_id'.{u, v}, bK.mk_eq_rank'', eq_comm, max_eq_left]
  exact key.2

Goal state after:
Module: Mathlib.Algebra.Category.CommHopfAlgCat

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A B C : CommHopfAlgCat R
X✝ Y✝ Z : Type v
inst✝⁵ : CommRing X✝
inst✝⁴ : HopfAlgebra R X✝
inst✝³ : CommRing Y✝
inst✝² : HopfAlgebra R Y✝
inst✝¹ : CommRing Z
inst✝ : HopfAlgebra R Z
X Y : CommHopfAlgCat R
f : X ⟶ Y
x✝ : IsIso ((forget (CommHopfAlgCat R)).map f)
⊢ IsIso f

Tactic:
let i := asIso ((forget (CommHopfAlgCat.{u} R)).map f)
    let e : X ≃ₐc[R] Y := { f.hom, i.toEquiv with }
    exact (isoMk e).isIso_hom

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

Goal state before:

Tactic:
_ = Y' ◁ η_ Y Y' ⊗≫ ((Y' ⊗ Y) ◁ f ≫ ε_ Y Y' ▷ Z) ⊗≫ 𝟙 _ := by
      dsimp [tensorLeftHomEquiv]; monoidal
    _ = (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') ⊗≫ f := by
      rw [whisker_exchange]; monoidal
    _ = _ := by rw [coevaluation_evaluation'']; monoidal

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

Goal state before:
pp: case pos
K : Type u
inst✝¹ : DivisionRing K
ι : Type u_1
inst✝ : Fintype ι
b : ι → ι → K
hb : LinearIndependent K b
hι : Nonempty ι
⊢ ⇑(basisOfPiSpaceOfLinearIndependent hb) = b

Tactic:
simp [hι, basisOfPiSpaceOfLinearIndependent]

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✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
⊢ η_ (ᘁY) Y ≫ (ᘁf) ▷ Y = η_ (ᘁX) X ≫ ᘁX ◁ f

Tactic:
apply_fun (tensorRightHomEquiv _ (ᘁY) Y _).symm

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y : C
inst✝¹ : HasLeftDual X
inst✝ : HasLeftDual Y
f : X ⟶ Y
⊢ (tensorRightHomEquiv (𝟙_ C) (ᘁY) Y ᘁX).symm (η_ (ᘁY) Y ≫ (ᘁf) ▷ Y) =
    (tensorRightHomEquiv (𝟙_ C) (ᘁY) Y ᘁX).symm (η_ (ᘁX) X ≫ ᘁX ◁ f)
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁ X₂ Y : C
p₁ : ExactPairing X₁ Y
p₂ : ExactPairing X₂ Y
⊢ ((ᘁ𝟙 Y) ≫ ᘁ𝟙 Y) = 𝟙 X₂

Tactic:
by
    rw [← @comp_leftAdjointMate C, Category.comp_id, @leftAdjointMate_id]
    rfl

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I₁ I₁' : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₁'] M
x y : M₁
⊢ B.IsOrtho x y ↔ B.flip.IsOrtho y x

Tactic:
by
  simp_rw [isOrtho_def, flip_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix

Goal state before:
pp: K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ lift.{v, u_2} (Module.rank K M) < ℵ₀

Tactic:
rw [lift_lt_aleph0]; have := Module.nontrivial K L; apply Module.rank_lt_aleph0

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
p : Submodule R₁ M₁
x✝¹ x✝ : ↥p
⊢ (B ↑x✝¹) ↑x✝ = 0 → (B ↑x✝) ↑x✝¹ = 0

Tactic:
exact H _ _

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

Goal state before:
pp: R : Type u_20
M : Type u_21
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : LinearMap.BilinForm R M
F : Type u_22
inst✝¹ : FunLike F M M
inst✝ : LinearMapClass F R M M
f : F
h : IsLeftRegular 2
hB : IsSymm B
hf : ∀ (x : M), (B (f x)) (f x) = (B x) x
⊢ IsOrthogonal B ⇑f

Tactic:
intro x y
  suffices 2 * B (f x) (f y) = 2 * B x y from h this
  have := hf (x + y)
  simp only [map_add, LinearMap.add_apply, hf x, hf y, show B y x = B x y from hB.eq y x] at this
  rw [show B (f y) (f x) = B (f x) (f y) from hB.eq (f y) (f x)] at this
  simp only [add_assoc, add_right_inj] at this
  simp only [← add_assoc, add_left_inj] at this
  simpa only [← two_mul] using this

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

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

Tactic:
refine ⟨fun h ↦ h.2, fun hB' ↦ ⟨?_, hB'⟩⟩
  rw [separatingLeft_iff_ker_eq_bot, hB.ker_eq_bot_iff_ker_flip_eq_bot.mpr]
  rwa [← separatingRight_iff_flip_ker_eq_bot]

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
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y

Tactic:
rcases lt_or_ge 0 (B x x) with hx | hx

Goal state after:
case inl
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
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : 0 < (B x) x
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y

case inr
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
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x ≤ 0
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y
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
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
x y : M
he : (B x) y * (B y) x = (B x) x * (B y) y
⊢ ¬LinearIndependent R ![x, y]

Tactic:
by
  have hz : (B x y) • x - (B x x) • y = 0 := by
    by_contra hc
    exact (ne_of_lt (hp ((B x) y • x - (B x) x • y) hc)).symm <|
      (apply_smul_sub_smul_sub_eq B x y).symm ▸ (mul_eq_zero_of_right ((B x) x)
      (sub_eq_zero_of_eq he.symm))
  by_contra hL
  by_cases hx : x = 0
  · simpa [hx] using LinearIndependent.ne_zero 0 hL
  · have h := sub_eq_zero.mpr (sub_eq_zero.mp hz).symm
    rw [sub_eq_add_neg, ← neg_smul, add_comm] at h
    exact (Ne.symm (ne_of_lt (hp x hx))) (LinearIndependent.eq_zero_of_pair hL h).2

Goal state after:
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
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
⊢ F.map (F.preimage (NormalMono.g ≫ (F.objObjPreimageIso (NormalMono.Z (F.map f))).inv)) ≫
      (F.objObjPreimageIso (NormalMono.Z (F.map f))).hom =
    NormalMono.g

Tactic:
by
        simp only [Functor.map_preimage, Category.assoc, Iso.inv_hom_id, Category.comp_id]

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:
by rw [← Category.assoc, eq_whisker hfa]

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
f : X ⟶ Y
g : (CokernelCofork.ofπ σ ⋯).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g = prod.map f f ≫ σ
hfg : f = g
⊢ σ ≫ f = prod.map f f ≫ σ

Tactic:
← hg,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
g : (CokernelCofork.ofπ σ ⋯).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g = prod.map f f ≫ σ
hfg : f = g
⊢ σ ≫ f = Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
g : (CokernelCofork.ofπ σ ⋯).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g = prod.map f f ≫ σ
⊢ prod.lift (𝟙 X) 0 ≫ prod.map f f ≫ σ = prod.lift (𝟙 X) 0 ≫ σ ≫ g

Tactic:
← hg,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
f : X ⟶ Y
g : (CokernelCofork.ofπ σ ⋯).pt ⟶ Y
hg : Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g = prod.map f f ≫ σ
⊢ prod.lift (𝟙 X) 0 ≫ Cofork.π (CokernelCofork.ofπ σ ⋯) ≫ g = prod.lift (𝟙 X) 0 ≫ σ ≫ g
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi f
s : PullbackCone f g
hs : IsLimit s
this : Epi ((limit.cone (cospan f g)).π.app WalkingCospan.right)
⊢ Epi s.snd

Tactic:
apply epi_of_epi_fac (IsLimit.conePointUniqueUpToIso_hom_comp (limit.isLimit _) hs _)

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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
s : PullbackCone f g
hs : IsLimit s
this : Epi ((limit.cone (cospan f g)).π.app WalkingCospan.left)
⊢ Epi s.fst

Tactic:
apply epi_of_epi_fac (IsLimit.conePointUniqueUpToIso_hom_comp (limit.isLimit _) hs _)

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
g₁ : Y ⟶ W
inst✝¹ : Epi g₁
g₂ : W ⟶ Z
inst✝ : Mono g₂
hg : g₁ ≫ g₂ = g
f' : X ⟶ W
hf : f' ≫ g₂ = f
t : PullbackCone f g
ht : IsLimit t
⊢ Epi t.fst

Tactic:
by
  apply epi_fst_of_isLimit _ _ (PullbackCone.isLimitOfFactors f g g₂ f' g₁ hf hg t ht)

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
A : C
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ h.ι ≫ h.descQ k ⋯ = 0

Tactic:
rw [show 0 = h.ι ≫ h.g' ≫ x by simp]
  congr 1
  simp only [← cancel_epi h.p, hx, p_descQ, p_g'_assoc]

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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₂.RightHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ (ofEpiOfIsIsoOfMono' φ h).g' ≫ φ.τ₃ = h.g'

Tactic:
by
  rw [← cancel_epi (ofEpiOfIsIsoOfMono' φ h).p, p_g'_assoc, ofEpiOfIsIsoOfMono'_p,
    assoc, p_g', φ.comm₂₃]

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 : ShortComplex C
h : S.RightHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
⊢ (h.map F).g' = F.map h.g'

Tactic:
← cancel_epi (h.map F).p,

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✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
S : ShortComplex C
h : S.RightHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
⊢ (h.map F).p ≫ (h.map F).g' = (h.map F).p ≫ F.map h.g'
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₂.τ₃ = -h.h₃ + (-h.h₂) ≫ S₂.g + φ₁.τ₃

Tactic:
h.comm₃,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₂.τ₃ = -h.h₃ + (-h.h₂) ≫ S₂.g + (h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃)
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ -φ₁.τ₃ = -h.h₃ + (-h.h₂) ≫ S₂.g + -φ₂.τ₃

Tactic:
h.comm₃,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ -(h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃) = -h.h₃ + (-h.h₂) ≫ S₂.g + -φ₂.τ₃