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

Goal state before:
pp: case coe.zero
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a b : α
inst✝¹ : Add α
inst✝ : ExistsAddOfLE α
a✝ : α
⊢ ↑a✝ ≤ 0 → ∃ c, 0 = ↑a✝ + c

pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a b : α
inst✝¹ : Add α
inst✝ : ExistsAddOfLE α
a✝¹ a✝ : α
⊢ ↑a✝¹ ≤ ↑a✝ → ∃ c, ↑a✝ = ↑a✝¹ + c

Tactic:
·

Goal state after:
case coe.zero
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a b : α
inst✝¹ : Add α
inst✝ : ExistsAddOfLE α
a✝ : α
⊢ ↑a✝ ≤ 0 → ∃ c, 0 = ↑a✝ + c
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case pos
m : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
h : findGreatest P n = 0
⊢ P (findGreatest P n)

pp: case neg
m : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
h : ¬findGreatest P n = 0
⊢ P (findGreatest P n)

Tactic:
·

Goal state after:
case pos
m : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
h : findGreatest P n = 0
⊢ P (findGreatest P n)
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case pos.zero
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : findGreatest P n = 0
hmb : 0 ≤ n
hm : P 0
⊢ P (findGreatest P n)

pp: case pos.succ
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : findGreatest P n = 0
n✝ : ℕ
hmb : n✝ + 1 ≤ n
hm : P (n✝ + 1)
⊢ P (findGreatest P n)

Tactic:
·

Goal state after:
case pos.zero
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : findGreatest P n = 0
hmb : 0 ≤ n
hm : P 0
⊢ P (findGreatest P n)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case bot
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
b : WithBot α
⊢ map (⇑f) (⊥ + b) = map ⇑f ⊥ + map (⇑f) b

pp: case coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
b : WithBot α
a✝ : α
⊢ map (⇑f) (↑a✝ + b) = map ⇑f ↑a✝ + map (⇑f) b

Tactic:
·

Goal state after:
case bot
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
b : WithBot α
⊢ map (⇑f) (⊥ + b) = map ⇑f ⊥ + map (⇑f) b
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
b : WithBot α
a✝ : α
⊢ map (⇑f) (↑a✝ + b) = map ⇑f ↑a✝ + map (⇑f) b

Tactic:
·

Goal state after:
case coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
b : WithBot α
a✝ : α
⊢ map (⇑f) (↑a✝ + b) = map ⇑f ↑a✝ + map (⇑f) b
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case neg
m : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
h : ¬findGreatest P n = 0
⊢ P (findGreatest P n)

Tactic:
·

Goal state after:
case neg
m : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
h : ¬findGreatest P n = 0
⊢ P (findGreatest P n)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case coe.bot
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝ : α
⊢ map (⇑f) (↑a✝ + ⊥) = map ⇑f ↑a✝ + map ⇑f ⊥

pp: case coe.coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map (⇑f) (↑a✝¹ + ↑a✝) = map ⇑f ↑a✝¹ + map ⇑f ↑a✝

Tactic:
·

Goal state after:
case coe.bot
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝ : α
⊢ map (⇑f) (↑a✝ + ⊥) = map ⇑f ↑a✝ + map ⇑f ⊥
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case pos
P : ℕ → Prop
inst✝ : DecidablePred P
m n m✝ : ℕ
hmk : m.le m✝
ih : findGreatest P m ≤ findGreatest P m✝
h✝ : P (m✝ + 1)
⊢ findGreatest P m ≤ m✝ + 1

pp: case neg
P : ℕ → Prop
inst✝ : DecidablePred P
m n m✝ : ℕ
hmk : m.le m✝
ih : findGreatest P m ≤ findGreatest P m✝
h✝ : ¬P (m✝ + 1)
⊢ findGreatest P m ≤ findGreatest P m✝

Tactic:
·

Goal state after:
case pos
P : ℕ → Prop
inst✝ : DecidablePred P
m n m✝ : ℕ
hmk : m.le m✝
ih : findGreatest P m ≤ findGreatest P m✝
h✝ : P (m✝ + 1)
⊢ findGreatest P m ≤ m✝ + 1
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case neg
P : ℕ → Prop
inst✝ : DecidablePred P
m n m✝ : ℕ
hmk : m.le m✝
ih : findGreatest P m ≤ findGreatest P m✝
h✝ : ¬P (m✝ + 1)
⊢ findGreatest P m ≤ findGreatest P m✝

Tactic:
·

Goal state after:
case neg
P : ℕ → Prop
inst✝ : DecidablePred P
m n m✝ : ℕ
hmk : m.le m✝
ih : findGreatest P m ≤ findGreatest P m✝
h✝ : ¬P (m✝ + 1)
⊢ findGreatest P m ≤ findGreatest P m✝
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case pos
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : P (n + 1)
⊢ findGreatest P (n + 1) ≤ findGreatest Q (n + 1)

pp: case neg
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : ¬P (n + 1)
⊢ findGreatest P (n + 1) ≤ findGreatest Q (n + 1)

Tactic:
·

Goal state after:
case pos
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : P (n + 1)
⊢ findGreatest P (n + 1) ≤ findGreatest Q (n + 1)
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case neg
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : ¬P (n + 1)
⊢ findGreatest P (n + 1) ≤ findGreatest Q (n + 1)

Tactic:
·

Goal state after:
case neg
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : ¬P (n + 1)
⊢ findGreatest P (n + 1) ≤ findGreatest Q (n + 1)
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Mul α
inst✝ : MulLeftReflectLT α
b c : WithZero α
h : 0 * b < 0 * c
this : 0 * c ≠ 0
⊢ b < c

pp: case coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Mul α
inst✝ : MulLeftReflectLT α
b c : WithZero α
a✝ : α
h : ↑a✝ * b < ↑a✝ * c
this : ↑a✝ * c ≠ 0
⊢ b < c

Tactic:
·

Goal state after:
case zero
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Mul α
inst✝ : MulLeftReflectLT α
b c : WithZero α
h : 0 * b < 0 * c
this : 0 * c ≠ 0
⊢ b < c
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case coe.zero
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Mul α
inst✝ : MulLeftReflectLT α
b : WithZero α
a✝ : α
h : ↑a✝ * b < ↑a✝ * 0
this : ↑a✝ * 0 ≠ 0
⊢ b < 0

pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Mul α
inst✝ : MulLeftReflectLT α
b : WithZero α
a✝¹ a✝ : α
h : ↑a✝¹ * b < ↑a✝¹ * ↑a✝
this : ↑a✝¹ * ↑a✝ ≠ 0
⊢ b < ↑a✝

Tactic:
·

Goal state after:
case coe.zero
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : Mul α
inst✝ : MulLeftReflectLT α
b : WithZero α
a✝ : α
h : ↑a✝ * b < ↑a✝ * 0
this : ↑a✝ * 0 ≠ 0
⊢ b < 0
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type ?u.6
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedRing α
inst✝ : Nontrivial α
bounded : ∀ (x : α), ∃ n, x ≤ ↑n
x : α
⊢ ∃ n, ↑n ≤ x

Tactic:
by
    obtain ⟨n, hn⟩ := bounded (-x)
    use -n
    simpa [neg_le]

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

Goal state before:
pp: case inl
y : Multiplicative ℤ
⊢ 0 < ↑y * exp 1 ↔ 0 ≤ ↑y

pp: case inr
x : WithZero (Multiplicative ℤ)
y : Multiplicative ℤ
hx : x ≠ 0
⊢ x < ↑y * exp 1 ↔ x ≤ ↑y

Tactic:
·

Goal state after:
case inl
y : Multiplicative ℤ
⊢ 0 < ↑y * exp 1 ↔ 0 ≤ ↑y
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case zero
G : Type u_3
inst✝¹ : Preorder G
inst✝ : AddGroup G
⊢ 0 ≤ exp (log 0)

pp: case coe
G : Type u_3
inst✝¹ : Preorder G
inst✝ : AddGroup G
a✝ : Multiplicative G
⊢ ↑a✝ ≤ exp (↑a✝).log

Tactic:
·

Goal state after:
case zero
G : Type u_3
inst✝¹ : Preorder G
inst✝ : AddGroup G
⊢ 0 ≤ exp (log 0)
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: case coe
G : Type u_3
inst✝¹ : Preorder G
inst✝ : AddGroup G
a✝ : Multiplicative G
⊢ ↑a✝ ≤ exp (↑a✝).log

Tactic:
·

Goal state after:
case coe
G : Type u_3
inst✝¹ : Preorder G
inst✝ : AddGroup G
a✝ : Multiplicative G
⊢ ↑a✝ ≤ exp (↑a✝).log
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a ≤ b
ha : a ≤ 0
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊

pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a ≤ b
ha : 0 ≤ a
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a ≤ b
ha : a ≤ 0
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a ≤ b
ha : 0 ≤ a
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a ≤ b
ha : 0 ≤ a
⊢ ⌊a⌋₊ ≤ ⌊b⌋₊
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
n : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
ha : a ≤ 0
⊢ n ≤ ⌊a⌋₊ ↔ ↑n ≤ a

pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
n : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
ha : 0 ≤ a
⊢ n ≤ ⌊a⌋₊ ↔ ↑n ≤ a

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
n : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
ha : a ≤ 0
⊢ n ≤ ⌊a⌋₊ ↔ ↑n ≤ a
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
n : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
ha : 0 ≤ a
⊢ n ≤ ⌊a⌋₊ ↔ ↑n ≤ a

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
n : ℕ
inst✝ : IsStrictOrderedRing R
hn : n ≠ 0
ha : 0 ≤ a
⊢ n ≤ ⌊a⌋₊ ↔ ↑n ≤ a
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
n : ℕ
hn : n ≠ 0
a : R
ha : a ≤ 0
⊢ ⌊a * ↑n⌋₊ / n = ⌊a⌋₊

pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
n : ℕ
hn : n ≠ 0
a : R
ha : 0 ≤ a
⊢ ⌊a * ↑n⌋₊ / n = ⌊a⌋₊

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
n : ℕ
hn : n ≠ 0
a : R
ha : a ≤ 0
⊢ ⌊a * ↑n⌋₊ / n = ⌊a⌋₊
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
n : ℕ
hn : n ≠ 0
a : R
ha : a ≤ 0
⊢ 0 / n = 0

pp: case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
n : ℕ
hn : n ≠ 0
a : R
ha : a ≤ 0
⊢ a * ↑n ≤ 0

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
n : ℕ
hn : n ≠ 0
a : R
ha : a ≤ 0
⊢ 0 / n = 0
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a : R
ha : a ≤ 0
⊢ ⌊a⌋₊ ≤ ⌈a⌉₊

pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a : R
ha : 0 ≤ a
⊢ ⌊a⌋₊ ≤ ⌈a⌉₊

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a : R
ha : a ≤ 0
⊢ ⌊a⌋₊ ≤ ⌈a⌉₊
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a : R
ha : 0 ≤ a
⊢ ⌊a⌋₊ ≤ ⌈a⌉₊

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a : R
ha : 0 ≤ a
⊢ ⌊a⌋₊ ≤ ⌈a⌉₊
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a < b
h' : 0 < b
ha : 0 ≤ a
⊢ ⌊a⌋₊ < ⌈b⌉₊

pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a < b
h' : 0 < b
ha : a < 0
⊢ ⌊a⌋₊ < ⌈b⌉₊

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a < b
h' : 0 < b
ha : 0 ≤ a
⊢ ⌊a⌋₊ < ⌈b⌉₊
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a < b
h' : 0 < b
ha : a < 0
⊢ ⌊a⌋₊ < ⌈b⌉₊

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a < b
h' : 0 < b
ha : a < 0
⊢ ⌊a⌋₊ < ⌈b⌉₊
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
hb : n ≤ b
⊢ ↑b ≤ a + ↑n ↔ b ≤ ⌊a⌋₊ + n

pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
hb : b ≤ n
⊢ ↑b ≤ a + ↑n ↔ b ≤ ⌊a⌋₊ + n

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
hb : n ≤ b
⊢ ↑b ≤ a + ↑n ↔ b ≤ ⌊a⌋₊ + n
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
hb : b ≤ n
⊢ ↑b ≤ a + ↑n ↔ b ≤ ⌊a⌋₊ + n

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
hb : b ≤ n
⊢ ↑b ≤ a + ↑n ↔ b ≤ ⌊a⌋₊ + n
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inl
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : a ≤ 0
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n

pp: case inr
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : a ≤ 0
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : a ≤ ↑n
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n

pp: case inr.inr
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : ↑n ≤ a
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n

Tactic:
·

Goal state after:
case inr.inl
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : a ≤ ↑n
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr.inr
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : ↑n ≤ a
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n

Tactic:
·

Goal state after:
case inr.inr
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : ↑n ≤ a
⊢ ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n
Module: Mathlib.Order.Directed

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Set β
h : DirectedOn r (f '' s)
x : β
hx : x ∈ s
y : β
hy : y ∈ s
⊢ ∃ z ∈ s, (r on f) x z ∧ (r on f) y z

Tactic:
obtain ⟨_, ⟨z, hz, rfl⟩, hz'⟩ := h (f x) (Set.mem_image_of_mem f hx) (f y)
    (Set.mem_image_of_mem f hy)

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Set β
h : DirectedOn r (f '' s)
x : β
hx : x ∈ s
y : β
hy : y ∈ s
z : β
hz : z ∈ s
hz' : r (f x) (f z) ∧ r (f y) (f z)
⊢ ∃ z ∈ s, (r on f) x z ∧ (r on f) y z
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
hb : n ≤ b
⊢ ↑b < a + ↑n ↔ b < ⌈a⌉₊ + n

pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
hb : b < n
⊢ ↑b < a + ↑n ↔ b < ⌈a⌉₊ + n

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
hb : n ≤ b
⊢ ↑b < a + ↑n ↔ b < ⌈a⌉₊ + n
Module: Mathlib.Order.Directed

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
he : Injective e
a b : β
ha : ¬∃ i, e i = a
⊢ ∃ z, (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ a) (extend e f ⊥ z) ∧ (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)

pp: case inr
α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
he : Injective e
b : β
i : ι
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
he : Injective e
a b : β
ha : ¬∃ i, e i = a
⊢ ∃ z, (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ a) (extend e f ⊥ z) ∧ (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
hb : b < n
⊢ ↑b < a + ↑n ↔ b < ⌈a⌉₊ + n

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
hb : b < n
⊢ ↑b < a + ↑n ↔ b < ⌈a⌉₊ + n
Module: Mathlib.Order.Directed

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
he : Injective e
b : β
i : ι
hb : ¬∃ i, e i = b
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)

pp: case inr.inr
α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
he : Injective e
i j : ι
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ (e j)) (extend e f ⊥ z)

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
ι : Sort u_3
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 ↦ x1 ≤ x2) f
he : Injective e
b : β
i : ι
hb : ¬∃ i, e i = b
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun x1 x2 ↦ x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inl
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
han : a ≤ ↑n
⊢ ⌈a - ↑n⌉₊ = ⌈a⌉₊ - n

pp: case inr
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
hna : ↑n ≤ a
⊢ ⌈a - ↑n⌉₊ = ⌈a⌉₊ - n

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
han : a ≤ ↑n
⊢ ⌈a - ↑n⌉₊ = ⌈a⌉₊ - n
Module: Mathlib.Order.Directed

Goal state before:
pp: case inl.inl
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
s : Set α
hd : DirectedOn r s
y : α
ha : ∀ b ∈ s, ∃ c ∈ s, r y c ∧ r b c
⊢ ∃ z ∈ insert y s, r y z ∧ r y z

pp: case inl.inr
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
s : Set α
hd : DirectedOn r s
x : α
ha : ∀ b ∈ s, ∃ c ∈ s, r x c ∧ r b c
y : α
hy : y ∈ s
⊢ ∃ z ∈ insert x s, r x z ∧ r y z

pp: case inr.inl
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
s : Set α
hd : DirectedOn r s
x : α
hx : x ∈ s
y : α
ha : ∀ b ∈ s, ∃ c ∈ s, r y c ∧ r b c
⊢ ∃ z ∈ insert y s, r x z ∧ r y z

pp: case inr.inr
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
a : α
s : Set α
hd : DirectedOn r s
ha : ∀ b ∈ s, ∃ c ∈ s, r a c ∧ r b c
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ∃ z ∈ insert a s, r x z ∧ r y z

Tactic:
·

Goal state after:
case inl.inl
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
s : Set α
hd : DirectedOn r s
y : α
ha : ∀ b ∈ s, ∃ c ∈ s, r y c ∧ r b c
⊢ ∃ z ∈ insert y s, r y z ∧ r y z
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inr
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
hna : ↑n ≤ a
⊢ ⌈a - ↑n⌉₊ = ⌈a⌉₊ - n

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : FloorSemiring R
inst✝³ : IsStrictOrderedRing R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
n : ℕ
hna : ↑n ≤ a
⊢ ⌈a - ↑n⌉₊ = ⌈a⌉₊ - n
Module: Mathlib.Order.Directed

Goal state before:
pp: case inl.inr
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
s : Set α
hd : DirectedOn r s
x : α
ha : ∀ b ∈ s, ∃ c ∈ s, r x c ∧ r b c
y : α
hy : y ∈ s
⊢ ∃ z ∈ insert x s, r x z ∧ r y z

pp: case inr.inl
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
s : Set α
hd : DirectedOn r s
x : α
hx : x ∈ s
y : α
ha : ∀ b ∈ s, ∃ c ∈ s, r y c ∧ r b c
⊢ ∃ z ∈ insert y s, r x z ∧ r y z

pp: case inr.inr
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
a : α
s : Set α
hd : DirectedOn r s
ha : ∀ b ∈ s, ∃ c ∈ s, r a c ∧ r b c
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ∃ z ∈ insert a s, r x z ∧ r y z

Tactic:
·

Goal state after:
case inl.inr
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
s : Set α
hd : DirectedOn r s
x : α
ha : ∀ b ∈ s, ∃ c ∈ s, r x c ∧ r b c
y : α
hy : y ∈ s
⊢ ∃ z ∈ insert x s, r x z ∧ r y z