mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Adjunction.Comma

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : (⊥_ StructuredArrow A G).right ⟶ B
B' : StructuredArrow A G := StructuredArrow.mk ((⊥_ StructuredArrow A G).hom ≫ G.map g)
g' : ⊥_ StructuredArrow A G ⟶ B' := StructuredArrow.homMk g ⋯
⊢ (fun f ↦ (initial.to (StructuredArrow.mk f)).right) ((fun g ↦ (⊥_ StructuredArrow A G).hom ≫ G.map g) g) = g

Tactic:
have : initial.to _ = g' := by cat_disch

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : (⊥_ StructuredArrow A G).right ⟶ B
B' : StructuredArrow A G := StructuredArrow.mk ((⊥_ StructuredArrow A G).hom ≫ G.map g)
g' : ⊥_ StructuredArrow A G ⟶ B' := StructuredArrow.homMk g ⋯
this : initial.to B' = g'
⊢ (fun f ↦ (initial.to (StructuredArrow.mk f)).right) ((fun g ↦ (⊥_ StructuredArrow A G).hom ≫ G.map g) g) = g
Module: Mathlib.CategoryTheory.Adjunction.Comma

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
G : D ⥤ C
inst✝ : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
f : A ⟶ G.obj B
⊢ (fun g ↦ (⊥_ StructuredArrow A G).hom ≫ G.map g) ((fun f ↦ (initial.to (StructuredArrow.mk f)).right) f) = f

Tactic:
by
    let B' : StructuredArrow A G := StructuredArrow.mk f
    apply (CommaMorphism.w (initial.to B')).symm.trans (Category.id_comp _)

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case map_units
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
⊢ ∀ (x : ↥M), IsUnit ((algebraMap R (End R S')) ↑x)

Tactic:
intro x
    rw [Module.End.isUnit_iff]
    constructor
    · rintro a b (e : x • a = x • b)
      simp_rw [Submonoid.smul_def, Algebra.smul_def] at e
      exact (h₁ x x.2).mul_left_cancel e
    · intro a
      refine ⟨((h₁ x x.2).unit⁻¹ :) * a, ?_⟩
      rw [Module.algebraMap_end_apply, Algebra.smul_def, ← mul_assoc, IsUnit.mul_val_inv, one_mul]

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : CommRing A
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module A N
inst✝⁵ : Algebra R A
inst✝⁴ : Module R N
inst✝³ : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
hS : ∀ s ∈ S, s ≠ 0 → IsRegular s
inst✝² : IsTorsionFree R M
inst✝¹ : IsLocalization S A
inst✝ : IsLocalizedModule S f
c : A
hc : IsRegular c
x y : N
hxy : (fun x ↦ c • x) x = (fun x ↦ c • x) y
hS₀ : 0 ∉ S
⊢ x = y

Tactic:
obtain ⟨⟨a, s⟩, rfl⟩ := IsLocalization.mk'_surjective S c

Goal state after:
case neg
R : Type u_1
M : Type u_2
A : Type u_3
N : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : CommRing A
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module A N
inst✝⁵ : Algebra R A
inst✝⁴ : Module R N
inst✝³ : IsScalarTower R A N
f : M →ₗ[R] N
S : Submonoid R
hS : ∀ s ∈ S, s ≠ 0 → IsRegular s
inst✝² : IsTorsionFree R M
inst✝¹ : IsLocalization S A
inst✝ : IsLocalizedModule S f
x y : N
hS₀ : 0 ∉ S
a : R
s : ↥S
hc :
  IsRegular
    ((fun x ↦
        match x with
        | (r, m) => IsLocalization.mk' A r m)
      (a, s))
hxy :
  (fun x ↦
        (fun x ↦
              match x with
              | (r, m) => IsLocalization.mk' A r m)
            (a, s) •
          x)
      x =
    (fun x ↦
        (fun x ↦
              match x with
              | (r, m) => IsLocalization.mk' A r m)
            (a, s) •
          x)
      y
⊢ x = y
Module: Mathlib.RingTheory.Finiteness.Ideal

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
n : ℕ
hI : I.FG
⊢ (I ^ Nat.zero).FG

Tactic:
by rw [I.pow_zero, one_eq_top]; exact fg_top R

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

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
F : C ⥤ D
inst✝ : LocallySmall.{w, v_1, u_1} C
H₁ : ObjectProperty.EssentiallySmall.{w, v_2, u_2} F.essImage
H₂ : ∀ (Y : D), ObjectProperty.EssentiallySmall.{w, v_1, u_1} fun x ↦ Nonempty (F.obj x ≅ Y)
Y : D
⊢ ⊤.map F Y ≤ F.essImage Y

Tactic:
by simp [ObjectProperty.map, Functor.essImage]

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type (max w v)
X✝ Y✝ : CostructuredArrow uliftYoneda.{w, v, u} F
f : X✝ ⟶ Y✝
⊢ (ConcreteCategory.hom (F.map f.left.op)) (F.elementsMk (op Y✝.left) (uliftYonedaEquiv Y✝.hom)).snd =
    (F.elementsMk (op X✝.left) (uliftYonedaEquiv X✝.hom)).snd

Tactic:
by
        dsimp
        rw [← CostructuredArrow.w f, uliftYonedaEquiv_naturality, Quiver.Hom.unop_op]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : HasPushout f f
h : IsColimit (Cofork.ofπ f.unop ⋯)
⊢ (Iso.refl (Opposite.op (Opposite.unop Y))).hom ≫ pushout.inr f f =
    (pullback.snd f.unop f.unop).op ≫ (pushoutIsoOpPullback f f).symm.hom

Tactic:
· rw [Iso.symm_hom, ← Quiver.Hom.op_unop (pushoutIsoOpPullback f f).inv, ← op_comp,
        pushoutIsoOpPullback_inv_snd, Quiver.Hom.op_unop, Iso.refl_hom, Category.id_comp]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
l₁ : (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
l : s.pt ⟶ (Fork.ofι h ⋯).pt
hl : l ≫ (Fork.ofι h ⋯).ι = s.ι ≫ k
p : s.pt ⟶ (PullbackCone.mk f g comm).pt
left✝ : p ≫ (PullbackCone.mk f g comm).fst = l
hp₂ : p ≫ (PullbackCone.mk f g comm).snd = s.ι
m : s.pt ⟶ (Fork.ofι g ⋯).pt
w : m ≫ (Fork.ofι g ⋯).ι = s.ι
z : m ≫ g = p ≫ g
this : Mono h
⊢ ∀ (j : WalkingCospan), m ≫ (PullbackCone.mk f g comm).π.app j = p ≫ (PullbackCone.mk f g comm).π.app j

Tactic:
apply (PullbackCone.mk f g comm).equalizer_ext

Goal state after:
case h₀
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
l₁ : (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
l : s.pt ⟶ (Fork.ofι h ⋯).pt
hl : l ≫ (Fork.ofι h ⋯).ι = s.ι ≫ k
p : s.pt ⟶ (PullbackCone.mk f g comm).pt
left✝ : p ≫ (PullbackCone.mk f g comm).fst = l
hp₂ : p ≫ (PullbackCone.mk f g comm).snd = s.ι
m : s.pt ⟶ (Fork.ofι g ⋯).pt
w : m ≫ (Fork.ofι g ⋯).ι = s.ι
z : m ≫ g = p ≫ g
this : Mono h
⊢ m ≫ (PullbackCone.mk f g comm).fst = p ≫ (PullbackCone.mk f g comm).fst

case h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
l₁ : (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
l : s.pt ⟶ (Fork.ofι h ⋯).pt
hl : l ≫ (Fork.ofι h ⋯).ι = s.ι ≫ k
p : s.pt ⟶ (PullbackCone.mk f g comm).pt
left✝ : p ≫ (PullbackCone.mk f g comm).fst = l
hp₂ : p ≫ (PullbackCone.mk f g comm).snd = s.ι
m : s.pt ⟶ (Fork.ofι g ⋯).pt
w : m ≫ (Fork.ofι g ⋯).ι = s.ι
z : m ≫ g = p ≫ g
this : Mono h
⊢ m ≫ (PullbackCone.mk f g comm).snd = p ≫ (PullbackCone.mk f g comm).snd
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
inst✝ : IsFilteredOrEmpty C
X Y : D
f g : X ⟶ Y
P : StructuredArrow X F → Prop := fun h ↦ ∃ Z q₁ q₂, h.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
Z : C
q₁ : (StructuredArrow.mk (g ≫ Final.homToLift F Y)).right ⟶ Z
q₂ : Final.lift F Y ⟶ Z
h : (StructuredArrow.mk (g ≫ Final.homToLift F Y)).hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
⊢ ∃ Z h, f ≫ h = g ≫ h

Tactic:
refine ⟨F.obj (IsFiltered.coeq q₁ q₂),
        Final.homToLift F Y ≫ F.map (q₁ ≫ IsFiltered.coeqHom q₁ q₂), ?_⟩

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
inst✝ : IsFilteredOrEmpty C
X Y : D
f g : X ⟶ Y
P : StructuredArrow X F → Prop := fun h ↦ ∃ Z q₁ q₂, h.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
Z : C
q₁ : (StructuredArrow.mk (g ≫ Final.homToLift F Y)).right ⟶ Z
q₂ : Final.lift F Y ⟶ Z
h : (StructuredArrow.mk (g ≫ Final.homToLift F Y)).hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
⊢ f ≫ Final.homToLift F Y ≫ F.map (q₁ ≫ IsFiltered.coeqHom q₁ q₂) =
    g ≫ Final.homToLift F Y ≫ F.map (q₁ ≫ IsFiltered.coeqHom q₁ q₂)
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y B X : C
f : X ⟶ B
inst✝ : EffectiveEpi f
c : PullbackCone f f
hc : IsLimit c
s : Cocone (parallelPair c.fst c.snd)
Z✝ : C
g₁ g₂ : Z✝ ⟶ X
hg : g₁ ≫ f = g₂ ≫ f
⊢ g₁ ≫ Cofork.π s = PullbackCone.IsLimit.lift hc g₁ g₂ hg ≫ c.snd ≫ Cofork.π s

Tactic:
← Cofork.app_zero_eq_comp_π_right

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y B X : C
f : X ⟶ B
inst✝ : EffectiveEpi f
c : PullbackCone f f
hc : IsLimit c
s : Cocone (parallelPair c.fst c.snd)
Z✝ : C
g₁ g₂ : Z✝ ⟶ X
hg : g₁ ≫ f = g₂ ≫ f
⊢ g₁ ≫ Cofork.π s = PullbackCone.IsLimit.lift hc g₁ g₂ hg ≫ s.ι.app WalkingParallelPair.zero
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
X₁ X₂ : J ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
hφ : ∀ (j : J), c₁.ι.app j ≫ h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } = f.app j ≫ c₂.ι.app j
⊢ W.colimitsOfShape J (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })

Tactic:
exact ⟨_, _, _, _, _, h₂, _, hf⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
X Y : C
f : X ⟶ Y
J : Type w'
hf : W.colimitsOfShape (Discrete J) f
inst✝ : Small.{w, w'} J
⊢ coproducts.{w, v, u} W f

Tactic:
rw [coproducts_iff]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
X Y : C
f : X ⟶ Y
J : Type w'
hf : W.colimitsOfShape (Discrete J) f
inst✝ : Small.{w, w'} J
⊢ ∃ J, W.colimitsOfShape (Discrete J) f
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: 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
⊢ IsPullback (map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯) (fst (fst f g) (fst f h)) (fst g h) (snd f g)

Tactic:
refine ⟨⟨by simp⟩, ⟨PullbackCone.IsLimit.mk _ ?_ ?_ ?_ ?_⟩⟩

Goal state after:
case refine_1
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
⊢ (s : PullbackCone (fst g h) (snd f g)) → s.pt ⟶ pullback (fst f g) (fst f h)

case refine_2
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
⊢ ∀ (s : PullbackCone (fst g h) (snd f g)), ?refine_1 s ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = s.fst

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
⊢ ∀ (s : PullbackCone (fst g h) (snd f g)), ?refine_1 s ≫ fst (fst f g) (fst f h) = s.snd

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
⊢ ∀ (s : PullbackCone (fst g h) (snd f g)) (m : s.pt ⟶ pullback (fst f g) (fst f h)),
    m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = s.fst →
      m ≫ fst (fst f g) (fst f h) = s.snd → m = ?refine_1 s
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 : X ⟶ M
⊢ f * 1 = f

Tactic:
change lift f (toUnit _ ≫ η) ≫ μ = 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 : X ⟶ M
⊢ lift f (toUnit X ≫ η) ≫ μ = f
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 X : C
inst✝¹ : MonObj M
F : C ⥤ D
inst✝ : F.Monoidal
f g : X ⟶ M
⊢ F.map (f * g) = F.map f * F.map g

Tactic:
by
  simp [Hom.mul_def]

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
inst✝ : F.OplaxMonoidal
X Y : C
⊢ δ F X Y ≫ fst (F.obj X) (F.obj Y) = F.map (fst X Y)

Tactic:
by
  trans F.map (X ◁ toUnit Y) ≫ F.map (ρ_ X).hom
  · rw [← whiskerLeft_fst _ (F.map (toUnit Y)), δ_natural_right_assoc]
    simp [← OplaxMonoidal.right_unitality_hom, rightUnitor_hom (F.obj X)]
  · simp [← Functor.map_comp, rightUnitor_hom]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : HopfAlgebra R A
⊢ toConv (toConv (antipodeAlgHom R A) * toConv (AlgHom.id R A)).ofConv.toLinearMap = toConv (ofConv 1).toLinearMap

Tactic:
rw [AlgHom.toLinearMap_convMul, AlgHom.toLinearMap_convOne]

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : HopfAlgebra R A
⊢ toConv (toConv (antipodeAlgHom R A)).ofConv.toLinearMap * toConv (toConv (AlgHom.id R A)).ofConv.toLinearMap = 1
Module: Mathlib.Logic.Equiv.Multiset

Goal state before:
pp: m : ℕ
l : List ℕ
n : ℕ
⊢ m :: lower (raise l (m + n)) (m + n) = m :: l

Tactic:
lower_raise l

Goal state after:
m : ℕ
l : List ℕ
n : ℕ
⊢ m :: l = m :: l
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Function.Surjective (WType.elim (↥(closure s)) (operate s))

Tactic:
rw [← Set.range_eq_univ]
  exact SetLike.coe_set_eq.mpr (rangeOfWType_eq_top s)

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

Tactic:
by
  rw [b.equivFun_apply, toDual_eq_repr]

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

Goal state before:
pp: case e_a.e_a.e_a
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
⊢ (λ_ ᘁZ).inv ≫ η_ (ᘁX) X ▷ ᘁZ ≫ (ᘁX ◁ f ≫ ᘁX ◁ g) ▷ ᘁZ =
    (λ_ ᘁZ).inv ≫
      η_ (ᘁY) Y ▷ ᘁZ ≫
        ((λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (ᘁX ◁ f) ▷ ᘁY ≫ (α_ (ᘁX) Y ᘁY).hom ≫ ᘁX ◁ ε_ (ᘁY) Y ≫ (ρ_ ᘁX).hom ⊗ₘ g) ▷ ᘁZ

Tactic:
simp only [← comp_whiskerRight]

Goal state after:
case e_a.e_a.e_a
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
⊢ (λ_ ᘁZ).inv ≫ (η_ (ᘁX) X ≫ ᘁX ◁ f ≫ ᘁX ◁ g) ▷ ᘁZ =
    (λ_ ᘁZ).inv ≫
      (η_ (ᘁY) Y ≫
          ((λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (ᘁX ◁ f) ▷ ᘁY ≫ (α_ (ᘁX) Y ᘁY).hom ≫ ᘁX ◁ ε_ (ᘁY) Y ≫ (ρ_ ᘁX).hom ⊗ₘ g)) ▷
        ᘁZ
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
U W : Submodule K V
h : IsCompl U W
⊢ finrank K ↥(U ⊔ W) + finrank K ↥(U ⊓ W) = finrank K V

Tactic:
h.codisjoint.eq_top,

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
U W : Submodule K V
h : IsCompl U W
⊢ finrank K ↥⊤ + finrank K ↥(U ⊓ W) = finrank K V
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)
n : ℕ
⊢ n ≤ (finrank K V).succ → n ≤ finrank K ↥(LinearMap.ker (f ^ n))

Tactic:
hn

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
h_contra : ∀ x ≤ finrank K V, ¬LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ)
n : ℕ
hn : n ≤ (finrank K V).succ
⊢ n ≤ finrank K ↥(LinearMap.ker (f ^ n))
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case neg
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 i' : n
j' : m
hij : ¬i = i' ∨ ¬j = j'
⊢ (toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) i' j' = Matrix.single i j 1 i' j'

Tactic:
rcases hij with hij | hij

Goal state after:
case neg.inl
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 i' : n
j' : m
hij : ¬i = i'
⊢ (toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) i' j' = Matrix.single i j 1 i' j'

case neg.inr
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 i' : n
j' : m
hij : ¬j = j'
⊢ (toMatrix bM bN) ((dualTensorHom R M N) (bM.coord j ⊗ₜ[R] bN i)) i' j' = Matrix.single i j 1 i' j'
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case mp
R : Type u_1
R₁ : Type u_2
M₁ : Type u_6
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I : R₁ →+* R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : B.IsAlt
x✝¹ x✝ : M₁
⊢ (B x✝¹) x✝ = ((-B.flip) x✝¹) x✝

Tactic:
neg_apply,

Goal state after:
case mp
R : Type u_1
R₁ : Type u_2
M₁ : Type u_6
inst✝⁵ : CommRing R
inst✝⁴ : CommSemiring R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
I : R₁ →+* R
inst✝¹ : NoZeroDivisors R
inst✝ : CharZero R
B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R
h : B.IsAlt
x✝¹ x✝ : M₁
⊢ (B x✝¹) x✝ = -(B.flip x✝¹) x✝
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
⊢ ∀ (s : Cone F) (m : s.pt ⟶ (equalizerCone F).pt),
    (∀ (j : WalkingParallelPair), m ≫ (equalizerCone F).π.app j = s.π.app j) →
      m = pullback.lift (s.π.app WalkingParallelPair.zero) (s.π.app WalkingParallelPair.zero) ⋯

Tactic:
intro c _ J
    have J0 := J WalkingParallelPair.zero
    apply pullback.hom_ext
    · simpa [limit.lift_π] using J0
    · simp [← J0, pullbackFst_eq_pullback_snd]

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₁
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
⊢ B.SeparatingRight

Tactic:
rw [isOrthoᵢ_flip] at hO
  rw [← flip_separatingLeft]
  refine IsOrthoᵢ.separatingLeft_of_not_isOrtho_basis_self v hO fun i ↦ ?_
  exact h i

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

Goal state before:
pp: case neg
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
⊢ (B (r • x)) (r • x) * (B (s • y)) (s • y) = (B (r • x)) (s • y) * (B (s • y)) (r • x)

Tactic:
simp [show s • y = - r • x by rwa [neg_smul, ← add_eq_zero_iff_eq_neg']]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R M
⊢ W.dualAnnihilator = ⊥ ↔ Subsingleton (Dual R (M ⧸ W))

Tactic:
rw [W.dualQuotEquivDualAnnihilator.toEquiv.subsingleton_congr, subsingleton_iff_eq_bot]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R (Dual R M)
⊢ W.quotDualCoannihilatorToDual.ker = ⊥ ∧ W.quotDualCoannihilatorToDual.flip.ker = ⊥

Tactic:
simp_rw [ker_eq_bot]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
W : Submodule R (Dual R M)
⊢ Function.Injective ⇑W.quotDualCoannihilatorToDual ∧ Function.Injective ⇑W.quotDualCoannihilatorToDual.flip
Module: Mathlib.Algebra.Category.ModuleCat.Kernels

Goal state before:
pp: case zero
R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f✝ f : M ⟶ N
g : N ⟶ P
H : Function.Exact ⇑(Hom.hom f) ⇑(Hom.hom g)
H₂ : Function.Injective ⇑(Hom.hom f)
x : ↑(((Functor.const WalkingParallelPair).obj (kernelCone g).pt).obj WalkingParallelPair.zero)
⊢ (Hom.hom ((kernelCone g).π.app WalkingParallelPair.zero)) x =
    (Hom.hom
        ((LinearEquiv.ofInjective (Hom.hom f) H₂ ≪≫ₗ
                  LinearEquiv.ofEq (Hom.hom f).range (Hom.hom g).ker ⋯).toModuleIso.symm.hom ≫
          (KernelFork.ofι f ⋯).π.app WalkingParallelPair.zero))
      x

Tactic:
simp [kernelCone]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Kernels

Goal state before:
pp: case one
R : Type u
inst✝ : Ring R
M N P : ModuleCat R
f✝ f : M ⟶ N
g : N ⟶ P
H : Function.Exact ⇑(Hom.hom f) ⇑(Hom.hom g)
H₂ : Function.Injective ⇑(Hom.hom f)
x : ↑(((Functor.const WalkingParallelPair).obj (kernelCone g).pt).obj WalkingParallelPair.one)
⊢ (Hom.hom ((kernelCone g).π.app WalkingParallelPair.one)) x =
    (Hom.hom
        ((LinearEquiv.ofInjective (Hom.hom f) H₂ ≪≫ₗ
                  LinearEquiv.ofEq (Hom.hom f).range (Hom.hom g).ker ⋯).toModuleIso.symm.hom ≫
          (KernelFork.ofι f ⋯).π.app WalkingParallelPair.one))
      x

Tactic:
simp [kernelCone]

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : HasZeroMorphisms C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms D
G : C ⥤ D
inst✝³ : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst✝² : HasCokernel f
inst✝¹ : HasCokernel (G.map f)
inst✝ : PreservesColimit (parallelPair f 0) G
⊢ IsIso (cokernelComparison f G)

Tactic:
rw [← PreservesCokernel.iso_inv]
  infer_instance

Goal state after: