mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

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

Tactic:
have h : ((·⁻¹) ∘ fun k ↦ f (k + 1) / f k) = fun k ↦ f k / f (k + 1) := by ext; apply inv_div
  rw [← inv_inj, prod_inv, map_map, inv_div, h, prod_range_div']

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

Goal state before:
pp: α : Type u
β : Type v
f : α → Option β
g : α → β
l : List α
⊢ filterMap f l = map g l → ∀ (x : α), x ∈ l → f x = some (g x)

Tactic:
by
    induction l with | nil => simp | cons a l ih => ?_
    rcases ha : f a with - | b
    · intro h
      have : (filterMap f l).length = l.length + 1 := by grind
      grind
    · simp +contextual [ha, ih]

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

Goal state before:
pp: α : Type u
l : List α
p : α → Bool
⊢ map (fun a ↦ ↑a) (filter (fun x ↦ p ↑x) l.attach) = map (fun a ↦ ↑a) (map (Subtype.map id ⋯) (filter p l).attach)

Tactic:
simp_rw [map_map, comp_def, Subtype.map, id, ← Function.comp_apply (g := Subtype.val),
      ← filter_map, attach_map_subtype_val]

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

Goal state before:
pp: x✝¹ : ℕ
x✝ : ℚ
⊢ x✝ ^ ↑x✝¹.succ = x✝ ^ ↑x✝¹ * x✝

Tactic:
Rat.zpow_natCast,

Goal state after:
x✝¹ : ℕ
x✝ : ℚ
⊢ x✝ ^ x✝¹.succ = x✝ ^ ↑x✝¹ * x✝
Module: Mathlib.Algebra.Ring.Rat

Goal state before:
pp: x✝¹ : ℕ
x✝ : ℚ
⊢ x✝ ^ x✝¹.succ = x✝ ^ ↑x✝¹ * x✝

Tactic:
Rat.zpow_natCast,

Goal state after:
x✝¹ : ℕ
x✝ : ℚ
⊢ x✝ ^ x✝¹.succ = x✝ ^ x✝¹ * x✝
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: m : ℕ
s : Bool
e : ℕ
⊢ 0 ≤ Rat.ofScientific m s e

Tactic:
rw [Rat.ofScientific]

Goal state after:
m : ℕ
s : Bool
e : ℕ
⊢ 0 ≤ if s = true then normalize (↑m) (10 ^ e) ⋯ else ↑(m * 10 ^ e)
Module: Mathlib.Algebra.Group.Semiconj.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a x y : G
⊢ SemiconjBy a⁻¹ y⁻¹ x⁻¹ ↔ SemiconjBy a x y

Tactic:
inv_inv_symm_iff

Goal state after:
G : Type u_1
inst✝ : Group G
a x y : G
⊢ SemiconjBy a x y ↔ SemiconjBy a x y
Module: Mathlib.Algebra.Group.Commute.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Semigroup G
a b c : G
h : SemiconjBy a b c
j : G
⊢ (fun x ↦ x * a) ((fun x ↦ x * c) j) = (fun x ↦ x * b) ((fun x ↦ x * a) j)

Tactic:
by simp only [mul_assoc, ← h.eq]

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
b a : R
e : ℕ
hone : Nat.rawCast 1 = e
hb : a ^ e * Nat.rawCast 1 = b
⊢ a = b + 0

Tactic:
simp [← hone, ← hb]

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:
by simp_rw [div_eq_mul_inv, tsub_mul]

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
i₁ : LinearOrder α
i₂ : OrderBot α
h : WellFoundedLT α
this : InfSet α := { sInf := fun s ↦ if hs : s.Nonempty then ⋯.min s hs else ⊥ }
s : Set α
x✝ : BddBelow s
hn : s.Nonempty
⊢ IsGLB s (⋯.min s hn)

Tactic:
exact IsLeast.isGLB ⟨h.wf.min_mem s hn, fun _ hx ↦ h.wf.min_le hx⟩

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

Goal state before:
pp: α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set α
⊢ s ∪ ⋂ i, ⋂ j, t i j = ⋂ i, ⋂ j, s ∪ t i j

Tactic:
simp_rw [union_iInter]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
hκ : Nonempty κ
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
⊢ ⨆ i ∈ ⋂ j, s j, f i = ⨅ j, ⨆ i ∈ s j, f i

Tactic:
rcases hκ with ⟨j⟩

Goal state after:
α : Type u
inst✝ : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
⊢ ⨆ i ∈ ⋂ j, s j, f i = ⨅ j, ⨆ i ∈ s j, f i
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
s t : Set α
a✝ b✝ c✝ d a b c : α
⊢ sSup (min a '' {b, c}) ≤ sSup {a ⊓ b, a ⊓ c}

Tactic:
image_pair

Goal state after:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
s t : Set α
a✝ b✝ c✝ d a b c : α
⊢ sSup {a ⊓ b, a ⊓ c} ≤ sSup {a ⊓ b, a ⊓ c}
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s t : Set α
h₁ : BddAbove t
h₂ : s ⊆ t
⊢ sSup s ≤ sSup t

Tactic:
rcases eq_empty_or_nonempty s with rfl | h

Goal state after:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
t : Set α
h₁ : BddAbove t
h₂ : ∅ ⊆ t
⊢ sSup ∅ ≤ sSup t

case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s t : Set α
h₁ : BddAbove t
h₂ : s ⊆ t
h : s.Nonempty
⊢ sSup s ≤ sSup t
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case h
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
b : β
hb : Option.some b ∈ lowerBounds s
c : β
hc : c ∈ (fun a ↦ ↑a) ⁻¹' s
⊢ b ≤ c

Tactic:
exact coe_le_coe.1 (hb hc)

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ [[a, b]] = Icc (min a b) (max b a)

pp: case h₁
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ b ≤ b

pp: case h₂
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ a ≤ a

Tactic:
max_comm

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ [[a, b]] = Icc (min a b) (max a b)

case h₁
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ b ≤ b

case h₂
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ a ≤ a
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ a ∈ Ι b c → b ∈ Ι a c → a = b

Tactic:
by
  simp_rw [mem_uIoc]; rintro (⟨_, _⟩ | ⟨_, _⟩) (⟨_, _⟩ | ⟨_, _⟩) <;> apply le_antisymm <;>
    first | assumption | exact le_of_lt ‹_› | exact le_trans ‹_› (le_of_lt ‹_›)

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
⊢ IsChain (fun x1 x2 ↦ r ↑x1 ↑x2) univ ↔ IsChain r s

Tactic:
simpa using isChain_preimage_subtypeVal s univ

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : One M
f : ι × κ → M
i : ι
j : κ
hj : j ∈ mulSupport fun j ↦ f (i, j)
⊢ (i, j) ∈ mulSupport f ∧ (i, j).2 = j

Tactic:
by simpa using hj

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

Goal state before:
pp: case mpr
n : ℕ
⊢ n ≤ 1 → n ! = 1

Tactic:
rintro (_ | _ | _) <;> rfl

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

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ (if 2 * fract (x + ↑y) < 1 then ⌊x + ↑y⌋ else ⌈x + ↑y⌉) = (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y

Tactic:
Int.fract_add_intCast,

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ (if 2 * fract x < 1 then ⌊x + ↑y⌋ else ⌈x + ↑y⌉) = (if 2 * fract x < 1 then ⌊x⌋ else ⌈x⌉) + y
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: a b : ℕ+
h : a < b
⊢ ↑a + (↑b - ↑a) = ↑b

Tactic:
exact add_tsub_cancel_of_le h.le

Goal state after:
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
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

Tactic:
if_neg (not_lt.mpr 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 - ↑⌈x⌉| = if fract x < 1 - fract x then fract x else 1 - fract x
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
this : 0 < fract x
⊢ |x - ↑⌈x⌉| = if fract x < 1 - fract x then fract x else 1 - fract x

Tactic:
if_neg (not_lt.mpr 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 - ↑⌈x⌉| = 1 - fract x
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr.refine_3
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m / ↑n = ↑(m % n) / ↑n + ↑(↑m / ↑n)

Tactic:
← mul_right_inj' hn'.ne',

Goal state after:
case inr.refine_3
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑n * (↑m / ↑n) = ↑n * (↑(m % n) / ↑n + ↑(↑m / ↑n))
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⌉

Tactic:
gcongr <;> apply le_ceil

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
hx : 0 < x
hy : 1 < y
N : ℕ
hN : x⁻¹ < y ^ N
⊢ ∃ m, y ^ m ≤ x

Tactic:
use -N

Goal state after:
case h
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
N : ℕ
hN : x⁻¹ < y ^ N
⊢ y ^ (-↑N) ≤ x
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
this : (q_inv - ↑⌊q_inv⌋).num < q.num
⊢ (fract q⁻¹).num < q.num

Tactic:
by rwa [q_inv_eq]

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

Goal state before:
pp: 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
⊢ ∃ m, y ≤ (↑m * δ) ^ n

Tactic:
refine ⟨m, le_trans ?_ (le_self_pow₀ ?_ hn)⟩

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 * δ

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.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
n m : ℕ
m0 : 0 < m
⊢ n ≤ n • m

Tactic:
by
    rw [← mul_one n, nsmul_eq_mul, Nat.cast_id, mul_one]
    exact Nat.le_mul_of_pos_right n m0

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

Goal state before:
pp: α : Type u_1
s : Multiset α
a : α
⊢ s < {a} ↔ s = 0

Tactic:
by
  simp only [lt_iff_le_and_ne, le_singleton, or_and_right, Ne, and_not_self, or_false,
    and_iff_left_iff_imp]
  rintro rfl
  exact (singleton_ne_zero _).symm

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

Goal state before:
pp: α : Type u_1
m : Multiset α
x : α
n : ℕ
⊢ m < replicate (n + 1) x ↔ m ≤ replicate n x

Tactic:
rw [lt_iff_cons_le]

Goal state after:
α : Type u_1
m : Multiset α
x : α
n : ℕ
⊢ (∃ a, a ::ₘ m ≤ replicate (n + 1) x) ↔ m ≤ replicate n x
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:
by
  rcases eq_or_ne a b with rfl | hab
  · simp [cons_erase h]
  · exact s.erase_cons_tail hab.symm

Goal state after:
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
⊢ ¬Injective xs.get

Tactic:
exact fun hinj => hne (hinj h)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : t ≤ s
⊢ (s - t).card + t.card = s.card

Tactic:
by rw [← card_add, Multiset.sub_add_cancel h]

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl₁ : l₁.Nodup
⊢ a ∈ l₁.diff l₂ ↔ a ∈ l₁ ∧ ¬a ∈ l₂

Tactic:
rw [hl₁.sdiff_eq_filter, mem_filter, decide_eq_true_iff]

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : l.dedup = [] ↔ l = []
⊢ (a :: l).dedup = [] ↔ a :: l = []

Tactic:
by_cases h : a ∈ l
    · simp only [List.dedup_cons_of_mem h, hl, List.ne_nil_of_mem h, reduceCtorEq]
    · simp only [List.dedup_cons_of_notMem h, List.cons_ne_nil]

Goal state after:
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:
· rw [dedup_cons_of_notMem' h, insert_of_not_mem h]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
this : n ≤ n + m
h₂ : xs.Nodup
⊢ List.take n xs ++ List.drop (n + m) xs ~ ys ∩ List.take n xs ++ ys ∩ List.drop (n + m) xs

Tactic:
exact Perm.append (Perm.take_inter _ h h') (Perm.drop_inter _ h h')

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

Goal state before:
pp: α : Type u_1
motive : List α → Sort u_2
nil : motive []
singleton : (a : α) → motive [a]
cons_append : (a : α) → (l : List α) → (b : α) → motive l → motive (a :: (l ++ [b]))
a : α
⊢ bidirectionalRec nil singleton cons_append [a] = singleton a

Tactic:
by
  grind [bidirectionalRec]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Fintype α
f : α → β
⊢ Set.InjOn f ↑univ ↔ Injective f

Tactic:
coe_univ,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Fintype α
f : α → β
⊢ Set.InjOn f Set.univ ↔ Injective f
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : Disjoint p q
⊢ Disjoint (filter p s) (filter q t)

Tactic:
by
  simp_rw [disjoint_left, mem_filter]
  rintro a ⟨_, hp⟩ ⟨_, hq⟩
  rw [Pi.disjoint_iff] at h
  simpa [hp, hq] using h a

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ (↑univ).Nonempty ↔ Nonempty α

Tactic:
coe_univ,

Goal state after:
α : Type u_1
inst✝ : Fintype α
⊢ Set.univ.Nonempty ↔ Nonempty α
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_4
H : ∀ (s : Finset α), s = ∅
a : α
⊢ False

Tactic:
specialize H {a}

Goal state after:
α : Type u_4
a : α
H : {a} = ∅
⊢ False
Module: Mathlib.Data.Fin.Embedding

Goal state before:
pp: n m : ℕ
hmn : n ≤ m
y : Fin m
⊢ y ∈ Set.range ⇑((addNatEmb (m - n)).trans (finCongr ⋯).toEmbedding) ↔ y ∈ {i | m ≤ ↑i + n}

Tactic:
exact ⟨fun ⟨x, hx⟩ ↦ by simp [← hx]; lia,
    fun xin ↦ ⟨subNat (m - n) (y.cast (Nat.add_sub_of_le hmn).symm)
    (Nat.sub_le_of_le_add xin), by simp⟩⟩

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p < p.succAbove i ↔ p < i.succ

Tactic:
rw [lt_succAbove_iff_le_castSucc, le_castSucc_iff]

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

Goal state before:
pp: case refine_2
α : Type u
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : (ofFn xs).Nodup → Function.Injective xs
⊢ (ofFn (Fin.cons x₀ xs)).Nodup → Function.Injective (Fin.cons x₀ xs)

Tactic:
· intro h
    rw [Fin.cons_injective_iff]
    simp_rw [ofFn_succ, Fin.cons_succ, nodup_cons, Fin.cons_zero, mem_ofFn] at h
    exact h.imp_right ih

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

Goal state before:
pp: case mpr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
hst : s ⊆ t
h : #s + 1 = #t
⊢ ∃ a ∉ s, insert a s = t

Tactic:
obtain ⟨a, ha⟩ : ∃ a, t \ s = {a} := card_eq_one.mp (by grind)

Goal state after:
case mpr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
hst : s ⊆ t
h : #s + 1 = #t
a : α
ha : t \ s = {a}
⊢ ∃ a ∉ s, insert a s = t
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_4
inst✝ : Finite α
val✝ : Fintype α
l : List α
e : ⟦l⟧ = univ.val
this : univ.val.Nodup ∧ ∀ (x : α), x ∈ univ.val
⊢ List.Nodup ?m.54 ∧ ∀ (x : α), x ∈ ?m.54

Tactic:
rwa [← e] at this

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → β
h : Injective f
b : β
w : b ∉ Set.range f
⊢ b ∉ ⇑{ toFun := f, inj' := h } '' ↑univ

Tactic:
coe_univ,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → β
h : Injective f
b : β
w : b ∉ Set.range f
⊢ b ∉ ⇑{ toFun := f, inj' := h } '' Set.univ
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Irrefl r
val✝ : Fintype α
x y : α
hxy : r x y
⊢ {z | r z x} ⊂ {z | r z y}

Tactic:
simp_rw [lt_iff_le_not_ge, Finset.subset_iff, mem_filter_univ]
      exact
        ⟨fun z hzx => _root_.trans hzx hxy,
          not_forall_of_exists_not ⟨x, Classical.not_imp.2 ⟨hxy, irrefl x⟩⟩⟩

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

Goal state before:
pp: case refine_1
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
⊢ snoc f a (natAdd m (last n)) = a

Tactic:
natAdd_last,

Goal state after:
case refine_1
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
⊢ snoc f a (last (m + n)) = a
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mp.cons_cons
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∃ f, ∀ (ix : ℕ), (a✝¹ :: l₁✝)[ix]? = (a✝¹ :: l₂✝)[f ix]?

Tactic:
refine
        ⟨OrderEmbedding.ofMapLEIff (fun ix : ℕ => if ix = 0 then 0 else (f ix.pred).succ) ?_, ?_⟩

Goal state after:
case mp.cons_cons.refine_1
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∀ (a b : ℕ), ((if a = 0 then 0 else (f a.pred).succ) ≤ if b = 0 then 0 else (f b.pred).succ) ↔ a ≤ b

case mp.cons_cons.refine_2
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∀ (ix : ℕ),
    (a✝¹ :: l₁✝)[ix]? =
      (a✝¹ ::
          l₂✝)[(OrderEmbedding.ofMapLEIff (fun ix ↦ if ix = 0 then 0 else (f ix.pred).succ) ?mp.cons_cons.refine_1) ix]?
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Infinite α
⊢ Infinite (Equiv.Perm α)

Tactic:
obtain ⟨a : α⟩ := Nontrivial.to_nonempty (α := α)
  exact Infinite.of_injective _ (Equiv.swap_injective_of_left a)

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝¹ : Finite ↑s
inst✝ : Finite ↑t
⊢ Finite ↑(s ∪ t)

Tactic:
by
  cases nonempty_fintype s
  cases nonempty_fintype t
  classical
  infer_instance

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

Goal state before:
pp: α : Type u
s t : Set α
hs : Finite ↑s
ht : Finite ↑t
⊢ (s ∪ t).Finite

Tactic:
apply toFinite

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

Goal state before:
pp: α : Type u
β : Type v
s : Set α
f : α → β
hs : s.Finite
this : Finite ↑s
⊢ (f '' s).Finite

Tactic:
apply toFinite

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
a b c : α
h₁ : decide (r a b) = true
h₂ : decide (r b c) = true
⊢ r a ?m.42

Tactic:
by simpa using h₁

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : Std.Irrefl r
a : α
l₁ l₂ : List α
h : Lex r (a :: l₁) (a :: l₂)
⊢ Lex r l₁ l₂

Tactic:
obtain - | h | h := h

Goal state after:
case rel
α : Type u
r : α → α → Prop
inst✝ : Std.Irrefl r
a : α
l₁ l₂ : List α
h : r a a
⊢ Lex r l₁ l₂

case cons
α : Type u
r : α → α → Prop
inst✝ : Std.Irrefl r
a : α
l₁ l₂ : List α
h : Lex r l₁ l₂
⊢ Lex r l₁ l₂
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → α → Prop
f : β → α
l : List β
⊢ IsChain R (map f l) ↔ IsChain (fun a b ↦ R (f a) (f b)) l

Tactic:
by
  induction l using twoStepInduction <;> grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
S : β → β → Prop
p : α → Prop
f : (a : α) → p a → β
l : List α
hl : ∀ (a : α), a ∈ l → p a
⊢ IsChain S (pmap f l hl) ↔ IsChain (fun a b ↦ ∃ ha hb, S (f a ha) (f b hb)) l

Tactic:
by
  induction l using twoStepInduction <;> grind

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

Goal state before:
pp: case refine_1
α : Type u_1
a : α
s : Multiset α
n : ℕ
ha : a ∈ n • s
⊢ n ≠ 0

Tactic:
rintro rfl
    simp [zero_nsmul] at ha

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

Goal state before:
pp: case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ m - (drop (n % l.length) l).length < n % l.length

Tactic:
· rwa [Nat.sub_lt_iff_lt_add' hm, length_drop, Nat.sub_add_cancel hlt.le]

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

Goal state before:
pp: α : Type u
l l' : List α
n : ℕ
⊢ l.rotate n = l' ↔ l.rotate n = (l'.rotate (l'.length - n % l'.length)).rotate n

Tactic:
rotate_rotate,

Goal state after:
α : Type u
l l' : List α
n : ℕ
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (l'.length - n % l'.length + n)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.reverse =
    (l.reverse.rotate (l.length - (l.length - n % l.length) % l.length)).rotate
      ((l.reverse.rotate (l.length - (l.length - n % l.length) % l.length)).length -
        n % (l.reverse.rotate (l.length - (l.length - n % l.length) % l.length)).length)

Tactic:
rotate_rotate,

Goal state after:
α : Type u
l : List α
n : ℕ
⊢ l.reverse =
    l.reverse.rotate
      (l.length - (l.length - n % l.length) % l.length +
        ((l.reverse.rotate (l.length - (l.length - n % l.length) % l.length)).length -
          n % (l.reverse.rotate (l.length - (l.length - n % l.length) % l.length)).length))
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
hl : l.Nodup
hn : l ≠ []
i j : ℕ
h : l.rotate i = l.rotate j
⊢ i % l.length = j % l.length

Tactic:
rw [← rotate_mod l i, ← rotate_mod l j] at h
  simpa only [head?_rotate, mod_lt, length_pos_of_ne_nil hn, getElem?_eq_getElem, Option.some_inj,
    hl.getElem_inj_iff, Fin.ext_iff] using congr_arg head? h

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

Goal state before:
pp: case h
α : Type u
n : ℕ
hd : α
tl : List α
⊢ ((hd :: tl).rotate n).rotate ((hd :: tl).length * n - n) = hd :: tl

Tactic:
rotate_rotate,

Goal state after:
case h
α : Type u
n : ℕ
hd : α
tl : List α
⊢ (hd :: tl).rotate (n + ((hd :: tl).length * n - n)) = hd :: tl