mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
f : α → α
n : ℕ
⊢ (image f)^[n] s = image f^[n] s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → Option β
s : Finset α
f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'
⊢ ∀ (x : β), x ∈ ↑(filterMap f s f_inj) ↔ x ∈ {b | ∃ a ∈ s, f a = some b}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
s' s t : Finset α
f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'
⊢ ∀ (a a' b : α), b ∈ some a → b ∈ some a' → a = a'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
x✝ : α
⊢ x✝ ∈ filterMap some s ⋯ ↔ x✝ ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → Option β
s t : Finset α
f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'
h : s ⊆ t
⊢ filterMap f s f_inj ⊆ filterMap f t f_inj

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → Option β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f_inj : ∀ (a a' : α) (b : β), f a = some b → f a' = some b → a = a'
s : List α
⊢ (List.filterMap f s).toFinset = filterMap f s.toFinset f_inj

Tactic:
by

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type ?u.18
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
x : ↥(filter p s)
⊢ p ↑x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
a : α
ha : p a
⊢ ⟨a, ha⟩ ∈ Finset.subtype p s ↔ ↑⟨a, ha⟩ ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
⊢ Finset.subtype p s = ∅ ↔ ∀ (x : α), p x → x ∉ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
⊢ map (Embedding.subtype p) (Finset.subtype p s) = filter p s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
h : ∀ x ∈ s, p x
⊢ ∀ (a : α), a ∈ map (Embedding.subtype p) (Finset.subtype p s) ↔ a ∈ s

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Prop
s : Finset { x // p x }
a : α
h : a ∈ map (Embedding.subtype fun x ↦ p x) s
⊢ p a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
t : Set α
s : Finset ↑t
⊢ ↑(map (Embedding.subtype fun x ↦ x ∈ t) s) ⊆ t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
⊢ ↑t ⊆ f '' s ↔ ∃ s', ↑s' ⊆ s ∧ image f s' = t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
⊢ t ⊆ image f s ↔ ∃ s' ⊆ s, image f s' = t

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
f : α → β
⊢ t ⊆ image f univ ↔ ∃ s', image f s' = t

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ range (n + 1) \ {0} = image Nat.succ (range n)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
s : Finset α
⊢ (fun s ↦ Finset.map e.symm.toEmbedding s) ((fun s ↦ Finset.map e.toEmbedding s) s) = s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
s : Finset β
⊢ (fun s ↦ Finset.map e.toEmbedding s) ((fun s ↦ Finset.map e.symm.toEmbedding s) s) = s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ (Equiv.refl α).finsetCongr = Equiv.refl (Finset α)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
e' : β ≃ γ
⊢ e.finsetCongr.trans e'.finsetCongr = (e.trans e').finsetCongr

Tactic:
by

Goal state after:
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 }
⊢ (fun s ↦ Finset.map (Subtype.impEmbedding (Membership.mem ↑s) p ⋯) (↑s).attach)
      ((fun s ↦ ⟨Finset.map { toFun := fun a ↦ ↑a, inj' := ⋯ } s, ⋯⟩) s) =
    s

Tactic:
by

Goal state after:
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 }
⊢ (fun s ↦ ⟨Finset.map { toFun := fun a ↦ ↑a, inj' := ⋯ } s, ⋯⟩)
      ((fun s ↦ Finset.map (Subtype.impEmbedding (Membership.mem ↑s) p ⋯) (↑s).attach) s) =
    s

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ i.rev = j ↔ i = j.rev

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ i.rev < j ↔ j.rev < i

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ i.rev ≤ j ↔ j.rev ≤ i

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ i < j.rev ↔ j < i.rev

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ i ≤ j.rev ↔ j ≤ i.rev

Tactic:
by

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

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

Tactic:
by

Goal state after:
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

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p.succAbove i.rev = (p.rev.succAbove i).rev

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ (p.succAbove i).rev = p.rev.succAbove i.rev

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : Fin n
i : Fin (n + 1)
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : Fin n
i : Fin (n + 1)
⊢ p.predAbove i.rev = (p.rev.predAbove i).rev

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : Fin n
i : Fin (n + 1)
⊢ (p.predAbove i).rev = p.rev.predAbove i.rev

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n m : ℕ
⊢ Nonempty (Fin n ↪ Fin m) ↔ n ≤ m

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n m : ℕ
p : Fin (n + 1)
hmn : n ≤ m
⊢ n + (m - n) = m

Tactic:
by

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
⊢ y ∈ {i | m ≤ ↑i + n}

Tactic:
by

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

Goal state before:
pp: n m : ℕ
hmn : n ≤ m
y : Fin m
xin : y ∈ {i | m ≤ ↑i + n}
⊢ ((addNatEmb (m - n)).trans (finCongr ⋯).toEmbedding) (subNat (m - n) (Fin.cast ⋯ y) ⋯) = y

Tactic:
by

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

Goal state before:
pp: n m : ℕ
hmn : n ≤ m
⊢ Set.range ⇑(natAdd_castLEEmb hmn) = {i | m - n ≤ ↑i}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ Monotone card

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
⊢ #({a} ∩ s) ≤ 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∉ s
⊢ #(insert a s) = #s + 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
h : a ∈ s
⊢ #(insert a s) = #s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ #(insert a s) ≤ #s + 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
⊢ #(insert a s) = if a ∈ s then #s else #s + 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a b : α
inst✝ : DecidableEq α
⊢ #{a, b} = 1 ∨ #{a, b} = 2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a b : α
inst✝ : DecidableEq α
⊢ #{a, b} = 2 ↔ a ≠ b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
a b c : α
inst✝ : DecidableEq α
⊢ #{a, b, c} = 3 ↔ a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
inst✝ : DecidableEq α
⊢ #s - 1 ≤ #(s.erase a)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
l : List α
P : α → Prop
inst✝ : DecidablePred P
h : l.Nodup
⊢ #(Finset.filter P l.toFinset) = countP (fun b ↦ decide (P b)) l

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
⊢ #(image f s) ≤ #s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : Set.InjOn f ↑s
⊢ #(image f s) = #s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
⊢ (Multiset.map f s.val).dedup = Multiset.map f s.val

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : #(image f s) = #s
⊢ Set.InjOn f ↑s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
y : β
⊢ #({x ∈ s | f x = y}) ≠ 0 ↔ y ∈ image f s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
H : ∀ s' ≤ s.val, n < s'.card → ∃ a ∈ s', ¬P a
s' : Finset α
hs' : s' ⊆ s
h : n < #s'
⊢ s'.val ≤ s.val

Tactic:
by

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
⊢ #(Finset.subtype p s) = #(filter p s)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
⊢ #(filter p s) = #s ↔ ∀ x ∈ s, p x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
⊢ #(filter p s) = 0 ↔ ∀ x ∈ s, ¬p x

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ (last n).rev = ⊥

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ ⊤.succ = ⊤

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ 0 = ⊤ ↔ n = 1

Tactic:
by

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

Goal state before:
pp: m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
h : m = n
⊢ Fin.cast h ⊤ = ⊤

Tactic:
by

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
a : α
x✝ : a ∈ s ↔ ∃ i, ∃ (hi : i ∈ range n), f i ⋯ = a
⊢ a ∈ s ↔ a ∈ image (fun i ↦ f ↑i ⋯) (range n).attach

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n a : ℕ
ha : a < n + 2
⊢ 1 = ⟨a, ha⟩ ↔ a = 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Fin (n + 1)
⊢ a < last n ↔ a ≠ last n

Tactic:
by

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
hb : b ≠ last n
hab : a ≤ b
⊢ a ≠ last n

Tactic:
by

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

Goal state before:
pp: n m : ℕ
a b : Fin n
ha : ↑a < m
hab : b ≤ a
⊢ ↑(a - b) < m

Tactic:
by

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
hab : b ≤ a
⊢ a - b ≠ last n

Tactic:
by

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

Goal state before:
pp: α : Sort u_1
k l : ℕ
h : k = l
f : Fin k → α
g : Fin l → α
⊢ f ≍ g ↔ ∀ (i : Fin k), f i = g ⟨↑i, ⋯⟩

Tactic:
by

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

Goal state before:
pp: α : Sort u_1
k l k' l' : ℕ
h : k = l
h' : k' = l'
f : Fin k → Fin k' → α
g : Fin l → Fin l' → α
⊢ f ≍ g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩

Tactic:
by

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

Goal state before:
pp: k l : ℕ
h : k = l
i : Fin k
j : Fin l
⊢ i ≍ j ↔ ↑i = ↑j

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ min (↑a) n = ↑a

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ max (↑a) n = n

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : Fin n
⊢ 0 < ↑a ↔ 0 < a

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
⊢ p.predAbove a ≤ p.predAbove b

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : Fin n
⊢ 0 < a ↔ a ≠ 0

Tactic:
by

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

Goal state before:
pp: k l : ℕ
inst✝¹ : NeZero k
inst✝ : NeZero l
h : k = l
x : Fin k
⊢ Fin.cast h x = 0 ↔ x = 0

Tactic:
by

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

Goal state before:
pp: k l : ℕ
h : k = l
a b : Fin k
hab : Fin.cast h a = Fin.cast h b
⊢ a = b

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ 1 < last (n + 1)

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
⊢ (fun p ↦ p.predAbove i) a ≤ (fun p ↦ p.predAbove i) b

Tactic:
by

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

Goal state before:
pp: n : ℕ
u v : Fin n
⊢ ↑↑(u - v) = if v ≤ u then ↑↑u - ↑↑v else ↑↑u - ↑↑v + ↑n

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
h : i < j
hij : i = j.predAbove i.succ
⊢ i.succ ≤ j.castSucc

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ Injective predAbove

Tactic:
by

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

Goal state before:
pp: m n : ℕ
p : Fin (n + 1)
i j : Fin n
⊢ Monotone ⇑equivSubtype

Tactic:
by

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

Goal state before:
pp: m n : ℕ
p : Fin (n + 1)
i j : Fin n
⊢ Monotone ⇑equivSubtype.symm

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ range ⇑i.succAboveOrderEmb = {i}ᶜ

Tactic:
by

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

Goal state before:
pp: n : ℕ
u v : Fin n
⊢ ↑↑(u - v) = (↑↑u - ↑↑v) % ↑n

Tactic:
by

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
⊢ s = image (fun i ↦ f ↑i ⋯) (range n).attach

Tactic:
by

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

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

Goal state before:
pp: m n : ℕ
e : Fin n ≃o Fin m
i : Fin n
⊢ ↑(e i) = ↑i

Tactic:
by

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

Goal state before:
pp: n : ℕ
u v : Fin n
⊢ ↑↑(u + v) = if ↑u + ↑v < n then ↑↑u + ↑↑v else ↑↑u + ↑↑v - ↑n

Tactic:
by

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

Goal state before:
pp: n : ℕ
u v : Fin n
⊢ ↑↑(u + v) = (↑↑u + ↑↑v) % ↑n

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ Nontrivial (Fin n) ↔ 2 ≤ n

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin n
h : 2 < n
⊢ n ≠ 0

Tactic:
by

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
⊢ #s = n

Tactic:
by

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

Goal state before:
pp: n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
h1 : 1 ≠ i ∧ 1 ≠ j
⊢ 1 < n

Tactic:
by

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

Goal state before:
pp: n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
h1 : ¬(1 ≠ i ∧ 1 ≠ j)
⊢ 2 < n

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin n
h : 2 < n
⊢ ∃ k, k ≠ i ∧ k ≠ j

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ ↑(a + b) = if n ≤ ↑a + ↑b then ↑a + ↑b - n else ↑a + ↑b

Tactic:
by

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

Goal state before:
pp: n : ℕ
a b : Fin n
huv : ↑a + ↑b < n
⊢ ↑(a + b) = ↑a + ↑b

Tactic:
by

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

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ ↑↑(a - b) = ↑↑a - ↑↑b + ↑(if b ≤ a then 0 else n)

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin n
hij : i ≤ j
⊢ ↑(j - i) < n - ↑i

Tactic:
by

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

Goal state before:
pp: n✝ m n : ℕ
i j : Fin n
hij : i < j
⊢ n - ↑i ≠ 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin n
hij : i < j
⊢ (j - i).castLT ⋯ ≠ 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
k : Fin n
⊢ k ≠ 0 → 1 ≤ k

Tactic:
by

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

Goal state before:
pp: α : 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
⊢ ⟨a, ha⟩ ∈ s.attach ∧ i ↑⟨a, ha⟩ ⋯ = i a ha

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ succ 1 = 2

Tactic:
by

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

Goal state before:
pp: n a b : ℕ
han : a ≤ n
hbn : b ≤ n
⊢ ↑a ≤ ↑b ↔ a ≤ b

Tactic:
by

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

Goal state before:
pp: α : 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
⊢ #s = #t

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after: