mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
⊢ c⁻¹ ≤ a / b ∧ a / b ≤ c ↔ a / b ≤ c ∧ b / a ≤ c

Tactic:
inv_le_div_iff_le_mul,

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b c : G
⊢ b ≤ a * c ∧ a / b ≤ c ↔ a / b ≤ c ∧ b / a ≤ c
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
⊢ |(a ⊔ c) / (b ⊔ c)|ₘ * |?m.37|ₘ ≤ |a / b|ₘ

Tactic:
mabs_div_sup_mul_mabs_div_inf

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
⊢ |a / b|ₘ ≤ |a / b|ₘ
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
⊢ |?m.37|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ ≤ |a / b|ₘ

Tactic:
mabs_div_sup_mul_mabs_div_inf

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b c : α
⊢ |a / b|ₘ ≤ |a / b|ₘ
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case H1
x y a b : ℕ
h : 0 < a
IH : ∀ {s t s' t' : ℤ}, x.P y (b % a, s, t) → x.P y (a, s', t') → x.P y ((b % a).xgcdAux s t a s' t')
s t s' t' : ℤ
p : x.P y (a, s, t)
p' : x.P y (b, s', t')
⊢ x.P y ((b % a).xgcdAux (s' - ↑b / ↑a * s) (t' - ↑b / ↑a * t) a s t)

Tactic:
refine IH ?_ p

Goal state after:
case H1
x y a b : ℕ
h : 0 < a
IH : ∀ {s t s' t' : ℤ}, x.P y (b % a, s, t) → x.P y (a, s', t') → x.P y ((b % a).xgcdAux s t a s' t')
s t s' t' : ℤ
p : x.P y (a, s, t)
p' : x.P y (b, s', t')
⊢ x.P y (b % a, s' - ↑b / ↑a * s, t' - ↑b / ↑a * t)
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
h : (∃ a, (map' f) a = 0) ∧ ∀ (a : β), ∃ a_1, (map' f) a_1 = ↑a
b : β
a : WithZero α
hab : (map' f) a = ↑b
⊢ ∃ a, f a = b

Tactic:
induction a using WithZero.recZeroCoe

Goal state after:
case refine_1.zero
α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
h : (∃ a, (map' f) a = 0) ∧ ∀ (a : β), ∃ a_1, (map' f) a_1 = ↑a
b : β
hab : (map' f) 0 = ↑b
⊢ ∃ a, f a = b

case refine_1.coe
α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
h : (∃ a, (map' f) a = 0) ∧ ∀ (a : β), ∃ a_1, (map' f) a_1 = ↑a
b : β
a✝ : α
hab : (map' f) ↑a✝ = ↑b
⊢ ∃ a, f a = b
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
x✝ : G
⊢ (fun n ↦ recZeroCoe 0 Units.val n) ((fun a ↦ if h : a = 0 then 0 else ↑(Units.mk0 a h)) x✝) = x✝

Tactic:
by simp only; split <;> simp_all

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
a b : α
inst✝ : LE α
hx : ⊥ = ⊥ → a ≤ b
⊢ unbotD a ⊥ ≤ b ↔ ⊥ ≤ ↑b

Tactic:
simp [hx]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe
α : Type u_1
a b : α
inst✝ : LE α
a✝ : α
hx : ↑a✝ = ⊥ → a ≤ b
⊢ unbotD a ↑a✝ ≤ b ↔ ↑a✝ ≤ ↑b

Tactic:
simp [hx]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
a b : α
inst✝ : LT α
hx : ⊥ = ⊥ → a < b
⊢ unbotD a ⊥ < b ↔ ⊥ < ↑b

Tactic:
simp [hx]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe
α : Type u_1
a b : α
inst✝ : LT α
a✝ : α
hx : ↑a✝ = ⊥ → a < b
⊢ unbotD a ↑a✝ < b ↔ ↑a✝ < ↑b

Tactic:
simp [hx]

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

Goal state before:
pp: P : ℤ → Prop
inst✝ : DecidablePred P
b : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hinh : ∃ z, P z
Hbdd' : ∀ (z : ℤ), P (-z) → -b ≤ z
Hinh' : ∃ z, P (-z)
lb : ℤ
Plb : P (-lb)
al : ∀ (z : ℤ), P (-z) → lb ≤ z
z : ℤ
h : P z
⊢ P (- -z)

Tactic:
by rwa [neg_neg]

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

Goal state before:
pp: case zero
α : Type u_1
inst✝ : LE α
a b : α
hx : 0 = 0 → a ≤ b
⊢ unzeroD a 0 ≤ b ↔ 0 ≤ ↑b

Tactic:
simp [hx]

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

Goal state before:
pp: case coe
α : Type u_1
inst✝ : LE α
a b a✝ : α
hx : ↑a✝ = 0 → a ≤ b
⊢ unzeroD a ↑a✝ ≤ b ↔ ↑a✝ ≤ ↑b

Tactic:
simp [hx]

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

Goal state before:
pp: case zero
α : Type u_1
inst✝ : LT α
a b : α
hx : 0 = 0 → a < b
⊢ unzeroD a 0 < b ↔ 0 < ↑b

Tactic:
simp [hx]

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

Goal state before:
pp: case coe
α : Type u_1
inst✝ : LT α
a b a✝ : α
hx : ↑a✝ = 0 → a < b
⊢ unzeroD a ↑a✝ < b ↔ ↑a✝ < ↑b

Tactic:
simp [hx]

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
⊢ 1 ≤ ⌈a⌉₊ ↔ 0 < a

Tactic:
rw [← zero_add 1, Nat.add_one_le_ceil_iff, Nat.cast_zero]

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

Goal state before:
pp: case inr.inl
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 : a ≤ ↑n
⊢ ⌊a⌋₊ ≤ n

Tactic:
exact Nat.cast_le.1 ((Nat.floor_le ha).trans h)

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : AddUnits R
⊢ -(-y).mulLeft ↑(-x) = -y.mulLeft ↑x

Tactic:
← y.neg_mulLeft,

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
x y : AddUnits R
⊢ - -y.mulLeft ↑(-x) = -y.mulLeft ↑x
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
a b c : K
hc : c ≠ 0
⊢ b + a / c = (a + b * c) / c

Tactic:
add_div',

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
a b c : K
hc : c ≠ 0
⊢ (b * c + a) / c = (a + b * c) / c

case hc
K : Type u_1
inst✝ : DivisionSemiring K
a b c : K
hc : c ≠ 0
⊢ c ≠ 0
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
hn : Odd 0
⊢ False

Tactic:
simp [Odd] at hn

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

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

Tactic:
simpa only [one_pow, abs_one] using sq_le_sq (a := a) (b := 1)

Goal state after:
Module: Mathlib.Order.Antisymmetrization

Goal state before:
pp: α : Type u_1
a b : α
inst✝ : Preorder α
⊢ a ≤ b ↔ a < b ∨ AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) a b

Tactic:
rw [lt_iff_le_not_ge, AntisymmRel]

Goal state after:
α : Type u_1
a b : α
inst✝ : Preorder α
⊢ a ≤ b ↔ a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
⊢ ⇑(ofInjective f hf).symm = rangeSplitting f

Tactic:
by
  ext ⟨y, x, rfl⟩
  apply hf
  simp [apply_rangeSplitting f]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
n : ℤ
m : ℕ
⊢ IsNat n m → IsNat (↑n) m

Tactic:
by rintro ⟨⟨⟩⟩; exact ⟨by simp⟩

Goal state after:
Module: Mathlib.Control.Functor

Goal state before:
pp: F : Type u_1 → Type u_2
m : {α β : Type u_1} → (α → β) → F α → F β
mc : {α β : Type u_1} → α → F β → F α
m' : {α β : Type u_1} → (α → β) → F α → F β
mc' : {α β : Type u_1} → α → F β → F α
H1 : LawfulFunctor F
H2 : LawfulFunctor F
H : ∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x
α β : Type u_1
f : α → β
x : F α
⊢ m f x = m' f x

Tactic:
apply H

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

Goal state before:
pp: case cons
M : Type u_2
inst✝ : MulOneClass M
l✝ : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
a : M
l : List M
ih : l ≠ [] → (∀ (x : M), x ∈ l → p x) → p l.prod
hl : a :: l ≠ []
base : ∀ (x : M), x ∈ a :: l → p x
⊢ p (a :: l).prod

Tactic:
by_cases hl_empty : l = []

Goal state after:
case pos
M : Type u_2
inst✝ : MulOneClass M
l✝ : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
a : M
l : List M
ih : l ≠ [] → (∀ (x : M), x ∈ l → p x) → p l.prod
hl : a :: l ≠ []
base : ∀ (x : M), x ∈ a :: l → p x
hl_empty : l = []
⊢ p (a :: l).prod

case neg
M : Type u_2
inst✝ : MulOneClass M
l✝ : List M
p : M → Prop
hom : ∀ (a b : M), p a → p b → p (a * b)
a : M
l : List M
ih : l ≠ [] → (∀ (x : M), x ∈ l → p x) → p l.prod
hl : a :: l ≠ []
base : ∀ (x : M), x ∈ a :: l → p x
hl_empty : ¬l = []
⊢ p (a :: l).prod
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑(na * nb) = ↑(k * nc)
⊢ ↑na * ⅟↑da * (↑nb * ⅟↑db) = ↑nc * ⅟↑dc

Tactic:
simp only [Nat.cast_mul] at h₁

Goal state after:
α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
⊢ ↑na * ⅟↑da * (↑nb * ⅟↑db) = ↑nc * ⅟↑dc
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
⊢ 0 < (-a)⁻¹ ↔ a < 0

Tactic:
inv_pos,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a : α
⊢ 0 < -a ↔ a < 0
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case inr.inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb : 0 < b
⊢ a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a

Tactic:
simp [hb, hb.not_gt, div_lt_one, hb.ne.symm]

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

Goal state before:
pp: case inr
α : Type u
l : List α
n : ℕ
a b : α
h : a ∈ l.insertIdx n b
hn : l.length ≥ n
⊢ a = b ∨ a ∈ l

Tactic:
| inr hn =>

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

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

Tactic:
| inr hn₂ =>

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
n : ℤ
hn : ¬n = 0
⊢ 0 ^ n = 0

Tactic:
exact zero_zpow n hn

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
l : List M
y : M
h : ∀ (x : M), x ∈ l → Commute y x
⊢ Commute y l.prod

Tactic:
induction l with
  | nil => simp
  | cons z l IH =>
    rw [List.forall_mem_cons] at h
    rw [List.prod_cons]
    exact Commute.mul_right h.1 (IH h.2)

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

Goal state before:
pp: α : Type u
inst✝ : Inhabited α
t s : List α
h : s ≠ []
⊢ (s ++ t).head! = s.head!

Tactic:
induction s

Goal state after:
case nil
α : Type u
inst✝ : Inhabited α
t : List α
h : [] ≠ []
⊢ ([] ++ t).head! = [].head!

case cons
α : Type u
inst✝ : Inhabited α
t : List α
head✝ : α
tail✝ : List α
tail_ih✝ : tail✝ ≠ [] → (tail✝ ++ t).head! = tail✝.head!
h : head✝ :: tail✝ ≠ []
⊢ (head✝ :: tail✝ ++ t).head! = (head✝ :: tail✝).head!
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: q a✝ b c : ℚ
C : ℚ → Sort u_1
a : ℚ
div : (n : ℤ) → (d : ℕ) → d ≠ 0 → n.natAbs.Coprime d → C (↑n / ↑d)
n : ℤ
d : ℕ
nz : d ≠ 0
red : n.natAbs.Coprime d
⊢ C { num := n, den := d, den_nz := nz, reduced := red }

Tactic:
Rat.mk_eq_divInt,

Goal state after:
q a✝ b c : ℚ
C : ℚ → Sort u_1
a : ℚ
div : (n : ℤ) → (d : ℕ) → d ≠ 0 → n.natAbs.Coprime d → C (↑n / ↑d)
n : ℤ
d : ℕ
nz : d ≠ 0
red : n.natAbs.Coprime d
⊢ C (n /. ↑d)
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: a b : ℤ
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 }
⊢ { num := n, den := d, den_nz := h, reduced := c }.num ∣ a

Tactic:
Rat.mk_eq_divInt,

Goal state after:
a b : ℤ
b0 : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = n /. ↑d
⊢ { num := n, den := d, den_nz := h, reduced := c }.num ∣ a
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
e : divNat a b = ⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩
hd : ↑d ≠ 0
hb' : b ≠ 0
⊢ ↑⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩ = ↑a / ↑b

Tactic:
Rat.mk_eq_divInt,

Goal state after:
α : Type u_3
inst✝ : DivisionSemiring α
a b : ℕ
hb : ↑b ≠ 0
d : ℕ
h : d ≠ 0
n : ℕ
c : (↑n).natAbs.Coprime d
hn : 0 ≤ { num := ↑n, den := d, den_nz := h, reduced := c }
hd : ↑d ≠ 0
hb' : b ≠ 0
e : divNat a b = ⟨Rat.divInt ↑n ↑d, ⋯⟩
⊢ ↑⟨{ num := ↑n, den := d, den_nz := h, reduced := c }, hn⟩ = ↑a / ↑b
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑(p * q) = ↑p * ↑q

Tactic:
rw [mul_eq_mkRat, cast_mkRat_of_ne_zero, cast_def, cast_def,
    (Nat.commute_cast _ _).div_mul_div_comm (Int.commute_cast _ _)]

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑(p.num * q.num) / ↑(p.den * q.den) = ↑p.num * ↑q.num / (↑p.den * ↑q.den)

case hb
α : Type u_3
inst✝ : DivisionRing α
p q : ℚ
hp : ↑p.den ≠ 0
hq : ↑q.den ≠ 0
⊢ ↑(p.den * q.den) ≠ 0
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case mp
m n : ℤ
hn : ↑n ≠ 0
⊢ (↑m / ↑n).den = 1 → n ∣ m

pp: case mpr
m n : ℤ
hn : ↑n ≠ 0
⊢ n ∣ m → (↑m / ↑n).den = 1

Tactic:
· rw [Rat.den_eq_one_iff, eq_div_iff hn]
    exact mod_cast (Dvd.intro_left _)

Goal state after:
case mpr
m n : ℤ
hn : ↑n ≠ 0
⊢ n ∣ m → (↑m / ↑n).den = 1
Module: Mathlib.Order.GaloisConnection.Basic

Goal state before:
pp: α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
gi : GaloisInsertion l u
a b : β
⊢ l (u a) ⊔ l (u b) = a ⊔ b

Tactic:
by simp only [gi.l_u_eq]

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

Goal state before:
pp: α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
gi : GaloisInsertion l u
a b : β
⊢ l (u (a ⊓ b)) = a ⊓ b

Tactic:
by simp only [gi.l_u_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : SupSet α
g : β → α
f : ι → β
⊢ sSup (g '' range f) = sSup (range fun i ↦ g (f i))

Tactic:
← range_comp'

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : SupSet α
g : β → α
f : ι → β
⊢ sSup (range fun x ↦ g (f x)) = sSup (range fun i ↦ g (f i))
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
S : Set (Set α)
⊢ (⋂₀ S)ᶜ = ⋃₀ (compl '' S)

Tactic:
rw [sUnion_eq_compl_sInter_compl, compl_compl_image]

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Sort u_4
ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → ConditionallyCompleteLattice (α i)
x✝¹ : Set ((i : ι) → α i)
hn : x✝¹.Nonempty
hb : BddBelow x✝¹
x✝ : ι
⊢ IsGLB (eval x✝ '' x✝¹) (sInf (eval x✝ '' x✝¹))

Tactic:
exact isGLB_csInf (image_nonempty.mpr hn) ((monotone_eval _).map_bddBelow hb)

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

Goal state before:
pp: case hs
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
⊢ ∀ x ∈ ⋃ i, Iic (f i), ∃ y ∈ range fun i ↦ f i, x ≤ y

Tactic:
rintro x ⟨-, ⟨i, rfl⟩, hi⟩
    exact ⟨f i, mem_range_self _, hi⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DistribLattice α
a b c : α
⊢ b ∈ [[a, c]] → c ∈ [[a, b]] → b = c

Tactic:
by
  simpa only [uIcc_comm a] using eq_of_mem_uIcc_of_mem_uIcc

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
s : Set ι
f : ι → α
⊢ (s.PairwiseDisjoint fun i ↦ {f i}) ↔ InjOn f s

Tactic:
simp [PairwiseDisjoint, InjOn, Set.Pairwise, not_imp_not]

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
f : α → β
h : ∀ ⦃a b : α⦄, r' (f a) (f b) → r a b
⊢ IsAntichain r' (f '' s)

Tactic:
rintro _ ⟨b, hb, rfl⟩ _ ⟨c, hc, rfl⟩ hbc hr

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
f : α → β
h : ∀ ⦃a b : α⦄, r' (f a) (f b) → r a b
b : α
hb : b ∈ s
c : α
hc : c ∈ s
hbc : f b ≠ f c
hr : r' (f b) (f c)
⊢ False
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
⊢ IsAntichain r' (⇑φ '' s)

Tactic:
by
  intro b hb b' hb' h₁ h₂
  rw [Set.mem_image] at hb hb'
  obtain ⟨⟨a, has, rfl⟩, ⟨a', has', rfl⟩⟩ := hb, hb'
  exact hs has has' (fun haa' => h₁ (by rw [haa'])) (φ.map_rel_iff.mp h₂)

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
h : (s ∩ Icc x y).OrdConnected
z : α
hz : z ∈ Icc x y
hxy : x ≤ y
⊢ z ∈ s

Tactic:
exact h.out ⟨hx, left_mem_Icc.2 hxy⟩ ⟨hy, right_mem_Icc.2 hxy⟩ hz |>.1

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
⊢ extend f g 1 x = 1

Tactic:
by_cases hf : ∃ a, f a = x

Goal state after:
case pos
ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
hf : ∃ a, f a = x
⊢ extend f g 1 x = 1

case neg
ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
hf : ¬∃ a, f a = x
⊢ extend f g 1 x = 1
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: i n : ℕ
⊢ i + (n + 1)! ≤ (i + (n + 1))!

Tactic:
cases (le_or_gt (2 : ℕ) i)
  · rw [← Nat.add_assoc]
    apply Nat.le_of_lt
    apply add_factorial_succ_lt_factorial_add_succ
    assumption
  · match i with
    | 0 => simp
    | 1 =>
      rw [← Nat.add_assoc, factorial_succ (1 + n), Nat.add_mul, Nat.one_mul, Nat.add_comm 1 n,
        Nat.add_le_add_iff_right]
      exact Nat.mul_pos n.succ_pos n.succ.factorial_pos
    | succ (succ n) => contradiction

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

Goal state before:
pp: n : ℕ
⊢ n * 1 = n * n.ascFactorial 0

Tactic:
ascFactorial_zero

Goal state after:
n : ℕ
⊢ n * 1 = n * 1
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DivisionRing α
p : ℚ
n : ℕ
⊢ ↑(p.num ^ n) / ↑(p.den ^ n) = (↑p.num / ↑p.den) ^ n

Tactic:
Nat.cast_pow,

Goal state after:
α : Type u_1
inst✝ : DivisionRing α
p : ℚ
n : ℕ
⊢ ↑(p.num ^ n) / ↑p.den ^ n = (↑p.num / ↑p.den) ^ n
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
n : ℕ
⊢ ↑(q.num ^ n) / ↑(q.den ^ n) = (↑q.num / ↑q.den) ^ n

Tactic:
Nat.cast_pow,

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
n : ℕ
⊢ ↑q.num ^ n / ↑(q.den ^ n) = (↑q.num / ↑q.den) ^ n
Module: Mathlib.Data.Rat.Cast.Lemmas

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
n : ℕ
⊢ ↑q.num ^ n / ↑(q.den ^ n) = (↑q.num / ↑q.den) ^ n

Tactic:
Nat.cast_pow,

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
n : ℕ
⊢ ↑q.num ^ n / ↑q.den ^ n = (↑q.num / ↑q.den) ^ n
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inl.inl
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 2 * fract x ≠ 1
m : ℤ
hm : ↑(m + m) = 2 * x
⊢ round x = (m + m) / 2

Tactic:
obtain rfl : m = x := mul_left_cancel₀ two_ne_zero <| by simp [← hm, ← two_mul]
      rw [round_intCast, ← two_mul, Int.mul_ediv_cancel_left _ two_ne_zero]

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

Goal state before:
pp: case pos
a b : ℕ+
h : b < a
⊢ ↑(↑a - ↑b).toPNat' = ↑a - ↑b

Tactic:
exact toPNat'_coe (tsub_pos_of_lt h)

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

Goal state before:
pp: case mpr
k m : ℕ+
⊢ m.mod k = k → ↑m % ↑k = 0

Tactic:
intro h
    by_cases h' : (m : ℕ) % (k : ℕ) = 0
    · exact h'
    · replace h : (mod m k : ℕ) = (k : ℕ) := congr_arg _ h
      rw [mod_coe, if_neg h'] at h
      exact ((Nat.mod_lt (m : ℕ) k.pos).ne h).elim

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
a b : R
⊢ fract (a + b) - fract a - fract b = ↑(⌊a⌋ + ⌊b⌋ - ⌊a + b⌋)

Tactic:
by unfold fract; grind

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

Goal state before:
pp: q : ℚ
⊢ ⌈q⌉ = -(-q.num / ↑q.den)

Tactic:
change -⌊-q⌋ = _

Goal state after:
q : ℚ
⊢ -⌊-q⌋ = -(-q.num / ↑q.den)
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
r : R
m : ℕ
⊢ IsNat r m → IsNat ⌊r⌋ m

Tactic:
by rintro ⟨⟨⟩⟩; exact ⟨by simp⟩

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

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
r : R
m : ℤ
⊢ IsInt r m → IsInt ⌊r⌋ m

Tactic:
by rintro ⟨⟨⟩⟩; exact ⟨by simp⟩

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

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
r : R
m : ℕ
⊢ IsNat r m → IsNat ⌈r⌉ m

Tactic:
by rintro ⟨⟨⟩⟩; exact ⟨by simp⟩

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

Goal state before:
pp: R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
r : R
m : ℤ
⊢ IsInt r m → IsInt ⌈r⌉ m

Tactic:
by rintro ⟨⟨⟩⟩; exact ⟨by simp⟩

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

Goal state before:
pp: R : Type u_3
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
n : ℤ
d : ℕ
res : ℤ
hres : round (↑n / ↑d) = res
inv : Invertible ↑d
⊢ IsInt (round (↑n * ⅟↑d)) res

Tactic:
subst res

Goal state after:
R : Type u_3
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
n : ℤ
d : ℕ
inv : Invertible ↑d
⊢ IsInt (round (↑n * ⅟↑d)) (round (↑n / ↑d))
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Archimedean R
y : R
inst✝ : ExistsAddOfLE R
x : R
hy1 : 1 < y
⊢ ∃ n, x < y ^ n

Tactic:
obtain ⟨z, hz, rfl⟩ := exists_pos_add_of_lt' hy1
  rw [add_comm]
  exact add_one_pow_unbounded_of_pos _ hz

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
⊢ ↑⌈a⌉ < b * a

Tactic:
obtain hab | hba := le_total a (b - 1)⁻¹

Goal state after:
case inl
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)⁻¹
⊢ ↑⌈a⌉ < b * a

case inr
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
hba : (b - 1)⁻¹ ≤ a
⊢ ↑⌈a⌉ < b * a
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
_l : List α
⊢ _l.Nodup ↔ ∀ (a : α), List.count a _l ≤ 1

Tactic:
exact List.nodup_iff_count_le_one

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

Goal state before:
pp: α : Type u_1
l₂ : List α
a : α
inst✝ : DecidableEq α
l₁ : List α
h : a ∈ l₂
⊢ (a :: l₁) ∩ l₂ = a :: l₁ ∩ l₂

Tactic:
by
  simp [Inter.inter, List.inter, h]

Goal state after: