mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case e'_3
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
k : 𝕜
h : 0 < addOrderOf ↑k
m : ℕ
hm : m < addOrderOf ↑k
hk : ↑(↑m / ↑(addOrderOf ↑k) * p) = ↑k
⊢ 1 * addOrderOf ↑k = addOrderOf ↑k

Tactic:
·

Goal state after:
case e'_3
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
k : 𝕜
h : 0 < addOrderOf ↑k
m : ℕ
hm : m < addOrderOf ↑k
hk : ↑(↑m / ↑(addOrderOf ↑k) * p) = ↑k
⊢ 1 * addOrderOf ↑k = addOrderOf ↑k
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_1
𝕜 : Type u_1
B : Type u_2
inst✝² : Field 𝕜
p q : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ m.gcd n = 1}
h : (fun m ↦ ⟨↑(↑↑m / ↑n * p), ⋯⟩) m₁ = (fun m ↦ ⟨↑(↑↑m / ↑n * p), ⋯⟩) m₂
⊢ ↑m₁ = ↑m₂

pp: case refine_2
𝕜 : Type u_1
B : Type u_2
inst✝² : Field 𝕜
p q : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
u : ↑{u | addOrderOf u = n}
⊢ ∃ a, (fun m ↦ ⟨↑(↑↑m / ↑n * p), ⋯⟩) a = u

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
B : Type u_2
inst✝² : Field 𝕜
p q : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ m.gcd n = 1}
h : (fun m ↦ ⟨↑(↑↑m / ↑n * p), ⋯⟩) m₁ = (fun m ↦ ⟨↑(↑↑m / ↑n * p), ⋯⟩) m₂
⊢ ↑m₁ = ↑m₂
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_2
𝕜 : Type u_1
B : Type u_2
inst✝² : Field 𝕜
p q : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
u : ↑{u | addOrderOf u = n}
⊢ ∃ a, (fun m ↦ ⟨↑(↑↑m / ↑n * p), ⋯⟩) a = u

Tactic:
·

Goal state after:
case refine_2
𝕜 : Type u_1
B : Type u_2
inst✝² : Field 𝕜
p q : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
u : ↑{u | addOrderOf u = n}
⊢ ∃ a, (fun m ↦ ⟨↑(↑↑m / ↑n * p), ⋯⟩) a = u
Module: Mathlib.Topology.Instances.AddCircle.Defs

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

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

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
⊢ Nat.card { u // addOrderOf u = 0 } = Nat.totient 0
Module: Mathlib.Topology.Instances.AddCircle.Defs

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

pp: case inl.inr
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
h : ¬∃ u, ¬IsOfFinAddOrder u
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0

Tactic:
·

Goal state after:
case inl.inl
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
hu : ¬IsOfFinAddOrder u
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0
Module: Mathlib.Topology.Instances.AddCircle.Defs

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

Tactic:
·

Goal state after:
case inl.inr
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
h : ¬∃ u, ¬IsOfFinAddOrder u
⊢ Nat.card { u // ¬IsOfFinAddOrder u } = 0
Module: Mathlib.Topology.Instances.AddCircle.Defs

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

Tactic:
·

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : n > 0
⊢ Nat.card { u // addOrderOf u = n } = n.totient
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case inl
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
hx : x ∈ Icc a (a + p)
h : x ≠ 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) ⟨x, hx⟩)) =
    Quot.mk (EndpointIdent p a) ⟨x, hx⟩

pp: case inr
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
hx : a + p ∈ 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 + p, hx⟩)) =
    Quot.mk (EndpointIdent p a) ⟨a + p, hx⟩

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
hx : x ∈ Icc a (a + p)
h : x ≠ 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) ⟨x, hx⟩)) =
    Quot.mk (EndpointIdent p a) ⟨x, hx⟩
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case inr
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
hx : a + p ∈ 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 + p, hx⟩)) =
    Quot.mk (EndpointIdent p a) ⟨a + p, hx⟩

Tactic:
·

Goal state after:
case inr
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
hx : a + p ∈ 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 + p, hx⟩)) =
    Quot.mk (EndpointIdent p a) ⟨a + p, hx⟩
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
h : a ≡ x [PMOD p]
⊢ Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩ = Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩

pp: case neg
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
h : ¬a ≡ x [PMOD p]
⊢ Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩ = Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
h : a ≡ x [PMOD p]
⊢ Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩ = Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩
Module: Mathlib.Algebra.Category.ModuleCat.Subobject

Goal state before:
pp: case e'_2
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) =
    (Hom.hom ((underlyingIso (↟N.subtype)).inv ≫ (mk (↟N.subtype)).arrow)).range

pp: case e'_3
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
⊢ N = (Hom.hom (↟N.subtype)).range

Tactic:
·

Goal state after:
case e'_2
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) =
    (Hom.hom ((underlyingIso (↟N.subtype)).inv ≫ (mk (↟N.subtype)).arrow)).range
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
h : ¬a ≡ x [PMOD p]
⊢ Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩ = Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩

Tactic:
·

Goal state after:
case neg
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
h : ¬a ≡ x [PMOD p]
⊢ Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩ = Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩
Module: Mathlib.Algebra.Category.ModuleCat.Subobject

Goal state before:
pp: case e'_3
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
⊢ N = (Hom.hom (↟N.subtype)).range

Tactic:
·

Goal state after:
case e'_3
R : Type u
inst✝ : Ring R
M : ModuleCat R
N : Submodule R ↑M
⊢ N = (Hom.hom (↟N.subtype)).range
Module: Mathlib.Algebra.Category.ModuleCat.Subobject

Goal state before:
pp: case i
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ underlying.obj S ≅ of R ↥((fun S ↦ (Hom.hom S.arrow).range) S)

pp: case w
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ Iso.hom ?i ≫ ↟((fun S ↦ (Hom.hom S.arrow).range) S).subtype = S.arrow

Tactic:
·

Goal state after:
case i
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ underlying.obj S ≅ of R ↥((fun S ↦ (Hom.hom S.arrow).range) S)
Module: Mathlib.Algebra.Category.ModuleCat.Subobject

Goal state before:
pp: 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)

pp: 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)

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

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)
Module: Mathlib.CategoryTheory.Preadditive.CommGrp_

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ MonObj.one ≫ (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X).hom = MonObj.one

pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ MonObj.mul ≫ (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X).hom =
    ((Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X).hom ⊗ₘ
        (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X).hom) ≫
      MonObj.mul

pp: case refine_3
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
⊢ ∀ {X Y : CommGrp C} (f : X ⟶ Y),
    (CommGrp.forget C ⋙ toCommGrp C).map f ≫
        (CommGrp.mkIso (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj Y).X) ⋯ ⋯).hom =
      (CommGrp.mkIso (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj X).X) ⋯ ⋯).hom ≫ (𝟭 (CommGrp C)).map f

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ MonObj.one ≫ (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X).hom = MonObj.one
Module: Mathlib.Algebra.Category.ModuleCat.Subobject

Goal state before:
pp: 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)

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

Goal state after:
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)
Module: Mathlib.Algebra.Category.ModuleCat.Subobject

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

Tactic:
LinearMap.range_codRestrict,

Goal state after:
case i.right
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ Submodule.comap (Hom.hom S.arrow).range.subtype (Hom.hom S.arrow).range = ⊤

case i.right.hf
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.CategoryTheory.Preadditive.CommGrp_

Goal state before:
pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ MonObj.mul ≫ (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X).hom =
    ((Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X).hom ⊗ₘ
        (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X).hom) ≫
      MonObj.mul

pp: case refine_3
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
⊢ ∀ {X Y : CommGrp C} (f : X ⟶ Y),
    (CommGrp.forget C ⋙ toCommGrp C).map f ≫
        (CommGrp.mkIso (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj Y).X) ⋯ ⋯).hom =
      (CommGrp.mkIso (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj X).X) ⋯ ⋯).hom ≫ (𝟭 (CommGrp C)).map f

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ MonObj.mul ≫ (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X).hom =
    ((Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X).hom ⊗ₘ
        (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X).hom) ≫
      MonObj.mul
Module: Mathlib.CategoryTheory.Preadditive.CommGrp_

Goal state before:
pp: case refine_2.h₁
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ lift (𝟙 ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X) 0 ≫
      (fst ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X +
        snd ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X) =
    lift (𝟙 ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X) 0 ≫ MonObj.mul

pp: case h₂
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ lift 0 (𝟙 ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X) ≫
      (fst ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X +
        snd ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X) =
    lift 0 (𝟙 ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X) ≫ MonObj.mul

Tactic:
·

Goal state after:
case refine_2.h₁
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ lift (𝟙 ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X) 0 ≫
      (fst ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X +
        snd ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X) =
    lift (𝟙 ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X) 0 ≫ MonObj.mul
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 (Subtype.val ∘ fun x ↦ ⟨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 (Subtype.val ∘ fun x ↦ ⟨toIcoMod ⋯ a x, ⋯⟩) (Ici x) x

Tactic:
·

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 (Subtype.val ∘ fun x ↦ ⟨toIocMod ⋯ a x, ⋯⟩) (Iic x) x
Module: Mathlib.Algebra.Category.ModuleCat.Subobject

Goal state before:
pp: case w
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ (LinearEquiv.ofBijective (LinearMap.codRestrict (Hom.hom S.arrow).range (Hom.hom S.arrow) ⋯) ⋯).toModuleIso.hom ≫
      ↟((fun S ↦ (Hom.hom S.arrow).range) S).subtype =
    S.arrow

Tactic:
·

Goal state after:
case w
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ (LinearEquiv.ofBijective (LinearMap.codRestrict (Hom.hom S.arrow).range (Hom.hom S.arrow) ⋯) ⋯).toModuleIso.hom ≫
      ↟((fun S ↦ (Hom.hom S.arrow).range) S).subtype =
    S.arrow
Module: Mathlib.CategoryTheory.Preadditive.CommGrp_

Goal state before:
pp: case e'_3.e'_6
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ 0 = 0 ≫ MonObj.one

pp: case refine_2.h₁.convert_7
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ OfNat (((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X ⟶ 𝟙_ C) 0

Tactic:
·

Goal state after:
case e'_3.e'_6
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ 0 = 0 ≫ MonObj.one
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
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 (Subtype.val ∘ fun x ↦ ⟨toIcoMod ⋯ a x, ⋯⟩) (Ici x) x

Tactic:
·

Goal state after:
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 (Subtype.val ∘ fun x ↦ ⟨toIcoMod ⋯ a x, ⋯⟩) (Ici x) x
Module: Mathlib.CategoryTheory.Preadditive.CommGrp_

Goal state before:
pp: case refine_2.h₁.convert_7
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ OfNat (((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X ⟶ 𝟙_ C) 0

Tactic:
·

Goal state after:
case refine_2.h₁.convert_7
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ OfNat (((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X ⟶ 𝟙_ C) 0
Module: Mathlib.CategoryTheory.Preadditive.CommGrp_

Goal state before:
pp: case h₂
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ lift 0 (𝟙 ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X) ≫
      (fst ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X +
        snd ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X) =
    lift 0 (𝟙 ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X) ≫ MonObj.mul

Tactic:
·

Goal state after:
case h₂
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ lift 0 (𝟙 ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X) ≫
      (fst ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X +
        snd ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X) =
    lift 0 (𝟙 ((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X) ≫ MonObj.mul
Module: Mathlib.Algebra.Category.ModuleCat.Subobject

Goal state before:
pp: R : Type u
inst✝ : Ring R
M : ModuleCat R
S T : Submodule R ↑M
h :
  { 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:
convert! LinearMap.range_comp_le_range (ofMkLEMk _ _ h).hom (ofHom T.subtype).hom

Goal state after:
case e'_3
R : Type u
inst✝ : Ring R
M : ModuleCat R
S T : Submodule R ↑M
h :
  { 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 = (Hom.hom (↟T.subtype) ∘ₗ Hom.hom (ofMkLEMk (↟S.subtype) (↟T.subtype) h)).range

case e'_4
R : Type u
inst✝ : Ring R
M : ModuleCat R
S T : Submodule R ↑M
h :
  { 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
⊢ T = (Hom.hom (↟T.subtype)).range
Module: Mathlib.Algebra.Category.ModuleCat.Subobject

Goal state before:
pp: case e'_3
R : Type u
inst✝ : Ring R
M : ModuleCat R
S T : Submodule R ↑M
h :
  { 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 = (Hom.hom (↟T.subtype) ∘ₗ Hom.hom (ofMkLEMk (↟S.subtype) (↟T.subtype) h)).range

pp: case e'_4
R : Type u
inst✝ : Ring R
M : ModuleCat R
S T : Submodule R ↑M
h :
  { 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
⊢ T = (Hom.hom (↟T.subtype)).range

Tactic:
·

Goal state after:
case e'_3
R : Type u
inst✝ : Ring R
M : ModuleCat R
S T : Submodule R ↑M
h :
  { 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 = (Hom.hom (↟T.subtype) ∘ₗ Hom.hom (ofMkLEMk (↟S.subtype) (↟T.subtype) h)).range
Module: Mathlib.CategoryTheory.Preadditive.CommGrp_

Goal state before:
pp: case e'_3.e'_6
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ 0 = 0 ≫ MonObj.one

pp: case h₂.convert_7
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ OfNat (((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X ⟶ 𝟙_ C) 0

Tactic:
·

Goal state after:
case e'_3.e'_6
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ 0 = 0 ≫ MonObj.one
Module: Mathlib.CategoryTheory.Preadditive.CommGrp_

Goal state before:
pp: case h₂.convert_7
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ OfNat (((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X ⟶ 𝟙_ C) 0

Tactic:
·

Goal state after:
case h₂.convert_7
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
x✝ : CommGrp C
⊢ OfNat (((CommGrp.forget C ⋙ toCommGrp C).obj x✝).X ⟶ 𝟙_ C) 0