mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ (∃ u ∈ Ioi a, Ioo a u ⊆ s) ↔ ∃ u ∈ Ioi a, Ioc a u ⊆ s

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ (∃ u ∈ Ioi a, Ioo a u ⊆ s) → ∃ u ∈ Ioi a, Ioc a u ⊆ s

case mpr
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ (∃ u ∈ Ioi a, Ioc a u ⊆ s) → ∃ u ∈ Ioi a, Ioo a u ⊆ s
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝ : Preorder α
t : OrderTopology α
⊢ OrderTopology αᵒᵈ

Tactic:
constructor

Goal state after:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝ : Preorder α
t : OrderTopology α
⊢ OrderDual.instTopologicalSpace = Preorder.topology αᵒᵈ
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ Equivalence EqOnSource

Tactic:
constructor

Goal state after:
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ ∀ (x : PartialEquiv α β), x.EqOnSource x

case symm
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ ∀ {x y : PartialEquiv α β}, x.EqOnSource y → y.EqOnSource x

case trans
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ ∀ {x y z : PartialEquiv α β}, x.EqOnSource y → y.EqOnSource z → x.EqOnSource z
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ e.trans f ≈ e'.trans f'

Tactic:
constructor

Goal state after:
case left
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ (e.trans f).source = (e'.trans f').source

case right
α : Type u_1
β : Type u_2
γ : Type u_3
e e' : PartialEquiv α β
f f' : PartialEquiv β γ
he : e ≈ e'
hf : f ≈ f'
⊢ EqOn (↑(e.trans f)) (↑(e'.trans f')) (e.trans f).source
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set α
⊢ e.restr s ≈ e'.restr s

Tactic:
constructor

Goal state after:
case left
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set α
⊢ (e.restr s).source = (e'.restr s).source

case right
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
he : e ≈ e'
s : Set α
⊢ EqOn (↑(e.restr s)) (↑(e'.restr s)) (e.restr s).source
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: ι : Type u_5
αi : ι → Type u_6
⊢ (PartialEquiv.pi fun i ↦ PartialEquiv.refl (αi i)) = PartialEquiv.refl ((i : ι) → αi i)

Tactic:
ext

Goal state after:
case h
ι : Type u_5
αi : ι → Type u_6
x✝¹ : (i : ι) → αi i
x✝ : ι
⊢ ↑(PartialEquiv.pi fun i ↦ PartialEquiv.refl (αi i)) x✝¹ x✝ = ↑(PartialEquiv.refl ((i : ι) → αi i)) x✝¹ x✝

case hsymm
ι : Type u_5
αi : ι → Type u_6
x✝¹ : (i : ι) → αi i
x✝ : ι
⊢ ↑(PartialEquiv.pi fun i ↦ PartialEquiv.refl (αi i)).symm x✝¹ x✝ = ↑(PartialEquiv.refl ((i : ι) → αi i)).symm x✝¹ x✝

case hs
ι : Type u_5
αi : ι → Type u_6
x✝ : (i : ι) → αi i
⊢ x✝ ∈ (PartialEquiv.pi fun i ↦ PartialEquiv.refl (αi i)).source ↔ x✝ ∈ (PartialEquiv.refl ((i : ι) → αi i)).source
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
γi : ι → Type u_8
ei : (i : ι) → PartialEquiv (αi i) (βi i)
ei' : (i : ι) → PartialEquiv (βi i) (γi i)
⊢ (PartialEquiv.pi ei).trans (PartialEquiv.pi ei') = PartialEquiv.pi fun i ↦ (ei i).trans (ei' i)

Tactic:
ext

Goal state after:
case h
ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
γi : ι → Type u_8
ei : (i : ι) → PartialEquiv (αi i) (βi i)
ei' : (i : ι) → PartialEquiv (βi i) (γi i)
x✝¹ : (i : ι) → αi i
x✝ : ι
⊢ ↑((PartialEquiv.pi ei).trans (PartialEquiv.pi ei')) x✝¹ x✝ = ↑(PartialEquiv.pi fun i ↦ (ei i).trans (ei' i)) x✝¹ x✝

case hsymm
ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
γi : ι → Type u_8
ei : (i : ι) → PartialEquiv (αi i) (βi i)
ei' : (i : ι) → PartialEquiv (βi i) (γi i)
x✝¹ : (i : ι) → γi i
x✝ : ι
⊢ ↑((PartialEquiv.pi ei).trans (PartialEquiv.pi ei')).symm x✝¹ x✝ =
    ↑(PartialEquiv.pi fun i ↦ (ei i).trans (ei' i)).symm x✝¹ x✝

case hs
ι : Type u_5
αi : ι → Type u_6
βi : ι → Type u_7
γi : ι → Type u_8
ei : (i : ι) → PartialEquiv (αi i) (βi i)
ei' : (i : ι) → PartialEquiv (βi i) (γi i)
x✝ : (i : ι) → αi i
⊢ x✝ ∈ ((PartialEquiv.pi ei).trans (PartialEquiv.pi ei')).source ↔
    x✝ ∈ (PartialEquiv.pi fun i ↦ (ei i).trans (ei' i)).source
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
this : ∀ s ∈ k, ∃ a ∈ c, s = Ioi a ∨ s = Iio a
⊢ k = kl ∪ kr

Tactic:
ext

Goal state after:
α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
this : ∀ s ∈ k, ∃ a ∈ c, s = Ioi a ∨ s = Iio a
x✝ : Set α
⊢ x✝ ∈ k ↔ x✝ ∈ kl ∪ kr
Module: Mathlib.Algebra.Category.Grp.Images

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
⊢ factorThruImage f ≫ ι f = f

Tactic:
ext

Goal state after:
G H : AddCommGrpCat
f : G ⟶ H
x✝ : ↑G
⊢ (Hom.hom (factorThruImage f ≫ ι f)) x✝ = (Hom.hom f) x✝
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α✝ : Type u
β : Type v
γ : Type w
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), OrderTopology (α i)
f : (i : ι) → α i
⊢ TendstoIxxClass Icc (𝓝 f) (𝓝 f)

Tactic:
constructor

Goal state after:
α✝ : Type u
β : Type v
γ : Type w
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), OrderTopology (α i)
f : (i : ι) → α i
⊢ Tendsto (fun p ↦ Icc p.1 p.2) (𝓝 f ×ˢ 𝓝 f) (𝓝 f).smallSets
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
B : Type uB
inst✝⁴ : AddCommGroup B
inst✝³ : Module R A
inst✝² : Module R B
C : Type u_2
inst✝¹ : AddCommGroup C
inst✝ : Module R C
f : A →ₗ[R] B
g : B →ₗ[R] C
⊢ dual (g ∘ₗ f) = dual f ∘ₗ dual g

Tactic:
ext

Goal state after:
R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
B : Type uB
inst✝⁴ : AddCommGroup B
inst✝³ : Module R A
inst✝² : Module R B
C : Type u_2
inst✝¹ : AddCommGroup C
inst✝ : Module R C
f : A →ₗ[R] B
g : B →ₗ[R] C
x✝¹ : CharacterModule C
x✝ : A
⊢ ((dual (g ∘ₗ f)) x✝¹) x✝ = ((dual f ∘ₗ dual g) x✝¹) x✝
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
⊢ s ∈ 𝓝 a ↔ ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s

Tactic:
constructor

Goal state after:
case mp
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
⊢ s ∈ 𝓝 a → ∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s

case mpr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hl : ∃ l, l < a
hu : ∃ u, a < u
⊢ (∃ l u, a ∈ Ioo l u ∧ Ioo l u ⊆ s) → s ∈ 𝓝 a
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
c : CharacterModule (A ⊗[R] B)
r : R
a : A
⊢ AddMonoidHom.comp c ↑((mk R A B) (r • a)) = (RingHom.id R) r • AddMonoidHom.comp c ↑((mk R A B) a)

Tactic:
ext

Goal state after:
R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
c : CharacterModule (A ⊗[R] B)
r : R
a : A
x✝ : B
⊢ (AddMonoidHom.comp c ↑((mk R A B) (r • a))) x✝ = ((RingHom.id R) r • AddMonoidHom.comp c ↑((mk R A B) a)) x✝
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
r : R
c : CharacterModule (A ⊗[R] B)
⊢ { toFun := fun x ↦ AddMonoidHom.comp (r • c) ↑((mk R A B) x), map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id R) r • { toFun := fun x ↦ AddMonoidHom.comp c ↑((mk R A B) x), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
ext

Goal state after:
R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
r : R
c : CharacterModule (A ⊗[R] B)
x✝¹ : A
x✝ : B
⊢ ({ toFun := fun x ↦ AddMonoidHom.comp (r • c) ↑((mk R A B) x), map_add' := ⋯, map_smul' := ⋯ } x✝¹) x✝ =
    (((RingHom.id R) r • { toFun := fun x ↦ AddMonoidHom.comp c ↑((mk R A B) x), map_add' := ⋯, map_smul' := ⋯ }) x✝¹)
      x✝
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
H : ∀ (a : Set α), IsOpen[inst✝³] a → {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a}.Countable
⊢ {x | ∃ y, x ⋖ y}.Countable

Tactic:
by
    have : s ⊆ ⋃ a ∈ countableBasis α, { x | x ∈ s ∧ x ∈ a ∧ y x ∉ a } := fun x hx => by
      rcases (isBasis_countableBasis α).exists_mem_of_ne (hy x hx).ne with ⟨a, ab, xa, ya⟩
      exact mem_iUnion₂.2 ⟨a, ab, hx, xa, ya⟩
    refine Set.Countable.mono this ?_
    refine Countable.biUnion (countable_countableBasis α) fun a ha => H _ ?_
    exact isOpen_of_mem_countableBasis ha

Goal state after:
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
hf : Function.Injective ⇑(dual f)
c : CharacterModule (A' ⧸ f.range)
b : A'
⊢ (dual f ∘ₗ dual f.range.mkQ) c = (dual f) 0

Tactic:
← dual_comp,

Goal state after:
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
hf : Function.Injective ⇑(dual f)
c : CharacterModule (A' ⧸ f.range)
b : A'
⊢ (dual (f.range.mkQ ∘ₗ f)) c = (dual f) 0
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : AddCommGroup 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsOrderedAddMonoid 𝕜
hp : 0 < p
x : 𝕜
hx : 0 < x
⊢ (∃ n, n • p = x) ↔ ∃ n, n • p = x

Tactic:
constructor

Goal state after:
case mp
𝕜 : Type u_1
inst✝² : AddCommGroup 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsOrderedAddMonoid 𝕜
hp : 0 < p
x : 𝕜
hx : 0 < x
⊢ (∃ n, n • p = x) → ∃ n, n • p = x

case mpr
𝕜 : Type u_1
inst✝² : AddCommGroup 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsOrderedAddMonoid 𝕜
hp : 0 < p
x : 𝕜
hx : 0 < x
⊢ (∃ n, n • p = x) → ∃ n, n • p = x
Module: Mathlib.Algebra.Category.Grp.LargeColimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
j j' : J
u : j ⟶ j'
⊢ F.map u ≫ ofHom ((AddEquiv.ulift.symm.toAddMonoidHom.comp χ).comp (Quot.ι F j')) =
    ofHom ((AddEquiv.ulift.symm.toAddMonoidHom.comp χ).comp (Quot.ι F j)) ≫
      ((Functor.const J).obj (of (ULift.{w, 0} (AddCircle 1)))).map u

Tactic:
ext

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝¹ : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
j j' : J
u : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ (Hom.hom (F.map u ≫ ofHom ((AddEquiv.ulift.symm.toAddMonoidHom.comp χ).comp (Quot.ι F j')))) x✝ =
    (Hom.hom
        (ofHom ((AddEquiv.ulift.symm.toAddMonoidHom.comp χ).comp (Quot.ι F j)) ≫
          ((Functor.const J).obj (of (ULift.{w, 0} (AddCircle 1)))).map u))
      x✝
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case inl
X : Type u_1
inst✝⁵ : ConditionallyCompleteLinearOrder X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
Y : Type u_2
inst✝² : ConditionallyCompleteLinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
x : X
hf : LeftOrdContinuous f
z : Y
hxz : f x ∈ Ioi z
⊢ ∃ u, IsOpen[inst✝⁴] u ∧ x ∈ u ∧ u ∩ Iic x ⊆ f ⁻¹' Ioi z

Tactic:
obtain hz | ne := em' (f ⁻¹' Iic z).Nonempty
    · exact ⟨univ, isOpen_univ, mem_univ _, fun a ha ↦ not_le.mp fun h ↦ hz ⟨a, h⟩⟩
    have bdd : BddAbove (f ⁻¹' Iic z) := ⟨x, fun a ha ↦ (hf.mono.reflect_lt (ha.trans_lt hxz)).le⟩
    have u_eq : Ioi (sSup (f ⁻¹' Iic z)) = f ⁻¹' Ioi z := by
      refine Set.ext fun a ↦ ⟨fun ha ↦ ?_, fun ha ↦ ?_⟩
      · exact not_le.mp fun h ↦ ha.not_ge (le_csSup bdd h)
      · apply lt_of_le_of_ne
        · exact csSup_le ne fun b hb ↦ (hf.mono.reflect_lt (hb.trans_lt ha)).le
        · have : sSup (f '' f ⁻¹' Iic z) ≤ z := csSup_le (.image _ ne) fun _ ⟨b, hb, heq⟩ ↦ heq ▸ hb
          exact fun h ↦ this.not_gt ((h ▸ ha).trans_eq (hf.map_csSup ne bdd))
    exact ⟨f ⁻¹' Ioi z, u_eq ▸ isOpen_Ioi, hxz, fun _ h ↦ h.1⟩

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

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < n
m : ℕ
⊢ addOrderOf ↑(↑m / ↑n * p) ∣ n

Tactic:
constructor

Goal state after:
case refine_1.h
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < n
m : ℕ
⊢ n = addOrderOf ↑(↑m / ↑n * p) * ?refine_1.w

case refine_1.w
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < n
m : ℕ
⊢ ℕ
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:
ext

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
this : F.Additive
⊢ μ ≫ Multiplicative.toAdd.toIso.hom =
    (Multiplicative.toAdd.toIso.hom ⊗ₘ Multiplicative.toAdd.toIso.hom) ≫
      Functor.LaxMonoidal.μ (forget AddCommGrpCat) (F.obj X) (F.obj X) ≫
        (forget AddCommGrpCat).map
          (SemiCartesianMonoidalCategory.fst (F.obj X) (F.obj X) +
            SemiCartesianMonoidalCategory.snd (F.obj X) (F.obj X))

Tactic:
ext

Goal state after:
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
this : F.Additive
x✝ :
  (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X ⊗
    (commGrpTypeEquivalenceCommGrp.inverse.obj (toCommGrp.obj (F.obj X))).X
⊢ (ConcreteCategory.hom (μ ≫ Multiplicative.toAdd.toIso.hom)).toFun x✝ =
    (ConcreteCategory.hom
          ((Multiplicative.toAdd.toIso.hom ⊗ₘ Multiplicative.toAdd.toIso.hom) ≫
            Functor.LaxMonoidal.μ (forget AddCommGrpCat) (F.obj X) (F.obj X) ≫
              (forget AddCommGrpCat).map
                (SemiCartesianMonoidalCategory.fst (F.obj X) (F.obj X) +
                  SemiCartesianMonoidalCategory.snd (F.obj X) (F.obj X)))).toFun
      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 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt ((equivIccQuot p a).toFun ∘ Quotient.mk') (Iic x) x ∧
    ContinuousWithinAt ((equivIccQuot p a).toFun ∘ Quotient.mk') (Ici x) x

Tactic:
constructor

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 ((equivIccQuot p a).toFun ∘ Quotient.mk') (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 ((equivIccQuot p a).toFun ∘ Quotient.mk') (Ici x) x
Module: Mathlib.Algebra.Category.ModuleCat.Subobject

Goal state before:
pp: case i
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ Function.Bijective ⇑(LinearMap.codRestrict (Hom.hom S.arrow).range (Hom.hom S.arrow) ?m.424)

pp: R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ ∀ (c : ↑(underlying.obj S)), (Hom.hom S.arrow) c ∈ (Hom.hom S.arrow).range

Tactic:
constructor

Goal state after:
case i.left
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ Function.Injective ⇑(LinearMap.codRestrict (Hom.hom S.arrow).range (Hom.hom S.arrow) ?m.424)

case i.right
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ Function.Surjective ⇑(LinearMap.codRestrict (Hom.hom S.arrow).range (Hom.hom S.arrow) ?m.424)

R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ ∀ (c : ↑(underlying.obj S)), (Hom.hom S.arrow) c ∈ (Hom.hom S.arrow).range
Module: Mathlib.Algebra.Category.GrpWithZero

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

Tactic:
ext

Goal state after:
α β : GrpWithZero
e : α.carrier ≃* β.carrier
x✝ : α.carrier
⊢ (ConcreteCategory.hom (ofHom (MonoidWithZeroHom.ofClass e) ≫ ofHom (MonoidWithZeroHom.ofClass e.symm))) x✝ =
    (ConcreteCategory.hom (𝟙 α)) x✝
Module: Mathlib.Algebra.Category.GrpWithZero

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

Tactic:
ext

Goal state after:
α β : GrpWithZero
e : α.carrier ≃* β.carrier
x✝ : β.carrier
⊢ (ConcreteCategory.hom (ofHom (MonoidWithZeroHom.ofClass e.symm) ≫ ofHom (MonoidWithZeroHom.ofClass e))) x✝ =
    (ConcreteCategory.hom (𝟙 β)) x✝
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:
ext

Goal state after:
R : Type u
inst✝ : CommRing R
x✝⁴ x✝³ x✝² : HopfAlgCat R
x✝¹ : x✝³ ⟶ x✝²
x✝ : ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (x✝⁴ ⊗ x✝³)).carrier
⊢ (BialgCat.Hom.toBialgHom ((forget₂ (HopfAlgCat R) (BialgCat R)).map (x✝⁴ ◁ x✝¹))) x✝ =
    (BialgCat.Hom.toBialgHom
        ((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))
      x✝
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:
ext

Goal state after:
R : Type u
inst✝ : CommRing R
X₁✝ X₂✝ : HopfAlgCat R
x✝² : X₁✝ ⟶ X₂✝
x✝¹ : HopfAlgCat R
x✝ : ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (X₁✝ ⊗ x✝¹)).carrier
⊢ (BialgCat.Hom.toBialgHom ((forget₂ (HopfAlgCat R) (BialgCat R)).map (x✝² ▷ x✝¹))) x✝ =
    (BialgCat.Hom.toBialgHom
        ((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))
      x✝
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:
ext

Goal state after:
R : Type u
inst✝ : CommRing R
X₁✝ Y₁✝ X₂✝ Y₂✝ : HopfAlgCat R
x✝² : X₁✝ ⟶ Y₁✝
x✝¹ : X₂✝ ⟶ Y₂✝
x✝ : ((forget₂ (HopfAlgCat R) (BialgCat R)).obj (X₁✝ ⊗ X₂✝)).carrier
⊢ (BialgCat.Hom.toBialgHom ((forget₂ (HopfAlgCat R) (BialgCat R)).map (x✝² ⊗ₘ x✝¹))) x✝ =
    (BialgCat.Hom.toBialgHom
        ((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))
      x✝