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

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a : R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
⊢ a ^ n ≤ 0 ↔ a ≤ 0

Tactic:
rw [le_iff_lt_or_eq, le_iff_lt_or_eq, hn.pow_neg_iff, pow_eq_zero_iff]
  rintro rfl; simp at hn

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
⊢ image2 f s t \ image2 f s t' ⊆ image2 f s (t \ t')

Tactic:
by
  rintro - ⟨⟨a, ha, b, hb, rfl⟩, h⟩
  exact ⟨_, ha, _, ⟨hb, fun hb' ↦ h ⟨_, ha, _, hb', rfl⟩⟩, rfl⟩

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

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

Tactic:
simp [geomSum]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
⊢ image2 f s (image2 g t u) = image2 g' t (image2 f' s u)

Tactic:
image2_swap f',

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
⊢ image2 f s (image2 g t u) = image2 g' t (image2 (fun a b ↦ f' b a) u s)
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: case zero
α : Type u_1
inst✝ : CommRing α
a b : α
n : ℕ
⊢ a ^ (0 + 1) - b ^ (0 + 1) = (a - b) * geomSum a b 0

Tactic:
simp [geomSum]

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a : α
s : Set α
ho : Iio a ⊆ s
hc : s ⊆ Iic a
h : a ∈ s
⊢ Iio a ⊆ s ∧ {a} ⊆ s

Tactic:
simp [*]

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

Goal state before:
pp: case refine_1.inr
α : Type u_1
inst✝ : Preorder α
s t : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)
hst : IsCofinalFor s t
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s ∧ IsCofinalFor t s ∨ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t ∧ IsCofinalFor s t

Tactic:
· exact .inr ⟨DirectedOn.of_isCofinalFor h subset_union_right hst.union_left, hst⟩

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

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
h1 : 0 < a
h2 : a < 1
⊢ a < 1 / 1

Tactic:
one_div_one

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

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
h1 : 0 < a
h2 : a ≤ 1
⊢ a ≤ 1 / 1

Tactic:
one_div_one

Goal state after:
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
h1 : 0 < a
h2 : a ≤ 1
⊢ a ≤ 1
Module: Mathlib.Algebra.BigOperators.Group.List.Defs

Goal state before:
pp: case nil
ι : Type u_1
M : Type u_2
inst✝ : MulOneClass M
⊢ (map (fun x ↦ 1) []).prod = 1

Tactic:
simp [*]

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

Goal state before:
pp: case cons
ι : Type u_1
M : Type u_2
inst✝ : MulOneClass M
head✝ : ι
tail✝ : List ι
tail_ih✝ : (map (fun x ↦ 1) tail✝).prod = 1
⊢ (map (fun x ↦ 1) (head✝ :: tail✝)).prod = 1

Tactic:
simp [*]

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

Goal state before:
pp: 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

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ 1 / a ^ n ≤ 1 / a ^ m

Tactic:
refine (one_div_le_one_div ?_ ?_).mpr (pow_right_mono₀ a1 mn) <;>
    exact pow_pos (zero_lt_one.trans_le a1) _

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

Goal state before:
pp: case zero
α : Type u_1
f : α → α
a : α
l : List α
⊢ iterateTR.loop f a 0 l = l.reverse ++ iterate f a 0

Tactic:
simp [*]

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

Goal state before:
pp: case succ
α : Type u_1
f : α → α
n✝ : ℕ
a✝ : ∀ (a : α) (l : List α), iterateTR.loop f a n✝ l = l.reverse ++ iterate f a n✝
a : α
l : List α
⊢ iterateTR.loop f a (n✝ + 1) l = l.reverse ++ iterate f a (n✝ + 1)

Tactic:
simp [*]

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

Goal state before:
pp: case succ.nil
α : Type u
n : ℕ
ih : ∀ (l : List α), tail^[n] l = drop n l
⊢ tail^[n + 1] [] = drop (n + 1) []

Tactic:
simp [*]

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

Goal state before:
pp: case succ.cons
α : Type u
n : ℕ
ih : ∀ (l : List α), tail^[n] l = drop n l
head✝ : α
tail✝ : List α
⊢ tail^[n + 1] (head✝ :: tail✝) = drop (n + 1) (head✝ :: tail✝)

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u
p : α → Bool
a : α
l l₂ : List α
⊢ loop p (a :: l) l₂ = (l₂.reverse ++ takeWhile p (a :: l), dropWhile p (a :: l))

Tactic:
by
    cases hp : p a <;> simp [hp, span.loop, span.loop_eq_take_drop, takeWhile, dropWhile]

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

Goal state before:
pp: α : Type u
β : Type v
a : α
l : List α
x : α
n k : ℕ
hk' : n + k < l.length
⊢ n + k + 1 < (l.insertIdx n x).length

Tactic:
length_insertIdx_of_le_length (by lia),

Goal state after:
α : Type u
β : Type v
a : α
l : List α
x : α
n k : ℕ
hk' : n + k < l.length
⊢ n + k + 1 < l.length + 1
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_4
inst✝³ : CommRing α
inst✝² : NoZeroDivisors α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a b : α
a0 : 0 ≤ a
b0 : 0 ≤ b
this : 0 ≤ -b → b = 0
⊢ a * a = b * b ↔ a = b

Tactic:
grind [sq_sub_sq, mul_eq_zero, add_eq_zero_iff_eq_neg]

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

Goal state before:
pp: α : Type u
n : ℕ
x : α
⊢ Injective fun l ↦ l.insertIdx n x

Tactic:
intro l₁ l₂ hl

Goal state after:
α : Type u
n : ℕ
x : α
l₁ l₂ : List α
hl : (fun l ↦ l.insertIdx n x) l₁ = (fun l ↦ l.insertIdx n x) l₂
⊢ l₁ = l₂
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case mpr.slnil
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l : List β
⊢ ∀ {l₁ : List α}, Forall₂ R l₁ [] → SublistForall₂ R l₁ []

Tactic:
| slnil =>

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

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2
⊢ 2 * (ε * a) * b * ε⁻¹ ≤ ((ε * a) ^ 2 + b ^ 2) * ε⁻¹

Tactic:
gcongr; exact inv_nonneg.mpr hε.le

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

Goal state before:
pp: case inr
α : Type u_1
l₁ l₂ : List α
m n : ℕ
h : l₁[m]? = l₂[n]?
hm : m ≥ l₁.length
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂

Tactic:
getElem?_eq_none hm,

Goal state after:
case inr
α : Type u_1
l₁ l₂ : List α
m n : ℕ
h : none = l₂[n]?
hm : m ≥ l₁.length
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
h : l ≠ []
⊢ l.length = 2 ↔ l = [l.head h, l.getLast h]

Tactic:
rw [length_eq_two]

Goal state after:
α : Type u
l : List α
h : l ≠ []
⊢ (∃ a b, l = [a, b]) ↔ l = [l.head h, l.getLast h]
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
L : List ι
f : ι → M
G : Type u_8
inst✝¹ : FunLike G M N
inst✝ : MonoidHomClass G M N
g : G
⊢ (map (⇑g ∘ f) L).prod = (map (⇑g) (map f L)).prod

Tactic:
map_map

Goal state after:
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
L : List ι
f : ι → M
G : Type u_8
inst✝¹ : FunLike G M N
inst✝ : MonoidHomClass G M N
g : G
⊢ (map (⇑g ∘ f) L).prod = (map (⇑g ∘ f) L).prod
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
L : List M
i : ℕ
⊢ (take i L).prod * (drop i L).prod = L.prod

Tactic:
by
  simp [← prod_append]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
⊢ 1 / l.eval = l⁻¹.eval

Tactic:
by
  simp [eval_inv]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
h : Surjective (map f)
x : β
⊢ ∃ a, f a = x

Tactic:
let ⟨[y], hxy⟩ := h [x]

Goal state after:
α : Type u
β : Type v
f : α → β
h : Surjective (map f)
x : β
y : α
hxy : map f [y] = [x]
⊢ ∃ a, f a = x
Module: Mathlib.Algebra.Order.Nonneg.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : { x // 0 ≤ x }
b : α
⊢ a < toNonneg b ↔ ↑a < b

Tactic:
obtain ⟨a, ha⟩ := a

Goal state after:
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
b a : α
ha : 0 ≤ a
⊢ ⟨a, ha⟩ < toNonneg b ↔ ↑⟨a, ha⟩ < b
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case nil
α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
b : β
⊢ foldrM f b [] = foldr (fun a mb ↦ mb >>= f a) (pure b) []

Tactic:
simp [*]

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

Goal state before:
pp: case cons
α : Type u
β : Type v
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
b : β
head✝ : α
tail✝ : List α
tail_ih✝ : foldrM f b tail✝ = foldr (fun a mb ↦ mb >>= f a) (pure b) tail✝
⊢ foldrM f b (head✝ :: tail✝) = foldr (fun a mb ↦ mb >>= f a) (pure b) (head✝ :: tail✝)

Tactic:
simp [*]

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

Goal state before:
pp: case nil
α : Type u
β : Type v
⊢ filterMap (fun x ↦ none) [] = []

Tactic:
simp [*]

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

Goal state before:
pp: case cons
α : Type u
β : Type v
head✝ : α
tail✝ : List α
tail_ih✝ : filterMap (fun x ↦ none) tail✝ = []
⊢ filterMap (fun x ↦ none) (head✝ :: tail✝) = []

Tactic:
simp [*]

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

Goal state before:
pp: case cons.zero
α : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), drop (take i (map length tail✝)).sum tail✝.flatten = (drop i tail✝).flatten
⊢ drop (take 0 (map length (head✝ :: tail✝))).sum (head✝ :: tail✝).flatten = (drop 0 (head✝ :: tail✝)).flatten

Tactic:
simp [*]

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

Goal state before:
pp: case cons.succ
α : Type u_2
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), drop (take i (map length tail✝)).sum tail✝.flatten = (drop i tail✝).flatten
n✝ : ℕ
⊢ drop (take (n✝ + 1) (map length (head✝ :: tail✝))).sum (head✝ :: tail✝).flatten =
    (drop (n✝ + 1) (head✝ :: tail✝)).flatten

Tactic:
simp [*]

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

Goal state before:
pp: q : ℚ
x✝ : q = 0
⊢ q.num = 0

Tactic:
simp [*]

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

Goal state before:
pp: case nil
α : Type u
β : Type v
l : List α
p : β → Prop
f : α → β
⊢ Forall p (map f []) ↔ Forall (p ∘ f) []

Tactic:
simp [*]

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

Goal state before:
pp: case cons
α : Type u
β : Type v
l : List α
p : β → Prop
f : α → β
head✝ : α
tail✝ : List α
tail_ih✝ : Forall p (map f tail✝) ↔ Forall (p ∘ f) tail✝
⊢ Forall p (map f (head✝ :: tail✝)) ↔ Forall (p ∘ f) (head✝ :: tail✝)

Tactic:
simp [*]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
n : ℕ
⊢ SemiconjBy a (x ^ ↑n) (y ^ ↑n)

Tactic:
simp [zpow_natCast, h.pow_right n]

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

Goal state before:
pp: α : Type u_1
inst✝ : MonoidWithZero α
x y : α
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : α), ¬IsUnit z → z ≠ 0 → z ∣ x → ¬z ∣ y
⊢ IsRelPrime x y

Tactic:
refine fun z hx hy ↦ by_contra fun h ↦ H z h ?_ hx hy
  rintro rfl; exact nonzero ⟨zero_dvd_iff.1 hx, zero_dvd_iff.1 hy⟩

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

Goal state before:
pp: m k : ℕ+
⊢ ↑(m.mod k) = if ↑m % ↑k = 0 then ↑k else ↑m % ↑k

Tactic:
dsimp [mod, modDiv]
  cases (m : ℕ) % (k : ℕ) with
  | zero =>
    rw [if_pos rfl]
    rfl
  | succ n =>
    rw [if_neg n.succ_ne_zero]
    rfl

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

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
h : ↑n₁ / ↑↑d₁ = ↑(n₂ /. ↑d₂)
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂

Tactic:
cast_divInt_of_ne_zero _ (by simpa)

Goal state after:
α : Type u_3
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
h : ↑n₁ / ↑↑d₁ = ↑n₂ / ↑↑d₂
d₁a : ↑d₁ ≠ 0
d₂a : ↑d₂ ≠ 0
⊢ n₁ /. ↑d₁ = n₂ /. ↑d₂
Module: Mathlib.Data.Rat.Lemmas

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

Tactic:
have hs : (q.den * r.den : ℤ) ≠ 0 := Int.natCast_ne_zero_iff_pos.mpr (Nat.mul_pos q.pos r.pos)

Goal state after:
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
⊢ (q * r).num * ↑q.den * ↑r.den = q.num * r.num * ↑(q * r).den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
⊢ ↑q.den * ↑r.den * (q * r).num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den

Tactic:
nth_rw 1 [c_mul_den]

Goal state after:
q r : ℚ
s : ℚ := q.num * r.num /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * r.num = c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den
⊢ c * ↑(↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).den * (q * r).num =
    c * (↑(q.num * r.num) / ↑(↑q.den * ↑r.den)).num * ↑(q * r).den
Module: Mathlib.Data.Rat.Lemmas

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

Tactic:
have hs : (q.den * r.den : ℤ) ≠ 0 := Int.natCast_ne_zero_iff_pos.mpr (Nat.mul_pos q.pos r.pos)

Goal state after:
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
⊢ (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 : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ ↑q.den * ↑r.den * (q + r).num = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den

Tactic:
nth_rw 1 [c_mul_den]

Goal state after:
q r : ℚ
s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)
hs : ↑q.den * ↑r.den ≠ 0
c : ℤ
c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num
c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den
⊢ c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den * (q + r).num =
    c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num * ↑(q + r).den
Module: Mathlib.Data.Rat.Cast.Defs

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

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q + r) = ↑q + ↑r

Tactic:
by
  rw [add_def, cast_divNat_of_ne_zero, cast_def, cast_def, mul_comm _ q.den,
    (Nat.commute_cast _ _).div_add_div (Nat.commute_cast _ _) hq hr]
  · push_cast
    rfl
  · push_cast
    exact mul_ne_zero hq hr

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

Goal state before:
pp: a : ℤ
ha0 : 0 < a
⊢ (↑a)⁻¹.num = 1

Tactic:
simp [*]

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

Goal state before:
pp: q : ℚ
hq : q ≠ 0
⊢ q⁻¹.den = q.num.natAbs

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
a b : α
ha : a = 0
hb : b = 0
⊢ a + b = 0

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u
inst✝¹ : Semiring α
inst✝ : PartialOrder α
a b : α
ha : a = 0
hb : b ≤ 0
⊢ a + b ≤ 0

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u
inst✝¹ : Semiring α
inst✝ : PartialOrder α
a b : α
ha : a = 0
hb : b < 0
⊢ a + b < 0

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u
inst✝¹ : Semiring α
inst✝ : PartialOrder α
a b : α
ha : a ≤ 0
hb : b = 0
⊢ a + b ≤ 0

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u
inst✝¹ : Semiring α
inst✝ : PartialOrder α
a b : α
ha : a < 0
hb : b = 0
⊢ a + b < 0

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u
inst✝² : Semiring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
a b : α
ha : a = 0
x✝ : 0 < b
⊢ b * a = 0

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n e t : α
h1 : n * e = t
⊢ n * -e = -t

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a c : R
b : ℕ
x✝ : a ^ b = c
⊢ (a + 0) ^ b = c + 0

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : Semifield R
a b : R
x✝ : a⁻¹ = b
⊢ (a + 0)⁻¹ = b + 0

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : SMul R α
r : R
b t : α
x✝ : ∀ (x : α), r • x = t * x
⊢ r • b = t * b

Tactic:
simp [*]

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
H1 : PartialOrder α
H2 : InfSet α
isGLB_sInf : ∀ (s : Set α), IsGLB s (sInf s)
a b c : α
hac : a ≤ c
hbc : b ≤ c
⊢ c ∈ {x | a ≤ x ∧ b ≤ x}

Tactic:
simp [*]

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
H1 : PartialOrder α
H2 : InfSet α
isGLB_sInf : ∀ (s : Set α), IsGLB s (sInf s)
a b c : α
hab : a ≤ b
hac : a ≤ c
⊢ a ∈ lowerBounds {b, c}

Tactic:
simp [*]

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
H1 : PartialOrder α
H2 : SupSet α
isLUB_sSup : ∀ (s : Set α), IsLUB s (sSup s)
a b c : α
hac : a ≤ c
hbc : b ≤ c
⊢ c ∈ upperBounds {a, b}

Tactic:
simp [*]

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
H1 : PartialOrder α
H2 : SupSet α
isLUB_sSup : ∀ (s : Set α), IsLUB s (sSup s)
a b c : α
hab : a ≤ b
hac : a ≤ c
⊢ a ∈ {x | x ≤ b ∧ x ≤ c}

Tactic:
simp [*]

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, x ∈ s i

Tactic:
rw [← w, Set.mem_iUnion] at p

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.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
a b : β
⊢ ⨆ x ∈ {a, b}, f x = f a ⊔ f b

Tactic:
by
  rw [iSup_insert, iSup_singleton]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
P : ι → α → Prop
⊢ ⋂ i, {x | P i x} = {x | ∀ (i : ι), P i x}

Tactic:
by
  ext
  exact mem_iInter

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
ι' : Sort u_6
p : ι → Prop
q : ι → ι' → Prop
s : (x : ι) → (y : ι') → p x ∧ q x y → Set α
⊢ ⋃ x, ⋃ y, ⋃ (h : p x ∧ q x y), s x y h = ⋃ x, ⋃ (hx : p x), ⋃ y, ⋃ (hy : q x y), s x y ⋯

Tactic:
simp only [iUnion_and, @iUnion_comm _ ι']

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
β : α → Type u_9
inst✝ : (i : α) → CompleteLattice (β i)
x✝¹ : Set ((i : α) → β i)
x✝ : α
⊢ IsGLB (eval x✝ '' x✝¹) (sInf (eval x✝ '' x✝¹))

Tactic:
exact isGLB_sInf _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
⊢ ⨆ i ∈ ⋂ j, s j, f i = ⨅ j, ⨆ i ∈ s j, f i

Tactic:
simp_rw [iInf_iSup_eq, mem_iInter]

Goal state after:
α : Type u
inst✝ : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
⊢ ⨆ i, ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i = ⨆ g, ⨆ (_ : ∀ (a : κ), g a ∈ s a), ⨅ a, f (g a)
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteBooleanAlgebra α
s : Set α
hs : s.Nonempty
a : α
⊢ a ∆ sSup s ≤ sSup ((fun x ↦ a ∆ x) '' s)

Tactic:
simpa [symmDiff_comm] using sSup_symmDiff_le (a := a) hs

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
n : α
this : OrderBot α
⊢ sInf s = n → n ∈ s ∧ ∀ a ∈ s, n ≤ a

Tactic:
intro rfl
    exact ⟨csInf_mem hs, fun _ ↦ csInf_le (OrderBot.bddBelow s)⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h : a < b ∨ c < d
⊢ Ico a b = Ico c d ↔ a = c ∧ b = d

Tactic:
refine ⟨fun h ↦ ?_, by grind⟩

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h✝ : a < b ∨ c < d
h : Ico a b = Ico c d
⊢ a = c ∧ b = d
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

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

Tactic:
obtain rfl : t = ∅ := by simpa [Set.eq_empty_iff_forall_notMem] using h
    rfl

Goal state after: