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 b : R
inst✝ : ExistsAddOfLE R
⊢ a * a + a * b + (b * b + b * a) = a * a + b * b + (a * b + b * a)

Tactic:
add_add_add_comm

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

Goal state before:
pp: u v : ℤ
h : u * v = 1
h' : v * u = 1
⊢ u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1

Tactic:
obtain rfl | rfl := eq_one_or_neg_one_of_mul_eq_one h

Goal state after:
case inl
v : ℤ
h : 1 * v = 1
h' : v * 1 = 1
⊢ 1 = 1 ∧ v = 1 ∨ 1 = -1 ∧ v = -1

case inr
v : ℤ
h : -1 * v = 1
h' : v * -1 = 1
⊢ -1 = 1 ∧ v = 1 ∨ -1 = -1 ∧ v = -1
Module: Mathlib.Algebra.Order.Ring.Abs

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

Tactic:
simp only [le_antisymm_iff, sq_le_sq]

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_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ image2 f (image2 g s t) u = image2 g' (image2 f' s u) t

Tactic:
rw [image2_swap g, image2_swap g']

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_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ image2 f (image2 (fun a b ↦ g b a) t s) u = image2 (fun a b ↦ g' b a) t (image2 f' s u)
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
val✝ : β
h : Sum.inr val✝ ∈ range Sum.inl
⊢ False

Tactic:
rcases h with ⟨x, h'⟩; cases h'

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
val✝ : α
h : Sum.inl val✝ ∈ range Sum.inr
⊢ False

Tactic:
rcases h with ⟨x, h'⟩; cases h'

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

Goal state before:
pp: γ : Type u_3
inst✝ : PartialOrder γ
j i : γ
hj : IsLUB (Iio i) j
⊢ j = i ∨ Iio i = Iic j

Tactic:
rcases eq_or_lt_of_le (le_of_isLUB_Iio i hj) with hj_eq_i | hj_lt_i
  · exact Or.inl hj_eq_i
  · right
    exact Set.ext fun k => ⟨fun hk_lt => hj.1 hk_lt, fun hk_le_j => lt_of_le_of_lt hk_le_j hj_lt_i⟩

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

Goal state before:
pp: γ : Type u_3
inst✝ : LinearOrder γ
i : γ
⊢ ∃ j, IsLUB (Iio i) j

Tactic:
by
  by_cases! h_exists_lt : ∃ j, j ∈ upperBounds (Iio i) ∧ j < i
  · obtain ⟨j, hj_ub, hj_lt_i⟩ := h_exists_lt
    exact ⟨j, hj_ub, fun k hk_ub => hk_ub hj_lt_i⟩
  · refine ⟨i, fun j hj => le_of_lt hj, ?_⟩
    rw [mem_lowerBounds]
    exact h_exists_lt

Goal state after:
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
⊢ a / b ≤ 1 ↔ b ≤ a

Tactic:
rw [div_le_iff_of_neg hb, one_mul]

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

Goal state before:
pp: α : Type u_1
⊢ (Forall₂ fun x1 x2 ↦ x1 = x2) = Eq

Tactic:
funext a b; apply propext
  constructor
  · intro h
    induction h
    · rfl
    simp only [*]
  · rintro rfl
    exact forall₂_refl _

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₂.length ≤ n
hm : m ≥ l₁.length
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂

Tactic:
eraseIdx_of_length_le h,

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

Goal state before:
pp: case e_tail
α : Type u
hα : Subsingleton α
head✝¹ : α
tail✝¹ : List α
ih : ∀ ⦃l2 : List α⦄, tail✝¹.length = l2.length → tail✝¹ = l2
head✝ : α
tail✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
⊢ tail✝¹ = tail✝

Tactic:
apply ih

Goal state after:
case e_tail
α : Type u
hα : Subsingleton α
head✝¹ : α
tail✝¹ : List α
ih : ∀ ⦃l2 : List α⦄, tail✝¹.length = l2.length → tail✝¹ = l2
head✝ : α
tail✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
⊢ tail✝¹.length = tail✝.length
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case e_tail
α : Type u
hα : Subsingleton α
head✝¹ : α
tail✝¹ : List α
ih : ∀ ⦃l2 : List α⦄, tail✝¹.length = l2.length → tail✝¹ = l2
head✝ : α
tail✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
⊢ tail✝¹ = tail✝

Tactic:
apply ih; simpa using hl

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
h' : ∀ (n : ℕ), n < max l₁.length l₂.length → l₁[n]? = l₂[n]?
⊢ l₁ = l₂

Tactic:
apply ext_getElem?

Goal state after:
α : Type u
l₁ l₂ : List α
h' : ∀ (n : ℕ), n < max l₁.length l₂.length → l₁[n]? = l₂[n]?
⊢ ∀ (i : ℕ), l₁[i]? = l₂[i]?
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
n : ℤ
e : M
he : e ≠ 0
L l l' : NF M
h : L.eval * l.eval = l'.eval
⊢ ((n + -n, e) ::ᵣ l').eval = l'.eval

Tactic:
simp [zpow'_zero_of_ne_zero he]

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

Goal state before:
pp: case succ
G : Type u_7
inst✝ : Group G
f : ℕ → G
n : ℕ
h : (map (fun k ↦ f k / f (k + 1)) (range n)).prod = f 0 / f n
⊢ (map (fun k ↦ f k / f (k + 1)) (range (n + 1))).prod = f 0 / f (n + 1)

Tactic:
| succ n h =>

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

Goal state before:
pp: num : ℕ
den : ℤ
n : ℕ
⊢ (↑num /. den) ^ n = ↑num ^ n /. den ^ n

Tactic:
simp [divInt_eq_div, div_pow]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: q : ℚ
⊢ |q| = { num := |q.num|, den := q.den, den_nz := ⋯, reduced := ⋯ }

Tactic:
refine ext ?_ ?_ <;>
    simp [Int.abs_eq_natAbs, abs_def,
      ← Rat.mk_eq_divInt (num := q.num.natAbs) (nz := q.den_ne_zero) (c := q.reduced)]

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

Goal state before:
pp: q : ℚ≥0
⊢ ↑(divNat q.num q.den) = ↑q

Tactic:
← (q : ℚ).mkRat_num_den'

Goal state after:
q : ℚ≥0
⊢ ↑(divNat q.num q.den) = mkRat (↑q).num (↑q).den
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
H : IsRelPrime x y
H1 : x ∣ z
H2 : y ∣ z
hy : IsPrimal y
⊢ x * y ∣ z

Tactic:
by
  obtain ⟨w, rfl⟩ := H1
  exact mul_dvd_mul_left x (H.symm.dvd_of_dvd_mul_left_of_isPrimal H2 hy)

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
x y : α
⊢ x ⊔ y = x ⊔ bif false then x else y

Tactic:
Bool.cond_false

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
x y : α
⊢ x ⊔ y = x ⊔ y
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: case a
α : Type u_1
inst✝² : CompleteLattice α
ι : Type u_8
inst✝¹ : LT ι
inst✝ : NoMaxOrder ι
f : ι → α
⊢ ⨆ i, ⨆ j, ⨆ (_ : j < i), f j ≤ ⨆ i, f i

Tactic:
exact iSup_le fun _ ↦ iSup₂_le fun _ _ ↦ le_iSup _ _

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

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : Preorder ι
f : ι → α
⊢ ⨆ i, ⨆ j, ⨆ (_ : j ≤ i), f j ≤ ⨆ i, f i

Tactic:
exact iSup_le fun _ ↦ iSup₂_le fun _ _ ↦ le_iSup _ _

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

Goal state before:
pp: case a
α : Type u_1
inst✝² : CompleteLattice α
ι : Type u_8
inst✝¹ : LT ι
inst✝ : NoMinOrder ι
f : ι → α
⊢ ⨆ i, ⨆ j, ⨆ (_ : j > i), f j ≤ ⨆ i, f i

Tactic:
exact iSup_le fun _ ↦ iSup₂_le fun _ _ ↦ le_iSup _ _

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

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : Preorder ι
f : ι → α
⊢ ⨆ i, ⨆ j, ⨆ (_ : j ≥ i), f j ≤ ⨆ i, f i

Tactic:
exact iSup_le fun _ ↦ iSup₂_le fun _ _ ↦ le_iSup _ _

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:
by
  simp only [iInter_and, @iInter_comm _ ι']

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

Goal state before:
pp: α : Type u_1
s : Set (Set α)
⊢ ⋂₀ s = ⋂ i ∈ s, i

Tactic:
rw [← sInter_image, image_id']

Goal state after:
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:
by
  rw [sUnion_eq_iUnion, iInf_iUnion, ← iInf_subtype'']

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
haS : a ∈ S
⊢ (if S ⊆ {⊤} ∨ ¬BddBelow S then ⊤ else ↑(sInf ((fun a ↦ ↑a) ⁻¹' S))) ≤ a

Tactic:
simp only [OrderBot.bddBelow, not_true_eq_false, or_false]
      split_ifs with h₁
      · cases a
        · exact le_rfl
        cases h₁ haS
      · cases a
        · exact le_top
        · apply WithTop.coe_le_coe.2
          refine csInf_le ?_ haS
          use ⊥
          intro b _
          exact bot_le

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

Goal state before:
pp: case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
a₁ a₂ : α
hne : e a₁ ≠ e a₂
⊢ (Disjoint on extend e f ⊥) (e a₁) (e a₂)

pp: case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₂ : β
a₁ : α
hne : e a₁ ≠ b₂
hb₂ : ¬∃ a₂, e a₂ = b₂
⊢ (Disjoint on extend e f ⊥) (e a₁) b₂

Tactic:
· simpa only [onFun, he.extend_apply] using! hf (ne_of_apply_ne e hne)

Goal state after:
case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₂ : β
a₁ : α
hne : e a₁ ≠ b₂
hb₂ : ¬∃ a₂, e a₂ = b₂
⊢ (Disjoint on extend e f ⊥) (e 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:
simp only [uIoc_eq_union, mem_union, mem_Ioc, ← not_le]
  tauto

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
hf : Monotone f
⊢ IsChain (fun x1 x2 ↦ x1 ≤ x2) (range f)

Tactic:
rw [← image_univ]
  exact hf.isChain_image (isChain_of_trichotomous _)

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

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
q : ℚ≥0
ha : 0 ≤ a
⊢ 0 ≤ ↑q * a

Tactic:
exact mul_nonneg q.cast_nonneg ha

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

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
x y : α
q : ℚ≥0
a : α
ha : 0 ≤ a
⊢ 0 ≤ ↑q * a

Tactic:
exact mul_nonneg q.cast_nonneg ha

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : DivInvMonoid α
a : α
⊢ a⁺ᵐ ≤ 1 ↔ a ≤ 1

Tactic:
simp [oneLePart]

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

Goal state before:
pp: n : ℕ
hi : 3 ≤ n
this : 0 < n
hn : 1 < n.pred
⊢ n < n !

Tactic:
← succ_pred_eq_of_pos ‹0 < n›,

Goal state after:
n : ℕ
hi : 3 ≤ n
this : 0 < n
hn : 1 < n.pred
⊢ n.pred.succ < n.pred.succ !
Module: Mathlib.Data.Nat.Factorial.Basic

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

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

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

Goal state before:
pp: n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) ^ (k + 2) < n.descFactorial (k + 2)

Tactic:
refine Nat.lt_of_le_of_lt (Nat.pow_le_pow_left (Nat.sub_le_sub_right n.le_succ _) _) ?_

Goal state after:
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n.succ - (k + 1 + 1)) ^ (k + 2) < n.descFactorial (k + 2)
Module: Mathlib.Algebra.Order.Round

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

Tactic:
rw [← hm, ceil_intCast]

Goal state after:
case inl
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 2 * fract x ≠ 1
m : ℤ
hm : ↑m = 2 * x
⊢ round x = m / 2
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
z : ℤ
a : R
⊢ ⌊↑z + a⌋ = z + ⌊a⌋

Tactic:
by
  simpa only [add_comm] using floor_add_intCast a z

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

Tactic:
sub_le_sub_iff_left,

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ↑⌊a⌋ + ↑⌊b⌋ ≤ ↑⌊a + b⌋
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 + fract x = -↑⌊x⌋

Tactic:
conv in -x => rw [← floor_add_fract x]

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) + fract x = -↑⌊x⌋
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : 0 < n
⊢ R (f (l + n • a)) (f y)

Tactic:
← sub_add_cancel y (n • a),

Goal state after:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : 0 < n
⊢ R (f (l + n • a)) (f (y - n • a + n • a))
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case refine_1
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
m : ℕ
hm : y / δ + 1 / δ ≤ ↑m
⊢ y / δ ≤ ↑m

Tactic:
exact (lt_add_of_pos_right _ <| by positivity).le.trans hm

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

Goal state before:
pp: α : Type u_1
a b : α
⊢ {a} = {b} ↔ a = b

Tactic:
simp_rw [← cons_zero]

Goal state after:
α : Type u_1
a b : α
⊢ a ::ₘ 0 = b ::ₘ 0 ↔ a = b
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hg : (fun i ↦ l[↑i]) ⟨i, hi⟩ = (fun i ↦ l[↑i]) ⟨j, hj⟩
⊢ ⟨i, hi⟩ = ⟨j, hj⟩

Tactic:
rcases Nat.lt_trichotomy i j with (hij | rfl | hji)

Goal state after:
case inl
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hg : (fun i ↦ l[↑i]) ⟨i, hi⟩ = (fun i ↦ l[↑i]) ⟨j, hj⟩
hij : i < j
⊢ ⟨i, hi⟩ = ⟨j, hj⟩

case inr.inl
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi hj : i < l.length
hg : (fun i ↦ l[↑i]) ⟨i, hi⟩ = (fun i ↦ l[↑i]) ⟨i, hj⟩
⊢ ⟨i, hi⟩ = ⟨i, hj⟩

case inr.inr
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hg : (fun i ↦ l[↑i]) ⟨i, hi⟩ = (fun i ↦ l[↑i]) ⟨j, hj⟩
hji : j < i
⊢ ⟨i, hi⟩ = ⟨j, hj⟩
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a b : α
h : a ∈ s
⊢ (b ::ₘ s).erase a = b ::ₘ s.erase a

Tactic:
rcases eq_or_ne a b with rfl | hab

Goal state after:
case inl
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
⊢ (a ::ₘ s).erase a = a ::ₘ s.erase a

case inr
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a b : α
h : a ∈ s
hab : a ≠ b
⊢ (b ::ₘ s).erase a = b ::ₘ s.erase a
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
h : s ≤ a ::ₘ t
m : a ∈ s
⊢ s.erase a ≤ t

Tactic:
by rw [← cons_erase m] at h; exact (cons_le_cons_iff _).1 h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ a ∈ s - t ↔ count a t < count a s

Tactic:
by
  rw [← count_pos, count_sub, Nat.sub_pos_iff_lt]

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type v
r : α → β → Prop
as₀ as₁ : Multiset α
a : α
s : Multiset α
ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
bs : Multiset β
⊢ (∃ bs₀ bs₁, (∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁) →
    ∃ b bs', r a b ∧ (∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs'

Tactic:
· intro h
        rcases h with ⟨bs₀, bs₁, h, h₁, rfl⟩
        rcases h with ⟨b, bs, hab, h₀, rfl⟩
        exact ⟨b, bs + bs₁, hab, ⟨bs, bs₁, h₀, h₁, rfl⟩, by simp⟩

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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ : List α
a : α
l₂ : List α
hl₁ : l₁.Nodup
⊢ l₁.diff (a :: l₂) = List.filter (fun x ↦ decide ¬x ∈ a :: l₂) l₁

Tactic:
rw [diff_cons, (hl₁.erase _).sdiff_eq_filter, hl₁.erase_eq_filter, filter_filter]

Goal state after:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ : List α
a : α
l₂ : List α
hl₁ : l₁.Nodup
⊢ List.filter (fun a_1 ↦ decide ¬a_1 ∈ l₂ && a_1 != a) l₁ = List.filter (fun x ↦ decide ¬x ∈ a :: l₂) l₁
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
⊢ xs ∪ ys.dedup = xs.dedup ++ ys.dedup

Tactic:
Disjoint.union_eq

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
⊢ xs.dedup ++ ys.dedup = xs.dedup ++ ys.dedup

α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs.Disjoint ys
⊢ xs.Disjoint ys.dedup
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l t₁ t₂ : List α
p : t₁ ~ t₂
⊢ l.bagInter t₁ = l.bagInter t₂

Tactic:
induction l generalizing t₁ t₂ p with | nil => simp | cons a l IH => ?_

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {t₁ t₂ : List α}, t₁ ~ t₂ → l.bagInter t₁ = l.bagInter t₂
t₁ t₂ : List α
p : t₁ ~ t₂
⊢ (a :: l).bagInter t₁ = (a :: l).bagInter t₂
Module: Mathlib.Data.Multiset.Basic

Goal state before:
pp: α : Type u_1
p : Multiset α → Sort u_3
s : Multiset α
H : (s : Multiset α) → ((t : Multiset α) → t < s → p t) → p s
⊢ s.strongInductionOn H = H s fun t _h ↦ t.strongInductionOn H

Tactic:
strongInductionOn

Goal state after:
α : Type u_1
p : Multiset α → Sort u_3
s : Multiset α
H : (s : Multiset α) → ((t : Multiset α) → t < s → p t) → p s
⊢ (H s fun t _h ↦ t.strongInductionOn H) = H s fun t _h ↦ t.strongInductionOn H
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h₁ : s ≤ u
h₂ : t ≤ u
⊢ s ∪ t ≤ u

Tactic:
rw [← eq_union_left h₂]; exact union_le_union_right h₁ t

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
⊢ 0 = (filter (fun a ↦ p (f a)) 0).card

Tactic:
filter_zero,

Goal state after:
case refine_1
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
⊢ 0 = card 0
Module: Mathlib.Data.Finset.Dedup

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.toList.Nodup

Tactic:
by
  rw [toList, ← Multiset.coe_nodup, Multiset.coe_toList]
  exact s.nodup

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
b : α
⊢ filter (Eq b) s = replicate (count b s) b

Tactic:
simp_rw [← filter_eq', eq_comm]

Goal state after:
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ (Multiset.map Subtype.val s.val.attach).dedup = s.val

Tactic:
Multiset.attach_map_val,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ s.val.dedup = s.val
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: n : ℕ
⊢ range (n + 1) \ {0} = image Nat.succ (range n)

Tactic:
induction n with
  | zero => simp
  | succ k hk =>
    conv_rhs => rw [range_add_one]
    rw [range_add_one, image_insert, ← hk, insert_sdiff_of_notMem]
    simp

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

Goal state before:
pp: case h.refine_1
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < ↑(e ⟨i, hi⟩)
this : e.symm ⟨j, ⋯⟩ < ⟨i, hi⟩
⊢ j < i

Tactic:
specialize h _ this (e.symm _).is_lt

Goal state after:
case h.refine_1
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
hi : i < n
j : ℕ
hj : j < ↑(e ⟨i, hi⟩)
h : ↑(e ⟨↑(e.symm ⟨j, ⋯⟩), ⋯⟩) = ↑(e.symm ⟨j, ⋯⟩)
this : e.symm ⟨j, ⋯⟩ < ⟨i, hi⟩
⊢ j < i
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case h
n : ℕ
motive : Fin n → Prop
h : ∀ (j : Fin n), (∀ (k : Fin n), k < j → motive k) → motive j
j : ℕ
hj : ∀ (m : ℕ), m < j → ∀ (hi : m < n), motive ⟨m, hi⟩
hi : j < n
⊢ motive ⟨j, hi⟩

Tactic:
| h j hj =>

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a : Fin (n + 1)
ha : a ≠ last n
⊢ (a.castPred ha).succ = a + 1

Tactic:
cases a using lastCases
  · exact (ha rfl).elim
  · rw [castPred_castSucc, coeSucc_eq_succ]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
⊢ cons x p i.succ = p i

Tactic:
by simp [cons]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
⊢ cons x p 0 = x

Tactic:
by simp [cons]

Goal state after:
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case refine_2
α : Type u_1
s : Finset α
inst✝ : Nonempty α
⊢ (∃ x, s ⊆ {x}) → #s ≤ 1

Tactic:
rintro ⟨x, hx⟩
    rw [← card_singleton x]
    exact card_le_card hx

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case neg
n : ℕ
p i : Fin n
hi : ¬i ≤ p
⊢ ∃ a, p.predAbove a = i

Tactic:
· rw [Fin.not_le] at hi
    exact ⟨i.succ, predAbove_succ_of_le p i (Fin.le_of_lt hi)⟩

Goal state after: