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

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommMonoidWithZero α
a✝ b : α
n : ℕ
a c : α
hc : c ≠ 0
hab : a ≤ a
⊢ a * c ≤ a * c

pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommMonoidWithZero α
a✝ b✝ : α
n : ℕ
a b : α
hab✝ : a ≤ b
c : α
hc : c ≠ 0
hab : a < b
⊢ a * c ≤ b * c

Tactic:
· simp

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrderedCommMonoidWithZero α
a✝ b✝ : α
n : ℕ
a b : α
hab✝ : a ≤ b
c : α
hc : c ≠ 0
hab : a < b
⊢ a * c ≤ b * c
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: m✝¹ n✝ k✝ : ℕ
p q : ℕ → Prop
inst✝ : DecidablePred p
H : ∃ n, p n
n : ℕ
pn : p n
m✝ m : ℕ
IH : ∀ (k : ℕ), n ≤ k + m → Acc lbp k
k : ℕ
kn : n ≤ k + m.succ
y : ℕ
r : y.lbp k
_a : ∀ (k_1 : ℕ), k_1 ≤ k → ¬p k_1
⊢ n ≤ k + 1 + m

Tactic:
rw [Nat.add_right_comm]; exact kn

Goal state after:
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: m : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ Nat.find h = m ↔ p m ∧ ∀ (n : ℕ), n < m → ¬p n

Tactic:
constructor
  · grind [Nat.find_min]
  · rintro ⟨hm, hlt⟩
    have := Nat.find_min' h hm
    grind

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

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

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

Tactic:
· simp

Goal state after:
case coe
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a b✝ : α
inst✝¹ : Add α
inst✝ : ExistsAddOfLE α
b : WithZero α
a✝ : α
⊢ ↑a✝ ≤ b → ∃ c, b = ↑a✝ + c
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:
· simp

Goal state after:
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
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
M : Type u_1
N : Type u_2
inst✝¹ : One M
inst✝ : One N
f : OneHom M N
⊢ map (⇑f) 1 = 1

Tactic:
by rw [WithBot.map_one, map_one, coe_one]

Goal state after:
Module: Mathlib.Data.Int.LeastGreatest

Goal state before:
pp: P : ℤ → Prop
inst✝ : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
Hb' : ∀ (z : ℤ), P z → b' ≤ z
Hinh : ∃ z, P z
⊢ ↑(b.leastOfBdd Hb Hinh) = ↑(b'.leastOfBdd Hb' Hinh)

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Int.LeastGreatest

Goal state before:
pp: P : ℤ → Prop
inst✝ : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hb' : ∀ (z : ℤ), P z → z ≤ b'
Hinh : ∃ z, P z
⊢ ↑(b.greatestOfBdd Hb Hinh) = ↑(b'.greatestOfBdd Hb' Hinh)

Tactic:
by grind

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

Goal state before:
pp: α : Type u_2
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : FloorSemiring α
n : ℕ
⊢ 0 ≤ ↑n

Tactic:
simpa using natCast_mono n.zero_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:
· simp

Goal state after:
case inr
x : WithZero (Multiplicative ℤ)
y : Multiplicative ℤ
hx : x ≠ 0
⊢ x < ↑y * exp 1 ↔ x ≤ ↑y
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

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

Tactic:
rw [← log_le_log, ← log_lt_log] <;> simp [log_mul, Int.lt_add_one_iff]

Goal state after:
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:
· simp

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: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
⊢ ⌊a⌋₊ = 0 ↔ a < 1

Tactic:
rw [← lt_one_iff, ← @cast_one R]
  exact floor_lt' Nat.one_ne_zero

Goal state after:
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:
· simp

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 ≤ 0
Module: Mathlib.Algebra.Order.Floor.Semiring

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

Tactic:
by
  rw [Nat.cast_comm, mul_cast_floor_div_cancel hn]

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
⊢ a ≤ ↑(⌊a⌋₊ + 1)

Tactic:
Nat.cast_add,

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
⊢ a ≤ ↑⌊a⌋₊ + ↑1
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
x✝ : ℕ
⊢ x✝ ∈ Nat.cast ⁻¹' Iio a ↔ x✝ ∈ Iio ⌈a⌉₊

Tactic:
simp [lt_ceil]

Goal state after:
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 d : ℕ
hb : n ≤ n + d
⊢ ↑(n + d) ≤ a + ↑n ↔ n + d ≤ ⌊a⌋₊ + n

Tactic:
Nat.cast_add,

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 d : ℕ
hb : n ≤ n + d
⊢ ↑n + ↑d ≤ a + ↑n ↔ n + d ≤ ⌊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
b d : ℕ
hb : b ≤ b + d
⊢ ↑b ≤ a + ↑(b + d) ↔ b ≤ ⌊a⌋₊ + (b + d)

Tactic:
Nat.cast_add,

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
b d : ℕ
hb : b ≤ b + d
⊢ ↑b ≤ a + (↑b + ↑d) ↔ b ≤ ⌊a⌋₊ + (b + d)
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 d : ℕ
hb : n ≤ n + d
⊢ ↑(n + d) < a + ↑n ↔ n + d < ⌈a⌉₊ + n

Tactic:
Nat.cast_add,

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 d : ℕ
hb : n ≤ n + d
⊢ ↑n + ↑d < a + ↑n ↔ n + d < ⌈a⌉₊ + n
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder R
inst✝⁵ : FloorSemiring R
a : R
S : Type u_3
inst✝⁴ : Semiring S
inst✝³ : LinearOrder S
inst✝² : FloorSemiring S
b : S
inst✝¹ : IsStrictOrderedRing R
inst✝ : IsStrictOrderedRing S
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
h₀ : 0 ≤ a ↔ 0 ≤ b
⊢ ⌊a⌋₊ = ⌊b⌋₊

Tactic:
obtain ha | ha := lt_or_ge a 0

Goal state after:
case inl
R : Type u_1
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder R
inst✝⁵ : FloorSemiring R
a : R
S : Type u_3
inst✝⁴ : Semiring S
inst✝³ : LinearOrder S
inst✝² : FloorSemiring S
b : S
inst✝¹ : IsStrictOrderedRing R
inst✝ : IsStrictOrderedRing S
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
h₀ : 0 ≤ a ↔ 0 ≤ b
ha : a < 0
⊢ ⌊a⌋₊ = ⌊b⌋₊

case inr
R : Type u_1
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder R
inst✝⁵ : FloorSemiring R
a : R
S : Type u_3
inst✝⁴ : Semiring S
inst✝³ : LinearOrder S
inst✝² : FloorSemiring S
b : S
inst✝¹ : IsStrictOrderedRing R
inst✝ : IsStrictOrderedRing S
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
h₀ : 0 ≤ a ↔ 0 ≤ b
ha : 0 ≤ a
⊢ ⌊a⌋₊ = ⌊b⌋₊
Module: Mathlib.Order.WithBot

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : LT α
inst✝ : NoMaxOrder α
h : DenselyOrdered (WithTop α)
a b : α
hab : a < b
c : WithTop α
hc : ↑a < c ∧ c < ↑b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
induction c with
    | top => simp at hc
    | coe c => exact ⟨c, by simpa using hc⟩

Goal state after:
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
a b : R
inst✝¹ : Invertible a
inst✝ : Invertible b
⊢ -(b + a) = a * ⅟b * a → -a = b + a * ⅟b * a

Tactic:
by grind

Goal state after:
Module: Mathlib.Algebra.Ring.Invertible

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
a b : R
inst✝¹ : Invertible a
inst✝ : Invertible b
⊢ -a = b + a * ⅟b * a ↔ -a = a * ⅟a * b + a * ⅟b * a

Tactic:
rw [mul_invOf_self, one_mul]

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

Goal state before:
pp: case inl
G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeInf G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
hc : 0 ≤ 0
⊢ 0 * (a ⊓ b) = 0 * a ⊓ 0 * b

pp: case inr
G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeInf G₀
inst✝ : PosMulReflectLT G₀
c : G₀
hc✝ : 0 ≤ c
a b : G₀
hc : 0 < c
⊢ c * (a ⊓ b) = c * a ⊓ c * b

Tactic:
· simp

Goal state after:
case inr
G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeInf G₀
inst✝ : PosMulReflectLT G₀
c : G₀
hc✝ : 0 ≤ c
a b : G₀
hc : 0 < c
⊢ c * (a ⊓ b) = c * a ⊓ c * b
Module: Mathlib.Algebra.Order.GroupWithZero.OrderIso

Goal state before:
pp: case inl
G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeSup G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
hc : 0 ≤ 0
⊢ 0 * (a ⊔ b) = 0 * a ⊔ 0 * b

pp: case inr
G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeSup G₀
inst✝ : PosMulReflectLT G₀
c : G₀
hc✝ : 0 ≤ c
a b : G₀
hc : 0 < c
⊢ c * (a ⊔ b) = c * a ⊔ c * b

Tactic:
· simp

Goal state after:
case inr
G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeSup G₀
inst✝ : PosMulReflectLT G₀
c : G₀
hc✝ : 0 ≤ c
a b : G₀
hc : 0 < c
⊢ c * (a ⊔ b) = c * a ⊔ c * b
Module: Mathlib.Algebra.Order.GroupWithZero.OrderIso

Goal state before:
pp: case inl
G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeInf G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
hc : 0 ≤ 0
⊢ (a ⊓ b) * 0 = a * 0 ⊓ b * 0

pp: case inr
G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeInf G₀
inst✝ : MulPosReflectLT G₀
c : G₀
hc✝ : 0 ≤ c
a b : G₀
hc : 0 < c
⊢ (a ⊓ b) * c = a * c ⊓ b * c

Tactic:
· simp

Goal state after:
case inr
G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeInf G₀
inst✝ : MulPosReflectLT G₀
c : G₀
hc✝ : 0 ≤ c
a b : G₀
hc : 0 < c
⊢ (a ⊓ b) * c = a * c ⊓ b * c
Module: Mathlib.Algebra.Order.GroupWithZero.OrderIso

Goal state before:
pp: case inl
G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeSup G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
hc : 0 ≤ 0
⊢ (a ⊔ b) * 0 = a * 0 ⊔ b * 0

pp: case inr
G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeSup G₀
inst✝ : MulPosReflectLT G₀
c : G₀
hc✝ : 0 ≤ c
a b : G₀
hc : 0 < c
⊢ (a ⊔ b) * c = a * c ⊔ b * c

Tactic:
· simp

Goal state after:
case inr
G₀ : Type u_1
inst✝² : GroupWithZero G₀
inst✝¹ : SemilatticeSup G₀
inst✝ : MulPosReflectLT G₀
c : G₀
hc✝ : 0 ≤ c
a b : G₀
hc : 0 < c
⊢ (a ⊔ b) * c = a * c ⊔ b * c
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝ : DivisionRing K
⊢ 0⁻¹ = 0 ↔ 0 = -1 ∨ 0 = 0 ∨ 0 = 1

pp: case inr
K : Type u_1
inst✝ : DivisionRing K
a : K
ha : a ≠ 0
⊢ a⁻¹ = a ↔ a = -1 ∨ a = 0 ∨ a = 1

Tactic:
· simp

Goal state after:
case inr
K : Type u_1
inst✝ : DivisionRing K
a : K
ha : a ≠ 0
⊢ a⁻¹ = a ↔ a = -1 ∨ a = 0 ∨ a = 1
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : NeZero 2
a : K
⊢ a - a / 2 = a / 2

Tactic:
sub_eq_iff_eq_add,

Goal state after:
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : NeZero 2
a : K
⊢ a = a / 2 + a / 2
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: u v : ℤ
⊢ u * v = -1 ↔ u = 1 ∧ v = -1 ∨ u = -1 ∧ v = 1

Tactic:
refine ⟨eq_one_or_neg_one_of_mul_eq_neg_one', fun h ↦ Or.elim h (fun H ↦ ?_) fun H ↦ ?_⟩ <;>
    obtain ⟨rfl, rfl⟩ := H

Goal state after:
case refine_1
h : 1 = 1 ∧ -1 = -1 ∨ 1 = -1 ∧ -1 = 1
⊢ 1 * -1 = -1

case refine_2
h : -1 = 1 ∧ 1 = -1 ∨ -1 = -1 ∧ 1 = 1
⊢ -1 * 1 = -1
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
p : γ → Prop
⊢ (∀ (z : γ), z ∈ image2 f s t → p z) ↔ ∀ (x : α), x ∈ s → ∀ (y : β), y ∈ t → p (f x y)

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
p : γ → Prop
⊢ (∃ z, z ∈ image2 f s t ∧ p z) ↔ ∃ x, x ∈ s ∧ ∃ y, y ∈ t ∧ p (f x y)

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → α → β
s t : Set α
hf : ∀ (a b : α), f a b = f b a
⊢ image2 f (s ∪ t) (s ∩ t) ⊆ image2 f s t

Tactic:
rw [image2_comm hf]
  exact image2_inter_union_subset hf

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

Goal state before:
pp: case zero
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
inst✝ : IsOrderedRing α
⊢ |a ^ 0 - b ^ 0| ≤ |a - b| * ↑0 * max |a| |b| ^ (0 - 1)

pp: case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
inst✝ : IsOrderedRing α
n : ℕ
⊢ |a ^ (n + 1) - b ^ (n + 1)| ≤ |a - b| * ↑(n + 1) * max |a| |b| ^ (n + 1 - 1)

Tactic:
· simp

Goal state after:
case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
inst✝ : IsOrderedRing α
n : ℕ
⊢ |a ^ (n + 1) - b ^ (n + 1)| ≤ |a - b| * ↑(n + 1) * max |a| |b| ^ (n + 1 - 1)
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u
ι : Sort x
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
F : ι → (a : α) → π a
⊢ BddAbove (range F) ↔ ∀ (a : α), BddAbove (range fun i ↦ F i a)

Tactic:
simp only [bddAbove_pi, ← range_comp]
  rfl

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
h : n < l.length
⊢ take 1 (drop n l) = [l.get ⟨n, h⟩]

Tactic:
by
  rw [drop_eq_getElem_cons h, take, take]
  simp

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

Goal state before:
pp: α : Type u
x : List α
n : ℕ
⊢ take n x = x → x.length ≤ n

Tactic:
by grind

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

Goal state before:
pp: α : Type u
i j : ℕ
hj : 0 < j
xs : List α
hi : i < xs.length
⊢ (dropSlice i j xs).length < xs.length

Tactic:
by grind

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

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
⊢ 1 - 2⁻¹ = 2⁻¹

Tactic:
sub_eq_iff_eq_add,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
a2 : 2 ≤ a
⊢ 1 = 2⁻¹ + 2⁻¹
Module: Mathlib.Data.List.InsertIdx

Goal state before:
pp: α : Type u
β : Type v
f : α → β
l : List α
n : ℕ
a : α
⊢ map f (l.insertIdx n a) = (map f l).insertIdx n (f a)

Tactic:
by
  simpa only [pmap_eq_map] using (insertIdx_pmap (fun a _ ↦ f a) (fun _ _ ↦ trivial) trivial).symm

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

Goal state before:
pp: α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
hl : ∀ (a : α), a ∈ l → p a
n✝ : ℕ
a : α
as : List α
h✝ : ∀ (a_1 : α), a_1 ∈ a :: as → p a_1
h : p a ∧ ∀ (x : α), x ∈ as → p x
n : ℕ
⊢ (pmap f (a :: as) h✝).eraseIdx (n + 1) = pmap f ((a :: as).eraseIdx (n + 1)) ⋯

Tactic:
simp [eraseIdx_pmap f h.2 n]

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

Goal state before:
pp: α : Type u
l : List α
x : α
i j : ℕ
h : i ≤ j
⊢ (take i (l.insertIdx j x)).length = (take i l).length

Tactic:
by grind

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

Goal state before:
pp: α : Type u
l : List α
x : α
i j : ℕ
h : i ≤ j
⊢ ∀ (i_1 : ℕ) (h₁ : i_1 < (take i (l.insertIdx j x)).length) (h₂ : i_1 < (take i l).length),
    (take i (l.insertIdx j x))[i_1] = (take i l)[i_1]

Tactic:
by grind

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

Goal state before:
pp: α : Type u
l : List α
i j : ℕ
h : i ≤ j
⊢ (take i (l.eraseIdx j)).length = (take i l).length

Tactic:
by grind

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

Goal state before:
pp: α : Type u
l : List α
i j : ℕ
h : i ≤ j
⊢ ∀ (i_1 : ℕ) (h₁ : i_1 < (take i (l.eraseIdx j)).length) (h₂ : i_1 < (take i l).length),
    (take i (l.eraseIdx j))[i_1] = (take i l)[i_1]

Tactic:
by grind

Goal state after:
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
x✝ : α
⊢ x✝ ∈ l → x✝ = b ∨ x✝ = a ↔ x✝ ≠ b → x✝ ≠ a → ¬x✝ ∈ l

Tactic:
by rw [← and_imp, ← not_or, not_imp_not]

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

Goal state before:
pp: α : Type u
p : α → Prop
a : α
l : List α
⊢ (∃ x, x ∈ a :: l ∧ p x) → p a ∨ ∃ x, x ∈ l ∧ p x

Tactic:
by grind

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

Goal state before:
pp: α : Type u
p : α → Prop
a : α
l : List α
⊢ (∃ x, x ∈ a :: l ∧ p x) ↔ p a ∨ ∃ x, x ∈ l ∧ p x

Tactic:
by grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
M : Type u_4
inst✝ : Monoid M
head✝ : M
tail✝ : List M
h : (head✝ :: tail✝).prod ≠ 1
⊢ 0 < (head✝ :: tail✝).length

Tactic:
· simp

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

Goal state before:
pp: α : Type u
x : α
hx : x ∈ [].getLast?
⊢ ∃ h, x = [].getLast h

Tactic:
by grind

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

Goal state before:
pp: α : Type u
a x : α
hx : x ∈ [a].getLast?
⊢ ∃ h, x = [a].getLast h

Tactic:
by grind

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

Goal state before:
pp: α : Type u
a b : α
l : List α
x : α
hx : x ∈ (a :: b :: l).getLast?
⊢ ∃ h, x = (a :: b :: l).getLast h

Tactic:
by grind

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
x : α
h : x ∈ l₂.getLast?
⊢ x ∈ (l₁ ++ l₂).getLast?

Tactic:
by grind

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℕ
hn : n ≠ 0
⊢ a ^ ↑n = a ^ n

pp: case hn
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0

Tactic:
· simp

Goal state after:
case hn
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
a d : α
ha : a ∈ l
ha' : a ≠ l.getLastD d
⊢ a ≠ l.getLast ⋯

Tactic:
by grind

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

Goal state before:
pp: α : Type u
l : List α
a : α
ha : a ∈ l
ha' : some a ≠ l.getLast?
⊢ a ≠ l.getLast ⋯

Tactic:
by grind

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

Goal state before:
pp: α : Type u
a : α
l : List α
h : l ≠ []
⊢ (l ++ [a]).tail = l.tail ++ [a]

Tactic:
by grind

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

Goal state before:
pp: case nil
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
⊢ idxOf a [] = 0 ↔ [] = [] ∨ [].head? = some a

pp: case cons
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a head✝ : α
tail✝ : List α
⊢ idxOf a (head✝ :: tail✝) = 0 ↔ head✝ :: tail✝ = [] ∨ (head✝ :: tail✝).head? = some a

Tactic:
· simp

Goal state after:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a head✝ : α
tail✝ : List α
⊢ idxOf a (head✝ :: tail✝) = 0 ↔ head✝ :: tail✝ = [] ∨ (head✝ :: tail✝).head? = some a
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l₁ l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
h : a ∈ l₁
⊢ idxOf a (l₁ ++ l₂) = idxOf a l₁

Tactic:
by grind

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
h : ¬a ∈ l₁
⊢ idxOf a (l₁ ++ l₂) = l₁.length + idxOf a l₂

Tactic:
by grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List M
i : ℕ
hlen : i < l.length
hcomm : ∀ (a' : M), a' ∈ take i l → Commute l[i] a'
⊢ i ≤ (l.eraseIdx i).length

Tactic:
by grind

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

Goal state before:
pp: α : Type u
l : List α
h : l.length = 1
⊢ ∀ (n : ℕ) (h₁ : n < l.length) (h₂ : n < [l.get ⟨0, ⋯⟩].length), l.get ⟨n, h₁⟩ = [l.get ⟨0, ⋯⟩].get ⟨n, h₂⟩

Tactic:
by grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case nil
α : Type u_2
i : ℕ
⊢ take (take i (map length [])).sum [].flatten = (take i []).flatten

pp: case cons
α : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), take (take i (map length tail✝)).sum tail✝.flatten = (take i tail✝).flatten
i : ℕ
⊢ take (take i (map length (head✝ :: tail✝))).sum (head✝ :: tail✝).flatten = (take i (head✝ :: tail✝)).flatten

Tactic:
· simp

Goal state after:
case cons
α : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), take (take i (map length tail✝)).sum tail✝.flatten = (take i tail✝).flatten
i : ℕ
⊢ take (take i (map length (head✝ :: tail✝))).sum (head✝ :: tail✝).flatten = (take i (head✝ :: tail✝)).flatten
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
p : α → Bool
l : List α
⊢ filter p l = foldr (fun a out ↦ bif p a then a :: out else out) [] l

Tactic:
by
  induction l <;> simp [*, filter]; rfl

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case nil
α : Type u_2
i : ℕ
⊢ drop (take i (map length [])).sum [].flatten = (drop i []).flatten

pp: case cons
α : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), drop (take i (map length tail✝)).sum tail✝.flatten = (drop i tail✝).flatten
i : ℕ
⊢ drop (take i (map length (head✝ :: tail✝))).sum (head✝ :: tail✝).flatten = (drop i (head✝ :: tail✝)).flatten

Tactic:
· simp

Goal state after:
case cons
α : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), drop (take i (map length tail✝)).sum tail✝.flatten = (drop i tail✝).flatten
i : ℕ
⊢ drop (take i (map length (head✝ :: tail✝))).sum (head✝ :: tail✝).flatten = (drop i (head✝ :: tail✝)).flatten
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
p : α → Bool
l : List α
a : α
al : a ∈ l
pa : p a = true
⊢ (eraseP p l).length + 1 = l.length

Tactic:
by grind

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

Goal state before:
pp: ι : Type u_1
l : List ι
i : ℕ
h : i < l.length
⊢ (l.eraseIdx i).length + 1 = l.length

Tactic:
by grind

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

Goal state before:
pp: a b c d : ℤ
b0 : 0 < b
d0 : 0 < d
⊢ 0 ≤ c /. d - a /. b ↔ 0 ≤ c * b - a * d

Tactic:
simp [sub_eq_add_neg, ne_of_gt b0, ne_of_gt d0, Int.mul_pos d0 b0]

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

Goal state before:
pp: case inl
a : ℤ
ha : a ≤ 0
⊢ mkRat a 0 ≤ 0

pp: case inr
a : ℤ
ha : a ≤ 0
b : ℕ
hb : b ≠ 0
⊢ mkRat a b ≤ 0

Tactic:
· simp

Goal state after:
case inr
a : ℤ
ha : a ≤ 0
b : ℕ
hb : b ≠ 0
⊢ mkRat a b ≤ 0
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: n₁ n₂ d₁ d₂ : ℕ
⊢ divNat n₁ d₁ * divNat n₂ d₂ = divNat (n₁ * n₂) (d₁ * d₂)

Tactic:
by
  ext; push_cast; exact Rat.divInt_mul_divInt _ _

Goal state after: