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

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderCobaseChange
⊢ P.pushouts ≤ Q → P ≤ Q

pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderCobaseChange
⊢ P ≤ Q → P.pushouts ≤ Q

Tactic:
· exact le_trans P.le_pushouts

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderCobaseChange
⊢ P ≤ Q → P.pushouts ≤ Q
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₂
this✝ : HasPushoutsAlong (Under.mk g').hom
this :
  pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ =
    ((pushoutSymmetry f (Under.mk g).hom).hom ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      (pushoutSymmetry (Under.mk g').hom f).hom ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯))
⊢ P (pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯)

Tactic:
rw [this]

Goal state after:
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₂
this✝ : HasPushoutsAlong (Under.mk g').hom
this :
  pushout.map f g f' g' i₁ i₂ (𝟙 S) ⋯ ⋯ =
    ((pushoutSymmetry f (Under.mk g).hom).hom ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      (pushoutSymmetry (Under.mk g').hom f).hom ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯))
⊢ P
    (((pushoutSymmetry f (Under.mk g).hom).hom ≫ Under.Hom.right ((Under.pushout f).map (Under.homMk i₂ ⋯))) ≫
      (pushoutSymmetry (Under.mk g').hom f).hom ≫ Under.Hom.right ((Under.pushout g').map (Under.homMk i₁ ⋯)))
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
⊢ W.IsStableUnderLimitsOfShape J ↔ W.limitsOfShape J ≤ W

Tactic:
by
  constructor
  · rintro h _ _ _ ⟨_, _, _, _, h₁, h₂, f, hf⟩
    exact h.condition _ _ _ _ h₁ h₂ f hf _ (by simp)
  · rintro h
    constructor
    intro X₁ X₂ c₁ c₂ h₁ h₂ f hf φ hφ
    exact h _ (limitsOfShape.mk' X₁ X₂ c₁ c₂ h₁ h₂ f hf φ hφ)

Goal state after:
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
J' : Type u_2
inst✝¹ : Category.{v_2, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
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₁' : IsColimit (Cocone.whisker F c₁)
h₂' : IsColimit (Cocone.whisker F c₂)
this : h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } = h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ (Cocone.whisker F c₂).ι }
⊢ W.colimitsOfShape J (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })

Tactic:
rw [this]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝² : Category.{v_1, u_1} J
J' : Type u_2
inst✝¹ : Category.{v_2, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
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₁' : IsColimit (Cocone.whisker F c₁)
h₂' : IsColimit (Cocone.whisker F c₂)
this : h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } = h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ (Cocone.whisker F c₂).ι }
⊢ W.colimitsOfShape J (h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ (Cocone.whisker F c₂).ι })
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
Q : MorphismProperty C
inst✝ : Q.IsStableUnderBaseChange
hP : Q ≤ P.diagonal
Y X S : C
g : Y ⟶ X
f : X ⟶ S
hf : Q f
hcomp : P (g ≫ f)
gr : Y ⟶ pullback (g ≫ f) f := pullback.lift (𝟙 Y) g ⋯
this : g = gr ≫ pullback.snd (g ≫ f) f
⊢ P g

Tactic:
rw [this]

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : P.IsMultiplicative
Q : MorphismProperty C
inst✝ : Q.IsStableUnderBaseChange
hP : Q ≤ P.diagonal
Y X S : C
g : Y ⟶ X
f : X ⟶ S
hf : Q f
hcomp : P (g ≫ f)
gr : Y ⟶ pullback (g ≫ f) f := pullback.lift (𝟙 Y) g ⋯
this : g = gr ≫ pullback.snd (g ≫ f) f
⊢ P (gr ≫ pullback.snd (g ≫ f) f)
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
P : ObjectProperty C
J : Type u'
inst✝² : Category.{v', u'} J
J' : Type u''
inst✝¹ : Category.{v'', u''} J'
inst✝ : P.IsClosedUnderColimitsOfShape WalkingParallelPair
X Y : C
h : Retract X Y
hY : P Y
c : Cofork (h.r ≫ h.i) (𝟙 Y) := Cofork.ofπ h.r ⋯
s : Cofork (h.r ≫ h.i) (𝟙 Y)
m : c.pt ⟶ s.pt
hm : c.π ≫ m = s.π
⊢ m = h.i ≫ s.π

Tactic:
by dsimp [c] at hm; simp [← hm]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
F : Cᵒᵖ ⥤ MonCat
α : (F ⋙ forget MonCat).RepresentableBy X
⊢ (ConcreteCategory.hom (F.map (α.homEquiv'.symm 1 ▷ X).op)) (α.homEquiv' (fst X X)) *
      (ConcreteCategory.hom (F.map (α.homEquiv'.symm 1 ▷ X).op)) (α.homEquiv' (snd X X)) =
    α.homEquiv' (λ_ X).hom

Tactic:
simp only [← α.homEquiv'_comp]

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
⊢ α.homEquiv' (α.homEquiv'.symm 1 ▷ X ≫ fst X X) * α.homEquiv' (α.homEquiv'.symm 1 ▷ X ≫ snd X X) =
    α.homEquiv' (λ_ X).hom
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
⊢ (ConcreteCategory.hom (F.map (X ◁ α.homEquiv'.symm 1).op)) (α.homEquiv' (fst X X)) *
      (ConcreteCategory.hom (F.map (X ◁ α.homEquiv'.symm 1).op)) (α.homEquiv' (snd X X)) =
    α.homEquiv' (ρ_ X).hom

Tactic:
simp only [← α.homEquiv'_comp]

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
⊢ α.homEquiv' (X ◁ α.homEquiv'.symm 1 ≫ fst X X) * α.homEquiv' (X ◁ α.homEquiv'.symm 1 ≫ snd X X) =
    α.homEquiv' (ρ_ X).hom
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
⊢ (ConcreteCategory.hom (F.map (α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) ▷ X).op))
        (α.homEquiv' (fst X X)) *
      (ConcreteCategory.hom (F.map (α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) ▷ X).op))
        (α.homEquiv' (snd X X)) =
    (ConcreteCategory.hom (F.map (α_ X X X).hom.op))
        ((ConcreteCategory.hom (F.map (X ◁ α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X))).op))
          (α.homEquiv' (fst X X))) *
      (ConcreteCategory.hom (F.map (α_ X X X).hom.op))
        ((ConcreteCategory.hom (F.map (X ◁ α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X))).op))
          (α.homEquiv' (snd X X)))

Tactic:
simp only [← α.homEquiv'_comp]

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
⊢ α.homEquiv' (α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) ▷ X ≫ fst X X) *
      α.homEquiv' (α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) ▷ X ≫ snd X X) =
    α.homEquiv' ((α_ X X X).hom ≫ X ◁ α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) ≫ fst X X) *
      α.homEquiv' ((α_ X X X).hom ≫ X ◁ α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) ≫ snd X X)
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
⊢ (ConcreteCategory.hom (F.map (fst (X ⊗ X) X).op)) (α.homEquiv' (fst X X)) *
      ((ConcreteCategory.hom (F.map (fst (X ⊗ X) X).op)) (α.homEquiv' (snd X X)) * α.homEquiv' (snd (X ⊗ X) X)) =
    (ConcreteCategory.hom (F.map (fst (X ⊗ X) X).op)) (α.homEquiv' (fst X X)) *
      ((ConcreteCategory.hom (F.map (α_ X X X).hom.op))
          ((ConcreteCategory.hom (F.map (snd X (X ⊗ X)).op)) (α.homEquiv' (fst X X))) *
        (ConcreteCategory.hom (F.map (α_ X X X).hom.op))
          ((ConcreteCategory.hom (F.map (snd X (X ⊗ X)).op)) (α.homEquiv' (snd X X))))

Tactic:
simp only [← α.homEquiv'_comp]

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
⊢ α.homEquiv' (fst (X ⊗ X) X ≫ fst X X) * (α.homEquiv' (fst (X ⊗ X) X ≫ snd X X) * α.homEquiv' (snd (X ⊗ X) X)) =
    α.homEquiv' (fst (X ⊗ X) X ≫ fst X X) *
      (α.homEquiv' ((α_ X X X).hom ≫ snd X (X ⊗ X) ≫ fst X X) * α.homEquiv' ((α_ X X X).hom ≫ snd X (X ⊗ X) ≫ snd X X))
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:
by
    change lift f (toUnit _ ≫ η) ≫ μ = f
    rw [← Category.comp_id f, ← lift_map_assoc, id_tensorHom, MonObj.mul_one,
      Category.comp_id, rightUnitor_hom]
    exact lift_fst _ _

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y✝ : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
F : Cᵒᵖ ⥤ MonCat
α : (F ⋙ forget MonCat).RepresentableBy X
this : MonObj X := ofRepresentableBy X F α
Y : Cᵒᵖ
f₁ f₂ : unop Y ⟶ X
⊢ (ConcreteCategory.hom (F.map (lift f₁ f₂).op)) (α.homEquiv' (fst X X)) *
      (ConcreteCategory.hom (F.map (lift f₁ f₂).op)) (α.homEquiv' (snd X X)) =
    α.homEquiv' f₁ * α.homEquiv' f₂

Tactic:
simp only [← α.homEquiv'_comp]

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₂ ≫ fst X X) * α.homEquiv' (lift f₁ f₂ ≫ snd X X) = α.homEquiv' f₁ * α.homEquiv' 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✝ N✝ O X Y : C
inst✝² : MonObj M✝
inst✝¹ : MonObj N✝
inst✝ : MonObj O
M N : Mon C
α : yonedaMon.obj M ⟶ yonedaMon.obj N
⊢ yonedaMon.map { hom := (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X), isMonHom_hom := ⋯ } = α

Tactic:
by
    ext Y f
    simp [← dsimp% yonedaMon_naturality]

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

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.Monoidal
inst✝¹ : F.Full
inst✝ : F.Faithful
G : Grp D
⊢ F.mapGrp.essImage G → F.essImage G.X

Tactic:
by rintro ⟨H, ⟨e⟩⟩; exact ⟨H.X, ⟨(Grp.forget _).mapIso e⟩⟩

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y Z : C
inst✝ : Closed X
f : X ⟶ Y
g : Y ⟶ Z
⊢ curry' f ≫ (ihom X).map g = curry' (f ≫ g)

Tactic:
by
  simp only [curry', ← curry_natural_right, Category.assoc]

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

Goal state before:
pp: 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)
⊢ Module.rank K (ℕ → K) * ℵ₀ < #K

Tactic:
mul_aleph0_eq aleph0_le

Goal state after:
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)
⊢ Module.rank K (ℕ → K) < #K
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_1
b : Basis ι R M
m m' : M
eq : (Dual.eval R M) m = (Dual.eval R M) m'
⊢ m = m'

Tactic:
simp_rw [LinearMap.ext_iff, Dual.eval_apply] at eq

Goal state after:
R : Type uR
M : Type uM
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_1
b : Basis ι R M
m m' : M
eq : ∀ (x : Dual R M), x m = x m'
⊢ m = m'
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: case h₀
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
i : ι
⊢ ∀ (b : ι), l b ≠ 0 → b ≠ i → (ε i) (l b • e b) = 0

Tactic:
intro q

Goal state after:
case h₀
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
i q : ι
⊢ l q ≠ 0 → q ≠ i → (ε i) (l q • e q) = 0
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 ε
H : Set ι
x : M
hmem : x ∈ span R (e '' H)
⊢ ∀ (i : ι), (ε i) x ≠ 0 → i ∈ H

Tactic:
intro i hi
  rcases (Finsupp.mem_span_image_iff_linearCombination _).mp hmem with ⟨l, supp_l, rfl⟩
  apply not_imp_comm.mp ((Finsupp.mem_supported' _ _).mp supp_l i)
  rwa [← lc_def, h.dual_lc] at hi

Goal state after:
Module: Mathlib.Algebra.Category.CommHopfAlgCat

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A B C : CommHopfAlgCat R
X✝ Y✝ Z : Type v
inst✝⁵ : CommRing X✝
inst✝⁴ : HopfAlgebra R X✝
inst✝³ : CommRing Y✝
inst✝² : HopfAlgebra R Y✝
inst✝¹ : CommRing Z
inst✝ : HopfAlgebra R Z
X Y : CommHopfAlgCat R
f : X ⟶ Y
x✝ : IsIso ((forget (CommHopfAlgCat R)).map f)
⊢ IsIso f

Tactic:
let i := asIso ((forget (CommHopfAlgCat.{u} R)).map f)

Goal state after:
R : Type u
inst✝⁶ : CommRing R
A B C : CommHopfAlgCat R
X✝ Y✝ Z : Type v
inst✝⁵ : CommRing X✝
inst✝⁴ : HopfAlgebra R X✝
inst✝³ : CommRing Y✝
inst✝² : HopfAlgebra R Y✝
inst✝¹ : CommRing Z
inst✝ : HopfAlgebra R Z
X Y : CommHopfAlgCat R
f : X ⟶ Y
x✝ : IsIso ((forget (CommHopfAlgCat R)).map f)
i : (forget (CommHopfAlgCat R)).obj X ≅ (forget (CommHopfAlgCat R)).obj Y := asIso ((forget (CommHopfAlgCat R)).map f)
⊢ IsIso f
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ Module.rank R (M ⧸ span R s) + #↑s = Module.rank R (M ⧸ span R s) + Module.rank R ↥(span R s)

pp: case refine_1
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ Injective sec

Tactic:
rank_span_set hs

Goal state after:
case refine_1
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ Module.rank R (M ⧸ span R s) + #↑s = Module.rank R (M ⧸ span R s) + #↑s

case refine_1
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
sec : M ⧸ span R s → M
hsec : ∀ (b : M ⧸ span R s), (span R s).mkQ (sec b) = b
hsec' : ⇑(span R s).mkQ ∘ sec = _root_.id
hst : Disjoint s (sec '' t)
⊢ Injective sec
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
inst✝ : Module.Finite K V
W : Submodule K V
v : V
hv : v ∉ W
hW : finrank K (V ⧸ W) = 1
⊢ W ⊔ K ∙ v = ⊤

Tactic:
apply Submodule.eq_top_of_disjoint
    · rw [← W.finrank_quotient_add_finrank, add_comm, add_le_add_iff_left, hW]
      aesop
    · exact Submodule.disjoint_span_singleton_of_notMem hv

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

Goal state before:
pp: case refine_1
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 ↥f.range = finrank K V₂
h : f.ker = ⊥
⊢ f.range = ⊤

Tactic:
exact eq_top_of_finrank_eq this

Goal state after:
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 + finrank K ↥W = finrank K V

Tactic:
by
  rw [← finrank_sup_add_finrank_inf_eq, h.codisjoint.eq_top, h.disjoint.eq_bot, finrank_bot,
    add_zero]
  exact finrank_top _ _

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

Goal state before:
pp: case «1»
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))
S : Subalgebra F E
this✝² : FiniteDimensional F E
this✝¹ : FiniteDimensional F ↥S
h : finrank F ↥S = 1
this✝ : 1 ≤ 2
this : 0 < 1
⊢ S = ⊥ ∨ S = ⊤

Tactic:
left
        exact Subalgebra.eq_bot_of_finrank_one h

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : CommSemiring R₁
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
⊢ B.flip.ker = B.ker

Tactic:
ext x
  simp [LinearMap.ext_iff, H.eq_iff]

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

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
W : Submodule R M
hW : (B.domRestrict₁₂ W W).Nondegenerate
x : M
hx : x ∈ W
hx' : x ∈ B.ker
x' : ↥W := ⟨x, hx⟩
⊢ x = 0

Tactic:
suffices x' = 0 by simpa [x']

Goal state after:
R : Type u_1
M : Type u_5
M₁ : Type u_6
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M₁
inst✝ : Module R M₁
B : M →ₗ[R] M →ₗ[R] M₁
W : Submodule R M
hW : (B.domRestrict₁₂ W W).Nondegenerate
x : M
hx : x ∈ W
hx' : x ∈ B.ker
x' : ↥W := ⟨x, hx⟩
⊢ x' = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : C ⥤ D
⊢ F.map (g ≫ π) = F.map g ≫ F.map π

Tactic:
F.map_comp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : C ⥤ D
⊢ F.map g ≫ F.map π = F.map g ≫ F.map π
Module: Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : C ⥤ D
⊢ F.map (π ≫ q.rightSection) = F.map π ≫ F.map q.rightSection

Tactic:
F.map_comp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : C ⥤ D
⊢ F.map π ≫ F.map q.rightSection = F.map π ≫ F.map q.rightSection
Module: Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
W : C
ι : W ⟶ X
q : IsSplitEqualizer f g ι
F : C ⥤ D
⊢ F.map (ι ≫ g) = F.map ι ≫ F.map g

Tactic:
F.map_comp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
W : C
ι : W ⟶ X
q : IsSplitEqualizer f g ι
F : C ⥤ D
⊢ F.map ι ≫ F.map g = F.map ι ≫ F.map g