mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ 0 < a * b⁻¹

Tactic:
]

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ 0 < a * b⁻¹
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a * b⁻¹

Tactic:
]

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a * b⁻¹
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ c * a ≤ b ↔ c * a ≤ b

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
hab : a ≤ b
d : R
hd : 0 ≤ d
hcd : c ≤ c + d
⊢ a * c + b * c + a * d ≤ a * c + b * c + b * d

Tactic:
]

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
hab : a ≤ b
d : R
hd : 0 ≤ d
hcd : c ≤ c + d
⊢ a * c + b * c + a * d ≤ a * c + b * c + b * d
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b ≤ c * a ↔ b ≤ c * a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c d : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
hba : b ≤ a
hdc : d ≤ c
⊢ b * c + a * d ≤ b * d + a * c

Tactic:
]

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c d : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
hba : b ≤ a
hdc : d ≤ c
⊢ b * c + a * d ≤ b * d + a * c
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
⊢ a ≤ b ↔ a ≤ b

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
⊢ b ≤ a ↔ b ≤ a

Tactic:
]

Goal state after:
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α₁ : Sort u
α₂ : Sort v
α₃ : Sort x
γ : Sort w
inst✝ : Inhabited γ
e₁₂ : α₁ ↪ α₂
e₂₃ : α₂ ↪ α₃
f : α₁ → γ
a : α₃
⊢ extend (⇑e₂₃) (extend (⇑e₁₂) f fun a ↦ default) (fun a ↦ default) a =
    extend (⇑e₂₃) (extend (⇑e₁₂) f fun x ↦ default) (fun a ↦ default) a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
⊢ a⁻¹ ≤ b ↔ a⁻¹ ≤ b

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hb : 0 ≤ b
hc✝ : 0 ≤ c
h : c * a ≤ b
hc : 0 < c
⊢ c * a ≤ b

Tactic:
]

Goal state after:
case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hb : 0 ≤ b
hc✝ : 0 ≤ c
h : c * a ≤ b
hc : 0 < c
⊢ c * a ≤ b
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : AddLeftReflectLT R
inst✝² : ExistsAddOfLE R
inst✝¹ : MulPosStrictMono R
inst✝ : AddLeftStrictMono R
hab : a < b
d : R
hd : 0 < d
hcd : c < c + d
⊢ a * c + b * c + a * d < a * c + b * c + b * d

Tactic:
]

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c : R
inst✝³ : AddLeftReflectLT R
inst✝² : ExistsAddOfLE R
inst✝¹ : MulPosStrictMono R
inst✝ : AddLeftStrictMono R
hab : a < b
d : R
hd : 0 < d
hcd : c < c + d
⊢ a * c + b * c + a * d < a * c + b * c + b * d
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c d : R
inst✝³ : AddLeftReflectLT R
inst✝² : ExistsAddOfLE R
inst✝¹ : MulPosStrictMono R
inst✝ : AddLeftStrictMono R
hba : b < a
hdc : d < c
⊢ b * c + a * d < b * d + a * c

Tactic:
]

Goal state after:
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
a b c d : R
inst✝³ : AddLeftReflectLT R
inst✝² : ExistsAddOfLE R
inst✝¹ : MulPosStrictMono R
inst✝ : AddLeftStrictMono R
hba : b < a
hdc : d < c
⊢ b * c + a * d < b * d + a * c
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hb✝ : 0 ≤ b
hc : 0 ≤ c
h : a ≤ b * c
hb : 0 < b
⊢ a ≤ b * c

Tactic:
]

Goal state after:
case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hb✝ : 0 ≤ b
hc : 0 ≤ c
h : a ≤ b * c
hb : 0 < b
⊢ a ≤ b * c
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ c * a < b ↔ c * a < b

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b < c * a ↔ b < c * a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
⊢ a⁻¹ < b ↔ a⁻¹ < b

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
⊢ a < b ↔ a < b

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
⊢ b < a ↔ b < a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a : G₀
ha : 0 < a
⊢ 1 < a⁻¹ ↔ a < 1

Tactic:
simpa using one_lt_inv_mul₀ ha (b := 1)

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : ZeroLEOneClass G₀
h : a ≤ b
hb : 0 ≤ b
⊢ a ≤ b

Tactic:
]

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : ZeroLEOneClass G₀
h : a ≤ b
hb : 0 ≤ b
⊢ a ≤ b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ n

Tactic:
]

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ n
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ (n + 1)

Tactic:
]

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 0 ≤ a
n : ℕ
⊢ 0 ≤ a ^ (n + 1)
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
a b c : R
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ 0 ≤ b * c ∨ 0 ≤ c * a

Tactic:
]

Goal state after:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
a b c : R
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ 0 ≤ b * c ∨ 0 ≤ c * a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 0 < a
n : ℕ
⊢ 0 < a ^ n

Tactic:
]

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 0 < a
n : ℕ
⊢ 0 < a ^ n
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 0 < a
n : ℕ
⊢ 0 < a ^ (n + 1)

Tactic:
]

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 0 < a
n : ℕ
⊢ 0 < a ^ (n + 1)
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
a b c : R
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c * a

Tactic:
]

Goal state after:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
a b c : R
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c * a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 1 ≤ a
n : ℤ
⊢ a ^ n ≤ a ^ n * a

Tactic:
]

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 1 ≤ a
n : ℤ
⊢ a ^ n ≤ a ^ n * a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁ : a ≤ 1
n : ℤ
⊢ a ^ n * a ≤ a ^ n

Tactic:
]

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁ : a ≤ 1
n : ℤ
⊢ a ^ n * a ≤ a ^ n
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 1 < a
n : ℤ
⊢ a ^ n < a ^ n * a

Tactic:
]

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 1 < a
n : ℤ
⊢ a ^ n < a ^ n * a
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
a b c : R
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0

Tactic:
]

Goal state after:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
a b c : R
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁ : a < 1
n : ℤ
⊢ a ^ n * a < a ^ n

Tactic:
]

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁ : a < 1
n : ℤ
⊢ a ^ n * a < a ^ n
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁ : a < 1
⊢ StrictAnti fun n ↦ a ^ n

Tactic:
by
  refine strictAnti_int_of_succ_lt fun n ↦ ?_
  rw [zpow_add_one₀ ha₀.ne']
  exact mul_lt_of_lt_one_right (zpow_pos ha₀ _) ha₁

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : a ≤ 0
hb : 0 ≤ b
⊢ a * b⁻¹ ≤ 0

Tactic:
]

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : a ≤ 0
hb : 0 ≤ b
⊢ a * b⁻¹ ≤ 0
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a * c ≤ b ↔ a * c ≤ b

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: case mp
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftStrictMono R
inst✝ : AddLeftReflectLT R
h : 0 < 0
⊢ False

Tactic:
]

Goal state after:
case mp
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftStrictMono R
inst✝ : AddLeftReflectLT R
h : 0 < 0
⊢ False
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b ≤ a * c ↔ b ≤ a * c

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a * c < b ↔ a * c < b

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ b < a * c ↔ b < a * c

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
⊢ b ^ 2 = b ^ 2

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
⊢ a * a + (a * b + b * b) = a * a + (a * b + b * b)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
a : R
ha : a < 0
b : R
hab : 0 = a + b
hb : 0 < b
⊢ a ^ 2 = a ^ 2

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a ≤ b ↔ a ≤ b

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hc : 0 < c
⊢ a < b ↔ a < b

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddLeftMono R
inst✝ : NoZeroDivisors R
r : R
⊢ r ^ 2 ≤ 0 ↔ r ^ 2 ≤ 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
⊢ a⁻¹ ≤ b ↔ a⁻¹ ≤ b

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
⊢ a⁻¹ < b ↔ a⁻¹ < b

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
hb : 0 < b
⊢ b ≤ a ↔ b ≤ a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
hb : 0 < b
⊢ b < a ↔ b < a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : NoZeroDivisors R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ a = 0 ∧ b = 0 ↔ a = 0 ∧ b = 0

pp: case ha
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : NoZeroDivisors R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ 0 ≤ a * a

pp: case hb
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : NoZeroDivisors R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ 0 ≤ b * b

Tactic:
]

Goal state after:
case ha
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : NoZeroDivisors R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ 0 ≤ a * a

case hb
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : NoZeroDivisors R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
⊢ 0 ≤ b * b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
hb : 0 < b
⊢ a ≤ b ↔ a ≤ b

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
hb : 0 < b
⊢ a < b ↔ a < b

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hb : 0 ≤ b
hc✝ : 0 ≤ c
h : a * c ≤ b
hc : 0 < c
⊢ a * c ≤ b

Tactic:
]

Goal state after:
case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hb : 0 ≤ b
hc✝ : 0 ≤ c
h : a * c ≤ b
hc : 0 < c
⊢ a * c ≤ b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hb✝ : 0 ≤ b
hc : 0 ≤ c
h : a ≤ c * b
hb : 0 < b
⊢ a ≤ c * b

Tactic:
]

Goal state after:
case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hb✝ : 0 ≤ b
hc : 0 ≤ c
h : a ≤ c * b
hb : 0 < b
⊢ a ≤ c * b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : MulPosReflectLT G₀
a b : G₀
inst✝ : ZeroLEOneClass G₀
h : a ≤ b
hb : 0 ≤ b
⊢ a ≤ b

Tactic:
]

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : MulPosReflectLT G₀
a b : G₀
inst✝ : ZeroLEOneClass G₀
h : a ≤ b
hb : 0 ≤ b
⊢ a ≤ b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hab : a ≤ b
hc : 0 ≤ c
⊢ a * c⁻¹ ≤ b * c⁻¹

Tactic:
]

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hab : a ≤ b
hc : 0 ≤ c
⊢ a * c⁻¹ ≤ b * c⁻¹
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
h : a < b
hc : 0 < c
⊢ a * c⁻¹ < b * c⁻¹

Tactic:
]

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
h : a < b
hc : 0 < c
⊢ a * c⁻¹ < b * c⁻¹
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ b ≤ a ↔ b ≤ a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ b < a ↔ b < a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ b⁻¹ ≤ a ↔ b⁻¹ ≤ a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ b⁻¹ < a ↔ b⁻¹ < a

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ b ≤ a⁻¹ ↔ b ≤ a⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ b < a⁻¹ ↔ b < a⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
ha : 0 ≤ a
hc : 0 < c
h : c ≤ b
⊢ a * b⁻¹ ≤ a * c⁻¹

Tactic:
]

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
ha : 0 ≤ a
hc : 0 < c
h : c ≤ b
⊢ a * b⁻¹ ≤ a * c⁻¹
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : LinearOrder R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b : R
⊢ 2 * (a * b) + 2 * (a * b) = 2 * (a * b) + 2 * (a * b)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c d : G₀
hc : 0 ≤ c
hac : a ≤ c
hd : 0 < d
hdb : d ≤ b
⊢ a * b⁻¹ ≤ c * d⁻¹

Tactic:
]

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c d : G₀
hc : 0 ≤ c
hac : a ≤ c
hd : 0 < d
hdb : d ≤ b
⊢ a * b⁻¹ ≤ c * d⁻¹