mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ∃ a b, a * (p + 1) + b * (q + 1) = n

Tactic:
refine ⟨a.toNat, b.toNat, Nat.cast_injective (R := ℤ) ?_⟩

Goal state after:
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
⊢ ↑(a.toNat * (p + 1) + b.toNat * (q + 1)) = ↑n
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: x y : ℤ
hc : x.gcd y ≠ 0
⊢ x ≠ 0 ∨ y ≠ 0

Tactic:
by
  contrapose! hc
  rw [hc.left, hc.right, gcd_zero_right, natAbs_zero]

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

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
rra : IsRightRegular a
⊢ IsRightRegular (a ^ n)

Tactic:
IsRightRegular,

Goal state after:
R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
rra : IsRightRegular a
⊢ Function.Injective fun x ↦ x * a ^ n
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝ : Mul α
x y : WithZero α
hxy : x * y ≠ 0
⊢ unzero hxy = unzero ⋯ * unzero ⋯

Tactic:
by
  simp only [← coe_inj, coe_mul, coe_unzero]

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
h : b ≠ ⊤
⊢ StrictMono fun x ↦ x - b

Tactic:
simpa [sub_eq_add_neg] using add_left_strictMono_of_ne_top (b := -b) (by simpa)

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ a - a = 0 ↔ a ≠ ⊤

Tactic:
sub_eq_add_neg,

Goal state after:
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ a + -a = 0 ↔ a ≠ ⊤
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝² : Add α
y z : WithTop α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x : α
⊢ ↑x + y ≤ ↑x + z → y ≤ z

Tactic:
cases y <;> cases z <;> simp [← coe_add]

Goal state after:
case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x a✝¹ a✝ : α
⊢ x + a✝¹ ≤ x + a✝ → a✝¹ ≤ a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝² : Add α
y z : WithTop α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x : α
⊢ y < z → ↑x + y < ↑x + z

Tactic:
cases y <;> cases z <;> simp [← coe_add]

Goal state after:
case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x a✝¹ a✝ : α
⊢ a✝¹ < a✝ → x + a✝¹ < x + a✝
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: case neg.mpr
α : Type u_1
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : AddRightReflectLE α
a b c : α
h : a < b
h' : a ≤ c + b
⊢ 0 ≤ c

Tactic:
exact zero_le

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

Goal state before:
pp: α : Type u
inst✝¹ : Add α
y z : WithBot α
inst✝ : IsLeftCancelAdd α
x : α
⊢ ↑x + y = ↑x + z ↔ y = z

Tactic:
cases y <;> cases z <;> simp [← coe_add]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a b : WithBot α
ha : a ≠ ⊥
hb : b ≠ ⊥
⊢ a.unbot ha = b.unbot hb ↔ a = b

Tactic:
by
  rw [unbot_eq_iff, coe_unbot]

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

Goal state before:
pp: α : Type u
inst✝² : Add α
y z : WithBot α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x : α
⊢ ↑x + y ≤ ↑x + z → y ≤ z

Tactic:
cases y <;> cases z <;> simp [← coe_add]

Goal state after:
case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : AddLeftReflectLE α
x a✝¹ a✝ : α
⊢ x + a✝¹ ≤ x + a✝ → a✝¹ ≤ a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝² : Add α
y z : WithBot α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x : α
⊢ y < z → ↑x + y < ↑x + z

Tactic:
cases y <;> cases z <;> simp [← coe_add]

Goal state after:
case coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x a✝¹ a✝ : α
⊢ a✝¹ < a✝ → x + a✝¹ < x + a✝
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✝¹ : Mul α
inst✝ : MulLeftMono α
b c : WithZero α
hbc : b ≤ c
⊢ 0 * b ≤ 0 * c

Tactic:
exact zero_le

Goal state after:
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✝¹ : Mul α
inst✝ : MulLeftMono α
c : WithZero α
a✝ : α
hbc : 0 ≤ c
⊢ ↑a✝ * 0 ≤ ↑a✝ * c

Tactic:
exact zero_le

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : WithZero (Multiplicative α)
b : α
ha : a ≠ 0
h : a < ↑(ofAdd b)
⊢ toAdd (unzero ha) < b

Tactic:
by
  rwa [← coe_unzero ha, coe_lt_coe, ← toAdd_lt, toAdd_ofAdd] at h

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

Goal state before:
pp: α : Type u_2
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : FloorSemiring α
n : ℕ
hn : ↑n = ↑n.succ
⊢ False

Tactic:
replace hn (k : ℕ) : ((n + k : ℕ) : α) = n := by
    induction k with | zero => rfl | succ k k_ih => grind

Goal state after:
α : Type u_2
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : FloorSemiring α
n : ℕ
hn : ∀ (k : ℕ), ↑(n + k) = ↑n
⊢ False
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
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : ExistsAddOfLE R
a : R
⊢ ⌈a - 1⌉₊ = ⌈a⌉₊ - 1

Tactic:
simpa using ceil_sub_natCast a 1

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
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
⊢ 0 ≤ a ↔ 0 ≤ b

Tactic:
simpa only [cast_zero] using h 0

Goal state after:
Module: Mathlib.Algebra.Group.Invertible.Basic

Goal state before:
pp: α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible (a * b)
⊢ b * (⅟(a * b) * a) = 1

Tactic:
← (isUnit_of_invertible a).mul_right_inj,

Goal state after:
α : Type u
inst✝² : Monoid α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible (a * b)
⊢ a * (b * (⅟(a * b) * a)) = a * 1
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: case ha
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ 0 ≤ 2 ^ n

pp: case h₂
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ a ^ (n + 1) * b + b ^ (n + 1) * a ≤ a ^ (n + 1) * a + b ^ (n + 1) * b

Tactic:
· exact pow_nonneg zero_le_two _

Goal state after:
case h₂
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ a ^ (n + 1) * b + b ^ (n + 1) * a ≤ a ^ (n + 1) * a + b ^ (n + 1) * b
Module: Mathlib.Algebra.Ring.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b
⊢ a ∣ b - c ↔ a ∣ c

Tactic:
sub_eq_add_neg,

Goal state after:
α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b
⊢ a ∣ b + -c ↔ a ∣ c
Module: Mathlib.Algebra.Ring.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b
⊢ a ∣ b + -c ↔ a ∣ c

Tactic:
dvd_add_right h,

Goal state after:
α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
h : a ∣ b
⊢ a ∣ -c ↔ a ∣ c
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a b c : K
⊢ a / c - b / c = (a - b) / c

Tactic:
sub_eq_add_neg,

Goal state after:
K : Type u_1
inst✝ : DivisionRing K
a b c : K
⊢ a / c + -(b / c) = (a - b) / c
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
s : Set α
t : Set β
f : α → β → γ
g : γ → δ
⊢ g '' image2 f s t = image2 (fun a b ↦ g (f a b)) s t

Tactic:
simp only [← image_prod, image_image]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
s : Set α
t : Set β
f : α → β → γ
g : γ → δ
⊢ g '' image2 f s t = image2 (fun a b ↦ g (f a b)) s t

Tactic:
by
  simp only [← image_prod, image_image]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
a b : α
h : IsLUB s a
⊢ a ≤ b ↔ b ∈ upperBounds s

Tactic:
rw [h.upperBounds_eq]

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : Set α
a b : α
h : IsLUB s a
⊢ a ≤ b ↔ b ∈ Ici a
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : SubtractionMonoid α
a b c : α
h : a + -b = c
⊢ a - b = c

Tactic:
sub_eq_add_neg,

Goal state after:
α : Type u_1
inst✝ : SubtractionMonoid α
a b c : α
h : a + -b = c
⊢ a + -b = c
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
⊢ 1 < a / b ↔ a < b

Tactic:
by rw [lt_div_iff_of_neg hb, one_mul]

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 : α
h : a < b
⊢ a + (b / 2 - a / 2) < b

Tactic:
sub_eq_add_neg,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
h : a < b
⊢ a + (b / 2 + -(a / 2)) < b
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case inl.inr.hb
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length ≥ n
⊢ ¬l₁ ~ l₂

Tactic:
grind [Perm.length_eq]

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

Goal state before:
pp: case nil.nil
α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
⊢ (Forall₂ r ∘r Perm) [] []

Tactic:
exact ⟨[], Forall₂.nil, Perm.nil⟩

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
⊢ l ⊆ [a, b] ↔ ∀ (c : α), c ∈ l → c = b ∨ c = a

pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ (∀ (c : α), c ∈ l → c = b ∨ c = a) ↔ ∀ (c : α), c ≠ b → c ≠ a → ¬c ∈ l

Tactic:
· simp [subset_def, or_comm]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ (∀ (c : α), c ∈ l → c = b ∨ c = a) ↔ ∀ (c : α), c ≠ b → c ≠ a → ¬c ∈ l
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List M
h : l.prod ≠ 1
⊢ ∃ x, x ∈ l ∧ x ≠ 1

Tactic:
by simpa only [not_forall, exists_prop] using mt prod_eq_one h

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

Goal state before:
pp: α : Type u
l : List α
a : α
⊢ l <+ [a] ↔ l = [] ∨ l = [a]

Tactic:
constructor <;> rintro (_ | _)

Goal state after:
case mp.cons
α : Type u
l : List α
a : α
a✝ : l <+ []
⊢ l = [] ∨ l = [a]

case mp.cons_cons
α : Type u
a : α
l₁✝ : List α
a✝ : l₁✝ <+ []
⊢ a :: l₁✝ = [] ∨ a :: l₁✝ = [a]

case mpr.inl
α : Type u
l : List α
a : α
h✝ : l = []
⊢ l <+ [a]

case mpr.inr
α : Type u
l : List α
a : α
h✝ : l = [a]
⊢ l <+ [a]
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
e : M
t t_n t_d : NF M
h : t.eval = t_n.eval / t_d.eval
⊢ ((0, e) ::ᵣ t).eval = ((1, e) ::ᵣ t_n).eval / ((1, e) ::ᵣ t_d).eval

Tactic:
by
  simp only [eval_cons, h, div_eq_mul_inv, mul_inv, ← zpow'_neg, ← add_neg_cancel (1:ℤ), zpow'_add]
  ac_rfl

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

Goal state before:
pp: q : ℚ
p : ℚ≥0
hq : 0 ≤ q
⊢ q.toNNRat < p ↔ q < ↑p

Tactic:
← coe_lt_coe,

Goal state after:
q : ℚ
p : ℚ≥0
hq : 0 ≤ q
⊢ ↑q.toNNRat < ↑p ↔ q < ↑p
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
⊢ OfScientific.ofScientific m b d = ↑(if b = true then NNRat.divNat m (10 ^ d) else ↑(m * 10 ^ d))

Tactic:
by
  rw [NNRatCast.toOfScientific_def]
  split_ifs
  · congr 2
    rw [← Rat.ofScientific_eq_ofScientific, Rat.ofScientific_def, if_pos ‹_›]
    congr
  · congr 2
    rw [← Rat.ofScientific_eq_ofScientific, Rat.ofScientific_def, if_neg ‹_›]
    congr

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

Goal state before:
pp: q : ℚ
n : ℤ
⊢ (q - ↑n).den = q.den

Tactic:
sub_eq_add_neg,

Goal state after:
q : ℚ
n : ℤ
⊢ (q + -↑n).den = q.den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: n : ℤ
q : ℚ
⊢ (↑n - q).den = q.den

Tactic:
sub_eq_add_neg,

Goal state after:
n : ℤ
q : ℚ
⊢ (↑n + -q).den = q.den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q r : ℚ
⊢ (q - r).num * ↑q.den * ↑r.den = (q.num * ↑r.den - r.num * ↑q.den) * ↑(q - r).den

Tactic:
sub_eq_add_neg,

Goal state after:
q r : ℚ
⊢ (q + -r).num * ↑q.den * ↑r.den = (q.num * ↑r.den - r.num * ↑q.den) * ↑(q + -r).den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q r : ℚ
⊢ (q + -r).num * ↑q.den * ↑r.den = (q.num * ↑r.den - r.num * ↑q.den) * ↑(q + -r).den

Tactic:
sub_eq_add_neg,

Goal state after:
q r : ℚ
⊢ (q + -r).num * ↑q.den * ↑r.den = (q.num * ↑r.den + -(r.num * ↑q.den)) * ↑(q + -r).den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: a b : ℤ
hb0 : 0 < b
h : a.natAbs.Coprime b.natAbs
⊢ (↑a / ↑b).num = a

Tactic:
by
  lift b to ℕ using hb0.le
  simp only [Int.natAbs_natCast, Int.natCast_pos] at h hb0
  rw [← Rat.divInt_eq_div, ← mk_eq_divInt (nz := hb0.ne') (c := h)]

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

Goal state before:
pp: a b : ℤ
hb0 : 0 < b
h : a.natAbs.Coprime b.natAbs
⊢ ↑(↑a / ↑b).den = b

Tactic:
by
  lift b to ℕ using hb0.le
  simp only [Int.natAbs_natCast, Int.natCast_pos] at h hb0
  rw [← Rat.divInt_eq_div, ← mk_eq_divInt (nz := hb0.ne') (c := h)]

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

Goal state before:
pp: R : Type u
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : NoZeroDivisors R
a b : R
⊢ 0 < a * b ↔ 0 < a ∧ 0 < b

Tactic:
simp only [pos_iff_ne_zero, ne_eq, mul_eq_zero, not_or]

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

Goal state before:
pp: α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
p : ι → Prop
f : (i : ι) → p i → α
hf : ∀ (i : ι) (hi : p i), u (l (f i hi)) = f i hi
⊢ l (⨅ x, f ↑x ⋯) = ⨅ i, ⨅ (hi : p i), l (f i hi)

Tactic:
iInf_subtype'

Goal state after:
α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
p : ι → Prop
f : (i : ι) → p i → α
hf : ∀ (i : ι) (hi : p i), u (l (f i hi)) = f i hi
⊢ l (⨅ x, f ↑x ⋯) = ⨅ x, l (f ↑x ⋯)
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
p : ι → Prop
f : (i : ι) → p i → α
hf : ∀ (i : ι) (hi : p i), u (l (f i hi)) = f i hi
⊢ l (⨅ x, f ↑x ⋯) = ⨅ x, l (f ↑x ⋯)

Tactic:
exact gi.l_iInf_of_u_l_eq_self _ fun _ => hf _ _

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
i₁ : LinearOrder α
i₂ : OrderBot α
h : WellFoundedLT α
⊢ sSup ∅ = ⊥

Tactic:
simp [sSup, bot_unique (WellFounded.min_le _ (mem_univ _))]

Goal state after:
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 ⊔ a

Tactic:
rw [iSup_sup_eq, iSup_const]

Goal state after:
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 ⊔ f x

Tactic:
rw [iSup_sup_eq, iSup_const]

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

Goal state before:
pp: β : Type u_2
ι : Type u_12
t : Set ι
s : ι → Set β
w : ⋃ i ∈ t, s i = ⊤
x : β
p : x ∈ ⋃ i ∈ t, s i
⊢ ∃ i ∈ t, x ∈ s i

Tactic:
Set.mem_iUnion

Goal state after:
β : Type u_2
ι : Type u_12
t : Set ι
s : ι → Set β
w : ⋃ i ∈ t, s i = ⊤
x : β
p : ∃ i, x ∈ ⋃ (_ : i ∈ t), s i
⊢ ∃ i ∈ t, x ∈ s i
Module: Mathlib.Data.Set.Order

Goal state before:
pp: α : Type u
β : Type v
s : Set α
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ ¬MonotoneOn f s ∧ ¬AntitoneOn f s ↔
    ∃ a, a ∈ s ∧ ∃ b, b ∈ s ∧ ∃ c, c ∈ s ∧ a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
simp [monotoneOn_iff_monotone, antitoneOn_iff_antitone, and_assoc, exists_and_left,
    not_monotone_not_antitone_iff_exists_lt_lt, @and_left_comm (_ ∈ s)]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : Frame α
s t : Set α
⊢ sSup s ⊓ sSup t = ⨆ p ∈ s ×ˢ t, p.1 ⊓ p.2

Tactic:
simp only [sSup_eq_iSup, biSup_inf_biSup]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : Frame α
ι : Type u_1
f : ι → α
h : Pairwise (Disjoint on f)
s t : Set ι
⊢ ⨆ i ∈ s ∩ t, f i = ⨆ p ∈ s ×ˢ t, f p.1 ⊓ f p.2

Tactic:
refine le_antisymm
    (iSup₂_le fun i ⟨his, hit⟩ ↦ le_iSup₂_of_le ⟨i, i⟩ ⟨his, hit⟩ (le_inf le_rfl le_rfl))
    (iSup₂_le fun ⟨i, j⟩ ⟨his, hjs⟩ ↦ ?_)

Goal state after:
α : Type u
inst✝ : Frame α
ι : Type u_1
f : ι → α
h : Pairwise (Disjoint on f)
s t : Set ι
x✝¹ : ι × ι
i j : ι
x✝ : (i, j) ∈ s ×ˢ t
his : (i, j).1 ∈ s
hjs : (i, j).2 ∈ t
⊢ f (i, j).1 ⊓ f (i, j).2 ≤ ⨆ i ∈ s ∩ t, f i
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case mpr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b c : α
hab : a ≤ b
hbc : b ≤ c
hfba : f b < f a
hfbc : f b < f c
⊢ ∃ a b, ∃ c ∈ [[a, b]], f c ∉ [[f a, f b]]

Tactic:
· exact ⟨a, c, b, Icc_subset_uIcc ⟨hab, hbc⟩, fun h => h.1.not_gt <| lt_min hfba hfbc⟩

Goal state after:
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
S T : A
⊢ ↑S ⊆ ↑T ∧ ↑S ≠ ↑T ↔ S ≤ T ∧ S ≠ T

Tactic:
coe_subset_coe,

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : SetLike A B
inst✝¹ : PartialOrder A
inst✝ : IsConcreteLE A B
S T : A
⊢ S ≤ T ∧ ↑S ≠ ↑T ↔ S ≤ T ∧ S ≠ T
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:
rw [mul, mul]

Goal state after:
α : 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 * f c ≤ f b * f c
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
h : 0 < n
⊢ n.pred ! * n.ascFactorial k = (n.pred + k)!

Tactic:
Nat.eq_add_of_sub_eq h rfl

Goal state after:
n k : ℕ
h : 0 < n
⊢ n.pred ! * (n - succ 0 + succ 0).ascFactorial k = (n.pred + k)!
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case succ
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
⊢ ∃ z, fract a * ↑c + fract a - fract (a * ↑c + a) = ↑z

Tactic:
rcases fract_add (a * c) a with ⟨y, hy⟩

Goal state after:
case succ
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
y : ℤ
hy : fract (a * ↑c + a) - fract (a * ↑c) - fract a = ↑y
⊢ ∃ z, fract a * ↑c + fract a - fract (a * ↑c + a) = ↑z
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr.inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
⊢ fract (↑(-↑m₀) / ↑n) = ↑(-↑m₀ % ↑n) / ↑n

Tactic:
let m₁ := q * ↑n - (↑m₀ : ℤ)

Goal state after:
case inr.inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
⊢ fract (↑(-↑m₀) / ↑n) = ↑(-↑m₀ % ↑n) / ↑n
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr.inr.calc_1
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ fract (-↑m₀ / ↑n) = fract (↑m₁ / ↑n)

Tactic:
rw [← fract_intCast_add q, ← mul_div_cancel_right₀ (q : k) hn.ne', ← add_div, ← sub_eq_add_neg]

Goal state after:
case inr.inr.calc_1
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ fract ((↑q * ↑n - ↑m₀) / ↑n) = fract (↑m₁ / ↑n)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr.inr.calc_2.e_a
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ (q * ↑n - ↑m₀) % ↑n = -↑m₀ % ↑n

Tactic:
sub_eq_add_neg,

Goal state after:
case inr.inr.calc_2.e_a
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
q : ℤ := ⌈↑m₀ / ↑n⌉
m₁ : ℤ := q * ↑n - ↑m₀
hm₁ : 0 ≤ m₁
⊢ (q * ↑n + -↑m₀) % ↑n = -↑m₀ % ↑n
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case inl
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
ha : a ≤ 0
n : ℕ
hn : c ^ n < b
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
exact ⟨n, ha.trans_lt (zpow_pos hc₀ _), mod_cast hn⟩

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

Goal state before:
pp: case inr.inl
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
ha : 0 < a
hb₁ : b ≤ 1
n : ℕ
hn : a < c ^ n ∧ c ^ n < b
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
exact ⟨n, mod_cast hn⟩

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

Goal state before:
pp: 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
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : K := ↑m.pred * δ
qny : q ^ n < y
q1y : |q| < max 1 y
xqn : max x 0 < q ^ n
⊢ ∃ q, 0 < q ∧ x < q ^ n ∧ q ^ n < y

Tactic:
exact ⟨q, lt_of_le_of_ne (by positivity) fun q0 ↦
    (le_sup_right.trans_lt xqn).ne <| q0 ▸ (zero_pow hn).symm, le_sup_left.trans_lt xqn, qny⟩

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

Goal state before:
pp: case coe.bot
G : Type u_1
M✝ : Type u_2
R : Type u_3
K : Type u_4
M : Type u_5
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : Archimedean M
y : M
hxy : 0 < ↑y
⊢ ∃ n, ⊥ ≤ n • ↑y

Tactic:
refine ⟨0, bot_le⟩

Goal state after: