mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommGroup α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedAddMonoid α
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
h : Monotone ⇑f
a : α
⊢ 0 ≤ a → 0 ≤ f a

Tactic:
rw [← map_zero f]

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommGroup α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedAddMonoid α
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
h : Monotone ⇑f
a : α
⊢ 0 ≤ a → f 0 ≤ f a
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommGroup α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedAddMonoid α
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
h : Monotone ⇑f
a : α
⊢ 0 ≤ a → 0 ≤ f a

Tactic:
rw [← map_zero f]
    apply h

Goal state after:
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommGroup α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedAddMonoid α
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
h : StrictMono ⇑f
a : α
⊢ 0 < a → 0 < f a

Tactic:
rw [← map_zero f]

Goal state after:
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommGroup α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedAddMonoid α
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
h : StrictMono ⇑f
a : α
⊢ 0 < a → f 0 < f a
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommGroup α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedAddMonoid α
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
h : StrictMono ⇑f
a : α
⊢ 0 < a → 0 < f a

Tactic:
rw [← map_zero f]
    apply h

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩
x✝² x✝¹ : X × ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
x✝ : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
s₁vS : v * ↑s₁ ∈ S
hs₂ : u * s₂ = ⟨v * ↑s₁, s₁vS⟩
⊢ ↑u * ↑s₂ ∈ S

Tactic:
norm_cast; rwa [hs₂]

Goal state after:
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: case e'_2.e'_3
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Mul α
inst✝ : Mul β
f : α ≃*o β
a b : β
⊢ f (f.symm a) = a

pp: case e'_2.e'_4
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Mul α
inst✝ : Mul β
f : α ≃*o β
a b : β
⊢ f (f.symm b) = b

Tactic:
<;>

Goal state after:
case e'_2.e'_3
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Mul α
inst✝ : Mul β
f : α ≃*o β
a b : β
⊢ f (f.symm a) = a

case e'_2.e'_4
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Mul α
inst✝ : Mul β
f : α ≃*o β
a b : β
⊢ f (f.symm b) = b
Module: Mathlib.Algebra.Order.Hom.MonoidWithZero

Goal state before:
pp: case zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
b : WithZero G
⊢ (MulEquiv.withZero e.toMulEquiv).toFun 0 ≤ (MulEquiv.withZero e.toMulEquiv).toFun b ↔ 0 ≤ b

pp: case coe
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
b : WithZero G
a✝ : G
⊢ (MulEquiv.withZero e.toMulEquiv).toFun ↑a✝ ≤ (MulEquiv.withZero e.toMulEquiv).toFun b ↔ ↑a✝ ≤ b

Tactic:
<;>

Goal state after:
case zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
b : WithZero G
⊢ (MulEquiv.withZero e.toMulEquiv).toFun 0 ≤ (MulEquiv.withZero e.toMulEquiv).toFun b ↔ 0 ≤ b

case coe
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
b : WithZero G
a✝ : G
⊢ (MulEquiv.withZero e.toMulEquiv).toFun ↑a✝ ≤ (MulEquiv.withZero e.toMulEquiv).toFun b ↔ ↑a✝ ≤ b
Module: Mathlib.Algebra.Order.Hom.MonoidWithZero

Goal state before:
pp: case zero.zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
⊢ (MulEquiv.withZero e.toMulEquiv).toFun 0 ≤ (MulEquiv.withZero e.toMulEquiv).toFun 0 ↔ 0 ≤ 0

pp: case zero.coe
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
a✝ : G
⊢ (MulEquiv.withZero e.toMulEquiv).toFun 0 ≤ (MulEquiv.withZero e.toMulEquiv).toFun ↑a✝ ↔ 0 ≤ ↑a✝

pp: case coe.zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
a✝ : G
⊢ (MulEquiv.withZero e.toMulEquiv).toFun ↑a✝ ≤ (MulEquiv.withZero e.toMulEquiv).toFun 0 ↔ ↑a✝ ≤ 0

pp: case coe.coe
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
a✝¹ a✝ : G
⊢ (MulEquiv.withZero e.toMulEquiv).toFun ↑a✝¹ ≤ (MulEquiv.withZero e.toMulEquiv).toFun ↑a✝ ↔ ↑a✝¹ ≤ ↑a✝

Tactic:
<;>

Goal state after:
case zero.zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
⊢ (MulEquiv.withZero e.toMulEquiv).toFun 0 ≤ (MulEquiv.withZero e.toMulEquiv).toFun 0 ↔ 0 ≤ 0

case zero.coe
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
a✝ : G
⊢ (MulEquiv.withZero e.toMulEquiv).toFun 0 ≤ (MulEquiv.withZero e.toMulEquiv).toFun ↑a✝ ↔ 0 ≤ ↑a✝

case coe.zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
a✝ : G
⊢ (MulEquiv.withZero e.toMulEquiv).toFun ↑a✝ ≤ (MulEquiv.withZero e.toMulEquiv).toFun 0 ↔ ↑a✝ ≤ 0

case coe.coe
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
a✝¹ a✝ : G
⊢ (MulEquiv.withZero e.toMulEquiv).toFun ↑a✝¹ ≤ (MulEquiv.withZero e.toMulEquiv).toFun ↑a✝ ↔ ↑a✝¹ ≤ ↑a✝
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case empty
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
ι : Type u_4
f : ι → M
s : ι → ↥S
⊢ ∏ i ∈ ∅, mk (f i) (s i) = mk (∏ i ∈ ∅, f i) (∏ i ∈ ∅, s i)

pp: case insert
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
ι : Type u_4
f : ι → M
s : ι → ↥S
a✝² : ι
s✝ : Finset ι
a✝¹ : a✝² ∉ s✝
a✝ : ∏ i ∈ s✝, mk (f i) (s i) = mk (∏ i ∈ s✝, f i) (∏ i ∈ s✝, s i)
⊢ ∏ i ∈ insert a✝² s✝, mk (f i) (s i) = mk (∏ i ∈ insert a✝² s✝, f i) (∏ i ∈ insert a✝² s✝, s i)

Tactic:
<;>

Goal state after:
case empty
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
ι : Type u_4
f : ι → M
s : ι → ↥S
⊢ ∏ i ∈ ∅, mk (f i) (s i) = mk (∏ i ∈ ∅, f i) (∏ i ∈ ∅, s i)

case insert
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
ι : Type u_4
f : ι → M
s : ι → ↥S
a✝² : ι
s✝ : Finset ι
a✝¹ : a✝² ∉ s✝
a✝ : ∏ i ∈ s✝, mk (f i) (s i) = mk (∏ i ∈ s✝, f i) (∏ i ∈ s✝, s i)
⊢ ∏ i ∈ insert a✝² s✝, mk (f i) (s i) = mk (∏ i ∈ insert a✝² s✝, f i) (∏ i ∈ insert a✝² s✝, s i)
Module: Mathlib.Algebra.Order.Hom.MonoidWithZero

Goal state before:
pp: case zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
x✝ : WithZero G ≃*o WithZero H
⊢ ((fun e ↦ { toMulEquiv := MulEquiv.withZero e.toMulEquiv, map_le_map_iff' := ⋯ })
        ((fun e ↦ { toMulEquiv := MulEquiv.withZero.symm ↑e, map_le_map_iff' := ⋯ }) x✝))
      0 =
    x✝ 0

pp: case coe
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
x✝ : WithZero G ≃*o WithZero H
a✝ : G
⊢ ((fun e ↦ { toMulEquiv := MulEquiv.withZero e.toMulEquiv, map_le_map_iff' := ⋯ })
        ((fun e ↦ { toMulEquiv := MulEquiv.withZero.symm ↑e, map_le_map_iff' := ⋯ }) x✝))
      ↑a✝ =
    x✝ ↑a✝

Tactic:
<;>

Goal state after:
case zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
x✝ : WithZero G ≃*o WithZero H
⊢ ((fun e ↦ { toMulEquiv := MulEquiv.withZero e.toMulEquiv, map_le_map_iff' := ⋯ })
        ((fun e ↦ { toMulEquiv := MulEquiv.withZero.symm ↑e, map_le_map_iff' := ⋯ }) x✝))
      0 =
    x✝ 0

case coe
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
x✝ : WithZero G ≃*o WithZero H
a✝ : G
⊢ ((fun e ↦ { toMulEquiv := MulEquiv.withZero e.toMulEquiv, map_le_map_iff' := ⋯ })
        ((fun e ↦ { toMulEquiv := MulEquiv.withZero.symm ↑e, map_le_map_iff' := ⋯ }) x✝))
      ↑a✝ =
    x✝ ↑a✝
Module: Mathlib.Algebra.Order.Hom.MonoidWithZero

Goal state before:
pp: case zero
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : DecidablePred fun a ↦ a = 0
b : WithZero αˣ
⊢ WithZero.withZeroUnitsEquiv.toFun 0 ≤ WithZero.withZeroUnitsEquiv.toFun b ↔ 0 ≤ b

pp: case coe
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : DecidablePred fun a ↦ a = 0
b : WithZero αˣ
a✝ : αˣ
⊢ WithZero.withZeroUnitsEquiv.toFun ↑a✝ ≤ WithZero.withZeroUnitsEquiv.toFun b ↔ ↑a✝ ≤ b

Tactic:
<;>

Goal state after:
case zero
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : DecidablePred fun a ↦ a = 0
b : WithZero αˣ
⊢ WithZero.withZeroUnitsEquiv.toFun 0 ≤ WithZero.withZeroUnitsEquiv.toFun b ↔ 0 ≤ b

case coe
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : DecidablePred fun a ↦ a = 0
b : WithZero αˣ
a✝ : αˣ
⊢ WithZero.withZeroUnitsEquiv.toFun ↑a✝ ≤ WithZero.withZeroUnitsEquiv.toFun b ↔ ↑a✝ ≤ b
Module: Mathlib.Algebra.Order.Hom.MonoidWithZero

Goal state before:
pp: case zero.zero
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : DecidablePred fun a ↦ a = 0
⊢ WithZero.withZeroUnitsEquiv.toFun 0 ≤ WithZero.withZeroUnitsEquiv.toFun 0 ↔ 0 ≤ 0

pp: case zero.coe
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : DecidablePred fun a ↦ a = 0
a✝ : αˣ
⊢ WithZero.withZeroUnitsEquiv.toFun 0 ≤ WithZero.withZeroUnitsEquiv.toFun ↑a✝ ↔ 0 ≤ ↑a✝

pp: case coe.zero
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : DecidablePred fun a ↦ a = 0
a✝ : αˣ
⊢ WithZero.withZeroUnitsEquiv.toFun ↑a✝ ≤ WithZero.withZeroUnitsEquiv.toFun 0 ↔ ↑a✝ ≤ 0

pp: case coe.coe
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : DecidablePred fun a ↦ a = 0
a✝¹ a✝ : αˣ
⊢ WithZero.withZeroUnitsEquiv.toFun ↑a✝¹ ≤ WithZero.withZeroUnitsEquiv.toFun ↑a✝ ↔ ↑a✝¹ ≤ ↑a✝

Tactic:
<;>

Goal state after:
case zero.zero
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : DecidablePred fun a ↦ a = 0
⊢ WithZero.withZeroUnitsEquiv.toFun 0 ≤ WithZero.withZeroUnitsEquiv.toFun 0 ↔ 0 ≤ 0

case zero.coe
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : DecidablePred fun a ↦ a = 0
a✝ : αˣ
⊢ WithZero.withZeroUnitsEquiv.toFun 0 ≤ WithZero.withZeroUnitsEquiv.toFun ↑a✝ ↔ 0 ≤ ↑a✝

case coe.zero
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : DecidablePred fun a ↦ a = 0
a✝ : αˣ
⊢ WithZero.withZeroUnitsEquiv.toFun ↑a✝ ≤ WithZero.withZeroUnitsEquiv.toFun 0 ↔ ↑a✝ ≤ 0

case coe.coe
F : Type u_1
α✝ : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
α : Type u_6
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : DecidablePred fun a ↦ a = 0
a✝¹ a✝ : αˣ
⊢ WithZero.withZeroUnitsEquiv.toFun ↑a✝¹ ≤ WithZero.withZeroUnitsEquiv.toFun ↑a✝ ↔ ↑a✝¹ ≤ ↑a✝
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case refine_2
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f ↑a.2 = f a.1
b : M × ↥S
hb : w * f ↑b.2 = f b.1
⊢ w * f ↑(a.2 * b.2) = f (↑a.2 * b.1)

Tactic:
simp_rw [mul_def, map_mul, ← hb]
    exact mul_left_comm w _ _

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), l ↑w ∈ U
z : N
⊢ ((k.map hl j).comp (f.map hy k)) z = (f.map ⋯ j) z

Tactic:
change j _ * _ = j (l _) * _

Goal state after:
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), l ↑w ∈ U
z : N
⊢ j (l (k.sec ((f.map hy k) z)).1) *
      ↑((IsUnit.liftRight ((j.toMonoidHom.comp l).domRestrict T) ⋯) (k.sec ((f.map hy k) z)).2)⁻¹ =
    j (l (g (f.sec z).1)) * ↑((IsUnit.liftRight ((j.toMonoidHom.comp (l.comp g)).domRestrict S) ⋯) (f.sec z).2)⁻¹
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithTop α
⊢ ⊤ * b = if ⊤ = 0 ∨ b = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ⊤ b

pp: case coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithTop α
a✝ : α
⊢ ↑a✝ * b = if ↑a✝ = 0 ∨ b = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) (↑a✝) b

Tactic:
<;>

Goal state after:
case top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithTop α
⊢ ⊤ * b = if ⊤ = 0 ∨ b = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ⊤ b

case coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithTop α
a✝ : α
⊢ ↑a✝ * b = if ↑a✝ = 0 ∨ b = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) (↑a✝) b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case top.top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
⊢ ⊤ * ⊤ = if ⊤ = 0 ∨ ⊤ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ⊤ ⊤

pp: case top.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
⊢ ⊤ * ↑a✝ = if ⊤ = 0 ∨ ↑a✝ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ⊤ ↑a✝

pp: case coe.top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
⊢ ↑a✝ * ⊤ = if ↑a✝ = 0 ∨ ⊤ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ↑a✝ ⊤

pp: case coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ a✝ : α
⊢ ↑a✝¹ * ↑a✝ = if ↑a✝¹ = 0 ∨ ↑a✝ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ↑a✝¹ ↑a✝

Tactic:
<;>

Goal state after:
case top.top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
⊢ ⊤ * ⊤ = if ⊤ = 0 ∨ ⊤ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ⊤ ⊤

case top.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
⊢ ⊤ * ↑a✝ = if ⊤ = 0 ∨ ↑a✝ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ⊤ ↑a✝

case coe.top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
⊢ ↑a✝ * ⊤ = if ↑a✝ = 0 ∨ ⊤ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ↑a✝ ⊤

case coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ a✝ : α
⊢ ↑a✝¹ * ↑a✝ = if ↑a✝¹ = 0 ∨ ↑a✝ = 0 then 0 else map₂ (fun x1 x2 ↦ x1 * x2) ↑a✝¹ ↑a✝
Module: Mathlib.Algebra.Order.Sub.WithTop

Goal state before:
pp: case top
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
⊢ ⊤ - ⊤ = ↑⊥

pp: case coe
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
a✝ : α
⊢ ↑a✝ - ⊤ = ↑⊥

Tactic:
<;>

Goal state after:
case top
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
⊢ ⊤ - ⊤ = ↑⊥

case coe
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
a✝ : α
⊢ ↑a✝ - ⊤ = ↑⊥
Module: Mathlib.Algebra.Order.Sub.WithTop

Goal state before:
pp: case top
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
b : WithTop α
⊢ ⊤ - b = ⊤ ↔ ⊤ = ⊤ ∧ b ≠ ⊤

pp: case coe
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
b : WithTop α
a✝ : α
⊢ ↑a✝ - b = ⊤ ↔ ↑a✝ = ⊤ ∧ b ≠ ⊤

Tactic:
<;>

Goal state after:
case top
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
b : WithTop α
⊢ ⊤ - b = ⊤ ↔ ⊤ = ⊤ ∧ b ≠ ⊤

case coe
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
b : WithTop α
a✝ : α
⊢ ↑a✝ - b = ⊤ ↔ ↑a✝ = ⊤ ∧ b ≠ ⊤
Module: Mathlib.Algebra.Order.Sub.WithTop

Goal state before:
pp: case top.top
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
⊢ ⊤ - ⊤ = ⊤ ↔ ⊤ = ⊤ ∧ ⊤ ≠ ⊤

pp: case top.coe
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
a✝ : α
⊢ ⊤ - ↑a✝ = ⊤ ↔ ⊤ = ⊤ ∧ ↑a✝ ≠ ⊤

pp: case coe.top
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
a✝ : α
⊢ ↑a✝ - ⊤ = ⊤ ↔ ↑a✝ = ⊤ ∧ ⊤ ≠ ⊤

pp: case coe.coe
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
a✝¹ a✝ : α
⊢ ↑a✝¹ - ↑a✝ = ⊤ ↔ ↑a✝¹ = ⊤ ∧ ↑a✝ ≠ ⊤

Tactic:
<;>

Goal state after:
case top.top
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
⊢ ⊤ - ⊤ = ⊤ ↔ ⊤ = ⊤ ∧ ⊤ ≠ ⊤

case top.coe
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
a✝ : α
⊢ ⊤ - ↑a✝ = ⊤ ↔ ⊤ = ⊤ ∧ ↑a✝ ≠ ⊤

case coe.top
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
a✝ : α
⊢ ↑a✝ - ⊤ = ⊤ ↔ ↑a✝ = ⊤ ∧ ⊤ ≠ ⊤

case coe.coe
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
a✝¹ a✝ : α
⊢ ↑a✝¹ - ↑a✝ = ⊤ ↔ ↑a✝¹ = ⊤ ∧ ↑a✝ ≠ ⊤
Module: Mathlib.Algebra.Order.Sub.WithTop

Goal state before:
pp: case top.top
α : Type u_1
β : Type u_2
inst✝⁴ : Add α
inst✝³ : LE α
inst✝² : OrderBot α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x : WithTop α
⊢ x - ⊤ ≤ ⊤ ↔ x ≤ ⊤ + ⊤

pp: case top.coe
α : Type u_1
β : Type u_2
inst✝⁴ : Add α
inst✝³ : LE α
inst✝² : OrderBot α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x : WithTop α
a✝ : α
⊢ x - ⊤ ≤ ↑a✝ ↔ x ≤ ↑a✝ + ⊤

Tactic:
<;>

Goal state after:
case top.top
α : Type u_1
β : Type u_2
inst✝⁴ : Add α
inst✝³ : LE α
inst✝² : OrderBot α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x : WithTop α
⊢ x - ⊤ ≤ ⊤ ↔ x ≤ ⊤ + ⊤

case top.coe
α : Type u_1
β : Type u_2
inst✝⁴ : Add α
inst✝³ : LE α
inst✝² : OrderBot α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x : WithTop α
a✝ : α
⊢ x - ⊤ ≤ ↑a✝ ↔ x ≤ ↑a✝ + ⊤
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: S : AddSubmonoid ℕ
hS : S ≠ ⊥
z : ℤ
⊢ ∃ x, ∃ y ∈ S, z = ↑x - ↑y

Tactic:
obtain ⟨z, rfl | rfl⟩ := z.eq_nat_or_neg

Goal state after:
case inl
S : AddSubmonoid ℕ
hS : S ≠ ⊥
z : ℕ
⊢ ∃ x, ∃ y ∈ S, ↑z = ↑x - ↑y

case inr
S : AddSubmonoid ℕ
hS : S ≠ ⊥
z : ℕ
⊢ ∃ x, ∃ y ∈ S, -↑z = ↑x - ↑y
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
⊢ (match ⊤, 0 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    1

pp: case coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
a✝ : α
⊢ (match ↑a✝, 0 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    1

Tactic:
<;>

Goal state after:
case top
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
⊢ (match ⊤, 0 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    1

case coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
a✝ : α
⊢ (match ↑a✝, 0 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    1
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case zero
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
a : WithTop α
⊢ (match a, 0 + 1 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    (match a, 0 with
      | Option.some a, n => ↑(a ^ n)
      | none, 0 => 1
      | none, _n.succ => ⊤) *
      a

pp: case succ
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
a : WithTop α
n✝ : ℕ
⊢ (match a, n✝ + 1 + 1 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    (match a, n✝ + 1 with
      | Option.some a, n => ↑(a ^ n)
      | none, 0 => 1
      | none, _n.succ => ⊤) *
      a

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
a : WithTop α
⊢ (match a, 0 + 1 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    (match a, 0 with
      | Option.some a, n => ↑(a ^ n)
      | none, 0 => 1
      | none, _n.succ => ⊤) *
      a

case succ
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
a : WithTop α
n✝ : ℕ
⊢ (match a, n✝ + 1 + 1 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    (match a, n✝ + 1 with
      | Option.some a, n => ↑(a ^ n)
      | none, 0 => 1
      | none, _n.succ => ⊤) *
      a