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

Goal state before:
pp: case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (fst g h) (snd f g)
⊢ lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯ ≫ fst (fst f g) (fst f h) = c.snd

Tactic:
apply pullback.hom_ext

Goal state after:
case refine_3.h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (fst g h) (snd f g)
⊢ (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯ ≫ fst (fst f g) (fst f h)) ≫ fst f g = c.snd ≫ fst f g

case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (fst g h) (snd f g)
⊢ (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯ ≫ fst (fst f g) (fst f h)) ≫ snd f g = c.snd ≫ snd f g
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case refine_4
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (fst g h) (snd f g)
m : c.pt ⟶ pullback (fst f g) (fst f h)
hfst : m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = c.fst
hsnd : m ≫ fst (fst f g) (fst f h) = c.snd
⊢ m ≫ snd (fst f g) (fst f h) = lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯ ≫ snd (fst f g) (fst f h)

Tactic:
apply pullback.hom_ext

Goal state after:
case refine_4.h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (fst g h) (snd f g)
m : c.pt ⟶ pullback (fst f g) (fst f h)
hfst : m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = c.fst
hsnd : m ≫ fst (fst f g) (fst f h) = c.snd
⊢ (m ≫ snd (fst f g) (fst f h)) ≫ fst f h =
    (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯ ≫ snd (fst f g) (fst f h)) ≫ fst f h

case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (fst g h) (snd f g)
m : c.pt ⟶ pullback (fst f g) (fst f h)
hfst : m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = c.fst
hsnd : m ≫ fst (fst f g) (fst f h) = c.snd
⊢ (m ≫ snd (fst f g) (fst f h)) ≫ snd f h =
    (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯ ≫ snd (fst f g) (fst f h)) ≫ snd f h
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case refine_4
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (fst g h) (snd f g)
m : c.pt ⟶ pullback (fst f g) (fst f h)
hfst : m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = c.fst
hsnd : m ≫ fst (fst f g) (fst f h) = c.snd
⊢ m ≫ snd (fst f g) (fst f h) = lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯ ≫ snd (fst f g) (fst f h)

Tactic:
apply pullback.hom_ext <;> simp [← hsnd, pullback.condition, ← hfst]

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
inst✝ : P.IsClosedUnderIsomorphisms
h : P.strictColimitsOfShape J ≤ P
⊢ P.colimitsOfShape J ≤ P

Tactic:
conv_rhs => rw [← P.isoClosure_eq_self]
    rw [← isoClosure_strictColimitsOfShape]
    exact monotone_isoClosure h

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
J : Type u'
inst✝¹ : Category.{v', u'} J
P : ObjectProperty D
inst✝ : P.IsClosedUnderIsomorphisms
e : C ≌ D
H : (P.inverseImage e.functor).IsClosedUnderColimitsOfShape J
X : D
⊢ P X ↔ (P.inverseImage e.functor).inverseImage e.inverse X

Tactic:
simpa using P.prop_iff_of_iso (e.counitIso.app X).symm

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X : C
⊢ Function.Injective (@toMonObj C inst✝¹ inst✝ X)

Tactic:
intro h₁

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X : C
h₁ : GrpObj X
⊢ ∀ ⦃a₂ : GrpObj X⦄, h₁.toMonObj = a₂.toMonObj → h₁ = a₂
Module: Mathlib.Data.W.Basic

Goal state before:
pp: case succ.succ
α : Type u_1
β : α → Type u_2
a b : α
ha : Nonempty (β a)
he : IsEmpty (β b)
hf : Finite (WType β)
hba : b ≠ a
n : ℕ
ih :
  ∀ ⦃m : ℕ⦄,
    (fun n ↦
            have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
            this)
          n =
        (fun n ↦
            have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
            this)
          m →
      n = m
