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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : MorphismProperty C
inst✝³ : P.IsStableUnderCobaseChange
inst✝² : P.IsStableUnderComposition
S X X' Y Y' : C
f : S ⟶ X
g : S ⟶ Y
f' : S ⟶ X'
g' : S ⟶ Y'
i₁ : X ⟶ X'
inst✝¹ : HasPushoutsAlong f
inst✝ : HasPushoutsAlong g'
i₂ : Y ⟶ Y'
h₁ : P i₁
h₂ : P i₂
e₁ : f' = f ≫ i₁
e₂ : g' = g ≫ i₂
⊢ HasPushoutsAlong (Under.mk g').hom

Tactic:
cat_disch

Goal state after:
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S R' S' : Type u
x✝¹⁰ : CommRing R
x✝⁹ : CommRing S
x✝⁸ : CommRing R'
x✝⁷ : CommRing S'
x✝⁶ : Algebra R S
x✝⁵ : Algebra R R'
x✝⁴ : Algebra R S'
x✝³ : Algebra S S'
x✝² : Algebra R' S'
x✝¹ : IsScalarTower R S S'
x✝ : IsScalarTower R R' S'
hsq : Algebra.IsPushout R S R' S'
hRS : (fun {R S} [CommRing R] [CommRing S] ↦ P) (algebraMap R S)
⊢ (fun {R S} [CommRing R] [CommRing S] ↦ P) (algebraMap R' S')

Tactic:
rw [← CommRingCat.isPushout_iff_isPushout] at hsq
    exact h.1 (f := CommRingCat.ofHom (algebraMap R S)) hsq.flip hRS

Goal state after:
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₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), (extendCofan c₁ c₂).ι.app j ≫ m = s.ι.app j
⊢ c₂.inr ≫ m =
    c₂.inr ≫
      ↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 })
          (t₁.desc { pt := s.pt, ι := Discrete.natTrans fun i ↦ s.ι.app { as := i.as.succ } }))

Tactic:
(BinaryCofan.IsColimit.desc' t₂ _ _).2.2

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₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
m : (extendCofan c₁ c₂).pt ⟶ s.pt
w : ∀ (j : Discrete (Fin (n + 1))), (extendCofan c₁ c₂).ι.app j ≫ m = s.ι.app j
⊢ c₂.inr ≫ m = t₁.desc { pt := s.pt, ι := Discrete.natTrans fun i ↦ s.ι.app { as := i.as.succ } }
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ W ≤ W.colimitsOfShape (Discrete PUnit.{w + 1})

Tactic:
intro X₁ X₂ f hf

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
⊢ W.colimitsOfShape (Discrete PUnit.{w + 1}) f
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ (P ⊓ Q).universally f ↔ P.universally f ∧ Q.universally f

Tactic:
simp_rw [universally, ← forall_and]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P Q : MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ (∀ ⦃X' Y' : C⦄ (i₁ : X' ⟶ X) (i₂ : Y' ⟶ Y) (f' : X' ⟶ Y'), IsPullback f' i₁ i₂ f → (P ⊓ Q) f') ↔
    ∀ (x x_1 : C) (x_2 : x ⟶ X) (x_3 : x_1 ⟶ Y) (x_4 : x ⟶ x_1), IsPullback x_4 x_2 x_3 f → P x_4 ∧ Q x_4
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y Z : C
f : X ⟶ Y ⊗ Z
⊢ lift (f ≫ fst Y Z) (f ≫ snd Y Z) = f

Tactic:
cat_disch

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
T X Y : C
⊢ Function.LeftInverse (fun f ↦ (f ≫ fst X Y, f ≫ snd X Y)) fun f ↦ lift f.1 f.2

Tactic:
cat_disch

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
T X Y : C
⊢ Function.RightInverse (fun f ↦ (f ≫ fst X Y, f ≫ snd X Y)) fun f ↦ lift f.1 f.2

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
⊢ lift f g ≫ h ▷ Z = lift (f ≫ h) g

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Z ⟶ W
⊢ lift f g ≫ Y ◁ h = lift f (g ≫ h)

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
⊢ lift (lift f g) h ≫ (α_ Y Z W).hom = lift f (lift g h)

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
⊢ lift f (lift g h) ≫ (α_ Y Z W).inv = lift (lift f g) h

Tactic:
cat_disch

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

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

Tactic:
cat_disch

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
M X : C
inst✝ : MonObj M
⊢ monoidHom (𝟙 M) X = MonoidHom.id (X ⟶ M)

Tactic:
cat_disch

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

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

Tactic:
cat_disch

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
M N O X : C
inst✝⁴ : MonObj M
inst✝³ : MonObj N
inst✝² : MonObj O
f : M ⟶ N
g : N ⟶ O
inst✝¹ : IsMonHom f
inst✝ : IsMonHom g
⊢ monoidHom (f ≫ g) X = (monoidHom g X).comp (monoidHom f X)

Tactic:
cat_disch

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
X Y₂ : Cᵒᵖ
φ : X ⟶ Y₂
f₁ f₂ : unop X ⟶ M
⊢ (φ.unop ≫ lift f₁ f₂) ≫ μ = lift (φ.unop ≫ f₁) (φ.unop ≫ f₂) ≫ μ

Tactic:
cat_disch

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
X Y : C
⊢ lift (snd X Y) (fst X Y) = (β_ X Y).hom

Tactic:
cat_disch

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
W X Y Z : C
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift (snd W Y ≫ g') (fst W Y ≫ g) = (β_ W Y).hom ≫ (g' ⊗ₘ g)

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
⊢ preservesTerminalIso (𝟭 C) = Iso.refl ((𝟭 C).obj (𝟙_ C))

Tactic:
cat_disch

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
inst✝² : PreservesLimit (Functor.empty C) F
inst✝¹ : PreservesLimit (Functor.empty D) G
inst✝ : PreservesLimit (Functor.empty C) (F ⋙ G)
⊢ preservesTerminalIso (F ⋙ G) = G.mapIso (preservesTerminalIso F) ≪≫ preservesTerminalIso G

Tactic:
cat_disch

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
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 B A' B' : C
E : Type u₂
inst✝² : Category.{v₂, u₂} E
inst✝¹ : CartesianMonoidalCategory E
G : D ⥤ E
inst✝ : PreservesLimit (pair A B) F
⊢ IsIso (prodComparison F A B)

Tactic:
rw [← prodComparisonIso_hom]

Goal state after:
C✝ : Type u
inst✝⁹ : Category.{v, u} C✝
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 B A' B' : C
E : Type u₂
inst✝² : Category.{v₂, u₂} E
inst✝¹ : CartesianMonoidalCategory E
G : D ⥤ E
inst✝ : PreservesLimit (pair A B) F
⊢ IsIso (prodComparisonIso F A B).hom
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
inst✝ : F.OplaxMonoidal
X Y : C
⊢ δ F X Y = CartesianMonoidalCategory.prodComparison F X Y

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Opposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
G : C
⊢ ∀ (x y : G ⟶ G), { unop' := x + y } = { unop' := x } + { unop' := y }

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Opposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
G : C
⊢ ∀ (m : (End G)ᵐᵒᵖ) (x : G ⟶ G), { unop' := m • x } = (RingHom.id (End G)ᵐᵒᵖ) m • { unop' := x }

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Opposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
G : C
⊢ Function.LeftInverse
    (fun x ↦
      match x with
      | { unop' := f } => f)
    fun f ↦ { unop' := f }

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Opposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
G : C
⊢ Function.RightInverse
    (fun x ↦
      match x with
      | { unop' := f } => f)
    fun f ↦ { unop' := f }

Tactic:
cat_disch

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

Goal state before:
pp: α : Type u
β : α → Type v
⊢ (sum fun i ↦ #(WType β) ^ lift.{max u v, v} #(β i)) = sum fun a ↦ #(WType β) ^ lift.{u, v} #(β a)

Tactic:
lift_umax.{v, u}

Goal state after:
α : Type u
β : α → Type v
⊢ (sum fun i ↦ #(WType β) ^ lift.{u, v} #(β i)) = sum fun a ↦ #(WType β) ^ lift.{u, v} #(β a)
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
⊢ h.coeffs (lc e l) = l

Tactic:
ext i
  rw [h.coeffs_apply, h.dual_lc]

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)) ((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))

Tactic:
rw [rid_tmul, one_smul, lid_symm_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))) =
    1 ⊗ₜ[K] (Basis.ofVectorSpace K V).dualBasis j
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
m : Type u_7
n : Type u_8
inst✝³ : Fintype m
inst✝² : Finite n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
bM : Basis m R M
bN : Basis n R N
j : m
i : n
⊢ (toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) = Matrix.single i j 1

Tactic:
ext i' j'
  by_cases hij : i = i' ∧ j = j'
  · simp [LinearMap.toMatrix_apply, hij]
  · rw [and_iff_not_or_not, Classical.not_not] at hij
    rcases hij with hij | hij <;> simp [LinearMap.toMatrix_apply, Finsupp.single_eq_pi_single, hij]

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✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
c : Cone F
m✝ : c.pt ⟶ (equalizerCone F).pt
⊢ (∀ (j : WalkingParallelPair), m✝ ≫ (equalizerCone F).π.app j = c.π.app j) →
    m✝ = pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯

Tactic:
J

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
c : Cone F
m✝ : c.pt ⟶ (equalizerCone F).pt
J : ∀ (j : WalkingParallelPair), m✝ ≫ (equalizerCone F).π.app j = c.π.app j
⊢ m✝ = pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯
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:
J

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 : ∀ (j : WalkingParallelPair), (coequalizerCocone F).ι.app j ≫ m = c.ι.app j
⊢ m = pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯
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.SeparatingLeft
i : n
ho : (B (v i)) (v i) = 0
vi : n →₀ R
j : n
this : (B (v i)) (v j) = 0
⊢ I' (vi j) • (B (v i)) (v j) = 0

Tactic:
rw [this, smul_zero]

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

Goal state before:
pp: case h₀
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₁
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), (B (v i)) (v i) ≠ 0
vi : n →₀ R
i : n
hB : ∑ x ∈ vi.support, (RingHom.id R) (vi x) • (B (v x)) (v i) = 0
j : n
_hj : j ∈ vi.support
hij : (B (v j)) (v i) = 0
⊢ (RingHom.id R) (vi j) • 0 = 0

Tactic:
RingHom.id_apply,

Goal state after:
case h₀
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₁
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), (B (v i)) (v i) ≠ 0
vi : n →₀ R
i : n
hB : ∑ x ∈ vi.support, (RingHom.id R) (vi x) • (B (v x)) (v i) = 0
j : n
_hj : j ∈ vi.support
hij : (B (v j)) (v i) = 0
⊢ vi j • 0 = 0
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case h₁
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₁
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), (B (v i)) (v i) ≠ 0
vi : n →₀ R
i : n
hB : ∑ x ∈ vi.support, (RingHom.id R) (vi x) • (B (v x)) (v i) = 0
hi : vi i = 0
⊢ (RingHom.id R) 0 • (B (v i)) (v i) = 0

Tactic:
RingHom.id_apply,

Goal state after:
case h₁
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₁
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : B.IsOrthoᵢ ⇑v
h : ∀ (i : n), (B (v i)) (v i) ≠ 0
vi : n →₀ R
i : n
hB : ∑ x ∈ vi.support, (RingHom.id R) (vi x) • (B (v x)) (v i) = 0
hi : vi i = 0
⊢ 0 • (B (v i)) (v i) = 0
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
hB : IsSymm B
⊢ Nondegenerate B ↔ ∀ (x : M), (B x) x = 0 ↔ x = 0

Tactic:
simp_rw [hB.isRefl.nondegenerate_iff_separatingLeft, separatingLeft_iff_ker_eq_bot,
    Submodule.eq_bot_iff, B.apply_apply_same_eq_zero_iff hs hB, mem_ker]

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 : M), B x = 0 → x = 0) ↔ ∀ (x : M), B x = 0 ↔ x = 0
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case mp
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
x y : M
hle : ∀ (z : M), 0 ≤ (B z) z
⊢ (B x) y * (B y) x < (B x) x * (B y) y → LinearIndependent R ![x, y]

Tactic:
contrapose!
    intro h
    rw [LinearIndependent.pair_iff] at h
    push Not at h
    obtain ⟨r, s, hl, h0⟩ := h
    by_cases hr : r = 0; · simp_all
    by_cases hs : s = 0; · simp_all
    suffices
        (B (r • x) (r • x)) * (B (s • y) (s • y)) = (B (r • x) (s • y)) * (B (s • y) (r • x)) by
      simp only [map_smul, smul_apply, smul_eq_mul] at this
      rw [show r * (r * (B x) x) * (s * (s * (B y) y)) = (r * r * s * s) * ((B x) x * (B y) y) by
        ring, show s * (r * (B x) y) * (r * (s * (B y) x)) = (r * r * s * s) * ((B x) y * (B y) x)
        by ring] at this
      have hrs : r * r * s * s ≠ 0 := by simp [hr, hs]
      exact le_of_eq <| mul_right_injective₀ hrs this
    simp [show s • y = - r • x by rwa [neg_smul, ← add_eq_zero_iff_eq_neg']]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Goal state before:
pp: case zero
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ ((Cone.postcompose
                (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
                    (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
            (G.mapCone c)).π.app
      WalkingParallelPair.zero =
    (Iso.refl
          ((Cone.postcompose
                  (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
              (G.mapCone c)).pt).hom ≫
      (c.map G).π.app WalkingParallelPair.zero

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Goal state before:
pp: case one
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : KernelFork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ ((Cone.postcompose
                (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
                    (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
            (G.mapCone c)).π.app
      WalkingParallelPair.one =
    (Iso.refl
          ((Cone.postcompose
                  (parallelPair.ext (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair f 0 ⋙ G).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
              (G.mapCone c)).pt).hom ≫
      (c.map G).π.app WalkingParallelPair.one

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Goal state before:
pp: case zero
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ ((Cocone.precompose
                  (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
              (G.mapCocone c)).ι.app
        WalkingParallelPair.zero ≫
      (Iso.refl
          ((Cocone.precompose
                  (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
              (G.mapCocone c)).pt).hom =
    (c.map G).ι.app WalkingParallelPair.zero

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Goal state before:
pp: case one
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ ((Cocone.precompose
                  (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
              (G.mapCocone c)).ι.app
        WalkingParallelPair.one ≫
      (Iso.refl
          ((Cocone.precompose
                  (parallelPair.ext (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.zero))
                      (Iso.refl ((parallelPair (G.map f) 0).obj WalkingParallelPair.one)) ⋯ ⋯).hom).obj
              (G.mapCocone c)).pt).hom =
    (c.map G).ι.app WalkingParallelPair.one

Tactic:
cat_disch

Goal state after: