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

Goal state before:
pp: case fst
α : 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✝ : f a × ((i : α) → i ∈ s → f i)
⊢ (insertPiProd f (prodPiInsert f x✝)).1 = x✝.1

pp: case snd
α : 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✝¹ : f a × ((i : α) → i ∈ s → f i)
x✝ : α
hi : x✝ ∈ s
⊢ (insertPiProd f (prodPiInsert f x✝¹)).2 x✝ hi = x✝¹.2 x✝ hi

Tactic:
<;>

Goal state after:
case fst
α : 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✝ : f a × ((i : α) → i ∈ s → f i)
⊢ (insertPiProd f (prodPiInsert f x✝)).1 = x✝.1

case snd
α : 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✝¹ : f a × ((i : α) → i ∈ s → f i)
x✝ : α
hi : x✝ ∈ s
⊢ (insertPiProd f (prodPiInsert f x✝¹)).2 x✝ hi = x✝¹.2 x✝ hi
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
h : a ∈ l
⊢ (a :: l).toFinset.val = (insert a l.toFinset).val

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
h : a ∉ l
⊢ (a :: l).toFinset.val = (insert a l.toFinset).val

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
h : a ∈ l
⊢ (a :: l).toFinset.val = (insert a l.toFinset).val

case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
h : a ∉ l
⊢ (a :: l).toFinset.val = (insert a l.toFinset).val
Module: Mathlib.Data.Finset.Insert

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

pp: case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).toFinset = ∅ ↔ head✝ :: tail✝ = []

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
⊢ [].toFinset = ∅ ↔ [] = []

case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
⊢ (head✝ :: tail✝).toFinset = ∅ ↔ head✝ :: tail✝ = []
Module: Mathlib.Data.Finset.Filter

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

pp: case neg
α : Type u_1
p : Prop
inst✝ : Decidable p
s : Finset α
h✝ : ¬p
⊢ filter (fun _a ↦ p) s = ∅

Tactic:
<;>

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

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

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

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h✝ : a ∉ s₂
⊢ insert a s₁ ∩ s₂ = s₁ ∩ s₂

Tactic:
<;>

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

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

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

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
a : α
h✝ : a ∉ s₁
⊢ s₁ ∩ insert a s₂ = s₁ ∩ s₂

Tactic:
<;>

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

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ {a} ∩ s = {a}

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ {a} ∩ s = ∅

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ {a} ∩ s = {a}

case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ {a} ∩ s = ∅
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ s ∩ {a} = {a}

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ s ∩ {a} = ∅

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ s ∩ {a} = {a}

case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ s ∩ {a} = ∅
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: case refine_1
α : Type u_1
s : Finset α
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
this : b ∈ s.erase a
⊢ a ∉ (s.erase a).erase b

pp: case refine_2
α : Type u_1
s : Finset α
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
this : b ∈ s.erase a
⊢ b ∉ (s.erase a).erase b

pp: case refine_3
α : Type u_1
s : Finset α
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
this : b ∈ s.erase a
⊢ ¬a = b

pp: case refine_4
α : Type u_1
s : Finset α
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
this : b ∈ s.erase a
⊢ cons a (cons b ((s.erase a).erase b) ?refine_2) ⋯ = s

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
s : Finset α
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
this : b ∈ s.erase a
⊢ a ∉ (s.erase a).erase b

case refine_2
α : Type u_1
s : Finset α
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
this : b ∈ s.erase a
⊢ b ∉ (s.erase a).erase b

case refine_3
α : Type u_1
s : Finset α
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
this : b ∈ s.erase a
⊢ ¬a = b

case refine_4
α : Type u_1
s : Finset α
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
this : b ∈ s.erase a
⊢ cons a (cons b ((s.erase a).erase b) ?refine_2) ⋯ = s
Module: Mathlib.Data.Fintype.Defs

Goal state before:
pp: case false
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ false ∈ { val := {true, false}, nodup := fintype._proof_1 }

pp: case true
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ true ∈ { val := {true, false}, nodup := fintype._proof_1 }

Tactic:
<;>

Goal state after:
case false
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ false ∈ { val := {true, false}, nodup := fintype._proof_1 }

case true
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ true ∈ { val := {true, false}, nodup := fintype._proof_1 }
Module: Mathlib.Data.Fintype.Defs

Goal state before:
pp: case lt
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ lt ∈ { val := {lt, eq, gt}, nodup := fintype._proof_1 }

pp: case eq
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ eq ∈ { val := {lt, eq, gt}, nodup := fintype._proof_1 }

pp: case gt
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ gt ∈ { val := {lt, eq, gt}, nodup := fintype._proof_1 }

Tactic:
<;>

Goal state after:
case lt
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ lt ∈ { val := {lt, eq, gt}, nodup := fintype._proof_1 }

case eq
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ eq ∈ { val := {lt, eq, gt}, nodup := fintype._proof_1 }

case gt
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ gt ∈ { val := {lt, eq, gt}, nodup := fintype._proof_1 }
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: case mp
α : Type u_1
s : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ Disjoint (filter p s) (filter q s) → ∀ x ∈ s, p x → ¬q x

pp: case mpr
α : Type u_1
s : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ (∀ x ∈ s, p x → ¬q x) → Disjoint (filter p s) (filter q s)

Tactic:
<;>

Goal state after:
case mp
α : Type u_1
s : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ Disjoint (filter p s) (filter q s) → ∀ x ∈ s, p x → ¬q x

case mpr
α : Type u_1
s : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ (∀ x ∈ s, p x → ¬q x) → Disjoint (filter p s) (filter q s)
Module: Mathlib.Data.Finset.Image

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

pp: case mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
⊢ map f.toEmbedding s ⊆ t → s ⊆ map f.symm.toEmbedding t

Tactic:
<;>

Goal state after:
case mp
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
⊢ s ⊆ map f.symm.toEmbedding t → map f.toEmbedding s ⊆ t

case mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
⊢ map f.toEmbedding s ⊆ t → s ⊆ map f.symm.toEmbedding t
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
a x : α
hn : n = 0
⊢ n ≠ 0 ∧ x = a ↔ x ∈ ∅

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
a x : α
hn : ¬n = 0
⊢ n ≠ 0 ∧ x = a ↔ x ∈ {a}

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
a x : α
hn : n = 0
⊢ n ≠ 0 ∧ x = a ↔ x ∈ ∅

case neg
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
a x : α
hn : ¬n = 0
⊢ n ≠ 0 ∧ x = a ↔ x ∈ {a}
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
x : α
⊢ x ∈ p.toFinset ↔ x ∈ s

Tactic:
@mem_toFinset _ _ (id _),

Goal state after:
α : Type u_1
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
x : α
⊢ x ∈ p ↔ x ∈ s
Module: Mathlib.Data.Finset.Image

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

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

Tactic:
<;>

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

case succ
n✝ n : ℕ
⊢ n + 1 ∈ range (n✝ + 1) ↔ n + 1 ∈ insert 0 (map { toFun := fun i ↦ i + 1, inj' := ⋯ } (range n✝))
Module: Mathlib.Data.Finset.Image

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

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

Tactic:
<;>

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

case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset { a // p a }
a : { a // p a }
⊢ a ∈ s →
    a ∈
      (fun s ↦ Finset.map (Subtype.impEmbedding (Membership.mem ↑s) p ⋯) (↑s).attach)
        ((fun s ↦ ⟨Finset.map { toFun := fun a ↦ ↑a, inj' := ⋯ } s, ⋯⟩) s)
Module: Mathlib.Data.Finset.Image

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

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

Tactic:
<;>

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

case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset { a // p a }
a : { a // p a }
h : a ∈ s
⊢ a ∈
    (fun s ↦ Finset.map (Subtype.impEmbedding (Membership.mem ↑s) p ⋯) (↑s).attach)
      ((fun s ↦ ⟨Finset.map { toFun := fun a ↦ ↑a, inj' := ⋯ } s, ⋯⟩) s)
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset { a // p a }
a : { a // p a }
h : ∃ a_1, ∃ (h : ∃ (x : p a_1), ⟨a_1, ⋯⟩ ∈ s), ⟨a_1, ⋯⟩ = a
⊢ a ∈ s

pp: case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset { a // p a }
a : { a // p a }
h : a ∈ s
⊢ ∃ a_1, ∃ (h : ∃ (x : p a_1), ⟨a_1, ⋯⟩ ∈ s), ⟨a_1, ⋯⟩ = a

Tactic:
<;>

Goal state after:
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset { a // p a }
a : { a // p a }
h : ∃ a_1, ∃ (h : ∃ (x : p a_1), ⟨a_1, ⋯⟩ ∈ s), ⟨a_1, ⋯⟩ = a
⊢ a ∈ s

case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset { a // p a }
a : { a // p a }
h : a ∈ s
⊢ ∃ a_1, ∃ (h : ∃ (x : p a_1), ⟨a_1, ⋯⟩ ∈ s), ⟨a_1, ⋯⟩ = a
Module: Mathlib.Data.Finset.Image

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

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

Tactic:
<;>

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

case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : { s // ∀ a ∈ s, p a }
a : α
⊢ a ∈ ↑s →
    a ∈
      ↑((fun s ↦ ⟨Finset.map { toFun := fun a ↦ ↑a, inj' := ⋯ } s, ⋯⟩)
          ((fun s ↦ Finset.map (Subtype.impEmbedding (Membership.mem ↑s) p ⋯) (↑s).attach) s))
Module: Mathlib.Data.Finset.Image

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

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

Tactic:
<;>

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

case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : { s // ∀ a ∈ s, p a }
a : α
h : a ∈ ↑s
⊢ a ∈
    ↑((fun s ↦ ⟨Finset.map { toFun := fun a ↦ ↑a, inj' := ⋯ } s, ⋯⟩)
        ((fun s ↦ Finset.map (Subtype.impEmbedding (Membership.mem ↑s) p ⋯) (↑s).attach) s))
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : { s // ∀ a ∈ s, p a }
a : α
h : ∃ a_1, ∃ (h : p a_1), (∃ a, ∃ (h_1 : a ∈ ↑s), True ∧ ⟨a, ⋯⟩ = ⟨a_1, ⋯⟩) ∧ a_1 = a
⊢ a ∈ ↑s

pp: case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : { s // ∀ a ∈ s, p a }
a : α
h : a ∈ ↑s
⊢ ∃ a_1, ∃ (h : p a_1), (∃ a, ∃ (h_1 : a ∈ ↑s), True ∧ ⟨a, ⋯⟩ = ⟨a_1, ⋯⟩) ∧ a_1 = a

Tactic:
<;>

Goal state after:
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : { s // ∀ a ∈ s, p a }
a : α
h : ∃ a_1, ∃ (h : p a_1), (∃ a, ∃ (h_1 : a ∈ ↑s), True ∧ ⟨a, ⋯⟩ = ⟨a_1, ⋯⟩) ∧ a_1 = a
⊢ a ∈ ↑s

case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : { s // ∀ a ∈ s, p a }
a : α
h : a ∈ ↑s
⊢ ∃ a_1, ∃ (h : p a_1), (∃ a, ∃ (h_1 : a ∈ ↑s), True ∧ ⟨a, ⋯⟩ = ⟨a_1, ⋯⟩) ∧ a_1 = a
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case isTrue
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ ↑(n - ↑v + ↑u) - ↑n = ↑↑u - ↑↑v

pp: case isTrue.H1
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ 0 ≤ ↑(n - ↑v + ↑u) - ↑n

pp: case isTrue.H2
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ ↑(n - ↑v + ↑u) - ↑n < ↑n

Tactic:
<;>

Goal state after:
case isTrue
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ ↑(n - ↑v + ↑u) - ↑n = ↑↑u - ↑↑v

case isTrue.H1
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ 0 ≤ ↑(n - ↑v + ↑u) - ↑n

case isTrue.H2
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ ↑(n - ↑v + ↑u) - ↑n < ↑n
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case isFalse
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ ↑(n - ↑v + ↑u) = ↑↑u - ↑↑v + ↑n

pp: case isFalse.H1
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ 0 ≤ ↑(n - ↑v + ↑u)

pp: case isFalse.H2
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ ↑(n - ↑v + ↑u) < ↑n

Tactic:
<;>

Goal state after:
case isFalse
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ ↑(n - ↑v + ↑u) = ↑↑u - ↑↑v + ↑n

case isFalse.H1
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ 0 ≤ ↑(n - ↑v + ↑u)

case isFalse.H2
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ ↑(n - ↑v + ↑u) < ↑n
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case isTrue.H1
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ 0 ≤ ↑↑u - ↑↑v

pp: case isTrue.H2
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ ↑↑u - ↑↑v < ↑n

Tactic:
<;>

Goal state after:
case isTrue.H1
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ 0 ≤ ↑↑u - ↑↑v

case isTrue.H2
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ ↑↑u - ↑↑v < ↑n
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case isFalse.H1
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ 0 ≤ ↑↑u - ↑↑v + ↑n

pp: case isFalse.H2
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ ↑↑u - ↑↑v + ↑n < ↑n

Tactic:
<;>

Goal state after:
case isFalse.H1
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ 0 ≤ ↑↑u - ↑↑v + ↑n

case isFalse.H2
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ ↑↑u - ↑↑v + ↑n < ↑n
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case isTrue
n : ℕ
u v : Fin n
h✝ : ↑u + ↑v < n
⊢ ↑(↑u + ↑v) = ↑↑u + ↑↑v

pp: case isTrue.H1
n : ℕ
u v : Fin n
h✝ : ↑u + ↑v < n
⊢ 0 ≤ ↑(↑u + ↑v)

pp: case isTrue.H2
n : ℕ
u v : Fin n
h✝ : ↑u + ↑v < n
⊢ ↑(↑u + ↑v) < ↑n

Tactic:
<;>

Goal state after:
case isTrue
n : ℕ
u v : Fin n
h✝ : ↑u + ↑v < n
⊢ ↑(↑u + ↑v) = ↑↑u + ↑↑v

case isTrue.H1
n : ℕ
u v : Fin n
h✝ : ↑u + ↑v < n
⊢ 0 ≤ ↑(↑u + ↑v)

case isTrue.H2
n : ℕ
u v : Fin n
h✝ : ↑u + ↑v < n
⊢ ↑(↑u + ↑v) < ↑n
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case isFalse
n : ℕ
u v : Fin n
h✝ : ¬↑u + ↑v < n
⊢ ↑(↑u + ↑v) - ↑n = ↑↑u + ↑↑v - ↑n

pp: case isFalse.H1
n : ℕ
u v : Fin n
h✝ : ¬↑u + ↑v < n
⊢ 0 ≤ ↑(↑u + ↑v) - ↑n

pp: case isFalse.H2
n : ℕ
u v : Fin n
h✝ : ¬↑u + ↑v < n
⊢ ↑(↑u + ↑v) - ↑n < ↑n

Tactic:
<;>

Goal state after:
case isFalse
n : ℕ
u v : Fin n
h✝ : ¬↑u + ↑v < n
⊢ ↑(↑u + ↑v) - ↑n = ↑↑u + ↑↑v - ↑n

case isFalse.H1
n : ℕ
u v : Fin n
h✝ : ¬↑u + ↑v < n
⊢ 0 ≤ ↑(↑u + ↑v) - ↑n

case isFalse.H2
n : ℕ
u v : Fin n
h✝ : ¬↑u + ↑v < n
⊢ ↑(↑u + ↑v) - ↑n < ↑n
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case calc_2.mp
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
b : β
⊢ b ∈ image (fun a ↦ i ↑a ⋯) s.attach → b ∈ t

pp: case calc_2.mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
b : β
⊢ b ∈ t → b ∈ image (fun a ↦ i ↑a ⋯) s.attach

Tactic:
<;>

Goal state after:
case calc_2.mp
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
b : β
⊢ b ∈ image (fun a ↦ i ↑a ⋯) s.attach → b ∈ t

case calc_2.mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
b : β
⊢ b ∈ t → b ∈ image (fun a ↦ i ↑a ⋯) s.attach
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case isTrue
n : ℕ
a b : Fin n
h✝ : b ≤ a
⊢ ↑↑(a - b) = ↑↑a - ↑↑b + ↑0

pp: case isFalse
n : ℕ
a b : Fin n
h✝ : ¬b ≤ a
⊢ ↑↑(a - b) = ↑↑a - ↑↑b + ↑n

Tactic:
<;>

Goal state after:
case isTrue
n : ℕ
a b : Fin n
h✝ : b ≤ a
⊢ ↑↑(a - b) = ↑↑a - ↑↑b + ↑0

case isFalse
n : ℕ
a b : Fin n
h✝ : ¬b ≤ a
⊢ ↑↑(a - b) = ↑↑a - ↑↑b + ↑n
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
e : α ≃ β
hst : ∀ (i : α), i ∈ s ↔ e i ∈ t
⊢ Set.MapsTo ⇑e ↑s ↑t

pp: case refine_2
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
e : α ≃ β
hst : ∀ (i : α), i ∈ s ↔ e i ∈ t
⊢ Set.MapsTo ⇑e.symm ↑t ↑s

pp: case refine_3
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
e : α ≃ β
hst : ∀ (i : α), i ∈ s ↔ e i ∈ t
⊢ Set.LeftInvOn ⇑e.symm ⇑e ↑s

pp: case refine_4
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
e : α ≃ β
hst : ∀ (i : α), i ∈ s ↔ e i ∈ t
⊢ Set.RightInvOn ⇑e.symm ⇑e ↑t

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
e : α ≃ β
hst : ∀ (i : α), i ∈ s ↔ e i ∈ t
⊢ Set.MapsTo ⇑e ↑s ↑t

case refine_2
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
e : α ≃ β
hst : ∀ (i : α), i ∈ s ↔ e i ∈ t
⊢ Set.MapsTo ⇑e.symm ↑t ↑s

case refine_3
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
e : α ≃ β
hst : ∀ (i : α), i ∈ s ↔ e i ∈ t
⊢ Set.LeftInvOn ⇑e.symm ⇑e ↑s

case refine_4
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
e : α ≃ β
hst : ∀ (i : α), i ∈ s ↔ e i ∈ t
⊢ Set.RightInvOn ⇑e.symm ⇑e ↑t
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ n - ↑i = n + 1 - (↑i + 1)

Tactic:
Nat.succ_sub_succ_eq_sub

Goal state after:
n : ℕ
i : Fin (n + 1)
⊢ n - ↑i = n - ↑i
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case zero
a b : Fin (0 + 1)
h : a < b
⊢ a + 1 ≤ b

pp: case succ
n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
⊢ a + 1 ≤ b

Tactic:
<;>

Goal state after:
case zero
a b : Fin (0 + 1)
h : a < b
⊢ a + 1 ≤ b

case succ
n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
⊢ a + 1 ≤ b
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ #(t \ s) = #(t \ (s ∩ t))

pp: α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ s ∩ t ⊆ t

Tactic:
<;>

Goal state after:
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ #(t \ s) = #(t \ (s ∩ t))

α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ s ∩ t ⊆ t
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s t : Finset α
h : #s < #t
⊢ ∃ e ∈ t, e ∉ s

Tactic:
simpa [Finset.Nonempty] using sdiff_nonempty_of_card_lt_card h

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
⊢ i.succ.succAbove 1 = (i.succAbove 0).succ

Tactic:
rw [← succ_zero_eq_one']
  exact succ_succAbove_succ i 0

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

Goal state before:
pp: case zero
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
⊢ cons x (update p i y) 0 = update (cons x p) i.succ y 0

pp: case succ
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
i✝ : Fin n
⊢ cons x (update p i y) i✝.succ = update (cons x p) i.succ y i✝.succ

Tactic:
<;>

Goal state after:
case zero
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
⊢ cons x (update p i y) 0 = update (cons x p) i.succ y 0

case succ
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
i✝ : Fin n
⊢ cons x (update p i y) i✝.succ = update (cons x p) i.succ y i✝.succ