mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_

Goal state before:
pp: A : CommGrpCat
⊢ (β_ (grpTypeEquivalenceGrp.inverse.obj ((forget₂ CommGrpCat GrpCat).obj A)).X
          (grpTypeEquivalenceGrp.inverse.obj ((forget₂ CommGrpCat GrpCat).obj A)).X).hom ≫
      μ =
    μ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_

Goal state before:
pp: ⊢ ∀ {X Y : CommGrpCat} (f : X ⟶ Y),
    (CommGrpTypeEquivalenceCommGrp.inverse ⋙ CommGrpTypeEquivalenceCommGrp.functor).map f ≫
        (let __src :=
              Equiv.refl ↑((CommGrpTypeEquivalenceCommGrp.inverse ⋙ CommGrpTypeEquivalenceCommGrp.functor).obj Y);
            { toEquiv := __src, map_mul' := ⋯ }).toCommGrpIso.hom =
      (let __src := Equiv.refl ↑((CommGrpTypeEquivalenceCommGrp.inverse ⋙ CommGrpTypeEquivalenceCommGrp.functor).obj X);
            { toEquiv := __src, map_mul' := ⋯ }).toCommGrpIso.hom ≫
        (𝟭 CommGrpCat).map f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
inst✝¹¹ : BraidedCategory C
D : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D
inst✝⁹ : MonoidalCategory D
inst✝⁸ : BraidedCategory D
E : Type u₃
inst✝⁷ : Category.{v₃, u₃} E
inst✝⁶ : MonoidalCategory E
inst✝⁵ : BraidedCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝⁴ : F.LaxBraided
inst✝³ : F'.LaxBraided
inst✝² : G.LaxBraided
M : C
inst✝¹ : MonObj M
inst✝ : IsCommMonObj M
⊢ (β_ (F.obj M) (F.obj M)).hom ≫ μ = μ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
⊢ ↑n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
⊢ n • u = 0 ↔ ∃ m < n, ↑(↑m / ↑n * p) = u

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : BraidedCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : MonoidalCategory D
inst✝⁶ : BraidedCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
inst✝³ : BraidedCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝² : F.LaxBraided
inst✝¹ : F'.LaxBraided
inst✝ : G.LaxBraided
A : CommMon C
⊢ (β_ (F.mapMon.obj A.toMon).X (F.mapMon.obj A.toMon).X).hom ≫ μ = μ

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
F✝ F' : C ⥤ D
G : D ⥤ E
F : LaxBraidedFunctor (Discrete PUnit.{u + 1}) C
x✝ : Discrete PUnit.{u + 1}
⊢ x✝ = (trivial (Discrete PUnit.{u + 1})).toMon.X

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
⊢ addOrderOf u = n ↔ ∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = u

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : BraidedCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
inst✝³ : BraidedCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
inst✝ : BraidedCategory E
F F' : C ⥤ D
G : D ⥤ E
X✝ Y✝ : LaxBraidedFunctor (Discrete PUnit.{u + 1}) C
f : X✝ ⟶ Y✝
⊢ (𝟭 (LaxBraidedFunctor (Discrete PUnit.{u + 1}) C)).map f ≫
      (isoOfComponents (fun x ↦ Y✝.mapIso (eqToIso ⋯)) ⋯ ⋯ ⋯).hom =
    (isoOfComponents (fun x ↦ X✝.mapIso (eqToIso ⋯)) ⋯ ⋯ ⋯).hom ≫ (laxBraidedToCommMon C ⋙ commMonToLaxBraided C).map f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
a : 𝕜
⊢ ¬IsOfFinAddOrder ↑a ↔ ∀ (q : ℚ), ↑q ≠ a / p

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
a : 𝕜
⊢ IsOfFinAddOrder ↑a ↔ ∃ q, ↑q = a / p

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝² : Field 𝕜
p q : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
⊢ Bijective fun m ↦ ⟨↑(↑↑m / ↑n * p), ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.LeftExactFunctor

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
⊢ ∀ (X : C ⥤ₗ Type v), leftExactFunctor C AddCommGrpCat (inverseAux.obj X)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
⊢ Infinite { u // ¬IsOfFinAddOrder u }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.LeftExactFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
F : C ⥤ AddCommGrpCat
inst✝ : PreservesFiniteLimits F
X : C
this✝ : (F ⋙ forget AddCommGrpCat).Braided := Functor.Braided.ofChosenFiniteProducts (F ⋙ forget AddCommGrpCat)
this : F.Monoidal := Functor.Monoidal.ofChosenFiniteProducts F
⊢ η ≫ Multiplicative.toAdd.toIso.hom = η

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
h : ¬∃ u, ¬IsOfFinAddOrder u
⊢ IsEmpty { u // ¬IsOfFinAddOrder u }

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
⊢ Nat.card { u // addOrderOf u = n } = n.totient

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : Quot (EndpointIdent p a)
⊢ ∀ (a_1 b : ↑(Icc a (a + p))), EndpointIdent p a a_1 b → ↑↑a_1 = ↑↑b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.LeftExactFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
F : C ⥤ AddCommGrpCat
inst✝ : PreservesFiniteLimits F
X : C
⊢ commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X)) ≅
    (F ⋙ forget AddCommGrpCat).mapCommGrp.obj (Preadditive.commGrpEquivalence.functor.obj X)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
⊢ ∀ (a_1 : ↑(Icc a (a + p))),
    (fun x ↦ Quot.mk (EndpointIdent p a) (Set.inclusion ⋯ ((equivIco p a) x)))
        ((fun x ↦ x.liftOn (fun x ↦ ↑↑x) ⋯) (Quot.mk (EndpointIdent p a) a_1)) =
      Quot.mk (EndpointIdent p a) a_1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Shrink

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F G : C ⥤ GrpCat
τ : F ⟶ G
inst✝¹ : ∀ (X : C), Small.{w, w'} ↑(F.obj X)
inst✝ : ∀ (X : C), Small.{w, w'} ↑(G.obj X)
X Y : C
f : X ⟶ Y
⊢ (shrinkFunctor.{w, w', v, u} F).map f ≫
      ofHom ((Shrink.mulEquiv.symm.toMonoidHom.comp (Hom.hom (τ.app Y))).comp Shrink.mulEquiv.toMonoidHom) =
    ofHom ((Shrink.mulEquiv.symm.toMonoidHom.comp (Hom.hom (τ.app X))).comp Shrink.mulEquiv.toMonoidHom) ≫
      (shrinkFunctor.{w, w', v, u} G).map f

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
⊢ (underlyingIso (↟N.subtype)).inv = ↟↑(underlyingIso (↟N.subtype)).symm.toLinearEquiv

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
⊢ ⇑(equivIccQuot p a) ∘ Quotient.mk'' = fun x ↦ Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
⊢ (fun S ↦ (Hom.hom S.arrow).range) ((fun N ↦ mk (↟N.subtype)) N) = N

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : CartesianMonoidalCategory C
X : C
⊢ 0 ▷ X ≫ (fst X X + snd X X) = (λ_ X).hom

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case left
𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt (fun x ↦ Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩) (Iic x) x

pp: case right
𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt ((equivIccQuot p a).toFun ∘ Quotient.mk') (Ici x) x

Tactic:
on_goal 2 => erw [equivIccQuot_comp_mk_eq_toIcoMod]

Goal state after:
case left
𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt (fun x ↦ Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩) (Iic x) x

case right
𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt (fun x ↦ Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩) (Ici x) x
Module: Mathlib.CategoryTheory.Preadditive.CommGrp_

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : CartesianMonoidalCategory C
X : C
⊢ X ◁ 0 ≫ (fst X X + snd X X) = (ρ_ X).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : CartesianMonoidalCategory C
X : C
⊢ (fst X X + snd X X) ▷ X ≫ (fst X X + snd X X) = (α_ X X X).hom ≫ X ◁ (fst X X + snd X X) ≫ (fst X X + snd X X)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (β_ X X).hom ≫ MonObj.mul = MonObj.mul

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
⊢ Continuous[QuotientAddGroup.instTopologicalSpace (zmultiples p), instTopologicalSpaceQuot] (equivIccQuot p a).toFun

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ S = (fun N ↦ mk (↟N.subtype)) ((fun S ↦ (Hom.hom S.arrow).range) S)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
hf : f a = f (a + p)
q : 𝕋
⊢ ?m.37

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
hf : f a = f (a + p)
q : 𝕋
⊢ liftIoc p a f q = liftIco p a f q

Tactic:
obtain ⟨x, hx, rfl⟩ := by simpa only [mem_image] using coe_image_Ico_eq p a ▸ mem_univ q

Goal state after:
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
hf : f a = f (a + p)
x : 𝕜
hx : x ∈ Ico a (a + p)
⊢ liftIoc p a f ↑x = liftIco p a f ↑x
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
hf : f a = f (a + p)
x : 𝕜
hx : x ∈ Ico a (a + p)
⊢ ?m.89

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
M : ModuleCat R
S T : Submodule R ↑M
⊢ { toFun := fun N ↦ mk (↟N.subtype), invFun := fun S ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } S ≤
      { toFun := fun N ↦ mk (↟N.subtype), invFun := fun S ↦ (Hom.hom S.arrow).range, left_inv := ⋯, right_inv := ⋯ } T ↔
    S ≤ T

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
x : ↥(Hom.hom f).ker
⊢ (ConcreteCategory.hom (kernelSubobject f).arrow) (toKernelSubobject x) = ↑x

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
L M N : ModuleCat R
f : L ⟶ M
inst✝¹ : HasImage f
g : underlying.obj (imageSubobject f) ⟶ N
inst✝ : HasCokernel g
x y : ↑N
l : ↑L
w : x = y + (ConcreteCategory.hom g) ((ConcreteCategory.hom (factorThruImageSubobject f)) l)
⊢ (ConcreteCategory.hom (cokernel.π g)) x = (ConcreteCategory.hom (cokernel.π g)) y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
hf : f a = f (a + p)
hx : a ∈ Ico a (a + p)
⊢ a + p ∈ Ioc a (a + p)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
hf : f a = f (a + p)
⊢ liftIoc p a f = liftIco p a f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
h : f a = f (a + p)
⊢ ∀ (a_1 b : ↑(Icc a (a + p))),
    EndpointIdent p a a_1 b → (Icc a (a + p)).domRestrict f a_1 = (Icc a (a + p)).domRestrict f b

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
h : f a = f (a + p)
⊢ liftIoc p a f = Quot.lift ((Icc a (a + p)).domRestrict f) ⋯ ∘ ⇑(equivIccQuot p a)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico 0 p
⊢ x ∈ Ico 0 (0 + p)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
⊢ CommGrp.forget C ⋙ toCommGrp C ≅ 𝟭 (CommGrp C)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ioc 0 p
⊢ x ∈ Ioc 0 (0 + p)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝⁶ : AddCommGroup 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f a = f (a + p)
hc : ContinuousOn f (Icc a (a + p))
⊢ Continuous[QuotientAddGroup.instTopologicalSpace (zmultiples p), inst✝] (liftIco p a f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝⁶ : AddCommGroup 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsOrderedAddMonoid 𝕜
p : 𝕜
hp : Fact (0 < p)
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f 0 = f p
hc : ContinuousOn f (Icc 0 p)
⊢ f 0 = f (0 + p)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝⁶ : AddCommGroup 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsOrderedAddMonoid 𝕜
p : 𝕜
hp : Fact (0 < p)
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f 0 = f p
hc : ContinuousOn f (Icc 0 p)
⊢ ContinuousOn f (Icc 0 (0 + p))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝⁶ : AddCommGroup 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f a = f (a + p)
hc : ContinuousOn f (Icc a (a + p))
⊢ Continuous[QuotientAddGroup.instTopologicalSpace (zmultiples p), inst✝] (liftIoc p a f)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : CartesianMonoidalCategory C
inst✝⁹ : BraidedCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : CartesianMonoidalCategory D
inst✝⁶ : BraidedCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : CartesianMonoidalCategory E
inst✝³ : BraidedCategory E
F F' : C ⥤ D
inst✝² : F.Braided
inst✝¹ : F'.Braided
G : D ⥤ E
inst✝ : G.Braided
A : CommGrp C
⊢ (β_ (F.mapGrp.obj A.toGrp).X (F.mapGrp.obj A.toGrp).X).hom ≫ μ = μ

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : CartesianMonoidalCategory C
inst✝⁹ : BraidedCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : CartesianMonoidalCategory D
inst✝⁶ : BraidedCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : CartesianMonoidalCategory E
inst✝³ : BraidedCategory E
F F' : C ⥤ D
inst✝² : F.Braided
inst✝¹ : F'.Braided
G : D ⥤ E
inst✝ : G.Braided
X : CommGrp C
⊢ η ≫ (Iso.refl ((𝟭 C).mapCommGrp.obj X).X).hom = η

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : CartesianMonoidalCategory C
inst✝⁹ : BraidedCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : CartesianMonoidalCategory D
inst✝⁶ : BraidedCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : CartesianMonoidalCategory E
inst✝³ : BraidedCategory E
F F' : C ⥤ D
inst✝² : F.Braided
inst✝¹ : F'.Braided
G : D ⥤ E
inst✝ : G.Braided
X : CommGrp C
⊢ μ ≫ (Iso.refl ((𝟭 C).mapCommGrp.obj X).X).hom =
    ((Iso.refl ((𝟭 C).mapCommGrp.obj X).X).hom ⊗ₘ (Iso.refl ((𝟭 C).mapCommGrp.obj X).X).hom) ≫ μ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.GrpWithZero

Goal state before:
pp: α β : GrpWithZero
e : α.carrier ≃* β.carrier
⊢ ofHom (MonoidWithZeroHom.ofClass e) ≫ ofHom (MonoidWithZeroHom.ofClass e.symm) = 𝟙 α

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.GrpWithZero

Goal state before:
pp: α β : GrpWithZero
e : α.carrier ≃* β.carrier
⊢ ofHom (MonoidWithZeroHom.ofClass e.symm) ≫ ofHom (MonoidWithZeroHom.ofClass e) = 𝟙 β

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Ulift

Goal state before:
pp: J : Type w
x✝ : Category.{w', w} J
F : J ⥤ AddCommGrpCat
c : Cocone F
hc : IsColimit c
⊢ Nonempty (IsColimit (uliftFunctor.mapCocone c))

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Small.{v, u} R
X Y : ModuleCat R
f g : X ⟶ Y
h : ∀ (G : ModuleCat R), ObjectProperty.singleton (of R (Shrink.{v, u} R)) G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.HopfAlgCat.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
V W : HopfAlgCat R
x✝² x✝¹ : V.Hom W
f g : V.carrier →ₐc[R] W.carrier
x✝ : { toBialgHom' := f }.toBialgHom = { toBialgHom' := g }.toBialgHom
⊢ { toBialgHom' := f } = { toBialgHom' := g }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.HopfAlgCat.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y : HopfAlgCat R
f : X ⟶ Y
x✝ : IsIso ((forget (HopfAlgCat R)).map f)
⊢ IsIso f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝³ x✝² x✝¹ : HopfAlgCat R
x✝ : x✝² ⟶ x✝¹
⊢ (forget₂ (HopfAlgCat R) (BialgCat R)).map (x✝³ ◁ x✝) =
    (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝³ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝²)).inv ≫
      (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝³ ◁ (forget₂ (HopfAlgCat R) (BialgCat R)).map x✝ ≫
        (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝³ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝¹)).hom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X₁✝ X₂✝ : HopfAlgCat R
x✝¹ : X₁✝ ⟶ X₂✝
x✝ : HopfAlgCat R
⊢ (forget₂ (HopfAlgCat R) (BialgCat R)).map (x✝¹ ▷ x✝) =
    (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj X₁✝ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝)).inv ≫
      (forget₂ (HopfAlgCat R) (BialgCat R)).map x✝¹ ▷ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝ ≫
        (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj X₂✝ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj x✝)).hom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.HopfAlgCat.Monoidal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X₁✝ Y₁✝ X₂✝ Y₂✝ : HopfAlgCat R
x✝¹ : X₁✝ ⟶ Y₁✝
x✝ : X₂✝ ⟶ Y₂✝
⊢ (forget₂ (HopfAlgCat R) (BialgCat R)).map (x✝¹ ⊗ₘ x✝) =
    (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj X₁✝ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj X₂✝)).inv ≫
      ((forget₂ (HopfAlgCat R) (BialgCat R)).map x✝¹ ⊗ₘ (forget₂ (HopfAlgCat R) (BialgCat R)).map x✝) ≫
        (Iso.refl ((forget₂ (HopfAlgCat R) (BialgCat R)).obj Y₁✝ ⊗ (forget₂ (HopfAlgCat R) (BialgCat R)).obj Y₂✝)).hom

Tactic:
by

Goal state after: