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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a x : α
hx : x ∈ insert a s
⊢ ⟨x, hx⟩ ∈ (insert a s).attach ↔ ⟨x, hx⟩ ∈ insert ⟨a, ⋯⟩ (image (fun x ↦ ⟨↑x, ⋯⟩) s.attach)

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a x : α
hx : x ∈ insert a s
⊢ ⟨x, hx⟩ ∈ (insert a s).attach ↔ ⟨x, hx⟩ ∈ insert ⟨a, ⋯⟩ (image (fun x ↦ ⟨↑x, ⋯⟩) s.attach)
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidablePred fun x ↦ x ∈ s
a✝ : ↥s
⊢ a✝ ∈ Finset.subtype (fun x ↦ x ∈ s) s ↔ a✝ ∈ s.attach

Tactic:
;

Goal state after:
α : Type u_1
s : Finset α
inst✝ : DecidablePred fun x ↦ x ∈ s
a✝ : ↥s
⊢ a✝ ∈ Finset.subtype (fun x ↦ x ∈ s) s ↔ a✝ ∈ s.attach
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
f : α → β
this : CanLift β (↑s) (f ∘ Subtype.val) fun y ↦ y ∈ f '' s :=
  {
    prf := fun y x ↦
      match x with
      | Exists.intro x ⟨hxt, hy⟩ => Exists.intro ⟨x, hxt⟩ hy }
t : Finset ↑s
y : β
⊢ y ∈ image f (map (Embedding.subtype fun x ↦ x ∈ s) t) ↔ y ∈ image (f ∘ Subtype.val) t

Tactic:
;

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
f : α → β
this : CanLift β (↑s) (f ∘ Subtype.val) fun y ↦ y ∈ f '' s :=
  {
    prf := fun y x ↦
      match x with
      | Exists.intro x ⟨hxt, hy⟩ => Exists.intro ⟨x, hxt⟩ hy }
t : Finset ↑s
y : β
⊢ y ∈ image f (map (Embedding.subtype fun x ↦ x ∈ s) t) ↔ y ∈ image (f ∘ Subtype.val) t
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : 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

Tactic:
;

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

Goal state before:
pp: α : 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

Tactic:
;

Goal state after:
α : 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
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: n : ℕ
i : Fin n
⊢ Fin.cast ⋯ i.rev = (Fin.cast ⋯ i).rev

Tactic:
;

Goal state after:
n : ℕ
i : Fin n
⊢ Fin.cast ⋯ i.rev = (Fin.cast ⋯ i).rev
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
h : i ≠ last n
h' : i.rev ≠ 0
⊢ (i.castPred h).rev = i.rev.pred h'

Tactic:
by
  rw [← succ_inj, succ_pred, ← rev_castSucc, castSucc_castPred]

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

Goal state before:
pp: n m : ℕ
hmn : n ≤ m
y : Fin m
x✝ : y ∈ Set.range ⇑((addNatEmb (m - n)).trans (finCongr ⋯).toEmbedding)
x : Fin n
hx : ((addNatEmb (m - n)).trans (finCongr ⋯).toEmbedding) x = y
⊢ m ≤ ↑x + (m - n) + n

Tactic:
;

Goal state after:
n m : ℕ
hmn : n ≤ m
y : Fin m
x✝ : y ∈ Set.range ⇑((addNatEmb (m - n)).trans (finCongr ⋯).toEmbedding)
x : Fin n
hx : ((addNatEmb (m - n)).trans (finCongr ⋯).toEmbedding) x = y
⊢ m ≤ ↑x + (m - n) + n
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case mp
α : 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
a : α
ha : a ∈ s
⊢ ∃ i, ∃ (hi : i ∈ range n), f i ⋯ = a

Tactic:
;

Goal state after:
case mp
α : 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
a : α
ha : a ∈ s
⊢ ∃ i, ∃ (hi : i ∈ range n), f i ⋯ = a
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case mp
α : 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
i : ℕ
hi : i < n
ha : f i hi ∈ s
⊢ ∃ i_1, ∃ (hi_1 : i_1 ∈ range n), f i_1 ⋯ = f i hi

Tactic:
;

Goal state after:
case mp
α : 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
i : ℕ
hi : i < n
ha : f i hi ∈ s
⊢ ∃ i_1, ∃ (hi_1 : i_1 ∈ range n), f i_1 ⋯ = f i hi
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: n : ℕ
⊢ (castOrderIso ⋯).symm = castOrderIso ⋯

Tactic:
;

Goal state after:
n : ℕ
⊢ (castOrderIso ⋯).symm = castOrderIso ⋯
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: n : ℕ
h : n = n
x✝ : Fin n
⊢ ↑((castOrderIso h) x✝) = ↑((OrderIso.refl (Fin n)) x✝)

Tactic:
;

Goal state after:
n : ℕ
h : n = n
x✝ : Fin n
⊢ ↑((castOrderIso h) x✝) = ↑((OrderIso.refl (Fin n)) x✝)
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: n : ℕ
⊢ (castOrderIso ⋯).toEquiv = Equiv.cast ⋯

Tactic:
;

Goal state after:
n : ℕ
⊢ (castOrderIso ⋯).toEquiv = Equiv.cast ⋯
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case mpr
α : 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
i : ℕ
hi : i ∈ range n
⊢ f i ⋯ ∈ s

Tactic:
;

Goal state after:
case mpr
α : 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
i : ℕ
hi : i ∈ range n
⊢ f i ⋯ ∈ s
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
⊢ 1 < n ↔ 2 ≤ n

Tactic:
;

Goal state after:
n : ℕ
⊢ 1 < n ↔ 2 ≤ n
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n✝ m n : ℕ
⊢ NeZero (n + 1)

Tactic:
;

Goal state after:
n✝ m n : ℕ
⊢ NeZero (n + 1)
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
w✝ : ↥s
left✝ : w✝ ∈ s.attach
h : i ↑w✝ ⋯ ∈ image (fun a ↦ i ↑a ⋯) s.attach
⊢ i ↑w✝ ⋯ ∈ t

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
w✝ : ↥s
left✝ : w✝ ∈ s.attach
h : i ↑w✝ ⋯ ∈ image (fun a ↦ i ↑a ⋯) s.attach
⊢ i ↑w✝ ⋯ ∈ t
Module: Mathlib.Data.Finset.Card

Goal state before:
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
a : α
ha : a ∈ s
h : i a ha ∈ t
⊢ i a ha ∈ image (fun a ↦ i ↑a ⋯) s.attach

Tactic:
;

Goal state after:
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
a : α
ha : a ∈ s
h : i a ha ∈ t
⊢ i a ha ∈ image (fun a ↦ i ↑a ⋯) s.attach
Module: Mathlib.Data.Fin.Basic

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

Tactic:
;

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ ↑↑n = ↑0
Module: Mathlib.Data.Fin.Basic

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

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

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

Goal state before:
pp: n : ℕ
⊢ ↑↑n = ↑(last n)

Tactic:
;

Goal state after:
n : ℕ
⊢ ↑↑n = ↑(last n)
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
k : Fin n
h : k ≤ 0
⊢ 0 = ↑0

Tactic:
;

Goal state after:
n : ℕ
inst✝ : NeZero n
k : Fin n
h : k ≤ 0
⊢ 0 = ↑0
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ 0 ≤ 0

Tactic:
;

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ 0 ≤ 0
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n a b : ℕ
han : a < n.succ
hbn : b < n.succ
⊢ ↑a < ↑b ↔ a < b

Tactic:
;

Goal state after:
n a b : ℕ
han : a < n.succ
hbn : b < n.succ
⊢ ↑a < ↑b ↔ a < b
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
h : n = n
x✝ : Fin n
⊢ ↑((finCongr h) x✝) = ↑((Equiv.refl (Fin n)) x✝)

Tactic:
;

Goal state after:
n : ℕ
h : n = n
x✝ : Fin n
⊢ ↑((finCongr h) x✝) = ↑((Equiv.refl (Fin n)) x✝)
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
⊢ finCongr ⋯ = Equiv.cast ⋯

Tactic:
;

Goal state after:
n : ℕ
⊢ finCongr ⋯ = Equiv.cast ⋯
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ a.castSucc < b.succ ↔ a ≤ b

Tactic:
rw [castSucc_lt_iff_succ_le, succ_le_succ_iff]

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
i : Fin n
hl : ↑i < ↑a
hu : ↑b < ↑i + 1
⊢ ↑b < ↑a

Tactic:
;

Goal state after:
n : ℕ
a b : Fin (n + 1)
i : Fin n
hl : ↑i < ↑a
hu : ↑b < ↑i + 1
⊢ ↑b < ↑a
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin n
⊢ 0 < i.castSucc ↔ 0 < i

Tactic:
simp [← val_pos_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
⊢ n - (↑i % n + 1) < n

Tactic:
;

Goal state after:
n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ n - (↑i % n + 1) < n
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : ↑t ⊆ f '' ↑s
⊢ #t ≤ #s

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : ↑t ⊆ f '' ↑s
⊢ #t ≤ #s
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n m : ℕ
i j : Fin (n + 1)
h : i ≤ j
hj : j < last n
⊢ i < last n

Tactic:
;

Goal state after:
n m : ℕ
i j : Fin (n + 1)
h : i ≤ j
hj : j < last n
⊢ i < last n
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
i : Fin (ofFn f).length
⊢ f ⟨↑i, ⋯⟩ = f (Fin.cast ⋯ i)

Tactic:
;

Goal state after:
α : Type u
n : ℕ
f : Fin n → α
i : Fin (ofFn f).length
⊢ f ⟨↑i, ⋯⟩ = f (Fin.cast ⋯ i)
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n m : ℕ
a b : Fin m
ha : ↑a < n
h : b ≤ a
⊢ a.castLT ha - b.castLT ⋯ = (a - b).castLT ⋯

Tactic:
rw [Fin.ext_iff]
  exact val_sub_castLT_of_le ha h

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

Goal state before:
pp: n : ℕ
p i : Fin (n + 1)
h : i < p
⊢ p.succAbove (i.castPred ⋯) = i

Tactic:
rw [succAbove_of_castSucc_lt _ _ (castSucc_castPred _ _ ▸ h), castSucc_castPred]

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

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

Tactic:
;

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

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

Tactic:
;

Goal state after:
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ #(s ∪ t) = #(s ∪ t) + #(s ∩ t) ↔ Disjoint s t
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
x✝ : Fin n
⊢ ↑((last n).succAbove x✝) = ↑x✝.castSucc

Tactic:
;

Goal state after:
n : ℕ
x✝ : Fin n
⊢ ↑((last n).succAbove x✝) = ↑x✝.castSucc
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case a
α : Type u_1
s t u : Finset α
inst✝ : DecidableEq α
hts : t ⊆ s
hus : u ⊆ s
hstu : t ∩ u = ∅
⊢ t ∪ u ⊆ s

Tactic:
;

Goal state after:
case a
α : Type u_1
s t u : Finset α
inst✝ : DecidableEq α
hts : t ⊆ s
hus : u ⊆ s
hstu : t ∩ u = ∅
⊢ t ∪ u ⊆ s
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
x : Fin (n + 1)
y : Fin n
⊢ x.succAbove y ≠ x

Tactic:
;

Goal state after:
n : ℕ
x : Fin (n + 1)
y : Fin n
⊢ x.succAbove y ≠ x
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
p : α → Bool
b : α
x✝ : p b = true ∧ ∃ i, f i = b ∧ ∀ (j : Fin n), j < i → ¬p (f j) = true
hpb : p b = true
i : Fin n
hfb : f i = b
h : ∀ (j : Fin n), j < i → ¬p (f j) = true
j : ℕ
hj : j < ↑i
⊢ (!p (ofFn f)[j]) = true

Tactic:
by simpa using! h ⟨j, by lia⟩ (by simpa using! hj)

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

Goal state before:
pp: α : Type u
n : ℕ
f g : Fin n → α
h : ⟨n, f⟩ = ⟨n, g⟩
⊢ f ≍ g

Tactic:
;

Goal state after:
α : Type u
n : ℕ
f g : Fin n → α
h : ⟨n, f⟩ = ⟨n, g⟩
⊢ f ≍ g
Module: Mathlib.Data.List.OfFn

Goal state before:
pp: case refl
α : Type u
n : ℕ
f : Fin n → α
⊢ f ≍ f

Tactic:
;

Goal state after:
case refl
α : Type u
n : ℕ
f : Fin n → α
⊢ f ≍ f
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:
;

Goal state after:
n : ℕ
j : Fin n
this : (succ 0).succAbove j.succ = (succAbove 0 j).succ
⊢ succAbove 1 j.succ = j.succ.succ
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 = cons x p (succ 0)

Tactic:
;

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)) = cons x p (last n).succ

Tactic:
;

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.Fintype.Basic

Goal state before:
pp: n : ℕ
a✝ : Fin n
⊢ a✝ ∈ (finRange n).toFinset ↔ a✝ ∈ univ

Tactic:
;

Goal state after:
n : ℕ
a✝ : Fin n
⊢ a✝ ∈ (finRange n).toFinset ↔ a✝ ∈ univ
Module: Mathlib.Data.Fintype.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
l : List α
f : α → β
⊢ image (fun i ↦ f l[↑i]) univ = (List.map f l).toFinset

Tactic:
by
  simp only [univ_image_def, List.ofFn_getElem_eq_map]

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

Goal state before:
pp: a : Fin 2
⊢ a = 0 ↔ a = 0

Tactic:
;

Goal state after:
a : Fin 2
⊢ a = 0 ↔ a = 0
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b

Tactic:
;

Goal state after:
α : Type u_1
s : Finset α
⊢ #s ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
a : Fin n
b : Fin (n + 1)
h : a.succ ≤ b
⊢ a.succ.predAbove b.succ = (b.pred ⋯).succ

Tactic:
predAbove_succ_of_le _ _ h,

Goal state after:
case inl
n : ℕ
a : Fin n
b : Fin (n + 1)
h : a.succ ≤ b
⊢ b = (b.pred ⋯).succ
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
inst✝ : Fintype ↑p
⊢ card ↑p = card ↑p

Tactic:
;

Goal state after:
α : Type u_1
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
inst✝ : Fintype ↑p
⊢ card ↑p = card ↑p
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ≃ β
⊢ card β = card β

Tactic:
;

Goal state after:
α : Type u_4
β : Type u_5
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ≃ β
⊢ card β = card β
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
;

Goal state after:
n : ℕ
α : Sort u_1
x : α
xs : Fin n → α
i : Fin (n + 1)
⊢ cons x xs i = (append (cons x elim0) xs ∘ Fin.cast ⋯) i
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: α : Sort u_1
m : ℕ
ys : Fin m → α
n' : ℕ
xs : Fin n' → α
⊢ append (xs ∘ Fin.cast ⋯) ys = append xs ys ∘ Fin.cast ⋯

Tactic:
;

Goal state after:
α : Sort u_1
m : ℕ
ys : Fin m → α
n' : ℕ
xs : Fin n' → α
⊢ append (xs ∘ Fin.cast ⋯) ys = append xs ys ∘ Fin.cast ⋯
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: α : Sort u_1
n : ℕ
xs : Fin n → α
m' : ℕ
ys : Fin m' → α
⊢ append xs (ys ∘ Fin.cast ⋯) = append xs ys ∘ Fin.cast ⋯

Tactic:
;

Goal state after:
α : Sort u_1
n : ℕ
xs : Fin n → α
m' : ℕ
ys : Fin m' → α
⊢ append xs (ys ∘ Fin.cast ⋯) = append xs ys ∘ Fin.cast ⋯
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)
hg : Antitone g
eq_iff : ∀ (i j : ℕ), #(g i) - 1 = #(g j) - 1 ↔ g i = g j
i j : ℕ
h : i ≤ j
⊢ #(g j) - 1 ≤ #(g i) - 1

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)
hg : Antitone g
eq_iff : ∀ (i j : ℕ), #(g i) - 1 = #(g j) - 1 ↔ g i = g j
i j : ℕ
h : i ≤ j
⊢ #(g j) - 1 ≤ #(g i) - 1
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case a
α : 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)
hg : Antitone g
eq_iff : ∀ (i j : ℕ), #(g i) - 1 = #(g j) - 1 ↔ g i = g j
i j : ℕ
h : i ≤ j
⊢ image f^[j] s ⊆ g i

Tactic:
;

Goal state after:
case a
α : 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)
hg : Antitone g
eq_iff : ∀ (i j : ℕ), #(g i) - 1 = #(g j) - 1 ↔ g i = g j
i j : ℕ
h : i ≤ j
⊢ image f^[j] s ⊆ g i
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Type u_2
f : Fin n → α
x x✝ : α
⊢ x✝ ∈ Set.range (snoc f x) ↔ x✝ ∈ insert x (Set.range f)

Tactic:
;

Goal state after:
n : ℕ
α : Type u_2
f : Fin n → α
x x✝ : α
⊢ x✝ ∈ Set.range (snoc f x) ↔ x✝ ∈ insert x (Set.range f)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
⊢ snoc (init q) (q (last n)) = q

Tactic:
ext j
  cases j using Fin.lastCases <;> simp [init]

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

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

Tactic:
;

Goal state after:
n m : ℕ
α : Sort u_2
xs : Fin n → α
x : α
ys : Fin m → α
⊢ (append xs (cons (cons x elim0 0) ys) ∘ Fin.cast ⋯) ∘ Fin.cast ⋯ = append xs (cons x ys) ∘ Fin.cast ⋯
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n m : ℕ
α : Sort u_2
xs : Fin n → α
y : α
ys : Fin m → α
⊢ append xs (cons y ys) = (append xs (cons y ys) ∘ Fin.cast ⋯) ∘ Fin.cast ⋯

Tactic:
;

Goal state after:
n m : ℕ
α : Sort u_2
xs : Fin n → α
y : α
ys : Fin m → α
⊢ append xs (cons y ys) = (append xs (cons y ys) ∘ Fin.cast ⋯) ∘ Fin.cast ⋯
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
n✝ : ℕ := card α
hn : n✝ = card α
n : ℕ
ha : n + 2 = card α
h : n + 2 ≤ 1
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Fintype α
n✝ : ℕ := card α
hn : n✝ = card α
n : ℕ
ha : n + 2 = card α
h : n + 2 ≤ 1
⊢ False
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:

Tactic:
;

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ card α ≤ 1 ↔ Subsingleton α

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Fintype α
⊢ card α ≤ 1 ↔ Subsingleton α
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_2
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
h : Injective (snoc x x₀)
⊢ ¬x₀ ∈ Set.range x

Tactic:
rintro ⟨i, hi⟩
    rw [← @snoc_last n (fun i ↦ α) x₀ x, ← @snoc_castSucc n (fun i ↦ α) x₀ x i,
      h.eq_iff] at hi
    exact ne_last_of_lt i.castSucc_lt_last hi

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

Goal state before:
pp: case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : j.castSucc < i
H₁ : i.succAbove j ≠ last n
H₂ : i.succAbove ((i.succAbove j).castPred H₁) = i.succAbove j
⊢ H₂ ▸ p ((i.succAbove j).castPred H₁) = p j

Tactic:
;

Goal state after:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : j.castSucc < i
H₁ : i.succAbove j ≠ last n
H₂ : i.succAbove ((i.succAbove j).castPred H₁) = i.succAbove j
⊢ H₂ ▸ p ((i.succAbove j).castPred H₁) = p j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : j.castSucc < i
H₁ : i.succAbove j ≠ last n
k : Fin n
hk : j = k
⊢ ∀ (H₂ : i.succAbove k = i.succAbove j), H₂ ▸ p k = p j

Tactic:
;

Goal state after:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : j.castSucc < i
H₁ : i.succAbove j ≠ last n
k : Fin n
hk : j = k
⊢ ∀ (H₂ : i.succAbove k = i.succAbove j), H₂ ▸ p k = p j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case pos.refl
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : j.castSucc < i
H₁ : i.succAbove j ≠ last n
H₂✝ : i.succAbove j = i.succAbove j
⊢ H₂✝ ▸ p j = p j

Tactic:
;

Goal state after:
case pos.refl
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : j.castSucc < i
H₁ : i.succAbove j ≠ last n
H₂✝ : i.succAbove j = i.succAbove j
⊢ H₂✝ ▸ p j = p j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : ¬j.castSucc < i
H₀ : NeZero (n + 1)
H₁ : i.succAbove j ≠ 0
H₂ : i.succAbove ((i.succAbove j).pred H₁) = i.succAbove j
⊢ H₂ ▸ p ((i.succAbove j).pred H₁) = p j

Tactic:
;

Goal state after:
case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : ¬j.castSucc < i
H₀ : NeZero (n + 1)
H₁ : i.succAbove j ≠ 0
H₂ : i.succAbove ((i.succAbove j).pred H₁) = i.succAbove j
⊢ H₂ ▸ p ((i.succAbove j).pred H₁) = p j
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
w : ∀ (s : Finset ι), #s ≤ n
⊢ Fintype ι

Tactic:
apply fintypeOfNotInfinite
  intro i
  obtain ⟨s, c⟩ := Infinite.exists_subset_card_eq ι (n + 1)
  specialize w s
  rw [c] at w
  exact Nat.not_succ_le_self n w

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

Goal state before:
pp: case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : ¬j.castSucc < i
H₀ : NeZero (n + 1)
H₁ : i.succAbove j ≠ 0
k : Fin n
hk : j = k
⊢ ∀ (H₂ : i.succAbove k = i.succAbove j), H₂ ▸ p k = p j

Tactic:
;

Goal state after:
case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : ¬j.castSucc < i
H₀ : NeZero (n + 1)
H₁ : i.succAbove j ≠ 0
k : Fin n
hk : j = k
⊢ ∀ (H₂ : i.succAbove k = i.succAbove j), H₂ ▸ p k = p j