mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x : WithInitial Cᵒᵖ
⊢ (match x, x, 𝟙 x with
    | WithInitial.of (op x), WithInitial.of (op y), f => WithInitial.down f
    | WithInitial.star, WithInitial.of (op unop), x =>
      op
        (starTerminal.from
          (Opposite.unop
            (match WithInitial.of (op unop) with
            | WithInitial.of x => op (of (Opposite.unop x))
            | WithInitial.star => op star)))
    | WithInitial.star, WithInitial.star, x =>
      𝟙
        (match WithInitial.star with
        | WithInitial.of x => op (of (unop x))
        | WithInitial.star => op star)) =
    𝟙
      (match x with
      | WithInitial.of x => op (of (unop x))
      | WithInitial.star => op star)

Tactic:
by cases x <;> rfl

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝ : (WithInitial C)ᵒᵖ
x : WithInitial C
⊢ (match 𝟙 (op x) with
    | op f =>
      match op x, op x, f, 𝟙 (op x) with
      | op (of x), op (of y), f, x_1 => (WithTerminal.down f).op
      | op (of a), op star, x, x_1 =>
        WithTerminal.starTerminal.from
          (match op (of a) with
          | op x =>
            match x with
            | of x => WithTerminal.of (op x)
            | star => WithTerminal.star)
      | op star, op star, x, x_1 =>
        𝟙
          (match op star with
          | op x =>
            match x with
            | of x => WithTerminal.of (op x)
            | star => WithTerminal.star)) =
    𝟙
      (match op x with
      | op x =>
        match x with
        | of x => WithTerminal.of (op x)
        | star => WithTerminal.star)

Tactic:
by cases x <;> rfl

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x : WithTerminal Cᵒᵖ
⊢ (match x, x, 𝟙 x with
    | WithTerminal.of (op x), WithTerminal.of (op y), f => down f
    | WithTerminal.of (op unop), WithTerminal.star, x =>
      op
        (starInitial.to
          (Opposite.unop
            (match WithTerminal.of (op unop) with
            | WithTerminal.of x => op (of (Opposite.unop x))
            | WithTerminal.star => op star)))
    | WithTerminal.star, WithTerminal.star, x =>
      𝟙
        (match WithTerminal.star with
        | WithTerminal.of x => op (of (unop x))
        | WithTerminal.star => op star)) =
    𝟙
      (match x with
      | WithTerminal.of x => op (of (unop x))
      | WithTerminal.star => op star)

Tactic:
by cases x <;> rfl

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
inst✝² : P.IsStableUnderCobaseChange
S S' X Y : C
f : S ⟶ S'
v₂₂ : S ⟶ Y
g : Y ⟶ X
inst✝¹ : HasPushout v₂₂ f
H : P g
inst✝ : HasPushout (v₂₂ ≫ g) f
⊢ P (pushout.desc (g ≫ pushout.inl (v₂₂ ≫ g) f) (pushout.inr (v₂₂ ≫ g) f) ⋯)

Tactic:
refine IsStableUnderCobaseChangeAlong.of_isPushout (f' := pushout.inl (v₂₂ ≫ g) f)
    (f := pushout.inl v₂₂ f) ?_ H

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
P : MorphismProperty C
inst✝² : P.IsStableUnderCobaseChange
S S' X Y : C
f : S ⟶ S'
v₂₂ : S ⟶ Y
g : Y ⟶ X
inst✝¹ : HasPushout v₂₂ f
H : P g
inst✝ : HasPushout (v₂₂ ≫ g) f
⊢ IsPushout (pushout.inl v₂₂ f) g (pushout.desc (g ≫ pushout.inl (v₂₂ ≫ g) f) (pushout.inr (v₂₂ ≫ g) f) ⋯)
    (pushout.inl (v₂₂ ≫ g) f)
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange P
hP' : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
H : P (CommRingCat.Hom.hom g)
this✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
this : Algebra ↑R ↑T := (CommRingCat.Hom.hom g).toAlgebra
⊢ P (CommRingCat.Hom.hom (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom))

Tactic:
apply hP R T S (S ⊗[R] T)

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange P
hP' : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
H : P (CommRingCat.Hom.hom g)
this✝ : Algebra ↑R ↑S := ⋯
this : Algebra ↑R ↑T := ⋯
⊢ P (algebraMap ↑R ↑T)
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
this : MonObj X := ofRepresentableBy X F α
Y : Cᵒᵖ
f₁ f₂ : unop Y ⟶ X
⊢ α.homEquiv'.toFun (f₁ * f₂) = α.homEquiv'.toFun f₁ * α.homEquiv'.toFun f₂

Tactic:
change α.homEquiv' (lift f₁ f₂ ≫ α.homEquiv'.symm (α.homEquiv' (fst X X) *
          α.homEquiv' (snd X X))) = α.homEquiv' f₁ * α.homEquiv' f₂

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
this : MonObj X := ofRepresentableBy X F α
Y : Cᵒᵖ
f₁ f₂ : unop Y ⟶ X
⊢ α.homEquiv' (lift f₁ f₂ ≫ α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X))) =
    α.homEquiv' f₁ * α.homEquiv' f₂
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
⊢ (β_ X Y).inv ≫ fst X Y = snd Y X

Tactic:
simp [fst_def, snd_def, ← BraidedCategory.braiding_inv_naturality_left_assoc]

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 ι
⊢ (algebraMap R A) (counit a) = (algebraMap R A) (counit a) * 1

Tactic:
mul_one

Goal state after:
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 ι
⊢ (algebraMap R A) (counit a) = (algebraMap R A) (counit a)
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: 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 ι
m : M
i : ι
⊢ (b.toDual m) (b i) = b.equivFun m i

Tactic:
rw [b.equivFun_apply, toDual_eq_repr]

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

Goal state before:
pp: K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
⊢ (db.coprod eb).range = ⊤

Tactic:
range_coprod,

Goal state after:
K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
⊢ db.range ⊔ eb.range = ⊤
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 ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥((s ⊔ t) ⊓ t) + Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(s ⊓ (s ⊓ t)) + Module.rank R ↥((s ⊔ t) ⊓ t)

Tactic:
← inf_assoc,

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 (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥((s ⊔ t) ⊓ t) + Module.rank R ↥(s ⊓ t) =
    Module.rank R (↥(s ⊔ t) ⧸ comap (s ⊔ t).subtype t) + Module.rank R ↥(s ⊓ s ⊓ t) + Module.rank R ↥((s ⊔ t) ⊓ 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
A : Type u_1
inst✝³ : Semiring A
inst✝² : Module A V
inst✝¹ : SMul K A
inst✝ : IsScalarTower K A V
h : finrank K V = 1
this : Nontrivial V
S : Submodule A V
hn : ¬restrictScalars K S = restrictScalars K ⊥
⊢ restrictScalars K S = restrictScalars K ⊤

Tactic:
have : FiniteDimensional _ _ := .of_finrank_eq_succ h

Goal state after:
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
A : Type u_1
inst✝³ : Semiring A
inst✝² : Module A V
inst✝¹ : SMul K A
inst✝ : IsScalarTower K A V
h : finrank K V = 1
this✝ : Nontrivial V
S : Submodule A V
hn : ¬restrictScalars K S = restrictScalars K ⊥
this : FiniteDimensional K V
⊢ restrictScalars K S = restrictScalars K ⊤
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
m : ℕ
hm : finrank K V ≤ m
⊢ LinearMap.ker (f ^ m) = LinearMap.ker (f ^ finrank K V)

Tactic:
obtain ⟨k, h_k_le, hk⟩ :
    ∃ k, k ≤ finrank K V ∧ LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ) :=
    exists_ker_pow_eq_ker_pow_succ f

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
hm : finrank K V ≤ m
k : ℕ
h_k_le : k ≤ finrank K V
hk : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
⊢ LinearMap.ker (f ^ m) = LinearMap.ker (f ^ finrank K V)
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix

Goal state before:
pp: R : Type u
S : Type u'
M : Type v
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : StrongRankCondition R
inst✝² : StrongRankCondition S
inst✝¹ : Module R S
inst✝ : SMulCommClass R S S
⊢ lift.{u', v} (Module.rank R M) * 1 = lift.{u', v} (Module.rank R M)

Tactic:
mul_one

Goal state after:
R : Type u
S : Type u'
M : Type v
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : StrongRankCondition R
inst✝² : StrongRankCondition S
inst✝¹ : Module R S
inst✝ : SMulCommClass R S S
⊢ lift.{u', v} (Module.rank R M) = lift.{u', v} (Module.rank R M)
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix

Goal state before:
pp: R : Type u
S : Type u'
M : Type v
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : StrongRankCondition R
inst✝² : StrongRankCondition S
inst✝¹ : Module R S
inst✝ : SMulCommClass R S S
⊢ finrank R M * 1 = finrank R M

Tactic:
mul_one

Goal state after:
R : Type u
S : Type u'
M : Type v
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : StrongRankCondition R
inst✝² : StrongRankCondition S
inst✝¹ : Module R S
inst✝ : SMulCommClass R S S
⊢ finrank R M = finrank R M
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 f' : M → M₁
g g' : M₁ → M
h : B.IsAdjointPair B' f g
h' : B.IsAdjointPair B' f' g'
x : M
x✝ : M₁
⊢ (B' ((f - f') x)) x✝ = (B x) ((g - g') x✝)

Tactic:
Pi.sub_apply,

Goal state after:
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 f' : M → M₁
g g' : M₁ → M
h : B.IsAdjointPair B' f g
h' : B.IsAdjointPair B' f' g'
x : M
x✝ : M₁
⊢ (B' (f x - f' x)) x✝ = (B x) ((g - g') x✝)
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 f' : M → M₁
g g' : M₁ → M
h : B.IsAdjointPair B' f g
h' : B.IsAdjointPair B' f' g'
x : M
x✝ : M₁
⊢ (B' (f x - f' x)) x✝ = (B x) ((g - g') x✝)

Tactic:
Pi.sub_apply,

Goal state after:
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 f' : M → M₁
g g' : M₁ → M
h : B.IsAdjointPair B' f g
h' : B.IsAdjointPair B' f' g'
x : M
x✝ : M₁
⊢ (B' (f x - f' x)) x✝ = (B x) (g x✝ - g' x✝)
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

Goal state after:
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.flip.IsOrthoᵢ ⇑v
hB : B.SeparatingRight
i : n
⊢ (B (v i)) (v i) ≠ 0
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type uK
V : Type uV
inst✝¹⁰ : CommSemiring K
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module K V
inst✝⁷ : Projective K V
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : IsReflexive R M
inst✝ : IsReflexive R N
⊢ Bijective ⇑(Dual.eval R (M × N))

Tactic:
let e : Dual R (Dual R (M × N)) ≃ₗ[R] Dual R (Dual R M) × Dual R (Dual R N) :=
      (dualProdDualEquivDual R M N).dualMap.trans
        (dualProdDualEquivDual R (Dual R M) (Dual R N)).symm

Goal state after:
K : Type uK
V : Type uV
inst✝¹⁰ : CommSemiring K
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module K V
inst✝⁷ : Projective K V
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : IsReflexive R M
inst✝ : IsReflexive R N
e : Dual R (Dual R (M × N)) ≃ₗ[R] Dual R (Dual R M) × Dual R (Dual R N) :=
  (dualProdDualEquivDual R M N).dualMap ≪≫ₗ (dualProdDualEquivDual R (Dual R M) (Dual R N)).symm
⊢ Bijective ⇑(Dual.eval R (M × N))
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case inr.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
hy : (B y) y ≤ 0
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y

Tactic:
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.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✝ : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, (L i).ker ≤ K.ker
hK : K ∉ span 𝕜 (Set.range L)
⊢ False

Tactic:
rcases exists_dual_map_eq_bot_of_notMem hK inferInstance with ⟨φ, φne, hφ⟩

Goal state after:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, (L i).ker ≤ K.ker
hK : K ∉ span 𝕜 (Set.range L)
φ : Dual 𝕜 (E →ₗ[𝕜] 𝕜)
φne : φ K ≠ 0
hφ : map φ (span 𝕜 (Set.range L)) = ⊥
⊢ False
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:
enter [2]; intro i; rw [← p.liftQ_mkQ (L i) (iInf_le _ i)]

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'
i : ι
| c i • p.liftQ (L i) ⋯ ∘ₗ p.mkQ
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
x y : M
hle : ∀ (z : M), 0 ≤ (B z) z
r s : R
hl : r • x + s • y = 0
h0 : r = 0 → s ≠ 0
hr : ¬r = 0
hs : ¬s = 0
this : r * (r * (B x) x) * (s * (s * (B y) y)) = s * (r * (B x) y) * (r * (s * (B y) x))
⊢ (B x) x * (B y) y ≤ (B x) y * (B y) x

Tactic:
show r * (r * (B x) x) * (s * (s * (B y) y)) = (r * r * s * s) * ((B x) x * (B y) y) by
        ring,

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
x y : M
hle : ∀ (z : M), 0 ≤ (B z) z
r s : R
hl : r • x + s • y = 0
h0 : r = 0 → s ≠ 0
hr : ¬r = 0
hs : ¬s = 0
this : r * r * s * s * ((B x) x * (B y) y) = s * (r * (B x) y) * (r * (s * (B y) x))
⊢ (B x) x * (B y) y ≤ (B x) y * (B y) x
Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∏ᶜ K.obj
Q : C := ∏ᶜ fun f ↦ K.obj f.fst.2
s : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
f : (p : J × J) × (p.1 ⟶ p.2)
⊢ G.map (Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd) ≫
      G.map (Pi.π (fun f ↦ K.obj f.fst.2) f) =
    G.map (Pi.π K.obj f.fst.1) ≫ G.map (K.map f.snd)

Tactic:
simp only [← G.map_comp, limit.lift_π]

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∏ᶜ K.obj
Q : C := ∏ᶜ fun f ↦ K.obj f.fst.2
s : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
f : (p : J × J) × (p.1 ⟶ p.2)
⊢ G.map
      ((Fan.mk (∏ᶜ K.obj) fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd).π.app { as := f }) =
    G.map (Pi.π K.obj f.fst.1 ≫ K.map f.snd)
Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∏ᶜ K.obj
Q : C := ∏ᶜ fun f ↦ K.obj f.fst.2
s : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
f : (p : J × J) × (p.1 ⟶ p.2)
⊢ G.map (Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.2 }) ≫ G.map (Pi.π (fun f ↦ K.obj f.fst.2) f) =
    G.map (Pi.π K.obj f.fst.2)

Tactic:
simp only [← G.map_comp, limit.lift_π]

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∏ᶜ K.obj
Q : C := ∏ᶜ fun f ↦ K.obj f.fst.2
s : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.1 } ≫ K.map f.snd
t : P ⟶ Q := Pi.lift fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
f : (p : J × J) × (p.1 ⟶ p.2)
⊢ G.map ((Fan.mk (∏ᶜ K.obj) fun f ↦ limit.π (Discrete.functor K.obj) { as := f.fst.2 }).π.app { as := f }) =
    G.map (Pi.π K.obj f.fst.2)
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_3
V₁ : Type u_4
V₂ : Type u_5
inst✝⁴ : Field K
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
⊢ Function.Surjective ⇑f.dualMap ↔ Function.Injective ⇑f

Tactic:
by
  rw [← LinearMap.range_eq_top, range_dualMap_eq_dualAnnihilator_ker,
      ← Submodule.dualAnnihilator_bot, Subspace.dualAnnihilator_inj, LinearMap.ker_eq_bot]

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

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

Tactic:
rw [iInf_option, iSup_option, dualAnnihilator_inf_eq, h]

Goal state after: