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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
J : Type w
inst✝ : Category.{r, w} J
F : J ⥤ C
D : Cocone F
i j : J
x : ToType (F.obj i)
y : ToType (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
k : J
f : i ⟶ k
g : j ⟶ k
hfg : (ConcreteCategory.hom ((F ⋙ forget C).map f)) x = (ConcreteCategory.hom (F.map g)) y
h1 : (F ⋙ forget C).map f ≫ E.ι.app k = E.ι.app i := E.ι.naturality f
h2 : (F ⋙ forget C).map g ≫ E.ι.app k = E.ι.app j := E.ι.naturality g
⊢ (ConcreteCategory.hom (E.ι.app k)) ((ConcreteCategory.hom ((F ⋙ forget C).map f)) x) =
    (ConcreteCategory.hom (E.ι.app j)) y

Tactic:
hfg

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
J : Type w
inst✝ : Category.{r, w} J
F : J ⥤ C
D : Cocone F
i j : J
x : ToType (F.obj i)
y : ToType (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
k : J
f : i ⟶ k
g : j ⟶ k
hfg : (ConcreteCategory.hom ((F ⋙ forget C).map f)) x = (ConcreteCategory.hom (F.map g)) y
h1 : (F ⋙ forget C).map f ≫ E.ι.app k = E.ι.app i := E.ι.naturality f
h2 : (F ⋙ forget C).map g ≫ E.ι.app k = E.ι.app j := E.ι.naturality g
⊢ (ConcreteCategory.hom (E.ι.app k)) ((ConcreteCategory.hom (F.map g)) y) = (ConcreteCategory.hom (E.ι.app j)) y
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
i j : K
F : J ⥤ K ⥤ C
f : i ⟶ j
⊢ (limitObjIsoLimitCompEvaluation F i).inv ≫ (limit F).map f =
    limMap (F.whiskerLeft ((evaluation K C).map f)) ≫ (limitObjIsoLimitCompEvaluation F j).inv

Tactic:
rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv,
    limit_map_limitObjIsoLimitCompEvaluation_hom]

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X✝ Y✝ : C
f : shrinkYoneda.{w, v, u}.obj X✝ ⟶ shrinkYoneda.{w, v, u}.obj Y✝
⊢ shrinkYoneda.{w, v, u}.map (shrinkYonedaObjObjEquiv (shrinkYonedaEquiv f)) = f

Tactic:
obtain ⟨f, rfl⟩ := shrinkYonedaEquiv.symm.surjective f
    cat_disch

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

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
s : Cocone (directLimitDiagram G f)
m : (directLimitCocone G f).pt ⟶ s.pt
h : ∀ (j : ι), (directLimitCocone G f).ι.app j ≫ m = s.ι.app j
i : ι
⊢ s.ι.app i = ↟(DirectLimit.of R ι (fun i ↦ G i) (fun i j H ↦ f i j H) i) ≫ m

Tactic:
rw [← h]

Goal state after:
R : Type u
inst✝⁶ : Ring R
J : Type v
inst✝⁵ : Category.{t, v} J
F : J ⥤ ModuleCat R
ι : Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Preorder ι
G : ι → Type v
inst✝² : (i : ι) → AddCommGroup (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
s : Cocone (directLimitDiagram G f)
m : (directLimitCocone G f).pt ⟶ s.pt
h : ∀ (j : ι), (directLimitCocone G f).ι.app j ≫ m = s.ι.app j
i : ι
⊢ (directLimitCocone G f).ι.app i ≫ m = ↟(DirectLimit.of R ι (fun i ↦ G i) (fun i j H ↦ f i j H) i) ≫ m
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 : ∀ {j j' : J} (f : j ⟶ j'), (ConcreteCategory.hom (F.map f)) (a j) = a j'
j j' : J
f : j ⟶ j'
⊢ ((Hom.hom (F.map f)) (a j))⁻¹ = (a j')⁻¹

Tactic:
ah f

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y Z : C
f : Y ⟶ Z
inst✝ : IsIso f
⊢ inv (X ◁ f) = X ◁ inv f

Tactic:
by
  cat_disch

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y : C
f : X ⟶ Y
Z : C
inst✝ : IsIso f
⊢ inv (f ▷ Z) = inv f ▷ Z

Tactic:
by
  cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
⊢ (tensorLeftTensor X Y).inv.app Z = (α_ X Y Z).inv

Tactic:
simp [tensorLeftTensor]

Goal state after:
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_3} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
inst✝¹ : CategoryTheory.Linear R C
inst✝ : CategoryTheory.Linear R D
F : C ⥤ D
⊢ Linear R F ↔ ∀ (X : C) (r : R), F.map (r • 𝟙 X) = r • 𝟙 (F.obj X)

Tactic:
by
  constructor
  · intro h X r
    rw [h.map_smul, F.map_id]
  · refine fun h => ⟨fun {X Y} f r => ?_⟩
    have : r • f = (r • 𝟙 X) ≫ f := by simp
    rw [this, F.map_comp, h, Linear.smul_comp, Category.id_comp]

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.CancelIso

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
x y : C
f : x ⟶ y
inst✝ : IsIso f
g : y ⟶ x
h : inv f = g
⊢ f ≫ g = 𝟙 x

Tactic:
rw [← h]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
x y : C
f : x ⟶ y
inst✝ : IsIso f
g : y ⟶ x
h : inv f = g
⊢ f ≫ inv f = 𝟙 x
Module: Mathlib.Tactic.CategoryTheory.CancelIso

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
x y : C
f : x ⟶ y
inst✝ : IsIso f
g : y ⟶ x
h : inv f = g
z : C
k : x ⟶ z
⊢ f ≫ g ≫ k = k

Tactic:
rw [← h]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
x y : C
f : x ⟶ y
inst✝ : IsIso f
g : y ⟶ x
h : inv f = g
z : C
k : x ⟶ z
⊢ f ≫ inv f ≫ k = k
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
X₁ X₂ Y₁ Y₂ : SemimoduleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ Hom.hom ((f ⊗ₘ g) ≫ (Y₁.braiding Y₂).hom) = Hom.hom ((X₁.braiding X₂).hom ≫ (g ⊗ₘ f))

Tactic:
apply TensorProduct.ext'

Goal state after:
R : Type u
inst✝ : CommSemiring R
X₁ X₂ Y₁ Y₂ : SemimoduleCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ ∀ (x : ↑X₁) (y : ↑X₂),
    (Hom.hom ((f ⊗ₘ g) ≫ (Y₁.braiding Y₂).hom)) (x ⊗ₜ[R] y) = (Hom.hom ((X₁.braiding X₂).hom ≫ (g ⊗ₘ f))) (x ⊗ₜ[R] y)
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x✝¹ x✝ : SemimoduleCat R
⊢ Hom.hom ((x✝¹.braiding x✝).hom ≫ (x✝.braiding x✝¹).hom) = Hom.hom (𝟙 (x✝¹ ⊗ x✝))

Tactic:
apply TensorProduct.ext'

Goal state after:
R : Type u
inst✝ : CommSemiring R
x✝¹ x✝ : SemimoduleCat R
⊢ ∀ (x : ↑x✝¹) (y : ↑x✝),
    (Hom.hom ((x✝¹.braiding x✝).hom ≫ (x✝.braiding x✝¹).hom)) (x ⊗ₜ[R] y) = (Hom.hom (𝟙 (x✝¹ ⊗ x✝))) (x ⊗ₜ[R] y)
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
x✝¹ x✝ : C
⊢ δ (F.prod' G) x✝¹ x✝ ≫ μ (F.prod' G) x✝¹ x✝ = 𝟙 ((F.prod' G).obj (x✝¹ ⊗ x✝))

Tactic:
ext
    · simp only [CategoryTheory.prod_comp_fst, prod'_μ_fst, prod'_δ_fst, δ_μ,
        prod'_obj, prod_id]
    · simp only [CategoryTheory.prod_comp_snd, prod'_μ_snd, prod'_δ_snd, δ_μ,
        prod'_obj, prod_id]

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
G : C ⥤ D
⊢ snd ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)) =
    (Iso.refl ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).pt).hom ≫ (c.map G).snd

Tactic:
dsimp only [snd]
        simp

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ PreservesLimit (cospan ((cospan g f).map WalkingCospan.Hom.inr) ((cospan g f).map WalkingCospan.Hom.inl)) G

Tactic:
dsimp
        infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.EpiMono

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesLimit (cospan f f) F
inst✝ : Mono f
this :
  have this := ⋯;
  IsLimit (PullbackCone.mk (F.map (𝟙 X)) (F.map (𝟙 X)) this)
⊢ Mono (F.map f)

Tactic:
simp_rw [F.map_id] at this

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesLimit (cospan f f) F
inst✝ : Mono f
this : IsLimit (PullbackCone.mk (𝟙 (F.obj X)) (𝟙 (F.obj X)) ⋯)
⊢ Mono (F.map f)
Module: Mathlib.CategoryTheory.Limits.Constructions.EpiMono

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesColimit (span f f) F
inst✝ : Epi f
this : IsColimit (PushoutCocone.mk (F.map (𝟙 Y)) (F.map (𝟙 Y)) ⋯)
⊢ Epi (F.map f)

Tactic:
simp_rw [F.map_id] at this

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : PreservesColimit (span f f) F
inst✝ : Epi f
this : IsColimit (PushoutCocone.mk (𝟙 (F.obj Y)) (𝟙 (F.obj Y)) ⋯)
⊢ Epi (F.map f)
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsMultiplicative
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
hf : W.multiplicativeClosure f✝
⊢ W f✝

Tactic:
induction hf with
  | of _ hf₀ => exact hf₀
  | id x => exact W.id_mem x
  | comp_of _ _ _ hg hf => exact W.comp_mem _ _ hf hg

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
h : W.multiplicativeClosure = W
⊢ W.IsMultiplicative

Tactic:
rw [← h]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
h : W.multiplicativeClosure = W
⊢ W.multiplicativeClosure.IsMultiplicative
Module: Mathlib.CategoryTheory.MorphismProperty.Concrete

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : C
⊢ MorphismProperty.bijective C (𝟙 X)

Tactic:
delta MorphismProperty.bijective

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : C
⊢ Bijective ⇑(ConcreteCategory.hom (𝟙 X))
Module: Mathlib.CategoryTheory.MorphismProperty.Concrete

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : MorphismProperty.bijective C f
hg : MorphismProperty.bijective C g
⊢ MorphismProperty.bijective C (f ≫ g)

Tactic:
delta MorphismProperty.bijective

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : MorphismProperty.bijective C f
hg : MorphismProperty.bijective C g
⊢ Bijective ⇑(ConcreteCategory.hom (f ≫ g))
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 : C
⊢ (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (ρ_ (𝟙_ C)).hom ▷ X = 𝟙_ C ◁ (λ_ X).hom

Tactic:
by rw [triangle_assoc_comp_right]

Goal state after:
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
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inst✝ : Invertible x
⊢ (⅟x).fst * x.fst = 1

Tactic:
rw [← fst_mul, invOf_mul_self, fst_one]

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
β : L₁ ⟶ L₂
βα : β ≫ α = 𝟙 L₁
⊢ (conjugateEquiv adj₁ adj₂) α ≫ (conjugateEquiv adj₂ adj₁) β = 𝟙 R₁

Tactic:
by
  rw [conjugateEquiv_comp, βα, conjugateEquiv_id]

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

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝¹ : Category.{v₁, u₁} A
inst✝ : Category.{v₂, u₂} B
L : A ⥤ B
R : B ⥤ A
adj : L ⊣ R
⊢ (conjugateEquiv adj (Adjunction.id.comp adj)) L.leftUnitor.hom = R.rightUnitor.inv

Tactic:
by
  cat_disch

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

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝¹ : Category.{v₁, u₁} A
inst✝ : Category.{v₂, u₂} B
L : A ⥤ B
R : B ⥤ A
adj : L ⊣ R
⊢ (conjugateEquiv adj (adj.comp Adjunction.id)) L.rightUnitor.hom = R.leftUnitor.inv

Tactic:
by
  cat_disch

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

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
this : Algebra R S := ⋯
⊢ Hom.hom ((restrictScalars f).map α) = Hom.hom ((restrictScalars f).map β)

Tactic:
apply TensorProduct.ext'

Goal state after:
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
α β : (extendScalars f).obj M ⟶ N
h : ∀ (m : ↑M), (ConcreteCategory.hom α) (1 ⊗ₜ[R] m) = (ConcreteCategory.hom β) (1 ⊗ₜ[R] m)
this : Algebra R S := ⋯
⊢ ∀ (x : ↑((restrictScalars f).obj (of S S))) (y : ↑M),
    (Hom.hom ((restrictScalars f).map α)) (x ⊗ₜ[R] y) = (Hom.hom ((restrictScalars f).map β)) (x ⊗ₜ[R] y)
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra S A
inst✝³ : Bialgebra R B
inst✝² : Algebra R A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
hcounit :
  ⇑counit =
    ⇑((↑(Algebra.TensorProduct.rid R S S)).comp
          (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B))).toLinearMap
hcomul :
  ⇑comul =
    ⇑((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B)).comp
          (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B))).toLinearMap
⊢ ((↑(Algebra.TensorProduct.rid R S S)).comp (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B))) 1 = 1

Tactic:
simp only [map_one, map_mul]

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra S A
inst✝³ : Bialgebra R B
inst✝² : Algebra R A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
hcounit :
  ⇑counit =
    ⇑((↑(Algebra.TensorProduct.rid R S S)).comp
          (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B))).toLinearMap
hcomul :
  ⇑comul =
    ⇑((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B)).comp
          (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B))).toLinearMap
x y : A ⊗[R] B
⊢ ((↑(Algebra.TensorProduct.rid R S S)).comp (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B)))
      (x * y) =
    ((↑(Algebra.TensorProduct.rid R S S)).comp (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B))) x *
      ((↑(Algebra.TensorProduct.rid R S S)).comp (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B))) y

Tactic:
simp only [map_one, map_mul]

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra S A
inst✝³ : Bialgebra R B
inst✝² : Algebra R A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
hcounit :
  ⇑counit =
    ⇑((↑(Algebra.TensorProduct.rid R S S)).comp
          (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B))).toLinearMap
hcomul :
  ⇑comul =
    ⇑((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B)).comp
          (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B))).toLinearMap
⊢ ((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B)).comp
        (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B)))
      1 =
    1

Tactic:
simp only [map_one, map_mul]

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: case refine_4
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Bialgebra S A
inst✝³ : Bialgebra R B
inst✝² : Algebra R A
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R S A
hcounit :
  ⇑counit =
    ⇑((↑(Algebra.TensorProduct.rid R S S)).comp
          (Algebra.TensorProduct.map (counitAlgHom S A) (counitAlgHom R B))).toLinearMap
hcomul :
  ⇑comul =
    ⇑((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B)).comp
          (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B))).toLinearMap
x y : A ⊗[R] B
⊢ ((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B)).comp
        (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B)))
      (x * y) =
    ((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B)).comp
          (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B)))
        x *
      ((↑(Algebra.TensorProduct.tensorTensorTensorComm R S R S A A B B)).comp
          (Algebra.TensorProduct.map (comulAlgHom S A) (comulAlgHom R B)))
        y

Tactic:
simp only [map_one, map_mul]

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : FunLike F α β
inst✝² : CoheytingAlgebra α
inst✝¹ : CoheytingAlgebra β
inst✝ : CoheytingHomClass F α β
f : F
a : α
⊢ f (￢a) = ￢f a

Tactic:
by rw [← top_sdiff', ← top_sdiff', map_sdiff, map_top]

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : FunLike F α β
inst✝² : CoheytingAlgebra α
inst✝¹ : CoheytingAlgebra β
inst✝ : CoheytingHomClass F α β
f : F
a b : α
⊢ f (a ∆ b) = f a ∆ f b

Tactic:
simp_rw [symmDiff, map_sup, map_sdiff]

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case neg
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
h_left : ∀ (x y : R), y ∈ s → x * y ∈ s
h_right : ∀ (y x : R), y ∈ s → y * x ∈ s
z : R
h_left' : ∀ {x y : R}, y ∈ closure s → x * y ∈ closure s
h_right' : ∀ {y x : R}, y ∈ closure s → y * x ∈ closure s
I : TwoSidedIdeal R := mk' ↑(closure s) ⋯ ⋯ ⋯ ⋯ ⋯
J : TwoSidedIdeal R
hJ : s ⊆ ↑J
x : R
hx✝ : x ∈ closure s
hx : x ∈ J
⊢ -x ∈ J

Tactic:
exact J.neg_mem hx

Goal state after:
Module: Mathlib.RingTheory.Localization.Integer

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
hf : Injective f
⊢ Injective (integerMultiple M s f)

Tactic:
by
  intro i j h
  rw [← SetLike.coe_eq_coe, ← hf.eq_iff,
    ← (IsLocalization.smul_bijective S (commonDenom M s f)).injective.eq_iff,
    ← map_integerMultiple M s f i, ← map_integerMultiple M s f j, h]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst : Mono g
W : C
fst' snd' : W ⟶ P
heq : fst' ≫ fst = snd' ≫ fst
⊢ fst' ≫ snd = snd' ≫ snd

Tactic:
by simp [← cancel_mono g, ← h.w, reassoc_of% heq]

Goal state after:
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
T : Type u_5
B : Type u_6
inst✝⁷ : CommSemiring T
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra T B
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R T B
inst✝ : IsScalarTower R A B
⊢ IsLocalizedModule S (IsScalarTower.toAlgHom R T B).toLinearMap ↔
    IsBaseChange A (IsScalarTower.toAlgHom R T B).toLinearMap

Tactic:
← isLocalizedModule_iff_isBaseChange (S := S)

Goal state after:
R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹⁰ : CommSemiring A
inst✝⁹ : Algebra R A
inst✝⁸ : IsLocalization S A
T : Type u_5
B : Type u_6
inst✝⁷ : CommSemiring T
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra R T
inst✝⁴ : Algebra T B
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R T B
inst✝ : IsScalarTower R A B
⊢ IsLocalizedModule S (IsScalarTower.toAlgHom R T B).toLinearMap ↔
    IsLocalizedModule S (IsScalarTower.toAlgHom R T B).toLinearMap
Module: Mathlib.Control.Bifunctor

Goal state before:
pp: F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α : Type u₀
⊢ ∀ {α_1 : Type u₁} (x : F α α_1), id <$> x = x

Tactic:
simp [Functor.map, functor_norm]

Goal state after:
Module: Mathlib.Control.Bifunctor

Goal state before:
pp: F : Type u₀ → Type u₁ → Type u₂
inst✝¹ : Bifunctor F
inst✝ : LawfulBifunctor F
α : Type u₀
⊢ ∀ {α_1 β γ : Type u₁} (g : α_1 → β) (h : β → γ) (x : F α α_1), (h ∘ g) <$> x = h <$> g <$> x

Tactic:
simp [Functor.map, functor_norm]

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

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
| x • 0

Tactic:
rw [← zero_mk 1, smul_def, smul_zero, zero_mk]

Goal state after:
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
| 0
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
X : C
inst✝ : IsIso T.μ
x✝ : IsSplitMono (T.η.app X)
⊢ retraction (T.η.app X) ≫ T.η.app X = T.map (𝟙 X)

Tactic:
← show T.η.app X ≫ retraction (T.η.app X) = 𝟙 X from IsSplitMono.id _,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
X : C
inst✝ : IsIso T.μ
x✝ : IsSplitMono (T.η.app X)
⊢ retraction (T.η.app X) ≫ T.η.app X = T.map (T.η.app X ≫ retraction (T.η.app X))