mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case pos
m : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
h : findGreatest P n = 0
⊢ P (findGreatest P n)

Tactic:
cases m
    · rwa [h]
    exact ((findGreatest_eq_zero_iff.1 h) (zero_lt_succ _) hmb hm).elim

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

Goal state before:
pp: x y : WithZero (Multiplicative ℤ)
hx : x ≠ 0
hy : y ≠ 0
⊢ ∃ k, exp (-↑k) < x ∧ exp (-↑k) < y

Tactic:
obtain ⟨z, hz, hzx, hzy⟩ := WithZero.exists_ne_zero_and_le_and_le hx hy
  obtain ⟨k, hk⟩ := exists_exp_neg_natCast_lt hz
  grind

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

Goal state before:
pp: 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
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x * x ^ n + y * y ^ n + x * y ^ n + y * x ^ n = x * x ^ n + (x * y ^ n + y * y ^ n) + y * x ^ n

Tactic:
add_comm (x * y ^ n) (y * y ^ n),

Goal state after:
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
h1 : 0 ≤ x * y ^ n + y * x ^ n
h2 : 0 ≤ x + y
⊢ x * x ^ n + y * y ^ n + x * y ^ n + y * x ^ n = x * x ^ n + (y * y ^ n + x * y ^ n) + y * x ^ n
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
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ 2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a)) ≤
    2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * a + b ^ (n + 1) * b))

Tactic:
by
        gcongr _ * (_ + _ + ?_)
        · exact pow_nonneg zero_le_two _
        obtain hab | hba := le_total a b
        · exact mul_add_mul_le_mul_add_mul (by gcongr) hab
        · exact mul_add_mul_le_mul_add_mul' (by gcongr) hba

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

Goal state before:
pp: u : ℤ
hu : IsUnit u
⊢ u = 1 ∨ u = -1

Tactic:
simpa only [natAbs_of_isUnit hu] using! natAbs_eq u

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝¹⁸ : Zero K
inst✝¹⁷ : Add K
inst✝¹⁶ : Neg K
inst✝¹⁵ : Sub K
inst✝¹⁴ : One K
inst✝¹³ : Mul K
inst✝¹² : Inv K
inst✝¹¹ : Div K
inst✝¹⁰ : SMul ℕ K
inst✝⁹ : SMul ℤ K
inst✝⁸ : SMul ℚ≥0 K
inst✝⁷ : SMul ℚ K
inst✝⁶ : Pow K ℕ
inst✝⁵ : Pow K ℤ
inst✝⁴ : NatCast K
inst✝³ : IntCast K
inst✝² : NNRatCast K
inst✝¹ : RatCast K
f : K → L
hf : Injective f
inst✝ : DivisionSemiring L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q
q : ℚ≥0
⊢ ↑q = f (↑q.num / ↑q.den)

Tactic:
NNRat.cast_def,

Goal state after:
K : Type u_1
L : Type u_2
inst✝¹⁸ : Zero K
inst✝¹⁷ : Add K
inst✝¹⁶ : Neg K
inst✝¹⁵ : Sub K
inst✝¹⁴ : One K
inst✝¹³ : Mul K
inst✝¹² : Inv K
inst✝¹¹ : Div K
inst✝¹⁰ : SMul ℕ K
inst✝⁹ : SMul ℤ K
inst✝⁸ : SMul ℚ≥0 K
inst✝⁷ : SMul ℚ K
inst✝⁶ : Pow K ℕ
inst✝⁵ : Pow K ℤ
inst✝⁴ : NatCast K
inst✝³ : IntCast K
inst✝² : NNRatCast K
inst✝¹ : RatCast K
f : K → L
hf : Injective f
inst✝ : DivisionSemiring L
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : K), f (x + y) = f x + f y
mul : ∀ (x y : K), f (x * y) = f x * f y
inv : ∀ (x : K), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : K), f (x / y) = f x / f y
nsmul : ∀ (n : ℕ) (x : K), f (n • x) = n • f x
nnqsmul : ∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x
npow : ∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
nnratCast : ∀ (q : ℚ≥0), f ↑q = ↑q
q : ℚ≥0
⊢ ↑q.num / ↑q.den = f (↑q.num / ↑q.den)
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ |a| = |b| ↔ a * a = b * b

Tactic:
rw [← abs_mul_abs_self, ← abs_mul_abs_self b]

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ |a| = |b| ↔ |a| * |a| = |b| * |b|
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ |a| < |b| ↔ a * a < b * b

Tactic:
rw [← abs_mul_abs_self, ← abs_mul_abs_self b]

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ |a| < |b| ↔ |a| * |a| < |b| * |b|
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ |a| ≤ |b| ↔ a * a ≤ b * b

Tactic:
rw [← abs_mul_abs_self, ← abs_mul_abs_self b]

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ |a| ≤ |b| ↔ |a| * |a| ≤ |b| * |b|
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: α : Type u_1
β : Type u_2
a✝¹ b c d : α
inst✝¹ : Preorder α
inst✝ : Preorder β
a✝ : (Antisymmetrization α fun x1 x2 ↦ x1 ≤ x2)ᵒᵈ
a : α
⊢ Quotient.map' id ⋯ (Quotient.map' id ⋯ (Quotient.mk'' a)) = Quotient.mk'' a

Tactic:
simp_rw [Quotient.map'_mk'', id]

Goal state after:
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: α : Type u_1
β : Type u_2
a✝¹ b c d : α
inst✝¹ : Preorder α
inst✝ : Preorder β
a✝ : Antisymmetrization αᵒᵈ fun x1 x2 ↦ x1 ≤ x2
a : αᵒᵈ
⊢ Quotient.map' id ⋯ (Quotient.map' id ⋯ (Quotient.mk'' a)) = Quotient.mk'' a

Tactic:
simp_rw [Quotient.map'_mk'', id]

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
⊢ range f = range g → f = g

Tactic:
hfg

Goal state after:
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
⊢ f = g
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
⊢ ↑(t \ s) ⊕ ↑(s ∩ t) ≃ ↑(t \ s ∪ s ∩ t)

Tactic:
by
          refine (Set.union' (· ∉ s) ?_ ?_).symm
          exacts [fun x hx => hx.2, fun x hx => not_not_intro hx.1]

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ Icc a b \ (Icc a b \ {a, b}) = {a, b}

Tactic:
sdiff_sdiff_cancel_left

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ {a, b} = {a, b}

α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ {a, b} ⊆ Icc a b
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: α : Type u
inst✝ : Inhabited α
l₁ l₂ : List α
n : ℕ
h : l₁.length = n
⊢ takeI n (l₁ ++ l₂) = l₁

Tactic:
rw [← h]

Goal state after:
α : Type u
inst✝ : Inhabited α
l₁ l₂ : List α
n : ℕ
h : l₁.length = n
⊢ takeI l₁.length (l₁ ++ l₂) = l₁
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: α : Type u
l₁ l₂ : List α
n : ℕ
a : α
h : l₁.length = n
⊢ takeD n (l₁ ++ l₂) a = l₁

Tactic:
rw [← h]

Goal state after:
α : Type u
l₁ l₂ : List α
n : ℕ
a : α
h : l₁.length = n
⊢ takeD l₁.length (l₁ ++ l₂) a = l₁
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| ≤ 1 ∧ |q - r| ≤ ε / (1 + ↑n * (B + 1) ^ (n - 1))
⊢ |q - r| * ↑n * max |q| |r| ^ (n - 1) < ε

Tactic:
le_div_iff₀ pos,

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 swap'
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
x✝ y✝ : α
l₁✝ l₂✝ : List α
h✝ : l₁✝ ~ l₂✝
r : ∀ (b : β), foldr f b l₁✝ = foldr f b l₂✝
b : β
⊢ foldr f b (y✝ :: x✝ :: l₁✝) = foldr f b (x✝ :: y✝ :: l₂✝)

Tactic:
simp only [foldr_cons]; rw [lcomm.left_comm, r b]

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

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

Tactic:
reverse_append

Goal state after:
α : Type u
l : List α
a : α
⊢ [a].reverse ++ l.reverse = a :: l.reverse
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
h : a = 0 ∧ n = 0
⊢ (a = 0 → ¬n = 0) → a ^ n = 0

pp: case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
h : ¬(a = 0 ∧ n = 0)
⊢ a = 0 → ¬n = 0

Tactic:
· tauto

Goal state after:
case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
h : ¬(a = 0 ∧ n = 0)
⊢ a = 0 → ¬n = 0
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
h : ¬(a = 0 ∧ n = 0)
⊢ a = 0 → ¬n = 0

Tactic:
· tauto

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

Goal state before:
pp: α : Type u
l : List α
⊢ (Surjective fun n ↦ l[n]?) ↔ ∀ (x : α), x ∈ l

Tactic:
refine ⟨fun h x ↦ mem_iff_getElem?.mpr <| h x, fun h x ↦ ?_⟩
  cases x with
  | none => exact ⟨l.length, getElem?_eq_none <| Nat.le_refl _⟩
  | some x => exact mem_iff_getElem?.mp <| h x

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
ha : a ∈ l
⊢ a ∈ l.dropLast ↔ idxOf a l < l.length - 1

Tactic:
dropLast_eq_take,

Goal state after:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
ha : a ∈ l
⊢ a ∈ take (l.length - 1) l ↔ idxOf a l < l.length - 1
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l₁ l₂ : List α
inst✝ : Inhabited α
hl : l₁.length = l₂.length
h : ∀ (n : ℕ), l₁[n]! = l₂[n]!
n : ℕ
h₁ : n < l₁.length
h₂ : n < l₂.length
⊢ l₁[n] = l₂[n]

Tactic:
simpa only [← getElem!_pos] using h n

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

Goal state before:
pp: q : ℚ
hq : q.den = 1
| q

Tactic:
← num_divInt_den q,

Goal state after:
q : ℚ
hq : q.den = 1
| q.num /. ↑q.den
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: p q : ℚ≥0
⊢ p < q ↔ p.num * q.den < q.num * p.den

Tactic:
by
  rw [← NNRat.coe_lt_coe, Rat.lt_iff]; norm_cast

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 (z * x) ↔ IsRelPrime y z

Tactic:
by
  rw [mul_comm, isRelPrime_mul_unit_left_right hu]

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

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p = ↑q
⊢ p = q

Tactic:
NNRat.cast_def,

Goal state after:
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num / ↑p.den = ↑q
⊢ p = q
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num / ↑p.den = ↑q
⊢ p = q

Tactic:
NNRat.cast_def,

Goal state after:
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p.num / ↑p.den = ↑q.num / ↑q.den
⊢ p = q
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q r : ℚ
hqd : ↑q.den ≠ 0
hrd : ↑r.den ≠ 0
| q + r

Tactic:
← num_divInt_den q,

Goal state after:
q r : ℚ
hqd : ↑q.den ≠ 0
hrd : ↑r.den ≠ 0
| q.num /. ↑q.den + r
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
⊢ False

Tactic:
rcases show (d : ℤ) ∣ b by rwa [e] at dd with ⟨k, ke⟩

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
d0 : ↑d = 0
dd : ↑(a /. b).den ∣ b
k : ℤ
ke : b = ↑d * k
⊢ False
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
q : ℚ
hq : ↑q.num ≠ 0
⊢ ↑q⁻¹ = (↑q)⁻¹

Tactic:
rw [inv_def, cast_divInt_of_ne_zero _ hq, cast_def, inv_div, Int.cast_natCast]

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

Goal state before:
pp: F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : FunLike F α β
inst✝² : DivisionSemiring α
inst✝¹ : DivisionSemiring β
inst✝ : RingHomClass F α β
f : F
q : ℚ≥0
⊢ f ↑q = ↑q

Tactic:
NNRat.cast_def,

Goal state after:
F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : FunLike F α β
inst✝² : DivisionSemiring α
inst✝¹ : DivisionSemiring β
inst✝ : RingHomClass F α β
f : F
q : ℚ≥0
⊢ f (↑q.num / ↑q.den) = ↑q.num / ↑q.den
Module: Mathlib.Tactic.Ring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
n n' : ℕ
r : R
hr : ↑n = r
hn : n' = n
a : R
⊢ n' • a = r * a

Tactic:
subst_vars
  simp only [nsmul_eq_mul]

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

Goal state before:
pp: case inl
R : Type u
inst✝⁶ : NonUnitalNonAssocSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hab : a ≤ b
⊢ (a - b) * c = a * c - b * c

Tactic:
tsub_eq_zero_iff_le.2 hab,

Goal state after:
case inl
R : Type u
inst✝⁶ : NonUnitalNonAssocSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : CanonicallyOrderedAdd R
inst✝³ : Sub R
inst✝² : OrderedSub R
inst✝¹ : Std.Total fun x1 x2 ↦ x1 ≤ x2
inst✝ : MulRightMono R
a b c : R
h : AddLECancellable (b * c)
hab : a ≤ b
⊢ 0 * c = a * c - b * c
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
⊢ u 0 ⊔ ⨆ i, u (i + 1) = ⨆ x ∈ {0} ∪ range Nat.succ, u x

Tactic:
{ rw [iSup_union, iSup_singleton, iSup_range] }

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

Goal state before:
pp: ι : Type u_12
α : Type u_13
s : Set ι
hs : s.Nonempty
f : ι → Set α
t : Set α
⊢ ⋂ i ∈ s, t ∩ f i = ⋂ i ∈ s, f i ∩ t

Tactic:
simp [inter_comm]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
f : ι → Set α
⊢ ⋂ i, f i = ∅ ↔ ∀ (x : α), ∃ i, x ∉ f i

Tactic:
simp [Set.eq_empty_iff_forall_notMem]

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

Goal state before:
pp: α : Type u_1
c : Set (Set α)
⊢ ⋂₀ c = ∅ ↔ ∀ (a : α), ∃ b ∈ c, a ∉ b

Tactic:
simp [Set.eq_empty_iff_forall_notMem]

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

Goal state before:
pp: α : Type u_1
s t : Set α
S : Set (Set α)
hs : t ∈ S
h : s ∩ ⋃₀ S = ∅
⊢ s ∩ t ⊆ ∅

Tactic:
rw [← h]

Goal state after:
α : Type u_1
s t : Set α
S : Set (Set α)
hs : t ∈ S
h : s ∩ ⋃₀ S = ∅
⊢ s ∩ t ⊆ s ∩ ⋃₀ S
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ a, ⨆ b, g a b
rhs : α✝ := ⨆ h, ⨅ a, g a (h a)
h : ¬∃ x, rhs < x ∧ x < lhs
hrl : rhs < lhs
⊢ lhs ≤ rhs

Tactic:
replace h : ∀ x, x ≤ rhs ∨ lhs ≤ x := by
        simpa only [not_exists, not_and_or, not_or, not_lt] using h

Goal state after:
α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ a, ⨆ b, g a b
rhs : α✝ := ⨆ h, ⨅ a, g a (h a)
hrl : rhs < lhs
h : ∀ (x : α✝), x ≤ rhs ∨ lhs ≤ x
⊢ lhs ≤ rhs
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

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

pp: case pos.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ∀ b_1 ∈ (fun a ↦ ↑a) ⁻¹' s, b_1 ≤ b

Tactic:
· rcases hs with ⟨⟨⟩ | b, hb⟩
        · exact absurd hb h₁
        · exact ⟨b, hb⟩

Goal state after:
case pos.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∉ s
h₂ : BddAbove ((fun a ↦ ↑a) ⁻¹' s)
b : β
hb : Option.some b ∈ upperBounds s
⊢ ∀ b_1 ∈ (fun a ↦ ↑a) ⁻¹' s, b_1 ≤ b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ lowerBounds s
b : WithTop β
hb : b ∈ s
⊢ b ∈ {⊤}

Tactic:
exact Set.mem_singleton_iff.2 (top_le_iff.1 (ha hb))

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case inr
α : Type u_1
ι : Type u_4
s : Set ι
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
x : α
hx₁ : x ∈ f i
hx₂ : x ∈ f j
h_lt : j < i
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ i < j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
· exact ⟨j, hj, i, hi, h_lt, x, hx₂, hx₁⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
E : Type u_3
inst✝¹ : EquivLike E α β
inst✝ : OrderIsoClass E α β
e : E
⊢ (range ⇑e).OrdConnected

Tactic:
by
  simp_rw [← image_univ]
  exact ordConnected_image (e : α ≃o β)

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
hS : S.Nonempty
⊢ sSup (Subtype.val '' S) ∈ Icc a b

Tactic:
refine ⟨?_, csSup_le (hS.image Subtype.val) (fun _ ⟨c, _, hc⟩ ↦ hc ▸ c.2.2)⟩

Goal state after:
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
hS : S.Nonempty
⊢ a ≤ sSup (Subtype.val '' S)
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
p q : ℚ≥0
h : p < q
⊢ ↑p < ↑q

Tactic:
NNRat.cast_def,

Goal state after:
K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
p q : ℚ≥0
h : p < q
⊢ ↑p.num / ↑p.den < ↑q
Module: Mathlib.Data.Rat.Cast.Order

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
p q : ℚ≥0
h : p < q
⊢ ↑p.num / ↑p.den < ↑q

Tactic:
NNRat.cast_def,

Goal state after:
K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
p q : ℚ≥0
h : p < q
⊢ ↑p.num / ↑p.den < ↑q.num / ↑q.den
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

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

case inr
ι : Type u_1
M : Type u_3
inst✝¹ : One M
inst✝ : DecidableEq ι
f : ι → M
x : ι
y : M
hy : y ≠ 1
a : ι
hne : a ≠ x
⊢ a ∈ mulSupport (update f x y) ↔ a ∈ insert x (mulSupport f)
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

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

case inr
ι : Type u_1
M : Type u_3
inst✝¹ : One M
inst✝ : DecidableEq ι
f : ι → M
x a : ι
hne : a ≠ x
⊢ a ∈ mulSupport (update f x 1) ↔ a ∈ mulSupport f \ {x}
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Group α
a : α
⊢ a⁺ᵐ = if 1 < a then a else 1

Tactic:
by
  grind [oneLePart_eq_ite]

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

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

Tactic:
succ_add_sub_one,

Goal state after:
n k : ℕ
⊢ (n + k - k) * n.succ.ascFactorial k = n * n.succ.ascFactorial k
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
q : ℚ≥0
⊢ ↑(↑q).num / ↑(↑q).den = ↑q

Tactic:
NNRat.cast_def,

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
q : ℚ≥0
⊢ ↑(↑q.num / ↑q.den).num / ↑(↑q.num / ↑q.den).den = ↑q
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: m n : ℕ+
h : n.mod m = m
⊢ m ≤ n

Tactic:
rw [← h]

Goal state after:
m n : ℕ+
h : n.mod m = m
⊢ n.mod m ≤ n
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
n : ℕ
hn : n ≠ 0
a : R
⊢ 0 < ↑n

Tactic:
positivity

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

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
n : ℕ
⊢ ⌊a / ↑n⌋ = ⌊a⌋ / ↑n

Tactic:
simpa using floor_div_cast_of_nonneg n.cast_nonneg a

Goal state after:
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
m : ℤ
a : R
⊢ fract (↑m + a) = fract a

Tactic:
rw [add_comm, fract_add_intCast]

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h : fract a = b
⊢ 0 ≤ b ∧ b < 1 ∧ ∃ z, a - b = ↑z

Tactic:
rw [← h]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h : fract a = b
⊢ 0 ≤ fract a ∧ fract a < 1 ∧ ∃ z, a - fract a = ↑z
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr.refine_1
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ 0 ≤ ↑(m % n) / ↑n

Tactic:
positivity

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

Goal state before:
pp: n d : ℕ
⊢ 0 ≤ ↑n / ↑d

Tactic:
positivity

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

Goal state before:
pp: α : Type u_1
q : ℚ≥0
hq : 0 < q
⊢ 0 < q.num

Tactic:
positivity

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

Goal state before:
pp: α : Type u_1
q : ℚ≥0
hq : q ≠ 0
⊢ q.num ≠ 0

Tactic:
positivity

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

Goal state before:
pp: α : Type u_1
q : ℚ≥0
⊢ 0 < q.den

Tactic:
positivity

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

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

Tactic:
positivity

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

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉ / b < a
hab : a ≤ (b - 1)⁻¹
⊢ 0 < b

Tactic:
positivity

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

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ b - 1 ≠ 0

Tactic:
positivity

Goal state after: