mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.CompleteLattice.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
⊢ max a b = if a ≤ b then b else a

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
h : a ≤ b
⊢ max a b = b

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
h : ¬a ≤ b
⊢ max a b = a
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
p : ι → Prop
f : (i : ι) → p i → α
a : α
h : ∃ i, p i
⊢ a ⊔ ⨆ i, ⨆ (h : p i), f i h = ⨆ i, ⨆ (h : p i), a ⊔ f i h

Tactic:
simpa only [sup_comm] using @biSup_sup α _ _ p _ _ h

Goal state after:
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
i : ι
⊢ (if h : p i then f i h else g i h) = (⨆ (h : p i), f i h) ⊔ ⨆ (h : ¬p i), g i h

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
i : ι
h : p i
⊢ f i h = (⨆ (h : p i), f i h) ⊔ ⨆ (h : ¬p i), g i h

case neg
α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
p : ι → Prop
inst✝ : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
i : ι
h : ¬p i
⊢ g i h = (⨆ (h : p i), f i h) ⊔ ⨆ (h : ¬p i), g i h
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
⊢ ↑(sInf s) =
    if (fun a ↦ ↑a) '' s ⊆ {⊤} ∨ ¬BddBelow ((fun a ↦ ↑a) '' s) then ⊤ else ↑(sInf ((fun a ↦ ↑a) ⁻¹' (fun a ↦ ↑a) '' s))

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h : (fun a ↦ ↑a) '' s ⊆ {⊤} ∨ ¬BddBelow ((fun a ↦ ↑a) '' s)
⊢ ↑(sInf s) = ⊤

case neg
α : Type u_1
inst✝¹ : Preorder α
inst✝ : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h : ¬((fun a ↦ ↑a) '' s ⊆ {⊤} ∨ ¬BddBelow ((fun a ↦ ↑a) '' s))
⊢ ↑(sInf s) = ↑(sInf ((fun a ↦ ↑a) ⁻¹' (fun a ↦ ↑a) '' s))
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
⊢ ⊤ ∈ upperBounds s

Tactic:
intro _ _
      exact le_top

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : ¬BddAbove ((fun a ↦ ↑a) ⁻¹' s)
⊢ ⊤ ∈ upperBounds s

Tactic:
intro _ _
      exact le_top

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case left
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ (if s ⊆ {⊤} then ⊤ else ↑(sInf ((fun a ↦ ↑a) ⁻¹' s))) ∈ lowerBounds s

Tactic:
split_ifs with h

Goal state after:
case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
⊢ ⊤ ∈ lowerBounds s

case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s)) ∈ lowerBounds s
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case right
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ (if s ⊆ {⊤} then ⊤ else ↑(sInf ((fun a ↦ ↑a) ⁻¹' s))) ∈ upperBounds (lowerBounds s)

Tactic:
split_ifs with h

Goal state after:
case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
⊢ ⊤ ∈ upperBounds (lowerBounds s)

case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s)) ∈ upperBounds (lowerBounds s)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : s ⊆ {⊤}
⊢ ⊤ ∈ upperBounds (lowerBounds s)

Tactic:
intro _ _
      exact le_top

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

Goal state before:
pp: α : Type u
β : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : CommMonoid β
inst✝ : Preorder β
f : β → α
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a b : β
ab : a ≤ b
c : β
⊢ f (a * c) ≤ f (b * c)

Tactic:
by rw [mul, mul]; grw [le.2 ab]

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
hf : Injective f
x : ι
hx : x ∈ mulSupport g
⊢ extend f g 1 (f x) ≠ 1

Tactic:
hf.extend_apply

Goal state after:
ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
hf : Injective f
x : ι
hx : x ∈ mulSupport g
⊢ g x ≠ 1
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : One M
i : ι
a : M
inst✝ : DecidableEq M
⊢ mulSupport (mulSingle i a) = if a = 1 then ∅ else {i}

Tactic:
split_ifs with h

Goal state after:
case pos
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : One M
i : ι
a : M
inst✝ : DecidableEq M
h : a = 1
⊢ mulSupport (mulSingle i a) = ∅

case neg
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : One M
i : ι
a : M
inst✝ : DecidableEq M
h : ¬a = 1
⊢ mulSupport (mulSingle i a) = {i}
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : One M
i : ι
a : M
⊢ (if a = 1 then ∅ else {i}).Subsingleton

Tactic:
split_ifs with h

Goal state after:
case pos
ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : One M
i : ι
a : M
h : a = 1
⊢ ∅.Subsingleton

case neg
ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : One M
i : ι
a : M
h : ¬a = 1
⊢ {i}.Subsingleton
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: i n : ℕ
n1 : 1 ≤ n
⊢ i + n ! ≤ (i + n)!

Tactic:
rcases n1 with - | @h

Goal state after:
case refl
i : ℕ
⊢ i + 1! ≤ (i + 1)!

case step
i h : ℕ
a✝ : Nat.le 1 h
⊢ i + h.succ ! ≤ (i + h.succ)!
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + 1 + k) * (n + k)! = (n + k + 1) * (n + k)!

Tactic:
Nat.add_right_comm

Goal state after:
n k : ℕ
⊢ (n + k + 1) * (n + k)! = (n + k + 1) * (n + k)!
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case succ
l k n' : ℕ
⊢ (n' + l)! * (n' + (1 + l)).ascFactorial k = (n' + (l + k))!

Tactic:
rw [Nat.add_comm 1 l, ← Nat.add_assoc, factorial_mul_ascFactorial, Nat.add_assoc]

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + k + 1) * (n + 1).ascFactorial k = (n + 1 + k) * (n + 1).ascFactorial k

Tactic:
Nat.add_right_comm

Goal state after:
n k : ℕ
⊢ (n + 1 + k) * (n + 1).ascFactorial k = (n + 1 + k) * (n + 1).ascFactorial k
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ 2 ^ n * n ! ≤ (2 * n)!

Tactic:
obtain _ | n := n

Goal state after:
case zero
⊢ 2 ^ 0 * 0! ≤ (2 * 0)!

case succ
n : ℕ
⊢ 2 ^ (n + 1) * (n + 1)! ≤ (2 * (n + 1))!
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case succ
n : ℕ
⊢ (n + 1)! * 2 ^ (n + 1) ≤ (n + 1 + (n + 1))!

Tactic:
calc
    _ ≤ (n + 1)! * (n + 2) ^ (n + 1) :=
      Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (le_add_left _ _) _)
    _ ≤ _ := Nat.factorial_mul_pow_le_factorial

Goal state after:
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ n.descFactorial k = if n < k then 0 else (n - k + 1).ascFactorialBinary k

Tactic:
split_ifs with h

Goal state after:
case pos
n k : ℕ
h : n < k
⊢ n.descFactorial k = 0

case neg
n k : ℕ
h : ¬n < k
⊢ n.descFactorial k = (n - k + 1).ascFactorialBinary k
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ (if 2 * fract x < 1 then ⌊x⌋ + ⌊fract x⌋ else ⌈↑⌊x⌋ + fract x⌉) = (⌊2 * ↑⌊x⌋ + 2 * fract x⌋ + 1) / 2

Tactic:
← Int.cast_ofNat,

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ (if ↑2 * fract x < 1 then ⌊x⌋ + ⌊fract x⌋ else ⌈↑⌊x⌋ + fract x⌉) = (⌊↑2 * ↑⌊x⌋ + ↑2 * fract x⌋ + 1) / 2
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ (if 2 * fract x < 1 then ⌊x⌋ + ⌊fract x⌋ else ⌊x⌋ + ⌈fract x⌉) = ⌊x⌋ + (⌊2 * fract x⌋ + 1) / 2

Tactic:
split_ifs with h

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.Data.PNat.Basic

Goal state before:
pp: a b : ℕ+
⊢ ↑(↑a - ↑b).toPNat' = if b < a then ↑a - ↑b else 1

Tactic:
split_ifs with h

Goal state after:
case pos
a b : ℕ+
h : b < a
⊢ ↑(↑a - ↑b).toPNat' = ↑a - ↑b

case neg
a b : ℕ+
h : ¬b < a
⊢ ↑(↑a - ↑b).toPNat' = 1
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: a b : ℕ+
⊢ (if b < a then ↑a - ↑b else 1) ≤ ↑a

Tactic:
split_ifs with h

Goal state after:
case pos
a b : ℕ+
h : b < a
⊢ ↑a - ↑b ≤ ↑a

case neg
a b : ℕ+
h : ¬b < a
⊢ 1 ≤ ↑a
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: a b : ℕ+
hab : a < b
⊢ ↑a ≤ if 1 < b then ↑b - ↑1 else 1

Tactic:
split_ifs with h

Goal state after:
case pos
a b : ℕ+
hab : a < b
h : 1 < b
⊢ ↑a ≤ ↑b - ↑1

case neg
a b : ℕ+
hab : a < b
h : ¬1 < b
⊢ ↑a ≤ 1
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: m k : ℕ+
⊢ (if ↑m % ↑k = 0 then ↑k else ↑m % ↑k) ≤ ↑m ∧ (if ↑m % ↑k = 0 then ↑k else ↑m % ↑k) ≤ ↑k

Tactic:
split_ifs with h

Goal state after:
case pos
m k : ℕ+
h : ↑m % ↑k = 0
⊢ ↑k ≤ ↑m ∧ ↑k ≤ ↑k

case neg
m k : ℕ+
h : ¬↑m % ↑k = 0
⊢ ↑m % ↑k ≤ ↑m ∧ ↑m % ↑k ≤ ↑k
Module: Mathlib.Algebra.Order.Floor.Ring

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

Tactic:
refine (ceil_lt_add_one _).le.trans ?_

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ b + 1 ≤ ↑⌈a + b⌉ + 1 - a
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
r : α
n d : ℕ
⊢ IsNNRat r n d → IsNNRat (fract r) (n % d) d

Tactic:
by
  rintro ⟨inv, rfl⟩
  refine ⟨inv, ?_⟩
  simp only [invOf_eq_inv, ← div_eq_mul_inv, fract_div_natCast_eq_div_natCast_mod]

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

Goal state before:
pp: case h
K : Type u_4
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
ε : K
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ 1 < ε * (↑n + 1)

pp: case h
K : Type u_4
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
ε : K
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ 0 < ↑n + 1

Tactic:
← div_lt_iff₀' hε

Goal state after:
case h
K : Type u_4
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
ε : K
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ 1 / ε < ↑n + 1

case h
K : Type u_4
inst✝³ : Semifield K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
ε : K
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ 0 < ↑n + 1
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha : 2⁻¹ < a
⊢ ↑⌈(2 - 1)⁻¹⌉ / 2 < a

Tactic:
by norm_num at ha ⊢; exact ha

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

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

Tactic:
by norm_num at ha ⊢; exact ha

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn✝ : 1 ≤ n
hy : R (f (l + n • a)) (f y)
hn : 1 < n
k : ℤ
⊢ R (f (l + k • a)) (f (l + (1 + k) • a))

Tactic:
add_zsmul,

Goal state after:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn✝ : 1 ≤ n
hy : R (f (l + n • a)) (f y)
hn : 1 < n
k : ℤ
⊢ R (f (l + k • a)) (f (l + (1 • a + k • a)))
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
rcases le_or_gt a 0 with ha | ha
  · obtain ⟨n, hn⟩ := exists_pow_lt_of_lt_one hb₀ hc₁
    exact ⟨n, ha.trans_lt (zpow_pos hc₀ _), mod_cast hn⟩
  · rcases le_or_gt b 1 with hb₁ | hb₁
    · obtain ⟨n, hn⟩ := exists_pow_btwn_of_lt_mul h hb₀ hb₁ hc₀ hc₁
      exact ⟨n, mod_cast hn⟩
    · rcases lt_or_ge a 1 with ha₁ | ha₁
      · refine ⟨0, ?_⟩
        rw [zpow_zero]
        exact ⟨ha₁, hb₁⟩
      · have : b⁻¹ < a⁻¹ * c := by rwa [lt_inv_mul_iff₀' ha, inv_mul_lt_iff₀ hb₀]
        obtain ⟨n, hn₁, hn₂⟩ :=
          exists_pow_btwn_of_lt_mul this (inv_pos_of_pos ha) (inv_le_one_of_one_le₀ ha₁) hc₀ hc₁
        refine ⟨-n, ?_, ?_⟩
        · rwa [lt_inv_comm₀ (pow_pos hc₀ n) ha, ← zpow_natCast, ← zpow_neg] at hn₂
        · rwa [inv_lt_comm₀ hb₀ (pow_pos hc₀ n), ← zpow_natCast, ← zpow_neg] at hn₁

Goal state after:
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 * δ

Tactic:
rw [← div_le_iff₀ δ_pos]

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
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
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:
rw [← div_le_iff₀ δ_pos]

Goal state after:
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.Data.Multiset.Count

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
_l : List α
⊢ countP p (Quot.mk (⇑(isSetoid α)) _l) = 0 ↔ ∀ (a : α), a ∈ Quot.mk (⇑(isSetoid α)) _l → ¬p a

Tactic:
simp [List.countP_eq_zero]

Goal state after:
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
d : s.Nodup
⊢ count a s = if a ∈ s then 1 else 0

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
d : s.Nodup
h : a ∈ s
⊢ count a s = 1

case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
d : s.Nodup
h : ¬a ∈ s
⊢ count a s = 0
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
b : Multiset β
⊢ Rel r 0 b ↔ b = 0

Tactic:
by rw [rel_iff]; simp

Goal state after:
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
a : Multiset α
⊢ Rel r a 0 ↔ a = 0

Tactic:
by rw [rel_iff]; simp

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

Goal state before:
pp: α : Type u
β : Type v
l : List α
f : α → Option β
h : ∀ (a a' : α) (b : β), b ∈ f a → b ∈ f a' → a = a'
a a' : α
n : a ≠ a'
b : β
bm : f a = some b
b' : β
bm' : f a' = some b'
e : b = b'
⊢ b' ∈ f a

Tactic:
rw [← e]

Goal state after:
α : Type u
β : Type v
l : List α
f : α → Option β
h : ∀ (a a' : α) (b : β), b ∈ f a → b ∈ f a' → a = a'
a a' : α
n : a ≠ a'
b : β
bm : f a = some b
b' : β
bm' : f a' = some b'
e : b = b'
⊢ b ∈ f a
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ ∀ {x y z : α}, x ≠ z → x ≠ y ∨ y ≠ z

Tactic:
intro x y z xz
    exact not_and_or.1 <| mt (fun h ↦ h.1.trans h.2) xz

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
inst✝ : DecidableEq α
h : l₁.Nodup
x : α
⊢ List.count x (l₁.bagInter l₂) ≤ 1

Tactic:
grind [List.count_bagInter]

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
inst✝ : DecidableEq α
h : l₂.Nodup
x : α
⊢ List.count x (l₁.bagInter l₂) ≤ 1

Tactic:
grind [List.count_bagInter]

Goal state after:
Module: Mathlib.Data.Multiset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ s ≤ s ∧ s.Nodup ↔ s.Nodup

Tactic:
and_iff_right le_rfl

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ s.Nodup ↔ s.Nodup
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ filter p (a ::ₘ s) = (if p a then {a} else 0) + filter p s

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
⊢ filter p (a ::ₘ s) = {a} + filter p s

case neg
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : ¬p a
⊢ filter p (a ::ₘ s) = 0 + filter p s
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ count a (filter p s) = if p a then count a s else 0

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : p a
⊢ count a (filter p s) = count a s

case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : ¬p a
⊢ count a (filter p s) = 0
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
t : Multiset α
ht : ndinsert a s = t
h : a ∈ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)

Tactic:
rw [ndinsert_of_mem h] at ht

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
t : Multiset α
ht✝ : ndinsert a s = t
ht : s = t
h : a ∈ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)
Module: Mathlib.Data.Finset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
⊢ (filter p s).Nonempty ↔ ∃ a, a ∈ s ∧ p a

Tactic:
by
  simp only [nonempty_iff_ne_empty, Ne, filter_eq_empty_iff, Classical.not_not, not_forall,
    exists_prop]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ s = t ∪ s ↔ t ⊆ s

Tactic:
rw [eq_comm, union_eq_right]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ {a} ∩ s = if a ∈ s then {a} else ∅

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ {a} ∩ s = {a}

case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ {a} ∩ s = ∅
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ s ∩ {a} = if a ∈ s then {a} else ∅

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ s ∩ {a} = {a}

case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ s ∩ {a} = ∅
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α ↪ β
a : α
s : Finset α
⊢ map f (insert a s) = insert (f a) (map f s)

Tactic:
by
  simp only [insert_eq, map_union, map_singleton]

Goal state after:
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
b : β
⊢ b ∈ image f s ↔ ∃ a ∈ s, f a = b

Tactic:
simp only [mem_def, image_val, mem_dedup, Multiset.mem_map]

Goal state after:
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset { a // p a }
⊢ (fun s ↦ Finset.map (Subtype.impEmbedding (Membership.mem ↑s) p ⋯) (↑s).attach)
      ((fun s ↦ ⟨Finset.map { toFun := fun a ↦ ↑a, inj' := ⋯ } s, ⋯⟩) s) =
    s

Tactic:
ext a; constructor <;> intro h <;>
    simp only [Finset.mem_map, Finset.mem_attach, true_and, Subtype.exists, Embedding.coeFn_mk,
      exists_and_right, exists_eq_right, Subtype.impEmbedding] at * <;>
    grind

Goal state after:
Module: Mathlib.Data.Fin.Embedding

Goal state before:
pp: case succ
n : ℕ
ihn : ∀ {m : ℕ}, Nonempty (Fin n ↪ Fin m) → n ≤ m
m : ℕ
e : Fin (n + 1) ↪ Fin m.succ
⊢ Fin n ↪ Fin m

Tactic:
refine ⟨fun i ↦ (e.setValue 0 0 i.succ).pred (mt e.setValue_eq_iff.1 i.succ_ne_zero),
      fun i j h ↦ ?_⟩

Goal state after:
case succ
n : ℕ
ihn : ∀ {m : ℕ}, Nonempty (Fin n ↪ Fin m) → n ≤ m
m : ℕ
e : Fin (n + 1) ↪ Fin m.succ
i j : Fin n
h : (fun i ↦ ((e.setValue 0 0) i.succ).pred ⋯) i = (fun i ↦ ((e.setValue 0 0) i.succ).pred ⋯) j
⊢ i = j
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
⊢ Monotone card

Tactic:
by apply card_le_card

Goal state after:
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : #(image f s) = #s
⊢ Set.InjOn f ↑s

Tactic:
by
  rw [card_def, card_def, image, toFinset] at H
  dsimp only at H
  have : (s.1.map f).dedup = s.1.map f := by
    refine Multiset.eq_of_le_of_card_le (Multiset.dedup_le _) ?_
    simp only [H, Multiset.card_map, le_rfl]
  rw [Multiset.dedup_eq_self] at this
  exact inj_on_of_nodup_map this

Goal state after:
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ 0 = ⊤ ↔ n = 1

Tactic:
by
  rw [← bot_eq_zero, subsingleton_iff_bot_eq_top, subsingleton_iff_le_one,
    le_one_iff_eq_zero_or_eq_one, or_iff_right (NeZero.ne n)]

Goal state after: