mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case hy
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := ⋯
RXm : Type (max w₁ 0) := ⋯
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := ⋯
g' : Fin n → RXn := ⋯
hh' : ∀ (x : RXm), f (aeval_h x) = f' x
s' : Set RXn := ⋯
leI : Ideal.span s' ≤ RingHom.ker f.toRingHom
x : RXn
hx : x ∈ RingHom.ker f.toRingHom
this : x ∈ adjoin R (Set.range MvPolynomial.X)
i : Fin n
⊢ MvPolynomial.X i - (MvPolynomial.aeval h) (g i) ∈ Set.range g'

Tactic:
exact Set.mem_range_self _

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_4.hx
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := ⋯
RXm : Type (max w₁ 0) := ⋯
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := ⋯
g' : Fin n → RXn := ⋯
hh' : ∀ (x : RXm), f (aeval_h x) = f' x
s' : Set RXn := ⋯
leI : Ideal.span s' ≤ RingHom.ker f.toRingHom
x : RXn
hx : x ∈ RingHom.ker f.toRingHom
this : x ∈ adjoin R (Set.range MvPolynomial.X)
x₁ : RXm
y₁ : RXn
hy₁ : y₁ ∈ (Ideal.span s').toAddSubmonoid
hx✝ : aeval_h.toRingHom x₁ + y₁ ∈ adjoin R (Set.range MvPolynomial.X)
h₁ : aeval_h.toRingHom x₁ + y₁ ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid
x₂ : RXm
y₂ : RXn
hy₂ : y₂ ∈ (Ideal.span s').toAddSubmonoid
hy✝ : aeval_h.toRingHom x₂ + y₂ ∈ adjoin R (Set.range MvPolynomial.X)
h₂ : aeval_h.toRingHom x₂ + y₂ ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid
⊢ aeval_h.toRingHom (x₁ * x₂) ∈ aeval_h.range.toAddSubmonoid

Tactic:
exact Set.mem_range_self _

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
k : IsKernelPair f a b
r : RegularEpi f
⊢ IsColimit (Cofork.ofπ f ⋯)

Tactic:
let t := k.isLimit.lift (PullbackCone.mk _ _ r.w)
  have ht : t ≫ a = r.left := k.isLimit.fac _ WalkingCospan.left
  have kt : t ≫ b = r.right := k.isLimit.fac _ WalkingCospan.right
  refine Cofork.IsColimit.mk _
    (fun s => Cofork.IsColimit.desc r.isColimit s.π
      (by rw [← ht, assoc, s.condition, reassoc_of% kt]))
    (fun s => ?_) (fun s m w => ?_)
  · apply Cofork.IsColimit.π_desc' r.isColimit
  · apply Cofork.IsColimit.hom_ext r.isColimit
    exact w.trans (Cofork.IsColimit.π_desc' r.isColimit _ _).symm

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a : R ⟶ X
inst✝¹ : IsIso a
inst✝ : Mono f
⊢ IsPullback a a f f

Tactic:
convert! (IsPullback.of_horiz_isIso ⟨(rfl : a ≫ 𝟙 X = _)⟩).paste_vert (IsKernelPair.id_of_mono f)

Goal state after:
case e'_8
C : Type u
inst✝² : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a : R ⟶ X
inst✝¹ : IsIso a
inst✝ : Mono f
⊢ a = a ≫ 𝟙 X

case e'_9
C : Type u
inst✝² : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a : R ⟶ X
inst✝¹ : IsIso a
inst✝ : Mono f
⊢ f = 𝟙 X ≫ f
Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
P Q : ObjectProperty C
inst✝² : P.ContainsZero
inst✝¹ : Q.ContainsZero
inst✝ : Q.IsClosedUnderIsomorphisms
⊢ ∃ Z, IsZero Z ∧ (P ⊓ Q) Z

Tactic:
obtain ⟨Z, hZ, hP⟩ := P.exists_prop_of_containsZero
    exact ⟨Z, hZ, hP, Q.prop_of_isZero hZ⟩

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:
rwa [← isClosedUnderLimitsOfShape_iff_op]

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'
Q : ObjectProperty Cᵒᵖ
inst✝ : Q.IsClosedUnderLimitsOfShape Jᵒᵖ
⊢ Q.unop.IsClosedUnderColimitsOfShape J

Tactic:
rwa [← isClosedUnderLimitsOfShape_op_iff_unop]

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 : Cᵒᵖ ⥤ MonCat
α : (F ⋙ forget MonCat).RepresentableBy X
⊢ α.homEquiv'.symm 1 ▷ X ≫ α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) = (λ_ X).hom

Tactic:
by
    apply α.homEquiv'.injective
    simp only [α.homEquiv'_comp, Equiv.apply_symm_apply, map_mul]
    simp only [← α.homEquiv'_comp]
    simp only [whiskerRight_fst, whiskerRight_snd, α.homEquiv'_comp, Equiv.apply_symm_apply]
    simp [leftUnitor_hom, -op_tensorObj, -op_whiskerRight, -op_tensorUnit]

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 : Cᵒᵖ ⥤ MonCat
α : (F ⋙ forget MonCat).RepresentableBy X
⊢ α.homEquiv' (α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) ▷ X ≫ fst X X) *
      α.homEquiv' (α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) ▷ X ≫ snd X X) =
    α.homEquiv' ((α_ X X X).hom ≫ X ◁ α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) ≫ fst X X) *
      α.homEquiv' ((α_ X X X).hom ≫ X ◁ α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) ≫ snd X X)

Tactic:
simp only [whiskerRight_fst, whiskerRight_snd, whiskerLeft_fst, associator_hom_fst,
      whiskerLeft_snd, α.homEquiv'_comp, Equiv.apply_symm_apply, map_mul, _root_.mul_assoc]

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
F : Cᵒᵖ ⥤ MonCat
α : (F ⋙ forget MonCat).RepresentableBy X
⊢ (ConcreteCategory.hom (F.map (fst (X ⊗ X) X).op)) (α.homEquiv' (fst X X)) *
      ((ConcreteCategory.hom (F.map (fst (X ⊗ X) X).op)) (α.homEquiv' (snd X X)) * α.homEquiv' (snd (X ⊗ X) X)) =
    (ConcreteCategory.hom (F.map (fst (X ⊗ X) X).op)) (α.homEquiv' (fst X X)) *
      ((ConcreteCategory.hom (F.map (α_ X X X).hom.op))
          ((ConcreteCategory.hom (F.map (snd X (X ⊗ X)).op)) (α.homEquiv' (fst X X))) *
        (ConcreteCategory.hom (F.map (α_ X X X).hom.op))
          ((ConcreteCategory.hom (F.map (snd X (X ⊗ X)).op)) (α.homEquiv' (snd X X))))
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
A B A' B' : C
inst✝¹ : IsIso (prodComparison F A B)
f : A ⟶ A'
g : B ⟶ B'
inst✝ : IsIso (prodComparison F A' B')
⊢ F.map (f ⊗ₘ g) ≫ prodComparison F A' B' = prodComparison F A B ≫ (F.map f ⊗ₘ F.map g)

Tactic:
prodComparison_natural

Goal state after:
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
A B A' B' : C
inst✝¹ : IsIso (prodComparison F A B)
f : A ⟶ A'
g : B ⟶ B'
inst✝ : IsIso (prodComparison F A' B')
⊢ prodComparison F A B ≫ (F.map f ⊗ₘ F.map g) = prodComparison F A B ≫ (F.map f ⊗ₘ F.map g)
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
inst✝ : Closed Y
f : X ⟶ Y
g : Y ⟶ Z
⊢ curry' (f ≫ g) = curry' f ≫ (ihom X).map g

Tactic:
curry'_ihom_map

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : Closed X
inst✝ : Closed Y
f : X ⟶ Y
g : Y ⟶ Z
⊢ curry' (f ≫ g) = curry' (f ≫ g)
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
s t : Submodule R M
| Module.rank R ↥s + Module.rank R ↥t

Tactic:
2

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
s t : Submodule R M
| Module.rank R ↥t
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✝ : FiniteDimensional K V
f : End K V
h_contra : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)
h_le_ker_pow : ∀ n ≤ (finrank K V).succ, n ≤ finrank K ↥(LinearMap.ker (f ^ n))
h_any_n_lt : ∀ n ≤ (finrank K V).succ, n ≤ finrank K V
⊢ False

Tactic:
exact Nat.not_succ_le_self _ (h_any_n_lt (finrank K V).succ (finrank K V).succ.le_refl)

Goal state after:
Module: Mathlib.LinearAlgebra.Coevaluation

Goal state before:
pp: K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.rTensor (Dual K V) (contractLeft K V) ∘ₗ
        ↑(TensorProduct.assoc K (Dual K V) V (Dual K V)).symm ∘ₗ LinearMap.lTensor (Dual K V) (coevaluation K V))
      (((TensorProduct.mk K (Dual K V) K) ((Basis.ofVectorSpace K V).dualBasis j)) 1) =
    (↑(TensorProduct.lid K (Dual K V)).symm ∘ₗ ↑(TensorProduct.rid K (Dual K V)))
      (((TensorProduct.mk K (Dual K V) K) ((Basis.ofVectorSpace K V).dualBasis j)) 1)

Tactic:
TensorProduct.mk_apply

Goal state after:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.rTensor (Dual K V) (contractLeft K V) ∘ₗ
        ↑(TensorProduct.assoc K (Dual K V) V (Dual K V)).symm ∘ₗ LinearMap.lTensor (Dual K V) (coevaluation K V))
      ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] 1) =
    (↑(TensorProduct.lid K (Dual K V)).symm ∘ₗ ↑(TensorProduct.rid K (Dual K V)))
      ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] 1)
Module: Mathlib.LinearAlgebra.Coevaluation

Goal state before:
pp: K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.lTensor V (contractLeft K V) ∘ₗ
        ↑(TensorProduct.assoc K V (Dual K V) V) ∘ₗ LinearMap.rTensor V (coevaluation K V))
      (((TensorProduct.mk K K V) 1) ((Basis.ofVectorSpace K V) j)) =
    (↑(TensorProduct.rid K V).symm ∘ₗ ↑(TensorProduct.lid K V))
      (((TensorProduct.mk K K V) 1) ((Basis.ofVectorSpace K V) j))

Tactic:
TensorProduct.mk_apply

Goal state after:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (LinearMap.lTensor V (contractLeft K V) ∘ₗ
        ↑(TensorProduct.assoc K V (Dual K V) V) ∘ₗ LinearMap.rTensor V (coevaluation K V))
      (1 ⊗ₜ[K] (Basis.ofVectorSpace K V) j) =
    (↑(TensorProduct.rid K V).symm ∘ₗ ↑(TensorProduct.lid K V)) (1 ⊗ₜ[K] (Basis.ofVectorSpace K V) j)
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✝⁴ : AddCommGroup 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.IsAlt
x y : M₁
⊢ -(B x) y = (B y) x

Tactic:
have H1 : B (y + x) (y + x) = 0 := self_eq_zero H (y + x)
  simpa [map_add, self_eq_zero H, add_eq_zero_iff_neg_eq] using H1

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

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
B : M →ₗ[R] M →ₗ[R] M₂
B' : M₁ →ₗ[R] M₁ →ₗ[R] M₂
f : M → M₁
g : M₁ → M
c : R
h : B.IsAdjointPair B' f g
x✝¹ : M
x✝ : M₁
⊢ (B' ((c • f) x✝¹)) x✝ = (B x✝¹) ((c • g) x✝)

Tactic:
by
  simp [h _]

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

Goal state before:
pp: n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst✝ : Nontrivial R
v : Basis n R M
h : B.IsOrthoᵢ ⇑v
hB : B.SeparatingRight
i : n
⊢ (B (v i)) (v i) ≠ 0

Tactic:
rw [isOrthoᵢ_flip] at h
  exact h.not_isOrtho_basis_self_of_separatingLeft (flip_separatingLeft.mpr hB) i

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

Goal state before:
pp: case refine_3.right
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
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
⊢ (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)).ι.app { as := WalkingPair.right } ≫
      G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)) ≫
        c.ι.app WalkingParallelPair.one =
    (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)).ι.app { as := WalkingPair.right } ≫
      G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
        c.ι.app WalkingParallelPair.one

Tactic:
simp only [BinaryCofan.ι_app_right, BinaryCofan.mk_inr, ←
              G.map_comp_assoc, coprod.inr_desc]

Goal state after:
case refine_3.right
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
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
⊢ G.map (K.map WalkingParallelPairHom.left) ≫ c.ι.app WalkingParallelPair.one =
    G.map (K.map WalkingParallelPairHom.right) ≫ c.ι.app WalkingParallelPair.one
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
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y

Tactic:
have aux (x y : M) : 0 ≤ (B x x) * ((B x x) * (B y y) - (B x y) * (B y x)) := by
    rw [← apply_smul_sub_smul_sub_eq B x y]
    exact hs (B x y • x - B x x • y)
  rcases lt_or_ge 0 (B x x) with hx | hx
  · exact sub_nonneg.mp <| nonneg_of_mul_nonneg_right (aux x y) hx
  · replace hx : B x x = 0 := le_antisymm hx (hs x)
    rcases lt_or_ge 0 (B y y) with hy | hy
    · rw [mul_comm (B x y), mul_comm (B x x)]
      exact sub_nonneg.mp <| nonneg_of_mul_nonneg_right (aux y x) hy
    · replace hy : B y y = 0 := le_antisymm hy (hs y)
      suffices B x y = - B y x by simpa [this, hx, hy] using mul_self_nonneg (B y x)
      rw [eq_neg_iff_add_eq_zero]
      apply le_antisymm
      · simpa [hx, hy, le_neg_iff_add_nonpos_left] using hs (x - y)
      · simpa [hx, hy] using hs (x + y)

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 y : M
⊢ (B x) y * (B x) y = (B x) y * (B y) x

Tactic:
← hB.eq,

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
x y : M
⊢ (RingHom.id R) ((B y) x) * (RingHom.id R) ((B y) x) = (RingHom.id R) ((B y) x) * (B y) x
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
hz : (B x) y • x - (B x) x • y = 0
⊢ ¬LinearIndependent R ![x, y]

Tactic:
by_contra hL

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
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
hz : (B x) y • x - (B x) x • y = 0
hL : LinearIndependent R ![x, y]
⊢ False
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 ∈ ker B

Tactic:
rw [LinearMap.mem_ker]
  refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
  ext y
  have := B.apply_sq_le_of_symm hs hB x y
  simp only [h, zero_mul] at this
  exact eq_zero_of_pow_eq_zero <| le_antisymm this (sq_nonneg (B x y))

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

Goal state before:
pp: ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, (L i).ker ≤ K.ker
x✝¹ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
p : Submodule 𝕜 E := ⨅ i, (L i).ker
p_eq : p = φ.ker
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := p.liftQ φ ⋯
x✝ : FiniteDimensional 𝕜 (E ⧸ p)
L' : ι → E ⧸ p →ₗ[𝕜] 𝕜 := fun i ↦ p.liftQ (L i) ⋯
K' : E ⧸ p →ₗ[𝕜] 𝕜 := p.liftQ K h
this : ⨅ i, (L' i).ker ≤ K'.ker
c : ι → 𝕜
hK' : ∑ i, c i • L' i = K'
| ∑ i, c i • L i

Tactic:
2

Goal state after:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, (L i).ker ≤ K.ker
x✝¹ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
p : Submodule 𝕜 E := ⨅ i, (L i).ker
p_eq : p = φ.ker
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := p.liftQ φ ⋯
x✝ : FiniteDimensional 𝕜 (E ⧸ p)
L' : ι → E ⧸ p →ₗ[𝕜] 𝕜 := fun i ↦ p.liftQ (L i) ⋯
K' : E ⧸ p →ₗ[𝕜] 𝕜 := p.liftQ K h
this : ⨅ i, (L' i).ker ≤ K'.ker
c : ι → 𝕜
hK' : ∑ i, c i • L' i = K'
| fun i ↦ c i • L i
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
inst✝ : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
hB : IsSymm B
x y : M
⊢ (B x) y * (B x) y = (B x) y * (B y) x

Tactic:
← hB.eq,

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
inst✝ : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → 0 < (B x) x
hB : IsSymm B
x y : M
⊢ (RingHom.id R) ((B y) x) * (RingHom.id R) ((B y) x) = (RingHom.id R) ((B y) x) * (B y) x
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
⊢ f = factorThruImage f ≫ Limits.image.ι f

Tactic:
Limits.image.fac

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ f = f
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
s : Cofork (biprod.lift f (-g)) 0
m : (biproductToPushoutCofork f g).pt ⟶ s.pt
h : Cofork.π (biproductToPushoutCofork f g) ≫ m = s.π
⊢ m = pushout.desc (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯

Tactic:
apply pushout.hom_ext <;> simp [← h]

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

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
x : ↑B
y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z : ↑B
hz : (fun x ↦ x • ↑(Hom.hom f).range) z = ↑y
⊢ (fun x ↦ x • ↑(Hom.hom f).range) (x * z) = x • ↑y

Tactic:
by simp [← hz, smul_smul]

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 : ShortComplex C
inst✝ : S.HasHomology
⊢ S.leftHomologyData.homologyIso.hom = S.leftHomologyIso.symm.hom

Tactic:
dsimp [homologyIso, leftHomologyIso, ShortComplex.leftHomologyIso]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ leftHomologyMap' (𝟙 S) S.homologyData.left S.leftHomologyData ≫
      leftHomologyMap' (𝟙 S) S.leftHomologyData S.leftHomologyData =
    leftHomologyMap' (𝟙 S) S.homologyData.left S.leftHomologyData
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
e : S₁ ≅ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ opcyclesMap' (𝟙 S₁) h₁ h₁ = 𝟙 h₁.Q

Tactic:
opcyclesMap'_id

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
e : S₁ ≅ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ 𝟙 h₁.Q = 𝟙 h₁.Q
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₁ S₂ S₃ : ShortComplex C
e : S₁ ≅ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ opcyclesMap' (𝟙 S₂) h₂ h₂ = 𝟙 h₂.Q

Tactic:
opcyclesMap'_id

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
e : S₁ ≅ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ 𝟙 h₂.Q = 𝟙 h₂.Q
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₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ opcyclesMap (opMap φ) ≫ S₁.opcyclesOpIso.hom = S₂.opcyclesOpIso.hom ≫ (cyclesMap φ).op

Tactic:
rw [← cancel_epi S₂.op.pOpcycles, p_opcyclesMap_assoc, opMap_τ₂,
    op_pOpcycles_opcyclesOpIso_hom, op_pOpcycles_opcyclesOpIso_hom_assoc, ← op_comp,
    ← op_comp, cyclesMap_i]

Goal state after: