mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s)) ∈ upperBounds (lowerBounds s)

Tactic:
· rintro (⟨⟩ | a) ha
      · exfalso
        apply h
        intro b hb
        exact Set.mem_singleton_iff.2 (top_le_iff.1 (ha hb))
      · refine coe_le_coe.2 (le_csInf ?_ ?_)
        · classical
            contrapose! h
            rintro (⟨⟩ | a) ha
            · exact mem_singleton ⊤
            · exact (not_nonempty_iff_eq_empty.2 h ⟨a, ha⟩).elim
        · intro b hb
          rw [← coe_le_coe]
          exact ha hb

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ sInf (f '' s) ≤ sInf (f '' t)

Tactic:
refine le_csInf ((hs.mono hst).image f) ?_

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ ∀ b ∈ f '' t, sInf (f '' s) ≤ b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inl
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
ha : a ∈ upperBounds S
h : S = ∅
⊢ sSup S ≤ a

Tactic:
change ite _ _ _ ≤ a

Goal state after:
case inl
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
ha : a ∈ upperBounds S
h : S = ∅
⊢ (if ⊤ ∈ S then ⊤ else if BddAbove ((fun a ↦ ↑a) ⁻¹' S) then ↑(sSup ((fun a ↦ ↑a) ⁻¹' S)) else ⊤) ≤ a
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ Monotone f ∨ Antitone f → ∀ (a b c : α), c ∈ [[a, b]] → f c ∈ [[f a, f b]]

pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ (∀ (a b c : α), c ∈ [[a, b]] → f c ∈ [[f a, f b]]) → Monotone f ∨ Antitone f

Tactic:
· rintro (hf | hf) a b c <;> simp_rw [← Icc_min_max, ← hf.map_min, ← hf.map_max]
    exacts [fun hc => ⟨hf hc.1, hf hc.2⟩, fun hc => ⟨hf hc.2, hf hc.1⟩]

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ (∀ (a b c : α), c ∈ [[a, b]] → f c ∈ [[f a, f b]]) → Monotone f ∨ Antitone f
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✝² : IsStrictOrderedRing 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
lt : ∀ {x y : S}, f x < f y ↔ x < y
a : S
ha : 0 < a
b c : S
hbc : b < c
⊢ b * a < c * a

Tactic:
rw [← lt, mul, mul]; refine mul_lt_mul_of_pos_right (lt.2 hbc) ?_; rwa [← zero, lt]

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ upperBounds t
⊢ ↑c ≤ sSup (Subtype.val '' t)

pp: case refine_2
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ upperBounds t
⊢ sSup (Subtype.val '' t) ≤ ↑B

Tactic:
· exact (Subtype.mono_coe (· ∈ s)).le_csSup_image hct ⟨B, hB⟩

Goal state after:
case refine_2
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set ↑s
c : ↑s
hct : c ∈ t
B : ↑s
hB : B ∈ upperBounds t
⊢ sSup (Subtype.val '' t) ≤ ↑B
Module: Mathlib.Tactic.NormNum.DivMod

Goal state before:
pp: a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h : ↑r + m = a
h₂ : r < b'
⊢ ↑r / ↑b' + q = q

Tactic:
Int.ediv_eq_zero_of_lt,

Goal state after:
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h : ↑r + m = a
h₂ : r < b'
⊢ 0 + q = q

case H1
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h : ↑r + m = a
h₂ : r < b'
⊢ 0 ≤ ↑r

case H2
a q m : ℤ
b' r : ℕ
hm : q * ↑b' = m
h : ↑r + m = a
h₂ : r < b'
⊢ ↑r < ↑b'
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]
    rcases m.even_or_odd with ⟨m, rfl⟩ | ⟨m, rfl⟩
    · obtain rfl : m = x := mul_left_cancel₀ two_ne_zero <| by simp [← hm, ← two_mul]
      rw [round_intCast, ← two_mul, Int.mul_ediv_cancel_left _ two_ne_zero]
    · refine absurd ?_ hx
      exact (mul_fract_eq_one_iff_exists_int one_lt_two).mpr ⟨m, mod_cast hm.symm⟩

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

Goal state before:
pp: R : Type u_4
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorRing R
n : ℕ
hn : n ≠ 0
a : R
⊢ 0 < ↑n

Tactic:
by positivity

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

Goal state before:
pp: k : Type u_4
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : FloorRing k
a b : k
ha : a ≠ 0
⊢ fract (b / a) * a + ↑⌊b / a⌋ * a = b

Tactic:
← add_mul,

Goal state after:
k : Type u_4
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : FloorRing k
a b : k
ha : a ≠ 0
⊢ (fract (b / a) + ↑⌊b / a⌋) * a = b
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: n d : ℕ
⊢ 0 ≤ ↑n / ↑d

Tactic:
by positivity

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

Goal state before:
pp: α : Type u_1
q : ℚ≥0
hq : 0 < q
⊢ 0 < q.num

Tactic:
by positivity

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

Goal state before:
pp: α : Type u_1
q : ℚ≥0
hq : q ≠ 0
⊢ q.num ≠ 0

Tactic:
by positivity

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

Goal state before:
pp: α : Type u_1
q : ℚ≥0
⊢ 0 < q.den

Tactic:
by positivity

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

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha✝ : 1 ≤ a
ha : 1 < a
this : 0 < a - 1
⊢ 0 ≤ ↑⌈(a - 1)⁻¹⌉

Tactic:
by positivity

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
a b : R
x✝ : ℤ
⊢ x✝ ∈ Int.cast ⁻¹' Ioc a b ↔ x✝ ∈ Ioc ⌊a⌋ ⌊b⌋

Tactic:
simp [floor_lt, le_floor]

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
⊢ 0 < 1 / δ

Tactic:
by positivity

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
⊢ 0 ≤ y / δ

Tactic:
by positivity

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
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : K := ↑m.pred * δ
qny : q ^ n < y
⊢ 0 ≤ q

Tactic:
by positivity

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
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : K := ↑m.pred * δ
qny : q ^ n < y
q1y : |q| < max 1 y
⊢ 0 ≤ δ

Tactic:
by positivity

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
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : K := ↑m.pred * δ
qny : q ^ n < y
q1y : |q| < max 1 y
xqn : max x 0 < q ^ n
⊢ 0 ≤ q

Tactic:
by positivity

Goal state after:
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
p₁ p₂ : P
⊢ v • p₁ /ₛ v • p₂ = p₁ /ₛ p₂

Tactic:
rw [sdiv_smul_eq_sdiv_div, smul_sdiv_assoc, mul_div_cancel_left]

Goal state after:
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 α
hs : Quot.mk (⇑(isSetoid α)) l = Quot.mk (⇑(isSetoid α)) l'
hp : ∀ (x : α), x ∈ Quot.mk (⇑(isSetoid α)) l → p x = p' x
⊢ countP p (Quot.mk (⇑(isSetoid α)) l) = countP p' (Quot.mk (⇑(isSetoid α)) l')

Tactic:
by
      simp only [quot_mk_to_coe'', coe_eq_coe] at hs
      apply hs.countP_congr
      simpa using hp

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

Goal state before:
pp: case cons.inr.inl
α : Type u
β : Type v
f : α → β
tl : List α
ih : (map f tl).Nodup → ∀ ⦃x : α⦄, x ∈ tl → ∀ ⦃y : α⦄, y ∈ tl → f x = f y → x = y
x✝ : α
h₁ : x✝ ∈ tl
y✝ : α
d : (∀ (x : α), x ∈ tl → f x ≠ f y✝) ∧ (map f tl).Nodup
h₃ : f x✝ = f y✝
⊢ x✝ = y✝

Tactic:
apply (d.1 _ h₁ h₃).elim

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

Goal state before:
pp: case mp
α : 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 β
h : ∃ b bs', r a b ∧ (∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs'
⊢ ∃ bs₀ bs₁, (∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁

Tactic:
rcases h with ⟨b, bs', hab, h, rfl⟩

Goal state after:
case mp
α : 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₁
b : β
bs' : Multiset β
hab : r a b
h : ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁
⊢ ∃ bs₀ bs₁, (∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ b ::ₘ bs' = bs₀ + bs₁
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : x ∈ xs
⊢ (f x :: map f xs).dedup = map f (x :: xs).dedup

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : ¬x ∈ xs
⊢ (f x :: map f xs).dedup = map f (x :: xs).dedup

Tactic:
· rw [dedup_cons_of_mem h, dedup_cons_of_mem (mem_map_of_mem h), ih]

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : ¬x ∈ xs
⊢ (f x :: map f xs).dedup = map f (x :: xs).dedup
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
h : t₁.Disjoint t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : ¬x ∈ t₁
h₂ : x ∈ t₂
⊢ x :: xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ x :: xs ∩ t₂

Tactic:
exact perm_cons_append_cons _ l_ih

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
h₁ : List.drop n xs = (List.take n' xs.reverse).reverse
⊢ (List.take n' xs.reverse).reverse ~ ys ∩ (List.take n' xs.reverse).reverse

Tactic:
apply (reverse_perm _).trans

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := ⋯
h₀ : n = xs.length - n'
h₁ : List.drop n xs = (List.take n' xs.reverse).reverse
⊢ List.take n' xs.reverse ~ ys ∩ (List.take n' xs.reverse).reverse
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := ⋯
h₀ : n = xs.length - n'
h₁ : List.drop n xs = (List.take n' xs.reverse).reverse
⊢ xs.reverse ~ ys

Tactic:
apply (reverse_perm _).trans

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := ⋯
h₀ : n = xs.length - n'
h₁ : List.drop n xs = (List.take n' xs.reverse).reverse
⊢ xs ~ ys
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a ↦ p a ∨ q a) s + filter (fun a ↦ p a ∧ q a) s
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) = filter (fun a ↦ p a ∨ q a) (a ::ₘ s) + filter (fun a ↦ p a ∧ q a) (a ::ₘ s)

Tactic:
by_cases p a

Goal state after:
case pos
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a ↦ p a ∨ q a) s + filter (fun a ↦ p a ∧ q a) s
h✝ : p a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) = filter (fun a ↦ p a ∨ q a) (a ::ₘ s) + filter (fun a ↦ p a ∧ q a) (a ::ₘ s)

case neg
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a ↦ p a ∨ q a) s + filter (fun a ↦ p a ∧ q a) s
h✝ : ¬p a
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) = filter (fun a ↦ p a ∨ q a) (a ::ₘ s) + filter (fun a ↦ p a ∧ q a) (a ::ₘ s)
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
⊢ countP p (map f 0) = (filter (fun a ↦ p (f a)) 0).card

Tactic:
map_zero,

Goal state after:
case refine_1
α : Type u_1
β : Type v
f : α → β
s : Multiset α
p : β → Prop
inst✝ : DecidablePred p
⊢ countP p 0 = (filter (fun a ↦ p (f a)) 0).card
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
t : Multiset α
ht : ndinsert a s = t
h : a ∈ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)

Tactic:
ndinsert_of_mem h

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
eq : ∀ (h : ∀ (p : { x // x ∈ s }), ↑p ∈ s), (fun p ↦ ⟨↑p, ⋯⟩) = id
t : Multiset α
ht✝ : ndinsert a s = t
ht : s = t
h : a ∈ s
⊢ t.attach = ndinsert ⟨a, ⋯⟩ (map (fun p ↦ ⟨↑p, ⋯⟩) s.attach)
Module: Mathlib.Data.List.Infix

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
h : ¬a ∈ l
⊢ l <:+ List.insert a l

Tactic:
· simp only [insert_of_not_mem h, suffix_cons]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
h : a ∉ s
⊢ s ≠ insert a t

Tactic:
contrapose h
  simp [h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s✝ t : Finset α
a✝ b : α
f✝ : α → β
s : Finset α
f : α → Type u_3
a : α
has : a ∉ s
x✝ : (i : α) → i ∈ insert a s → f i
⊢ prodPiInsert f (insertPiProd f x✝) = x✝

Tactic:
by grind [prodPiInsert, insertPiProd]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ l.toFinset = ∅ ↔ l = []

Tactic:
cases l <;> simp

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Finset α
⊢ s ∪ insert a t = insert a (s ∪ t)

Tactic:
simp only [insert_eq, union_left_comm]

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

Goal state before:
pp: α : Type u_1
t : Set α
s : Finset ↑t
a : α
ha : a ∈ ↑(map (Embedding.subtype fun x ↦ x ∈ t) s)
⊢ a ∈ t

Tactic:
rw [mem_coe] at ha

Goal state after:
α : Type u_1
t : Set α
s : Finset ↑t
a : α
ha : a ∈ map (Embedding.subtype fun x ↦ x ∈ t) s
⊢ a ∈ t
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ ⊥ = ⊤ ↔ n = 1

Tactic:
subsingleton_iff_bot_eq_top,

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ Subsingleton (Fin n) ↔ n = 1
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: a n : ℕ
inst✝ : NeZero n
⊢ ↑a = 0 ↔ n ∣ a

Tactic:
by
  simp [Fin.ext_iff, Nat.dvd_iff_mod_eq_zero]

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

Goal state before:
pp: n m : ℕ
eq : n = m
a b : Fin n
⊢ Fin.cast eq a = Fin.cast eq b ↔ a = b

Tactic:
simp [← val_inj]

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

Goal state before:
pp: n : ℕ
u v : Fin (n + 2)
h : u < v
⊢ v - (u + 1) < v - u

Tactic:
by
  fin_omega

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

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

Tactic:
rw [lt_castPred_succ_iff, le_def]

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

Goal state before:
pp: α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = n

Tactic:
classical
  refine Nat.decreasingInduction' ?_ hnt ⟨t, by simp [hst]⟩
  intro k _ hnk ⟨u, hu₁, hu₂, hu₃⟩
  obtain ⟨a, ha⟩ : (u \ s).Nonempty := by grind
  exact ⟨u.erase a, by grind⟩

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

Goal state before:
pp: case grind
α : Type u_1
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : 2 * n < #(X ∪ Y)
h✝ : ∀ (a : Finset α), #a ≤ n ∨ ¬a ⊆ X ∧ ¬a ⊆ Y
⊢ False

Tactic:
have : #(X ∪ Y) = #X + #(Y \ X)

Goal state after:
case grind
α : Type u_1
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : 2 * n < #(X ∪ Y)
h✝ : ∀ (a : Finset α), #a ≤ n ∨ ¬a ⊆ X ∧ ¬a ⊆ Y
this : #(X ∪ Y) = #X + #(Y \ X)
⊢ False
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
p i : Fin n
h : i ≤ p
⊢ p.predAbove i.castSucc = i

Tactic:
rw [predAbove_of_le_castSucc _ _ (castSucc_le_castSucc_iff.mpr h), castPred_castSucc]

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

Goal state before:
pp: case grind
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
hst : s ⊆ t
h✝¹ : #s + 1 = #t
a : α
ha : t \ s = {a}
h✝ : ∀ (a : α), insert a s = t → a ∈ s
this : a ∈ t \ s
h : insert a s ⊆ t
⊢ False

Tactic:
have := eq_of_subset_of_card_le h

Goal state after:
case grind
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
hst : s ⊆ t
h✝¹ : #s + 1 = #t
a : α
ha : t \ s = {a}
h✝ : ∀ (a : α), insert a s = t → a ∈ s
this : a ∈ t \ s
h : insert a s ⊆ t
this✝ : #t ≤ #(insert a s) → insert a s = t
⊢ False
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin n
⊢ i.predAbove 0 = 0

Tactic:
by
  cases n
  · exact i.elim0
  · rw [predAbove_of_le_castSucc _ _ (zero_le _), castPred_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
e : α ≃ β
⊢ map (⇑e) univ.val = univ.val

Tactic:
by
  rw [← congr_arg Finset.val (Finset.map_univ_equiv e), Finset.map_val, Equiv.coe_toEmbedding]

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

Goal state before:
pp: case h
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
IH : ∀ m < n, P (f m)
IH' : ∀ (x : Fin n), P (f ↑x)
⊢ P (f n)

Tactic:
hf,

Goal state after:
case h
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
IH : ∀ m < n, P (f m)
IH' : ∀ (x : Fin n), P (f ↑x)
⊢ P (seqOfForallFinsetExistsAux P r h' n)
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ #sᶜ + #s = Fintype.card α

Tactic:
rw [Nat.add_comm, card_add_card_compl]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ 2 < #s ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
by
  classical
    simp_rw [lt_iff_add_one_le, le_card_iff_exists_subset_card, reduceAdd, card_eq_three,
      ← exists_and_left, exists_comm (α := Finset α)]
    constructor
    · rintro ⟨a, b, c, t, hsub, hab, hac, hbc, rfl⟩
      exact ⟨a, b, c, by simp_all [insert_subset_iff]⟩
    · rintro ⟨a, b, c, ha, hb, hc, hab, hac, hbc⟩
      exact ⟨a, b, c, {a, b, c}, by simp_all [insert_subset_iff]⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
n : ℕ
s : Finset α
hsn : #s ≤ n
hnα : n ≤ Fintype.card α
⊢ ∃ t, s ⊆ t ∧ #t = n

Tactic:
simpa using exists_subsuperset_card_eq s.subset_univ hsn hnα

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

Goal state before:
pp: m n : ℕ
α : Sort u_1
f : Fin (m + n) → α
⊢ (append (fun i ↦ f (castAdd n i)) fun i ↦ f (natAdd m i)) = f

Tactic:
unfold append addCases
  simp

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 (last (m + n)) = a

Tactic:
snoc_last

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

Goal state before:
pp: n : ℕ
β : Sort u_2
x : β
p : Fin (n + 1) → β
i : Fin (n + 1)
x✝ : Fin n
⊢ (cons x p ∘ i.succ.succAbove) x✝.succ = cons x (i.removeNth p) x✝.succ

Tactic:
simp [removeNth]

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ p j ≍ snoc (fun j ↦ cast ⋯ (p j)) x j.castSucc

Tactic:
rw [snoc_castSucc]

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ p j ≍ cast ⋯ (p j)
Module: Mathlib.Data.Set.Finite.Basic

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

Tactic:
classical
  infer_instance

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

Goal state before:
pp: case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
p : α → Prop
inst✝ : Finite ↑s
val✝ : Fintype ↑s
⊢ Finite ↑{a | a ∈ s ∧ p a}

Tactic:
classical
  infer_instance

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

Goal state before:
pp: case intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
s : Set α
f : α → β
inst✝ : Finite ↑s
val✝ : Fintype ↑s
⊢ Finite ↑(f '' s)

Tactic:
classical
  infer_instance

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
x : α p
f : (j : Fin (n + 1)) → α j
i : Fin n
⊢ p.removeNth (update f p x) i = p.removeNth f i

Tactic:
simp [removeNth]

Goal state after: