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

Goal state before:
pp: case pos
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ ⌊x⌋ + ⌊fract x⌋ = ⌊x⌋ + (⌊2 * fract x⌋ + 1) / 2

pp: case neg
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : ¬2 * fract x < 1
⊢ ⌊x⌋ + ⌈fract x⌉ = ⌊x⌋ + (⌊2 * fract x⌋ + 1) / 2

Tactic:
<;>

Goal state after:
case pos
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ ⌊x⌋ + ⌊fract x⌋ = ⌊x⌋ + (⌊2 * fract x⌋ + 1) / 2

case neg
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : ¬2 * fract x < 1
⊢ ⌊x⌋ + ⌈fract x⌉ = ⌊x⌋ + (⌊2 * fract x⌋ + 1) / 2
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ ⌊fract x⌋ = (⌊2 * fract x⌋ + 1) / 2

Tactic:
Int.floor_eq_zero_iff.mpr,

Goal state after:
case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ 0 = (⌊2 * fract x⌋ + 1) / 2

case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ fract x ∈ Ico 0 1
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case pos.e_a.hb
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ 0 ≤ fract x

pp: case h
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ 1 ≤ 2

Tactic:
<;>

Goal state after:
case pos.e_a.hb
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ 0 ≤ fract x

case h
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ 1 ≤ 2
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: case mp
k m : ℕ+
⊢ k ∣ m → ↑k ∣ ↑m

pp: case mpr
k m : ℕ+
⊢ ↑k ∣ ↑m → k ∣ m

Tactic:
<;>

Goal state after:
case mp
k m : ℕ+
⊢ k ∣ m → ↑k ∣ ↑m

case mpr
k m : ℕ+
⊢ ↑k ∣ ↑m → k ∣ m
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case left
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
this✝ : ↑⌊x + 1 / 2⌋ ≤ x + 1 / 2
this : x + 1 / 2 < ↑⌊x + 1 / 2⌋ + 1
⊢ x - ↑⌊x + 1 / 2⌋ ≤ 1 / 2

pp: case right
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
this✝ : ↑⌊x + 1 / 2⌋ ≤ x + 1 / 2
this : x + 1 / 2 < ↑⌊x + 1 / 2⌋ + 1
⊢ ↑⌊x + 1 / 2⌋ - x ≤ 1 / 2

Tactic:
<;>

Goal state after:
case left
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
this✝ : ↑⌊x + 1 / 2⌋ ≤ x + 1 / 2
this : x + 1 / 2 < ↑⌊x + 1 / 2⌋ + 1
⊢ x - ↑⌊x + 1 / 2⌋ ≤ 1 / 2

case right
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
this✝ : ↑⌊x + 1 / 2⌋ ≤ x + 1 / 2
this : x + 1 / 2 < ↑⌊x + 1 / 2⌋ + 1
⊢ ↑⌊x + 1 / 2⌋ - x ≤ 1 / 2
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case h₁
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ↑⌊a⌋ ≤ a

pp: case h₂
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ↑⌊b⌋ ≤ b

Tactic:
<;>

Goal state after:
case h₁
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ↑⌊a⌋ ≤ a

case h₂
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ↑⌊b⌋ ≤ b
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case left
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = ↑z
⊢ a - b ≤ a

pp: case right
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = ↑z
⊢ a < a - b + 1

Tactic:
<;>

Goal state after:
case left
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = ↑z
⊢ a - b ≤ a

case right
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h₀ : 0 ≤ b
h₁ : b < 1
z : ℤ
hz : a - b = ↑z
⊢ a < a - b + 1
Module: Mathlib.Algebra.Order.Ring.Pow

Goal state before:
pp: case hbc.Hcomm
R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ b ^ 2
Hsq' : 0 ≤ (a + b) ^ 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ Commute a b

pp: case hbc.ha
R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ b ^ 2
Hsq' : 0 ≤ (a + b) ^ 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ 0 ≤ a

pp: case hbc.Hsq
R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ b ^ 2
Hsq' : 0 ≤ (a + b) ^ 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ 0 ≤ b ^ 2

pp: case hbc.Hsq'
R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ b ^ 2
Hsq' : 0 ≤ (a + b) ^ 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ 0 ≤ (a + b) ^ 2

pp: case hbc.H
R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ b ^ 2
Hsq' : 0 ≤ (a + b) ^ 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ 0 ≤ 2 * a + b

Tactic:
<;>

Goal state after:
case hbc.Hcomm
R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ b ^ 2
Hsq' : 0 ≤ (a + b) ^ 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ Commute a b

case hbc.ha
R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ b ^ 2
Hsq' : 0 ≤ (a + b) ^ 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ 0 ≤ a

case hbc.Hsq
R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ b ^ 2
Hsq' : 0 ≤ (a + b) ^ 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ 0 ≤ b ^ 2

case hbc.Hsq'
R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ b ^ 2
Hsq' : 0 ≤ (a + b) ^ 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ 0 ≤ (a + b) ^ 2

case hbc.H
R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ b ^ 2
Hsq' : 0 ≤ (a + b) ^ 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ 0 ≤ 2 * a + b
Module: Mathlib.Algebra.Order.Ring.Pow

Goal state before:
pp: case hbc
R : Type u_1
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b : R
Hcomm : Commute a b
ha : 0 ≤ a
Hsq : 0 ≤ b ^ 2
Hsq' : 0 ≤ (a + b) ^ 2
H : 0 ≤ 2 * a + b
n : ℕ
⊢ a ^ (n + 1) + ↑(n + 1) * a ^ n * b ≤ (a + b) ^ (n + 1)

Tactic:
apply Commute.pow_add_mul_le_add_pow_of_sq_nonneg <;> assumption

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

Goal state before:
pp: case mp
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
⊢ (∃ z, -x = ↑z) → ∃ z, x = ↑z

pp: case mpr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
⊢ (∃ z, x = ↑z) → ∃ z, -x = ↑z

Tactic:
<;>

Goal state after:
case mp
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
⊢ (∃ z, -x = ↑z) → ∃ z, x = ↑z

case mpr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
⊢ (∃ z, x = ↑z) → ∃ z, -x = ↑z
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case mp
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
z : ℤ
hz : -x = ↑z
⊢ ∃ z, x = ↑z

pp: case mpr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
z : ℤ
hz : x = ↑z
⊢ ∃ z, -x = ↑z

Tactic:
<;>

Goal state after:
case mp
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
z : ℤ
hz : -x = ↑z
⊢ ∃ z, x = ↑z

case mpr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
z : ℤ
hz : x = ↑z
⊢ ∃ z, -x = ↑z
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case h
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
z : ℤ
hz : -x = ↑z
⊢ x = ↑(-z)

pp: case h
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
z : ℤ
hz : x = ↑z
⊢ -x = ↑(-z)

Tactic:
<;>

Goal state after:
case h
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
z : ℤ
hz : -x = ↑z
⊢ x = ↑(-z)

case h
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
z : ℤ
hz : x = ↑z
⊢ -x = ↑(-z)
Module: Mathlib.Tactic.Positivity.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LT α
ha : 0 < a
hb : 0 < b
h✝ : p
⊢ 0 < if p then a else b

pp: case neg
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LT α
ha : 0 < a
hb : 0 < b
h✝ : ¬p
⊢ 0 < if p then a else b

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LT α
ha : 0 < a
hb : 0 < b
h✝ : p
⊢ 0 < if p then a else b

case neg
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LT α
ha : 0 < a
hb : 0 < b
h✝ : ¬p
⊢ 0 < if p then a else b
Module: Mathlib.Tactic.Positivity.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : 0 ≤ a
hb : 0 ≤ b
h✝ : p
⊢ 0 ≤ if p then a else b

pp: case neg
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : 0 ≤ a
hb : 0 ≤ b
h✝ : ¬p
⊢ 0 ≤ if p then a else b

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : 0 ≤ a
hb : 0 ≤ b
h✝ : p
⊢ 0 ≤ if p then a else b

case neg
α : Type u_1
inst✝² : Zero α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LE α
ha : 0 ≤ a
hb : 0 ≤ b
h✝ : ¬p
⊢ 0 ≤ if p then a else b
Module: Mathlib.Tactic.Positivity.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Zero α
p : Prop
inst✝ : Decidable p
a b : α
ha : a ≠ 0
hb : b ≠ 0
h✝ : p
⊢ (if p then a else b) ≠ 0

pp: case neg
α : Type u_1
inst✝¹ : Zero α
p : Prop
inst✝ : Decidable p
a b : α
ha : a ≠ 0
hb : b ≠ 0
h✝ : ¬p
⊢ (if p then a else b) ≠ 0

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝¹ : Zero α
p : Prop
inst✝ : Decidable p
a b : α
ha : a ≠ 0
hb : b ≠ 0
h✝ : p
⊢ (if p then a else b) ≠ 0

case neg
α : Type u_1
inst✝¹ : Zero α
p : Prop
inst✝ : Decidable p
a b : α
ha : a ≠ 0
hb : b ≠ 0
h✝ : ¬p
⊢ (if p then a else b) ≠ 0
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case h₁
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ a ≤ ↑⌈a⌉

pp: case h₂
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ b ≤ ↑⌈b⌉

Tactic:
<;>

Goal state after:
case h₁
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ a ≤ ↑⌈a⌉

case h₂
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ b ≤ ↑⌈b⌉
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: q : ℚ
this : ↑q.num < (q - fract q + 1) * ↑q.den
⊢ ↑q.num < (↑⌊q⌋ + 1) * ↑q.den

Tactic:
have : (⌊q⌋ : ℚ) = q - fract q := eq_sub_of_add_eq <| floor_add_fract q
    rwa [this]

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

Goal state before:
pp: case refine_1
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha : 1 ≤ a
⊢ 0 < 2⁻¹

pp: case refine_2
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha : 1 ≤ a
⊢ 2⁻¹ < 1

pp: case refine_3
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha : 1 ≤ a
⊢ ↑⌈2⁻¹ / (1 - 2⁻¹)⌉ ≤ a

Tactic:
<;>

Goal state after:
case refine_1
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha : 1 ≤ a
⊢ 0 < 2⁻¹

case refine_2
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha : 1 ≤ a
⊢ 2⁻¹ < 1

case refine_3
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha : 1 ≤ a
⊢ ↑⌈2⁻¹ / (1 - 2⁻¹)⌉ ≤ a
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case refine_1
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x y : K
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : x < ↑z / ↑n
zh' : ↑z / ↑n < y
⊢ x < ↑(↑z / ↑n)

pp: case refine_2
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x y : K
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : x < ↑z / ↑n
zh' : ↑z / ↑n < y
⊢ ↑(↑z / ↑n) < y

Tactic:
<;>

Goal state after:
case refine_1
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x y : K
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : x < ↑z / ↑n
zh' : ↑z / ↑n < y
⊢ x < ↑(↑z / ↑n)

case refine_2
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x y : K
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : x < ↑z / ↑n
zh' : ↑z / ↑n < y
⊢ ↑(↑z / ↑n) < y
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case refine_1
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
m : ℕ
hm : y / δ + 1 / δ ≤ ↑m
⊢ y ≤ ↑m * δ

pp: case refine_2
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
m : ℕ
hm : y / δ + 1 / δ ≤ ↑m
⊢ 1 ≤ ↑m * δ

Tactic:
<;>

Goal state after:
case refine_1
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
m : ℕ
hm : y / δ + 1 / δ ≤ ↑m
⊢ y ≤ ↑m * δ

case refine_2
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
m : ℕ
hm : y / δ + 1 / δ ≤ ↑m
⊢ 1 ≤ ↑m * δ
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case refine_1
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : max x 0 < ↑q₁
hq₁₂ : q₁ < q₂
this : 0 < q₂
q : ℚ
hq : 0 < q
hq₁ : q₁ < q ^ n
hq₂ : q ^ n < q₂
⊢ ↑q₁ < ↑q ^ n

pp: case refine_2
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : max x 0 < ↑q₁
hq₁₂ : q₁ < q₂
this : 0 < q₂
q : ℚ
hq : 0 < q
hq₁ : q₁ < q ^ n
hq₂ : q ^ n < q₂
⊢ ↑q ^ n < ↑q₂

Tactic:
<;>

Goal state after:
case refine_1
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : max x 0 < ↑q₁
hq₁₂ : q₁ < q₂
this : 0 < q₂
q : ℚ
hq : 0 < q
hq₁ : q₁ < q ^ n
hq₂ : q ^ n < q₂
⊢ ↑q₁ < ↑q ^ n

case refine_2
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : max x 0 < ↑q₁
hq₁₂ : q₁ < q₂
this : 0 < q₂
q : ℚ
hq : 0 < q
hq₁ : q₁ < q ^ n
hq₂ : q ^ n < q₂
⊢ ↑q ^ n < ↑q₂
Module: Mathlib.Data.List.Perm.Subperm

Goal state before:
pp: case pos
α : Type u_1
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
ha : a ∈ l₁
⊢ a ∈ l₁ → count a l₁ ≤ count a l₂ ↔ count a l₁ ≤ count a l₂

pp: case neg
α : Type u_1
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
ha : ¬a ∈ l₁
⊢ a ∈ l₁ → count a l₁ ≤ count a l₂ ↔ count a l₁ ≤ count a l₂

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
ha : a ∈ l₁
⊢ a ∈ l₁ → count a l₁ ≤ count a l₂ ↔ count a l₁ ≤ count a l₂

case neg
α : Type u_1
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
ha : ¬a ∈ l₁
⊢ a ∈ l₁ → count a l₁ ≤ count a l₂ ↔ count a l₁ ≤ count a l₂
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case mp.zero
α : Type u_1
s t : Multiset α
⊢ 0 = 0

pp: case mp.cons
α : Type u_1
s t : Multiset α
a✝² b✝ : α
as✝ bs✝ : Multiset α
a✝¹ : a✝² = b✝
a✝ : Rel (fun x1 x2 ↦ x1 = x2) as✝ bs✝
a_ih✝ : as✝ = bs✝
⊢ a✝² ::ₘ as✝ = b✝ ::ₘ bs✝

Tactic:
<;>

Goal state after:
case mp.zero
α : Type u_1
s t : Multiset α
⊢ 0 = 0

case mp.cons
α : Type u_1
s t : Multiset α
a✝² b✝ : α
as✝ bs✝ : Multiset α
a✝¹ : a✝² = b✝
a✝ : Rel (fun x1 x2 ↦ x1 = x2) as✝ bs✝
a_ih✝ : as✝ = bs✝
⊢ a✝² ::ₘ as✝ = b✝ ::ₘ bs✝
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case nil
α : Type u
⊢ (∀ (a : α), ¬[a, a] <+ []) → [].Nodup

pp: case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ (a : α), ¬[a, a] <+ tail✝) → tail✝.Nodup
⊢ (∀ (a : α), ¬[a, a] <+ head✝ :: tail✝) → (head✝ :: tail✝).Nodup

Tactic:
<;>

Goal state after:
case nil
α : Type u
⊢ (∀ (a : α), ¬[a, a] <+ []) → [].Nodup

case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ (a : α), ¬[a, a] <+ tail✝) → tail✝.Nodup
⊢ (∀ (a : α), ¬[a, a] <+ head✝ :: tail✝) → (head✝ :: tail✝).Nodup
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case zero
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
⊢ card 0 = card 0

pp: case cons
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
a✝² : α
b✝ : β
as✝ : Multiset α
bs✝ : Multiset β
a✝¹ : r a✝² b✝
a✝ : Rel r as✝ bs✝
a_ih✝ : as✝.card = bs✝.card
⊢ (a✝² ::ₘ as✝).card = (b✝ ::ₘ bs✝).card

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
⊢ card 0 = card 0

case cons
α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
a✝² : α
b✝ : β
as✝ : Multiset α
bs✝ : Multiset β
a✝¹ : r a✝² b✝
a✝ : Rel r as✝ bs✝
a_ih✝ : as✝.card = bs✝.card
⊢ (a✝² ::ₘ as✝).card = (b✝ ::ₘ bs✝).card
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case e'_2
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ a) = List.count a (l.erase a)

pp: case e'_3
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a ⟦l⟧ = List.count a l

Tactic:
<;>

Goal state after:
case e'_2
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ a) = List.count a (l.erase a)

case e'_3
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a ⟦l⟧ = List.count a l
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case e'_2
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ a) = count a ↑(l.erase a)

pp: case e'_3
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a ⟦l⟧ = count a ↑l

Tactic:
<;>

Goal state after:
case e'_2
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ a) = count a ↑(l.erase a)

case e'_3
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a ⟦l⟧ = count a ↑l
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case e'_2
α : Type u_1
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ b) = List.count a (l.erase b)

pp: case e'_3
α : Type u_1
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a ⟦l⟧ = List.count a l

Tactic:
<;>

Goal state after:
case e'_2
α : Type u_1
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ b) = List.count a (l.erase b)

case e'_3
α : Type u_1
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a ⟦l⟧ = List.count a l
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case e'_2
α : Type u_1
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ b) = count a ↑(l.erase b)

pp: case e'_3
α : Type u_1
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a ⟦l⟧ = count a ↑l

Tactic:
<;>

Goal state after:
case e'_2
α : Type u_1
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ b) = count a ↑(l.erase b)

case e'_3
α : Type u_1
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
s : Multiset α
l : List α
⊢ count a ⟦l⟧ = count a ↑l
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ ∀ (a_1 b : List α), count a (⟦a_1⟧ - ⟦b⟧) = count a ⟦a_1⟧ - count a ⟦b⟧

Tactic:
by simp [List.count_diff]

Goal state after:
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case nil
α : Type u
hne : [] ≠ []
hnd : [].Nodup
⊢ [].head hne = [].getLast hne ↔ ∃ x, [] = [x]

pp: case cons
α : Type u
head✝ : α
tail✝ : List α
hne : head✝ :: tail✝ ≠ []
hnd : (head✝ :: tail✝).Nodup
⊢ (head✝ :: tail✝).head hne = (head✝ :: tail✝).getLast hne ↔ ∃ x, head✝ :: tail✝ = [x]

Tactic:
<;>

Goal state after:
case nil
α : Type u
hne : [] ≠ []
hnd : [].Nodup
⊢ [].head hne = [].getLast hne ↔ ∃ x, [] = [x]

case cons
α : Type u
head✝ : α
tail✝ : List α
hne : head✝ :: tail✝ ≠ []
hnd : (head✝ :: tail✝).Nodup
⊢ (head✝ :: tail✝).head hne = (head✝ :: tail✝).getLast hne ↔ ∃ x, head✝ :: tail✝ = [x]
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: case isTrue
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
a✝ : α
h✝ : a✝ = a
⊢ count a✝ s - 1 = count a✝ (s.erase a)

pp: case isFalse
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
a✝ : α
h✝ : ¬a✝ = a
⊢ count a✝ s - 0 = count a✝ (s.erase a)

Tactic:
<;>

Goal state after:
case isTrue
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
a✝ : α
h✝ : a✝ = a
⊢ count a✝ s - 1 = count a✝ (s.erase a)

case isFalse
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
a✝ : α
h✝ : ¬a✝ = a
⊢ count a✝ s - 0 = count a✝ (s.erase a)
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case left
α : Type u
l : List α
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : l.Nodup
h' : ¬a ∈ l
⊢ ¬a ∈ l

pp: case right
α : Type u
l : List α
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : l.Nodup
h' : ¬a ∈ l
⊢ l.Nodup

Tactic:
<;>

Goal state after:
case left
α : Type u
l : List α
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : l.Nodup
h' : ¬a ∈ l
⊢ ¬a ∈ l

case right
α : Type u
l : List α
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : l.Nodup
h' : ¬a ∈ l
⊢ l.Nodup
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: case mp
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
⊢ map f s = {b} → ∃ a, s = {a} ∧ f a = b

Tactic:
intro h
    obtain ⟨a, ha⟩ : ∃ a, s = {a} := by rw [← card_eq_one, ← card_map, h, card_singleton]
    refine ⟨a, ha, ?_⟩
    rw [← mem_singleton, ← h, ha, map_singleton, mem_singleton]

Goal state after: