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

Goal state before:
pp: α✝ : Type u
m n o✝ : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
i : Fin o
h : ¬↑i < m
⊢ ↑i - m < n

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
h : n = m
i : Fin n
⊢ map (finCongr h).toEmbedding (Iio i) = Iio (Fin.cast h i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ image (natAdd m) (Icc i j) = Icc (natAdd m i) (natAdd m j)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ image (natAdd m) (Ico i j) = Ico (natAdd m i) (natAdd m j)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ image (natAdd m) (Ioc i j) = Ioc (natAdd m i) (natAdd m j)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ image (natAdd m) (Ioo i j) = Ioo (natAdd m i) (natAdd m j)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ image (natAdd m) (uIcc i j) = uIcc (natAdd m i) (natAdd m j)

Tactic:
by

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

Goal state before:
pp: m n : ℕ
α : Type u_1
o : ℕ
ho : o = m + n
u : Fin m → α
v : Fin n → α
⊢ vecAppend ho u v = fun i ↦ if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ image (natAdd m) (Ici i) = Ici (natAdd m i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ image (natAdd m) (Ioi i) = Ioi (natAdd m i)

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
v : Fin n → α
⊢ vecAppend ⋯ ![] v = v

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ map (natAddEmb m) (Icc i j) = Icc (natAdd m i) (natAdd m j)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ map (natAddEmb m) (Ico i j) = Ico (natAdd m i) (natAdd m j)

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
v : Fin n → α
⊢ vecAppend ⋯ v ![] = v

Tactic:
by

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

Goal state before:
pp: α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
⊢ o = m + n

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ map (natAddEmb m) (Ioc i j) = Ioc (natAdd m i) (natAdd m j)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ map (natAddEmb m) (Ioo i j) = Ioo (natAdd m i) (natAdd m j)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: α : Fin 2 → Type u
s : Set (α 0)
t : Set (α 1)
⊢ (fun f ↦ (f 0, f 1)) ⁻¹' s ×ˢ t = Set.univ.pi (cons s (cons t finZeroElim))

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n : ℕ
i x : Fin (n + 1)
⊢ (fun x ↦ x.casesOn' i i.succAbove) (i.insertNth none some i) = i

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n : ℕ
i x : Fin (n + 1)
j : Fin n
⊢ (fun x ↦ x.casesOn' i i.succAbove) (i.insertNth none some (i.succAbove j)) = i.succAbove j

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n : ℕ
i : Fin (n + 1)
x : Option (Fin n)
⊢ i.insertNth none some ((fun x ↦ x.casesOn' i i.succAbove) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ (finSuccEquiv' i) i = none

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
m : Fin n
h : m.castSucc < i
⊢ (finSuccEquiv' i) m.castSucc = some m

Tactic:
rw [← Fin.succAbove_of_castSucc_lt _ _ h, finSuccEquiv'_succAbove]

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
m : Fin n
h : m.castSucc < i
⊢ (finSuccEquiv' i) m.castSucc = some m

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
m : Fin n
h : i ≤ m.castSucc
⊢ (finSuccEquiv' i) m.succ = some m

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
i : Fin n
⊢ (finSuccEquiv' (Fin.last n)) i.castSucc = some i

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
h : i ≠ Fin.last n
⊢ (finSuccEquiv' (Fin.last n)) i = some (i.castLT ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
hi : i ≠ Fin.last n
hj : j ≠ i
⊢ (finSuccEquiv' i) j = some ((i.castLT ⋯).predAbove j)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ map (natAddEmb m) (uIcc i j) = uIcc (natAdd m i) (natAdd m j)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ map (natAddEmb m) (Ici i) = Ici (natAdd m i)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
x : { x // x ≠ Fin.last n }
⊢ (finSuccAboveEquiv (Fin.last n)).symm x = (↑x).castLT ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ map (natAddEmb m) (Ioi i) = Ioi (natAdd m i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ image (fun x ↦ x.addNat m) (Icc i j) = Icc (i.addNat m) (j.addNat m)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ image (fun x ↦ x.addNat m) (Ico i j) = Ico (i.addNat m) (j.addNat m)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
h : p ≠ Fin.last n
x : { x // x ≠ p }
⊢ (finSuccAboveEquiv p).symm x = (p.castLT ⋯).predAbove ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ image (fun x ↦ x.addNat m) (Ioc i j) = Ioc (i.addNat m) (j.addNat m)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
⊢ finSuccEquivLast (Fin.last n) = none

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ image (fun x ↦ x.addNat m) (Ioo i j) = Ioo (i.addNat m) (j.addNat m)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ image (fun x ↦ x.addNat m) (uIcc i j) = uIcc (i.addNat m) (j.addNat m)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
ι : Type u_1
f : (e : Fin n ↪ ι) × { i // ¬i ∈ Set.range ⇑e }
⊢ ⇑((embeddingFinSucc n ι).symm f) = Fin.cons ↑f.snd ⇑f.fst

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ image (fun x ↦ x.addNat m) (Ici i) = Ici (i.addNat m)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ image (fun x ↦ x.addNat m) (Ioi i) = Ioi (i.addNat m)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ map (addNatEmb m) (Icc i j) = Icc (i.addNat m) (j.addNat m)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ map (addNatEmb m) (Ico i j) = Ico (i.addNat m) (j.addNat m)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n : ℕ
x : Fin m ⊕ Fin n
⊢ (fun i ↦ Fin.addCases Sum.inl Sum.inr i) (Sum.elim (Fin.castAdd n) (Fin.natAdd m) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ map (addNatEmb m) (Ioc i j) = Ioc (i.addNat m) (j.addNat m)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ map (addNatEmb m) (Ioo i j) = Ioo (i.addNat m) (j.addNat m)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
⊢ ∏ᶠ (i : α) (_ : i ∈ g '' s), f i = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
i j : Fin n
⊢ map (addNatEmb m) (uIcc i j) = uIcc (i.addNat m) (j.addNat m)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n : ℕ
x : Fin (m + n)
⊢ Sum.elim (Fin.castAdd n) (Fin.natAdd m) ((fun i ↦ Fin.addCases Sum.inl Sum.inr i) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
i : Fin n
⊢ (finSumNatEquiv n).symm ↑i = Sum.inl i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ map (addNatEmb m) (Ici i) = Ici (i.addNat m)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n i : ℕ
⊢ (finSumNatEquiv n).symm (i + n) = Sum.inr i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ map (addNatEmb m) (Ioi i) = Ioi (i.addNat m)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n i : ℕ
⊢ (finSumNatEquiv n).symm (n + i) = Sum.inr i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ image succ (Iic i) = Ioc 0 i.succ

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ image succ (Iio i) = Ioo 0 i.succ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
g : β → α
hg : InjOn g (mulSupport (f ∘ g))
⊢ ∏ᶠ (i : α) (_ : i ∈ range g), f i = ∏ᶠ (j : β), f (g j)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ map (succEmb n) (Iic i) = Ioc 0 i.succ

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ map (succEmb n) (Iio i) = Ioo 0 i.succ

Tactic:
by

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

Goal state before:
pp: α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
⊢ vecAppend ho (vecCons x u) v = vecCons x (vecAppend ⋯ u v)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ image rev (Icc i j) = Icc j.rev i.rev

Tactic:
by

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

Goal state before:
pp: α : Type u
m n o : ℕ
hm : m = n + n
v : Fin m → α
k : Fin n
⊢ ↑k + ↑k < m

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ image rev (Ico i j) = Ioc j.rev i.rev

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ image rev (Ioc i j) = Ico j.rev i.rev

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Set α
t : Set β
f : α → M
g : β → M
e : α → β
he₀ : BijOn e s t
he₁ : ∀ x ∈ s, f x = g (e x)
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (j : β) (_ : j ∈ t), g j

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ image rev (Ioo i j) = Ioo j.rev i.rev

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n i : ℕ
⊢ ((finSumNatEquiv n).symm i).isLeft = decide (i < n)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ image rev (uIcc i j) = uIcc i.rev j.rev

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ image rev (Ici i) = Iic i.rev

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → M
g : β → M
e : α → β
he₀ : Bijective e
he₁ : ∀ (x : α), f x = g (e x)
⊢ ∏ᶠ (i : α), f i = ∏ᶠ (j : β), g j

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ image rev (Ioi i) = Iio i.rev

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ image rev (Iic i) = Ici i.rev

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
⊢ ∏ᶠ (j : ↑s), f ↑j = ∏ᶠ (i : α) (_ : i ∈ s), f i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ image rev (Iio i) = Ioi i.rev

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n i : ℕ
⊢ ((finSumNatEquiv n).symm i).isRight = decide (n ≤ i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Icc i j) = Icc j.rev i.rev

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m : ℕ
k : Fin m
n : ℕ
⊢ finAddFlip (Fin.castAdd n k) = Fin.natAdd n k

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: n : ℕ
k : Fin n
m : ℕ
⊢ finAddFlip (Fin.natAdd m k) = Fin.castAdd m k

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Ico i j) = Ioc j.rev i.rev

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Ioc i j) = Ico j.rev i.rev

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n k : ℕ
h : k < m
hk : k < m + n
hnk : n + k < n + m
⊢ finAddFlip ⟨k, hk⟩ = ⟨n + k, hnk⟩

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Ioo i j) = Ioo j.rev i.rev

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ k - m < n + m

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
v : Fin n → α
⊢ vecAlt0 ⋯ (vecAppend ⋯ v v) = v ∘ fun n_1 ↦ n_1 + n_1

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ map (Equiv.toEmbedding revPerm) (uIcc i j) = uIcc i.rev j.rev

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ k - m < n

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Ici i) = Iic i.rev

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n k : ℕ
h₁ : m ≤ k
h₂ : k < m + n
⊢ finAddFlip ⟨k, h₂⟩ = ⟨k - m, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Ioi i) = Iio i.rev

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Iic i) = Ici i.rev

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n : ℕ
x : Fin m × Fin n
⊢ ↑x.2 + n * ↑x.1 + 1 = ↑x.1 * n + ↑x.2 + 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Iio i) = Ioi i.rev

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n : ℕ
x✝ : Fin m × Fin n
x : Fin m
y : Fin n
H : 0 < n
⊢ ↑y / n + ↑x = 0 + ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
h : (s ∩ mulSupport f).Finite
⊢ (∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s \ t), f i = ∏ᶠ (i : α) (_ : i ∈ s), f i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ #(Icc a b) = ↑b + 1 - ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ #(Ico a b) = ↑b - ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n✝ n : ℕ
inst✝ : NeZero n
p : ℕ × Fin n
⊢ (fun a ↦ (a / n, Fin.ofNat n a)) ((fun p ↦ p.1 * n + ↑p.2) p) = p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
hst : s ⊆ t
ht : (t ∩ mulSupport f).Finite
⊢ (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t \ s), f i = ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ #(Ioc a b) = ↑b - ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n✝ n : ℕ
inst✝ : NeZero n
a : ℤ
⊢ (fun p ↦ p.1 * ↑n + ↑↑p.2) ((fun a ↦ (a / ↑n, Fin.ofNat n (a.natMod ↑n))) a) = a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ #(Ioo a b) = ↑b - ↑a - 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ #(uIcc a b) = (↑↑b - ↑↑a).natAbs + 1

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n✝ n : ℕ
inst✝ : NeZero n
x✝ : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
h1 : 0 ≤ ↑r
h2 : ↑r < ↑n
⊢ (↑r + q * ↑n) / ↑n = q ∧ ↑(Fin.ofNat n ((↑r + q * ↑n).natMod ↑n)) = r

Tactic:
add_mul_ediv_right _ _ (natCast_eq_zero.not.2 (NeZero.ne n)),

Goal state after:
m n✝ n : ℕ
inst✝ : NeZero n
x✝ : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
h1 : 0 ≤ ↑r
h2 : ↑r < ↑n
⊢ ↑r / ↑n + q = q ∧ ↑(Fin.ofNat n ((↑r + q * ↑n).natMod ↑n)) = r
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a : Fin n
⊢ #(Ici a) = n - ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a : Fin n
⊢ #(Ioi a) = n - 1 - ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
b : Fin n
⊢ #(Iic b) = ↑b + 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
b : Fin n
⊢ #(Iio b) = ↑b

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
v : Fin (n + 1 + 1) → α
i : Fin (n + 1 + 1)
h : n + 1 + 1 ≤ ↑i + ↑i + 1
⊢ 1 < n + 2

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m n✝ n : ℕ
inst✝ : NeZero n
x✝ : ℤ × Fin n
q : ℤ
r : ℕ
hrn : r < n
⊢ (fun a ↦ (a / ↑n, Fin.ofNat n (a.natMod ↑n))) ((fun p ↦ p.1 * ↑n + ↑↑p.2) (q, ⟨r, hrn⟩)) = (q, ⟨r, hrn⟩)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
b : Fin n
hb : ↑b + 1 < n
⊢ Iio (b + 1) = Iic b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
b : Fin n
hb : ↑b + 1 < n
⊢ Iio (b + 1) = Iic b

Tactic:
by
  grind [= Fin.lt_def, = Fin.le_def, = Fin.val_add_one_of_lt']

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m✝ n✝ n m : ℕ
h : n ≤ m
i : Fin n
⊢ ↑(castLE h i) < n

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m✝ n✝ n m : ℕ
h : n ≤ m
x✝ : Fin n
⊢ (fun i ↦ ⟨↑↑i, ⋯⟩) ((fun i ↦ ⟨castLE h i, ⋯⟩) x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
b : Fin n
⊢ 0 < b → Iic (b - 1) = Iio b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m✝ n✝ n m : ℕ
h : n ≤ m
x✝ : { i // ↑i < n }
⊢ (fun i ↦ ⟨castLE h i, ⋯⟩) ((fun i ↦ ⟨↑↑i, ⋯⟩) x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a : Fin n
ha : ↑a + 1 < n
⊢ Ici (a + 1) = Ioi a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m✝ n✝ : ℕ
α : Type u_1
m n : ℕ
fg : (Fin m → α) × (Fin n → α)
⊢ (fun f ↦ (fun i ↦ f (castAdd n i), fun i ↦ f (natAdd m i))) ((fun fg ↦ append fg.1 fg.2) fg) = fg

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a : Fin n
⊢ 0 < a → Ioi (a - 1) = Ici a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Basic

Goal state before:
pp: m✝ n✝ : ℕ
α : Type u_1
m n : ℕ
f : Fin (m + n) → α
⊢ (fun fg ↦ append fg.1 fg.2) ((fun f ↦ (fun i ↦ f (castAdd n i), fun i ↦ f (natAdd m i))) f) = f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ 0 < a → Ioc (a - 1) b = Icc a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a b : Fin n
ha : ↑a + 1 < n
⊢ Icc (a + 1) b = Ioc a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a b : Fin n
ha : ↑a + 1 < n
⊢ Icc (a + 1) b = Ioc a b

Tactic:
by
  grind [= Fin.lt_def, = Fin.le_def, = Fin.val_add_one_of_lt']

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ 0 < a → Ioo (a - 1) b = Ico a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a b : Fin n
ha : ↑a + 1 < n
⊢ Ico (a + 1) b = Ioo a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a b : Fin n
ha : ↑a + 1 < n
⊢ Ico (a + 1) b = Ioo a b

Tactic:
by
  grind [= Fin.lt_def, = Fin.le_def, = Fin.val_add_one_of_lt']

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ 0 < b → Icc a (b - 1) = Ico a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a b : Fin n
hb : ↑b + 1 < n
⊢ Ico a (b + 1) = Icc a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a b : Fin n
hb : ↑b + 1 < n
⊢ Ico a (b + 1) = Icc a b

Tactic:
by
  grind [= Fin.lt_def, = Fin.le_def, = Fin.val_add_one_of_lt']

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a b : Fin n
⊢ 0 < b → Ioc a (b - 1) = Ioo a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a b : Fin n
hb : ↑b + 1 < n
⊢ Ioo a (b + 1) = Ioc a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a b : Fin n
hb : ↑b + 1 < n
⊢ Ioo a (b + 1) = Ioc a b

Tactic:
by
  grind [= Fin.lt_def, = Fin.le_def, = Fin.val_add_one_of_lt']

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

Goal state before:
pp: α : Type u
n : ℕ
v : Fin (n + 1) → α
⊢ vecAlt1 ⋯ (vecAppend ⋯ v v) = v ∘ fun n_1 ↦ n_1 + n_1 + 1

Tactic:
by

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

Goal state before:
pp: α : Type u
m n : ℕ
hm : m + 2 = n + 1 + (n + 1)
v : Fin (m + 2) → α
⊢ vecHead (vecAlt1 hm v) = v 1

Tactic:
by

Goal state after: