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

Goal state before:
pp: α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst✝² : MulZeroClass α
a✝ b✝ c✝ d : α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLE α
a : α>0
b c : α
h : ↑a * b < ↑a * c
⊢ b ≠ c

Tactic:
rintro rfl
        simp at h

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

Goal state before:
pp: α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
inst✝² : MulZeroClass α
a✝ b✝ c✝ d : α
inst✝¹ : PartialOrder α
inst✝ : MulPosReflectLE α
a : α>0
b c : α
h : b * ↑a < c * ↑a
⊢ b ≠ c

Tactic:
rintro rfl
        simp at h

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

Goal state before:
pp: α : Type u_1
inst✝³ : MulZeroClass α
a c : α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
a0 : 0 < a
hab : a ≤ a
hcd : c ≤ c
d0 : 0 < c
⊢ a * c = a * c

Tactic:
;

Goal state after:
α : Type u_1
inst✝³ : MulZeroClass α
a c : α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
a0 : 0 < a
hab : a ≤ a
hcd : c ≤ c
d0 : 0 < c
⊢ a * c = a * c
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : MulZeroClass α
a c : α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
c0 : 0 < c
hab : a ≤ a
b0 : 0 < a
hcd : c ≤ c
⊢ a * c = a * c

Tactic:
;

Goal state after:
α : Type u_1
inst✝³ : MulZeroClass α
a c : α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
c0 : 0 < c
hab : a ≤ a
b0 : 0 < a
hcd : c ≤ c
⊢ a * c = a * c
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case refine_2
α : Type u_1
inst✝⁵ : MulZeroClass α
a b c d : α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulReflectLE α
inst✝² : MulPosReflectLE α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
ha : 0 < a
hc : 0 < c
hab : a ≤ b
hcd : c ≤ d
h : b * d ≤ b * c
⊢ d ≤ c

pp: case ha
α : Type u_1
inst✝⁵ : MulZeroClass α
a b c d : α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulReflectLE α
inst✝² : MulPosReflectLE α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
ha : 0 < a
hc : 0 < c
hab : a ≤ b
hcd : c ≤ d
h : b * d ≤ a * c
⊢ 0 ≤ c

Tactic:
· exact le_of_mul_le_mul_of_pos_left h <| ha.trans_le hab

Goal state after:
case ha
α : Type u_1
inst✝⁵ : MulZeroClass α
a b c d : α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulReflectLE α
inst✝² : MulPosReflectLE α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
ha : 0 < a
hc : 0 < c
hab : a ≤ b
hcd : c ≤ d
h : b * d ≤ a * c
⊢ 0 ≤ c
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: case h₂
R : Type u
inst✝⁴ : Semiring R
inst✝³ : Preorder R
a b : R
inst✝² : ZeroLEOneClass R
inst✝¹ : MulPosMono R
inst✝ : AddLeftMono R
a2 : 2 ≤ a
b0 : 0 ≤ b
⊢ b ≤ a * b

Tactic:
;

Goal state after:
case h₂
R : Type u
inst✝⁴ : Semiring R
inst✝³ : Preorder R
a b : R
inst✝² : ZeroLEOneClass R
inst✝¹ : MulPosMono R
inst✝ : AddLeftMono R
a2 : 2 ≤ a
b0 : 0 ≤ b
⊢ b ≤ a * b
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: case ha
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ 0 ≤ d

Tactic:
;

Goal state after:
case ha
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ 0 ≤ d
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
inst✝ : ZeroLEOneClass M₀
n : ℕ
⊢ 0 ≤ 1

Tactic:
;

Goal state after:
M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
inst✝ : ZeroLEOneClass M₀
n : ℕ
⊢ 0 ≤ 1
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inl
M₀ : Type u_2
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a b : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha : 1 ≤ a
hb : 1 < b
⊢ 1 < a * b

pp: case inr
M₀ : Type u_2
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a b : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha : 1 < a
hb : 1 ≤ b
⊢ 1 < a * b

Tactic:
;

Goal state after:
case inl
M₀ : Type u_2
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a b : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha : 1 ≤ a
hb : 1 < b
⊢ 1 < a * b

case inr
M₀ : Type u_2
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a b : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha : 1 < a
hb : 1 ≤ b
⊢ 1 < a * b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
a : M₀
inst✝ : PosMulMono M₀
h₀ : 0 ≤ a
h₁ : a < 1
n : ℕ
x✝ : n + 1 ≠ 0
⊢ a * a ^ n < 1

Tactic:
;

Goal state after:
M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : Preorder M₀
a : M₀
inst✝ : PosMulMono M₀
h₀ : 0 ≤ a
h₁ : a < 1
n : ℕ
x✝ : n + 1 ≠ 0
⊢ a * a ^ n < 1
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : Preorder M₀
a : M₀
inst✝¹ : ZeroLEOneClass M₀
inst✝ : PosMulMono M₀
h : 1 ≤ a
n : ℕ
⊢ a ^ n ≤ a ^ n * a

Tactic:
;

Goal state after:
M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : Preorder M₀
a : M₀
inst✝¹ : ZeroLEOneClass M₀
inst✝ : PosMulMono M₀
h : 1 ≤ a
n : ℕ
⊢ a ^ n ≤ a ^ n * a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : Preorder M₀
a : M₀
inst✝¹ : ZeroLEOneClass M₀
inst✝ : PosMulMono M₀
ha : 1 < a
n : ℕ
x✝ : n + 1 ≠ 0
⊢ 1 < a * a ^ n

Tactic:
;

Goal state after:
M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : Preorder M₀
a : M₀
inst✝¹ : ZeroLEOneClass M₀
inst✝ : PosMulMono M₀
ha : 1 < a
n : ℕ
x✝ : n + 1 ≠ 0
⊢ 1 < a * a ^ n
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: case ha
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ 0 ≤ d

Tactic:
;

Goal state after:
case ha
R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : Preorder R
a b c : R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
h : b ≤ a
hc : c ≤ 0
d : R
hcd : 0 = c + d
⊢ 0 ≤ d
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝⁵ : MonoidWithZero M₀
inst✝⁴ : PartialOrder M₀
a b c d : M₀
inst✝³ : PosMulMono M₀
inst✝² : PosMulStrictMono M₀
inst✝¹ : MulPosStrictMono M₀
inst✝ : DecidableLE M₀
h1 : a < c
h2 : b < d
h3 : 0 ≤ a
h4 : 0 ≤ b
b0 : 0 = b
⊢ 0 < c * d

Tactic:
;

Goal state after:
M₀ : Type u_2
inst✝⁵ : MonoidWithZero M₀
inst✝⁴ : PartialOrder M₀
a b c d : M₀
inst✝³ : PosMulMono M₀
inst✝² : PosMulStrictMono M₀
inst✝¹ : MulPosStrictMono M₀
inst✝ : DecidableLE M₀
h1 : a < c
h2 : b < d
h3 : 0 ≤ a
h4 : 0 ≤ b
b0 : 0 = b
⊢ 0 < c * d
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝⁴ : MonoidWithZero M₀
inst✝³ : PartialOrder M₀
a : M₀
inst✝² : PosMulStrictMono M₀
inst✝¹ : ZeroLEOneClass M₀
ha : 0 < a
inst✝ : Nontrivial M₀
⊢ 0 < a ^ 0

Tactic:
;

Goal state after:
M₀ : Type u_2
inst✝⁴ : MonoidWithZero M₀
inst✝³ : PartialOrder M₀
a : M₀
inst✝² : PosMulStrictMono M₀
inst✝¹ : ZeroLEOneClass M₀
ha : 0 < a
inst✝ : Nontrivial M₀
⊢ 0 < a ^ 0
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝⁴ : MonoidWithZero M₀
inst✝³ : PartialOrder M₀
a : M₀
inst✝² : PosMulStrictMono M₀
inst✝¹ : ZeroLEOneClass M₀
ha : 0 < a
inst✝ : Nontrivial M₀
⊢ 0 < 1

Tactic:
;

Goal state after:
M₀ : Type u_2
inst✝⁴ : MonoidWithZero M₀
inst✝³ : PartialOrder M₀
a : M₀
inst✝² : PosMulStrictMono M₀
inst✝¹ : ZeroLEOneClass M₀
ha : 0 < a
inst✝ : Nontrivial M₀
⊢ 0 < 1
Module: Mathlib.Algebra.Order.Ring.Defs

Goal state before:
pp: R : Type u_1
inst✝⁴ : AddMonoidWithOne R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : NeZero 1
inst✝ : AddLeftStrictMono R
n : ℕ
⊢ ↑n < ↑n + 1

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁴ : AddMonoidWithOne R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : NeZero 1
inst✝ : AddLeftStrictMono R
n : ℕ
⊢ ↑n < ↑n + 1
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: case ha
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : Preorder R
a b c d : R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosMono R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
hca : c ≤ a
hbd : b ≤ d
hc : 0 ≤ c
hb : b ≤ 0
⊢ 0 ≤ c

Tactic:
;

Goal state after:
case ha
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : Preorder R
a b c d : R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosMono R
inst✝² : PosMulMono R
inst✝¹ : AddRightMono R
inst✝ : AddRightReflectLE R
hca : c ≤ a
hbd : b ≤ d
hc : 0 ≤ c
hb : b ≤ 0
⊢ 0 ≤ c
Module: Mathlib.Algebra.Order.Ring.Defs

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : b + b * c ≤ a + c
⊢ 1 - a ≤ (1 - b) * (1 + c)

Tactic:
rw [one_sub_mul, mul_one_add, sub_le_sub_iff, add_assoc, add_comm c]

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : b + b * c ≤ a + c
⊢ 1 + (b + b * c) ≤ 1 + (a + c)
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: case mk
α : Sort u
β : Sort v
g : α ↪ β
toFun✝ : α → β
inj'✝ : Injective toFun✝
h : { toFun := toFun✝, inj' := inj'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, inj' := inj'✝ } = g

Tactic:
;

Goal state after:
case mk
α : Sort u
β : Sort v
g : α ↪ β
toFun✝ : α → β
inj'✝ : Injective toFun✝
h : { toFun := toFun✝, inj' := inj'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, inj' := inj'✝ } = g
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: case mk.mk
α : Sort u
β : Sort v
toFun✝¹ : α → β
inj'✝¹ : Injective toFun✝¹
toFun✝ : α → β
inj'✝ : Injective toFun✝
h : { toFun := toFun✝¹, inj' := inj'✝¹ }.toFun = { toFun := toFun✝, inj' := inj'✝ }.toFun
⊢ { toFun := toFun✝¹, inj' := inj'✝¹ } = { toFun := toFun✝, inj' := inj'✝ }

Tactic:
;

Goal state after:
case mk.mk
α : Sort u
β : Sort v
toFun✝¹ : α → β
inj'✝¹ : Injective toFun✝¹
toFun✝ : α → β
inj'✝ : Injective toFun✝
h : { toFun := toFun✝¹, inj' := inj'✝¹ }.toFun = { toFun := toFun✝, inj' := inj'✝ }.toFun
⊢ { toFun := toFun✝¹, inj' := inj'✝¹ } = { toFun := toFun✝, inj' := inj'✝ }
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
inst✝ : IsEmpty α
a✝ : α ↪ β
⊢ a✝ = { toFun := fun a ↦ isEmptyElim a, inj' := ⋯ }

Tactic:
;

Goal state after:
α : Sort u_1
β : Sort u_2
inst✝ : IsEmpty α
a✝ : α ↪ β
⊢ a✝ = { toFun := fun a ↦ isEmptyElim a, inj' := ⋯ }
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
inst✝ : IsEmpty α
a✝ : α ↪ β
v : α
⊢ a✝ v = { toFun := fun a ↦ isEmptyElim a, inj' := ⋯ } v

Tactic:
;

Goal state after:
α : Sort u_1
β : Sort u_2
inst✝ : IsEmpty α
a✝ : α ↪ β
v : α
⊢ a✝ v = { toFun := fun a ↦ isEmptyElim a, inj' := ⋯ } v
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α : Sort ?u.9
β : Type ?u.24
x✝¹ : α ≃ β
x✝ : α
⊢ ((fun f ↦ (↑f).equivOfSurjective ⋯) ((fun f ↦ ⟨f.toEmbedding, ⋯⟩) x✝¹)) x✝ = x✝¹ x✝

Tactic:
;

Goal state after:
α : Sort ?u.9
β : Type ?u.24
x✝¹ : α ≃ β
x✝ : α
⊢ ((fun f ↦ (↑f).equivOfSurjective ⋯) ((fun f ↦ ⟨f.toEmbedding, ⋯⟩) x✝¹)) x✝ = x✝¹ x✝
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.Logic.Embedding.Basic

Goal state before:
pp: one : Type u_1
α : Type u_2
inst✝ : Unique one
f : one ↪ α
x✝ : one
⊢ ((fun a ↦ { toFun := fun x ↦ a, inj' := ⋯ }) ((fun f ↦ f default) f)) x✝ = f x✝

Tactic:
;

Goal state after:
one : Type u_1
α : Type u_2
inst✝ : Unique one
f : one ↪ α
x✝ : one
⊢ ((fun a ↦ { toFun := fun x ↦ a, inj' := ⋯ }) ((fun f ↦ f default) f)) x✝ = f x✝
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.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
a b : R
inst✝¹ : MulPosStrictMono R
inst✝ : PosMulStrictMono R
hab : 0 ≤ a * b
⊢ (0 ≤ a → b < 0) → ¬(a ≤ 0 → 0 < b)

Tactic:
;

Goal state after:
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
a b : R
inst✝¹ : MulPosStrictMono R
inst✝ : PosMulStrictMono R
hab : 0 ≤ a * b
⊢ (0 ≤ a → b < 0) → ¬(a ≤ 0 → 0 < b)
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
a b : R
inst✝¹ : MulPosStrictMono R
inst✝ : PosMulStrictMono R
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
⊢ False

Tactic:
;

Goal state after:
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
a b : R
inst✝¹ : MulPosStrictMono R
inst✝ : PosMulStrictMono R
hab : 0 ≤ a * b
ab : 0 ≤ a → b < 0
nab : a ≤ 0 → 0 < b
⊢ False
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.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.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosMono G₀
n : ℕ
⊢ MonotoneOn (fun a ↦ a ^ ↑n) {a | 0 ≤ a}

Tactic:
;

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosMono G₀
n : ℕ
⊢ MonotoneOn (fun a ↦ a ^ ↑n) {a | 0 ≤ a}
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosMono G₀
n : ℕ
hn : 0 < ↑n
⊢ StrictMonoOn (fun a ↦ a ^ ↑n) {a | 0 ≤ a}

Tactic:
;

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosMono G₀
n : ℕ
hn : 0 < ↑n
⊢ StrictMonoOn (fun a ↦ a ^ ↑n) {a | 0 ≤ a}
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: case ha
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hab : a ≤ b
hc : 0 ≤ c
⊢ 0 ≤ c⁻¹

Tactic:
;

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

Goal state before:
pp: case h₁
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 ≤ a ^ 2 + b ^ 2

Tactic:
;

Goal state after:
case h₁
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 ≤ a ^ 2 + b ^ 2
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

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

Tactic:
;

Goal state after:
case hb
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c d : G₀
hac : a < c
hdb : d ≤ b
hc : 0 ≤ c
hd : 0 < d
⊢ 0 < d
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : LinearOrder G₀
a : G₀
inst✝ : PosMulMono G₀
this : PosMulReflectLT G₀
⊢ a⁻¹ < 0 ↔ a < 0

Tactic:
;

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : LinearOrder G₀
a : G₀
inst✝ : PosMulMono G₀
this : PosMulReflectLT G₀
⊢ a⁻¹ < 0 ↔ a < 0
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : LinearOrder G₀
a : G₀
inst✝ : PosMulMono G₀
this : PosMulReflectLT G₀
⊢ a⁻¹ ≤ 0 ↔ a ≤ 0

Tactic:
;

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : LinearOrder G₀
a : G₀
inst✝ : PosMulMono G₀
this : PosMulReflectLT G₀
⊢ a⁻¹ ≤ 0 ↔ a ≤ 0
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

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

Tactic:
;

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α ↪ β
map_rel_iff'✝¹ : ∀ {a b : α}, s (f a) (f b) ↔ r a b
g : α ↪ β
map_rel_iff'✝ : ∀ {a b : α}, s (g a) (g b) ↔ r a b
⊢ { toEmbedding := f, map_rel_iff' := map_rel_iff'✝¹ }.toEmbedding =
      { toEmbedding := g, map_rel_iff' := map_rel_iff'✝ }.toEmbedding →
    { toEmbedding := f, map_rel_iff' := map_rel_iff'✝¹ } = { toEmbedding := g, map_rel_iff' := map_rel_iff'✝ }

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α ↪ β
map_rel_iff'✝¹ : ∀ {a b : α}, s (f a) (f b) ↔ r a b
g : α ↪ β
map_rel_iff'✝ : ∀ {a b : α}, s (g a) (g b) ↔ r a b
⊢ { toEmbedding := f, map_rel_iff' := map_rel_iff'✝¹ }.toEmbedding =
      { toEmbedding := g, map_rel_iff' := map_rel_iff'✝ }.toEmbedding →
    { toEmbedding := f, map_rel_iff' := map_rel_iff'✝¹ } = { toEmbedding := g, map_rel_iff' := map_rel_iff'✝ }
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
⊢ (0 < -a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ -a) ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)

Tactic:
;

Goal state after:
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
a b : R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
⊢ (0 < -a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ -a) ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ (x - a) * (x - b) ≤ 0 ↔ a ≤ x ∧ x ≤ b

Tactic:
rw [mul_nonpos_iff, sub_nonneg, sub_nonneg, sub_nonpos, sub_nonpos, or_iff_left_iff_imp, and_comm]

Goal state after:
R : Type u
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
a b : R
inst✝² : MulPosStrictMono R
inst✝¹ : PosMulStrictMono R
inst✝ : AddLeftMono R
x : R
h : a ≤ b
⊢ b ≤ x ∧ x ≤ a → a ≤ x ∧ x ≤ b
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α γ : Type u
r : α → α → Prop
t : γ → γ → Prop
x : α
s : α → α → Prop
h₁' : α = γ
h₂ : r ≍ s
h₂' : s ≍ t
⊢ ((RelIso.cast ⋯ h₂).trans (RelIso.cast h₁' h₂')) x = (RelIso.cast ⋯ ⋯) x

Tactic:
;

Goal state after:
α γ : Type u
r : α → α → Prop
t : γ → γ → Prop
x : α
s : α → α → Prop
h₁' : α = γ
h₂ : r ≍ s
h₂' : s ≍ t
⊢ ((RelIso.cast ⋯ h₂).trans (RelIso.cast h₁' h₂')) x = (RelIso.cast ⋯ ⋯) x
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
x✝¹ : r ≃r s
x✝ : α
⊢ ((fun f ↦ ofSurjective ↑f ⋯) ((fun f ↦ ⟨f.toRelEmbedding, ⋯⟩) x✝¹)) x✝ = x✝¹ x✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
x✝¹ : r ≃r s
x✝ : α
⊢ ((fun f ↦ ofSurjective ↑f ⋯) ((fun f ↦ ⟨f.toRelEmbedding, ⋯⟩) x✝¹)) x✝ = x✝¹ x✝
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₁ : r₁ →r s₁
x✝ : α₁
⊢ ((fun f₂ ↦ e₂.symm.toRelEmbedding.toRelHom.comp (f₂.comp e₁.toRelEmbedding.toRelHom))
        ((fun f₁ ↦ e₂.toRelEmbedding.toRelHom.comp (f₁.comp e₁.symm.toRelEmbedding.toRelHom)) f₁))
      x✝ =
    f₁ x✝

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₁ : r₁ →r s₁
x✝ : α₁
⊢ ((fun f₂ ↦ e₂.symm.toRelEmbedding.toRelHom.comp (f₂.comp e₁.toRelEmbedding.toRelHom))
        ((fun f₁ ↦ e₂.toRelEmbedding.toRelHom.comp (f₁.comp e₁.symm.toRelEmbedding.toRelHom)) f₁))
      x✝ =
    f₁ x✝