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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ Disjoint (s.erase a) t ↔ Disjoint s (t.erase a)

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ Disjoint (s.erase a) t ↔ Disjoint s (t.erase a)
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ t
hst : Disjoint (s.erase a) t
⊢ Disjoint s t

Tactic:
rw [← erase_insert ha, ← disjoint_erase_comm, disjoint_insert_right]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ t
hst : Disjoint (s.erase a) t
⊢ a ∉ s.erase a ∧ Disjoint (s.erase a) t
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:
[

Goal state after:
α : 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)
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b x✝¹ : β
x✝ : x✝¹ ∈ s
⊢ x✝¹ ≠ b ↔ b ≠ x✝¹

Tactic:
[

Goal state after:
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b x✝¹ : β
x✝ : x✝¹ ∈ s
⊢ x✝¹ ≠ b ↔ b ≠ x✝¹
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : Subsingleton α
⊢ s.Nonempty → s = univ

Tactic:
rintro ⟨x, hx⟩
  exact eq_univ_of_forall fun y => by rwa [Subsingleton.elim y x]

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
⊢ insert a (insert a s)ᶜ = sᶜ

Tactic:
[

Goal state after:
α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
⊢ insert a (insert a s)ᶜ = sᶜ
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ s
hi' : i ∈ s ∪ t
⊢ (piFinsetUnion α h) (f, g) ⟨i, hi'⟩ = f ⟨i, hi⟩

Tactic:
[

Goal state after:
ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ s
hi' : i ∈ s ∪ t
⊢ (piFinsetUnion α h) (f, g) ⟨i, hi'⟩ = f ⟨i, hi⟩
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
β' : Type u_4
f : β ↪ γ
g : α ↪ β
f' : α ↪ β'
g' : β' ↪ γ
h_comm : ∀ (a : α), f (g a) = g' (f' a)
⊢ map f (map g s) = map g' (map f' s)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
β' : Type u_4
f : β ↪ γ
g : α ↪ β
f' : α ↪ β'
g' : β' ↪ γ
h_comm : ∀ (a : α), f (g a) = g' (f' a)
⊢ map f (map g s) = map g' (map f' s)
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ t
hi' : i ∈ s ∪ t
⊢ (piFinsetUnion α h) (f, g) ⟨i, hi'⟩ = g ⟨i, hi⟩

Tactic:
[

Goal state after:
ι : Type u_5
inst✝ : DecidableEq ι
α : ι → Type u_4
s t : Finset ι
h : Disjoint s t
f : (i : ↥s) → α ↑i
g : (i : ↥t) → α ↑i
i : ι
hi : i ∈ t
hi' : i ∈ s ∪ t
⊢ (piFinsetUnion α h) (f, g) ⟨i, hi'⟩ = g ⟨i, hi⟩
Module: Mathlib.Data.Finset.SymmDiff

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ a ∈ s ∆ t ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ a ∈ s ∆ t ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
⊢ x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s

Tactic:
have := disjoint_left.1 h

Goal state after:
α : Type u_4
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
x : α
this : ∀ ⦃a : α⦄, a ∈ s → a ∉ t
⊢ x ∈ s ∨ x ∈ t ↔ x ∈ s ∧ x ∉ t ∨ x ∈ t ∧ x ∉ s
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
t : Set α
s : Finset α
inst✝ : Fintype ↑t
⊢ s ⊆ t.toFinset ↔ ↑s ⊆ t

Tactic:
by
  rw [← Finset.coe_subset, coe_toFinset]

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
t : Finset α
⊢ s.toFinset ⊆ t ↔ s ⊆ ↑t

Tactic:
by
  rw [← Finset.coe_subset, coe_toFinset]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f g : α → β
s : Finset α
h : Set.EqOn f g ↑s
a✝ : β
⊢ a✝ ∈ image f s ↔ a✝ ∈ image g s

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f g : α → β
s : Finset α
h : Set.EqOn f g ↑s
a✝ : β
⊢ a✝ ∈ image f s ↔ a✝ ∈ image g s
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq β
s : Finset α
β' : Type u_4
inst✝¹ : DecidableEq β'
inst✝ : DecidableEq γ
f : β → γ
g : α → β
f' : α → β'
g' : β' → γ
h_comm : ∀ (a : α), f (g a) = g' (f' a)
⊢ image f (image g s) = image g' (image f' s)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq β
s : Finset α
β' : Type u_4
inst✝¹ : DecidableEq β'
inst✝ : DecidableEq γ
f : β → γ
g : α → β
f' : α → β'
g' : β' → γ
h_comm : ∀ (a : α), f (g a) = g' (f' a)
⊢ image f (image g s) = image g' (image f' s)
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α ↪ β
s : Finset α
a : α
⊢ map f (s.erase a) = (map f s).erase (f a)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
inst✝ : DecidableEq α
f : α ↪ β
s : Finset α
a : α
⊢ map f (s.erase a) = (map f s).erase (f a)
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: n : ℕ
j : Fin (n + 1)
⊢ ↑j + ↑j.rev = n

Tactic:
j.add_rev_cast

Goal state after:
n : ℕ
j : Fin (n + 1)
⊢ n = n
Module: Mathlib.Order.Fin.Basic

Goal state before:

Tactic:
_ ≤ _ := Nat.pred_le _
      _ ≤ _ := H

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

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this : s = image (fun i ↦ f ↑i ⋯) (range n).attach
⊢ #s = #(image (fun i ↦ f ↑i ⋯) (range n).attach)

Tactic:
this

Goal state after:
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this : s = image (fun i ↦ f ↑i ⋯) (range n).attach
⊢ #(image (fun i ↦ f ↑i ⋯) (range n).attach) = #(image (fun i ↦ f ↑i ⋯) (range n).attach)
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
⊢ ∃ k, k ≠ ⟨i, hi⟩ ∧ k ≠ ⟨j, hj⟩

Tactic:
[

Goal state after:
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
⊢ ∃ k, k ≠ ⟨i, hi⟩ ∧ k ≠ ⟨j, hj⟩
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
h : 1 ≠ 0
⊢ pred 1 h = 0

Tactic:
[

Goal state after:
n : ℕ
inst✝ : NeZero n
h : 1 ≠ 0
⊢ pred 1 h = 0
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
h : ¬last (n + 1) = 0
⊢ (last (n + 1)).pred h = last n

Tactic:
[

Goal state after:
n : ℕ
h : ¬last (n + 1) = 0
⊢ (last (n + 1)).pred h = last n
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
hi : i ≠ last n
j : Fin n
h : i = j.castSucc
⊢ i.castPred hi = j

Tactic:
[

Goal state after:
n : ℕ
i : Fin (n + 1)
hi : i ≠ last n
j : Fin n
h : i = j.castSucc
⊢ i.castPred hi = j
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hinj : Set.InjOn f ↑s
hst : #t ≤ #s
this : image f s = t
⊢ t ⊆ image f s

Tactic:
this

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hinj : Set.InjOn f ↑s
hst : #t ≤ #s
this : image f s = t
⊢ t ⊆ t
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hsurj : Set.SurjOn f ↑s ↑t
hst : #s ≤ #t
this : image f s = t
⊢ #(image f s) = #t

Tactic:
this

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hsurj : Set.SurjOn f ↑s ↑t
hst : #s ≤ #t
this : image f s = t
⊢ #t = #t
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
hi : i ≠ last n
hj : j ≠ last n
⊢ i.castPred hi = j.castPred hj ↔ i = j

Tactic:
[

Goal state after:
n : ℕ
i j : Fin (n + 1)
hi : i ≠ last n
hj : j ≠ last n
⊢ i.castPred hi = j.castPred hj ↔ i = j
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: α : Type u
m : ℕ
f : Fin m → α
⊢ ofFn f = ofFn fun i ↦ f (Fin.cast ⋯ i)

Tactic:
[

Goal state after:
α : Type u
m : ℕ
f : Fin m → α
⊢ ofFn f = ofFn fun i ↦ f (Fin.cast ⋯ i)
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: α : Type u
m n : ℕ
a : Fin m → α
b : Fin n → α
⊢ ofFn (Fin.append a b) = ofFn a ++ ofFn b

Tactic:
[

Goal state after:
α : Type u
m n : ℕ
a : Fin m → α
b : Fin n → α
⊢ ofFn (Fin.append a b) = ofFn a ++ ofFn b
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
rw [castPred_le_iff, succ_le_castSucc_iff]

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

Goal state before:
pp: case succ
α : Type u
n m : ℕ
IH : ∀ (f : Fin (m * n) → α), ofFn f = (ofFn fun i ↦ ofFn fun j ↦ f ⟨↑i * n + ↑j, ⋯⟩).flatten
f : Fin ((m + 1) * n) → α
⊢ ofFn f = (ofFn fun i ↦ ofFn fun j ↦ f ⟨↑i * n + ↑j, ⋯⟩).flatten

Tactic:
[

Goal state after:
case succ
α : Type u
n m : ℕ
IH : ∀ (f : Fin (m * n) → α), ofFn f = (ofFn fun i ↦ ofFn fun j ↦ f ⟨↑i * n + ↑j, ⋯⟩).flatten
f : Fin ((m + 1) * n) → α
⊢ ofFn f = (ofFn fun i ↦ ofFn fun j ↦ f ⟨↑i * n + ↑j, ⋯⟩).flatten
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: α : Type u
m n : ℕ
f : Fin (m * n) → α
⊢ ofFn f = (ofFn fun i ↦ ofFn fun j ↦ f ⟨m * ↑i + ↑j, ⋯⟩).flatten

Tactic:
[

Goal state after:
α : Type u
m n : ℕ
f : Fin (m * n) → α
⊢ ofFn f = (ofFn fun i ↦ ofFn fun j ↦ f ⟨m * ↑i + ↑j, ⋯⟩).flatten
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: α : Type u
n : ℕ
c : α
⊢ (ofFn fun x ↦ c) = replicate (n + 1) c

Tactic:
rw [replicate, ← ofFn_const n]

Goal state after:
α : Type u
n : ℕ
c : α
⊢ (ofFn fun x ↦ c) = c :: ofFn fun x ↦ c
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case pos
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : j.castSucc < p
hij : i.succ = j.castSucc
⊢ i = j

Tactic:
rw [← hij] at hj
    cases hi <| Nat.lt_trans i.castSucc_lt_succ hj

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

Goal state before:
pp: α : Type u
m : ℕ
a : Fin m → α
n : ℕ
⊢ ofFn (Fin.repeat n a) = (replicate n (ofFn a)).flatten

Tactic:
[

Goal state after:
α : Type u
m : ℕ
a : Fin m → α
n : ℕ
⊢ ofFn (Fin.repeat n a) = (replicate n (ofFn a)).flatten
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : a.succAbove b ≠ 0
⊢ (a.pred ha).succAbove (b.pred hb) = (a.succAbove b).pred hk

Tactic:
[

Goal state after:
n : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : a.succAbove b ≠ 0
⊢ (a.pred ha).succAbove (b.pred hb) = (a.succAbove b).pred hk
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ last (n + 1)
hb : b ≠ last n
hk : a.succAbove b ≠ last (n + 1)
⊢ (a.castPred ha).succAbove (b.castPred hb) = (a.succAbove b).castPred hk

Tactic:
[

Goal state after:
n : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ last (n + 1)
hb : b ≠ last n
hk : a.succAbove b ≠ last (n + 1)
⊢ (a.castPred ha).succAbove (b.castPred hb) = (a.succAbove b).castPred hk
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
h : (ofFn (Fin.cons x₀ xs)).Nodup
⊢ ¬x₀ ∈ Set.range xs ∧ Function.Injective xs

Tactic:
[

Goal state after:
case refine_2
α : Type u
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : (ofFn xs).Nodup → Function.Injective xs
h : (ofFn (Fin.cons x₀ xs)).Nodup
⊢ ¬x₀ ∈ Set.range xs ∧ Function.Injective xs
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case zero
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
⊢ cons (q 0) (tail q) 0 = q 0

Tactic:
simp [tail]

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

Goal state before:
pp: case succ
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i✝ : Fin n
⊢ cons (q 0) (tail q) i✝.succ = q i✝.succ

Tactic:
simp [tail]

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

Goal state before:
pp: ι : Type u_4
α : ι → Type u_5
inst✝ : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
h : 1 < #s
⊢ ∃ i, 1 < #(image (fun x ↦ x i) s) ∧ ∀ (ai : α i), {x ∈ s | x i = ai} ⊂ s

Tactic:
[

Goal state after:
ι : Type u_4
α : ι → Type u_5
inst✝ : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
h : 1 < #s
⊢ ∃ i, 1 < #(image (fun x ↦ x i) s) ∧ ∀ (ai : α i), {x ∈ s | x i = ai} ⊂ s
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
z : α 0
j : Fin n
⊢ tail (update q 0 z) j = tail q j

Tactic:
simp [tail]

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

Goal state before:
pp: case pos
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
j : Fin n
h : j = i
⊢ tail (update q i.succ y) i = update (tail q) i y i

Tactic:
simp [tail]

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

Goal state before:
pp: n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
q : Fin n.succ → α
j : Fin n
⊢ (g ∘ tail q) j = tail (g ∘ q) j

Tactic:
simp [tail]

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
inst✝ : (i : Fin (n + 1)) → Preorder (α i)
x : α 0
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α i.succ
j : Fin n
⊢ q j.succ ≤ cons x p j.succ ↔ tail q j ≤ p j

Tactic:
simp [tail]

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

Goal state before:
pp: case inr
n : ℕ
a : Fin n
b : Fin (n + 1)
h : b ≤ a.castSucc
⊢ a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc

Tactic:
rw [predAbove_of_le_castSucc _ _ h, predAbove_castSucc_of_le _ _ h, castSucc_castPred]

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:
[

Goal state after:
α : Type u_1
s : Finset α
⊢ 2 < #s ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ 2 < card α ↔ ∃ a b c, a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : Fintype α
⊢ 2 < card α ↔ ∃ a b c, a ≠ b ∧ a ≠ c ∧ b ≠ c
Module: Mathlib.Data.Finset.Card

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

Tactic:
[

Goal state after:
α : Type u_1
s : Finset α
⊢ 2 < #s ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≠ b ∧ a ≠ c ∧ b ≠ c
Module: Mathlib.Data.Finset.Card

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

Tactic:
[

Goal state after:
α : Type u_1
s : Finset α
⊢ 3 < #s ↔ ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
s : Set α
inst✝ : Fintype ↑s
⊢ Fintype.card ↑s = Fintype.card α ↔ s = Set.univ

Tactic:
rw [← Set.toFinset_card, Finset.card_eq_iff_eq_univ, ← Set.toFinset_univ, Set.toFinset_inj]

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

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

Tactic:
· intro i
    rw [Fin.append_right, Function.comp_apply, Fin.cast_natAdd, eq_comm, Fin.addNat_one]
    exact Fin.cons_succ _ _ _

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

Goal state before:
pp: n : ℕ
α : Sort u_1
x : α
xs : Fin n → α
⊢ cons x xs = append (cons x elim0) xs ∘ Fin.cast ⋯

Tactic:
funext i; simp [append_left_eq_cons]

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

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

Tactic:
[

Goal state after:
α : Type u_1
s : Finset α
⊢ 3 < #s ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, ∃ d ∈ s, a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
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:
[

Goal state after:
α : 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}
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: α : Type u_1
l : List α
⊢ l.Nodup ↔ ∀ (x : α), ¬x ∈+ l

Tactic:
[

Goal state after:
α : Type u_1
l : List α
⊢ l.Nodup ↔ ∀ (x : α), ¬x ∈+ l
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
i : ℕ
⊢ g (i + 1) ⊆ g i

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
i : ℕ
⊢ g (i + 1) ⊆ g i
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl : ∀ (a : α), a ∈ x :: xs → ∀ (b : α), b ∈ x :: xs → (r a b ↔ s (f a) (f b))
⊢ map f (insertionSort r (x :: xs)) = insertionSort s (map f (x :: xs))

Tactic:
[

Goal state after:
case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl : ∀ (a : α), a ∈ x :: xs → ∀ (b : α), b ∈ x :: xs → (r a b ↔ s (f a) (f b))
⊢ map f (insertionSort r (x :: xs)) = insertionSort s (map f (x :: xs))
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    (∀ (x_1 : α), x_1 ∈ xs → (r x_1 x ↔ s (f x_1) (f x))) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs → (r x x_2 ↔ s (f x) (f x_2))
⊢ map f (insertionSort r (x :: xs)) = insertionSort s (map f (x :: xs))

Tactic:
[

Goal state after:
case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
x : α
xs : List α
ih :
  (∀ (a : α), a ∈ xs → ∀ (b : α), b ∈ xs → (r a b ↔ s (f a) (f b))) →
    map f (insertionSort r xs) = insertionSort s (map f xs)
hl :
  ((r x x ↔ s (f x) (f x)) ∧ ∀ (x_1 : α), x_1 ∈ xs → (r x x_1 ↔ s (f x) (f x_1))) ∧
    (∀ (x_1 : α), x_1 ∈ xs → (r x_1 x ↔ s (f x_1) (f x))) ∧
      ∀ (x : α), x ∈ xs → ∀ (x_2 : α), x_2 ∈ xs → (r x x_2 ↔ s (f x) (f x_2))
⊢ map f (insertionSort r (x :: xs)) = insertionSort s (map f (x :: xs))
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s t : Set α
inst✝ : Finite ↑s
h : t ⊆ s
⊢ Finite ↑t

Tactic:
rw [← sep_eq_of_subset h]

Goal state after:
α : Type u
s t : Set α
inst✝ : Finite ↑s
h : t ⊆ s
⊢ Finite ↑{x | x ∈ s ∧ x ∈ t}
Module: Mathlib.Data.Set.Finite.Basic

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

Tactic:
[

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
n : ℕ
f : Fin n → α
⊢ (ofFn f).SortedGT ↔ StrictAnti f

Tactic:
by
  simp only [sortedGT_iff_strictAnti_get, StrictAnti, Fin.forall_iff,
    length_ofFn, get_ofFn, Fin.cast_mk, Fin.mk_lt_mk]

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

Goal state before:
pp: n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
i : Fin n
⊢ i < Fin.find p h ↔ ∀ (m : Fin n), m ≤ i → ¬p m

Tactic:
[

Goal state after:
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
i : Fin n
⊢ i < Fin.find p h ↔ ∀ (m : Fin n), m ≤ i → ¬p m
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
i : Fin n
⊢ i ≤ Fin.find p h ↔ ∀ (m : Fin n), m < i → ¬p m

Tactic:
[

Goal state after:
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
i : Fin n
⊢ i ≤ Fin.find p h ↔ ∀ (m : Fin n), m < i → ¬p m
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
h0 : ¬p 0
⊢ Fin.find p h = (Fin.find (fun k ↦ p k.succ) ⋯).succ

Tactic:
[

Goal state after:
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
h0 : ¬p 0
⊢ Fin.find p h = (Fin.find (fun k ↦ p k.succ) ⋯).succ
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
l : List α
⊢ (map (⇑e) l).SortedLE ↔ l.SortedLE

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
l : List α
⊢ (map (⇑e) l).SortedLE ↔ l.SortedLE
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
l : List α
⊢ (map (⇑e) l).SortedLT ↔ l.SortedLT

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
l : List α
⊢ (map (⇑e) l).SortedLT ↔ l.SortedLT
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
l : List α
⊢ (map (⇑e) l).SortedGE ↔ l.SortedGE

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
l : List α
⊢ (map (⇑e) l).SortedGE ↔ l.SortedGE
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
l : List α
⊢ (map (⇑e) l).SortedGT ↔ l.SortedGT

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
l : List α
⊢ (map (⇑e) l).SortedGT ↔ l.SortedGT
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
⊢ (find? fun x ↦ decide (p x)) = if h : ∃ i, p i then some (Fin.find p h) else none

Tactic:
[

Goal state after:
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
⊢ (find? fun x ↦ decide (p x)) = if h : ∃ i, p i then some (Fin.find p h) else none
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
i : Fin n
p : Fin n → Bool
h : p i = true
⊢ (find? p).get ⋯ = Fin.find (fun x ↦ p x = true) ⋯

Tactic:
[

Goal state after:
n : ℕ
i : Fin n
p : Fin n → Bool
h : p i = true
⊢ (find? p).get ⋯ = Fin.find (fun x ↦ p x = true) ⋯