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

Goal state before:
pp: case mp
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
k : J
f g : i ⟶ k
h : (hom (F.map f)) x = (hom (F.map g)) y
⊢ (hom (F.map (f ≫ IsFiltered.coeqHom f g))) x = (hom (F.map (f ≫ IsFiltered.coeqHom f g))) y

Tactic:
conv_rhs => rw [IsFiltered.coeq_condition]

Goal state after:
case mp
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
k : J
f g : i ⟶ k
h : (hom (F.map f)) x = (hom (F.map g)) y
⊢ (hom (F.map (f ≫ IsFiltered.coeqHom f g))) x = (hom (F.map (g ≫ IsFiltered.coeqHom f g))) y
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case neg
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j
i : ι
h₁ : ¬(i = k ∨ i ∈ s → i < k)
h₂ : ¬k = i
⊢ update (s.piecewise b a) k (s.piecewise b a k - b k) i = b i

Tactic:
push Not at h₁
      rw [update_of_ne (Ne.symm h₂), s.piecewise_eq_of_mem _ _ (h₁.1.resolve_left <| Ne.symm h₂)]

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
x y z : ↑(R F)
⊢ (x + y) * z = x * z + y * z

Tactic:
by
      refine Quot.induction_on₃ x y z ?_; clear x y z; intro x y z
      obtain ⟨j₁, x⟩ := x; obtain ⟨j₂, y⟩ := y; obtain ⟨j₃, z⟩ := z
      let k := IsFiltered.max₃ j₁ j₂ j₃
      let f := IsFiltered.firstToMax₃ j₁ j₂ j₃
      let g := IsFiltered.secondToMax₃ j₁ j₂ j₃
      let h := IsFiltered.thirdToMax₃ j₁ j₂ j₃
      erw [colimit_add_mk_eq _ ⟨j₁, _⟩ ⟨j₂, _⟩ k f g, colimit_mul_mk_eq _ ⟨k, _⟩ ⟨j₃, _⟩ k (𝟙 k) h,
        colimit_mul_mk_eq _ ⟨j₁, _⟩ ⟨j₃, _⟩ k f h, colimit_mul_mk_eq _ ⟨j₂, _⟩ ⟨j₃, _⟩ k g h,
        colimit_add_mk_eq _ ⟨k, _⟩ ⟨k, _⟩ k (𝟙 k) (𝟙 k)]
      simp only [CategoryTheory.Functor.map_id]
      erw [right_distrib (F.map f x) (F.map g y) (F.map h z)]
      rfl

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
⊢ f ▷ 𝟙_ C = (ρ_ X).hom ≫ f ≫ (ρ_ Y).inv

Tactic:
rw [← assoc, ← rightUnitor_naturality]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
f : X ⟶ Y
⊢ f ▷ 𝟙_ C = (f ▷ 𝟙_ C ≫ (ρ_ Y).hom) ≫ (ρ_ Y).inv
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 : C
j : J
⊢ (rightDistributor f X).inv ≫ biproduct.π f j ▷ X = biproduct.π (fun j ↦ f j ⊗ X) j

Tactic:
classical
  cases nonempty_fintype J
  simp [rightDistributor_inv, Preadditive.sum_comp, ← comp_whiskerRight,
    biproduct.ι_π, dite_whiskerRight, comp_dite]

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.toOplaxMonoidal = b.toOplaxMonoidal
⊢ ε F = ε F

Tactic:
rw [← cancel_mono (εIso _).inv]

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.toOplaxMonoidal = b.toOplaxMonoidal
⊢ ε F ≫ (εIso F).inv = ε F ≫ (εIso F).inv
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
f g h i j : C
α : f ≅ g
η : g ⟶ h
ηs : h ⟶ i
θ : i ⟶ j
ι : h ⟶ j
e_ι : ηs ≫ θ = ι
⊢ (α.hom ≫ η ≫ ηs) ≫ θ = α.hom ≫ η ≫ ι

Tactic:
by
  simp [e_ι]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
c : Cocone F
hc : IsColimit c
s : Cone F.leftOp
m : s.pt ⟶ (coneLeftOpOfCocone c).pt
w : ∀ (j : Jᵒᵖ), m ≫ (coneLeftOpOfCocone c).π.app j = s.π.app j
⊢ m = (hc.desc (coconeOfConeLeftOp s)).unop

Tactic:
refine Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj ?_)
    simpa only [Quiver.Hom.op_unop, IsColimit.fac, coconeOfConeLeftOp_ι_app] using! w (op j)

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 : C} (f : X ⟶ Y) (Z : C), f ▷ Z ≫ (β Y Z).hom = (β X Z).hom ≫ Z ◁ f

Tactic:
by
    intros
    apply F.map_injective
    refine (cancel_epi (μ F ?_ ?_)).1 ?_
    rw [Functor.map_comp, ← μ_natural_left_assoc, w, Functor.map_comp,
      reassoc_of% w, braiding_naturality_left_assoc, μ_natural_right]

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

Goal state before:
pp: case mpr
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
a✝ : (forget C).PreservesMonomorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : monomorphisms C f
this : Mono f
⊢ Function.Injective ⇑(hom ((forget C).map f))

Tactic:
rw [← mono_iff_injective]

Goal state after:
case mpr
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
a✝ : (forget C).PreservesMonomorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : monomorphisms C f
this : Mono f
⊢ Mono ((forget C).map f)
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

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

Tactic:
by
  rw [HasPushout, hasColimit_iff_of_iso (spanOp f g), hasColimit_inverse_equivalence_comp_iff,
    hasColimit_op_iff_hasLimit]

Goal state after:
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₂
| 𝟙 X₁ ≫ f₁ ⊗ₘ (f₂ ⊗ₘ g₁) ≫ (β_ Y₂ V₁).hom ⊗ₘ g₂

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:
← id_comp g₂,

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₁ ≫ f₁ ⊗ₘ (f₂ ⊗ₘ g₁) ≫ (β_ Y₂ V₁).hom ⊗ₘ 𝟙 U₂ ≫ 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.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝¹ : DecidableEq J
A : Type w
inst✝ : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
x : Quot F
⊢ (ConcreteCategory.hom (hc.desc (toCocone F f))) ((desc F c) x) = f x

Tactic:
conv_rhs => rw [← Quot.desc_toCocone_desc F c f hc]

Goal state after:
J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝¹ : DecidableEq J
A : Type w
inst✝ : AddCommGroup A
f : Quot F →+ A
hc : IsColimit c
x : Quot F
⊢ (ConcreteCategory.hom (hc.desc (toCocone F f))) ((desc F c) x) =
    ((Hom.hom (hc.desc (toCocone F f))).comp (desc F c)) x
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare R₁ H G R₂
d : D
⊢ L₂.map (α.app d) ≫ adj₂.counit.app (H.obj d) =
    ((mateEquiv adj₁ adj₂).symm α).app (R₁.obj d) ≫ H.map (adj₁.counit.app d)

Tactic:
by
  conv_lhs => rw [← (mateEquiv adj₁ adj₂).right_inv α]
  exact (mateEquiv_counit adj₁ adj₂ ((mateEquiv adj₁ adj₂).symm α) d)

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
m₁ m₂ : M
⊢ m₁ <• 0 = 0

Tactic:
op_zero,

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
m₁ m₂ : M
⊢ 0 •> m₁ = 0
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₆
X : Type u₇
Y : Type u₈
Z : 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
inst✝² : Category.{v₇, u₇} X
inst✝¹ : Category.{v₈, u₈} Y
inst✝ : Category.{v₉, u₉} Z
G₁ : A ⥤ D
H₁ : B ⥤ E
K₁ : C ⥤ F
G₂ : D ⥤ X
H₂ : E ⥤ Y
K₂ : F ⥤ Z
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : B ⥤ C
R₂ : C ⥤ B
L₃ : D ⥤ E
R₃ : E ⥤ D
L₄ : E ⥤ F
R₄ : F ⥤ E
L₅ : X ⥤ Y
R₅ : Y ⥤ X
L₆ : Y ⥤ Z
R₆ : Z ⥤ Y
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
adj₄ : L₄ ⊣ R₄
adj₅ : L₅ ⊣ R₅
adj₆ : L₆ ⊣ R₆
α : TwoSquare G₁ L₁ L₃ H₁
β : TwoSquare H₁ L₂ L₄ K₁
γ : TwoSquare G₂ L₃ L₅ H₂
δ : TwoSquare H₂ L₄ L₆ K₂
⊢ (mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆)) ((α ≫ᵥ β) ≫ₕ γ ≫ᵥ δ) =
    ((mateEquiv adj₂ adj₄) β ≫ₕ (mateEquiv adj₁ adj₃) α) ≫ᵥ (mateEquiv adj₄ adj₆) δ ≫ₕ (mateEquiv adj₃ adj₅) γ

Tactic:
by
  have vcomp :=
    mateEquiv_vcomp (adj₁.comp adj₂) (adj₃.comp adj₄) (adj₅.comp adj₆) (α ≫ᵥ β) (γ ≫ᵥ δ)
  simp only [mateEquiv_hcomp] at vcomp
  assumption

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

Goal state before:
pp: case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
m : M
⊢ -(0 •> m <• 0) = snd 0

Tactic:
op_zero,

Goal state after:
case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
m : M
⊢ -(0 •> 0 •> m) = snd 0
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
⊢ 0 = TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ comul ∘ₗ inr R A B

Tactic:
comul_comp_inr,

Goal state after:
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
⊢ 0 =
    TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul
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 = TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ comul ∘ₗ inr R A B

Tactic:
comul_comp_inr,

Goal state after:
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 =
    TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul
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
⊢ rTensor (A × B) counit ∘ₗ comul ∘ₗ inr R A B = (TensorProduct.mk R R (A × B)) 1 ∘ₗ inr R A B

Tactic:
comul_comp_inr,

Goal state after:
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
⊢ rTensor (A × B) counit ∘ₗ TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul =
    (TensorProduct.mk R R (A × B)) 1 ∘ₗ inr R A B
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
⊢ lTensor (A × B) counit ∘ₗ comul ∘ₗ inr R A B = (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inr R A B

Tactic:
comul_comp_inr,

Goal state after:
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
⊢ lTensor (A × B) counit ∘ₗ TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul =
    (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inr R A B
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: case e'_2.tmul.tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
F : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B)) ≃ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)) :=
  AlgebraTensorModule.tensorTensorTensorComm R S R S A (A ⊗[S] A) B (B ⊗[R] B) ≪≫ₗ
    AlgebraTensorModule.congr (LinearEquiv.refl S (A ⊗[R] B))
      (AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B)
F' : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B)) →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)) :=
  mapOfCompatibleSMul S S S (A ⊗[R] B) (A ⊗[R] B ⊗[S] (A ⊗[R] B)) ∘ₗ
    map LinearMap.id (mapOfCompatibleSMul S S S (A ⊗[R] B) (A ⊗[R] B)) ∘ₗ ↑F
x₁ x₂ : A
y₁ y₂ : B
⊢ (TensorProduct.assoc S (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B))
      ((AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B) (comul x₁ ⊗ₜ[R] comul y₁) ⊗ₜ[S] (x₂ ⊗ₜ[R] y₂)) =
    F ((TensorProduct.assoc S A A A) (comul x₁ ⊗ₜ[S] x₂) ⊗ₜ[R] (TensorProduct.assoc R B B B) (comul y₁ ⊗ₜ[R] y₂))

Tactic:
hopf_tensor_induction comul (R := S) x₁ with x₁₁ x₁₂

Goal state after:
case e'_2.tmul.tmul.tmul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
F : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B)) ≃ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)) :=
  AlgebraTensorModule.tensorTensorTensorComm R S R S A (A ⊗[S] A) B (B ⊗[R] B) ≪≫ₗ
    AlgebraTensorModule.congr (LinearEquiv.refl S (A ⊗[R] B))
      (AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B)
F' : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B)) →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)) :=
  mapOfCompatibleSMul S S S (A ⊗[R] B) (A ⊗[R] B ⊗[S] (A ⊗[R] B)) ∘ₗ
    map LinearMap.id (mapOfCompatibleSMul S S S (A ⊗[R] B) (A ⊗[R] B)) ∘ₗ ↑F
x₁ x₂ : A
y₁ y₂ : B
x₁₁ x₁₂ : A
⊢ (TensorProduct.assoc S (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B))
      ((AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B) (x₁₁ ⊗ₜ[S] x₁₂ ⊗ₜ[R] comul y₁) ⊗ₜ[S]
        (x₂ ⊗ₜ[R] y₂)) =
    F ((TensorProduct.assoc S A A A) (x₁₁ ⊗ₜ[S] x₁₂ ⊗ₜ[S] x₂) ⊗ₜ[R] (TensorProduct.assoc R B B B) (comul y₁ ⊗ₜ[R] y₂))
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:
← top_sdiff',

Goal state after:
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
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:
← top_sdiff',

Goal state after:
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
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case succ.mp
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
c : R
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ normalize a ::ₘ replicate n (normalize a) ≤ normalizedFactors a + normalizedFactors (a ^ n * c)

Tactic:
normalizedFactors_irreducible ha,

Goal state after:
case succ.mp
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
c : R
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ normalize a ::ₘ replicate n (normalize a) ≤ {normalize a} + normalizedFactors (a ^ n * c)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case inr
R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
p x : R
hnorm : normalize p = p
n : ℕ
hle : p ^ n ∣ x
hlt : ¬p ^ (n + 1) ∣ x
hp : Irreducible p
⊢ count p (normalizedFactors x) = n

Tactic:
exact count_normalizedFactors_eq hp hnorm hle hlt

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
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

Tactic:
ring_nf

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

Goal state before:
pp: case h
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
a b : R
h : (algebraMap S T) ((algebraMap R S) a) = (algebraMap S T) ((algebraMap R S) b)
n : ℕ
hn : (algebraMap R S) (y ^ n * a) = (algebraMap R S) (y ^ n * b)
m : ℕ
hm : x ^ m * (y ^ n * a) = x ^ m * (y ^ n * b)
⊢ y ^ m * x ^ n * (x ^ m * (y ^ n * a)) = y ^ m * x ^ n * (x ^ m * (y ^ n * b))

Tactic:
· rw [hm]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : d ≤ 0
⊢ mk' B 1 (Submonoid.pow x d.natAbs) * selfZPow x B (-d) = 1

Tactic:
selfZPow_of_nonneg,

Goal state after:
case pos
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : d ≤ 0
⊢ mk' B 1 (Submonoid.pow x d.natAbs) * (algebraMap R B) x ^ (-d).natAbs = 1

case pos.hn
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
d : ℤ
hd : d ≤ 0
⊢ 0 ≤ -d
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
⊢ ((λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)) ▷ (M ⊗ N) ≫ tensorμ M N M N ≫ (μ ⊗ₘ μ) = (λ_ (M ⊗ N)).hom

Tactic:
by
  simp only [comp_whiskerRight_assoc]
  slice_lhs 2 3 => rw [tensorμ_natural_left]
  slice_lhs 3 4 => rw [tensorHom_comp_tensorHom, one_mul, one_mul]
  symm
  exact tensor_left_unitality M N

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

Goal state before:
pp: case a
C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
M N O X✝ : C
inst✝⁹ : MonObj M
inst✝⁸ : MonObj N
inst✝⁷ : MonObj O
inst✝⁶ : BraidedCategory C
X Y Z W : C
inst✝⁵ : MonObj X
inst✝⁴ : MonObj Y
inst✝³ : MonObj Z
inst✝² : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst✝¹ : IsMonHom f
inst✝ : IsMonHom g
| (η ⊗ₘ η) ≫ (f ⊗ₘ g)

pp: case a
C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
M N O X✝ : C
inst✝⁹ : MonObj M
inst✝⁸ : MonObj N
inst✝⁷ : MonObj O
inst✝⁶ : BraidedCategory C
X Y Z W : C
inst✝⁵ : MonObj X
inst✝⁴ : MonObj Y
inst✝³ : MonObj Z
inst✝² : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst✝¹ : IsMonHom f
inst✝ : IsMonHom g
| (λ_ (𝟙_ C)).inv

Tactic:
rw [tensorHom_comp_tensorHom, one_hom, one_hom]

Goal state after:
case a
C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
M N O X✝ : C
inst✝⁹ : MonObj M
inst✝⁸ : MonObj N
inst✝⁷ : MonObj O
inst✝⁶ : BraidedCategory C
X Y Z W : C
inst✝⁵ : MonObj X
inst✝⁴ : MonObj Y
inst✝³ : MonObj Z
inst✝² : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst✝¹ : IsMonHom f
inst✝ : IsMonHom g
| η ⊗ₘ η

case a
C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
M N O X✝ : C
inst✝⁹ : MonObj M
inst✝⁸ : MonObj N
inst✝⁷ : MonObj O
inst✝⁶ : BraidedCategory C
X Y Z W : C
inst✝⁵ : MonObj X
inst✝⁴ : MonObj Y
inst✝³ : MonObj Z
inst✝² : MonObj W
f : X ⟶ Y
g : Z ⟶ W
inst✝¹ : IsMonHom f
inst✝ : IsMonHom g
| (λ_ (𝟙_ C)).inv