mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: case refine_1
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
t : IsLimit c
this : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
x✝¹ : J
x✝ :
  ((Functor.const J).obj
        ((forget MonCat).mapCone
            { pt := of (Types.Small.limitCone (F ⋙ forget MonCat)).pt,
              π := { app := fun j ↦ ofHom (limitπMonoidHom F j), naturality := ⋯ } }).pt).obj
    x✝¹
⊢ (limitπMonoidHom F x✝¹) x✝ =
    (ConcreteCategory.hom (c.π.app x✝¹)) ((ConcreteCategory.hom (t.lift (Types.coneOfSection ⋯))) PUnit.unit)

Tactic:
simp [← CategoryTheory.comp_apply]

Goal state after:
case refine_1
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
t : IsLimit c
this : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
x✝¹ : J
x✝ :
  ((Functor.const J).obj
        ((forget MonCat).mapCone
            { pt := of (Types.Small.limitCone (F ⋙ forget MonCat)).pt,
              π := { app := fun j ↦ ofHom (limitπMonoidHom F j), naturality := ⋯ } }).pt).obj
    x✝¹
⊢ (limitπMonoidHom F x✝¹) x✝ = (ConcreteCategory.hom ((Types.coneOfSection ⋯).π.app x✝¹)) PUnit.unit
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ GrpCat
a : (j : J) → ↑(F.obj j)
ah : a ∈ (F ⋙ forget GrpCat).sections
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom ((F ⋙ forget GrpCat).map f)) (a⁻¹ j) = a⁻¹ j'

Tactic:
simp only [Functor.comp_map, Pi.inv_apply]

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ GrpCat
a : (j : J) → ↑(F.obj j)
ah : a ∈ (F ⋙ forget GrpCat).sections
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (↾⇑(ConcreteCategory.hom (F.map f)))) (a j)⁻¹ = (a j')⁻¹
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
W X Y Z : D
⊢ F.map ((α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom) =
    F.map ((α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom)

Tactic:
simp only [Functor.map_comp, fData.whiskerRight_eq, fData.associator_eq, Iso.trans_assoc,
      Iso.trans_hom, Iso.symm_hom, tensorIso_hom, Iso.refl_hom, tensorHom_id, id_tensorHom,
      comp_whiskerRight, whisker_assoc, assoc, fData.whiskerLeft_eq, whiskerLeft_comp,
      Iso.hom_inv_id_assoc, whiskerLeft_hom_inv_assoc, hom_inv_whiskerRight_assoc,
      Iso.inv_hom_id_assoc, Iso.cancel_iso_inv_left]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
W X Y Z : D
⊢ (fData.μIso (W ⊗ X) Y).inv ▷ F.obj Z ≫
      (fData.μIso W X).inv ▷ F.obj Y ▷ F.obj Z ≫
        (α_ (F.obj W) (F.obj X) (F.obj Y)).hom ▷ F.obj Z ≫
          (α_ (F.obj W) (F.obj X ⊗ F.obj Y) (F.obj Z)).hom ≫
            F.obj W ◁ (fData.μIso X Y).hom ▷ F.obj Z ≫
              F.obj W ◁ (fData.μIso X Y).inv ▷ F.obj Z ≫
                F.obj W ◁ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫
                  F.obj W ◁ F.obj X ◁ (fData.μIso Y Z).hom ≫
                    F.obj W ◁ (fData.μIso X (Y ⊗ Z)).hom ≫ (fData.μIso W (X ⊗ Y ⊗ Z)).hom =
    (fData.μIso (W ⊗ X) Y).inv ▷ F.obj Z ≫
      (α_ (F.obj (W ⊗ X)) (F.obj Y) (F.obj Z)).hom ≫
        F.obj (W ⊗ X) ◁ (fData.μIso Y Z).hom ≫
          (fData.μIso W X).inv ▷ F.obj (Y ⊗ Z) ≫
            (α_ (F.obj W) (F.obj X) (F.obj (Y ⊗ Z))).hom ≫
              F.obj W ◁ (fData.μIso X (Y ⊗ Z)).hom ≫ (fData.μIso W (X ⊗ Y ⊗ Z)).hom
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hg : IsIso g
hfg : IsIso (f ≫ g)
⊢ isomorphisms C f

Tactic:
simpa using (inferInstance : IsIso ((f ≫ g) ≫ inv g))

Goal state after:
Module: Mathlib.CategoryTheory.ConcreteCategory.EpiMono

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : (forget C).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
⊢ IsIso f ↔ IsIso (↾⇑(hom f))

Tactic:
refine ⟨fun _ ↦ inferInstance, fun h ↦ ?_⟩

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : (forget C).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
h : IsIso (↾⇑(hom f))
⊢ IsIso f
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
⊢ HasPullback f.op g.op

Tactic:
hasPullback_op_iff_hasPushout

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : HasPushout f g
⊢ HasPushout f g
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| (f₁ ⊗ₘ (f₂ ⊗ₘ g₁) ⊗ₘ g₂) ≫ (𝟙 Y₁ ⊗ₘ (β_ Y₂ V₁).hom ⊗ₘ 𝟙 V₂)

pp: case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| 𝟙 Y₁ ⊗ₘ (α_ V₁ Y₂ V₂).hom

pp: case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv

pp: case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| (α_ X₁ X₂ (U₁ ⊗ U₂)).hom

pp: case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| 𝟙 X₁ ⊗ₘ (α_ X₂ U₁ U₂).inv

Tactic:
rw [tensorHom_comp_tensorHom, tensorHom_comp_tensorHom, comp_id f₁, ← id_comp f₁, comp_id g₂,
      ← id_comp g₂, braiding_naturality, ← tensorHom_comp_tensorHom, ← tensorHom_comp_tensorHom]

Goal state after:
case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| (𝟙 X₁ ⊗ₘ (β_ X₂ U₁).hom ⊗ₘ 𝟙 U₂) ≫ (f₁ ⊗ₘ (g₁ ⊗ₘ f₂) ⊗ₘ g₂)

case a.a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| 𝟙 Y₁ ⊗ₘ (α_ V₁ Y₂ V₂).hom

case a.a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| (α_ Y₁ V₁ (Y₂ ⊗ V₂)).inv

case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| (α_ X₁ X₂ (U₁ ⊗ U₂)).hom

case a.a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
| 𝟙 X₁ ⊗ₘ (α_ X₂ U₁ U₂).inv
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
⊢ 𝟙 (((X₁ ⊗ X₂) ⊗ Y₁ ⊗ Y₂) ⊗ Z₁ ⊗ Z₂) ⊗≫
      X₁ ◁ ((β_ X₂ Y₁).hom ▷ (Y₂ ⊗ Z₁) ≫ (Y₁ ⊗ X₂) ◁ (β_ Y₂ Z₁).hom) ▷ Z₂ ⊗≫
        X₁ ◁ Y₁ ◁ (β_ X₂ Z₁).hom ▷ Y₂ ▷ Z₂ ⊗≫ 𝟙 ((X₁ ⊗ Y₁ ⊗ Z₁) ⊗ X₂ ⊗ Y₂ ⊗ Z₂) =
    (α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (Z₁ ⊗ Z₂)).hom ≫
      (X₁ ⊗ X₂) ◁
          ((α_ Y₁ Y₂ (Z₁ ⊗ Z₂)).hom ≫
            Y₁ ◁ (α_ Y₂ Z₁ Z₂).inv ≫ Y₁ ◁ (β_ Y₂ Z₁).hom ▷ Z₂ ≫ Y₁ ◁ (α_ Z₁ Y₂ Z₂).hom ≫ (α_ Y₁ Z₁ (Y₂ ⊗ Z₂)).inv) ≫
        (α_ X₁ X₂ ((Y₁ ⊗ Z₁) ⊗ Y₂ ⊗ Z₂)).hom ≫
          X₁ ◁ (α_ X₂ (Y₁ ⊗ Z₁) (Y₂ ⊗ Z₂)).inv ≫
            X₁ ◁
                ((α_ X₂ Y₁ Z₁).inv ≫
                    (β_ X₂ Y₁).hom ▷ Z₁ ≫ (α_ Y₁ X₂ Z₁).hom ≫ Y₁ ◁ (β_ X₂ Z₁).hom ≫ (α_ Y₁ Z₁ X₂).inv) ▷
                  (Y₂ ⊗ Z₂) ≫
              X₁ ◁ (α_ (Y₁ ⊗ Z₁) X₂ (Y₂ ⊗ Z₂)).hom ≫ (α_ X₁ (Y₁ ⊗ Z₁) (X₂ ⊗ Y₂ ⊗ Z₂)).inv

Tactic:
rw [← whisker_exchange]; monoidal

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
inst✝² : Category.{v₄, u₄} D
inst✝¹ : Category.{v₅, u₅} E
inst✝ : Category.{v₆, u₆} F
G : A ⥤ D
H : B ⥤ E
K : C ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : D ⥤ E
R₂ : E ⥤ D
L₃ : B ⥤ C
R₃ : C ⥤ B
L₄ : E ⥤ F
R₄ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
adj₄ : L₄ ⊣ R₄
α : TwoSquare G L₁ L₂ H
β : TwoSquare H L₃ L₄ K
c : C
⊢ adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫
        R₂.map (R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c))))) ≫
          R₂.map (R₄.map (β.natTrans.app (L₁.obj (R₁.obj (R₃.obj c))))) ≫
            R₂.map (R₄.map (K.map (L₃.map (adj₁.counit.app (R₃.obj c))))) ≫
              R₂.map (R₄.map (K.map (adj₃.counit.app c))) =
    adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      (R₂.map
            (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c)))) ≫
              R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c)) ≫ H.map (adj₁.counit.app (R₃.obj c))))) ≫
          R₂.map (R₄.map (β.natTrans.app (R₃.obj c)))) ≫
        R₂.map (R₄.map (K.map (adj₃.counit.app c)))

Tactic:
R₂.map_comp,

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
inst✝² : Category.{v₄, u₄} D
inst✝¹ : Category.{v₅, u₅} E
inst✝ : Category.{v₆, u₆} F
G : A ⥤ D
H : B ⥤ E
K : C ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : D ⥤ E
R₂ : E ⥤ D
L₃ : B ⥤ C
R₃ : C ⥤ B
L₄ : E ⥤ F
R₄ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
adj₄ : L₄ ⊣ R₄
α : TwoSquare G L₁ L₂ H
β : TwoSquare H L₃ L₄ K
c : C
⊢ adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫
        R₂.map (R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c))))) ≫
          R₂.map (R₄.map (β.natTrans.app (L₁.obj (R₁.obj (R₃.obj c))))) ≫
            R₂.map (R₄.map (K.map (L₃.map (adj₁.counit.app (R₃.obj c))))) ≫
              R₂.map (R₄.map (K.map (adj₃.counit.app c))) =
    adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫
      ((R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫
            R₂.map (R₄.map (L₄.map (α.natTrans.app (R₁.obj (R₃.obj c)) ≫ H.map (adj₁.counit.app (R₃.obj c)))))) ≫
          R₂.map (R₄.map (β.natTrans.app (R₃.obj c)))) ≫
        R₂.map (R₄.map (K.map (adj₃.counit.app c)))
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
n : ℕ
⊢ (List.map (fun i ↦ x.fst ^ (n.succ.pred - i + i) •> x.snd) (List.range n.succ)).sum =
    n.succ •> x.fst ^ n.succ.pred •> x.snd

Tactic:
simp_rw [Nat.pred_succ]

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n✝ : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
n : ℕ
⊢ (List.map (fun i ↦ x.fst ^ (n - i + i) •> x.snd) (List.range n.succ)).sum = n.succ •> x.fst ^ n •> x.snd
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁶ : AddCommGroup M
inst✝⁵ : Semiring R
inst✝⁴ : Module Rᵐᵒᵖ M
inst✝³ : Module R M
inst✝² : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
inst✝¹ : Invertible x
inst✝ : Invertible x.fst
⊢ (⅟x).snd = -(⅟x.fst •> x.snd <• ⅟x.fst)

Tactic:
let := invertibleOfInvertibleFst x
  convert! congr_arg (TrivSqZeroExt.snd (R := R) (M := M)) (_ : _ = ⅟x)
  convert! rfl

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

Goal state before:
pp: case hr
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
⊢ (comul ∘ₗ LinearMap.fst R A B) ∘ₗ inr R A B =
    (TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul) ∘ₗ inr R A B

Tactic:
· rw [comp_assoc, fst_comp_inr, comp_zero, comp_assoc, comul_comp_inr, ← comp_assoc,
      ← TensorProduct.map_comp, fst_comp_inr, TensorProduct.map_zero_left, zero_comp]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : AddCommMonoid C
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : Module R C
inst✝² : CoalgebraStruct R A
inst✝¹ : CoalgebraStruct R B
inst✝ : CoalgebraStruct R C
e✝ e' e : A ≃ₗc[R] B
⊢ ↑(TensorProduct.congr e.toLinearEquiv e.toLinearEquiv).symm ∘ₗ comul = comul ∘ₗ ↑e.toLinearEquiv.symm

Tactic:
LinearEquiv.toLinearMap_symm_comp_eq

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : AddCommMonoid C
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : Module R C
inst✝² : CoalgebraStruct R A
inst✝¹ : CoalgebraStruct R B
inst✝ : CoalgebraStruct R C
e✝ e' e : A ≃ₗc[R] B
⊢ comul = ↑(TensorProduct.congr e.toLinearEquiv e.toLinearEquiv) ∘ₗ comul ∘ₗ ↑e.toLinearEquiv.symm
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: S : Type u_1
R : Type u
M : Type v
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : Module R M
inst✝⁵ : Module Rᵐᵒᵖ M
inst✝⁴ : SMulCommClass R Rᵐᵒᵖ M
inst✝³ : IsScalarTower S R M
inst✝² : IsScalarTower S Rᵐᵒᵖ M
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra S A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
⊢ Subalgebra.map (lift f g hg hfg hgf) (inlAlgHom S R M).range ⊔
      Algebra.adjoin S (⇑(lift f g hg hfg hgf) '' Set.range inr) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range ⇑g)

Tactic:
← AlgHom.range_comp,

Goal state after:
S : Type u_1
R : Type u
M : Type v
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Semiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : Module R M
inst✝⁵ : Module Rᵐᵒᵖ M
inst✝⁴ : SMulCommClass R Rᵐᵒᵖ M
inst✝³ : IsScalarTower S R M
inst✝² : IsScalarTower S Rᵐᵒᵖ M
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra S A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
⊢ ((lift f g hg hfg hgf).comp (inlAlgHom S R M)).range ⊔ Algebra.adjoin S (⇑(lift f g hg hfg hgf) '' Set.range inr) =
    Subalgebra.map f ⊤ ⊔ Algebra.adjoin S (Set.range ⇑g)
Module: Mathlib.RingTheory.Bialgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
F : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : FunLike F A B
inst✝ : BialgHomClass F R A B
c : F
r : R
⊢ c ((algebraMap R A) r) = (algebraMap R B) r

Tactic:
by
    simp only [Algebra.algebraMap_eq_smul_one, map_smul, map_one]

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

Goal state before:
pp: case refine_1.refine_1
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
z : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
s₁ s₂ : S
⊢ evalAt f (s₁ + s₂) g = evalAt f s₁ g + evalAt f s₂ g

Tactic:
ext
      dsimp only [m2, evalAt_apply, LinearMap.add_apply]
      rw [← add_smul]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Unique

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
G G' G'' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
adj3 : F ⊣ G''
x : D
⊢ (adj1.rightAdjointUniq adj2).hom.app x ≫ (adj2.rightAdjointUniq adj3).hom.app x =
    (adj1.rightAdjointUniq adj3).hom.app x

Tactic:
rw [← rightAdjointUniq_trans adj1 adj2 adj3]

Goal state after:
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
G G' G'' : D ⥤ C
adj1 : F ⊣ G
adj2 : F ⊣ G'
adj3 : F ⊣ G''
x : D
⊢ (adj1.rightAdjointUniq adj2).hom.app x ≫ (adj2.rightAdjointUniq adj3).hom.app x =
    ((adj1.rightAdjointUniq adj2).hom ≫ (adj2.rightAdjointUniq adj3).hom).app x
Module: Mathlib.CategoryTheory.Category.Bipointed

Goal state before:
pp: X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedFst.obj Y✝
⊢ { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
          invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
          left_inv := ⋯, right_inv := ⋯ }.symm
      (f ≫ g) =
    pointedToBipointedFst.map f ≫
      { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
            invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ },
            left_inv := ⋯, right_inv := ⋯ }.symm
        g

Tactic:
by
        apply Bipointed.Hom.ext
        funext x
        cases x <;> rfl

Goal state after:
Module: Mathlib.CategoryTheory.Category.Bipointed

Goal state before:
pp: X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedSnd.obj Y✝
⊢ { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
          invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ },
          left_inv := ⋯, right_inv := ⋯ }.symm
      (f ≫ g) =
    pointedToBipointedSnd.map f ≫
      { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
            invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ },
            left_inv := ⋯, right_inv := ⋯ }.symm
        g

Tactic:
by
        apply Bipointed.Hom.ext
        funext x
        cases x <;> rfl

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

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
M N O : C
inst✝⁶ : ComonObj M
inst✝⁵ : ComonObj N
inst✝⁴ : ComonObj O
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : MonoidalCategory D
A : C
inst✝¹ : ComonObj A
F : C ⥤ D
inst✝ : F.OplaxMonoidal
⊢ (F.map Δ ≫ δ F A A) ≫ (F.map ε ≫ η F) ▷ F.obj A = (λ_ (F.obj A)).inv

Tactic:
simp_rw [comp_whiskerRight, Category.assoc, δ_natural_left_assoc, left_unitality,
      ← F.map_comp_assoc, counit_comul]

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
z : S
a : R
n : ℕ
h : z * (algebraMap R S) ↑(a, ⟨(fun x_1 ↦ x ^ x_1) n, ⋯⟩).2 = (algebraMap R S) (a, ⟨(fun x_1 ↦ x ^ x_1) n, ⋯⟩).1
⊢ ∃ n a, z * (algebraMap R S) x ^ n = (algebraMap R S) a

Tactic:
use n, a

Goal state after:
case h
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
z : S
a : R
n : ℕ
h : z * (algebraMap R S) ↑(a, ⟨(fun x_1 ↦ x ^ x_1) n, ⋯⟩).2 = (algebraMap R S) (a, ⟨(fun x_1 ↦ x ^ x_1) n, ⋯⟩).1
⊢ z * (algebraMap R S) x ^ n = (algebraMap R S) a
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
S : Type u_2
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommSemiring P
Q : Type u_4
inst✝³ : CommSemiring Q
inst✝² : Algebra P Q
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
H : ∀ (a : P), ∃ b m, f b = f r ^ m * a
a : P
n : ℕ
b : R
m : ℕ
e : f b = f r ^ m * a
⊢ f (r ^ (0 + n) * b) = f r ^ (0 + (n + m)) * a

Tactic:
simp [e, pow_add]

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
S : Type u_2
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommSemiring P
Q : Type u_4
inst✝³ : CommSemiring Q
inst✝² : Algebra P Q
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
H : ∀ (a : P), ∃ b m, f b = f r ^ m * a
a : P
n : ℕ
b : R
m : ℕ
e : f b = f r ^ m * a
⊢ f r ^ n * (f r ^ m * a) = f r ^ n * f r ^ m * a
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
I : TwoSidedIdeal R
⊢ span s ≤ I ↔ s ⊆ ↑I

Tactic:
rw [TwoSidedIdeal.ringCon_le_iff, RingCon.gi _ |>.gc]

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
I : TwoSidedIdeal R
⊢ (fun a b ↦ a - b ∈ s) ≤ ⇑I.ringCon ↔ s ⊆ ↑I
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: S : Type u_4
T : Type u_5
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra S T
R : Type u_6
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
h₁ : Function.Surjective ⇑(algebraMap S T)
h₂ : Function.Surjective ⇑(algebraMap R S)
r : R
hr : IsUnit ((algebraMap R T) r)
n : ℕ
hn : r ^ n • RingHom.ker (algebraMap R T) ≤ RingHom.ker (algebraMap R S)
⊢ Away ((algebraMap R S) r) T

Tactic:
refine Away.of_surjective h₁ ?_ n ?_

Goal state after:
case refine_1
S : Type u_4
T : Type u_5
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra S T
R : Type u_6
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
h₁ : Function.Surjective ⇑(algebraMap S T)
h₂ : Function.Surjective ⇑(algebraMap R S)
r : R
hr : IsUnit ((algebraMap R T) r)
n : ℕ
hn : r ^ n • RingHom.ker (algebraMap R T) ≤ RingHom.ker (algebraMap R S)
⊢ IsUnit ((algebraMap S T) ((algebraMap R S) r))

case refine_2
S : Type u_4
T : Type u_5
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra S T
R : Type u_6
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
h₁ : Function.Surjective ⇑(algebraMap S T)
h₂ : Function.Surjective ⇑(algebraMap R S)
r : R
hr : IsUnit ((algebraMap R T) r)
n : ℕ
hn : r ^ n • RingHom.ker (algebraMap R T) ≤ RingHom.ker (algebraMap R S)
⊢ (algebraMap R S) r ^ n • RingHom.ker (algebraMap S T) ≤ ⊥
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case mpr
R : Type u
inst✝ : Ring R
I : Ideal R
M : Set (Ideal R)
hM : ∀ J ∈ M, J.IsMaximal ∨ J = ⊤
hInf : I = sInf M
⊢ I.jacobson = I

Tactic:
refine le_antisymm (fun x hx => ?_) le_jacobson

Goal state after:
case mpr
R : Type u
inst✝ : Ring R
I : Ideal R
M : Set (Ideal R)
hM : ∀ J ∈ M, J.IsMaximal ∨ J = ⊤
hInf : I = sInf M
x : R
hx : x ∈ I.jacobson
⊢ x ∈ I
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
f : R →+* S
a b : R
H : ∀ (a_1 : S), ∃ b_1 m, f b_1 = f (a * b) ^ m * a_1
s : S
n : ℕ
c : R
m : ℕ
e : f c = f (a * b) ^ m * s
⊢ f (a ^ (0 + n) * c) = f (a ^ (0 + (n + m)) * b ^ m) * s

Tactic:
simp [e, pow_add]

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
f : R →+* S
a b : R
H : ∀ (a_1 : S), ∃ b_1 m, f b_1 = f (a * b) ^ m * a_1
s : S
n : ℕ
c : R
m : ℕ
e : f c = f (a * b) ^ m * s
⊢ f a ^ n * ((f a * f b) ^ m * s) = f a ^ n * f a ^ m * f b ^ m * s