mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case mk.mk.zero
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
inst✝ : IsMulTorsionFree M
a₁✝ : Localization S
a : M × ↥S
a₂✝ : Localization S
b : M × ↥S
c : M
hc : c ∈ S
hn : 0 ≠ 0
hab : c * (↑b.2 ^ 0 * a.1 ^ 0) = c * (↑a.2 ^ 0 * b.1 ^ 0)
⊢ (fun a ↦ a ^ 0) (c * (↑b.2 * a.1)) = (fun a ↦ a ^ 0) (c * (↑a.2 * b.1))

pp: case mk.mk.succ
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
inst✝ : IsMulTorsionFree M
a₁✝ : Localization S
a : M × ↥S
a₂✝ : Localization S
b : M × ↥S
c : M
hc : c ∈ S
n : ℕ
hn : n + 1 ≠ 0
hab : c * (↑b.2 ^ (n + 1) * a.1 ^ (n + 1)) = c * (↑a.2 ^ (n + 1) * b.1 ^ (n + 1))
⊢ (fun a ↦ a ^ (n + 1)) (c * (↑b.2 * a.1)) = (fun a ↦ a ^ (n + 1)) (c * (↑a.2 * b.1))

Tactic:
·

Goal state after:
case mk.mk.zero
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
inst✝ : IsMulTorsionFree M
a₁✝ : Localization S
a : M × ↥S
a₂✝ : Localization S
b : M × ↥S
c : M
hc : c ∈ S
hn : 0 ≠ 0
hab : c * (↑b.2 ^ 0 * a.1 ^ 0) = c * (↑a.2 ^ 0 * b.1 ^ 0)
⊢ (fun a ↦ a ^ 0) (c * (↑b.2 * a.1)) = (fun a ↦ a ^ 0) (c * (↑a.2 * b.1))
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case mk.mk.succ
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
inst✝ : IsMulTorsionFree M
a₁✝ : Localization S
a : M × ↥S
a₂✝ : Localization S
b : M × ↥S
c : M
hc : c ∈ S
n : ℕ
hn : n + 1 ≠ 0
hab : c * (↑b.2 ^ (n + 1) * a.1 ^ (n + 1)) = c * (↑a.2 ^ (n + 1) * b.1 ^ (n + 1))
⊢ (fun a ↦ a ^ (n + 1)) (c * (↑b.2 * a.1)) = (fun a ↦ a ^ (n + 1)) (c * (↑a.2 * b.1))

Tactic:
·

Goal state after:
case mk.mk.succ
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
inst✝ : IsMulTorsionFree M
a₁✝ : Localization S
a : M × ↥S
a₂✝ : Localization S
b : M × ↥S
c : M
hc : c ∈ S
n : ℕ
hn : n + 1 ≠ 0
hab : c * (↑b.2 ^ (n + 1) * a.1 ^ (n + 1)) = c * (↑a.2 ^ (n + 1) * b.1 ^ (n + 1))
⊢ (fun a ↦ a ^ (n + 1)) (c * (↑b.2 * a.1)) = (fun a ↦ a ^ (n + 1)) (c * (↑a.2 * b.1))
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : a = 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b

pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : a = 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : b = 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b

pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : ¬b = 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : b = 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case neg.top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithTop α
hb : ¬b = 0
ha : ¬⊤ = 0
⊢ untopD 0 (⊤ * b) = untopD 0 ⊤ * untopD 0 b

pp: case neg.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithTop α
hb : ¬b = 0
a✝ : α
ha : ¬↑a✝ = 0
⊢ untopD 0 (↑a✝ * b) = untopD 0 ↑a✝ * untopD 0 b

Tactic:
·

Goal state after:
case neg.top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
b : WithTop α
hb : ¬b = 0
ha : ¬⊤ = 0
⊢ untopD 0 (⊤ * b) = untopD 0 ⊤ * untopD 0 b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case neg.coe.top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
ha : ¬↑a✝ = 0
hb : ¬⊤ = 0
⊢ untopD 0 (↑a✝ * ⊤) = untopD 0 ↑a✝ * untopD 0 ⊤

pp: case neg.coe.coe
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝¹ : α
ha : ¬↑a✝¹ = 0
a✝ : α
hb : ¬↑a✝ = 0
⊢ untopD 0 (↑a✝¹ * ↑a✝) = untopD 0 ↑a✝¹ * untopD 0 ↑a✝

Tactic:
·

Goal state after:
case neg.coe.top
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
ha : ¬↑a✝ = 0
hb : ¬⊤ = 0
⊢ untopD 0 (↑a✝ * ⊤) = untopD 0 ↑a✝ * untopD 0 ⊤
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case refine_1
M : Type u_1
G : Type u_2
F : Type u_3
inst✝³ : CommMonoid M
inst✝² : CommGroup G
S : Submonoid G
inst✝¹ : FunLike F G M
inst✝ : MulHomClass F G M
f : F
h : S.IsLocalizationMap ⇑f
g g' : G
eq : f g = f g'
⊢ g = g'

pp: case refine_2
M : Type u_1
G : Type u_2
F : Type u_3
inst✝³ : CommMonoid M
inst✝² : CommGroup G
S : Submonoid G
inst✝¹ : FunLike F G M
inst✝ : MulHomClass F G M
f : F
h : S.IsLocalizationMap ⇑f
m : M
⊢ ∃ a, f a = m

Tactic:
·

Goal state after:
case refine_1
M : Type u_1
G : Type u_2
F : Type u_3
inst✝³ : CommMonoid M
inst✝² : CommGroup G
S : Submonoid G
inst✝¹ : FunLike F G M
inst✝ : MulHomClass F G M
f : F
h : S.IsLocalizationMap ⇑f
g g' : G
eq : f g = f g'
⊢ g = g'
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case refine_2
M : Type u_1
G : Type u_2
F : Type u_3
inst✝³ : CommMonoid M
inst✝² : CommGroup G
S : Submonoid G
inst✝¹ : FunLike F G M
inst✝ : MulHomClass F G M
f : F
h : S.IsLocalizationMap ⇑f
m : M
⊢ ∃ a, f a = m

Tactic:
·

Goal state after:
case refine_2
M : Type u_1
G : Type u_2
F : Type u_3
inst✝³ : CommMonoid M
inst✝² : CommGroup G
S : Submonoid G
inst✝¹ : FunLike F G M
inst✝ : MulHomClass F G M
f : F
h : S.IsLocalizationMap ⇑f
m : M
⊢ ∃ a, f a = m
Module: Mathlib.Algebra.Order.Sub.WithTop

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

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

Tactic:
·

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

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

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

Tactic:
·

Goal state after:
case coe.top
α : Type u_1
β : Type u_2
inst✝⁴ : Add α
inst✝³ : LE α
inst✝² : OrderBot α
inst✝¹ : Sub α
inst✝ : OrderedSub α
z : WithTop α
a✝ : α
⊢ ⊤ - ↑a✝ ≤ z ↔ ⊤ ≤ z + ↑a✝
Module: Mathlib.Algebra.Order.Sub.WithTop

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

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

Tactic:
·

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

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

pp: case inr
S : AddSubmonoid ℕ
hS : S ≠ ⊥
z : ℕ
⊢ ∃ x, ∃ y ∈ S, -↑z = ↑x - ↑y

Tactic:
·

Goal state after:
case inl
S : AddSubmonoid ℕ
hS : S ≠ ⊥
z : ℕ
⊢ ∃ x, ∃ y ∈ S, ↑z = ↑x - ↑y
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: S : AddSubmonoid ℕ
hS : S ≠ ⊥
z : ℕ
⊢ ↑z = ↑z - ↑0

Tactic:
by lia

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

Goal state before:
pp: S : AddSubmonoid ℕ
hS : S ≠ ⊥
z n : ℕ
hnS : n ∈ S
hn0 : n ≠ 0
key : z < n * (z / n + 1)
⊢ -↑z = ↑((z / n + 1) * n - z) - ↑((z / n + 1) * n)

Tactic:
by lia

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inl
α : Type u_1
inst✝⁶ : DecidableEq α
R : Type u_2
S : Type u_3
inst✝⁵ : MulZeroOneClass R
inst✝⁴ : DecidableEq R
inst✝³ : Nontrivial R
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : R →*₀ S
hf : Function.Injective ⇑f
y : WithTop R
this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0
⊢ map (⇑f) (0 * y) = map (⇑f) 0 * map (⇑f) y

pp: case inr
α : Type u_1
inst✝⁶ : DecidableEq α
R : Type u_2
S : Type u_3
inst✝⁵ : MulZeroOneClass R
inst✝⁴ : DecidableEq R
inst✝³ : Nontrivial R
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : R →*₀ S
hf : Function.Injective ⇑f
x y : WithTop R
this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0
hx : x ≠ 0
⊢ map (⇑f) (x * y) = map (⇑f) x * map (⇑f) y

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝⁶ : DecidableEq α
R : Type u_2
S : Type u_3
inst✝⁵ : MulZeroOneClass R
inst✝⁴ : DecidableEq R
inst✝³ : Nontrivial R
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : R →*₀ S
hf : Function.Injective ⇑f
y : WithTop R
this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0
⊢ map (⇑f) (0 * y) = map (⇑f) 0 * map (⇑f) y
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝⁶ : DecidableEq α
R : Type u_2
S : Type u_3
inst✝⁵ : MulZeroOneClass R
inst✝⁴ : DecidableEq R
inst✝³ : Nontrivial R
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : R →*₀ S
hf : Function.Injective ⇑f
x : WithTop R
this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0
hx : x ≠ 0
⊢ map (⇑f) (x * 0) = map (⇑f) x * map (⇑f) 0

pp: case inr.inr
α : Type u_1
inst✝⁶ : DecidableEq α
R : Type u_2
S : Type u_3
inst✝⁵ : MulZeroOneClass R
inst✝⁴ : DecidableEq R
inst✝³ : Nontrivial R
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : R →*₀ S
hf : Function.Injective ⇑f
x y : WithTop R
this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0
hx : x ≠ 0
hy : y ≠ 0
⊢ map (⇑f) (x * y) = map (⇑f) x * map (⇑f) y

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
inst✝⁶ : DecidableEq α
R : Type u_2
S : Type u_3
inst✝⁵ : MulZeroOneClass R
inst✝⁴ : DecidableEq R
inst✝³ : Nontrivial R
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : R →*₀ S
hf : Function.Injective ⇑f
x : WithTop R
this : ∀ (z : WithTop R), map (⇑f) z = 0 ↔ z = 0
hx : x ≠ 0
⊢ map (⇑f) (x * 0) = map (⇑f) x * map (⇑f) 0
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
b c : WithTop α
⊢ 0 * b * c = 0 * (b * c)

pp: case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a b c : WithTop α
ha : a ≠ 0
⊢ a * b * c = a * (b * c)

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
b c : WithTop α
⊢ 0 * b * c = 0 * (b * c)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a c : WithTop α
ha : a ≠ 0
⊢ a * 0 * c = a * (0 * c)

pp: case inr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a b c : WithTop α
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b * c = a * (b * c)

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a c : WithTop α
ha : a ≠ 0
⊢ a * 0 * c = a * (0 * c)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.inr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a b : WithTop α
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b * 0 = a * (b * 0)

pp: case inr.inr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a b c : WithTop α
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
⊢ a * b * c = a * (b * c)

Tactic:
·

Goal state after:
case inr.inr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
a b : WithTop α
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b * 0 = a * (b * 0)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
c : α
hc : c = 0
⊢ ↑c * (a + b) = ↑c * a + ↑c * b

pp: case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
c : α
hc : ¬c = 0
⊢ ↑c * (a + b) = ↑c * a + ↑c * b

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
c : α
hc : c = 0
⊢ ↑c * (a + b) = ↑c * a + ↑c * b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
c : α
hc : c = 0
⊢ (a + b) * ↑c = a * ↑c + b * ↑c

pp: case neg
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
c : α
hc : ¬c = 0
⊢ (a + b) * ↑c = a * ↑c + b * ↑c

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
a b : WithTop α
c : α
hc : c = 0
⊢ (a + b) * ↑c = a * ↑c + b * ↑c
Module: Mathlib.Order.Iterate

Goal state before:
pp: case succ.refine_1
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn : (∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n ≤ y n
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
⊢ ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)

pp: case succ.refine_2
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn : (∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n ≤ y n
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
⊢ ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)

Tactic:
·

Goal state after:
case succ.refine_1
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn : (∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n ≤ y n
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
⊢ ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)
Module: Mathlib.Order.Iterate

Goal state before:
pp: case succ.refine_2
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn : (∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n ≤ y n
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
⊢ ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)

Tactic:
·

Goal state after:
case succ.refine_2
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn : (∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n ≤ y n
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
⊢ ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inl
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
b₂ : WithTop α
this : MulPosStrictMono α
a₁ b₁ : α
hb : ↑b₁ < b₂
ha : ↑a₁ < ⊤
⊢ ↑a₁ * ↑b₁ < ⊤ * b₂

pp: case inr
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₂ b₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : ↑a₁ < a₂
b₁ : α
hb : ↑b₁ < b₂
ha₂ : a₂ ≠ ⊤
⊢ ↑a₁ * ↑b₁ < a₂ * b₂

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
b₂ : WithTop α
this : MulPosStrictMono α
a₁ b₁ : α
hb : ↑b₁ < b₂
ha : ↑a₁ < ⊤
⊢ ↑a₁ * ↑b₁ < ⊤ * b₂
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : ↑a₁ < a₂
b₁ : α
ha₂ : a₂ ≠ ⊤
hb : ↑b₁ < ⊤
⊢ ↑a₁ * ↑b₁ < a₂ * ⊤

pp: case inr.inr
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₂ b₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : ↑a₁ < a₂
b₁ : α
hb : ↑b₁ < b₂
ha₂ : a₂ ≠ ⊤
hb₂ : b₂ ≠ ⊤
⊢ ↑a₁ * ↑b₁ < a₂ * b₂

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a₂ : WithTop α
this : MulPosStrictMono α
a₁ : α
ha : ↑a₁ < a₂
b₁ : α
ha₂ : a₂ ≠ ⊤
hb : ↑b₁ < ⊤
⊢ ↑a₁ * ↑b₁ < a₂ * ⊤
Module: Mathlib.Order.Iterate

Goal state before:
pp: case h₀
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ f^[0] x ≤ g^[0] x

pp: case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ ∀ (k : ℕ), k < n → f^[k + 1] x ≤ f (f^[k] x)

pp: case hy
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ ∀ (k : ℕ), k < n → f (g^[k] x) ≤ g^[k + 1] x

Tactic:
·

Goal state after:
case h₀
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ f^[0] x ≤ g^[0] x
Module: Mathlib.Order.Iterate

Goal state before:
pp: case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ ∀ (k : ℕ), k < n → f^[k + 1] x ≤ f (f^[k] x)

pp: case hy
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ ∀ (k : ℕ), k < n → f (g^[k] x) ≤ g^[k + 1] x

Tactic:
·

Goal state after:
case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ ∀ (k : ℕ), k < n → f^[k + 1] x ≤ f (f^[k] x)
Module: Mathlib.Order.Iterate

Goal state before:
pp: case hy
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ ∀ (k : ℕ), k < n → f (g^[k] x) ≤ g^[k + 1] x

Tactic:
·

Goal state after:
case hy
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ ∀ (k : ℕ), k < n → f (g^[k] x) ≤ g^[k + 1] x
Module: Mathlib.Order.Iterate

Goal state before:
pp: case h₀
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ f^[0] x ≤ g^[0] x

pp: case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ ∀ (k : ℕ), k < n → f^[k + 1] x ≤ f (f^[k] x)

pp: case hy
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ ∀ (k : ℕ), k < n → f (g^[k] x) < g^[k + 1] x

Tactic:
·

Goal state after:
case h₀
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ f^[0] x ≤ g^[0] x
Module: Mathlib.Order.Iterate

Goal state before:
pp: case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ ∀ (k : ℕ), k < n → f^[k + 1] x ≤ f (f^[k] x)

pp: case hy
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ ∀ (k : ℕ), k < n → f (g^[k] x) < g^[k + 1] x

Tactic:
·

Goal state after:
case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ ∀ (k : ℕ), k < n → f^[k + 1] x ≤ f (f^[k] x)
Module: Mathlib.Order.Iterate

Goal state before:
pp: case hy
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ ∀ (k : ℕ), k < n → f (g^[k] x) < g^[k + 1] x

Tactic:
·

Goal state after:
case hy
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ ∀ (k : ℕ), k < n → f (g^[k] x) < g^[k + 1] x
Module: Mathlib.Order.Iterate

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : f x < g x
⊢ f^[n] x < g^[n] x ↔ f x < g x

pp: case inr.inl
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : f x = g x
⊢ f^[n] x < g^[n] x ↔ f x < g x

pp: case inr.inr
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : g x < f x
⊢ f^[n] x < g^[n] x ↔ f x < g x

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : f x < g x
⊢ f^[n] x < g^[n] x ↔ f x < g x
Module: Mathlib.Order.Iterate

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : f x = g x
⊢ f^[n] x < g^[n] x ↔ f x < g x

pp: case inr.inr
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : g x < f x
⊢ f^[n] x < g^[n] x ↔ f x < g x

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : f x = g x
⊢ f^[n] x < g^[n] x ↔ f x < g x
Module: Mathlib.Order.Iterate

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : g x < f x
⊢ f^[n] x < g^[n] x ↔ f x < g x

Tactic:
·

Goal state after:
case inr.inr
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
H : g x < f x
⊢ f^[n] x < g^[n] x ↔ f x < g x
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : a = 0
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b

pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : ¬a = 0
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : a = 0
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b