m : ℕ
h :
  (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      (n + 1) =
    (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      (m + 1)
⊢ (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      n =
    (fun n ↦
        have this := Nat.recOn n (mk b he.elim') fun x ih ↦ mk a fun x ↦ ih;
        this)
      m

Tactic:
simp_all [funext_iff]

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

Goal state before:
pp: case intro
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 ι
f : ι →₀ R
i : ι
val✝ : Fintype ι
⊢ ∑ d, (f d • b.dualBasis d) (b i) = f i

Tactic:
simp_rw [LinearMap.smul_apply, smul_eq_mul, dualBasis_apply_self, mul_boole,
      Finset.sum_ite_eq, if_pos (Finset.mem_univ i)]

Goal state after:
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 ι
l : Dual R M
i : ι
⊢ b.dualBasis.equivFun l i = l (b i)

Tactic:
by rw [Basis.equivFun_apply, dualBasis_repr]

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

Goal state before:
pp: case inr
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
⊢ False

Tactic:
obtain ⟨e⟩ := lift_mk_le'.mp (card_ιL.trans_eq (lift_uzero #ιL).symm)

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

Goal state before:
pp: R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
⊢ lift.{u, v} (Module.rank R (M' ⧸ Submodule.map f p)) ≤
    lift.{u, v} (Module.rank R (M' ⧸ f.range)) + lift.{v, u} (Module.rank R (M ⧸ p))

Tactic:
rw [rank_quot_submodule_map_eq, lift_add]

Goal state after:
R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
⊢ lift.{u, v} (Module.rank R (M' ⧸ f.range)) +
      lift.{u, v} (Module.rank R (↥f.range ⧸ Submodule.map f.rangeRestrict p)) ≤
    lift.{u, v} (Module.rank R (M' ⧸ f.range)) + lift.{v, u} (Module.rank R (M ⧸ p))
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
s t : Submodule K V
inst✝¹ : FiniteDimensional K ↥s
inst✝ : FiniteDimensional K ↥t
key : Module.rank K ↥(s ⊔ t) + Module.rank K ↥(s ⊓ t) = Module.rank K ↥s + Module.rank K ↥t
⊢ finrank K ↥(s ⊔ t) + finrank K ↥(s ⊓ t) = finrank K ↥s + finrank K ↥t

Tactic:
repeat rw [← finrank_eq_rank] at key

Goal state after:
K : Type u
V : Type v
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
s t : Submodule K V
inst✝¹ : FiniteDimensional K ↥s
inst✝ : FiniteDimensional K ↥t
key : ↑(finrank K ↥(s ⊔ t)) + ↑(finrank K ↥(s ⊓ t)) = ↑(finrank K ↥s) + ↑(finrank K ↥t)
⊢ finrank K ↥(s ⊔ t) + finrank K ↥(s ⊓ t) = finrank K ↥s + finrank K ↥t
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
X Y Z : C
inst✝² : HasLeftDual X
inst✝¹ : HasLeftDual Y
inst✝ : HasLeftDual Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ η_ (ᘁX) X ⊗≫ ᘁX ◁ f ⊗≫ ᘁX ◁ (Y ◁ η_ (ᘁY) Y ⊗≫ ε_ (ᘁY) Y ▷ Y) ⊗≫ ᘁX ◁ g = η_ (ᘁX) X ≫ ᘁX ◁ f ≫ ᘁX ◁ g

Tactic:
rw [coevaluation_evaluation'']

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⊗ X ⟶ Z
⊢ 𝟙 (Y' ⊗ X) ⊗≫ (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') ▷ X ⊗≫ f = f

Tactic:
rw [coevaluation_evaluation'']

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⊗ X ⟶ Z
⊢ 𝟙 (Y' ⊗ X) ⊗≫ ⊗𝟙.hom ▷ X ⊗≫ f = f
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
this : W ⊓ K ∙ v = ⊥
hv₀ : v ≠ 0
aux : finrank K ↥⊤ + 0 = finrank K ↥W + 1
⊢ finrank K (V ⧸ W) = 1

Tactic:
finrank_top,

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : W ⊔ K ∙ v = ⊤
this : W ⊓ K ∙ v = ⊥
hv₀ : v ≠ 0
aux : finrank K V + 0 = finrank K ↥W + 1
⊢ finrank K (V ⧸ W) = 1
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : X ⟶ Z ⊗ Y'
⊢ f ⊗≫ Z ◁ (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') ⊗≫ 𝟙 (Z ⊗ Y') = f

Tactic:
rw [coevaluation_evaluation'']

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : X ⟶ Z ⊗ Y'
⊢ f ⊗≫ Z ◁ ⊗𝟙.hom ⊗≫ 𝟙 (Z ⊗ Y') = f
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⟶ Z
⊢ (Y' ◁ η_ Y Y' ⊗≫ ε_ Y Y' ▷ Y') ⊗≫ f = (ρ_ Y').hom ≫ f

Tactic:
rw [coevaluation_evaluation'']

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
Y Y' Z : C
inst✝ : ExactPairing Y Y'
f : Y' ⟶ Z
⊢  ⊗𝟙.hom ⊗≫ f = (ρ_ Y').hom ≫ f
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
W : Submodule K V
h : finrank K ↥W = finrank K V
⊢ W = ⊤

Tactic:
apply eq_of_le_of_finrank_eq le_top

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
W : Submodule K V
h : finrank K ↥W = finrank K V
⊢ finrank K ↥W = finrank 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✝ : Module.Finite K V
W : Submodule K V
h : finrank K ↥W = finrank K V
⊢ finrank K ↥W = finrank K ↥⊤

Tactic:
finrank_top,

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Module.Finite K V
W : Submodule K V
h : finrank K ↥W = finrank K V
⊢ finrank K ↥W = finrank K V
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✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
⊢ (tensorLeftHomEquiv (𝟙_ C) Y Yᘁ Xᘁ).symm (η_ X Xᘁ ≫ f ▷ Xᘁ) = (ρ_ Yᘁ).hom ≫ fᘁ

Tactic:
dsimp [tensorLeftHomEquiv, rightAdjointMate]
  simp

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

Goal state before:
pp: case refine_2
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
this : finrank K ↥⊤ + finrank K ↥f.ker = finrank K V
h : f.range = ⊤
⊢ f.ker = ⊥

Tactic:
finrank_top,

Goal state after:
case refine_2
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₂
H : finrank K V = finrank K V₂
f : V →ₗ[K] V₂
this : finrank K V₂ + finrank K ↥f.ker = finrank K V
h : f.range = ⊤
⊢ f.ker = ⊥
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

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

Tactic:
by_cases hι : Nonempty ι

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

case neg
K : Type u
inst✝¹ : DivisionRing K
ι : Type u_1
inst✝ : Fintype ι
b : ι → ι → K
hb : LinearIndependent K b
hι : ¬Nonempty ι
⊢ ⇑(basisOfPiSpaceOfLinearIndependent hb) = b
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Ring E
inst✝ : Algebra F E
hr : finrank F E = 2
i : Nontrivial E := nontrivial_of_finrank_pos (LT.lt.trans_eq zero_lt_two (Eq.symm hr))
h : ⊥ = ⊤
⊢ False

Tactic:
by cases hr.symm.trans (Subalgebra.bot_eq_top_iff_finrank_eq_one.1 h)

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✝ : HasRightDual X
f : Y ⟶ Xᘁ
⊢ f ⊗≫ Xᘁ ◁ η_ X Xᘁ ⊗≫ ε_ X Xᘁ ▷ Xᘁ = f ≫ (λ_ Xᘁ).inv

Tactic:
rw [coevaluation_evaluation'']

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : HasRightDual X
f : Y ⟶ Xᘁ
⊢ f ⊗≫ ⊗𝟙.hom = f ≫ (λ_ Xᘁ).inv
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
inst✝ : ExactPairing X' Y
i : X ≅ X'
⊢ Y ◁ η_ X' Y ⊗≫ ε_ X' Y ▷ Y = (ρ_ Y).hom ≫ (λ_ Y).inv

Tactic:
rw [coevaluation_evaluation'']

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X X' Y : C
inst✝ : ExactPairing X' Y
i : X ≅ X'
⊢  ⊗𝟙.hom = (ρ_ Y).hom ≫ (λ_ Y).inv
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
W : Type v'
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Module K W
f : V →ₗ[K] W
p : Submodule K W
inst✝¹ : FiniteDimensional K ↥p
inst✝ : FiniteDimensional K ↥f.ker
⊢ Module.Finite K ↥(comap f p)

Tactic:
← rank_lt_aleph0_iff,

Goal state after:
K : Type u
V : Type v
W : Type v'
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Module K W
f : V →ₗ[K] W
p : Submodule K W
inst✝¹ : FiniteDimensional K ↥p
inst✝ : FiniteDimensional K ↥f.ker
⊢ Module.rank K ↥(comap f p) < ℵ₀
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
W : Type v'
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Module K W
f : V →ₗ[K] W
p : Submodule K V
inst✝¹ : FiniteDimensional K (V ⧸ p)
inst✝ : FiniteDimensional K (W ⧸ f.range)
⊢ Module.Finite K (W ⧸ map f p)

Tactic:
← rank_lt_aleph0_iff,

Goal state after:
K : Type u
V : Type v
W : Type v'
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : Module K W
f : V →ₗ[K] W
p : Submodule K V
inst✝¹ : FiniteDimensional K (V ⧸ p)
inst✝ : FiniteDimensional K (W ⧸ f.range)
⊢ Module.rank K (W ⧸ map f p) < ℵ₀
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' : C
inst✝ : ExactPairing X Y'
i : Y ≅ Y'
⊢ 𝟙 (Y ⊗ 𝟙_ C) ⊗≫ i.hom ⊗≫ (Y' ◁ η_ X Y' ⊗≫ ε_ X Y' ▷ Y') ⊗≫ i.inv ⊗≫ 𝟙 (𝟙_ C ⊗ Y) =
    𝟙 (Y ⊗ 𝟙_ C) ⊗≫ (i.hom ≫ i.inv) ⊗≫ 𝟙 (𝟙_ C ⊗ Y)

Tactic:
rw [coevaluation_evaluation'']

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y Y' : C
inst✝ : ExactPairing X Y'
i : Y ≅ Y'
⊢ 𝟙 (Y ⊗ 𝟙_ C) ⊗≫ i.hom ⊗≫ ⊗𝟙.hom ⊗≫ i.inv ⊗≫ 𝟙 (𝟙_ C ⊗ Y) = 𝟙 (Y ⊗ 𝟙_ C) ⊗≫ (i.hom ≫ i.inv) ⊗≫ 𝟙 (𝟙_ C ⊗ Y)
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
g : P →ₗ[R] N
comp_eq_id : g ∘ₗ f = LinearMap.id
h : Function.Bijective ⇑(dualTensorHom R M P)
⊢ lTensor (Dual R M) g ∘ₗ lTensor (Dual R M) f = LinearMap.id

Tactic:
← lTensor_comp,

Goal state after:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : N →ₗ[R] P
g : P →ₗ[R] N
comp_eq_id : g ∘ₗ f = LinearMap.id
h : Function.Bijective ⇑(dualTensorHom R M P)
⊢ lTensor (Dual R M) (g ∘ₗ f) = LinearMap.id
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 : ∀ (j : WalkingParallelPair), m✝ ≫ (equalizerCone F).π.app j = c.π.app j
J0 : m✝ ≫ (equalizerCone F).π.app WalkingParallelPair.zero = c.π.app WalkingParallelPair.zero
⊢ m✝ = pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯

Tactic:
apply pullback.hom_ext

Goal state after:
case h₀
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
J0 : m✝ ≫ (equalizerCone F).π.app WalkingParallelPair.zero = c.π.app WalkingParallelPair.zero
⊢ m✝ ≫
      pullback.fst (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
        (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) =
    pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯ ≫
      pullback.fst (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
        (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right))

case h₁
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
J0 : m✝ ≫ (equalizerCone F).π.app WalkingParallelPair.zero = c.π.app WalkingParallelPair.zero
⊢ m✝ ≫
      pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
        (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) =
    pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯ ≫
      pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
        (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right))
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: R : Type u_7
M : Type u_8
N : Type u_9
ι : Type u_10
κ : Type u_11
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
⊢ dualDistrib R M N ∘ₗ dualDistribInvOfBasis b c = LinearMap.id

Tactic:
apply (b.tensorProduct c).dualBasis.ext

Goal state after:
R : Type u_7
M : Type u_8
N : Type u_9
ι : Type u_10
κ : Type u_11
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
⊢ ∀ (i : ι × κ),
    (dualDistrib R M N ∘ₗ dualDistribInvOfBasis b c) ((b.tensorProduct c).dualBasis i) =
      LinearMap.id ((b.tensorProduct c).dualBasis i)
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
x y : M
⊢ (B x) x * ((B x) y * (B x) y) - (B x) x * ((B x) y * (B y) x) -
      ((B x) x * ((B x) y * (B x) y) - (B x) x * ((B x) x * (B y) y)) =
    (B x) x * ((B x) x * (B y) y) - (B x) x * ((B x) y * (B y) x)

Tactic:
abel

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)
φ : Dual 𝕜 (E →ₗ[𝕜] 𝕜)
φne : φ K ≠ 0
hφ : map φ (span 𝕜 (Set.range L)) = ⊥
φs : E := (evalEquiv 𝕜 E).symm φ
this : K φs = 0
⊢ False

Tactic:
simp only [apply_evalEquiv_symm_apply, φs, φne] at this

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
⊢ K ∈ span 𝕜 (Set.range L)

Tactic:
let ψ : (E ⧸ p) →ₗ[𝕜] ι → 𝕜 := p.liftQ φ p_eq.le

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 φ ⋯
⊢ K ∈ span 𝕜 (Set.range L)
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
inst✝ : FiniteDimensional K V₁
⊢ finrank K ↥⊤ = 1

Tactic:
finrank_top,

Goal state after:
K : Type u_1
V₁ : Type u_2
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V₁
inst✝¹ : Module K V₁
f : Dual K V₁
hf : f ≠ 0
inst✝ : FiniteDimensional K V₁
⊢ finrank K K = 1