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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
⊢ a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ

Tactic:
by
  by_cases ha : IsUnit a
  · have hb := h.mp ha
    obtain ⟨ia⟩ := ha.nonempty_invertible
    obtain ⟨ib⟩ := hb.nonempty_invertible
    simp_rw [inverse_invertible, invOf_sub_invOf]
  · have hb := h.not.mp ha
    simp [inverse_non_unit, ha, hb]

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

Goal state before:
pp: case inr.inr
R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
hn₀ : n ≠ 0
a b : R
hab : a < b
ha : a ≤ 0
hb : b ≤ 0
c : R
hac : 0 = a + c
d : R
hbd : 0 = b + d
hd : 0 ≤ d
⊢ d + (a + b) < c + (a + b)

Tactic:
rwa [add_rotate', ← hbd, add_zero, add_left_comm, ← add_assoc, ← hac, zero_add]

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

Goal state before:
pp: α✝¹ : Sort u
β✝¹ : Sort v
γ : Sort w
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
f : α → β
s : Set ↑(range f)
x : ↑s
⊢ (fun x ↦ ⟨⟨f ↑x, ⋯⟩, ⋯⟩) ((fun x ↦ ⟨rangeSplitting f ↑x, ⋯⟩) x) = x

Tactic:
by simp [apply_rangeSplitting f]

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}

Tactic:
by_cases ha : a ∈ s

Goal state after:
case pos
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}

case neg
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}
Module: Mathlib.Order.Bounds.Basic

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

Tactic:
obtain rfl | ht := t.eq_empty_or_nonempty
    · aesop
    · exact .inr ⟨h, ht⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
s t : Set α
a : α
ha : a ∈ upperBounds s
b : α
hb : b ∈ upperBounds t
c : α
hca : a ≤ c
hcb : b ≤ c
⊢ BddAbove (s ∪ t)

Tactic:
rw [BddAbove, upperBounds_union]

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
s t : Set α
a : α
ha : a ∈ upperBounds s
b : α
hb : b ∈ upperBounds t
c : α
hca : a ≤ c
hcb : b ≤ c
⊢ (upperBounds s ∩ upperBounds t).Nonempty
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ (Icc a b \ {b}) \ {a}

Tactic:
apply_rules [subset_sdiff_singleton]

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c d : α
h : a ≤ b
h' : c ≤ d
heq : ∀ (x : α), a ≤ x ∧ x ≤ b ↔ c ≤ x ∧ x ≤ d
h₁ : b ≤ d
h₂ : c ≤ a
h₃ : a ≤ c
⊢ a = c ∧ b = d

Tactic:
obtain ⟨-, h₄⟩ := (heq d).mpr ⟨h', le_refl _⟩

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b c d : α
h : a ≤ b
h' : c ≤ d
heq : ∀ (x : α), a ≤ x ∧ x ≤ b ↔ c ≤ x ∧ x ≤ d
h₁ : b ≤ d
h₂ : c ≤ a
h₃ : a ≤ c
h₄ : d ≤ b
⊢ a = c ∧ b = d
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : ℕ → Prop
n : ℕ
inst✝ : DecidablePred p
⊢ (∀ k < n, ¬p k) ↔ n ∈ lowerBounds {n | p n}

Tactic:
simp [mem_lowerBounds, @imp_not_comm _ (p _)]

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommGroup α
n : ℤ
x a : α
n' : ℤ
a' : α
h₁ : -n = n'
h₂ : -a = a'
⊢ -termg n x a = termg n' x a'

Tactic:
by
  simpa [h₂.symm, h₁.symm, termg] using add_comm _ _

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

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

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
m : ℕ
⊢ IsNat (↑↑m) m
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:
rintro ⟨⟨⟩⟩

Goal state after:
R : Type u_1
inst✝ : Ring R
m : ℕ
⊢ IsNat (↑↑m) m
Module: Mathlib.Tactic.NormNum.Basic

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

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
R : Type u_1
inst✝ : Ring R
m : ℤ
⊢ IsInt (↑↑m) m
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc
h₂ : da.mul db = k.mul dc
⊢ IsRat (a + -b) nc dc

Tactic:
refine isRat_add rfl ra (isRat_neg (n' := -nb) rfl rb rfl) (k := k) (nc := nc) ?_ h₂

Goal state after:
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc
h₂ : da.mul db = k.mul dc
⊢ (na.mul ↑db).add ((-nb).mul ↑da) = (↑k).mul nc
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
h₂ : ↑nc * ↑(da * db) * (⅟↑da * ⅟↑db * ⅟↑dc) = ↑nc * ↑(k * dc) * (⅟↑da * ⅟↑db * ⅟↑dc)
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc

Tactic:
simp only [Nat.cast_mul, ← mul_assoc] 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
h₂ : ↑nc * ↑da * ↑db * ⅟↑da * ⅟↑db * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
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
h₂ : ↑nc * ↑(da * db) * (⅟↑da * ⅟↑db * ⅟↑dc) = ↑nc * ↑(k * dc) * (⅟↑da * ⅟↑db * ⅟↑dc)
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc

Tactic:
simp only [Nat.cast_mul, ← mul_assoc] at h₂

Goal state after:
α : Type u_1
inst✝ : Ring α
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
h₂ : ↑nc * ↑da * ↑db * ⅟↑da * ⅟↑db * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑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 b c : α
hc : c < 0
⊢ b / c < a ↔ c * a < b

Tactic:
by
  rw [mul_comm, div_lt_iff_of_neg hc]

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

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

Tactic:
by_cases hl : l = []

Goal state after:
case pos
α : Type u
a : α
l : List α
ih : ∀ (h : l ≠ []), drop (l.length - 1) l = [l.getLast h]
h : a :: l ≠ []
hl : l = []
⊢ drop ((a :: l).length - 1) (a :: l) = [(a :: l).getLast h]

case neg
α : Type u
a : α
l : List α
ih : ∀ (h : l ≠ []), drop (l.length - 1) l = [l.getLast h]
h : a :: l ≠ []
hl : ¬l = []
⊢ drop ((a :: l).length - 1) (a :: l) = [(a :: l).getLast h]
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: case pos
α : Type u
a : α
l : List α
ih : ∀ (h : l ≠ []), drop (l.length - 1) l = [l.getLast h]
h : a :: l ≠ []
hl : l = []
⊢ drop ((a :: l).length - 1) (a :: l) = [(a :: l).getLast h]

pp: case neg
α : Type u
a : α
l : List α
ih : ∀ (h : l ≠ []), drop (l.length - 1) l = [l.getLast h]
h : a :: l ≠ []
hl : ¬l = []
⊢ drop ((a :: l).length - 1) (a :: l) = [(a :: l).getLast h]

Tactic:
· simp_all

Goal state after:
case neg
α : Type u
a : α
l : List α
ih : ∀ (h : l ≠ []), drop (l.length - 1) l = [l.getLast h]
h : a :: l ≠ []
hl : ¬l = []
⊢ drop ((a :: l).length - 1) (a :: l) = [(a :: l).getLast h]
Module: Mathlib.Algebra.Order.Field.Basic

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

Tactic:
by
  simpa using one_div_lt_one_div_of_neg_of_lt (one_div b ▸ inv_lt_zero'.2 hb) h

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 : α
hc : a * b < c
hb : b ≤ 0
a' : α
ha' : a < a'
⊢ ∃ a' > a, a' * b < c

Tactic:
exact ⟨a', ha', hc.trans_le' (antitone_mul_right hb ha'.le)⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
hr : BiUnique R
a : α
b : β
h : R a b
a' : α
as : List α
b' : β
bs : List β
h₁ : R a' b'
h₂ : Forall₂ R as bs
⊢ (fun x1 x2 ↦ x1 ∈ x2) a (a' :: as) ↔ (fun x1 x2 ↦ x1 ∈ x2) b (b' :: bs)

Tactic:
simp only [mem_cons]
    exact rel_or (rel_eq hr h h₁) (rel_mem hr h h₂)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
p : α → Bool
q : β → Bool
hpq : (R ⇒ fun x1 x2 ↦ x1 ↔ x2) (fun x ↦ p x = true) fun x ↦ q x = true
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
⊢ Forall₂ R (filter p (a :: as)) (filter q (b :: bs))

Tactic:
by
    dsimp [LiftFun] at hpq
    by_cases h : p a
    · have : q b := by rwa [← hpq h₁]
      simp only [filter_cons_of_pos h, filter_cons_of_pos this, forall₂_cons, h₁, true_and,
        rel_filter hpq h₂]
    · 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.Perm.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
this : l ⊆ [a, b] ↔ ∀ (c : α), c ≠ b → c ≠ a → ¬c ∈ l
⊢ (count a l = count a (replicate m a ++ replicate n b) ∧
      (b ≠ a → count b l = count b (replicate m a ++ replicate n b)) ∧
        ∀ (b_1 : α), b_1 ≠ b → b_1 ≠ a → count b_1 l = count b_1 (replicate m a ++ replicate n b)) ↔
    count a l = m ∧ count b l = n ∧ l ⊆ [a, b]

Tactic:
by
    simp +contextual [count_replicate, h, this, count_eq_zero, Ne.symm]

Goal state after:
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:
simp [← prod_append]

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
h : l₂ ≠ []
⊢ (l₁ ++ l₂).getLast ⋯ = l₂.getLast h

Tactic:
induction l₁ with grind

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

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

Tactic:
| cons z l IH =>

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

Goal state before:
pp: α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a b : α
l : List α
h : a ∈ b :: l
⊢ f a * (map f ((b :: l).erase a)).prod = (map f (b :: l)).prod

Tactic:
obtain rfl | ⟨ne, h⟩ := List.eq_or_ne_mem_of_mem h
    · simp only [map, erase_cons_head, prod_cons]
    · simp only [map, erase_cons_tail (not_beq_of_ne ne.symm), prod_cons, prod_map_erase _ h,
        mul_left_comm (f a) (f b)]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
r : ℤ
hr : r ≠ 0
x : M
hx : x = l.eval
⊢ x ^ r = (l ^ r).eval

Tactic:
rw [← zpow'_of_ne_zero_right x r hr, eval_zpow', hx]

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

Goal state before:
pp: n₁ d₁ n₂ d₂ : ℤ
⊢ n₁ /. d₁ / (n₂ /. d₂) = n₁ * d₂ /. (d₁ * n₂)

Tactic:
rw [div_def, inv_divInt, divInt_mul_divInt]

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : a ∈ l
⊢ (l.erase a).length + 1 = l.length

Tactic:
rw [erase_eq_eraseP, length_eraseP_add_one h BEq.rfl]

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

Goal state before:
pp: case cons
j : ℕ
L : List ℕ
IH : (∀ (i : ℕ), i ∈ L → 1 ≤ i) → L.length ≤ L.sum
h : ∀ (i : ℕ), i ∈ j :: L → 1 ≤ i
⊢ (j :: L).length ≤ (j :: L).sum

Tactic:
rw [sum_cons, length, add_comm]
    exact Nat.add_le_add (h _ mem_cons_self) (IH fun i hi => h i (mem_cons.2 (Or.inr hi)))

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

Goal state before:
pp: x : ℤ
hx : x ≠ 0
n d : ℤ
⊢ n /. x * (x /. d) = n /. d

Tactic:
by
  by_cases hd : d = 0
  · rw [hd]
    simp
  rw [divInt_mul_divInt, x.mul_comm, divInt_mul_right hx]

Goal state after:
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:
by rw [Rat.mk_eq_divInt, Rat.divInt_eq_div]; exact div n d nz red

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

Goal state before:
pp: q : ℚ
⊢ 0 < q.toNNRat ↔ 0 < q

Tactic:
simp [toNNRat, ← coe_lt_coe]

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

Goal state before:
pp: q : ℚ
p : ℚ≥0
hq : 0 ≤ q
⊢ q.toNNRat < p ↔ q < ↑p

Tactic:
rw [← coe_lt_coe, Rat.coe_toNNRat q hq]

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
hbd : Commute b d
hbc : Commute b⁻¹ c
⊢ a / b * (c / d) = a * c / (b * d)

Tactic:
by
  simp_rw [div_eq_mul_inv, mul_inv_rev, hbd.inv_inv.symm.eq, hbc.mul_mul_mul_comm]

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

Goal state before:
pp: a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ (Int.negOfNat a).pow b = Int.negOfNat c

Tactic:
by
  rw [← hb, Int.negOfNat_eq, Int.negOfNat_eq, Int.pow_eq, pow_succ, pow_mul, neg_pow_two, ← pow_mul,
    two_mul, pow_add, ← hc, ← h1]
  simp [mul_comm, mul_left_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : Field α
n1 n2 k e1 e2 t1 : α
h1 : n1 * e1 = t1
h2 : n2 / e2 = 1
h3 : n1 * n2 = k
⊢ k * (e1 / e2) = t1

Tactic:
by
  rw [← h3, mul_assoc, mul_div_left_comm, h2, ← mul_assoc, h1, mul_comm, one_mul]

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

Goal state before:
pp: α : Type u_1
inst✝ : SupSet α
p : Prop
f₁ f₂ : p → α
pq : p ↔ p
f : ∀ (x : p), f₁ ⋯ = f₂ x
x : p
⊢ f₁ x = f₂ x

Tactic:
apply f

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a b : α
s : α → Set β
⊢ ⋂ x ∈ {a, b}, s x = s a ∩ s b

Tactic:
rw [biInter_insert, biInter_singleton]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
⊢ ⨅ i, ⨆ j, f i j = ⨆ g, ⨅ i, f i (g i)

Tactic:
refine le_antisymm ?_ le_iInf_iSup

Goal state after:
α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
⊢ ⨅ i, ⨆ j, f i j ≤ ⨆ g, ⨅ i, f i (g i)
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, ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i = ⨆ g, ⨆ (_ : ∀ (a : κ), g a ∈ s a), ⨅ a, f (g a)

Tactic:
refine le_antisymm
    (iSup₂_le fun i hi ↦ le_iSup₂_of_le (fun _ ↦ i) hi (le_iInf fun _ ↦ le_rfl))
    (iSup₂_le fun I hI ↦ ?_)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice β
S : Set (Set α)
f : α → β
⊢ ⨆ x ∈ ⋃₀ S, f x = ⨆ s ∈ S, ⨆ x ∈ s, f x

Tactic:
rw [sUnion_eq_iUnion, iSup_iUnion, ← iSup_subtype'']

Goal state after:
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : Lattice α
inst✝ : OrderBot α
⊢ ComplementedLattice ↑(Iic a) ↔ ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a

Tactic:
complementedLattice_iff,

Goal state after:
α : Type u_1
a : α
inst✝¹ : Lattice α
inst✝ : OrderBot α
⊢ (∀ (a_1 : ↑(Iic a)), ∃ b, IsCompl a_1 b) ↔ ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
a b : α
inst✝ : DenselyOrdered α
⊢ Ioi b ⊆ Ici a ↔ a ≤ b

Tactic:
refine ⟨fun h => ?_, Ioi_subset_Ici⟩

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
a b : α
inst✝ : DenselyOrdered α
h : Ioi b ⊆ Ici a
⊢ a ≤ b
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ a ∉ Ι b c ↔ a ≤ b ∧ a ≤ c ∨ c < a ∧ b < a

Tactic:
by
  simp only [uIoc_eq_union, mem_union, mem_Ioc, ← not_le]
  tauto

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: case inr.inl
α : Type u_1
r : α → α → Prop
s : Set α
inst✝ : Std.Trichotomous r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a = b
⊢ a = b

pp: case inr.inr
α : Type u_1
r : α → α → Prop
s : Set α
inst✝ : Std.Trichotomous r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : r b a
⊢ a = b

Tactic:
· exact hab

Goal state after:
case inr.inr
α : Type u_1
r : α → α → Prop
s : Set α
inst✝ : Std.Trichotomous r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : r b a
⊢ a = b
Module: Mathlib.Algebra.Order.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
⊢ 0 ≤ 1

Tactic:
simp only [← le, zero, one, zero_le_one]

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

Goal state before:
pp: m n : ℕ
hn : 1 < n
h : n ! = m !
⊢ n = m

Tactic:
obtain hnm | rfl | hnm := lt_trichotomy n m

Goal state after:
case inl
m n : ℕ
hn : 1 < n
h : n ! = m !
hnm : n < m
⊢ n = m

case inr.inl
n : ℕ
hn : 1 < n
h : n ! = n !
⊢ n = n

case inr.inr
m n : ℕ
hn : 1 < n
h : n ! = m !
hnm : m < n
⊢ n = m
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: k n m : ℕ
h : n ≤ m
⊢ n.ascFactorial k ≤ m.ascFactorial k

Tactic:
induction k with
  | zero => rfl
  | succ k ih => exact Nat.mul_le_mul (by lia) ih

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

Goal state before:
pp: n : ℕ
⊢ n.descFactorial 0 = 0 ↔ n < 0

Tactic:
by simp only [descFactorial_zero, Nat.one_ne_zero, Nat.not_lt_zero]

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

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

Tactic:
have hd := @den_div_eq_of_coprime q.num q.den ?hdp q.coprime_num_den

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

Goal state before:
pp: a b : ℕ+
⊢ a - b ≤ a

Tactic:
rw [← coe_le_coe, sub_coe]

Goal state after:
a b : ℕ+
⊢ (if b < a then ↑a - ↑b else 1) ≤ ↑a
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: a b : ℕ+
hab : a < b
⊢ a ≤ b - 1

Tactic:
rw [← coe_le_coe, sub_coe]

Goal state after:
a b : ℕ+
hab : a < b
⊢ ↑a ≤ if 1 < b then ↑b - ↑1 else 1
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:
rintro ⟨⟨⟩⟩

Goal state after:
R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℕ
⊢ IsNat ⌊↑m⌋ m
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:
rintro ⟨⟨⟩⟩

Goal state after:
R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℤ
⊢ IsInt ⌊↑m⌋ m
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:
rintro ⟨⟨⟩⟩

Goal state after:
R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℕ
⊢ IsNat ⌈↑m⌉ m
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:
rintro ⟨⟨⟩⟩

Goal state after:
R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℤ
⊢ IsInt ⌈↑m⌉ m
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
r : R
m : ℕ
⊢ IsNat r m → IsNat (fract r) 0

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℕ
⊢ IsNat (fract ↑m) 0
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
r : R
m : ℤ
⊢ IsInt r m → IsNat (fract r) 0

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℤ
⊢ IsNat (fract ↑m) 0
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 (round r) m

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℕ
⊢ IsNat (round ↑m) m
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 (round r) m

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
R : Type u_3
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
m : ℤ
⊢ IsInt (round ↑m) m
Module: Mathlib.Data.List.Count

Goal state before:
pp: α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
p : α → Bool
l : List α
a : α
⊢ countP p (l.erase a) = countP p l - if a ∈ l ∧ p a = true then 1 else 0

Tactic:
grind [countP_eq_length_filter]

Goal state after:
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
a b : α
⊢ (a ::ₘ {b}).card = 2

Tactic:
card_cons,

Goal state after:
α : Type u_1
a b : α
⊢ {b}.card + 1 = 2
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case refine_2
α : Type u_1
m✝ : Multiset α
r : α → α → Prop
a : α
m : Multiset α
ih : (∀ (x : α), x ∈ m → r x x) → Rel r m m
h : ∀ (x : α), x ∈ a ::ₘ m → r x x
⊢ Rel r (a ::ₘ m) (a ::ₘ m)

Tactic:
exact Rel.cons (h _ (mem_cons_self _ _)) (ih fun _ ha => h _ (mem_cons_of_mem ha))

Goal state after: