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

Goal state before:
pp: n m : ℕ
a b : Fin m
⊢ castAdd n a = castAdd n b ↔ a = b

Tactic:
by

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

Goal state before:
pp: m n : ℕ
inst✝ : NeZero m
h : m ≤ n
a : ℕ
⊢ castLE h ↑a = ↑(a % m)

Tactic:
by

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

Goal state before:
pp: n k : ℕ
h : n ≤ k
i : Fin k
hi : i ∈ Set.range (castLE h)
⊢ ↑((Equiv.ofInjective (castLE h) ⋯).symm ⟨i, hi⟩) = ↑i

Tactic:
by

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

Goal state before:
pp: n m : ℕ
eq : n = m
a b : Fin n
⊢ Fin.cast eq a = Fin.cast eq b ↔ a = b

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n m : ℕ
h : n = m
⊢ Fin.cast h = cast ⋯

Tactic:
by

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
⊢ (m * n - (↑i + 1)) % n = (m * n - (↑i / n * n + ↑i % n + 1)) % n

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ a.castSucc < b.succ ↔ 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 → β
j : (a : β) → a ∈ t → α
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : β) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : β) (ha : a ∈ t), i (j a ha) ⋯ = a
⊢ #s = #t

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ i.castSucc < p ∨ p < i.succ

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 : α → β
hi : Set.MapsTo i ↑s ↑t
i_inj : Set.InjOn i ↑s
i_surj : Set.SurjOn i ↑s ↑t
⊢ ∀ b ∈ t, ∃ a, ∃ (_ : a ∈ s), i a = b

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ i.succ ≤ p ∨ p ≤ i.castSucc

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
p i : Fin n
h : p < i
⊢ i.castSucc ≠ 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
p i : Fin n
h : i < p
⊢ i.succ ≠ last n

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ ↑↑a = a.castSucc

Tactic:
by

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

Goal state before:
pp: n : ℕ
j k : Fin n
⊢ ↑↑j < ↑↑k ↔ j < k

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ n ≤ n + 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin n.succ
hi : i ∈ Set.range castSucc
⊢ ↑((Equiv.ofInjective castSucc ⋯).symm ⟨i, hi⟩) = ↑i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
e : α ≃ β
hst : ∀ (i : α), i ∈ s ↔ e i ∈ t
⊢ #s = #t

Tactic:
by

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
⊢ (m * n - (↑i / n * n + ↑i % n + 1)) % n = ((m - ↑i / n - 1) * n + (n - (↑i % n + 1))) % n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
f_inj : Set.InjOn f ↑s
⊢ #s ≤ #t

Tactic:
by

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

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ (castAdd m i).succ = if h : i.succ = last n then natAdd n 0 else castAdd (m + 1) ⟨↑i + 1, ⋯⟩

Tactic:
by

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

Goal state before:
pp: m n : ℕ
a b : Fin n
h : b ≤ a
⊢ castAdd m a - castAdd m b = castAdd m (a - b)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ i.pred hi < j ↔ i < j.succ

Tactic:
by

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

Goal state before:
pp: n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ j < i.pred hi ↔ j.succ < i

Tactic:
by

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

Goal state before:
pp: n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ i.pred hi ≤ j ↔ i ≤ j.succ

Tactic:
by

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
⊢ ((m - ↑i / n - 1) * n + (n - (↑i % n + 1))) % n = n - (↑i % n + 1)

Tactic:
by

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

Goal state before:
pp: n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ j ≤ i.pred hi ↔ j.succ ≤ i

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Fin (n + 1)
ha : a ≠ 0
⊢ (a.pred ha).castSucc + 1 = a

Tactic:
by

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a.castSucc ≠ 0
⊢ b ≤ a.castSucc.pred ha ↔ b < a

Tactic:
by

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

Goal state before:
pp: n : ℕ
motive : Fin n → Prop
h : ∀ (j : Fin n), (∀ (k : Fin n), k < j → motive k) → motive j
i : Fin n
⊢ motive i

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
⊢ #s ≤ #t

Tactic:
by

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a.castSucc ≠ 0
⊢ a.castSucc.pred ha < 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 β
f : α → β
hf : Set.SurjOn f ↑s ↑t
⊢ #t ≤ #s

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Fin (n + 1)
ha : a.castSucc ≠ 0
⊢ a.castSucc.pred ha < a

Tactic:
by

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a ≠ 0
⊢ b ≤ (a.pred ha).castSucc ↔ b < a

Tactic:
by

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a ≠ 0
⊢ (a.pred ha).castSucc < b ↔ a ≤ b

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Fin (n + 1)
ha : a ≠ 0
⊢ (a.pred ha).castSucc < a

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : Set.MapsTo f ↑s ↑t
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
f : ℕ → α
hf : ∀ i < n, f i ∈ s
f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j
⊢ Set.MapsTo f ↑(range n) ↑s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
f : ℕ → α
hf : ∀ i < n, f i ∈ s
f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j
⊢ Set.InjOn f ↑(range n)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
⊢ ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f ↔ ∀ (i : Fin n), r (f i.castSucc) (f i.succ)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : #t ≤ #s
f' : ↥s → β := fun a ↦ f ↑a ⋯
hinj' : Set.InjOn f' ↑s.attach
hmapsto' : Set.MapsTo f' ↑s.attach ↑t
b : β
hb : b ∈ t
⊢ #t ≤ #s.attach

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: i : Fin 2
hi : i ≠ 0
⊢ i = 1

Tactic:
by

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

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

Tactic:
← castSucc_le_castSucc_iff,

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : #t ≤ #s
⊢ ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), b = f a ha

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
← castSucc_le_castSucc_iff,

Goal state after:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
⊢ j.castSucc ≤ (i.castPred hi).castSucc ↔ j.castSucc ≤ i
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
h : a < b
⊢ a + 1 ≤ b

Tactic:
by

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

Goal state before:
pp: n : ℕ
a b : Fin n
h : a ≤ b
k : ℕ
hk : ↑b = ↑a + k
⊢ k ≤ ↑b

Tactic:
by

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

Goal state before:
pp: n : ℕ
a b : Fin n
h : a ≤ b
⊢ ∃ k, k ≤ b ∧ b = a + k

Tactic:
by

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

Goal state before:
pp: n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
k : ℕ
hk : ↑b = ↑a + k + 1
⊢ k < ↑b

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n✝ : ℕ
a b : Fin (n✝ + 1 + 1)
h : a < b
k : ℕ
hk : ↑b = ↑a + k + 1
hkb : k < ↑b
⊢ ⟨k, ⋯⟩ + 1 ≤ b

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
h : i ≠ last n
⊢ i.castPred h = 0 ↔ i = 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
h : a < b
⊢ ∃ k, k < b ∧ k + 1 ≤ b ∧ b = a + k + 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
u v : Fin (n + 2)
h : u < v
⊢ v - (u + 1) < v - u

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin n
h : ↑i + 1 < n
⊢ ↑i + 1 < n

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ castPred 1 ⋯ = 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n m : ℕ
inst✝¹ : NeZero n
inst✝ : NeZero (OfNat.ofNat m)
this : m % (n + m) = m
⊢ NeZero (OfNat.ofNat m)

Tactic:
by

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

Goal state before:
pp: n m : ℕ
inst✝¹ : NeZero n
inst✝ : NeZero (OfNat.ofNat m)
⊢ NeZero (OfNat.ofNat m)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : #s ≤ #t
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
f' : ↥s → β := fun a ↦ f ↑a ⋯
x : β
hx : x ∈ ↑t
⊢ x ∈ f' '' ↑s.attach

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
i : Fin (ofFn f).length
⊢ (ofFn f).length = n

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by
  subst h
  simp_rw [Fin.cast_refl, id]

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n.succ → α
⊢ ofFn f = (ofFn fun i ↦ f i.castSucc).concat (f (Fin.last n))

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
m n : ℕ
f : Fin (m * n) → α
i : Fin m
j : Fin n
⊢ ↑i * n + n = (↑i + 1) * n

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : #s ≤ #t
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
f' : ↥s → β := fun a ↦ f ↑a ⋯
hsurj' : Set.SurjOn f' ↑s.attach ↑t
⊢ #s.attach ≤ #t

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : #s ≤ #t
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
f' : ↥s → β := fun a ↦ f ↑a ⋯
hsurj' : Set.SurjOn f' ↑s.attach ↑t
hinj' : Set.InjOn f' ↑s.attach
⊢ ⟨a₁, ha₁⟩ ∈ ↑s.attach

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
hb : b ≠ 0
⊢ a.castPred ha ≤ b.pred hb ↔ 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 β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : #s ≤ #t
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
f' : ↥s → β := fun a ↦ f ↑a ⋯
hsurj' : Set.SurjOn f' ↑s.attach ↑t
hinj' : Set.InjOn f' ↑s.attach
⊢ ⟨a₂, ha₂⟩ ∈ ↑s.attach

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Fin (n + 1)
h₁ : a ≠ 0
h₂ : a ≠ last n
⊢ a.pred h₁ < a.castPred h₂

Tactic:
by

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

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

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: α : Type u
m n : ℕ
f : Fin (m * n) → α
i : Fin n
j : Fin m
⊢ m * ↑i + m = m * (↑i + 1)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : #s ≤ #t
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
⊢ a₁ = a₂

Tactic:
by

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

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

Goal state before:
pp: n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
⊢ n - ↑b + ↑a < n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
t : Finset β
inst✝ : DecidableEq β
h : #s ≤ #t
⊢ image f s = t ↔ Set.BijOn f ↑s ↑t

Tactic:
by

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

Goal state before:
pp: n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
⊢ m - ↑b + ↑a < m

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
⊢ ofFn [].get = []

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
hb : b ≠ last n
h : a ≤ b
⊢ ↑(a.castPred ⋯ - b.castPred hb) = ↑(a - b) - 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ ∀ (a : α) (s_1 : Finset α),
    a ∉ s_1 → #(s ∪ s_1) + #(s ∩ s_1) = #s + #s_1 → #(s ∪ insert a s_1) + #(s ∩ insert a s_1) = #s + #(insert a s_1)

Tactic:
by

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

Goal state before:
pp: α : Type u
a : α
l : List α
⊢ ofFn (a :: l).get = a :: l

Tactic:
by

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

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

Tactic:
by

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

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type u_1
l : List α
f : α → β
⊢ (ofFn fun i ↦ f l[↑i]) = map f l

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
a : α
⊢ a ∈ ofFn f ↔ a ∈ Set.range f

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
f : Fin n → α
P : α → Prop
⊢ (∀ (i : α), i ∈ ofFn f → P i) ↔ ∀ (j : Fin n), P (f j)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after: