mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
ht : t.PairwiseDisjoint fun b ↦ (fun a ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
⊢ f x.1 x.2 ∈ (fun a ↦ f a y.2) '' s

Tactic:
h

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
ht : t.PairwiseDisjoint fun b ↦ (fun a ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
⊢ (fun p ↦ f p.1 p.2) y ∈ (fun a ↦ f a y.2) '' s
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
⊢ s.OrdConnected

Tactic:
by
  rw [ordConnected_iff]
  intro x hx y hy hxy
  rcases eq_or_lt_of_le hxy with (rfl | hxy'); · simpa
  rw [← Ioc_insert_left hxy, ← Ioo_insert_right hxy']
  exact insert_subset_iff.2 ⟨hx, insert_subset_iff.2 ⟨hy, hs x hx y hy hxy'⟩⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : (range ⇑e).OrdConnected
x y : α
⊢ ⇑e '' Ico x y = Ico (e x) (e y)

Tactic:
by
  rw [← e.preimage_Ico, image_preimage_eq_inter_range,
    inter_eq_left.2 <| Ico_subset_Icc_self.trans <| he.out ⟨_, rfl⟩ ⟨_, rfl⟩]

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

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝ : decide (num✝¹.mul db ≤ num✝.mul da) = true
h : ↑(num✝¹.mul db) ≤ ↑(num✝.mul da)
ha : 0 ≤ ⅟↑da
hb : 0 ≤ ⅟↑db
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db

Tactic:
have h := (mul_le_mul_of_nonneg_left · hb) <| mul_le_mul_of_nonneg_right h ha

Goal state after:
α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (num✝¹.mul db ≤ num✝.mul da) = true
h✝ : ↑(num✝¹.mul db) ≤ ↑(num✝.mul da)
ha : 0 ≤ ⅟↑da
hb : 0 ≤ ⅟↑db
h : ⅟↑db * (↑(num✝¹.mul db) * ⅟↑da) ≤ ⅟↑db * (↑(num✝.mul da) * ⅟↑da)
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝ : decide (num✝¹.mul (Int.ofNat db) ≤ num✝.mul (Int.ofNat da)) = true
h : ↑(num✝¹.mul (Int.ofNat db)) ≤ ↑(num✝.mul (Int.ofNat da))
ha : 0 ≤ ⅟↑da
hb : 0 ≤ ⅟↑db
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db

Tactic:
have h := (mul_le_mul_of_nonneg_left · hb) <| mul_le_mul_of_nonneg_right h ha

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝¹ : decide (num✝¹.mul (Int.ofNat db) ≤ num✝.mul (Int.ofNat da)) = true
h✝ : ↑(num✝¹.mul (Int.ofNat db)) ≤ ↑(num✝.mul (Int.ofNat da))
ha : 0 ≤ ⅟↑da
hb : 0 ≤ ⅟↑db
h : ⅟↑db * (↑(num✝¹.mul (Int.ofNat db)) * ⅟↑da) ≤ ⅟↑db * (↑(num✝.mul (Int.ofNat da)) * ⅟↑da)
⊢ ↑num✝¹ * ⅟↑da ≤ ↑num✝ * ⅟↑db
Module: Mathlib.Tactic.NormNum.Ineq

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h : decide (num✝¹ * ↑db < num✝ * ↑da) = true
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db

Tactic:
have h := Int.cast_strictMono (R := α) <| of_decide_eq_true h

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
num✝¹ num✝ : ℤ
da db : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h✝ : decide (num✝¹ * ↑db < num✝ * ↑da) = true
h : (fun x ↦ ↑x) (num✝¹ * ↑db) < (fun x ↦ ↑x) (num✝ * ↑da)
⊢ ↑num✝¹ * ⅟↑da < ↑num✝ * ⅟↑db
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ (a ⊔ 1) * a⁻ᵐ = |a|ₘ

Tactic:
sup_mul,

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a * a⁻ᵐ ⊔ 1 * a⁻ᵐ = |a|ₘ
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ (a⁻¹ ⊔ 1) * a ⊔ (a⁻¹ ⊔ 1) = |a|ₘ

Tactic:
sup_mul,

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a⁻¹ * a ⊔ 1 * a ⊔ (a⁻¹ ⊔ 1) = |a|ₘ
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: m n : ℕ
h : m ≤ n
⊢ m ! ∣ n !

Tactic:
induction h with

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

Goal state before:
pp: case mp
n : ℕ
h : n ! = 1
⊢ ¬1 < n !

Tactic:
h

Goal state after:
case mp
n : ℕ
h : n ! = 1
⊢ ¬1 < 1
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
h

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

Goal state before:
pp: case inr.inr
m n : ℕ
hn : 1 < m
h : n ! = m !
hnm : m ! < n !
⊢ n = m

Tactic:
h

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

Goal state before:
pp: ⊢ ascFactorial 0 (succ 0) = 0

Tactic:
ascFactorial_succ,

Goal state after:
⊢ (0 + 0) * ascFactorial 0 0 = 0
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: k : ℕ
⊢ ascFactorial 0 (k + 1).succ = 0

Tactic:
ascFactorial_succ,

Goal state after:
k : ℕ
⊢ (0 + (k + 1)) * ascFactorial 0 (k + 1) = 0
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: k : ℕ
⊢ ascFactorial 1 (k + 1) = (k + 1)!

Tactic:
ascFactorial_succ,

Goal state after:
k : ℕ
⊢ (1 + k) * ascFactorial 1 k = (k + 1)!
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ n ! * (n + 1).ascFactorial (k + 1) = (n + (k + 1))!

Tactic:
ascFactorial_succ,

Goal state after:
n k : ℕ
⊢ n ! * ((n + 1 + k) * (n + 1).ascFactorial k) = (n + (k + 1))!
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case zero.succ
k n✝ : ℕ
⊢ ascFactorial 0 (n✝ + 1) * (0 + (n✝ + 1)).ascFactorial k = ascFactorial 0 (n✝ + 1 + k)

Tactic:
simp only [Nat.add_right_comm, zero_ascFactorial, Nat.zero_add, Nat.zero_mul]

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

Goal state before:
pp: n k : ℕ
⊢ n * n ^ k ≤ n.ascFactorial (k + 1)

Tactic:
ascFactorial_succ,

Goal state after:
n k : ℕ
⊢ n * n ^ k ≤ (n + k) * n.ascFactorial k
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ n ^ (k + 1) ≤ n.ascFactorial (k + 1)

Tactic:
rw [Nat.pow_succ, Nat.mul_comm, ascFactorial_succ, ← succ_ascFactorial]

Goal state after:
n k : ℕ
⊢ n * n ^ k ≤ n * n.succ.ascFactorial k
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + 1).ascFactorial (k + 1) ≤ (n + (k + 1)) ^ (k + 1)

Tactic:
ascFactorial_succ,

Goal state after:
n k : ℕ
⊢ (n + 1 + k) * (n + 1).ascFactorial k ≤ (n + (k + 1)) ^ (k + 1)
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case inr
n k j : ℕ
hn : n > 0
⊢ n.ascFactorial (j + 1) ≤ (j + 1)! * n ^ (j + 1)

Tactic:
ascFactorial_succ,

Goal state after:
case inr
n k j : ℕ
hn : n > 0
⊢ (n + j) * n.ascFactorial j ≤ (j + 1)! * n ^ (j + 1)
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
x✝ : 2 ≤ k + 2
⊢ (n + 1).ascFactorial (k + 2) < (n + (k + 2)) * (n + (k + 2)) ^ (k + 1)

Tactic:
ascFactorial_succ,

Goal state after:
n k : ℕ
x✝ : 2 ≤ k + 2
⊢ (n + 1 + (k + 1)) * (n + 1).ascFactorial (k + 1) < (n + (k + 2)) * (n + (k + 2)) ^ (k + 1)
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n : ℕ
⊢ (n + 1).descFactorial (0 + 1) = (n + 1) * n.descFactorial 0

Tactic:
rw [descFactorial_zero, descFactorial_one, Nat.mul_one]

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

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

Tactic:
rw [descFactorial_succ, mul_eq_zero, descFactorial_eq_zero_iff_lt, Nat.lt_succ_iff,
      Nat.sub_eq_zero_iff_le, Nat.lt_iff_le_and_ne, or_iff_left_iff_imp, and_imp]
    exact fun h _ => h

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

Goal state before:
pp: n k : ℕ
⊢ (n + k + 1) * (n + k).descFactorial k = (n + 1).ascFactorial k.succ

Tactic:
ascFactorial_succ,

Goal state after:
n k : ℕ
⊢ (n + k + 1) * (n + k).descFactorial k = (n + 1 + k) * (n + 1).ascFactorial k
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + k.succ - 1 - k) * (n + k.succ - 1).descFactorial k = n.ascFactorial k.succ

Tactic:
ascFactorial_succ,

Goal state after:
n k : ℕ
⊢ (n + k.succ - 1 - k) * (n + k.succ - 1).descFactorial k = (n + k) * n.ascFactorial k
Module: Mathlib.Tactic.NormNum.OfScientific

Goal state before:
pp: α : Type u_1
inst✝ : DivisionSemiring α
x✝¹ x✝ num✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
eq : ↑(NNRat.divNat x✝¹ (10 ^ x✝)) = ↑num✝ * ⅟↑denom✝
⊢ OfScientific.ofScientific x✝¹ true x✝ = ↑num✝ * ⅟↑denom✝

Tactic:
rwa [NNRatCast.ofScientific_eq_ite, if_pos rfl]

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ ⌊fract x⌋ = (⌊2 * fract x⌋ + 1) / 2

Tactic:
rw [Int.floor_eq_zero_iff.mpr, Int.floor_eq_zero_iff.mpr]

Goal state after:
case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ 0 = (0 + 1) / 2

case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ 2 * fract x ∈ Ico 0 1

case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ fract x ∈ Ico 0 1
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case neg.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
H : ⌊2 * fract x⌋ = 1
h : fract x ≤ 0
⊢ 2 * fract x < 1

Tactic:
h

Goal state after:
case neg.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
H : ⌊2 * fract x⌋ = 1
h : fract x ≤ 0
⊢ 2 * 0 < 1
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ x - 1 / 2 < ↑(round x)

Tactic:
round_eq x,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ x - 1 / 2 < ↑⌊x + 1 / 2⌋
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌊↑n / ↑d⌋ = ↑(n / d)

Tactic:
rw [← Int.ofNat_ediv_ofNat, ← floor_natCast_div_natCast n d,
    ← floor_cast (α := α), Rat.cast_div, cast_natCast, cast_natCast]

Goal state after:
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✝² : AddGroup G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H a b
f : F
x : G
n : ℕ
⊢ f (x + Int.negSucc n • a) = f x + Int.negSucc n • b

Tactic:
simp [← sub_eq_add_neg]

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

Goal state before:
pp: K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
⊢ ∃ n, y ^ (n + 1) < x ∧ x ≤ y ^ n

Tactic:
by
  rcases exists_nat_pow_near (one_le_inv_iff₀.2 ⟨xpos, hx⟩) (one_lt_inv_iff₀.2 ⟨ypos, hy⟩) with
    ⟨n, hn, h'n⟩
  refine ⟨n, ?_, ?_⟩
  · rwa [inv_pow, inv_lt_inv₀ xpos (pow_pos ypos _)] at h'n
  · rwa [inv_pow, inv_le_inv₀ (pow_pos ypos _) xpos] at hn

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

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : Ring S
inst✝⁴ : LinearOrder S
inst✝³ : FloorRing R
inst✝² : FloorRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : StrictMono ⇑f
a : R
n : ℤ
⊢ ↑n ≤ f a ↔ ↑n ≤ a

Tactic:
by rw [← map_intCast f, hf.le_iff_le]

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

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : Ring S
inst✝⁴ : LinearOrder S
inst✝³ : FloorRing R
inst✝² : FloorRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : StrictMono ⇑f
a : R
n : ℤ
⊢ f a ≤ ↑n ↔ a ≤ ↑n

Tactic:
by rw [← map_intCast f, hf.le_iff_le]

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

Goal state before:
pp: R : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrder R
⊢ Subsingleton (FloorRing R)

Tactic:
refine ⟨fun H₁ H₂ => ?_⟩
  have : H₁.floor = H₂.floor :=
    funext fun a => (H₁.gc_coe_floor.u_unique H₂.gc_coe_floor) fun _ => rfl
  have : H₁.ceil = H₂.ceil := funext fun a => (H₁.gc_ceil_coe.l_unique H₂.gc_ceil_coe) fun _ => rfl
  cases H₁; cases H₂; congr

Goal state after:
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:
← div_le_iff₀ δ_pos

Goal state after:
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
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case refine_2
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
⊢ 1 ≤ ↑m * δ

Tactic:
← div_le_iff₀ δ_pos

Goal state after:
case refine_2
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
⊢ 1 / δ ≤ ↑m
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: α : Type u_1
s s' : Multiset α
p p' : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred p'
l l' : List α
hp : ∀ (x : α), x ∈ Quot.mk (⇑(isSetoid α)) l → p x = p' x
hs : l ~ l'
⊢ ∀ (x : α), x ∈ l → decide (p x) = decide (p' x)

Tactic:
simpa using hp

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

Goal state before:
pp: α : Type u_1
m : Multiset α
r : α → α → Prop
⊢ (∀ (x : α), x ∈ m → r x x) → Rel r m m

Tactic:
refine m.induction_on ?_ ?_

Goal state after:
case refine_1
α : Type u_1
m : Multiset α
r : α → α → Prop
⊢ (∀ (x : α), x ∈ 0 → r x x) → Rel r 0 0

case refine_2
α : Type u_1
m : Multiset α
r : α → α → Prop
⊢ ∀ (a : α) (s : Multiset α),
    ((∀ (x : α), x ∈ s → r x x) → Rel r s s) → (∀ (x : α), x ∈ a ::ₘ s → r x x) → Rel r (a ::ₘ s) (a ::ₘ s)
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
⊢ (∀ (x : α), x ∈ a ::ₘ m → r x x) → Rel r (a ::ₘ m) (a ::ₘ m)

Tactic:
h

Goal state after:
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)
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
xs : List α
n m : Fin xs.length
h : xs.get n = xs.get m
hne : n ≠ m
⊢ ¬xs.Nodup

Tactic:
rw [nodup_iff_injective_get]

Goal state after:
α : Type u
xs : List α
n m : Fin xs.length
h : xs.get n = xs.get m
hne : n ≠ m
⊢ ¬Injective xs.get
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
s : Multiset α
t : Multiset β
h : Rel r s t
⊢ ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b

Tactic:
induction h with

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

Goal state before:
pp: case refine_2
α : Type u_1
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → m1.card = t.card → Rel r m1 t
m : Multiset α
⊢ (∀ (a_1 b : α), a_1 ∈ m → b ∈ a ::ₘ t → r a_1 b) → m.card = (a ::ₘ t).card → Rel r m (a ::ₘ t)

Tactic:
h

Goal state after:
case refine_2
α : Type u_1
m2 : Multiset α
r : α → α → Prop
a : α
t : Multiset α
ih : ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ t → r a b) → m1.card = t.card → Rel r m1 t
m : Multiset α
h : ∀ (a_1 b : α), a_1 ∈ m → b ∈ a ::ₘ t → r a_1 b
⊢ m.card = (a ::ₘ t).card → Rel r m (a ::ₘ t)
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:
diff_cons,

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

Goal state before:
pp: α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
⊢ b ∈ map f s

Tactic:
h

Goal state after:
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
⊢ b ∈ b ::ₘ t
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: case mpr
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
t : Multiset β
a : α
u : Multiset α
h1 : a ∈ a ::ₘ u
h : map f u = t
this : f a ∈ map f (a ::ₘ u)
⊢ map f u = t

Tactic:
h

Goal state after:
case mpr
α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
t : Multiset β
a : α
u : Multiset α
h1 : a ∈ a ::ₘ u
h : map f u = t
this : f a ∈ map f (a ::ₘ u)
⊢ t = t
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
x y : α
⊢ ∀ {z : α}, x ≠ z → x ≠ y ∨ y ≠ z

Tactic:
z

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
x y z : α
⊢ x ≠ z → x ≠ y ∨ y ≠ z
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
h : ¬a ∈ (l₁ ++ l₂).dedup
⊢ a :: (l₁ ++ l₂).dedup = List.insert a (l₁ ++ l₂).dedup

Tactic:
insert_of_not_mem h

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
l₂ : List α
a : α
l₁ : List α
IH : (l₁ ++ l₂).dedup = l₁ ∪ l₂.dedup
h : ¬a ∈ (l₁ ++ l₂).dedup
⊢ a :: (l₁ ++ l₂).dedup = a :: (l₁ ++ l₂).dedup
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
a : α
inst✝ : DecidableEq α
h : a ∈ l₁ ∩ l₂
⊢ a ∈ l₂

Tactic:
by simpa using of_mem_filter h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
⊢ xs ∩ ys.reverse = xs ∩ ys

Tactic:
simp only [List.inter_def, elem_eq_mem, mem_reverse]

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

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

Tactic:
refine Multiset.induction_on s ?_ fun a t IH => ?_
  · rw [map_zero, countP_zero, filter_zero, card_zero]
  · rw [map_cons, countP_cons, IH, filter_cons, card_add, apply_ite card, card_zero, card_singleton,
      Nat.add_comm]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h : ¬p a
⊢ count a (filter p s) = 0

Tactic:
· exact count_filter_of_neg h

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

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : _root_.Disjoint (Quot.mk (⇑(isSetoid α)) a✝) (Quot.mk (⇑(isSetoid α)) b✝)
⊢ ndunion (Quot.mk (⇑(isSetoid α)) a✝) (Quot.mk (⇑(isSetoid α)) b✝) =
    dedup (Quot.mk (⇑(isSetoid α)) a✝) + Quot.mk (⇑(isSetoid α)) b✝

Tactic:
exact congr_arg ((↑) : List α → Multiset α) <| List.Disjoint.union_eq <| by simpa using h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : s ∈ {s | a ∈ s}
t : Finset α
ht : t ∈ {s | a ∈ s}
h : s.erase a = (fun s ↦ s.erase a) t
⊢ insert a (s.erase a) = insert a (t.erase a)

Tactic:
h

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : s ∈ {s | a ∈ s}
t : Finset α
ht : t ∈ {s | a ∈ s}
h : s.erase a = (fun s ↦ s.erase a) t
⊢ insert a ((fun s ↦ s.erase a) t) = insert a (t.erase a)
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ s \ {a} = ∅ ↔ s = ∅ ∨ s = {a}

Tactic:
sdiff_eq_empty_iff_subset,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ s ⊆ {a} ↔ s = ∅ ∨ s = {a}
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
n : ℕ
a : α
⊢ (replicate n a).toFinset = if n = 0 then ∅ else {a}

Tactic:
ext x
  simp only [mem_toFinset, mem_replicate]
  split_ifs with hn <;> simp [hn]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
⊢ ↑t ⊆ f '' s ↔ ∃ s', ↑s' ⊆ s ∧ image f s' = t

Tactic:
by
  constructor
  · intro h
    let : CanLift β s (f ∘ (↑)) fun y => y ∈ f '' s := ⟨fun y ⟨x, hxt, hy⟩ => ⟨⟨x, hxt⟩, hy⟩⟩
    lift t to Finset s using h
    refine ⟨t.map (Embedding.subtype _), map_subtype_subset _, ?_⟩
    ext y; simp
  · grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∈ s
⊢ #(insert a s) = #s

Tactic:
by rw [insert_eq_of_mem h]

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

Goal state before:
pp: α : Type u_1
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
⊢ filter p s = s ↔ ∀ x ∈ s, p x

Tactic:
filter_eq_self

Goal state after:
α : Type u_1
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
⊢ (∀ x ∈ s, p x) ↔ ∀ x ∈ s, p x
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : Fin n
⊢ 0 < ↑a ↔ 0 < a

Tactic:
by
  rw [← val_fin_lt, val_zero]

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 : ℕ
hi : i < n
j : ℕ
hj : j < ↑(e ⟨i, hi⟩)
this : e.symm ⟨j, ⋯⟩ < ⟨i, hi⟩
h : j = ↑(e.symm ⟨j, ⋯⟩)
⊢ j < i

Tactic:
h

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⟩)
this : e.symm ⟨j, ⋯⟩ < ⟨i, hi⟩
h : j = ↑(e.symm ⟨j, ⋯⟩)
⊢ ↑(e.symm ⟨j, ⋯⟩) < i