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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
f : α ↪o β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
a₁ a₂ : α
h : Disjoint (f a₁) (f a₂)
x : α
h₁ : x ≤ a₁
h₂ : x ≤ a₂
⊢ x ≤ ⊥

Tactic:
← f.le_iff_le

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
f : α ↪o β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
a₁ a₂ : α
h : Disjoint (f a₁) (f a₂)
x : α
h₁ : f x ≤ f a₁
h₂ : f x ≤ f a₂
⊢ f x ≤ f ⊥
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ a ^ (n + 2) ≤ b ^ (n + 2 - 1) * a

Tactic:
by
    calc
      a ^ (n + 2) = a ^ (n + 1) * a := by rw [pow_succ]
      _ ≤ b ^ n * a * a := by grw [pow_le_pow_mul_of_sq_le_mul hab (by lia)]; simp
      _ = b ^ n * a ^ 2 := by rw [mul_assoc, sq]
      _ ≤ b ^ n * (b * a) := by grw [hab]
      _ = b ^ (n + 1) * a := by rw [← mul_assoc, ← pow_succ]

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

Goal state before:
pp: case inr.inl.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : |a * b|ₘ = a⁻¹ * b
ab : a * b ≤ 1
⊢ b⁻¹ = b

Tactic:
mabs_of_le_one ab,

Goal state after:
case inr.inl.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
hab : a ≤ b
ha : a < 1
hb : 1 ≤ b
this : (|a * b|ₘ = a⁻¹ * b ↔ b ≤ 1) ↔ (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
h : (a * b)⁻¹ = a⁻¹ * b
ab : a * b ≤ 1
⊢ b⁻¹ = b
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case inr
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a : α
h : a ≤ 1
⊢ |a|ₘ⁻¹ ≤ a

Tactic:
· simp [mabs_of_le_one h]

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

Goal state before:
pp: n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ ↑p * ↑q ≤ ↑n

Tactic:
← Nat.cast_mul,

Goal state after:
n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ ↑(p * q) ≤ ↑n
Module: Mathlib.Algebra.GroupWithZero.Regular

Goal state before:
pp: R : Type u_1
inst✝ : MulZeroClass R
⊢ ¬IsRightRegular 0 ↔ Nontrivial R

Tactic:
rw [nontrivial_iff, not_iff_comm, isRightRegular_zero_iff_subsingleton, subsingleton_iff]

Goal state after:
R : Type u_1
inst✝ : MulZeroClass R
⊢ (¬∃ x y, x ≠ y) ↔ ∀ (x y : R), x = y
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case some.some
α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
b c : α
⊢ ↑a + Option.some b ≤ ↑a + Option.some c → Option.some b ≤ Option.some c

Tactic:
· simpa [none_eq_top, some_eq_coe, ← coe_add] using fun a ↦ ha a

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
hc : AddLECancellable c
h₁ : b ≤ a
h₂ : c ≤ a
⊢ a < b + c ↔ a - c < b

Tactic:
hc.tsub_lt_iff_right h₂

Goal state after:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
hc : AddLECancellable c
h₁ : b ≤ a
h₂ : c ≤ a
⊢ a < b + c ↔ a < b + c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝ : AddMonoid α
a : WithTop α
⊢ 0 • a = 0

Tactic:
by simp_rw [HSMul.hSMul, SMul.smul]; cases a <;> simp [zero_nsmul]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LE α
x : WithBot α
hx : x ≠ ⊥
⊢ a ≤ x.unbot hx ↔ ↑a ≤ x

Tactic:
by lift x to α using hx; simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LE α
x : WithBot α
hx : x ≠ ⊥
⊢ x.unbot hx ≤ a ↔ x ≤ ↑a

Tactic:
by lift x to α using hx; simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a b : α
inst✝ : LE α
x : WithBot α
hx : x ≠ ⊥
⊢ b ≤ unbotD a x ↔ ↑b ≤ x

Tactic:
by lift x to α using hx; simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LT α
x : WithBot α
hx : x ≠ ⊥
⊢ a < x.unbot hx ↔ ↑a < x

Tactic:
by lift x to α using hx; simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
b : α
inst✝ : LT α
x : WithBot α
hx : x ≠ ⊥
⊢ x.unbot hx < b ↔ x < ↑b

Tactic:
by lift x to α using hx; simp

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
a b : α
inst✝ : LT α
x : WithBot α
hx : x ≠ ⊥
⊢ b < unbotD a x ↔ ↑b < x

Tactic:
by lift x to α using hx; simp

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

Goal state before:
pp: case refine_3.inr
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
x✝ : Nontrivial αˣ ∧ DenselyOrdered αˣ
H₁ : Nontrivial αˣ
H₂ : DenselyOrdered αˣ
x : α
y : αˣ
h : x < ↑y
hx : 0 < x
⊢ ∃ a, x < a ∧ a < ↑y

Tactic:
· lift x to αˣ using hx.ne'.isUnit
      obtain ⟨z, hz, hz'⟩ := H₂.dense x y (Units.val_lt_val.mpr h)
      exact ⟨z, by simp [hz, hz']⟩

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

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

Tactic:
· exact (findGreatest_eq_iff.1 rfl).2.1 h

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

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

Tactic:
by
  rwa [← coe_unzero ha, coe_lt_coe, ← ofAdd_toAdd (unzero ha), ofAdd_lt]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x : WithTop αᵒᵈ
y : WithBot α
⊢ x < WithBot.toDual y ↔ y < WithTop.ofDual x

Tactic:
cases x <;> cases y <;> simp [lt_toDual]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : LT α
x : WithTop α
y : WithBot αᵒᵈ
⊢ x < WithBot.ofDual y ↔ y < WithTop.toDual x

Tactic:
cases x <;> cases y <;> simp [lt_toDual]

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

Goal state before:
pp: R : Type u_3
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
a : R
ha : a < 0
⊢ 0 < a ^ 2

Tactic:
by rw [sq]; exact mul_pos_of_neg_of_neg ha ha

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

Goal state before:
pp: u v : ℤ
hu : IsUnit u
hv : IsUnit v
⊢ u ≠ v ↔ u = -v

Tactic:
obtain rfl | rfl := isUnit_eq_one_or hu <;> obtain rfl | rfl := isUnit_eq_one_or hv

Goal state after:
case inl.inl
hu hv : IsUnit 1
⊢ 1 ≠ 1 ↔ 1 = -1

case inl.inr
hu : IsUnit 1
hv : IsUnit (-1)
⊢ 1 ≠ -1 ↔ 1 = - -1

case inr.inl
hu : IsUnit (-1)
hv : IsUnit 1
⊢ -1 ≠ 1 ↔ -1 = -1

case inr.inr
hu hv : IsUnit (-1)
⊢ -1 ≠ -1 ↔ -1 = - -1
Module: Mathlib.Algebra.Ring.Int.Units

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

Tactic:
by
  simpa only [Units.ext_iff] using! isUnit_eq_one_or u.isUnit

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

Goal state before:
pp: α : Type u_1
β : Type u_3
s : Set α
t : Set β
h : t.Nonempty
⊢ image2 (fun x x_1 ↦ x) s t = s

Tactic:
simp [nonempty_def.mp h, Set.ext_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
s : Set α
t : Set β
h : s.Nonempty
⊢ image2 (fun x y ↦ y) s t = t

Tactic:
simp [nonempty_def.mp h, Set.ext_iff]

Goal state after:
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_3
s t : Set α
h : s ⊆ t
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ↑t
hx : ↑x ∈ s
⊢ (Set.sumDiffSubset h).symm x = Sum.inl ⟨↑x, hx⟩

Tactic:
by
  apply (Equiv.Set.sumDiffSubset h).injective
  simp only [apply_symm_apply, sumDiffSubset_apply_inl, Set.inclusion_mk]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set β
x : β
⊢ IsLUB (⇑f ⁻¹' s) (f.symm x) ↔ IsLUB s x

Tactic:
isLUB_preimage,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set β
x : β
⊢ IsLUB s (f (f.symm x)) ↔ IsLUB s x
Module: Mathlib.Order.Interval.Set.Basic

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

Tactic:
rw [insert_eq, ← sdiff_sdiff, Icc_sdiff_left, Ioc_sdiff_right]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Ioi x)
a : α
ha : a ∈ Ioi x
⊢ ∃ b, b < ⟨a, ha⟩

Tactic:
rcases exists_between ha with ⟨b, hb₁, hb₂⟩

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Ioi x)
a : α
ha : a ∈ Ioi x
b : α
hb₁ : x < b
hb₂ : b < a
⊢ ∃ b, b < ⟨a, ha⟩
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ (2 + 1) * a / 3 = a

Tactic:
two_add_one_eq_three,

Goal state after:
α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ 3 * a / 3 = a
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b : α
inst✝ : IsStrictOrderedRing α
hb : 0 < b
⊢ 0 < a / b ↔ 0 < a

Tactic:
simp only [div_eq_mul_inv, mul_pos_iff_of_pos_right (inv_pos.2 hb)]

Goal state after:
Module: Mathlib.Control.Functor

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝³ : Functor F
inst✝² : Functor G
inst✝¹ : LawfulFunctor F
inst✝ : LawfulFunctor G
α : Type v
x : F (G α)
⊢ Comp.map id (mk x) = mk x

Tactic:
simp only [Comp.map, id_map, id_map']; rfl

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
N : Type u_3
inst✝¹ : Monoid M
inst✝ : Monoid N
l✝ : List ι
r : M → N → Prop
f : ι → M
g : ι → N
h₁ : r 1 1
h₂ : ∀ ⦃i : ι⦄ ⦃a : M⦄ ⦃b : N⦄, r a b → r (f i * a) (g i * b)
a : ι
l : List ι
hl : r (map f l).prod (map g l).prod
⊢ r (map f (a :: l)).prod (map g (a :: l)).prod

Tactic:
simp only [map_cons, prod_cons, h₂ hl]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
⊢ Forall₂ R (drop l₁.length l) l₂

Tactic:
have h' : Forall₂ R (drop (length l₁) l) (drop (length l₁) (l₁ ++ l₂)) :=
    forall₂_drop (length l₁) h

Goal state after:
α : Type u_1
β : Type u_2
R : α → β → Prop
l : List α
l₁ l₂ : List β
h : Forall₂ R l (l₁ ++ l₂)
h' : Forall₂ R (drop l₁.length l) (drop l₁.length (l₁ ++ l₂))
⊢ Forall₂ R (drop l₁.length l) l₂
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Bool
q : β → Bool
hpq : ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → (p a = true ↔ q b = true)
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
h : ¬p a = true
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))

Tactic:
have : ¬q b := by rwa [← hpq h₁]
      simp only [filter_cons_of_neg h, filter_cons_of_neg this, rel_filter hpq h₂]

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

Goal state before:
pp: case some
α : Type u
l : List α
h : ∀ (x : α), x ∈ l
x : α
⊢ ∃ a, (fun n ↦ l[n]?) a = some x

Tactic:
exact mem_iff_getElem?.mp <| h x

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

Goal state before:
pp: case cons
M : Type u_4
inst✝¹ : Monoid M
l✝ : List M
a : M
inst✝ : DecidableEq M
b : M
l : List M
ih : a ∈ l → (∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x) → a * (l.erase a).prod = l.prod
ha : a ∈ b :: l
comm : ∀ (x : M), x ∈ b :: l → ∀ (y : M), y ∈ b :: l → x * y = y * x
⊢ a * ((b :: l).erase a).prod = (b :: l).prod

Tactic:
| cons b l ih =>

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

Goal state before:
pp: M : Type u_1
inst✝⁴ : GroupWithZero M
inst✝³ : PartialOrder M
inst✝² : PosMulStrictMono M
inst✝¹ : PosMulReflectLT M
inst✝ : ZeroLEOneClass M
r : ℤ
x : M
hx : 0 < x
l : NF M
hl : 0 < l.eval
⊢ 0 < zpow' x r

Tactic:
zpow'_of_ne_zero_left _ _ hx.ne'

Goal state after:
M : Type u_1
inst✝⁴ : GroupWithZero M
inst✝³ : PartialOrder M
inst✝² : PosMulStrictMono M
inst✝¹ : PosMulReflectLT M
inst✝ : ZeroLEOneClass M
r : ℤ
x : M
hx : 0 < x
l : NF M
hl : 0 < l.eval
⊢ 0 < x ^ r
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
x✝ : b = a
e : b = a := x✝
⊢ idxOf b (b :: l) = 0

Tactic:
exact idxOf_cons_self

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

Goal state before:
pp: α : Type u
β : Type v
f g : α → β → β
b : β
l : List α
H : ∀ (a : α), a ∈ l → ∀ (b : β), f a b = g a b
⊢ foldr f b l = foldr g b l

Tactic:
induction l with | nil => rfl | cons hd tl ih => ?_

Goal state after:
case cons
α : Type u
β : Type v
f g : α → β → β
b : β
hd : α
tl : List α
ih : (∀ (a : α), a ∈ tl → ∀ (b : β), f a b = g a b) → foldr f b tl = foldr g b tl
H : ∀ (a : α), a ∈ hd :: tl → ∀ (b : β), f a b = g a b
⊢ foldr f b (hd :: tl) = foldr g b (hd :: tl)
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
s t : List α
hs : ∀ (a : α), a ∈ s → p a
ht : ∀ (a : α), a ∈ t → p a
hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a'
h : s.Disjoint t
⊢ (pmap f s hs).Disjoint (pmap f t ht)

Tactic:
simp only [Disjoint, mem_pmap]

Goal state after:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
s t : List α
hs : ∀ (a : α), a ∈ s → p a
ht : ∀ (a : α), a ∈ t → p a
hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a'
h : s.Disjoint t
⊢ ∀ ⦃a : β⦄, (∃ a_1 h, f a_1 ⋯ = a) → (∃ a_2 h, f a_2 ⋯ = a) → False
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case mpr
q : ℚ
nr : ℤ
hnr : q.num = nr * nr
dr : ℕ
hdr : q.den = dr * dr
⊢ q = ↑(nr * nr) / (↑dr * ↑dr)

Tactic:
← Nat.cast_mul,

Goal state after:
case mpr
q : ℚ
nr : ℤ
hnr : q.num = nr * nr
dr : ℕ
hdr : q.den = dr * dr
⊢ q = ↑(nr * nr) / ↑(dr * dr)
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:
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)
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:
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✝ : 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
⊢ False

Tactic:
have dd := den_dvd a b

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
⊢ False
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ (a < b) = (bd * ad * a < ad * bd * b)

pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < 1 / gcd

Tactic:
mul_comm bd,

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ (a < b) = (ad * bd * a < ad * bd * b)

α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < 1 / gcd
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ (a ≤ b) = (bd * ad * a ≤ ad * bd * b)

pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < 1 / gcd

Tactic:
mul_comm bd,

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ (a ≤ b) = (ad * bd * a ≤ ad * bd * b)

α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < 1 / gcd
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a₁ a₂ : R
⊢ -(a₁ + a₂) = -a₁ + -a₂

Tactic:
simp [add_comm]

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

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
inst✝ : CompleteLattice α
s : Set (ULift α)
⊢ (sSup s).down = ⨆ a ∈ s, a.down

Tactic:
by rw [sSup_eq_iSup', down_iSup, iSup_subtype'']

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

Goal state before:
pp: α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
s : Set β
⊢ l (⨆ a ∈ s, u a) = sSup s

Tactic:
gi.l_biSup_u,

Goal state after:
α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
s : Set β
⊢ ⨆ i ∈ s, i = sSup s
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
minAx : Frame.MinimalAxioms β
f : α → β
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
a : α
s : Set α
⊢ a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b

Tactic:
by
    rw [← le, ← sSup_image, map_inf, map_sSup s, minAx.inf_iSup₂_eq]
    simp_rw [← map_inf]
    exact ((map_sSup _).trans iSup_image).ge

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

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

Tactic:
rintro (⟨⟩ | a) ha

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

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
⊢ Option.some a ≤ ↑(sSup ((fun a ↦ ↑a) ⁻¹' s))
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
⊢ ⊤ ∈ lowerBounds (upperBounds s)

Tactic:
rintro (⟨⟩ | a) ha

Goal state after:
case pos.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
ha : none ∈ upperBounds s
⊢ ⊤ ≤ none

case pos.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
h₁ : ⊤ ∈ s
a : β
ha : Option.some a ∈ upperBounds s
⊢ ⊤ ≤ Option.some a
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s)) ∈ lowerBounds s

Tactic:
rintro (⟨⟩ | a) ha

Goal state after:
case neg.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ s
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s)) ≤ none

case neg.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s)) ≤ Option.some a
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s)) ∈ upperBounds (lowerBounds s)

Tactic:
rintro (⟨⟩ | a) ha

Goal state after:
case neg.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ lowerBounds s
⊢ none ≤ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s))

case neg.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
⊢ Option.some a ≤ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s))
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.some.refine_1
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
a : β
ha : Option.some a ∈ lowerBounds s
h : (fun a ↦ ↑a) ⁻¹' s = ∅
⊢ s ⊆ {⊤}

Tactic:
rintro (⟨⟩ | a) ha

Goal state after:
case neg.some.refine_1.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
a : β
ha✝ : Option.some a ∈ lowerBounds s
h : (fun a ↦ ↑a) ⁻¹' s = ∅
ha : none ∈ s
⊢ none ∈ {⊤}

case neg.some.refine_1.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
a✝ : β
ha✝ : Option.some a✝ ∈ lowerBounds s
h : (fun a ↦ ↑a) ⁻¹' s = ∅
a : β
ha : Option.some a ∈ s
⊢ Option.some a ∈ {⊤}
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ioi a \ Ici b = Ioo a b

Tactic:
rw [sdiff_eq, compl_Ici, Ioi_inter_Iio]

Goal state after: