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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ C
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
j : J
⊢ m ≫ c.π.app j = (hom ((hc (op s.pt)).lift ((coyoneda.obj (op s.pt)).mapCone s))) (𝟙 s.pt) ≫ c.π.app j

Tactic:
have eq := congr_hom ((hc (op s.pt)).fac ((coyoneda.obj (op s.pt)).mapCone s) j) (𝟙 s.pt)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ C
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
j : J
eq :
  (hom ((hc (op s.pt)).lift ((coyoneda.obj (op s.pt)).mapCone s) ≫ ((coyoneda.obj (op s.pt)).mapCone c).π.app j))
      (𝟙 s.pt) =
    (hom (((coyoneda.obj (op s.pt)).mapCone s).π.app j)) (𝟙 s.pt)
⊢ m ≫ c.π.app j = (hom ((hc (op s.pt)).lift ((coyoneda.obj (op s.pt)).mapCone s))) (𝟙 s.pt) ≫ c.π.app j
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : Category.{t, w} J
F : J ⥤ C
c : Cone F
x✝ : (X : Cᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone c)
⊢ (fun h x ↦ isLimitOfPreserves (coyoneda.obj x) h) ((fun h ↦ coyonedaJointlyReflectsLimits F c h) x✝) = x✝

Tactic:
ext; apply Subsingleton.elim

Goal state after:
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 s
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
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFilteredOrEmpty J
D : Cocone F
hD : IsColimit D
x : ToType D.pt
k : J
⊢ ∃ j x_1 y, (ConcreteCategory.hom (D.ι.app j)) y = x

Tactic:
obtain ⟨j, y, rfl⟩ := isColimit_exists_rep F hD x
  refine ⟨IsFiltered.max k j, IsFiltered.leftToMax _ _, F.map (IsFiltered.rightToMax _ _) y, ?_⟩
  rw [← ConcreteCategory.comp_apply]
  congr 1
  simp

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
⊢ IsLimit ((forget₂ SemiRingCat MonCat).mapCone (limitCone F))

Tactic:
let _ : Small.{u} (Functor.sections ((F ⋙ forget₂ _ MonCat) ⋙ forget MonCat)) :=
    inferInstanceAs <| Small.{u} (Functor.sections (F ⋙ forget SemiRingCat))
  apply MonCat.HasLimits.limitConeIsLimit (F ⋙ forget₂ SemiRingCat MonCat.{u})

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

Goal state before:
pp: C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalPreadditive C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
X✝ Y✝ Z✝ : D
⊢ F.map (X✝ ◁ 0) = F.map 0

Tactic:
simp [Functor.Monoidal.map_whiskerLeft]

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X : C
f : J → C
j : J
⊢ X ◁ biproduct.ι f j ≫ (leftDistributor X f).hom = biproduct.ι (fun j ↦ X ⊗ f j) j

Tactic:
classical
  cases nonempty_fintype J
  simp [leftDistributor_hom, Preadditive.comp_sum, ← whiskerLeft_comp_assoc,
    biproduct.ι_π, whiskerLeft_dite, dite_comp]

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
f : J → C
X Y : C
g h : X ⟶ (⨁ f) ⊗ Y
w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y = h ≫ biproduct.π f j ▷ Y
⊢ g = h

Tactic:
by
  cases nonempty_fintype J
  apply (cancel_mono (rightDistributor f Y).hom).mp
  ext
  simp [w]

Goal state after:
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 : C ⥤ D
G : D ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y Z : C
⊢ (G.map (δ F (X ⊗ Y) Z) ≫ δ G (F.obj (X ⊗ Y)) (F.obj Z)) ≫
      (G.map (δ F X Y) ≫ δ G (F.obj X) (F.obj Y)) ▷ (F ⋙ G).obj Z ≫
        (α_ ((F ⋙ G).obj X) ((F ⋙ G).obj Y) ((F ⋙ G).obj Z)).hom =
    (F ⋙ G).map (α_ X Y Z).hom ≫
      (G.map (δ F X (Y ⊗ Z)) ≫ δ G (F.obj X) (F.obj (Y ⊗ Z))) ≫
        (F ⋙ G).obj X ◁ (G.map (δ F Y Z) ≫ δ G (F.obj Y) (F.obj Z))

Tactic:
by
    dsimp
    rw [comp_whiskerRight, assoc, assoc, assoc, δ_natural_left_assoc, associativity,
      ← G.map_comp_assoc, ← G.map_comp_assoc, assoc, associativity, map_comp, map_comp,
      assoc, assoc, MonoidalCategory.whiskerLeft_comp, δ_natural_right_assoc]

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

Goal state before:
pp: case δ
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
eq : a.toLaxMonoidal = b.toLaxMonoidal
x✝¹ x✝ : C
⊢ δ F x✝¹ x✝ = δ F x✝¹ x✝

Tactic:
← cancel_epi (μIso F _ _).hom

Goal state after:
case δ
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
eq : a.toLaxMonoidal = b.toLaxMonoidal
x✝¹ x✝ : C
⊢ (μIso F x✝¹ x✝).hom ≫ δ F x✝¹ x✝ = (μIso F x✝¹ x✝).hom ≫ δ F x✝¹ x✝
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 : C ⥤ D
h : F.CoreMonoidal
X✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ (h.μIso X✝ x✝).inv ≫ F.map x✝¹ ▷ F.obj x✝ = F.map (x✝¹ ▷ x✝) ≫ (h.μIso Y✝ x✝).inv

Tactic:
by
    rw [← cancel_epi (h.μIso _ _).hom, Iso.hom_inv_id_assoc,
      ← h.μIso_hom_natural_left_assoc, Iso.hom_inv_id, comp_id]

Goal state after:
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 : C ⥤ D
h : F.CoreMonoidal
x✝ : C
⊢ (ρ_ (F.obj x✝)).inv = F.map (ρ_ x✝).inv ≫ (h.μIso x✝ (𝟙_ C)).inv ≫ F.obj x✝ ◁ h.εIso.inv

Tactic:
by
    rw [← cancel_epi (ρ_ _).hom, Iso.hom_inv_id, h.right_unitality, assoc, assoc,
      Iso.map_hom_inv_id_assoc, Iso.hom_inv_id_assoc, whiskerLeft_hom_inv]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ HasWidePushouts Cᵒᵖ ↔ HasWidePullbacks C

Tactic:
by
  refine ⟨fun h ι ↦ ?_, fun _ ↦ inferInstance⟩
  rw [← hasColimitsOfShape_opposite_opposite_iff]
  exact hasColimitsOfShape_of_equivalence (widePullbackShapeOpEquiv _).symm

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

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
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
⊢ (α_ (F.obj X✝) (F.obj Y✝) (F.obj Z✝)).inv ≫
      (β_ (F.obj X✝ ⊗ F.obj Y✝) (F.obj Z✝)).hom ≫
        (α_ (F.obj Z✝) (F.obj X✝) (F.obj Y✝)).inv ≫ μ F Z✝ X✝ ▷ F.obj Y✝ ≫ μ F (Z✝ ⊗ X✝) Y✝ =
    F.obj X✝ ◁ (β_ (F.obj Y✝) (F.obj Z✝)).hom ≫
      (α_ (F.obj X✝) (F.obj Z✝) (F.obj Y✝)).inv ≫
        (β_ (F.obj X✝) (F.obj Z✝)).hom ▷ F.obj Y✝ ≫ μ F Z✝ X✝ ▷ F.obj Y✝ ≫ μ F (Z✝ ⊗ X✝) Y✝

Tactic:
hexagon_reverse_assoc

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
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : BraidedCategory D
β : (X Y : C) → X ⊗ Y ≅ Y ⊗ X
w : ∀ (X Y : C), μ F X Y ≫ F.map (β X Y).hom = (β_ (F.obj X) (F.obj Y)).hom ≫ μ F Y X
X✝ Y✝ Z✝ : C
⊢ F.obj X✝ ◁ (β_ (F.obj Y✝) (F.obj Z✝)).hom ≫
      (α_ (F.obj X✝) (F.obj Z✝) (F.obj Y✝)).inv ≫
        (β_ (F.obj X✝) (F.obj Z✝)).hom ▷ F.obj Y✝ ≫ μ F Z✝ X✝ ▷ F.obj Y✝ ≫ μ F (Z✝ ⊗ X✝) Y✝ =
    F.obj X✝ ◁ (β_ (F.obj Y✝) (F.obj Z✝)).hom ≫
      (α_ (F.obj X✝) (F.obj Z✝) (F.obj Y✝)).inv ≫
        (β_ (F.obj X✝) (F.obj Z✝)).hom ▷ F.obj Y✝ ≫ μ F Z✝ X✝ ▷ F.obj Y✝ ≫ μ F (Z✝ ⊗ X✝) Y✝
Module: Mathlib.Algebra.Category.ModuleCat.Colimits

Goal state before:
pp: R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
⊢ ∀ (j : J),
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
        colimMap { app := fun j ↦ (F.obj j).smul 1, naturality := ⋯ } =
      colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫ 1

Tactic:
by simp +instances

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

Goal state before:
pp: R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
r s : R
j : J
⊢ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
      colimMap { app := fun j ↦ (F.obj j).smul (r * s), naturality := ⋯ } =
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
      (colimMap { app := fun j ↦ (F.obj j).smul r, naturality := ⋯ } *
        colimMap { app := fun j ↦ (F.obj j).smul s, naturality := ⋯ })

Tactic:
by simp +instances

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

Goal state before:
pp: R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
⊢ ∀ (j : J),
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
        colimMap { app := fun j ↦ (F.obj j).smul 0, naturality := ⋯ } =
      colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫ 0

Tactic:
by simp +instances

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
r : R
x : tsze R M
h : r * x.fst = 1
⊢ (inl r + inr (-(r •> x.snd <• r))) * x = 1

Tactic:
ext <;> dsimp
  · rw [add_zero, h]
  · rw [add_zero, zero_add, smul_neg, op_smul_op_smul, h, op_one, one_smul,
      add_neg_cancel]

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

Goal state before:
pp: R : Type u
A : Type v
ι : Type u_1
κ : ι → Type u_2
Λ : ι → Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
B : Type u_4
inst✝³ : AddCommMonoid B
inst✝² : Module R B
F : Type u_5
inst✝¹ : FunLike F A B
inst✝ : LinearMapClass F R A B
f g h : F
a : A
repr : Repr R a ι
a₁ : (i : ι) → Repr R (repr.left i) (κ i)
a₂ : (i : ι) → Repr R (repr.right i) (Λ i)
⊢ ∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, f (repr.left i) ⊗ₜ[R] (g ((a₂ i).left j) ⊗ₜ[R] h ((a₂ i).right j)) =
    ∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, f ((a₁ i).left j) ⊗ₜ[R] (g ((a₁ i).right j) ⊗ₜ[R] h (repr.right i))

Tactic:
by
  have := sum_tmul_tmul_eq repr a₁ a₂
  apply_fun TensorProduct.map (f : A →ₗ[R] B)
    (TensorProduct.map (g : A →ₗ[R] B) (h : A →ₗ[R] B)) at this
  simp_all only [map_sum, TensorProduct.map_tmul, LinearMap.coe_coe]

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

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
inst✝ : Category.{v₄, u₄} D
G : A ⥤ C
H : B ⥤ D
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : A ⥤ B
R₂ : B ⥤ A
L₃ : C ⥤ D
R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : L₂ ⟶ L₁
β : TwoSquare G L₂ L₃ H
b : B
⊢ ((mateEquiv adj₁ adj₃) (β.whiskerLeft α)).natTrans.app b =
    (((mateEquiv adj₂ adj₃) β).whiskerTop ((conjugateEquiv adj₁ adj₂) α)).natTrans.app b

Tactic:
have vcomp := mateEquiv_vcomp adj₁ adj₂ adj₃ (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) β

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
inst✝ : Category.{v₄, u₄} D
G : A ⥤ C
H : B ⥤ D
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : A ⥤ B
R₂ : B ⥤ A
L₃ : C ⥤ D
R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : L₂ ⟶ L₁
β : TwoSquare G L₂ L₃ H
b : B
vcomp :
  (mateEquiv adj₁ adj₃) ((L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) ≫ₕ β) =
    (mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) ≫ᵥ (mateEquiv adj₂ adj₃) β
⊢ ((mateEquiv adj₁ adj₃) (β.whiskerLeft α)).natTrans.app b =
    (((mateEquiv adj₂ adj₃) β).whiskerTop ((conjugateEquiv adj₁ adj₂) α)).natTrans.app b
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
hx : x.fst ≠ 0
⊢ 1 * x⁻¹⁻¹ = x * x⁻¹ * x⁻¹⁻¹

Tactic:
by rw [TrivSqZeroExt.mul_inv_cancel hx]

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → Coalgebra R (A i)
⊢ lTensor ((i : n) → A i) counit ∘ₗ comul = (TensorProduct.mk R ((i : n) → A i) R).flip 1

Tactic:
ext : 1
    rw [comp_assoc, comul_comp_single, ← comp_assoc, lTensor_comp_map, counit_comp_single,
      ← rTensor_comp_lTensor, comp_assoc, lTensor_counit_comp_comul, rTensor_comp_flip_mk]

Goal state after:
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a ⊓ (a ⊔ b) = a

Tactic:
by
  dsimp only [(· ⊔ ·), (· ⊓ ·)]
  rw [mul_add, mul_add, mul_self, ← mul_assoc, mul_self, add_assoc, add_self, add_zero]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : FunLike F α β
inst✝¹ : CoheytingAlgebra α
x✝ : CoheytingAlgebra β
inst✝ : CoheytingHomClass F α β
f : F
⊢ f (⊤ \ ⊤) = ⊥

Tactic:
← sdiff_self,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : FunLike F α β
inst✝¹ : CoheytingAlgebra α
x✝ : CoheytingAlgebra β
inst✝ : CoheytingHomClass F α β
f : F
⊢ f (⊤ \ ⊤) = ?m.32 \ ?m.32

F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : FunLike F α β
inst✝¹ : CoheytingAlgebra α
x✝ : CoheytingAlgebra β
inst✝ : CoheytingHomClass F α β
f : F
⊢ β
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : FunLike F α β
inst✝¹ : BiheytingAlgebra α
x✝ : BiheytingAlgebra β
inst✝ : BiheytingHomClass F α β
f : F
⊢ f (⊤ \ ⊤) = ⊥

Tactic:
← sdiff_self,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : FunLike F α β
inst✝¹ : BiheytingAlgebra α
x✝ : BiheytingAlgebra β
inst✝ : BiheytingHomClass F α β
f : F
⊢ f (⊤ \ ⊤) = ?m.28 \ ?m.28

F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : FunLike F α β
inst✝¹ : BiheytingAlgebra α
x✝ : BiheytingAlgebra β
inst✝ : BiheytingHomClass F α β
f : F
⊢ β
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : Ring R
I : Ideal R
x : R
hx : x ∈ I.jacobson
y : R
hxy : I ⊔ span {y * x + 1} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {y * x + 1}
hpq : p + q = 1
r : R
hr : r * (y * x + 1) = q
⊢ r * y * x + r - 1 ∈ I

Tactic:
rw [mul_assoc, ← mul_add_one, hr, ← hpq, ← neg_sub, add_sub_cancel_right]
          exact I.neg_mem hpi

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
⊢ (((α_ (M ⊗ N) (M ⊗ N) (M ⊗ N)).hom ≫ (M ⊗ N) ◁ tensorμ M N M N ≫ tensorμ M N (M ⊗ M) (N ⊗ N)) ≫ (M ◁ μ ⊗ₘ N ◁ μ)) ≫
      (μ ⊗ₘ μ) =
    (α_ (M ⊗ N) (M ⊗ N) (M ⊗ N)).hom ≫ (M ⊗ N) ◁ tensorμ M N M N ≫ (M ⊗ N) ◁ (μ ⊗ₘ μ) ≫ tensorμ M N M N ≫ (μ ⊗ₘ μ)

Tactic:
slice_lhs 3 4 => rw [← tensorμ_natural_right]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
M N : C
inst✝¹ : MonObj M
inst✝ : MonObj N
⊢ (α_ (M ⊗ N) (M ⊗ N) (M ⊗ N)).hom ≫ (M ⊗ N) ◁ tensorμ M N M N ≫ ((M ⊗ N) ◁ (μ ⊗ₘ μ) ≫ tensorμ M N M N) ≫ (μ ⊗ₘ μ) =
    (α_ (M ⊗ N) (M ⊗ N) (M ⊗ N)).hom ≫ (M ⊗ N) ◁ tensorμ M N M N ≫ (M ⊗ N) ◁ (μ ⊗ₘ μ) ≫ tensorμ M N M N ≫ (μ ⊗ₘ μ)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: case h₁
C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit t₁
s : PullbackCone (g₁ ≫ g₂) i₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hm₁ : m ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hm₂ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd
⊢ (m ≫ t₁.snd) ≫ t₂.snd = (l₁ ≫ t₁.snd) ≫ t₂.snd

Tactic:
simpa [hl₁', hl₂'] using hm₂

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

Goal state before:
pp: case fac
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ ∀ (s : Fork g g'), H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ (Fork.ofι f ⋯).ι = s.ι

pp: case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ ∀ (s : Fork g g') (m : s.pt ⟶ (Fork.ofι f ⋯).pt),
    m ≫ (Fork.ofι f ⋯).ι = s.ι → m = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯)

Tactic:
· exact fun s => H.isLimit.fac _ WalkingCospan.left

Goal state after:
case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ ∀ (s : Fork g g') (m : s.pt ⟶ (Fork.ofι f ⋯).pt),
    m ≫ (Fork.ofι f ⋯).ι = s.ι → m = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯)
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
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
⊢ ∀ (a : LocalizedModule S A), 0 * a = 0

Tactic:
with_unfolding_all
      rintro ⟨a, s⟩
      exact mk_eq.mpr ⟨1, by simp only [zero_mul, smul_zero]⟩

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
⊢ p ∈ s

Tactic:
by
  have := Classical.decPred (· ∈ s)
  have : ∀ x, IsSupported x s →
        ∃ n : ℤ, lift (fun a => if a ∈ s then (0 : ℤ[X]) else Polynomial.X) x = n := by
    intro x hx
    refine Subring.InClosure.recOn hx ?_ ?_ ?_ ?_
    · use 1
      rw [map_one]
      norm_cast
    · use -1
      rw [map_neg, map_one, Int.cast_neg, Int.cast_one]
    · rintro _ ⟨z, hzs, rfl⟩ _ _
      use 0
      rw [map_mul, lift_of, if_pos hzs, zero_mul]
      norm_cast
    · rintro x y ⟨q, hq⟩ ⟨r, hr⟩
      refine ⟨q + r, ?_⟩
      rw [map_add, hq, hr]
      norm_cast
  specialize this (of p) hps
  rw [lift_of] at this
  split_ifs at this with h
  · exact h
  exfalso
  apply Ne.symm Int.zero_ne_one
  rcases this with ⟨w, H⟩
  rw [← Polynomial.C_eq_intCast] at H
  have : Polynomial.X.coeff 1 = (Polynomial.C ↑w).coeff 1 := by rw [H]; rfl
  rwa [Polynomial.coeff_C, if_neg (one_ne_zero : 1 ≠ 0), Polynomial.coeff_X, if_pos rfl] at this

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
⊢ ∀ (m m' : M) (s s' : ↥S), lift' S g h (mk m s + mk m' s') = lift' S g h (mk m s) + lift' S g h (mk m' s')

Tactic:
intro a a' b b'
      rw [mk_add_mk, LocalizedModule.lift'_mk, LocalizedModule.lift'_mk, LocalizedModule.lift'_mk]
      rw [map_add, Module.End.algebraMap_isUnit_inv_apply_eq_iff, smul_add, ← map_smul,
        ← map_smul, ← map_smul]
      congr 1 <;> symm
      · rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff]
        simp only [Submonoid.coe_mul, LinearMap.map_smul_of_tower]
        rw [mul_smul, Submonoid.smul_def]
      · dsimp
        rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, mul_comm, mul_smul, ← map_smul]
        rfl

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

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
m : M
s : ↥S
⊢ l ((mkLinearMap S M) m) = ↑s • l (mk m s)

Tactic:
LocalizedModule.mkLinearMap_apply,

Goal state after:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
m : M
s : ↥S
⊢ l (mk m 1) = ↑s • l (mk m s)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : AddCommMonoid M''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
p : LocalizedModule S M
m : M
t : ↥S
⊢ LocalizedModule.mk (↑(m, t).2 • m) t = (LocalizedModule.mkLinearMap S M) (m, t).1

Tactic:
LocalizedModule.mkLinearMap_apply,

Goal state after:
R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : AddCommMonoid M''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
p : LocalizedModule S M
m : M
t : ↥S
⊢ LocalizedModule.mk (↑(m, t).2 • m) t = LocalizedModule.mk (m, t).1 1
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x y : LocalizedModule S M
eq1 : (fromLocalizedModule S f) x = (fromLocalizedModule S f) y
⊢ x = y

Tactic:
induction x with | _ a b

Goal state after:
case h
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
y : LocalizedModule S M
a : M
b : ↥S
eq1 : (fromLocalizedModule S f) (LocalizedModule.mk a b) = (fromLocalizedModule S f) y
⊢ LocalizedModule.mk a b = y