mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Nonneg.Field

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

Tactic:
exact mul_nonneg q.cast_nonneg a.2

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

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
⊢ Injective fun a ↦ (a⁺ᵐ, a⁻ᵐ)

Tactic:
simp only [Injective, Prod.mk.injEq, and_imp]
  rintro a b hpos hneg
  rw [← oneLePart_div_leOnePart a, ← oneLePart_div_leOnePart b, hpos, hneg]

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

Goal state before:
pp: case inr
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
hq : ↑q.num ≠ 0
n : ℕ
⊢ ↑(q⁻¹ ^ n) = (↑q)⁻¹ ^ n

Tactic:
NNRat.cast_pow

Goal state after:
case inr
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
hq : ↑q.num ≠ 0
n : ℕ
⊢ ↑q⁻¹ ^ n = (↑q)⁻¹ ^ n
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: k : ℕ+
q : ℕ
x✝ : ¬(0 = 0 ∧ q + 1 = 0)
⊢ ↑k + ↑k * q = 0 + (↑k * q + ↑k)

Tactic:
zero_add,

Goal state after:
k : ℕ+
q : ℕ
x✝ : ¬(0 = 0 ∧ q + 1 = 0)
⊢ ↑k + ↑k * q = ↑k * q + ↑k
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
⊢ 0 + 1 ≤ ⌊a⌋ ↔ 1 ≤ a

Tactic:
zero_add,

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
⊢ 1 ≤ ⌊a⌋ ↔ 1 ≤ a
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:
exact le_floor_add _ _

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
z : ℤ
⊢ fract ↑z = 0

Tactic:
unfold fract
  rw [floor_intCast]
  exact sub_self _

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 : R
⊢ Int.cast ⁻¹' Ici a = Ici ⌈a⌉

Tactic:
by
  ext
  simp [ceil_le]

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

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsStrictOrderedRing R
a : R
ha : -1 < a
⊢ ↑⌈a⌉₊ < a + 1

Tactic:
by_cases! h : 0 ≤ a

Goal state after:
case pos
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsStrictOrderedRing R
a : R
ha : -1 < a
h : 0 ≤ a
⊢ ↑⌈a⌉₊ < a + 1

case neg
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsStrictOrderedRing R
a : R
ha : -1 < a
h : a < 0
⊢ ↑⌈a⌉₊ < a + 1
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
⊢ ∃ q, 0 < q ∧ x < q ^ n ∧ q ^ n < y

Tactic:
have m_pos : 0 < m := (Nat.find_pos _).mpr <| by simpa [zero_pow hn] using hy

Goal state after:
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, 0 < q ∧ x < q ^ n ∧ q ^ n < y
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
x : K
x0 : 0 < x
⊢ ∃ q, 0 < q ∧ ↑q < x

Tactic:
simpa only [Rat.cast_pos] using exists_rat_btwn x0

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ count a ↑l = List.count a l

Tactic:
count,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ countP (fun x ↦ a = x) ↑l = List.count a l
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case cons.inr
α : Type u_1
β : Type v
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
a✝ : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
a : α
ha✝ : a ∈ x ::ₘ s
ha : a ∈ s
⊢ ∃ b, b ∈ y ::ₘ t ∧ r a b

Tactic:
rcases ih ha with ⟨b, hbt, hab⟩
      exact ⟨b, mem_cons.2 (Or.inr hbt), hab⟩

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

Goal state before:
pp: α : Type u_1
l₁ : List α
a : α
inst✝ : DecidableEq α
l₂ : List α
h : ¬a ∈ l₁
⊢ l₁.bagInter (a :: l₂) = l₁.bagInter l₂

Tactic:
by
  induction l₁ generalizing l₂ <;> grind

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

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

Tactic:
by
  induction l₁ generalizing l₂ <;> grind

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

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

Tactic:
by
  induction l₁ generalizing l₂ <;> grind

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

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

Tactic:
← eq_union_left h₂

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h₁ : s ≤ u
h₂ : t ≤ u
⊢ s ∪ t ≤ u ∪ t
Module: Mathlib.Data.Finset.Dedup

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

Tactic:
toList,

Goal state after:
α : Type u_1
s : Finset α
⊢ s.val.toList.Nodup
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
this : count x (filter (fun a ↦ f x = f a) s) = (filter (fun a ↦ f x = f a) s).card
⊢ count (f x) (map f s) = count x s

Tactic:
count,

Goal state after:
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Set.InjOn f {x | x ∈ s}
x : α
H : x ∈ s
this : count x (filter (fun a ↦ f x = f a) s) = (filter (fun a ↦ f x = f a) s).card
⊢ countP (fun x_1 ↦ f x = x_1) (map f s) = count x s
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
⊢ count a s = (filter (fun x ↦ a = x) s).card

Tactic:
count,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
⊢ countP (fun x ↦ a = x) s = (filter (fun x ↦ a = x) s).card
Module: Mathlib.Data.List.Infix

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
h : l₁ <+: l₂
⊢ l₂ = l₁ ++ drop l₁.length l₂

Tactic:
by
  induction l₂ generalizing l₁ with
  | nil => simp [List.prefix_nil.mp h]
  | cons _ _ ih =>
    cases l₁ with
    | nil => rfl
    | cons =>
      obtain ⟨rfl, h'⟩ := List.cons_prefix_cons.mp h
      simpa using ih h'

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

Goal state before:
pp: α : Type u_1
a : α
s : Finset α
⊢ s.toList = [a] ↔ s = {a}

Tactic:
toList,

Goal state after:
α : Type u_1
a : α
s : Finset α
⊢ s.val.toList = [a] ↔ s = {a}
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
⊢ ∀ (a b : Finset α), P a b

Tactic:
by
  intro a b
  refine Finset.induction_on b empty_right fun x s _xs hi => symm ?_
  rw [Finset.insert_eq]
  apply union_of _ (symm hi)
  refine Finset.induction_on a empty_right fun a t _ta hi => symm ?_
  rw [Finset.insert_eq]
  exact union_of singletons (symm hi)

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

Goal state before:
pp: case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.succ ≤ p.rev
⊢ i.castSucc = (p.succAbove i.rev).rev

Tactic:
succAbove_of_le_castSucc _ _ (rev_succ _ ▸ (le_rev_iff.mpr h)),

Goal state after:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.succ ≤ p.rev
⊢ i.castSucc = i.rev.succ.rev
Module: Mathlib.Data.Fin.Embedding

Goal state before:
pp: n m✝ m : ℕ
a b : Fin n
⊢ (fun x ↦ x.addNat m) a = (fun x ↦ x.addNat m) b → a = b

Tactic:
simp [Fin.ext_iff]

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

Goal state before:
pp: n✝ m✝ n m : ℕ
a b : Fin m
⊢ natAdd n a = natAdd n b → a = b

Tactic:
simp [Fin.ext_iff]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.toList.length = #s

Tactic:
toList,

Goal state after:
α : Type u_1
s : Finset α
⊢ s.val.toList.length = #s
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
⊢ Injective ⇑f → ∀ (i : Fin n), f i.castSucc ≠ f i.succ

Tactic:
intro hf i hi

Goal state after:
case mp
α : Type u_2
inst✝ : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
hf : Injective ⇑f
i : Fin n
hi : f i.castSucc = f i.succ
⊢ False
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ a.succ = b.succ → a = b

Tactic:
simp [Fin.ext_iff]

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

Goal state before:
pp: n m : ℕ
hmn : m ≤ n
a b : Fin m
⊢ castLE hmn a = castLE hmn b ↔ a = b

Tactic:
simp [Fin.ext_iff]

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

Goal state before:
pp: n m : ℕ
a b : Fin m
⊢ castAdd n a = castAdd n b ↔ a = b

Tactic:
simp [Fin.ext_iff]

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

Goal state before:
pp: n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ (m * n - (↑i / n * n + ↑i % n + 1)) % n = (m * n - ↑i / n * n - (↑i % n + 1)) % n

pp: n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ n ≤ (m - ↑i / n) * n

Tactic:
Nat.sub_sub,

Goal state after:
n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ (m * n - (↑i / n * n + ↑i % n + 1)) % n = (m * n - (↑i / n * n + (↑i % n + 1))) % n

n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ n ≤ (m - ↑i / n) * n
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: case succ
α : Type u
n : ℕ
IH : ∀ (f : Fin n.succ → α), ofFn f = (ofFn fun i ↦ f i.castSucc).concat (f (Fin.last n))
f : Fin (n + 1).succ → α
⊢ f 0 :: (ofFn fun i ↦ f i.castSucc.succ).concat (f (Fin.last n).succ) =
    f (Fin.castSucc 0) :: (ofFn fun i ↦ f i.succ.castSucc).concat (f (Fin.last (n + 1)))

Tactic:
Fin.castSucc_zero,

Goal state after:
case succ
α : Type u
n : ℕ
IH : ∀ (f : Fin n.succ → α), ofFn f = (ofFn fun i ↦ f i.castSucc).concat (f (Fin.last n))
f : Fin (n + 1).succ → α
⊢ f 0 :: (ofFn fun i ↦ f i.castSucc.succ).concat (f (Fin.last n).succ) =
    f 0 :: (ofFn fun i ↦ f i.succ.castSucc).concat (f (Fin.last (n + 1)))
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
j : Fin n
this : (succ 0).succAbove j.succ = (succAbove 0 j).succ
⊢ succAbove 1 j.succ = j.succ.succ

Tactic:
succ_zero_eq_one,

Goal state after:
n : ℕ
j : Fin n
this : succAbove 1 j.succ = (succAbove 0 j).succ
⊢ succAbove 1 j.succ = j.succ.succ
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
α : Fin 0 → Sort u
⊢ Unique ((i : Fin 0) → α i)

Tactic:
by infer_instance

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

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

Tactic:
rw [← cons_succ x p]

Goal state after:
n : ℕ
α : Fin (n + 2) → Sort u_1
x : α 0
p : (i : Fin n.succ) → α i.succ
⊢ cons x p 1 = cons x p (succ 0)
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
rw [← cons_succ x p]

Goal state after:
n : ℕ
α : Fin (n + 2) → Sort u_1
x : α 0
p : (i : Fin n.succ) → α i.succ
⊢ cons x p (last (n + 1)) = cons x p (last n).succ
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: α : Type u_1
l : List α
x : α
h : x ∈+ x :: l
⊢ x ∈ l

Tactic:
by
  obtain h | h := h
  · exact h
  · exact h.mem

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

Goal state before:
pp: m n : ℕ
h : m ≤ n
| m

Tactic:
rw [← Fintype.card_fin m]

Goal state after:
m n : ℕ
h : m ≤ n
| card (Fin m)
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
a b : ℕ
⊢ f 0 < f (b + 1)

Tactic:
OrderEmbedding.lt_iff_lt

Goal state after:
α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
a b : ℕ
⊢ 0 < b + 1
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
ix : ℕ
⊢ f 0 < f (ix + 1)

Tactic:
OrderEmbedding.lt_iff_lt

Goal state after:
α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
ix : ℕ
⊢ 0 < ix + 1
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
h : card α = card β
⊢ α ≃ β

Tactic:
letI := Classical.decEq α

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
h : card α = card β
this : DecidableEq α := Classical.decEq α
⊢ α ≃ β
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ card α = 1 ↔ ∃ x, ∀ (y : α), y = x

Tactic:
rw [← card_unit, card_eq]

Goal state after:
α : Type u_1
inst✝ : Fintype α
⊢ Nonempty (α ≃ Unit) ↔ ∃ x, ∀ (y : α), y = x
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Fintype α
s : Finset β
h : Fintype.card α ≤ Fintype.card ↥s
f : α ↪ ↥s
⊢ Set.range ⇑(f.trans (subtype fun x ↦ x ∈ s)) ⊆ ↑s

Tactic:
simp [Set.range_subset_iff]

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

Goal state before:
pp: α : Type u_4
inst✝ : Infinite α
⊢ Nonempty α

Tactic:
by infer_instance

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✝¹ : Fintype ↑s
inst✝ : DecidablePred fun x ↦ x ∈ t
h : t ⊆ s
⊢ Fintype ↑t

Tactic:
← inter_eq_self_of_subset_right h

Goal state after:
α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred fun x ↦ x ∈ t
h : t ⊆ s
⊢ Fintype ↑(s ∩ t)
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
p : Set β → Prop
⊢ (∃ t, t.Finite ∧ p t ∧ t ⊆ f '' s) ↔ ∃ t, t.Finite ∧ p (f '' t) ∧ t ⊆ s

Tactic:
exists_finite_iff_finset,

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set α
p : Set β → Prop
⊢ (∃ s_1, p ↑s_1 ∧ ↑s_1 ⊆ f '' s) ↔ ∃ s_1, p (f '' ↑s_1) ∧ ↑s_1 ⊆ s
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
motive : (s : Set α) → s.Finite → Prop
s : Set α
hs : s.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s → ∀ (hts : t ⊆ s), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
⊢ ∀ {a : α} {s_1 : Set α},
    a ∉ s_1 →
      s_1.Finite → (∀ (hts : s_1 ⊆ s), motive s_1 ⋯) → ∀ (hts : Insert.insert a s_1 ⊆ s), motive (Insert.insert a s_1) ⋯

Tactic:
intro a s has _ hCs haS

Goal state after:
α : Type u
motive : (s : Set α) → s.Finite → Prop
s✝ : Set α
hs : s✝.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s✝ → ∀ (hts : t ⊆ s✝), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
a : α
s : Set α
has : a ∉ s
hs✝ : s.Finite
hCs : ∀ (hts : s ⊆ s✝), motive s ⋯
haS : Insert.insert a s ⊆ s✝
⊢ motive (Insert.insert a s) ⋯
Module: Mathlib.Data.Multiset.Fold

Goal state before:
pp: case pos
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : a ∈ s
⊢ op a (fold op b (s.erase a)) = op (op a a) (fold op b (s.erase a))

Tactic:
hi.idempotent

Goal state after:
case pos
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : a ∈ s
⊢ op a (fold op b (s.erase a)) = op a (fold op b (s.erase a))
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case neg.inl
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
b : α
l : List α
h : Pairwise r (b :: l)
b' : α
h' : ¬r b' b
bm : b' ∈ List.orderedInsert r b' l
⊢ r b b'

pp: case neg.inr
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : ¬r a b
b' : α
bm✝ : b' ∈ List.orderedInsert r a l
bm : b' ∈ l
⊢ r b b'

Tactic:
· exact (total_of r _ _).resolve_left h'

Goal state after:
case neg.inr
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : ¬r a b
b' : α
bm✝ : b' ∈ List.orderedInsert r a l
bm : b' ∈ l
⊢ r b b'
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s : Set α
inst✝ : Infinite α
hs : s.Finite
h : ∀ (a : α), a ∈ s
⊢ False

Tactic:
exact infinite_univ (hs.subset fun a _ ↦ h _)

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

Goal state before:
pp: α : Type u
l : List α
hl : l.Nodup
n : ℕ
⊢ l.rotate n = l ↔ n % l.length = 0 % ?m.15 ∨ l = []

pp: α : Type u
l : List α
hl : l.Nodup
n : ℕ
⊢ ℕ

Tactic:
← hl.rotate_congr_iff,

Goal state after:
α : Type u
l : List α
hl : l.Nodup
n : ℕ
⊢ l.rotate n = l ↔ l.rotate n = l.rotate 0
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case nil
α : Type u
n : ℕ
⊢ [].rotate n ~r []

Tactic:
exists 0

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

Goal state before:
pp: α : Type u
l l' : List α
h : l ~r l'
⊢ l.reverse ~r l'.reverse

Tactic:
obtain ⟨n, rfl⟩ := h
  exact ⟨_, (reverse_rotate _ _).symm⟩

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

Goal state before:
pp: s : Multiset ℕ
n : ℕ
⊢ s.sum % n = (map (fun x ↦ x % n) s).sum % n

Tactic:
by
  induction s using Multiset.induction <;> simp [Nat.add_mod, *]

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

Goal state before:
pp: k : ℕ
⊢ (0 + 1) * choose 0 (k + 1) = (0 + 1).choose (k + 1 + 1) * (k + 1 + 1)

Tactic:
simp [choose]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst✝ : DecidableEq α
ht : t.Nonempty
⊢ image Prod.fst (s ×ˢ t) = s

Tactic:
by
  ext i
  simp [mem_image, ht.exists_mem]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst✝ : DecidableEq β
ht : s.Nonempty
⊢ image Prod.snd (s ×ˢ t) = t

Tactic:
by
  ext i
  simp [mem_image, ht.exists_mem]

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

Goal state before:
pp: i j : ℕ
this : i ! * (i + j - i)! ∣ (i + j)!
⊢ i ! * j ! ∣ (i + j)!

Tactic:
Nat.add_sub_cancel_left i j

Goal state after:
i j : ℕ
this : i ! * j ! ∣ (i + j)!
⊢ i ! * j ! ∣ (i + j)!
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case neg.h
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
⊢ ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1) = ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1)

Tactic:
cons_swap a a'

Goal state after:
case neg.h
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
⊢ ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1) = ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1)
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case neg.hf.h
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
b : β a
a✝ : b ∈ t a
⊢ ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1) = ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1)

Tactic:
cons_swap a a'

Goal state after:
case neg.hf.h
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
b : β a
a✝ : b ∈ t a
⊢ ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1) = ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1)
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: case neg.hf.hf.h
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
b : β a
a✝¹ : b ∈ t a
b' : β a'
a✝ : b' ∈ t a'
⊢ ((a_1 : α) → a_1 ∈ a ::ₘ a' ::ₘ m → β a_1) = ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1)

Tactic:
cons_swap a a'

Goal state after:
case neg.hf.hf.h
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
b : β a
a✝¹ : b ∈ t a
b' : β a'
a✝ : b' ∈ t a'
⊢ ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1) = ((a_1 : α) → a_1 ∈ a' ::ₘ a ::ₘ m → β a_1)
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: ι : Type u_3
inst✝ : Finite ι
κ : ι → Type u_4
t : (i : ι) → Set (κ i)
ht : ∀ (i : ι), (t i).Finite
⊢ (univ.pi t).Finite

Tactic:
by
  cases nonempty_fintype ι
  lift t to ∀ d, Finset (κ d) using ht
  classical
    rw [← Fintype.coe_piFinset]
    apply Finset.finite_toSet

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

Goal state before:
pp: k : ℕ
⊢ multichoose 1 k = 1

Tactic:
by
  induction k with
  | zero => simp
  | succ k IH => simp [multichoose_succ_succ 0 k, IH]

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
b : ConjClasses α
⊢ a ∈ b.carrier ↔ ConjClasses.mk a = b

Tactic:
by
  revert b
  rw [forall_isConj]
  intro b
  rw [carrier, eq_comm, mk_eq_mk_iff_isConj, ← quotient_mk_eq_mk, Quotient.lift_mk]
  rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective ((U i).restrictPreimage f)
x y : α
e : f x = f y
⊢ f x ∈ iUnion U

Tactic:
rw [hU]; trivial

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective ((U i).restrictPreimage f)
x : β
⊢ x ∈ iUnion U

Tactic:
rw [hU]; trivial

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ i, p i
f : α → β
h : InjOn f (⋃ i, ⋃ (hi : p i), s i hi)
this : Nonempty { i // p i }
⊢ InjOn f (⋃ i, s ↑i ⋯)

Tactic:
simpa only [iUnion, iSup_subtype'] using h

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Basic

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
ι : Sort u_3
p : ι → Subsemigroup M
⊢ ⨆ i, p i = closure (⋃ i, ↑(p i))

Tactic:
Subsemigroup.closure_iUnion,

Goal state after:
M : Type u_1
inst✝ : Mul M
ι : Sort u_3
p : ι → Subsemigroup M
⊢ ⨆ i, p i = ⨆ i, closure ↑(p i)
Module: Mathlib.Algebra.Group.Submonoid.MulAction

Goal state before:
pp: M' : Type u_1
α : Type u_2
β : Type u_3
inst✝ : Monoid M'
S : Submonoid M'
⊢ IsScalarTower (↥S) M' M'

Tactic:
by infer_instance

Goal state after: