mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : MulLeftStrictMono α
a b c : α
h : b ≤ c ∨ c ≤ b
⊢ a * c = a * b ↔ c = b

Tactic:
refine ⟨fun h' => ?_, (· ▸ rfl)⟩
  contrapose h'
  obtain h | h := h
  · exact mul_lt_mul_right (h.lt_of_ne' h') a |>.ne'
  · exact mul_lt_mul_right (h.lt_of_ne h') a |>.ne

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

Goal state before:
pp: case inr.inr.inr.inr
α : Type u_1
inst✝³ : Mul α
inst✝² : LinearOrder α
a b c d : α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
h : a * b = c * d
hca : c < a
hdb : d < b
⊢ a = c ∧ b = d ∨ a < c ∨ b < d

Tactic:
· exact False.elim <| ne_of_lt (mul_lt_mul_of_lt_of_lt hca hdb) h.symm

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

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : PartialOrder M₀
a : M₀
inst✝¹ : PosMulStrictMono M₀
inst✝ : ZeroLEOneClass M₀
h : 1 < a
n : ℕ
⊢ a ^ n < a ^ (n + 1)

Tactic:
simpa only [one_mul, pow_succ] using lt_mul_right (pow_pos (zero_le_one.trans_lt h) _) h

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : AddMonoidWithOne R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : NeZero 1
inst✝ : AddLeftStrictMono R
n : ℕ
⊢ ↑n < ↑n + 1

Tactic:
apply lt_add_one

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ 0 < a / b

Tactic:
rw [div_eq_mul_inv]

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ 0 < a * b⁻¹
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a / b

Tactic:
rw [div_eq_mul_inv]

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a * b⁻¹
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 1 ≤ a
⊢ Monotone fun n ↦ a ^ n

Tactic:
refine monotone_int_of_le_succ fun n ↦ ?_

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 1 ≤ a
n : ℤ
⊢ a ^ n ≤ a ^ (n + 1)
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
n : ℤ
ha : 1 < a
⊢ 1 < a ^ n ↔ 0 < n

Tactic:
by
  simp [← zpow_lt_zpow_iff_right₀ ha]

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
n : ℤ
ha : 1 < a
⊢ a ^ n < 1 ↔ n < 0

Tactic:
by
  simp [← zpow_lt_zpow_iff_right₀ ha]

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : a ≤ 0
hb : 0 ≤ b
⊢ a / b ≤ 0

Tactic:
rw [div_eq_mul_inv]

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : a ≤ 0
hb : 0 ≤ b
⊢ a * b⁻¹ ≤ 0
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : LinearOrder G₀
a b : G₀
inst✝ : PosMulMono G₀
ha : 0 ≤ a
hb : b ≤ 0
⊢ a / b ≤ 0

Tactic:
rw [div_eq_mul_inv]

Goal state after:
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : LinearOrder G₀
a b : G₀
inst✝ : PosMulMono G₀
ha : 0 ≤ a
hb : b ≤ 0
⊢ a * b⁻¹ ≤ 0
Module: Mathlib.Algebra.Order.Archimedean.Defs

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x : R
n : ℤ
h : -x < ↑n
⊢ ↑(-n) < x

Tactic:
rw [Int.cast_neg]; exact neg_lt.1 h

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

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
⊢ max a 1 * max a⁻¹ 1 = |a|ₘ

Tactic:
symm

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
⊢ |a|ₘ = max a 1 * max a⁻¹ 1
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case inl
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
h : 1 ≤ a
⊢ |a|ₘ⁻¹ ≤ a

Tactic:
simpa [mabs_of_one_le h] using (inv_le_one'.2 h).trans h

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: p : ℕ
⊢ 0 < 2

Tactic:
decide

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: case ofNat
α : Type u_1
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
a : α
k : ℕ
⊢ (-a) ^ (2 * k + 1) = -a ^ (2 * k + 1)

Tactic:
simp [pow_add]

Goal state after:
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: case negSucc
α : Type u_1
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
a : α
k : ℕ
⊢ ((-a) ^ (1 + k * 2))⁻¹ = -(a ^ (1 + k * 2))⁻¹

Tactic:
simp [pow_add]

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : AddMonoidWithOne α
inst✝ : CharZero α
⊢ 1 ≠ 0

Tactic:
decide

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

Goal state before:
pp: m : ℤ
even : Even m
⊢ 0 < 2

Tactic:
decide

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs

Goal state before:
pp: α : Type u
inst✝² : Semigroup α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedMul α
a b c : α
hbc : b ≤ b * c
⊢ ∃ c_1, (fun x1 x2 ↦ x1 * x2) a (b * c) = (fun x1 x2 ↦ x1 * x2) a b * c_1

Tactic:
exact ⟨c, (mul_assoc _ _ _).symm⟩

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

Goal state before:
pp: case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : (p + 1).pred * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ ↑n < ↑n

Tactic:
p.pred_succ,

Goal state after:
case succ.succ
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * (q + 1).pred ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ ↑n < ↑n
Module: Mathlib.Algebra.Order.Monoid.WithTop

Goal state before:
pp: case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝¹ : α
hx : ↑a✝¹ ≠ ⊥
a✝ : α
⊢ ↑a✝ ≤ ↑a✝ + ↑a✝¹

Tactic:
rw [← WithBot.coe_add, WithBot.coe_le_coe]
    exact le_self_add

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

Goal state before:
pp: M : Type u_4
inst✝ : AddMonoid M
x y : WithZero (Multiplicative M)
hx : x ≠ 0
hy : y ≠ 0
⊢ (x * y).log = x.log + y.log

Tactic:
lift x to Multiplicative M using hx; lift y to Multiplicative M using hy; rfl

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

Goal state before:
pp: M : Type u_4
inst✝ : AddMonoid M
x y : WithZero (Multiplicative M)
hx : x ≠ 0
hy : y ≠ 0
⊢ (x * y).log = x.log + y.log

Tactic:
by
  lift x to Multiplicative M using hx; lift y to Multiplicative M using hy; rfl

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

Goal state before:
pp: ⊢ IsCompl {n | Even n} {n | Odd n}

Tactic:
by
  simp only [← Set.compl_ofPred, isCompl_compl, ← not_even_iff_odd]

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 : α
h1 : c ≤ a
h2 : c ≤ b
⊢ a - c ≤ b - c ∧ b ≤ a ↔ a ≤ b ∧ b ≤ a

Tactic:
tsub_le_tsub_iff_right h2

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

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ z ≤ ⌈a⌉ ↔ ↑z - 1 < a

Tactic:
rw [← sub_one_lt_iff, lt_ceil]

Goal state after:
α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ ↑(z - 1) < a ↔ ↑z - 1 < a
Module: Mathlib.Algebra.Order.Floor.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
n : ℕ
ha : 0 ≤ a
⊢ n ≤ ⌊a⌋.toNat ↔ ↑n ≤ a

Tactic:
by rw [Int.le_toNat (Int.floor_nonneg.2 ha), Int.le_floor, Int.cast_natCast]

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

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

Tactic:
· rw [eq_tsub_iff_add_eq_of_le (le_floor h), ← floor_add_natCast _, tsub_add_cancel_of_le h]
    exact le_tsub_of_add_le_left ((add_zero _).trans_le h)

Goal state after:
Module: Mathlib.Order.Directed

Goal state before:
pp: case inl
β : Type u_2
inst✝² : PartialOrder β
inst✝¹ : Nontrivial β
inst✝ : IsCodirectedOrder β
a b : β
hne : a ≠ b
ha : IsBot a
⊢ ∃ a b, a < b

pp: case inr
β : Type u_2
inst✝² : PartialOrder β
inst✝¹ : Nontrivial β
inst✝ : IsCodirectedOrder β
a b : β
hne : a ≠ b
c : β
hc : c < a
⊢ ∃ a b, a < b

Tactic:
exacts [⟨a, b, (ha b).lt_of_ne hne⟩, ⟨_, _, hc⟩]

Goal state after:
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: case inl.inl
hu hv : IsUnit 1
⊢ 1 ≠ 1 ↔ 1 = -1

Tactic:
decide

Goal state after:
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: case inl.inr
hu : IsUnit 1
hv : IsUnit (-1)
⊢ 1 ≠ -1 ↔ 1 = - -1

Tactic:
decide

Goal state after:
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: case inr.inl
hu : IsUnit (-1)
hv : IsUnit 1
⊢ -1 ≠ 1 ↔ -1 = -1

Tactic:
decide

Goal state after:
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: case inr.inr
hu hv : IsUnit (-1)
⊢ -1 ≠ -1 ↔ -1 = - -1

Tactic:
decide

Goal state after:
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: ⊢ -1 * -1 = 1

Tactic:
decide

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

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : R
n : ℕ
⊢ a ^ n = 1 ↔ n = 0 ∨ a = 1 ∨ a = -1 ∧ Even n

Tactic:
by
  simp [← pow_eq_pow_iff_cases]

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

Goal state before:
pp: n : ℕ
hn : Odd n
hm : 2 ∣ n
⊢ ¬Odd 2

Tactic:
decide

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ IsWellOrder α r ↔ ∀ (s : Set α), s.Nonempty → ∃ m, m ∈ s ∧ ∀ (x : α), x ∈ s → ¬r x m ∧ (m = x ∨ r m x)

Tactic:
refine ⟨fun h s hs ↦ ?_, fun h ↦ { wf := ?_, trichotomous a b := ?_ }⟩
  · grind [h.wf.has_min, trichotomous_of r]
  · grind [wellFounded_iff_has_min]
  · grind [h {a, b} <| by simp]

Goal state after:
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type u
s t : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ↑(s ∪ t) ⊕ ↑(s ∩ t) ≃ ↑(s ∪ t \ s) ⊕ ↑(s ∩ t)

Tactic:
rw [union_sdiff_self]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ico a b \ {a} ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∈ s
⊢ Icc a b ⊆ s

Tactic:
sdiff_singleton_subset_iff,

Goal state after:
case pos
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ico a b ⊆ insert a s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∈ s
⊢ Icc a b ⊆ s
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Icc a b \ {b} ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∈ s
⊢ Icc a b ⊆ s

Tactic:
sdiff_singleton_subset_iff,

Goal state after:
case pos
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Icc a b ⊆ insert b s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∈ s
⊢ Icc a b ⊆ s
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: case neg.refine_2
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ico a b \ {a} ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ Ico a b ⊆ s

Tactic:
sdiff_singleton_subset_iff,

Goal state after:
case neg.refine_2
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ico a b ⊆ insert a s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ Ico a b ⊆ s
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: case pos.refine_2
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioc a b \ {b} ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ Ioc a b ⊆ s

Tactic:
sdiff_singleton_subset_iff,

Goal state after:
case pos.refine_2
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioc a b ⊆ insert b s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ Ioc a b ⊆ s
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b : α
inst✝ : IsStrictOrderedRing α
s : Set α
ha : 0 ≤ a
hs : IsGLB s b
⊢ IsGLB ((fun b ↦ a * b) '' s) (a * b)

Tactic:
rcases lt_or_eq_of_le ha with (ha | rfl)
  · exact (OrderIso.mulLeft₀ _ ha).isGLB_image'.2 hs
  · simp_rw [zero_mul]
    rw [hs.nonempty.image_const]
    exact isGLB_singleton

Goal state after:
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
f : α → α → α
a b : α
na nb nc da db dc k : ℕ
⊢ f = HMul.hMul →
    IsNNRat a na da → IsNNRat b nb db → na.mul nb = k.mul nc → da.mul db = k.mul dc → IsNNRat (f a b) nc dc

Tactic:
by
  rintro rfl ⟨_, rfl⟩ ⟨_, rfl⟩ (h₁ : na * nb = k * nc) (h₂ : da * db = k * dc)
  have : Invertible (↑(da * db) : α) := by simpa using invertibleMul (da:α) db
  have := invertibleOfMul' (α := α) h₂
  refine ⟨this, ?_⟩
  have H := (Nat.cast_commute (α := α) da db).invOf_left.invOf_right.right_comm
  have h₁ := congr_arg (Nat.cast (R := α)) h₁
  simp only [Nat.cast_mul] at h₁
  simp only [← mul_assoc, (Nat.cast_commute (α := α) da nb).invOf_left.right_comm, h₁]
  have h₂ := congr_arg (↑nc * ↑· * (⅟↑da * ⅟↑db * ⅟↑dc : α)) h₂
  simp only [Nat.cast_mul, ← mul_assoc] at h₂; rw [H] at h₂
  simp only [mul_invOf_cancel_right'] at h₂; rw [h₂, Nat.cast_commute]
  simp only [mul_invOf_cancel_right',
    (Nat.cast_commute (α := α) da dc).invOf_left.invOf_right.right_comm,
    (Nat.cast_commute (α := α) db dc).invOf_left.invOf_right.right_comm]

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 b : α
hb : b < 0
⊢ AntitoneOn (fun x ↦ x⁻¹) (Set.Icc a b)

Tactic:
convert! sub_inv_antitoneOn_Icc_left hb
  exact (sub_zero _).symm

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ min 1 (ε / (1 + ↑n * (B + 1) ^ (n - 1)))
⊢ |q - r| * ↑n * max |q| |r| ^ (n - 1) < ε

Tactic:
le_inf_iff,

Goal state after:
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
ε : α
hε : 0 < ε
n : ℕ
B : α
B_pos : 0 < B
pos : 0 < 1 + ↑n * (B + 1) ^ (n - 1)
q r : α
hr : |r| ≤ B
hqr : |q - r| ≤ 1 ∧ |q - r| ≤ ε / (1 + ↑n * (B + 1) ^ (n - 1))
⊢ |q - r| * ↑n * max |q| |r| ^ (n - 1) < ε
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case trans
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
l₁✝ l₂✝ l₃✝ : List α
h₁✝ : l₁✝ ~ l₂✝
h₂✝ : l₂✝ ~ l₃✝
r₁ : ∀ (b : β), foldr f b l₁✝ = foldr f b l₂✝
r₂ : ∀ (b : β), foldr f b l₂✝ = foldr f b l₃✝
b : β
⊢ foldr f b l₁✝ = foldr f b l₃✝

Tactic:
| trans _ _ r₁ r₂ =>

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

Goal state before:
pp: case cons.inr
M : Type u_4
inst✝¹ : Monoid M
l✝ : List M
a : M
inst✝ : DecidableEq M
b : M
l : List M
ih : a ∈ l → (∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x) → a * (l.erase a).prod = l.prod
ha : a ∈ b :: l
comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x
ne : a ≠ b
h : a ∈ l
⊢ b * (a * (l.erase a).prod) = b * l.prod

Tactic:
ih h fun x hx y hy ↦ comm _ (List.mem_cons_of_mem b hx) _ (List.mem_cons_of_mem b hy)

Goal state after:
case cons.inr
M : Type u_4
inst✝¹ : Monoid M
l✝ : List M
a : M
inst✝ : DecidableEq M
b : M
l : List M
ih : a ∈ l → (∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x) → a * (l.erase a).prod = l.prod
ha : a ∈ b :: l
comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x
ne : a ≠ b
h : a ∈ l
⊢ b * l.prod = b * l.prod
Module: Mathlib.Data.List.Basic

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

Tactic:
by
  cases l
  · simp
  · grind

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

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a b : G
l : List G
⊢ (a :: b :: l).alternatingProd = a * (b :: l).alternatingProd⁻¹

Tactic:
rw [alternatingProd_cons_cons', alternatingProd_cons' b l, mul_inv, inv_inv, mul_assoc]

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

Goal state before:
pp: q a b c : ℚ
⊢ 1 ≠ 0

Tactic:
decide

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

Goal state before:
pp: m e : ℕ
⊢ ¬false = true

Tactic:
decide

Goal state after:
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: p q : ℚ≥0
⊢ 1 ≠ 0

Tactic:
decide

Goal state after:
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: n : ℕ
⊢ divNat n 0 = 0

Tactic:
by simp [divNat]

Goal state after:
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime (y * x) (z * x) ↔ IsRelPrime y z

Tactic:
rw [isRelPrime_mul_unit_right_left hu, isRelPrime_mul_unit_right_right hu]

Goal state after:
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoid α
x y z : α
inst✝ : DecompositionMonoid α
H1 : IsRelPrime x z
H2 : IsRelPrime y z
a b : α
ha : a ∣ x
hb : b ∣ y
h : a * b ∣ x * y
hz : a * b ∣ z
⊢ IsUnit (a * b)

Tactic:
exact (H1 ha <| (dvd_mul_right a b).trans hz).mul (H2 hb <| (dvd_mul_left b a).trans hz)

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q₁ q₂ : ℚ
⊢ ↑(q₁.den.gcd q₂.den) ∣ q₁.num * ↑q₂.den + q₂.num * ↑q₁.den

Tactic:
apply Int.dvd_add
    <;> apply dvd_mul_of_dvd_right <;> rw [Int.natCast_dvd_natCast]
    <;> [exact Nat.gcd_dvd_right _ _; exact Nat.gcd_dvd_left _ _]

Goal state after:
Module: Mathlib.Tactic.NormNum.Pow

Goal state before:
pp: a b c : ℕ
h1 : a.pow b = c
⊢ a.pow (2 * b) = c.mul c

Tactic:
simp [two_mul, pow_add, ← h1]

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLinearOrder α
s : Set α
⊢ sSup s = ⊤ ↔ ∀ b < ⊤, ∃ a ∈ s, b < a

Tactic:
eq_top_iff,

Goal state after:
α : Type u_1
inst✝ : CompleteLinearOrder α
s : Set α
⊢ ⊤ ≤ sSup s ↔ ∀ b < ⊤, ∃ a ∈ s, b < a
Module: Mathlib.Order.CompleteLattice.Defs

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : CompleteLinearOrder α
f : ι → α
⊢ iSup f = ⊤ ↔ ∀ b < ⊤, ∃ i, b < f i

Tactic:
eq_top_iff,

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝ : CompleteLinearOrder α
f : ι → α
⊢ ⊤ ≤ iSup f ↔ ∀ b < ⊤, ∃ i, b < f i
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : ∀ (b : α), a₀ ≤ b ↔ b ∈ upperBounds s
hb₀ : ∀ (b : β), b₀ ≤ b ↔ b ∈ upperBounds t
⊢ IsLUB (image2 l s t) (l a₀ b₀)

Tactic:
mem_upperBounds

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
s : Set α
t : Set β
l : α → β → γ
u₁ : β → γ → α
u₂ : α → γ → β
a₀ : α
b₀ : β
h₁ : ∀ (b : β), GaloisConnection (swap l b) (u₁ b)
h₂ : ∀ (a : α), GaloisConnection (l a) (u₂ a)
ha₀ : ∀ (b : α), a₀ ≤ b ↔ ∀ x ∈ s, x ≤ b
hb₀ : ∀ (b : β), b₀ ≤ b ↔ ∀ x ∈ t, x ≤ b
⊢ IsLUB (image2 l s t) (l a₀ b₀)
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
a : α
s : Set β
hs : s.Nonempty
this : Nonempty ↑s
⊢ ⨆ i, a = a

Tactic:
iSup_const

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
a : α
s : Set β
hs : s.Nonempty
this : Nonempty ↑s
⊢ a = a
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ (⨆ x, f x) ⊔ a = (⨆ x, f x) ⊔ ⨆ x, a

Tactic:
iSup_const

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ (⨆ x, f x) ⊔ a = (⨆ x, f x) ⊔ a
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ a ⊔ ⨆ x, f x = (⨆ x, a) ⊔ ⨆ x, f x

Tactic:
iSup_const

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ a ⊔ ⨆ x, f x = a ⊔ ⨆ x, f x
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: β : Type u_2
ι : Type u_12
x : ι → β
t : ι → Set β
⊢ (⋃ i, t i) ∪ ⋃ i, {x i} = (⋃ i, t i) ∪ range x

Tactic:
iUnion_singleton_eq_range

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
t : α → Set β
⊢ ⋃ x ∈ ⋃ i, s i, t x = ⋃ i, ⋃ x ∈ s i, t x

Tactic:
by simp [@iUnion_comm _ ι]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α → Set β
s₁ s₂ : Set α
⊢ s₁ ⊆ s₂ ∪ s₁ \ s₂

Tactic:
rw [union_sdiff_self]

Goal state after:
α : Type u_1
β : Type u_2
t : α → Set β
s₁ s₂ : Set α
⊢ s₁ ⊆ s₂ ∪ s₁
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
inst✝¹ : CompleteBooleanAlgebra α
f : ι → α
inst✝ : Nonempty ι
a : α
⊢ a ∆ ⨆ i, f i ≤ ⨆ i, a ∆ f i

Tactic:
simpa [symmDiff_comm] using iSup_symmDiff_le (a := a)

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ioi a \ Ioi b = Ioc a b

Tactic:
rw [sdiff_eq, compl_Ioi, Ioi_inter_Iic]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ sInf (f '' s) = sInf (f '' t)

Tactic:
refine le_antisymm ?_ (by gcongr; exacts [ht, hs.image f])

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ sInf (f '' s) ≤ sInf (f '' t)
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ b < a ∧ a ≤ c ∨ a ∈ Ioc c b ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b

Tactic:
mem_Ioc

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
h : ∃ t, IsChain r s ∧ SuperChain r s t
⊢ IsChain r (SuccChain r s)

Tactic:
exact (succChain_spec h).1

Goal state after: