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

Goal state before:
pp: p q n : ℕ
dvd : p.gcd q ∣ n
le : p.pred * q.pred ≤ n
⊢ ∃ a b, a * p + b * q = n

Tactic:
by
  obtain _ | p := p
  · have ⟨b, eq⟩ := q.gcd_zero_left ▸ dvd
    exact ⟨0, b, by simpa [mul_comm, eq_comm] using eq⟩
  obtain _ | q := q
  · have ⟨a, eq⟩ := p.gcd_zero_right ▸ dvd
    exact ⟨a, 0, by simpa [mul_comm, eq_comm] using eq⟩
  rw [← Int.gcd_natCast_natCast, Int.gcd_dvd_iff] at dvd
  have ⟨a_n, b_n, eq⟩ := dvd
  let a := a_n % q.succ
  let b := b_n + a_n / q.succ * p.succ
  refine ⟨a.toNat, b.toNat, Nat.cast_injective (R := ℤ) ?_⟩
  have : a * p.succ + b * q.succ = n := by rw [add_mul, ← add_assoc,
    add_right_comm, mul_right_comm, ← add_mul, Int.emod_add_ediv_mul, eq, mul_comm, mul_comm b_n]
  rw [Nat.cast_add, Nat.cast_mul, Nat.cast_mul, Int.natCast_toNat_eq_self.mpr
    (Int.emod_nonneg _ <| by lia), Int.natCast_toNat_eq_self.mpr, this]
  -- show b ≥ 0 by contradiction
  by_contra hb
  replace hb : b ≤ -1 := by lia
  apply lt_irrefl (n : ℤ)
  have ha := Int.emod_lt a_n (by lia : (q.succ : ℤ) ≠ 0)
  rw [p.pred_succ, q.pred_succ] at le
  calc n = a * p.succ + b * q.succ := this.symm
       _ ≤ q * p.succ + -1 * q.succ := by gcongr <;> lia
       _ = p * q - 1 := by simp_rw [Nat.cast_succ, mul_add, mul_comm]; lia
       _ ≤ n - 1 := by rwa [sub_le_sub_iff_right, ← Nat.cast_mul, Nat.cast_le]
       _ < n := by lia

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Regular

Goal state before:
pp: R : Type u_1
inst✝ : MulZeroClass R
⊢ ¬IsLeftRegular 0 ↔ Nontrivial R

Tactic:
rw [nontrivial_iff, not_iff_comm, isLeftRegular_zero_iff_subsingleton, subsingleton_iff]

Goal state after:
R : Type u_1
inst✝ : MulZeroClass R
⊢ (¬∃ x y, x ≠ y) ↔ ∀ (x y : R), x = y
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case inr
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
hb : b ≠ ⊤
⊢ 0 < a - b ↔ b < a ∨ b = ⊤

Tactic:
· simp [← sub_self_eq_zero_of_ne_top hb, hb]

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
h : b ≤ a
⊢ a - b = c ↔ a = c + b

Tactic:
rw [eq_comm, hb.eq_tsub_iff_add_eq_of_le h, eq_comm]

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

Goal state before:
pp: case inl
α : Type u_1
inst✝⁵ : AddCommMonoid α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
h : a ≤ b
⊢ a + a - (b + b) = a - b + (a - b)

pp: case inr
α : Type u_1
inst✝⁵ : AddCommMonoid α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
h : b ≤ a
⊢ a + a - (b + b) = a - b + (a - b)

Tactic:
· rw [tsub_eq_zero_of_le h, tsub_eq_zero_of_le (add_le_add h h), add_zero]

Goal state after:
case inr
α : Type u_1
inst✝⁵ : AddCommMonoid α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
a b : α
h : b ≤ a
⊢ a + a - (b + b) = a - b + (a - b)
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
x : WithZero α
inst✝ : NoMinOrder α
hx : x ≠ 0
⊢ ∃ y, y ≠ 0 ∧ y < x

Tactic:
obtain ⟨z, hlt⟩ := exists_lt (WithZero.unzero hx)

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
x : WithZero α
inst✝ : NoMinOrder α
hx : x ≠ 0
z : α
hlt : z < unzero hx
⊢ ∃ y, y ≠ 0 ∧ y < x
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
zero_le : ∀ (a : α), 0 ≤ a
⊢ IsOrderedAddMonoid (WithZero α)

Tactic:
have := WithZero.addLeftMono zero_le

Goal state after:
α : Type u_1
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
zero_le : ∀ (a : α), 0 ≤ a
this : AddLeftMono (WithZero α)
⊢ IsOrderedAddMonoid (WithZero α)
Module: Mathlib.Algebra.Order.GroupWithZero.Canonical

Goal state before:
pp: G : Type u_3
inst✝¹ : Preorder G
a : G
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
hx : x ≠ 0
⊢ x.log ≤ a ↔ x ≤ exp a

Tactic:
by
  rw [← toAdd_unzero_eq_log hx, ← le_ofAdd_iff hx, exp]

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
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
⊢ ↑b < a + ↑n ↔ b < ⌈a⌉₊ + n

Tactic:
obtain hb | hb := le_or_gt n b

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

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 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:
exact iff_of_true (lt_add_of_nonneg_of_lt ha <| cast_lt.2 hb) (Nat.lt_add_left _ hb)

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
inst✝ : Invertible (a + b)
h : ⅟(a + b) = ⅟a + ⅟b
h' : -1 = ⅟a * b + ⅟b * a
⊢ a * ⅟b * a = b * ⅟a * b

Tactic:
have h_a_binv_a : -(b + a) = a * ⅟b * a := neg_add_eq_mul_invOf_mul_same_iff.mpr h'

Goal state after:
R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
h : ⅟(a + b) = ⅟a + ⅟b
h' : -1 = ⅟a * b + ⅟b * a
h_a_binv_a : -(b + a) = a * ⅟b * a
⊢ a * ⅟b * a = b * ⅟a * b
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: case succ
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
⊢ x ^ (k + 1 + 1) + y ^ (k + 1 + 1) ≤ (x + y) ^ (k + 1 + 1)

Tactic:
let n := k.succ

Goal state after:
case succ
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
k : ℕ
ih : k + 1 ≠ 0 → x ^ (k + 1) + y ^ (k + 1) ≤ (x + y) ^ (k + 1)
hn : k + 1 + 1 ≠ 0
n : ℕ := k.succ
⊢ x ^ (k + 1 + 1) + y ^ (k + 1 + 1) ≤ (x + y) ^ (k + 1 + 1)
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
n : ℕ
⊢ 2 ^ n * (2 ^ (n - 1) * ((a ^ 2) ^ n + (b ^ 2) ^ n)) = 2 ^ (2 * n - 1) * (a ^ (2 * n) + b ^ (2 * n))

Tactic:
simp only [← mul_assoc, ← pow_add, ← pow_mul]

Goal state after:
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
n : ℕ
⊢ 2 ^ (n + (n - 1)) * (a ^ (2 * n) + b ^ (2 * n)) = 2 ^ (2 * n - 1) * (a ^ (2 * n) + b ^ (2 * n))
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Sort u_1
a : α
r : α → α → Prop
h : ∃ b, r b a ∧ ¬Acc r b
⊢ ∃ b, ¬Acc r b ∧ r b a

Tactic:
simpa only [and_comm]

Goal state after:
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
e : α ≃o β
x y : α
z : ↑(Icc (e x) (e y))
⊢ e.symm ↑z ∈ Icc x y

Tactic:
simp only [mem_Icc, e.le_symm_apply, e.symm_apply_le]; exact z.property

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

Goal state before:
pp: γ : Type u_3
inst✝ : LinearOrder γ
a b : γ
s t : Set γ
ha : IsLeast s a
hb : IsLeast t b
⊢ min a b ∈ s ∪ t

Tactic:
rcases le_total a b with h | h <;> simp [h, ha.1, hb.1]

Goal state after:
Module: Mathlib.Control.Functor

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝³ : Functor F
inst✝² : Functor G
inst✝¹ : LawfulFunctor F
inst✝ : LawfulFunctor G
α : Type v
x : F (G α)
⊢ Comp.map id (mk x) = mk x

Tactic:
simp only [Comp.map, id_map, id_map']

Goal state after:
F : Type u → Type w
G : Type v → Type u
inst✝³ : Functor F
inst✝² : Functor G
inst✝¹ : LawfulFunctor F
inst✝ : LawfulFunctor G
α : Type v
x : F (G α)
⊢ mk (mk x) = mk x
Module: Mathlib.Algebra.BigOperators.Group.List.Defs

Goal state before:
pp: case succ
M : Type u_2
inst✝ : Monoid M
a : M
n : ℕ
ih : (replicate n a).prod = a ^ n
⊢ (replicate (n + 1) a).prod = a ^ (n + 1)

Tactic:
replicate_succ,

Goal state after:
case succ
M : Type u_2
inst✝ : Monoid M
a : M
n : ℕ
ih : (replicate n a).prod = a ^ n
⊢ (a :: replicate n a).prod = a ^ (n + 1)
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
ha : 0 ≤ 0
hs : IsLUB ∅ b
⊢ IsLUB ((fun a ↦ 0) '' ∅) 0

Tactic:
simp only [Set.image_empty, isLUB_empty_iff] at hs ⊢

Goal state after:
case inr.inl
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
b : α
inst✝ : IsStrictOrderedRing α
ha : 0 ≤ 0
hs : IsBot b
⊢ IsBot 0
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, l₁.length = l₂.length → (∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ (a :: l₁).zip (b :: l₂) → R a_1 b_1
h₁ : l₁.length = l₂.length
a✝ : α
b✝ : β
h : (a✝, b✝) ∈ l₁.zip l₂
⊢ (a✝, b✝) ∈ (a :: l₁).zip (b :: l₂)

Tactic:
simp only [zip, zipWith, mem_cons, Prod.mk.injEq]; right
            simpa [zip] using h

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : a * b < c
⊢ ∃ a' > a, a' * b < c

Tactic:
rcases le_or_gt b 0 with hb | hb

Goal state after:
case inl
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : a * b < c
hb : b ≤ 0
⊢ ∃ a' > a, a' * b < c

case inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : a * b < c
hb : 0 < b
⊢ ∃ a' > a, a' * b < c
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
⊢ zpow' a (m + n) = zpow' a m * zpow' a n

Tactic:
by_cases ha : a = 0

Goal state after:
case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : a = 0
⊢ zpow' a (m + n) = zpow' a m * zpow' a n

case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
⊢ zpow' a (m + n) = zpow' a m * zpow' a n
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
⊢ zpow' a (m * n) = zpow' (zpow' a m) n

Tactic:
by_cases ha : a = 0

Goal state after:
case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : a = 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n

case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : CommGroupWithZero α
n : ℤ
a b : α
⊢ zpow' (a * b) n = zpow' a n * zpow' b n

Tactic:
by_cases ha : a = 0

Goal state after:
case pos
α : Type u_1
inst✝ : CommGroupWithZero α
n : ℤ
a b : α
ha : a = 0
⊢ zpow' (a * b) n = zpow' a n * zpow' b n

case neg
α : Type u_1
inst✝ : CommGroupWithZero α
n : ℤ
a b : α
ha : ¬a = 0
⊢ zpow' (a * b) n = zpow' a n * zpow' b n
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
h : ∀ (a : α), (∀ (a' : α), a' ≠ a → a' ∈ as → f a' = 1) → (map f as).prod = f a ^ count a as
a : α
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
⊢ (map f (a' :: as)).prod = f a ^ count a (a' :: as)

Tactic:
specialize h a fun a' ha' hfa' => hf a' ha' (mem_cons_of_mem _ hfa')

Goal state after:
case cons
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
h : (map f as).prod = f a ^ count a as
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
⊢ (map f (a' :: as)).prod = f a ^ count a (a' :: as)
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
p q : α → Bool
l : List α
⊢ filter p (filter q l) = filter q (filter p l)

Tactic:
simp [Bool.and_comm]

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

Goal state before:
pp: a b s x : ℕ
hx : x ∈ range' a b s
⊢ a ≤ x

Tactic:
obtain ⟨i, _, rfl⟩ := List.mem_range'.mp hx

Goal state after:
a b s i : ℕ
left✝ : i < b
hx : a + s * i ∈ range' a b s
⊢ a ≤ a + s * i
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: q : ℚ
⊢ q.toNNRat = 0 ↔ q ≤ 0

Tactic:
simpa [-toNNRat_pos] using (@toNNRat_pos q).not

Goal state after:
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: F : Type u_1
α : Type u_3
inst✝² : DivisionRing α
inst✝¹ : FunLike F ℚ α
inst✝ : RingHomClass F ℚ α
f : F
q : ℚ
⊢ f q = ↑q

Tactic:
by rw [← map_ratCast f, Rat.cast_id]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set α
⊢ s ∪ ⋂ i, ⋂ j, t i j = ⋂ i, ⋂ j, s ∪ t i j

Tactic:
by simp_rw [union_iInter]

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

Goal state before:
pp: case neg
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLattice α
f : ι → α
htriv : ∃ i, f i ≠ ⊥
i : ι
hi : ¬f i = ⊥
⊢ ∃ i', f i ≤ f ↑i'

Tactic:
exact ⟨⟨i, hi⟩, rfl.le⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LE α
inst✝ : SupSet α
s : Set α
hs : BddAbove s
⊢ ↑(sSup s) = if BddAbove s then ↑(sSup s) else ⊤

pp: case h
α : Type u_1
inst✝¹ : LE α
inst✝ : SupSet α
s : Set α
hs : BddAbove s
⊢ Injective fun a ↦ ↑a

pp: case hnc
α : Type u_1
inst✝¹ : LE α
inst✝ : SupSet α
s : Set α
hs : BddAbove s
⊢ ⊤ ∉ (fun a ↦ ↑a) '' s

Tactic:
if_pos hs

Goal state after:
α : Type u_1
inst✝¹ : LE α
inst✝ : SupSet α
s : Set α
hs : BddAbove s
⊢ ↑(sSup s) = ↑(sSup s)

case h
α : Type u_1
inst✝¹ : LE α
inst✝ : SupSet α
s : Set α
hs : BddAbove s
⊢ Injective fun a ↦ ↑a

case hnc
α : Type u_1
inst✝¹ : LE α
inst✝ : SupSet α
s : Set α
hs : BddAbove s
⊢ ⊤ ∉ (fun a ↦ ↑a) '' s
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
inst✝ : Frame α
a : α
f : ι → α
⊢ a ⊓ ⨆ i, f i = ⨆ i, a ⊓ f i

Tactic:
simpa only [inf_comm] using iSup_inf_eq f a

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι✝¹ : Sort w
κ : ι✝¹ → Sort w'
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → CompletelyDistribLattice (π i)
ι✝ : Type (max u_1 u_2)
κ✝ : ι✝ → Type (max u_1 u_2)
f : (a : ι✝) → κ✝ a → (i : ι) → π i
⊢ ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)

Tactic:
by ext i; simp only [iInf_apply, iSup_apply, iInf_iSup_eq]

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

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
⊢ sSup s = sSup t

Tactic:
by_cases B : BddAbove s ∨ BddAbove t

Goal state after:
case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
⊢ sSup s = sSup t

case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : ¬(BddAbove s ∨ BddAbove t)
⊢ sSup s = sSup t
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
n : α
this : OrderBot α
⊢ (n ∈ s ∧ ∀ a ∈ s, n ≤ a) → sInf s = n

Tactic:
intro ⟨hn, hle⟩
    exact le_antisymm (csInf_le (OrderBot.bddBelow s) hn) (le_csInf hs hle)

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : DistribLattice α
a b c : α
h : ∀ (x : α), x ∈ (fun b ↦ [[b, a]]) b ↔ x ∈ (fun b ↦ [[b, a]]) c
⊢ b = c

Tactic:
exact eq_of_mem_uIcc_of_mem_uIcc ((h _).1 left_mem_uIcc) ((h _).2 left_mem_uIcc)

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b ↦ Ι b a) b ↔ x ∈ (fun b ↦ Ι b a) c
ha : b ≤ a
⊢ b = c

pp: case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b ↦ Ι b a) b ↔ x ∈ (fun b ↦ Ι b a) c
ha : a < b
⊢ b = c

Tactic:
· have hb := (h b).not
    simp only [ha, left_mem_uIoc, true_iff, notMem_uIoc, ← not_le,
      and_true, not_true, false_and, not_false_iff, or_false] at hb
    refine hb.eq_of_not_lt fun hc => ?_
    simpa [ha, and_iff_right hc, ← @not_le _ _ _ a, iff_not_self, -not_le] using h c

Goal state after:
case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ (fun b ↦ Ι b a) b ↔ x ∈ (fun b ↦ Ι b a) c
ha : a < b
⊢ b = c
Module: Mathlib.Data.SetLike.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : SetLike A B
inst✝¹ : PartialOrder A
inst✝ : IsConcreteLE A B
p q : A
⊢ p < q → ∃ x, x ∈ q ∧ ¬x ∈ p

Tactic:
simpa [← coe_ssubset_coe] using! Set.exists_of_ssubset

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

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
q : ℚ≥0
ha : 0 ≤ a
⊢ 0 ≤ q • a

Tactic:
by
  rw [NNRat.smul_def]; exact mul_nonneg q.cast_nonneg ha

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : One M
inst✝ : DecidableEq ι
f : ι → M
x : ι
y : M
hy : y ≠ 1
a : ι
⊢ a ∈ mulSupport (update f x y) ↔ a ∈ insert x (mulSupport f)

Tactic:
obtain rfl | hne := eq_or_ne a x <;> simp [*]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : One M
inst✝ : DecidableEq ι
f : ι → M
x a : ι
⊢ a ∈ mulSupport (update f x 1) ↔ a ∈ mulSupport f \ {x}

Tactic:
obtain rfl | hne := eq_or_ne a x <;> simp [*]

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
a : α
⊢ a⁻ᵐ / a⁺ᵐ = a⁻¹

Tactic:
← inv_div,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
a : α
⊢ (a⁺ᵐ / a⁻ᵐ)⁻¹ = a⁻¹
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case mp
n : ℕ
⊢ n ! = 1 → n ≤ 1

pp: case mpr
n : ℕ
⊢ n ≤ 1 → n ! = 1

Tactic:
· intro h
    rw [← not_lt, ← one_lt_factorial, h]
    apply lt_irrefl

Goal state after:
case mpr
n : ℕ
⊢ n ≤ 1 → n ! = 1
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
succ_sub_succ,

Goal state after:
n k : ℕ
⊢ (n - k) * ((n + 1) * n.descFactorial k) = (n + 1) * ((n - k) * n.descFactorial k)
Module: Mathlib.Algebra.Order.Hom.Basic

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ f (x / y) = f (y / x)

Tactic:
← inv_div,

Goal state after:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : GroupSeminormClass F α β
f : F
x y : α
⊢ f (y / x)⁻¹ = f (y / x)
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
h : k.succ ≤ n.succ
⊢ (n.succ - k.succ)! * ((n + 1) * n.descFactorial k) = n.succ !

Tactic:
succ_sub_succ,

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

Goal state before:
pp: n k : ℕ
⊢ (n + 1 - (k + 1)) ^ k * (n + 1 - (k + 1)) ≤ (n - k) * n.descFactorial k

Tactic:
succ_sub_succ,

Goal state after:
n k : ℕ
⊢ (n - k) ^ k * (n - k) ≤ (n - k) * n.descFactorial k
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: case negSucc
α : Type u_1
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑(Int.negSucc n))⁻¹ = (↑(Int.negSucc n))⁻¹

Tactic:
· simp only [Int.cast_negSucc, cast_neg, inv_neg, cast_inv_nat]

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

Goal state before:
pp: case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℤ
hn✝ : 0 ≤ n
a : k
hn : 0 < n
⊢ ⌊a / ↑n⌋ = ⌊a⌋ / n

Tactic:
nth_rw 2 [← div_mul_cancel₀ (a := a) (ne_of_gt (Int.cast_pos.mpr hn))]

Goal state after:
case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℤ
hn✝ : 0 ≤ n
a : k
hn : 0 < n
⊢ ⌊a / ↑n⌋ = ⌊a / ↑n * ↑n⌋ / n
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 : R
m : ℤ
⊢ fract (a + ↑m) = fract a

Tactic:
rw [fract]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
m : ℤ
⊢ a + ↑m - ↑⌊a + ↑m⌋ = fract a
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 : R
m : ℕ
⊢ fract (a + ↑m) = fract a

Tactic:
rw [fract]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
m : ℕ
⊢ a + ↑m - ↑⌊a + ↑m⌋ = fract a
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 : R
m : ℤ
⊢ fract (a - ↑m) = fract a

Tactic:
rw [fract]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
m : ℤ
⊢ a - ↑m - ↑⌊a - ↑m⌋ = fract a
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 : R
n : ℕ
⊢ fract (a - ↑n) = fract a

Tactic:
rw [fract]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
n : ℕ
⊢ a - ↑n - ↑⌊a - ↑n⌋ = fract a
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : 0 < ↑n
l₀ : ℕ
hl : 0 ≤ -↑l₀
⊢ fract (↑(-↑l₀) / ↑n) = ↑(-↑l₀ % ↑n) / ↑n

Tactic:
rw [Right.nonneg_neg_iff, natCast_nonpos_iff] at hl

Goal state after:
case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m : ℤ
n : ℕ
hn : 0 < ↑n
l₀ : ℕ
hl : l₀ = 0
⊢ fract (↑(-↑l₀) / ↑n) = ↑(-↑l₀ % ↑n) / ↑n
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : ℚ
⊢ round ↑x = round x

Tactic:
have : ((x + 1 / 2 : ℚ) : α) = x + 1 / 2 := by simp

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : ℚ
this : ↑(x + 1 / 2) = ↑x + 1 / 2
⊢ round ↑x = round x
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Archimedean R
inst✝ : ExistsAddOfLE R
x y : R
hx : 1 ≤ x
hy : 1 < y
⊢ ∃ n, y ^ n ≤ x ∧ x < y ^ (n + 1)

Tactic:
have h : ∃ n : ℕ, x < y ^ n := pow_unbounded_of_one_lt _ hy

Goal state after:
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Archimedean R
inst✝ : ExistsAddOfLE R
x y : R
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
⊢ ∃ n, y ^ n ≤ x ∧ x < y ^ (n + 1)