mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst✝⁴ : AddCommGroup M
inst✝³ : SubtractionCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ mk' f m₁ s₁ - mk' f m₂ s₂ = mk' f (s₂ • m₁ - s₁ • m₂) (s₁ * s₂)

Tactic:
by
  rw [sub_eq_add_neg, ← mk'_neg, mk'_add_mk', smul_neg, ← sub_eq_add_neg]

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
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))
m₁ : M
t₁ : ↥S
hxy :
  (fun x ↦
        (fun x ↦
              match x with
              | (r, m) => IsLocalization.mk' A r m)
            (a, s) •
          x)
      (Function.uncurry (mk' f) (m₁, t₁)) =
    (fun x ↦
        (fun x ↦
              match x with
              | (r, m) => IsLocalization.mk' A r m)
            (a, s) •
          x)
      y
⊢ Function.uncurry (mk' f) (m₁, t₁) = y

Tactic:
obtain ⟨⟨m₂, t₂⟩, rfl⟩ := IsLocalizedModule.mk'_surjective S f y

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
hS₀ : 0 ∉ S
a : R
s : ↥S
hc :
  IsRegular
    ((fun x ↦
        match x with
        | (r, m) => IsLocalization.mk' A r m)
      (a, s))
m₁ : M
t₁ : ↥S
m₂ : M
t₂ : ↥S
hxy :
  (fun x ↦
        (fun x ↦
              match x with
              | (r, m) => IsLocalization.mk' A r m)
            (a, s) •
          x)
      (Function.uncurry (mk' f) (m₁, t₁)) =
    (fun x ↦
        (fun x ↦
              match x with
              | (r, m) => IsLocalization.mk' A r m)
            (a, s) •
          x)
      (Function.uncurry (mk' f) (m₂, t₂))
⊢ Function.uncurry (mk' f) (m₁, t₁) = Function.uncurry (mk' f) (m₂, t₂)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᴸ C
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ F.mapComp f g ▷ F.map h ≫ F.mapComp (f ≫ g) h =
    (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ F.mapComp g h ≫ F.mapComp f (g ≫ h) ≫ F.map₂ (α_ f g h).inv

Tactic:
← F.map₂_associator_assoc,

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᴸ C
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ F.mapComp f g ▷ F.map h ≫ F.mapComp (f ≫ g) h =
    F.mapComp f g ▷ F.map h ≫ F.mapComp (f ≫ g) h ≫ F.map₂ (α_ f g h).hom ≫ F.map₂ (α_ f g h).inv
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᵖ C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ F.map₂ (λ_ f).inv = (λ_ (F.map f)).inv ≫ (F.mapId a✝).inv ▷ F.map f ≫ (F.mapComp (𝟙 a✝) f).inv

Tactic:
rw [← F.map₂Iso_inv, eq_inv_comp, comp_inv_eq]
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᵖ C
a✝ b✝ : B
f : a✝ ⟶ b✝
⊢ F.map₂ (ρ_ f).inv = (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b✝).inv ≫ (F.mapComp f (𝟙 b✝)).inv

Tactic:
rw [← F.map₂Iso_inv, eq_inv_comp, comp_inv_eq]
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
F' : F.PseudoCore
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ F.map₂ (α_ f g h).hom =
    F.mapComp (f ≫ g) h ≫
      F.mapComp f g ▷ F.map h ≫
        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv

Tactic:
← F.map₂_associator_assoc,

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
F' : F.PseudoCore
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
⊢ F.map₂ (α_ f g h).hom =
    F.map₂ (α_ f g h).hom ≫
      F.mapComp f (g ≫ h) ≫ F.map f ◁ F.mapComp g h ≫ F.map f ◁ (F'.mapCompIso g h).inv ≫ (F'.mapCompIso f (g ≫ h)).inv
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a b : B
f : a ⟶ b
⊢ F.map₂ (λ_ f).hom = (F'.mapCompIso (𝟙 a) f).hom ≫ (F'.mapIdIso a).hom ▷ F.map f ≫ (λ_ (F.map f)).hom

Tactic:
← IsIso.inv_eq_inv,

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a b : B
f : a ⟶ b
⊢ inv (F.map₂ (λ_ f).hom) = inv ((F'.mapCompIso (𝟙 a) f).hom ≫ (F'.mapIdIso a).hom ▷ F.map f ≫ (λ_ (F.map f)).hom)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a b : B
f : a ⟶ b
⊢ F.map₂ (ρ_ f).hom = (F'.mapCompIso f (𝟙 b)).hom ≫ F.map f ◁ (F'.mapIdIso b).hom ≫ (ρ_ (F.map f)).hom

Tactic:
← IsIso.inv_eq_inv,

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᴸ C
F' : F.PseudoCore
a b : B
f : a ⟶ b
⊢ inv (F.map₂ (ρ_ f).hom) = inv ((F'.mapCompIso f (𝟙 b)).hom ≫ F.map f ◁ (F'.mapIdIso b).hom ≫ (ρ_ (F.map f)).hom)
Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
h : P ≤ Q
hPQ : Q ≤ P.isoClosure
x✝ : Q.FullSubcategory
Y : C
hY : Q Y
⊢ (ιOfLE h).essImage { obj := Y, property := hY }

Tactic:
obtain ⟨X, hX, ⟨e⟩⟩ := hPQ _ hY

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
h : P ≤ Q
hPQ : Q ≤ P.isoClosure
x✝ : Q.FullSubcategory
Y : C
hY : Q Y
X : C
hX : P X
e : Y ≅ X
⊢ (ιOfLE h).essImage { obj := Y, property := hY }
Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
Q : ObjectProperty D
e : C ≌ D
inst✝ : Q.IsClosedUnderIsomorphisms
h : Q.inverseImage e.functor = P
x✝ : Q.FullSubcategory
Y : D
hY : Q Y
⊢ P ((Q.ι ⋙ e.inverse).obj { obj := Y, property := hY })

Tactic:
rw [← h]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
Q : ObjectProperty D
e : C ≌ D
inst✝ : Q.IsClosedUnderIsomorphisms
h : Q.inverseImage e.functor = P
x✝ : Q.FullSubcategory
Y : D
hY : Q Y
⊢ Q.inverseImage e.functor ((Q.ι ⋙ e.inverse).obj { obj := Y, property := hY })
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝¹ : Q.IsMultiplicative
F : C ⥤ D
X : D
inst✝ : F.Faithful
A B : P.CostructuredArrow ⊤ F X
f g : A ⟶ B
⊢ (CostructuredArrow.toOver P F X).map f = (CostructuredArrow.toOver P F X).map g → f = g

Tactic:
hfg

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝¹ : Q.IsMultiplicative
F : C ⥤ D
X : D
inst✝ : F.Faithful
A B : P.CostructuredArrow ⊤ F X
f g : A ⟶ B
hfg : (CostructuredArrow.toOver P F X).map f = (CostructuredArrow.toOver P F X).map g
⊢ f = g
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝³ : HasPullback f₁ f₂
inst✝² : HasPullback f₃ f₄
inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄
inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ (pullbackAssoc f₁ f₂ f₃ f₄).hom ≫ pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂) =
    pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂

Tactic:
rw [← Iso.eq_inv_comp, pullbackAssoc_inv_fst_fst]

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

Goal state before:
pp: case refine_1.refine_1
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ f ≫ i = f ≫ inv (fst i (𝟙 S)) ≫ fst i (𝟙 S) ≫ i

Tactic:
IsIso.inv_hom_id_assoc

Goal state after:
case refine_1.refine_1
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ f ≫ i = f ≫ i
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case refine_1.refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ g ≫ i = g ≫ inv (fst i (𝟙 S)) ≫ fst i (𝟙 S) ≫ i

Tactic:
IsIso.inv_hom_id_assoc

Goal state after:
case refine_1.refine_2
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
X Y Z : C
inst✝⁴ : HasPullbacks C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst✝³ : HasPullback i i
inst✝² : HasPullback f g
inst✝¹ : HasPullback (f ≫ i) (g ≫ i)
inst✝ : HasPullback (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ g ≫ i = g ≫ i
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

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

Tactic:
by
  constructor
  · exact le_trans P.le_pushouts
  · intro h
    exact le_trans (pushouts_monotone h) pushouts_le

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

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

Tactic:
exact ⟨_, _, _, _, _, h₂, f, fun j ↦ h _ (hf j)⟩

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
⊢ W.colimitsOfShape (Discrete (Shrink.{w, w'} J)) f

Tactic:
← W.colimitsOfShape_eq_of_equivalence (Discrete.equivalence (equivShrink.{w} J))

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
⊢ W.colimitsOfShape (Discrete J) f
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y Z : C
f : X ⟶ Y ⊗ Z
⊢ lift (f ≫ fst Y Z) (f ≫ snd Y Z) = f

Tactic:
by
  cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
⊢ lift f g ≫ h ▷ Z = lift (f ≫ h) g

Tactic:
by
  cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Z ⟶ W
⊢ lift f g ≫ Y ◁ h = lift f (g ≫ h)

Tactic:
by
  cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
⊢ lift (lift f g) h ≫ (α_ Y Z W).hom = lift f (lift g h)

Tactic:
by
  cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
⊢ lift f (lift g h) ≫ (α_ Y Z W).inv = lift (lift f g) h

Tactic:
by
  cat_disch

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : CartesianMonoidalCategory C
M X : C
inst✝ : MonObj M
⊢ monoidHom (𝟙 M) X = MonoidHom.id (X ⟶ M)

Tactic:
by
  cat_disch

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
M N O X : C
inst✝⁴ : MonObj M
inst✝³ : MonObj N
inst✝² : MonObj O
f : M ⟶ N
g : N ⟶ O
inst✝¹ : IsMonHom f
inst✝ : IsMonHom g
⊢ monoidHom (f ≫ g) X = (monoidHom g X).comp (monoidHom f X)

Tactic:
by
  cat_disch

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

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : CartesianMonoidalCategory C
F : Cᵒᵖ ⥤ MonCat
M : Mon C
α : yonedaMon.obj M ≅ F
⊢ (F ⋙ forget MonCat).IsRepresentable

Tactic:
exact ⟨M.X, ⟨Functor.representableByEquiv.symm (Functor.isoWhiskerRight α (forget _))⟩⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CartesianMonoidalCategory C
⊢ preservesTerminalIso (𝟭 C) = Iso.refl ((𝟭 C).obj (𝟙_ C))

Tactic:
by
  cat_disch

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
E : Type u₂
inst✝⁴ : Category.{v₂, u₂} E
inst✝³ : CartesianMonoidalCategory E
G : D ⥤ E
inst✝² : PreservesLimit (Functor.empty C) F
inst✝¹ : PreservesLimit (Functor.empty D) G
inst✝ : PreservesLimit (Functor.empty C) (F ⋙ G)
⊢ preservesTerminalIso (F ⋙ G) = G.mapIso (preservesTerminalIso F) ≪≫ preservesTerminalIso G

Tactic:
by
  cat_disch

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
antipode : A →ₗ[R] A
antipode_convMul_id : toConv antipode * toConv LinearMap.id = 1
id_convMul_antipode : toConv LinearMap.id * toConv antipode = 1
⊢ mul' R A ∘ₗ rTensor A antipode ∘ₗ comul = Algebra.linearMap R A ∘ₗ counit

Tactic:
by simpa using! congr(($antipode_convMul_id).ofConv)

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M N P : ModuleCat R
f : (MonoidalCategory.tensorLeft M).obj N ⟶ P
⊢ Hom.hom
      ((fun f ↦ (β_ M N).hom ≫ ↟(TensorProduct.lift (Hom.hom₂ f)))
        ((fun f ↦ ofHom₂ ((TensorProduct.mk R ↑N ↑M).compr₂ (Hom.hom ((β_ N M).hom ≫ f)))) f)) =
    Hom.hom f

Tactic:
apply TensorProduct.ext'

Goal state after:
R : Type u
inst✝ : CommRing R
M N P : ModuleCat R
f : (MonoidalCategory.tensorLeft M).obj N ⟶ P
⊢ ∀ (x : ↑M) (y : ↑N),
    (Hom.hom
          ((fun f ↦ (β_ M N).hom ≫ ↟(TensorProduct.lift (Hom.hom₂ f)))
            ((fun f ↦ ofHom₂ ((TensorProduct.mk R ↑N ↑M).compr₂ (Hom.hom ((β_ N M).hom ≫ f)))) f)))
        (x ⊗ₜ[R] y) =
      (Hom.hom f) (x ⊗ₜ[R] y)
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M X'✝ X✝ Y✝ : ModuleCat R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y✝
⊢ Hom.hom ((M.monoidalClosedHomEquiv X'✝ Y✝).symm (f✝ ≫ g✝)) =
    Hom.hom ((MonoidalCategory.tensorLeft M).map f✝ ≫ (M.monoidalClosedHomEquiv X✝ Y✝).symm g✝)

Tactic:
apply TensorProduct.ext'

Goal state after:
R : Type u
inst✝ : CommRing R
M X'✝ X✝ Y✝ : ModuleCat R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y✝
⊢ ∀ (x : ↑M) (y : ↑X'✝),
    (Hom.hom ((M.monoidalClosedHomEquiv X'✝ Y✝).symm (f✝ ≫ g✝))) (x ⊗ₜ[R] y) =
      (Hom.hom ((MonoidalCategory.tensorLeft M).map f✝ ≫ (M.monoidalClosedHomEquiv X✝ Y✝).symm g✝)) (x ⊗ₜ[R] y)
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed

Goal state before:
pp: R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ Hom.hom (MonoidalClosed.uncurry (𝟙 ((ihom M).obj N))) =
    Hom.hom
      (↟((TensorProduct.uncurry (RingHom.id R) ↑M ↑((ihom M).obj N) ↑N)
          (LinearMap.lcomp R ↑N ↑homLinearEquiv ∘ₗ LinearMap.id.flip)))

Tactic:
apply TensorProduct.ext'

Goal state after:
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ ∀ (x : ↑M) (y : ↑((ihom M).obj N)),
    (Hom.hom (MonoidalClosed.uncurry (𝟙 ((ihom M).obj N)))) (x ⊗ₜ[R] y) =
      (Hom.hom
          (↟((TensorProduct.uncurry (RingHom.id R) ↑M ↑((ihom M).obj N) ↑N)
              (LinearMap.lcomp R ↑N ↑homLinearEquiv ∘ₗ LinearMap.id.flip))))
        (x ⊗ₜ[R] y)
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: case e'_4.inl
α : Type u
s : Set α
inst✝ : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : #↑s < ℵ₀
⊢ ℵ₀ = max (lift.{u, 0} #(Fin 6) + #↑s) ℵ₀

Tactic:
max_eq_right

Goal state after:
case e'_4.inl
α : Type u
s : Set α
inst✝ : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : #↑s < ℵ₀
⊢ ℵ₀ = ℵ₀

case e'_4.inl
α : Type u
s : Set α
inst✝ : DivisionRing α
this : lift.{u, 0} #(Fin 6) < ℵ₀
h : #↑s < ℵ₀
⊢ lift.{u, 0} #(Fin 6) + #↑s ≤ ℵ₀
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
f' : M' ⧸ Submodule.map f p →ₗ[R] M' ⧸ f.range := factor ⋯
g : ↥f.range →ₗ[R] ↥f'.ker :=
  ↑(LinearEquiv.ofEq (Submodule.map (Submodule.map f p).mkQ f.range) f'.ker ⋯) ∘ₗ
    (Submodule.map f p).mkQ.submoduleMap f.range
g_surj : Surjective ⇑g
g_ker : g.ker = Submodule.map f.rangeRestrict p
⊢ (↥f.range ⧸ Submodule.map f.rangeRestrict p) ≃ₗ[R] ↥f'.ker

Tactic:
let e := g.quotKerEquivOfSurjective g_surj

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
f' : M' ⧸ Submodule.map f p →ₗ[R] M' ⧸ f.range := factor ⋯
g : ↥f.range →ₗ[R] ↥f'.ker :=
  ↑(LinearEquiv.ofEq (Submodule.map (Submodule.map f p).mkQ f.range) f'.ker ⋯) ∘ₗ
    (Submodule.map f p).mkQ.submoduleMap f.range
g_surj : Surjective ⇑g
g_ker : g.ker = Submodule.map f.rangeRestrict p
e : (↥f.range ⧸ g.ker) ≃ₗ[R] ↥f'.ker := g.quotKerEquivOfSurjective g_surj
⊢ (↥f.range ⧸ Submodule.map f.rangeRestrict p) ≃ₗ[R] ↥f'.ker
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
⊢ p ≤ comap f.rangeRestrict (Submodule.map f.rangeRestrict p)

Tactic:
rw [comap_map_eq]; exact le_sup_left

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

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
B F : M →ₗ[R] M →ₗ[R] M₂
e : M₁ ≃ₗ[R] M
f : End R M
x✝¹ x✝ : M₁
⊢ ((F.compl₁₂ ↑e ↑e ∘ₗ e.symm.conj f) x✝¹) x✝ = (((F ∘ₗ f).compl₁₂ ↑e ↑e) x✝¹) x✝

Tactic:
simp only [LinearEquiv.symm_conj_apply, coe_comp, LinearEquiv.coe_coe, compl₁₂_apply,
      LinearEquiv.apply_symm_apply, Function.comp_apply]

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

Goal state before:
pp: R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
B F : M →ₗ[R] M →ₗ[R] M₂
e : M₁ ≃ₗ[R] M
f : End R M
hₗ : F.compl₁₂ ↑e ↑e ∘ₗ e.symm.conj f = (F ∘ₗ f).compl₁₂ ↑e ↑e
hᵣ : (B.compl₁₂ ↑e ↑e).compl₂ (e.symm.conj f) = (B.compl₂ f).compl₁₂ ↑e ↑e
he : Function.Surjective ⇑↑e
⊢ B.IsAdjointPair F ⇑f ⇑f ↔ (B.compl₁₂ ↑e ↑e).IsAdjointPair (F.compl₁₂ ↑e ↑e) ⇑(e.symm.conj f) ⇑(e.symm.conj f)

Tactic:
isAdjointPair_iff_comp_eq_compl₂,

Goal state after:
R : Type u_1
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
B F : M →ₗ[R] M →ₗ[R] M₂
e : M₁ ≃ₗ[R] M
f : End R M
hₗ : F.compl₁₂ ↑e ↑e ∘ₗ e.symm.conj f = (F ∘ₗ f).compl₁₂ ↑e ↑e
hᵣ : (B.compl₁₂ ↑e ↑e).compl₂ (e.symm.conj f) = (B.compl₂ f).compl₁₂ ↑e ↑e
he : Function.Surjective ⇑↑e
⊢ F ∘ₗ f = B.compl₂ f ↔ F.compl₁₂ ↑e ↑e ∘ₗ e.symm.conj f = (B.compl₁₂ ↑e ↑e).compl₂ (e.symm.conj f)
Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasLimitsOfShape (Discrete J) C
inst✝⁴ : HasLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasEqualizers C
G : C ⥤ D
inst✝² : PreservesLimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesLimitsOfShape (Discrete J) G
inst✝ : PreservesLimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ⋯
Q : C := ⋯
s : P ⟶ Q := ⋯
t : P ⟶ Q := ⋯
I : C := ⋯
i : I ⟶ P := ⋯
⊢ buildLimit (G.map s) (G.map t) ⋯ ⋯ (Fork.ofι (G.map i) ⋯) ≅
    G.mapCone (buildLimit s t ⋯ ⋯ (limit.cone (parallelPair s t)))

Tactic:
· refine Cone.ext (Iso.refl _) ?_
      intro j; dsimp [P, Q, I, i]; simp

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

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W : Subspace K V₁
⊢ (Submodule.dualPairing W).Nondegenerate

Tactic:
constructor
  · rw [LinearMap.separatingLeft_iff_ker_eq_bot, dualPairing_eq]
    apply LinearEquiv.ker
  · intro x h
    rw [← forall_dual_apply_eq_zero_iff K x]
    intro φ
    simpa only [Submodule.dualPairing_apply, dualLift_of_subtype] using
      h (Submodule.Quotient.mk (W.dualLift φ))

Goal state after: