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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝ y✝ : (WithInitial C)ᵒᵖ
f✝ : x✝ ⟶ y✝
x y : C
f : op (of x) ⟶ op (of y)
⊢ (𝟭 (WithInitial C)ᵒᵖ).map f ≫
      (match op (of y) with
        | op x =>
          match x with
          | of x => Iso.refl ((𝟭 (WithInitial C)ᵒᵖ).obj (op (of x)))
          | star => Iso.refl ((𝟭 (WithInitial C)ᵒᵖ).obj (op star))).hom =
    (match op (of x) with
        | op x =>
          match x with
          | of x => Iso.refl ((𝟭 (WithInitial C)ᵒᵖ).obj (op (of x)))
          | star => Iso.refl ((𝟭 (WithInitial C)ᵒᵖ).obj (op star))).hom ≫
      ({
              obj := fun x ↦
                match x with
                | op x =>
                  match x with
                  | of x => WithTerminal.of (op x)
                  | star => WithTerminal.star,
              map := fun {x y} x_1 ↦
                match x_1 with
                | op f =>
                  match x, y, f, x_1 with
                  | op (of x), op (of y), f, x_2 => (WithTerminal.down f).op
                  | op (of a), op star, x, x_2 =>
                    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_2 =>
                    𝟙
                      (match op star with
                      | op x =>
                        match x with
                        | of x => WithTerminal.of (op x)
                        | star => WithTerminal.star),
              map_id := ⋯, map_comp := ⋯ } ⋙
            {
              obj := fun x ↦
                match x with
                | WithTerminal.of x => op (of (unop x))
                | WithTerminal.star => op star,
              map := fun {x y} f ↦
                match x, y, f 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),
              map_id := ⋯, map_comp := ⋯ }).map
        f

Tactic:
simp only [Functor.id_obj, Functor.comp_obj,
              Functor.id_map, Iso.refl_hom, Category.comp_id, Functor.comp_map, Category.id_comp]
            rfl

Goal state after:
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
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
T : C ⥤ D
inst✝ : T.Final
S : D ⥤ E
X : E
f : StructuredArrow X S
⊢ IsConnected (StructuredArrow f (pre X T S))

Tactic:
isConnected_iff_of_equivalence (StructuredArrow.preEquivalence T f)

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
T : C ⥤ D
inst✝ : T.Final
S : D ⥤ E
X : E
f : StructuredArrow X S
⊢ IsConnected (StructuredArrow f.right T)
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : Mono f
⊢ IsIso a

Tactic:
←
    show _ = a from
      (Category.comp_id _).symm.trans
        ((IsKernelPair.id_of_mono f).isLimit.conePointUniqueUpToIso_inv_comp h.isLimit
          WalkingCospan.left)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : Mono f
⊢ IsIso ((IsPullback.isLimit ⋯).conePointUniqueUpToIso (IsPullback.isLimit h)).inv
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: case refine_1
P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hQ : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (e : S ≃+* T),
    (fun {R S} [CommRing R] [CommRing S] f ↦ P f ∧ Q f) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P f ∧ Q f) (e.toRingHom.comp f)

pp: case refine_2
P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hQ : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : S →+* T) (e : R ≃+* S),
    (fun {R S} [CommRing R] [CommRing S] f ↦ P f ∧ Q f) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P f ∧ Q f) (f.comp e.toRingHom)

Tactic:
· introv hf
    exact ⟨hP.1 f e hf.1, hQ.1 f e hf.2⟩

Goal state after:
case refine_2
P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hQ : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : S →+* T) (e : R ≃+* S),
    (fun {R S} [CommRing R] [CommRing S] f ↦ P f ∧ Q f) f →
      (fun {R S} [CommRing R] [CommRing S] f ↦ P f ∧ Q f) (f.comp e.toRingHom)
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.IsStableUnderBaseChange
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : Mono g
hcomp : P (f ≫ g)
this : f = (asIso (pullback.fst (f ≫ g) g)).inv ≫ pullback.snd (f ≫ g) g
⊢ P (pullback.snd (f ≫ g) g)

Tactic:
exact P.pullback_snd _ _ hcomp

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
Y₁ Y₂ : C
g : (𝟭 C).obj Y₁ ⟶ (𝟭 C).obj Y₂
X Y : C
X₁ X₂ : J ⥤ C
c₁ : Cone X₁
c₂ : Cone X₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e : { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅ { left := Y₁, right := Y₂, hom := g }
e₁ : Arrow.leftFunc.obj { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Arrow.leftFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.leftFunc.mapIso e
e₂ : Arrow.rightFunc.obj { left := c₁.1, right := c₂.1, hom := h₂.1 { pt := c₁.pt, π := c₁.π ≫ f } } ≅
  Arrow.rightFunc.obj { left := Y₁, right := Y₂, hom := g } :=
  Arrow.rightFunc.mapIso e
fac : g ≫ e₂.inv = e₁.inv ≫ h₂.lift { pt := c₁.pt, π := c₁.π ≫ f }
c₁' : Cone X₁ := { pt := Y₁, π := (Functor.const J).map e₁.inv ≫ c₁.π }
c₂' : Cone X₂ := { pt := Y₂, π := (Functor.const J).map e₂.inv ≫ c₂.π }
h₁' : IsLimit c₁'
h₂' : IsLimit c₂'
j : J
⊢ h₂'.lift { pt := c₁'.pt, π := c₁'.π ≫ f } ≫ c₂'.π.app j = g ≫ c₂'.π.app j

Tactic:
rw [h₂'.fac]
        simp [reassoc_of% fac, c₁', c₂']

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

Goal state before:
pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : P.IsStableUnderRetracts
⊢ P ≤ P.retractClosure

Tactic:
exact le_retractClosure P

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

Goal state before:
pp: case refine_2.hg
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 := ⋯
this : g = gr ≫ pullback.snd (g ≫ f) f
⊢ P (pullback.snd (g ≫ f) f)

Tactic:
exact P.pullback_snd _ _ hcomp

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 (fst (𝟙_ C) X).op)) 1 * α.homEquiv' (snd (𝟙_ C) X) = α.homEquiv' (λ_ X).hom

Tactic:
simp [leftUnitor_hom, -op_tensorObj, -op_whiskerRight, -op_tensorUnit]

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₁ f₂ f₃ : X ⟶ M
⊢ lift f₁ (lift f₂ f₃) ≫ M ◁ μ ≫ μ = lift f₁ (lift f₂ f₃ ≫ μ) ≫ μ

Tactic:
rw [← id_tensorHom, lift_map_assoc, Category.comp_id]

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 : X ⟶ M
⊢ lift f (toUnit X) ≫ M ◁ η ≫ μ = f ≫ 𝟙 M

Tactic:
MonObj.mul_one,

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) ≫ (ρ_ M).hom = f ≫ 𝟙 M
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
⊢ η ≫ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X) = η

Tactic:
dsimp only [yonedaMon_obj] at α ⊢

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
M N : Mon C
α : yonedaMonObj M.X ⟶ yonedaMonObj N.X
⊢ η ≫ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.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
M N : Mon C
α : yonedaMon.obj M ⟶ yonedaMon.obj N
⊢ μ ≫ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X) =
    ((ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X) ⊗ₘ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X)) ≫ μ

Tactic:
dsimp only [yonedaMon_obj] at α ⊢

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
M N : Mon C
α : yonedaMonObj M.X ⟶ yonedaMonObj N.X
⊢ μ ≫ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X) =
    ((ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X) ⊗ₘ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X)) ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: case δ
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : CartesianMonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : CartesianMonoidalCategory E
F : C ⥤ D
G : D ⥤ E
X Y Z : C
inst✝¹ : F.OplaxMonoidal
inst✝ : PreservesFiniteProducts F
a b : F.OplaxMonoidal
x✝¹ x✝ : C
⊢ δ F x✝¹ x✝ = δ F x✝¹ x✝

Tactic:
δ_of_cartesianMonoidalCategory,

Goal state after:
case δ
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : CartesianMonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : CartesianMonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : CartesianMonoidalCategory E
F : C ⥤ D
G : D ⥤ E
X Y Z : C
inst✝¹ : F.OplaxMonoidal
inst✝ : PreservesFiniteProducts F
a b : F.OplaxMonoidal
x✝¹ x✝ : C
⊢ CartesianMonoidalCategory.prodComparison F x✝¹ x✝ = δ F x✝¹ x✝
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
⊢ ∀ (s : PullbackCone μ μ) (m : s.pt ⟶ (A ⊗ A) ⊗ A),
    m ≫ μ ▷ A = s.fst →
      m ≫ (α_ A A A).hom ≫ A ◁ μ = s.snd →
        m = lift (lift (s.snd ≫ fst A A) (lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ)) (s.fst ≫ snd A A)

Tactic:
intro s m hm₁ hm₂

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : CartesianMonoidalCategory C
A : C
inst✝ : GrpObj A
s : PullbackCone μ μ
m : s.pt ⟶ (A ⊗ A) ⊗ A
hm₁ : m ≫ μ ▷ A = s.fst
hm₂ : m ≫ (α_ A A A).hom ≫ A ◁ μ = s.snd
⊢ m = lift (lift (s.snd ≫ fst A A) (lift (s.snd ≫ fst A A ≫ ι) (s.fst ≫ fst A A) ≫ μ)) (s.fst ≫ snd A A)
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X : C
h₁ h₂ : GrpObj X
e : h₁.toMonObj = h₂.toMonObj
this : ι = ι
⊢ h₁ = h₂

Tactic:
by cases h₁; congr!

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
G✝ X✝ : C
inst✝¹ : GrpObj G✝
A B G : C
inst✝ : MonObj G
h : (X : C) → (f : X ⟶ G) → Invertible f
X Y : Cᵒᵖ
f : X ⟶ Y
g : (yoneda.obj G).obj X
⊢ (ConcreteCategory.hom ((yoneda.obj G).map f ≫ ↾fun f ↦ ⅟f)).toFun g =
    (ConcreteCategory.hom ((↾fun f ↦ ⅟f) ≫ (yoneda.obj G).map f)).toFun g

Tactic:
simp only [yoneda_obj_map, TypeCat.Fun.toFun_apply, comp_apply,
        ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk, invOf_eq_iff_left]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : CartesianMonoidalCategory C
G✝ X✝ : C
inst✝¹ : GrpObj G✝
A B G : C
inst✝ : MonObj G
h : (X : C) → (f : X ⟶ G) → Invertible f
X Y : Cᵒᵖ
f : X ⟶ Y
g : (yoneda.obj G).obj X
⊢ f.unop ≫ ⅟g * f.unop ≫ g = 1
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: case convert_3.inl.«0»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ((fun i ↦ i) ⟨0, ⋯⟩)))

Tactic:
dsimp only [id_eq]

Goal state after:
case convert_3.inl.«0»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ⟨0, ⋯⟩))
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: case convert_3.inl.«1»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ((fun i ↦ i) ⟨1, ⋯⟩)))

Tactic:
dsimp only [id_eq]

Goal state after:
case convert_3.inl.«1»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ⟨1, ⋯⟩))
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: case convert_3.inl.«2»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ((fun i ↦ i) ⟨2, ⋯⟩)))

Tactic:
dsimp only [id_eq]

Goal state after:
case convert_3.inl.«2»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ⟨2, ⋯⟩))
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: case convert_3.inl.«3»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ((fun i ↦ i) ⟨3, ⋯⟩)))

Tactic:
dsimp only [id_eq]

Goal state after:
case convert_3.inl.«3»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ⟨3, ⋯⟩))
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: case convert_3.inl.«4»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ((fun i ↦ i) ⟨4, ⋯⟩)))

Tactic:
dsimp only [id_eq]

Goal state after:
case convert_3.inl.«4»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ⟨4, ⋯⟩))
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: case convert_3.inl.«5»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ((fun i ↦ i) ⟨5, ⋯⟩)))

Tactic:
dsimp only [id_eq]

Goal state after:
case convert_3.inl.«5»
α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ Finite (Operands s (Sum.inl ⟨5, ⋯⟩))
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
b : Basis ι R M
inst✝ : Fintype ι
f : Dual R M
m : M
⊢ f (∑ x, (b.coord x) m • b x) = f m

Tactic:
Basis.coord_apply,

Goal state after:
R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
inst✝ : Fintype ι
f : Dual R M
m : M
⊢ f (∑ x, (b.repr m) x • b x) = f m
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
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 ↥f.ker = finrank K V
⊢ Injective ⇑f ↔ Surjective ⇑f

Tactic:
rw [← ker_eq_bot, ← range_eq_top]

Goal state after:
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 ↥f.ker = finrank K V
⊢ f.ker = ⊥ ↔ f.range = ⊤
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: case ha
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
⊢ lift.{v, v'} (Module.rank K ↥p) < ℵ₀

Tactic:
rwa [lift_lt_aleph0, rank_lt_aleph0_iff]

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

Goal state before:
pp: case hb
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
⊢ lift.{v', v} (Module.rank K ↥f.ker) < ℵ₀

Tactic:
rwa [lift_lt_aleph0, rank_lt_aleph0_iff]

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

Goal state before:
pp: case ha
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)
⊢ lift.{v, v'} (Module.rank K (W ⧸ f.range)) < ℵ₀

Tactic:
rwa [lift_lt_aleph0, rank_lt_aleph0_iff]

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

Goal state before:
pp: case hb
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)
⊢ lift.{v', v} (Module.rank K (V ⧸ p)) < ℵ₀

Tactic:
rwa [lift_lt_aleph0, rank_lt_aleph0_iff]

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

Goal state before:
pp: R : Type u_20
M : Type u_21
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : LinearMap.BilinForm R M
F : Type u_22
inst✝¹ : FunLike F M M
inst✝ : LinearMapClass F R M M
f : F
h : IsLeftRegular 2
hB : IsSymm B
hf : ∀ (x : M), (B (f x)) (f x) = (B x) x
x y : M
this : (B x) x + (B (f y)) (f x) + ((B (f x)) (f y) + (B y) y) = (B x) x + (B x) y + ((B x) y + (B y) y)
⊢ 2 * (B (f x)) (f y) = 2 * (B x) y

Tactic:
rw [show B (f y) (f x) = B (f x) (f y) from hB.eq (f y) (f x)] at this

Goal state after:
R : Type u_20
M : Type u_21
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
B : LinearMap.BilinForm R M
F : Type u_22
inst✝¹ : FunLike F M M
inst✝ : LinearMapClass F R M M
f : F
h : IsLeftRegular 2
hB : IsSymm B
hf : ∀ (x : M), (B (f x)) (f x) = (B x) x
x y : M
this : (B x) x + (B (f x)) (f y) + ((B (f x)) (f y) + (B y) y) = (B x) x + (B x) y + ((B x) y + (B y) y)
⊢ 2 * (B (f x)) (f y) = 2 * (B x) y
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
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))

Tactic:
have : Dual.eval R (M × N) = e.symm.comp ((Dual.eval R M).prodMap (Dual.eval R N)) := by
      ext m f <;> simp [e]

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
this : Dual.eval R (M × N) = ↑e.symm ∘ₗ (Dual.eval R M).prodMap (Dual.eval R N)
⊢ Bijective ⇑(Dual.eval R (M × N))
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers

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
inst✝² : HasCoequalizer f g
inst✝¹ : HasCoequalizer (G.map f) (G.map g)
inst✝ : PreservesColimit (parallelPair f g) G
⊢ G.map (coequalizer.π f g) ≫ (PreservesCoequalizer.iso G f g).inv = coequalizer.π (G.map f) (G.map g)

Tactic:
by
  rw [← ι_comp_coequalizerComparison_assoc, ← PreservesCoequalizer.iso_hom, Iso.hom_inv_id,
    comp_id]

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

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

Tactic:
exact eq_zero_of_pow_eq_zero <| le_antisymm this (sq_nonneg (B x y))

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
⊢ W ≤ W.dualAnnihilator.subtype.flip.ker

Tactic:
intro w

Goal state after:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
w : M
⊢ w ∈ W → w ∈ W.dualAnnihilator.subtype.flip.ker
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
hB : IsSymm B
x y : M
⊢ (B x) y * (B y) x < (B x) x * (B y) y ↔ LinearIndependent R ![x, y]

Tactic:
exact apply_mul_apply_lt_iff_linearIndependent B hp x y

Goal state after: