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

Goal state before:
pp: m n : ℕ
α✝ : Fin (n + 1) → Sort u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ i.succ
i : Fin n
y : α✝ i.succ
z : α✝ 0
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
⊢ m = m

Tactic:
]

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

Goal state before:
pp: case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ a t, a ∉ t ∧ insert a t = s ∧ #t = 2) → ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
]

Goal state after:
case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ a t, a ∉ t ∧ insert a t = s ∧ #t = 2) → ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_1
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
l : Fin m
⊢ u l = u (Fin.cast ⋯ (castAdd n l))

Tactic:
]

Goal state after:
case refine_1
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
l : Fin m
⊢ u l = u (Fin.cast ⋯ (castAdd n l))
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ a t, a ∉ t ∧ insert a t = s ∧ #t = 3) → ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

Tactic:
]

Goal state after:
case mp
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ a t, a ∉ t ∧ insert a t = s ∧ #t = 3) → ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
p : α → Prop
s : Finset α
H : ∀ (x : α), x ∈ s ↔ p x
inst✝ : Fintype { x // p x }
⊢ card { x // p x } = card { x // p x }

Tactic:
]

Goal state after:
α : Type u_1
p : α → Prop
s : Finset α
H : ∀ (x : α), x ∈ s ↔ p x
inst✝ : Fintype { x // p x }
⊢ card { x // p x } = card { x // p x }
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.Fintype.Card

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
s : Finset α
hs : #s = Fintype.card α
⊢ Fintype.card α ≤ Fintype.card α

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
S₁ S₂ : Finset ι
h : Disjoint S₁ S₂
h' : #S₁ + #S₂ = #univ
⊢ Disjoint S₁ S₂

Tactic:
]

Goal state after:
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
S₁ S₂ : Finset ι
h : Disjoint S₁ S₂
h' : #S₁ + #S₂ = #univ
⊢ Disjoint S₁ S₂
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
α✝ : Fin (n + 1) → Sort u
x : α✝ 0
q : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ i.succ
i : Fin n
y : α✝ i.succ
z : α✝ 0
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
⊢ n = n

Tactic:
]

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

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ j = j

pp: case inl.h
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ j.castSucc ≤ (i.pred ⋯).castSucc

Tactic:
]

Goal state after:
case inl.h
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ j.castSucc ≤ (i.pred ⋯).castSucc
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑sᶜ
⊢ #s.toFinsetᶜ = #s.toFinsetᶜ

Tactic:
]

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

Goal state before:
pp: case refine_2
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ v r = v (Fin.cast ⋯ (natAdd m r))

Tactic:
]

Goal state after:
case refine_2
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ v r = v (Fin.cast ⋯ (natAdd m r))
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl.h
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ j.castSucc < i

Tactic:
]

Goal state after:
case inl.h
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ j.castSucc < i
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
⊢ append (append a b) c i = append a (append b c) (Fin.cast ⋯ i)

Tactic:
]

Goal state after:
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
⊢ append (append a b) c i = append a (append b c) (Fin.cast ⋯ i)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_1
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
⊢ append a b l = append a (append b c) (Fin.cast ⋯ (castAdd p l))

Tactic:
]

Goal state after:
case refine_1
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
⊢ append a b l = append a (append b c) (Fin.cast ⋯ (castAdd p l))
Module: Mathlib.Data.Fin.SuccPred

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

pp: case inr.h
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ (i.castPred ⋯).castSucc < j.succ

Tactic:
]

Goal state after:
case inr.h
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ (i.castPred ⋯).castSucc < j.succ
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_4
inst✝ : Finite α
val✝ : Fintype α
l : List α
e : ⟦l⟧ = univ.val
this✝ : univ.val.Nodup ∧ ∀ (x : α), x ∈ univ.val
this : Multiset.Nodup ⟦l⟧ ∧ ∀ (x : α), x ∈ ⟦l⟧
⊢ List.Nodup ?m.54 ∧ ∀ (x : α), x ∈ ?m.54

Tactic:
]

Goal state after:
α : Type u_4
inst✝ : Finite α
val✝ : Fintype α
l : List α
e : ⟦l⟧ = univ.val
this✝ : univ.val.Nodup ∧ ∀ (x : α), x ∈ univ.val
this : Multiset.Nodup ⟦l⟧ ∧ ∀ (x : α), x ∈ ⟦l⟧
⊢ List.Nodup ?m.54 ∧ ∀ (x : α), x ∈ ?m.54
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr.h
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ i ≤ j.castSucc

Tactic:
]

Goal state after:
case inr.h
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ i ≤ j.castSucc
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_1.refine_1
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
ll : Fin m
⊢ a ll = append a (append b c) (Fin.cast ⋯ (castAdd p (castAdd n ll)))

Tactic:
]

Goal state after:
case refine_1.refine_1
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
ll : Fin m
⊢ a ll = append a (append b c) (Fin.cast ⋯ (castAdd p (castAdd n ll)))
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ i = i

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → β
h : Injective f
b : β
w : b ∉ Set.range f
⊢ b ∉ Set.range ⇑{ toFun := f, inj' := h }

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → β
h : Injective f
b : β
w : b ∉ Set.range f
⊢ b ∉ Set.range ⇑{ toFun := f, inj' := h }
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_1.refine_2
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
lr : Fin n
⊢ b lr = append a (append b c) (Fin.cast ⋯ (castAdd p (natAdd m lr)))

Tactic:
]

Goal state after:
case refine_1.refine_2
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
lr : Fin n
⊢ b lr = append a (append b c) (Fin.cast ⋯ (castAdd p (natAdd m lr)))
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_2
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
r : Fin p
⊢ c r = append a (append b c) (Fin.cast ⋯ (natAdd (m + n) r))

Tactic:
]

Goal state after:
case refine_2
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
r : Fin p
⊢ c r = append a (append b c) (Fin.cast ⋯ (natAdd (m + n) r))
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ IsEmpty α ↔ IsEmpty α

Tactic:
]

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

Goal state before:
pp: α : Type u_4
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ (∃! a, p a) ↔ ∃ a, {x | p x} = {a}

Tactic:
]

Goal state after:
α : Type u_4
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ (∃! a, p a) ↔ ∃ a, {x | p x} = {a}
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_1
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin 1
⊢ cons (x₀ 0) x (Fin.cast ⋯ (castAdd n 0)) = x₀ 0

Tactic:
]

Goal state after:
case refine_1
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin 1
⊢ cons (x₀ 0) x (Fin.cast ⋯ (castAdd n 0)) = x₀ 0
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
⊢ cons (x₀ 0) x i.succ = x i

Tactic:
]

Goal state after:
case refine_2
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin n
⊢ cons (x₀ 0) x i.succ = x i
Module: Mathlib.Data.Fintype.Card

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

Tactic:
by simpa using exists_subsuperset_card_eq s.subset_univ hsn hnα

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

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

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
p : α → Prop
inst✝ : Fintype { a // p a }
x : α
hx : ¬p x
⊢ x ∉ {x | p x}

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
p : α → Prop
inst✝ : Fintype { a // p a }
x : α
hx : ¬p x
⊢ x ∉ {x | p x}
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m✝ n✝ : ℕ
α✝ : Fin (n✝ + 1) → Sort u
x : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ i.succ
i : Fin n✝
y : α✝ i.succ
z : α✝ 0
α : Sort u_1
n m : ℕ
xs : Fin n → α
ys : Fin m → α
n' : ℕ
h : n' = n
⊢ n + m = n + m

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ card α - #{x | p x}.toFinset = card α - #?s

pp: case s
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ Finset α

pp: case H
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ ∀ (x : α), x ∈ ?s ↔ p x

pp: case H
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ ∀ (x : α), x ∈ {x | p x}ᶜ.toFinset ↔ ¬p x

Tactic:
]

Goal state after:
case H
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ ∀ (x : α), x ∈ {x | p x}.toFinset ↔ p x

case H
α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : Fintype { x // p x }
inst✝ : Fintype { x // ¬p x }
⊢ ∀ (x : α), x ∈ {x | p x}ᶜ.toFinset ↔ ¬p x
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m✝ n✝ : ℕ
α✝ : Fin (n✝ + 1) → Sort u
x : α✝ 0
q : (i : Fin (n✝ + 1)) → α✝ i
p : (i : Fin n✝) → α✝ i.succ
i : Fin n✝
y : α✝ i.succ
z : α✝ 0
α : Sort u_1
n m : ℕ
xs : Fin n → α
ys : Fin m → α
m' : ℕ
h : m' = m
⊢ n + m = n + m

Tactic:
]

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

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

Tactic:
]

Goal state after:
α : Sort u_1
m n : ℕ
xs : Fin m → α
ys : Fin n → α
i : Fin (m + n)
⊢ append xs ys i = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ i.rev)
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
p : Finset α → Sort u_4
H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s
s : Finset α
⊢ (H s fun t h ↦
      have this := ⋯;
      strongInduction H t) =
    H s fun t x ↦ strongInduction H t

Tactic:
]

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

Goal state before:
pp: α : Type u_1
p : Finset α → Sort u_4
s : Finset α
H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s
⊢ (H s fun t h ↦
      have this := ⋯;
      strongInduction H t) =
    H s fun t x ↦ strongInduction H t

Tactic:
]

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

Goal state before:
pp: case cons_cons
α : Type u_1
l : List α
x : α
l' l₁✝ l₂✝ : List α
y : α
h : l₁✝ <+ l₂✝
IH : x ∈+ l₁✝ → x ∈+ l₂✝
hx : y = x ∧ x ∈ l₁✝ ∨ x ∈+ l₁✝
⊢ y = x ∧ x ∈ l₂✝ ∨ x ∈+ l₂✝

Tactic:
]

Goal state after:
case cons_cons
α : Type u_1
l : List α
x : α
l' l₁✝ l₂✝ : List α
y : α
h : l₁✝ <+ l₂✝
IH : x ∈+ l₁✝ → x ∈+ l₂✝
hx : y = x ∧ x ∈ l₁✝ ∨ x ∈+ l₁✝
⊢ y = x ∧ x ∈ l₂✝ ∨ x ∈+ l₂✝
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
α : Sort u_1
xs : Fin m → α
ys : Fin n → α
finSumFinEquiv : Fin m ⊕ Fin n ≃ Fin (m + n) :=
  { toFun := Sum.elim (castAdd n) (natAdd m), invFun := fun i ↦ addCases Sum.inl Sum.inr i, left_inv := ⋯,
    right_inv := ⋯ }
⊢ Injective (append xs ys ∘ Sum.elim (castAdd n) (natAdd m)) ↔
    Injective (append xs ys ∘ Sum.elim (castAdd n) (natAdd m))

Tactic:
]

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

Goal state before:
pp: n : ℕ
α : Sort u_1
a : Fin n → α
h : 1 * n = n
⊢ ∀ (x : Fin n), «repeat» 1 a (Fin.cast ⋯ x) = (a ∘ Fin.cast h) (Fin.cast ⋯ x)

Tactic:
]

Goal state after:
n : ℕ
α : Sort u_1
a : Fin n → α
h : 1 * n = n
⊢ ∀ (x : Fin n), «repeat» 1 a (Fin.cast ⋯ x) = (a ∘ Fin.cast h) (Fin.cast ⋯ x)
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: case neg
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
⊢ [x, x] <+ l ↔ [x, x] <+ y :: l

Tactic:
]

Goal state after:
case neg
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
⊢ [x, x] <+ l ↔ [x, x] <+ y :: l
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
n : ℕ
p : Finset α → Sort u_4
H : (t₁ : Finset α) → ({t₂ : Finset α} → #t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → #t₁ ≤ n → p t₁
s : Finset α
⊢ (H s fun {t} ht h ↦
      have this := ⋯;
      have this := ⋯;
      strongDownwardInduction H t ht) =
    H s fun {t} ht x ↦ strongDownwardInduction H t ht

Tactic:
]

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

Goal state before:
pp: n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
h : m.succ * n = n + m * n
⊢ ∀ (x : Fin (n + m * n)), «repeat» m.succ a (Fin.cast ⋯ x) = (append a («repeat» m a) ∘ Fin.cast h) (Fin.cast ⋯ x)

Tactic:
]

Goal state after:
n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
h : m.succ * n = n + m * n
⊢ ∀ (x : Fin (n + m * n)), «repeat» m.succ a (Fin.cast ⋯ x) = (append a («repeat» m a) ∘ Fin.cast h) (Fin.cast ⋯ x)
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
n : ℕ
p : Finset α → Sort u_4
s : Finset α
H : (t₁ : Finset α) → ({t₂ : Finset α} → #t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → #t₁ ≤ n → p t₁
⊢ (fun a ↦
      H s
        (fun {t} ht h ↦
          have this := ⋯;
          have this := ⋯;
          strongDownwardInduction H t ht)
        a) =
    H s fun {t} ht x ↦ strongDownwardInduction H t ht

Tactic:
]

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

Goal state before:
pp: case h.inr
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α], card α = m → P α
α : Type u_4
inst✝¹ : Fintype α
hn : card α = n
hnontriv : Nontrivial α
β : Type u_4
inst✝ : Fintype β
hlt : card β < n
⊢ P β

Tactic:
]

Goal state after:
case h.inr
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α], card α = m → P α
α : Type u_4
inst✝¹ : Fintype α
hn : card α = n
hnontriv : Nontrivial α
β : Type u_4
inst✝ : Fintype β
hlt : card β < n
⊢ P β
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Sort u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
⊢ ∀ (x : Fin (m₁ * n + m₂ * n)),
    «repeat» (m₁ + m₂) a (Fin.cast ⋯ x) = (append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h) (Fin.cast ⋯ x)

Tactic:
]

Goal state after:
n : ℕ
α : Sort u_1
a : Fin n → α
m₁ m₂ : ℕ
h : (m₁ + m₂) * n = m₁ * n + m₂ * n
⊢ ∀ (x : Fin (m₁ * n + m₂ * n)),
    «repeat» (m₁ + m₂) a (Fin.cast ⋯ x) = (append («repeat» m₁ a) («repeat» m₂ a) ∘ Fin.cast h) (Fin.cast ⋯ x)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
α : Fin (n + 1) → Sort u_1
x✝ : α (last n)
q : (i : Fin (n + 1)) → α i
p✝ : (i : Fin n) → α i.castSucc
i✝ : Fin n
y : α i✝.castSucc
z : α (last n)
p : (i : Fin n) → α i.castSucc
x : α (last n)
i : Fin (n + 1)
h : ↑i < n
⊢ α i = α i

Tactic:
]

Goal state after:
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 : ℕ
⊢ image f^[i] s ⊆ image f^[i] s

Tactic:
]

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

Goal state before:
pp: m n : ℕ
α : Fin (n + 1) → Sort u_1
x✝ : α (last n)
q : (i : Fin (n + 1)) → α i
p✝ : (i : Fin n) → α i.castSucc
i✝ : Fin n
y : α i✝.castSucc
z : α (last n)
p : (i : Fin n) → α i.castSucc
x : α (last n)
i : Fin (n + 1)
h : ¬↑i < n
⊢ α (last n) = α (last n)

Tactic:
]

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

Goal state before:
pp: n : ℕ
α : Sort u_2
a : α
f : Fin n → α
i : Fin n
⊢ f i = f i

Tactic:
]

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

Goal state before:
pp: case refine_1
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i : Fin (n + 1)
⊢ a = a

Tactic:
]

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

Goal state before:
pp: case refine_2
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i✝ : Fin (n + 1)
i : Fin n
⊢ f (natAdd m i) = f (natAdd m i)

Tactic:
]

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

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

Tactic:
]

Goal state after:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
j : Fin n
h : j = i
⊢ init (update q i.castSucc y) i = update (init q) i y i
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case succ.cast
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
j : Fin n
⊢ snoc q b j.castSucc = snoc (cons a q) b j.castSucc.succ

Tactic:
]

Goal state after:
case succ.cast
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
j : Fin n
⊢ snoc q b j.castSucc = snoc (cons a q) b j.castSucc.succ
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case neg
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
h : ¬↑j < n
⊢ (g ∘ snoc q y) (last n) = snoc (g ∘ q) (g y) (last n)

Tactic:
]

Goal state after:
case neg
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
h : ¬↑j < n
⊢ (g ∘ snoc q y) (last n) = snoc (g ∘ q) (g y) (last n)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_1
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin n
⊢ x i = snoc x (x₀ 0) (castAdd 1 i)

Tactic:
]

Goal state after:
case refine_1
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin n
⊢ x i = snoc x (x₀ 0) (castAdd 1 i)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_2
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin 1
⊢ x₀ 0 = snoc x (x₀ 0) (natAdd n 0)

Tactic:
]

Goal state after:
case refine_2
α : Sort u_2
n : ℕ
x : Fin n → α
x₀ : Fin 1 → α
i : Fin 1
⊢ x₀ 0 = snoc x (x₀ 0) (natAdd n 0)
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.List.NodupEquivFin

Goal state before:
pp: case cons
α : 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]?
this : ∃ h, l'[f 0] = hd
⊢ hd :: tl <+ l'

Tactic:
]

Goal state after:
case cons
α : 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]?
this : ∃ h, l'[f 0] = hd
⊢ hd :: tl <+ l'
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 : ℕ
⊢ a ≤ b ↔ a ≤ b

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 + 1 ≤ f (b + 1)

Tactic:
]

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 : ℕ
⊢ f 0 + 1 ≤ f (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
a b : ℕ
⊢ 0 < b + 1

Tactic:
]

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.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
α : Fin (n + 1) → Sort u_1
x✝ : α (last n)
q : (i : Fin (n + 1)) → α i
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
z : α (last n)
motive : ((i : Fin n.succ) → α i) → Sort u_2
snoc : (xs : (i : Fin n) → α i.castSucc) → (x : α (last n)) → motive (Fin.snoc xs x)
x : (i : Fin n.succ) → α i
⊢ motive x = motive x

Tactic:
]

Goal state after: