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

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a b : α
⊢ |a * b| = |a| * |b|

Tactic:
rw [abs_eq (mul_nonneg (abs_nonneg a) (abs_nonneg b))]

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
a b : α
⊢ a * b = |a| * |b| ∨ a * b = -(|a| * |b|)
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t : Set β
⊢ (fun x ↦ f x.1 x.2) '' (s ∪ s') ×ˢ t = (fun x ↦ f x.1 x.2) '' s ×ˢ t ∪ (fun x ↦ f x.1 x.2) '' s' ×ˢ t

Tactic:
union_prod,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t : Set β
⊢ (fun x ↦ f x.1 x.2) '' (s ×ˢ t ∪ s' ×ˢ t) = (fun x ↦ f x.1 x.2) '' s ×ˢ t ∪ (fun x ↦ f x.1 x.2) '' s' ×ˢ t
Module: Mathlib.Algebra.Order.Ring.Abs

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
n : ℕ
⊢ 1 ^ n = 1

Tactic:
one_pow

Goal state after:
α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedRing α
n : ℕ
⊢ 1 = 1
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
b : β
⊢ image2 f s {b} ∪ image2 f s t = (fun a ↦ f a b) '' s ∪ image2 f s t

Tactic:
image2_singleton_right

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
b : β
⊢ (fun a ↦ f a b) '' s ∪ image2 f s t = (fun a ↦ f a b) '' s ∪ image2 f s t
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hg : Monotone g
⊢ BddAbove (range (g ∘ f))

Tactic:
simpa only [Set.range_comp] using hg.map_bddAbove hf

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
x x' : α
h : x = x'
⊢ x = term 1 x' 0

Tactic:
simp [term, h, one_nsmul]

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
l : List M
m : M
h : ∀ (x : M), x ∈ l → x = m
⊢ l.prod = m ^ l.length

Tactic:
rw [← prod_replicate, ← List.eq_replicate_iff.mpr ⟨rfl, h⟩]

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 c : α
hc : c < 0
⊢ a ≤ b / c ↔ b ≤ a * c

Tactic:
le_div_iff_of_neg hc

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ b ≤ a * c ↔ b ≤ a * c
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ 1 < a / 0 ↔ 0 < 0 ∧ 0 < a ∨ 0 < 0 ∧ a < 0

pp: case inr.inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb : 0 < b
⊢ 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b

Tactic:
· simp [zero_le_one]

Goal state after:
case inr.inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb : 0 < b
⊢ 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case inr.inl
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
⊢ a / 0 ≤ 1 ↔ 0 < 0 ∧ a ≤ 0 ∨ 0 = 0 ∨ 0 < 0 ∧ 0 ≤ a

pp: case inr.inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb : 0 < b
⊢ a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a

Tactic:
· simp [zero_le_one]

Goal state after:
case inr.inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb : 0 < b
⊢ a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a
Module: Mathlib.Data.List.Basic

Goal state before:
pp: ι : Type u_1
α : Type u
β : Type v
γ : Type w
l✝ l₁ l₂ l : List α
i : ℕ
h : i < l.tail.length
⊢ i + 1 < l.length

Tactic:
by simp only [length_tail] at h; lia

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ Injective (map f) ↔ Injective f

Tactic:
by
  refine ⟨fun h x y hxy => ?_, (·.list_map)⟩
  suffices [x] = [y] by simpa using this
  apply h
  simp [hxy]

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

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

Tactic:
divInt_mul_right hx

Goal state after:
case neg
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : ¬d = 0
⊢ n /. d = n /. d
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
⊢ ↑⟨OfScientific.ofScientific m b d, ⋯⟩ = ↑(if b = true then NNRat.divNat m (10 ^ d) else ↑(m * 10 ^ d))

Tactic:
split_ifs

Goal state after:
case pos
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : b = true
⊢ ↑⟨OfScientific.ofScientific m b d, ⋯⟩ = ↑(NNRat.divNat m (10 ^ d))

case neg
K : Type u_1
inst✝ : NNRatCast K
m : ℕ
b : Bool
d : ℕ
h✝ : ¬b = true
⊢ ↑⟨OfScientific.ofScientific m b d, ⋯⟩ = ↑↑(m * 10 ^ d)
Module: Mathlib.Data.Rat.Cast.Defs

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

pp: case hb
α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.den * r.den) ≠ 0

Tactic:
(Nat.cast_commute _ _).div_add_div (Nat.commute_cast _ _) hq hr

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.num * ↑r.den + ↑q.den * r.num) / ↑(q.den * r.den) = (↑q.num * ↑r.den + ↑q.den * ↑r.num) / (↑q.den * ↑r.den)

case hb
α : Type u_3
inst✝ : DivisionRing α
q r : ℚ
hq : ↑q.den ≠ 0
hr : ↑r.den ≠ 0
⊢ ↑(q.den * r.den) ≠ 0
Module: Mathlib.Data.Rat.Lemmas

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

Tactic:
← den_neg_eq_den r,

Goal state after:
q r : ℚ
⊢ (q + -r).num * ↑q.den * ↑(-r).den = (q.num * ↑(-r).den + (-r).num * ↑q.den) * ↑(q + -r).den
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: a : ℕ
inst✝ : a.AtLeastTwo
⊢ (OfNat.ofNat a)⁻¹.den = OfNat.ofNat a

Tactic:
by
  simp [den_inv, Int.natAbs_eq_iff]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : Semifield α
inst✝⁴ : LinearOrder α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ (a - b) / c = a / c - b / c

Tactic:
simp_rw [div_eq_mul_inv, tsub_mul]

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
⊢ ⨅ i, ⨅ (_ : i > 0), f i = ⨅ b ∈ range fun i ↦ i + 1, f b

Tactic:
Nat.range_succ

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
f : ℕ → α
⊢ ⨅ i, ⨅ (_ : i > 0), f i = ⨅ b ∈ {i | 0 < i}, f b
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ (⨆ x, f x) ⊔ a = ⨆ x, f x ⊔ a

Tactic:
by
  rw [iSup_sup_eq, iSup_const]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝¹ : CompleteLattice α
inst✝ : Nonempty ι
f : ι → α
a : α
⊢ a ⊔ ⨆ x, f x = ⨆ x, a ⊔ f x

Tactic:
by
  rw [iSup_sup_eq, iSup_const]

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

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

Tactic:
iSup_sup_eq

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
s : Set α
b : α
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
⊢ sSup s ⊓ b = ⨆ a ∈ s, a ⊓ b

Tactic:
by
  simpa only [inf_comm] using inf_sSup_eq s b minAx

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

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

Tactic:
refine le_antisymm iSup_iInf_le ?_

Goal state after:
α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLattice α
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
⊢ ⨅ g, ⨆ i, f i (g i) ≤ ⨆ i, ⨅ j, f i j
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
r : α → α → Prop
S : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) S
h : ∀ x ∈ S, DirectedOn r x
⊢ DirectedOn r (⋃₀ S)

Tactic:
rw [sUnion_eq_iUnion]
  exact directedOn_iUnion (directedOn_iff_directed.mp hd) (fun i ↦ h i.1 i.2)

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

Goal state before:
pp: α : Type u
β : Type v
s : Set α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ StrictMonoOn f s ↔ StrictMono fun a ↦ f ↑a

Tactic:
by
  simp [StrictMono, StrictMonoOn]

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : s.Nonempty
h's : BddBelow s
⊢ ↑(sInf s) = ⨅ a ∈ s, ↑a

Tactic:
rw [coe_sInf' hs h's, sInf_image]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : β → α
t : Set β
s : Set α
hs : s.OrdConnected
hf : MonotoneOn f t
⊢ ∃ u, u.OrdConnected ∧ t ∩ f ⁻¹' s = t ∩ u

Tactic:
let u := {x | (∃ y ∈ t, y ≤ x ∧ f y ∈ s) ∧ (∃ z ∈ t, x ≤ z ∧ f z ∈ s)}

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : β → α
t : Set β
s : Set α
hs : s.OrdConnected
hf : MonotoneOn f t
u : Set β := {x | (∃ y ∈ t, y ≤ x ∧ f y ∈ s) ∧ ∃ z ∈ t, x ≤ z ∧ f z ∈ s}
⊢ ∃ u, u.OrdConnected ∧ t ∩ f ⁻¹' s = t ∩ u
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
a : S
ha : 0 ≤ a
b c : S
hbc : b ≤ c
⊢ a * b ≤ a * c

Tactic:
by
    rw [← le, mul, mul]; refine mul_le_mul_of_nonneg_left (le.2 hbc) ?_; rwa [← zero, le]

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

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℚ
n : ℕ
⊢ ↑m < ↑n ↔ m < ↑n

Tactic:
rw [← cast_lt (K := K), cast_natCast]

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

Goal state before:
pp: K : Type u_5
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℕ
n : ℚ
⊢ ↑m < ↑n ↔ ↑m < n

Tactic:
rw [← cast_lt (K := K), cast_natCast]

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

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℚ≥0
n : ℕ
⊢ ↑m < ↑n ↔ m < ↑n

Tactic:
rw [← cast_lt (K := K), cast_natCast]

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

Goal state before:
pp: K : Type u_5
inst✝² : Semifield K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
m : ℕ
n : ℚ≥0
⊢ ↑m < ↑n ↔ ↑m < n

Tactic:
rw [← cast_lt (K := K), cast_natCast]

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ a / |a|ₘ = (a⁻ᵐ ^ 2)⁻¹

Tactic:
← mabs_div_eq_leOnePart_sq,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ a / |a|ₘ = (|a|ₘ / a)⁻¹
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 1 - fract x ≤ fract x
⊢ |x - ↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉)| = if fract x < 1 - fract x then fract x else 1 - fract x

Tactic:
have : 0 < fract x := by
      replace hx : 0 < fract x + fract x := lt_of_lt_of_le zero_lt_one (tsub_le_iff_left.mp hx)
      simpa only [← two_mul, mul_pos_iff_of_pos_left, zero_lt_two] using hx

Goal state after:
case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 1 - fract x ≤ fract x
this : 0 < fract x
⊢ |x - ↑(if fract x < 1 - fract x then ⌊x⌋ else ⌈x⌉)| = if fract x < 1 - fract x then fract x else 1 - fract x
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: n : ℕ+
a : ℕ
h : a ∣ ↑n
hzero : a = 0
⊢ False

Tactic:
rw [hzero] at h

Goal state after:
n : ℕ+
a : ℕ
h : 0 ∣ ↑n
hzero : a = 0
⊢ False
Module: Mathlib.Algebra.Order.Ring.Pow

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : R
H : -1 ≤ a
n : ℕ
⊢ 1 + ↑n * (a - 1) ≤ a ^ n

Tactic:
by
  have : -2 ≤ a - 1 := by
    rwa [← one_add_one_eq_two, neg_add, ← sub_eq_add_neg, sub_le_sub_iff_right]
  simpa only [add_sub_cancel] using one_add_mul_le_pow this n

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

Goal state before:

Tactic:
(q - fract q + 1) * q.den = (q + (1 - fract q)) * q.den := by ring
        _ = q * q.den + (1 - fract q) * q.den := by rw [add_mul]
        _ = q.num + (1 - fract q) * q.den := by simp

Goal state after:
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
g : G
p₁ p₂ : P
⊢ g • p₁ /ₛ p₂ = g * (p₁ /ₛ p₂)

Tactic:
apply smul_right_cancel p₂
  rw [sdiv_smul, mul_smul, sdiv_smul]

Goal state after:
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ : P
g : G
⊢ g⁻¹ = (p₂ /ₛ p₁) * ((p₁ /ₛ p₂) / g)

Tactic:
←
    mul_div_assoc,

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ : P
g : G
⊢ g⁻¹ = (p₂ /ₛ p₁) * (p₁ /ₛ p₂) / g
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
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
⊢ ∃ n, a < c ^ n ∧ c ^ n < b

Tactic:
by
  rcases le_or_gt a 0 with ha | ha
  · obtain ⟨n, hn⟩ := exists_pow_lt_of_lt_one hb₀ hc₁
    exact ⟨n, ha.trans_lt (zpow_pos hc₀ _), mod_cast hn⟩
  · rcases le_or_gt b 1 with hb₁ | hb₁
    · obtain ⟨n, hn⟩ := exists_pow_btwn_of_lt_mul h hb₀ hb₁ hc₀ hc₁
      exact ⟨n, mod_cast hn⟩
    · rcases lt_or_ge a 1 with ha₁ | ha₁
      · refine ⟨0, ?_⟩
        rw [zpow_zero]
        exact ⟨ha₁, hb₁⟩
      · have : b⁻¹ < a⁻¹ * c := by rwa [lt_inv_mul_iff₀' ha, inv_mul_lt_iff₀ hb₀]
        obtain ⟨n, hn₁, hn₂⟩ :=
          exists_pow_btwn_of_lt_mul this (inv_pos_of_pos ha) (inv_le_one_of_one_le₀ ha₁) hc₀ hc₁
        refine ⟨-n, ?_, ?_⟩
        · rwa [lt_inv_comm₀ (pow_pos hc₀ n) ha, ← zpow_natCast, ← zpow_neg] at hn₂
        · rwa [inv_lt_comm₀ hb₀ (pow_pos hc₀ n), ← zpow_natCast, ← zpow_neg] at hn₁

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

Goal state before:
pp: case mp
α : Type u_1
l : List α
a : α
s : List α
hla : s ~ [a]
h : l <+ [a]
⊢ l = [] ∨ l = [a]

Tactic:
sublist_singleton

Goal state after:
case mp
α : Type u_1
l : List α
a : α
s : List α
hla : s ~ [a]
h : l = [] ∨ l = [a]
⊢ l = [] ∨ l = [a]
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
v : G
s t : Set P
⊢ v • s /ₛ v • t = s /ₛ t

Tactic:
ext; simp [mem_sdiv, mem_smul_set]

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

Goal state before:
pp: case mpr
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
⊢ (a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs) → a ::ₘ as = b ::ₘ bs

Tactic:
intro h
    rcases h with (⟨eq₁, eq₂⟩ | ⟨_, cs, eq₁, eq₂⟩)
    · simp [*]
    · simp [*, cons_swap a b]

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

Goal state before:
pp: α : Type u_1
l₂ : List α
a : α
inst✝ : DecidableEq α
l₁ : List α
⊢ (a :: l₁) ∩ l₂ = if a ∈ l₂ then a :: l₁ ∩ l₂ else l₁ ∩ l₂

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
l₂ : List α
a : α
inst✝ : DecidableEq α
l₁ : List α
h✝ : a ∈ l₂
⊢ (a :: l₁) ∩ l₂ = a :: l₁ ∩ l₂

case neg
α : Type u_1
l₂ : List α
a : α
inst✝ : DecidableEq α
l₁ : List α
h✝ : ¬a ∈ l₂
⊢ (a :: l₁) ∩ l₂ = l₁ ∩ l₂
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
a : α
inst✝ : DecidableEq α
⊢ (a :: l₁).bagInter l₂ = if a ∈ l₂ then a :: l₁.bagInter (l₂.erase a) else l₁.bagInter l₂

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
l₁ l₂ : List α
a : α
inst✝ : DecidableEq α
h✝ : a ∈ l₂
⊢ (a :: l₁).bagInter l₂ = a :: l₁.bagInter (l₂.erase a)

case neg
α : Type u_1
l₁ l₂ : List α
a : α
inst✝ : DecidableEq α
h✝ : ¬a ∈ l₂
⊢ (a :: l₁).bagInter l₂ = l₁.bagInter l₂
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : ¬n ≤ xs.length
⊢ List.drop n xs ~ ys ∩ List.drop n xs

Tactic:
· grind [drop_eq_nil_of_le]

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

Goal state before:
pp: case cons.e_a
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ map (fun x ↦ f x) (if p a then {a} else 0) = (if p a then some {f a} else none).getD 0

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h✝ : p a
⊢ map (fun x ↦ f x) {a} = (some {f a}).getD 0

case neg
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
h✝ : ¬p a
⊢ map (fun x ↦ f x) 0 = none.getD 0
Module: Mathlib.Data.Finset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b : List α
⊢ a.toFinset = b.toFinset ↔ ∀ (x : α), x ∈ a ↔ x ∈ b

Tactic:
by
  simp only [Finset.ext_iff, mem_toFinset]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ (↑l₁).ndinter ↑l₂ = ↑(l₁ ∩ l₂)

Tactic:
simp only [ndinter, mem_coe, filter_coe, coe_eq_coe, ← elem_eq_mem]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ List.filter (fun b ↦ elem b l₂) l₁ ~ l₁ ∩ l₂
Module: Mathlib.Data.Multiset.Range

Goal state before:
pp: a : ℕ
m : Multiset ℕ
x : ℕ
⊢ x ∈ range a → ¬x ∈ map (fun x ↦ a + x) m

Tactic:
hxa

Goal state after:
a : ℕ
m : Multiset ℕ
x : ℕ
hxa : x ∈ range a
⊢ ¬x ∈ map (fun x ↦ a + x) m
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ (insert a s).val = a ::ₘ s.val

Tactic:
by
  rw [insert_val, ndinsert_of_notMem h]

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

Goal state before:
pp: α : Type u_1
p : Prop
inst✝ : Decidable p
s : Finset α
⊢ filter (fun _a ↦ p) s = if p then s else ∅

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
p : Prop
inst✝ : Decidable p
s : Finset α
h✝ : p
⊢ filter (fun _a ↦ p) s = s

case neg
α : Type u_1
p : Prop
inst✝ : Decidable p
s : Finset α
h✝ : ¬p
⊢ filter (fun _a ↦ p) s = ∅
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
⊢ insert a s₁ ∩ s₂ = if a ∈ s₂ then insert a (s₁ ∩ s₂) else s₁ ∩ s₂

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h✝ : a ∈ s₂
⊢ insert a s₁ ∩ s₂ = insert a (s₁ ∩ s₂)

case neg
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h✝ : a ∉ s₂
⊢ insert a s₁ ∩ s₂ = s₁ ∩ s₂
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
⊢ s₁ ∩ insert a s₂ = if a ∈ s₁ then insert a (s₁ ∩ s₂) else s₁ ∩ s₂

Tactic:
split_ifs

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h✝ : a ∈ s₁
⊢ s₁ ∩ insert a s₂ = insert a (s₁ ∩ s₂)

case neg
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h✝ : a ∉ s₁
⊢ s₁ ∩ insert a s₂ = s₁ ∩ s₂
Module: Mathlib.Data.Finset.Basic

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

Tactic:
rw [← sdiff_singleton_eq_erase, sdiff_eq_empty_iff_subset, subset_singleton_iff]

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

Goal state before:
pp: α : Type u_1
s t u : Finset α
h : Disjoint s t
⊢ Disjoint (s.disjUnion t h) u ↔ Disjoint s u ∧ Disjoint t u

Tactic:
simp only [disjoint_left, mem_disjUnion, or_imp, forall_and]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ {a}ᶜ = univ.erase a

Tactic:
compl_eq_univ_sdiff,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ univ \ {a} = univ.erase a
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
⊢ s ⊆ map f.symm.toEmbedding t ↔ map f.toEmbedding s ⊆ t

Tactic:
by
  constructor <;> intro h x hx
  · simp only [mem_map_equiv] at hx
    simpa using h hx
  · simp only [mem_map_equiv]
    exact h (by simp [hx])

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

Goal state before:
pp: case zero
n : ℕ
⊢ 0 ∈ range (n + 1) ↔ 0 ∈ insert 0 (map { toFun := fun i ↦ i + 1, inj' := ⋯ } (range n))

Tactic:
simp [Nat.zero_lt_succ n]

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

Goal state before:
pp: case succ
n✝ n : ℕ
⊢ n + 1 ∈ range (n✝ + 1) ↔ n + 1 ∈ insert 0 (map { toFun := fun i ↦ i + 1, inj' := ⋯ } (range n✝))

Tactic:
simp [Nat.zero_lt_succ n]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset { a // p a }
a : { a // p a }
⊢ a ∈
      (fun s ↦ Finset.map (Subtype.impEmbedding (Membership.mem ↑s) p ⋯) (↑s).attach)
        ((fun s ↦ ⟨Finset.map { toFun := fun a ↦ ↑a, inj' := ⋯ } s, ⋯⟩) s) ↔
    a ∈ s

Tactic:
constructor <;> intro h <;>
    simp only [Finset.mem_map, Finset.mem_attach, true_and, Subtype.exists, Embedding.coeFn_mk,
      exists_and_right, exists_eq_right, Subtype.impEmbedding] at * <;>
    grind

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

Goal state before:
pp: case succ
n : ℕ
k : Fin (n + 1).succ
this : NeZero (n + 1).succ
hk : k ≠ 0
⊢ ↑1 ≤ ↑k

Tactic:
Fin.val_one,

Goal state after:
case succ
n : ℕ
k : Fin (n + 1).succ
this : NeZero (n + 1).succ
hk : k ≠ 0
⊢ 1 ≤ ↑k
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case succ
n✝ : ℕ
⊢ (n✝ + 1 + 1 - ↑1) % (n✝ + 1 + 1) = n✝ + 1

Tactic:
Fin.val_one,

Goal state after:
case succ
n✝ : ℕ
⊢ (n✝ + 1 + 1 - 1) % (n✝ + 1 + 1) = n✝ + 1
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : #s ≤ #t
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
f' : ↥s → β := fun a ↦ f ↑a ⋯
⊢ a₁ = a₂

Tactic:
have hsurj' : Set.SurjOn f' s.attach t := fun x hx ↦ by simpa [f'] using hsurj x hx

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : #s ≤ #t
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
f' : ↥s → β := fun a ↦ f ↑a ⋯
hsurj' : Set.SurjOn f' ↑s.attach ↑t
⊢ a₁ = a₂
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case neg
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
hi : ¬i = 0
⊢ predAbove 0 i = i.pred hi

Tactic:
predAbove_zero_of_ne_zero hi

Goal state after:
case neg
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
hi : ¬i = 0
⊢ i.pred hi = i.pred hi
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_1
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin 1
⊢ append x₀ x (castAdd n 0) = (cons (x₀ 0) x ∘ Fin.cast ⋯) (castAdd n 0)

Tactic:
Fin.append_left,

Goal state after:
case refine_1
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin 1
⊢ x₀ 0 = (cons (x₀ 0) x ∘ Fin.cast ⋯) (castAdd n 0)