mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α : Sort u
β : Sort v
x✝¹ x✝ : α ≃ β
h : x✝¹.toEmbedding = x✝.toEmbedding
⊢ x✝¹ = x✝

Tactic:
rwa [DFunLike.ext'_iff] at h ⊢

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✝ a : G₀
ha : 0 < a
⊢ a * (a * 0) < a * (a * a⁻¹)

Tactic:
simpa [ha.ne']

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₀
ha : 0 < a
b c : G₀
hbc : b < c
⊢ a⁻¹ * (a * b) < a⁻¹ * (a * c)

Tactic:
simpa [ha.ne']

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✝ a : G₀
ha : 0 < a
⊢ 0 * a * a < a⁻¹ * a * a

Tactic:
simpa [ha.ne']

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 : G₀
ha : 0 < a
b c : G₀
hbc : b < c
⊢ b * a * a⁻¹ < c * a * a⁻¹

Tactic:
simpa [ha.ne']

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : OrderTop α
inst✝¹ : SemilatticeSup β
inst✝ : OrderTop β
a b : α
f : α ≃o β
ha : Codisjoint a b
⊢ Codisjoint (f a) (f b)

Tactic:
rw [codisjoint_iff_le_sup, ← f.map_sup, ← f.map_top]

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : SemilatticeSup α
inst✝² : OrderTop α
inst✝¹ : SemilatticeSup β
inst✝ : OrderTop β
a b : α
f : α ≃o β
ha : Codisjoint a b
⊢ f ⊤ ≤ f (a ⊔ b)
Module: Mathlib.Algebra.Order.Group.Lattice

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊓ b) * (a ⊔ b) = (a ⊓ b) * (a * b * b⁻¹ ⊔ a * b * a⁻¹)

Tactic:
mul_inv_cancel_right,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (a ⊓ b) * (a ⊔ b) = (a ⊓ b) * (a ⊔ a * b * a⁻¹)
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)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ = |a / b|ₘ

Tactic:
let : DistribLattice α := CommGroup.toDistribLattice α
  calc
    |(a ⊔ c) / (b ⊔ c)|ₘ * |(a ⊓ c) / (b ⊓ c)|ₘ =
        (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * |(a ⊓ c) / (b ⊓ c)|ₘ := by
        rw [sup_div_inf_eq_mabs_div]
    _ = (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) := by
        rw [sup_div_inf_eq_mabs_div (b ⊓ c) (a ⊓ c)]
    _ = (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * (((b ⊔ a) ⊓ c) / (b ⊓ a ⊓ c)) := by
        rw [← sup_inf_right, ← inf_sup_right, sup_assoc, sup_comm c (a ⊔ c), sup_right_idem,
          sup_assoc, inf_assoc, inf_comm c (a ⊓ c), inf_right_idem, inf_assoc]
    _ = (b ⊔ a ⊔ c) * ((b ⊔ a) ⊓ c) / ((b ⊓ a ⊔ c) * (b ⊓ a ⊓ c)) := by rw [div_mul_div_comm]
    _ = (b ⊔ a) * c / ((b ⊓ a) * c) := by
        rw [mul_comm, inf_mul_sup, mul_comm (b ⊓ a ⊔ c), inf_mul_sup]
    _ = (b ⊔ a) / (b ⊓ a) := by
        rw [div_eq_mul_inv, mul_inv_rev, mul_assoc, mul_inv_cancel_left, ← div_eq_mul_inv]
    _ = |a / b|ₘ := by rw [sup_div_inf_eq_mabs_div]

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

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a b : R
ha : IsLeftRegular a
h : a * b = a
⊢ b = 1

Tactic:
rwa [← ha.eq_iff, mul_one]

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

Goal state before:
pp: case coe.coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map (⇑f) (↑a✝¹ + ↑a✝) = map ⇑f ↑a✝¹ + map ⇑f ↑a✝

Tactic:
map_coe,

Goal state after:
case coe.coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map (⇑f) (↑a✝¹ + ↑a✝) = ↑(f a✝¹) + map ⇑f ↑a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case coe.coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map (⇑f) (↑a✝¹ + ↑a✝) = ↑(f a✝¹) + map ⇑f ↑a✝

Tactic:
map_coe,

Goal state after:
case coe.coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map (⇑f) (↑a✝¹ + ↑a✝) = ↑(f a✝¹) + ↑(f a✝)
Module: Mathlib.Algebra.Order.Ring.Cast

Goal state before:
pp: R : Type u_1
inst✝³ : AddCommGroupWithOne R
inst✝² : PartialOrder R
inst✝¹ : AddLeftMono R
inst✝ : ZeroLEOneClass R
m n : ℤ
h : m ≤ n
⊢ ↑m ≤ ↑n

Tactic:
rw [← sub_nonneg] at h

Goal state after:
R : Type u_1
inst✝³ : AddCommGroupWithOne R
inst✝² : PartialOrder R
inst✝¹ : AddLeftMono R
inst✝ : ZeroLEOneClass R
m n : ℤ
h : 0 ≤ n - m
⊢ ↑m ≤ ↑n
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a b : α
inst✝ : LT α
⊢ ↑a < ↑b ↔ a < b

Tactic:
by simp [lt_def]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a : α
⊢ ⊥ < ↑a

Tactic:
by simp [lt_def]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a : WithBot α
⊢ ¬a < ⊥

Tactic:
by simp [lt_def]

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

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a b : α
⊢ ↑a < ↑b ↔ a < b

Tactic:
by simp [lt_def]

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

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a : α
⊢ 0 < ↑a

Tactic:
by simp [lt_def]

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

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a : WithZero α
⊢ ¬a < 0

Tactic:
by simp [lt_def]

Goal state after:
Module: Mathlib.Data.Nat.Find

Goal state before:
pp: case step
P : ℕ → Prop
inst✝ : DecidablePred P
m n m✝ : ℕ
hmk : m.le m✝
ih : findGreatest P m ≤ findGreatest P m✝
⊢ findGreatest P m ≤ findGreatest P m✝.succ

Tactic:
rw [findGreatest_succ]

Goal state after:
case step
P : ℕ → Prop
inst✝ : DecidablePred P
m n m✝ : ℕ
hmk : m.le m✝
ih : findGreatest P m ≤ findGreatest P m✝
⊢ findGreatest P m ≤ if P (m✝ + 1) then m✝ + 1 else findGreatest P m✝
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
n : ℕ
hn : n ≠ 0
⊢ ⌈a⌉₊ = n ↔ ↑(n - 1) < a ∧ a ≤ ↑n

Tactic:
← ceil_le,

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
n : ℕ
hn : n ≠ 0
⊢ ⌈a⌉₊ = n ↔ ↑(n - 1) < a ∧ ⌈a⌉₊ ≤ n
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
n : ℕ
hn : n ≠ 0
⊢ ⌈a⌉₊ = n ↔ ¬a ≤ ↑(n - 1) ∧ ⌈a⌉₊ ≤ n

Tactic:
← ceil_le,

Goal state after:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : LinearOrder R
inst✝ : FloorSemiring R
a : R
n : ℕ
hn : n ≠ 0
⊢ ⌈a⌉₊ = n ↔ ¬⌈a⌉₊ ≤ n - 1 ∧ ⌈a⌉₊ ≤ n
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
⊢ b ≤ ⌊a + ↑n⌋₊ ↔ b ≤ ⌊a⌋₊ + n

Tactic:
by
    rw [le_floor_iff (add_nonneg ha n.cast_nonneg)]
    obtain hb | hb := le_total n b
    · obtain ⟨d, rfl⟩ := exists_add_of_le hb
      rw [Nat.cast_add, add_comm n, add_comm (n : R), add_le_add_iff_right, add_le_add_iff_right,
        le_floor_iff ha]
    · obtain ⟨d, rfl⟩ := exists_add_of_le hb
      rw [Nat.cast_add, add_left_comm _ b, add_left_comm _ (b : R)]
      refine iff_of_true ?_ le_self_add
      exact le_add_of_nonneg_right <| ha.trans <| le_add_of_nonneg_right d.cast_nonneg

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

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
a b : R
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a + b)
⊢ ⅟(a + b) = ⅟a + ⅟b ↔ -1 = ⅟a * b + ⅟b * a

Tactic:
by
  calc ⅟(a + b) = ⅟a + ⅟b
      ↔ ⅟(a + b) * (a + b) = (⅟a + ⅟b) * (a + b) := by rw [mul_left_inj_of_invertible]
    _ ↔ 1 = ⅟a * a + ⅟b * a + (⅟a * b + ⅟b * b) := by rw [invOf_mul_self, mul_add, add_mul, add_mul]
    _ ↔ 1 = 1 + ⅟b * a + (1 + ⅟a * b) := by rw [invOf_mul_self, invOf_mul_self, add_comm _ 1]
    _ ↔ 1 = 1 + 1 + ⅟b * a + ⅟a * b := by rw [← add_assoc, add_comm _ 1, ← add_assoc]
    _ ↔ -2 + 1 = -2 + (2 + ⅟b * a + ⅟a * b) := by rw [one_add_one_eq_two, add_right_inj]
    _ ↔ -2 + 1 = ⅟b * a + ⅟a * b := by rw [← add_assoc, ← add_assoc, neg_add_cancel, zero_add]
    _ ↔ -1 + 0 = ⅟b * a + ⅟a * b := by rw [← one_add_one_eq_two, neg_add, add_assoc, neg_add_cancel]
    _ ↔ -1 = ⅟a * b + ⅟b * a := by rw [add_zero, add_comm]

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

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a b c d : K
hbc : Commute b c
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
⊢ a / b - c / d = (a * d - b * c) / (b * d)

Tactic:
by
  simpa only [mul_neg, neg_div, ← sub_eq_add_neg] using hbc.neg_right.div_add_div hbd hb hd

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

Goal state before:
pp: case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
n✝ : ℕ
inst✝ : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n
⊢ |a * geomSum a b n| + |b ^ (n + 1)| ≤ (↑(n + 1) + 1) * max |a| |b| ^ (n + 1)

Tactic:
rw [abs_mul, abs_pow, Nat.cast_succ, add_one_mul]

Goal state after:
case succ
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
n✝ : ℕ
inst✝ : IsOrderedRing α
n : ℕ
ih : |geomSum a b n| ≤ (↑n + 1) * max |a| |b| ^ n
⊢ |a| * |geomSum a b n| + |b| ^ (n + 1) ≤ (↑n + 1) * max |a| |b| ^ (n + 1) + max |a| |b| ^ (n + 1)
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: case ha
α : Type u_1
inst✝² : CommRing α
inst✝¹ : LinearOrder α
a b : α
inst✝ : IsOrderedRing α
n : ℕ
⊢ 0 ≤ |a - b|

Tactic:
exact abs_nonneg _

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

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

Tactic:
by
  have : (Icc a b \ {a, b}) ∪ {a, b} = Icc a b := sdiff_union_of_subset fun
    | x, .inl rfl => left_mem_Icc.mpr h
    | x, .inr rfl => right_mem_Icc.mpr h
  rw [← this, Icc_sdiff_both]

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

Goal state before:
pp: α : Type u
l : List α
h : l ≠ []
⊢ drop (l.length - 1) l = [l.getLast h]

Tactic:
by
  induction l with
  | nil => aesop
  | cons a l ih =>
    by_cases hl : l = []
    · simp_all
    rw [length_cons, Nat.add_one_sub_one, List.drop_length_cons hl a]
    simp [getLast_cons, hl]

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

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

Tactic:
simp only [zip, zipWith, mem_cons, Prod.mk.injEq]

Goal state after:
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, l₁.length = l₂.length → (∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ (a :: l₁).zip (b :: l₂) → R a_1 b_1
h₁ : l₁.length = l₂.length
a✝ : α
b✝ : β
h : (a✝, b✝) ∈ l₁.zip l₂
⊢ a✝ = a ∧ b✝ = b ∨ (a✝, b✝) ∈ zipWith Prod.mk l₁ l₂
Module: Mathlib.Algebra.Order.Field.Basic

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

Tactic:
· obtain ⟨a', ha', hc'⟩ := exists_between ((lt_div_iff₀ hb).2 hc)
    exact ⟨a', ha', (lt_div_iff₀ hb).1 hc'⟩

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

Goal state before:
pp: case inl
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
d : α
d_ab : d < a * b
hd : d < 0
⊢ d ≤ c

Tactic:
exact hd.le.trans hc

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

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
l : List M
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
⊢ (map (⇑f) l).prod = f l.prod

Tactic:
by
  simp only [prod, foldr_map, ← map_one f]
  exact l.foldr_hom f (fun x y => (map_mul f x y).symm)

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

Goal state before:
pp: α : Type u
l : List α
p : α → Prop
⊢ (∃ x, (∃ i h, l[i] = x) ∧ p x) ↔ ∃ i x, p l[i]

Tactic:
exact ⟨fun ⟨_x, ⟨i, hi, hix⟩, hxp⟩ ↦ ⟨i, hi, hix ▸ hxp⟩, fun ⟨i, hi, hp⟩ ↦ ⟨_, ⟨i, hi, rfl⟩, hp⟩⟩

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

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
a₁ a₂ : ℤ × M
l₁ l₂ l : NF M
h : l₁.eval * (a₂ ::ᵣ l₂).eval = l.eval
⊢ (a₁ ::ᵣ l₁).eval * (a₂ ::ᵣ l₂).eval = (a₁ ::ᵣ l).eval

Tactic:
simp only [eval_cons, ← h]
  ac_rfl

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

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
a₁ a₂ : ℤ × M
l₁ l₂ l : NF M
h : (a₁ ::ᵣ l₁).eval * l₂.eval = l.eval
⊢ (a₁ ::ᵣ l₁).eval * (a₂ ::ᵣ l₂).eval = (a₂ ::ᵣ l).eval

Tactic:
simp only [eval_cons, ← h]
  ac_rfl

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

Goal state before:
pp: L : List ℕ
⊢ L.tail.sum = L.sum - L.headI

Tactic:
← headI_add_tail_sum L,

Goal state after:
L : List ℕ
⊢ L.tail.sum = L.headI + L.tail.sum - L.headI
Module: Mathlib.Algebra.Ring.Rat

Goal state before:
pp: q : ℚ
⊢ q * ↑q.den = ↑q.num

Tactic:
suffices (q.num /. ↑q.den) * (↑q.den /. 1) = q.num /. 1 by simp_all

Goal state after:
q : ℚ
⊢ q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1
Module: Mathlib.Algebra.Ring.Rat

Goal state before:
pp: q : ℚ
⊢ ↑q.den * q = ↑q.num

Tactic:
rw [mul_comm, mul_den_eq_num]

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

Goal state before:
pp: q : ℚ≥0
⊢ ↑q.den * q = ↑q.num

Tactic:
rw [mul_comm, mul_den_eq_num]

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

Goal state before:
pp: G : Type u_1
inst✝ : DivisionMonoid G
a b c d : G
hbc : Commute b c
hbd : Commute b⁻¹ d
hcd : Commute c⁻¹ d
⊢ a * b⁻¹ * (d * c⁻¹) = a * c⁻¹ * (d * b⁻¹)

Tactic:
hbd.symm.eq,

Goal state after:
G : Type u_1
inst✝ : DivisionMonoid G
a b c d : G
hbc : Commute b c
hbd : Commute b⁻¹ d
hcd : Commute c⁻¹ d
⊢ a * b⁻¹ * (d * c⁻¹) = a * c⁻¹ * (b⁻¹ * d)
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case neg
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
⊢ ↑{ num := n, den := d, den_nz := h, reduced := c }.den ∣ b

Tactic:
refine Int.dvd_natAbs.1 <| Int.natCast_dvd_natCast.2 <| c.symm.dvd_of_dvd_mul_left ?_

Goal state after:
case neg
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
⊢ d ∣ n.natAbs * b.natAbs
Module: Mathlib.Data.Nat.Set

Goal state before:
pp: α : Type u_2
x : α
f : ℕ → α → α
⊢ (range fun n ↦ rec x f n) = {x} ∪ range fun n ↦ rec (f 0 x) (f ∘ succ) n

Tactic:
by
  convert! (range_of_succ (fun n => Nat.rec x f n : ℕ → α)).symm using 4
  dsimp
  rename_i n
  induction n with
  | zero => rfl
  | succ n ihn => dsimp at ihn ⊢; rw [ihn]

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 α
s : Set α
H : ¬(upperBounds s).Nonempty
⊢ sSup s = sSup ∅

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

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

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

Tactic:
simp [nonempty_iff_ne_empty, sInter_eq_empty_iff]

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

Goal state before:
pp: α : Type u_1
π : α → Type u_12
i : Set α
s t : (a : α) → Set (π a)
⊢ i.pi s \ i.pi t ⊆ ⋃ a ∈ i, eval a ⁻¹' (s a \ t a)

Tactic:
refine sdiff_subset_comm.2 fun x hx a ha => ?_

Goal state after:
α : Type u_1
π : α → Type u_12
i : Set α
s t : (a : α) → Set (π a)
x : (i : α) → π i
hx : x ∈ i.pi s \ ⋃ a ∈ i, eval a ⁻¹' (s a \ t a)
a : α
ha : a ∈ i
⊢ x a ∈ t a
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
S : Set (Set α)
f : α → β
⊢ ⨅ i, ⨅ a ∈ ↑i, f a = ⨅ s ∈ S, ⨅ x ∈ s, f x

Tactic:
← iInf_subtype''

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
S : Set (Set α)
f : α → β
⊢ ⨅ i, ⨅ a ∈ ↑i, f a = ⨅ i, ⨅ x ∈ ↑i, f x
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
a b : α
inst✝ : Fact (a < b)
x y : ↑(Ico a b)
⊢ Disjoint x y ↔ ↑x ⊓ ↑y = a

Tactic:
by
  simp [_root_.disjoint_iff, Subtype.ext_iff]

Goal state after:
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
x y : ↑(Iic a)
⊢ Disjoint x y ↔ Disjoint ↑x ↑y

Tactic:
by
  simp [_root_.disjoint_iff, Subtype.ext_iff]

Goal state after:
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
inst✝ : SemilatticeInf α
a : α
x y : ↑(Ici a)
⊢ Disjoint x y ↔ ↑x ⊓ ↑y = a

Tactic:
by
  simp [_root_.disjoint_iff, Subtype.ext_iff]

Goal state after:
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
a b : α
inst✝¹ : SemilatticeInf α
inst✝ : Fact (a ≤ b)
x y : ↑(Icc a b)
⊢ Disjoint x y ↔ ↑x ⊓ ↑y = a

Tactic:
by
  simp [_root_.disjoint_iff, Subtype.ext_iff]

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

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

Tactic:
exact le_csSup h₂ ha

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ IsChain r univ ↔ Std.Trichotomous r

Tactic:
refine ⟨fun h => ⟨fun a b => ?_⟩, fun h => @isChain_of_trichotomous _ _ h univ⟩
  have : a ≠ b → (r a b ∨ r b a) := h trivial trivial
  grind

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
⊢ s ⊆ SuccChain r s

Tactic:
if h : ∃ t, IsChain r s ∧ SuperChain r s t then exact (succChain_spec h).2.1
  else
    simp [SuccChain, h]

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ ↑(sInf (range fun i ↦ f i)) = a ⊓ ⨅ i, ↑(f i)

Tactic:
coe_sInf

Goal state after:
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ a ⊓ sInf (Subtype.val '' range fun i ↦ f i) = a ⊓ ⨅ i, ↑(f i)
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case refl
m n : ℕ
this : ∀ {n : ℕ}, 0 < n → n ! < (n + 1)!
hn : 0 < n
⊢ n ! < n.succ !

Tactic:
exact this hn

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

Goal state before:
pp: n : ℕ
⊢ n ^ 0 ≤ 1

Tactic:
Nat.pow_zero

Goal state after:
n : ℕ
⊢ 1 ≤ 1
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ 1 ≤ (n + 0) ^ 0

Tactic:
Nat.pow_zero

Goal state after:
n : ℕ
⊢ 1 ≤ 1
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ (n + 1 - 0) ^ 0 ≤ 1

Tactic:
Nat.pow_zero

Goal state after:
n : ℕ
⊢ 1 ≤ 1
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ 1 ≤ n ^ 0

Tactic:
Nat.pow_zero

Goal state after:
n : ℕ
⊢ 1 ≤ 1
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ min (fract (↑m / ↑n)) (1 - fract (↑m / ↑n)) = ↑(min (m % n) (n - m % n)) / ↑n

Tactic:
Nat.cast_min,

Goal state after:
case inr
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ min (fract (↑m / ↑n)) (1 - fract (↑m / ↑n)) = min ↑(m % n) ↑(n - m % n) / ↑n
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ min (↑(m % n) / ↑n) (1 - ↑(m % n) / ↑n) = min (↑(m % n) / ↑n) (↑n / ↑n - ↑(m % n) / ↑n)

Tactic:
div_self hn'.ne'

Goal state after:
case inr
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ min (↑(m % n) / ↑n) (1 - ↑(m % n) / ↑n) = min (↑(m % n) / ↑n) (1 - ↑(m % n) / ↑n)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
n : ℕ
a : ℤ
⊢ a ≤ ⌊↑n⌋ ↔ a ≤ ↑n

Tactic:
by rw [le_floor, ← cast_natCast, cast_le]

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 : R
⊢ fract a = 0 ↔ a ∈ range Int.cast

Tactic:
by
  simp [fract_eq_iff, eq_comm]

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

Goal state before:
pp: case right
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
hx : fract x ≠ 0
⊢ -x - (1 - fract x) = ↑(-⌊x⌋ - 1)

Tactic:
simp only [sub_sub_eq_add_sub, cast_sub, cast_neg, cast_one, sub_left_inj]

Goal state after:
case right
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
x : R
hx : fract x ≠ 0
⊢ -x + fract x = -↑⌊x⌋
Module: Mathlib.Algebra.Order.Floor.Ring

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

Tactic:
← ceil_le,

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
z : ℤ
a : R
⊢ ⌈a⌉ = z ↔ ↑z - 1 < a ∧ ⌈a⌉ ≤ z
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌈↑n / ↑d⌉ = ↑⌈↑n / ↑d⌉.toNat

Tactic:
Int.natCast_toNat_eq_self.mpr (ceil_nonneg (div_nonneg n.cast_nonneg d.cast_nonneg))

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌈↑n / ↑d⌉ = ⌈↑n / ↑d⌉
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n | a ^ n ≤ g}
⊢ ∃! k, a ^ k ≤ g ∧ g < a ^ (k + 1)

Tactic:
obtain ⟨k, hk : g⁻¹ ≤ a ^ k⟩ := MulArchimedean.arch g⁻¹ ha

Goal state after:
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n | a ^ n ≤ g}
k : ℕ
hk : g⁻¹ ≤ a ^ k
⊢ ∃! k, a ^ k ≤ g ∧ g < a ^ (k + 1)
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
hb : b < 1
hba : ↑⌈b / (1 - b)⌉ ≤ a
⊢ b / (1 - b) ≤ ↑⌊a⌋

Tactic:
← ceil_le,

Goal state after:
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉ ≤ a
⊢ ⌈b / (1 - b)⌉ ≤ ⌊a⌋