mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
⊢ x ∈ span R s → ∃ f t, ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∑ a ∈ t, f a • a = x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x : M
⊢ (∃ f t, ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∑ a ∈ t, f a • a = x) → x ∈ span R s

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝¹ : Type u_3
R₂ : Type u_4
K : Type u_5
M✝¹ : Type u_6
M'✝ : Type u_7
M''✝ : Type u_8
V : Type u
V' : Type u_9
inst✝¹⁶ : Semiring R✝¹
inst✝¹⁵ : AddCommMonoid M✝¹
inst✝¹⁴ : Module R✝¹ M✝¹
inst✝¹³ : AddCommMonoid M'✝
inst✝¹² : Module R✝¹ M'✝
ι : Type u_10
R✝ : Type u_11
M✝ : Type u_12
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
b✝ : Basis ι R✝ M✝
inst✝⁸ : Module R✝ M'✝
i✝ : ι
M'' : Type u_13
b'✝ : Basis ι' R✝ M'✝
e : ι ≃ ι'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : Module R✝ M''
R : Type u_14
M : Type u_15
M' : Type u_16
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
inst✝ : SMulCommClass R R M'
f : M → M'
g : M' → M
hf : ∀ (i : ι), f (b i) ∈ range ⇑b'
hg : ∀ (i : ι'), g (b' i) ∈ range ⇑b
hgf : ∀ (i : ι), g (f (b i)) = b i
hfg : ∀ (i : ι'), f (g (b' i)) = b' i
i : ι'
i' : ι
hi' : b i' = g (b' i)
⊢ ((b.constr R) (f ∘ ⇑b) ∘ₗ (b'.constr R) (g ∘ ⇑b')) (b' i) = LinearMap.id (b' i)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset M
x : M
⊢ x ∈ span R ↑s → ∃ f, Function.support f ⊆ ↑s ∧ ∑ a ∈ s, f a • a = x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_10
R : Type u_14
M : Type u_15
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
ι' : Type u_17
inst✝ : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
⊢ ∑ j, (b.repr (b' j)) i * (b'.repr x) j = (b.repr x) i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset M
x : M
⊢ (∃ f, Function.support f ⊆ ↑s ∧ ∑ a ∈ s, f a • a = x) → x ∈ span R ↑s

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x : M
⊢ (∀ (i : ι), (b.coord i) x = 0) ↔ b.repr x = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
b : Basis ι R M
inst✝ : Fintype ι
⊢ ⇑b.sumCoords = ⇑(∑ i, b.coord i)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
⊢ b.sumCoords (b i) = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
m : M
r : R
⊢ (b.coord i) (r • m) = r * (b.coord i) m

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set M
inst✝ : Fintype ↑s
x : M
⊢ x ∈ span R s ↔ ∃ f, ∑ a, f a • ↑a = x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
i : ι
f : ι →₀ R
⊢ (b.coord i) (b.repr.symm f) = f i

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 α
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ (∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i =
    (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
⊢ ⇑b.sumCoords = fun m ↦ ∑ᶠ (i : ι), (b.coord i) m

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
s : Set M
⊢ m ∈ span R s ↔ ∃ c, ↑c.support ⊆ s ∧ (c.sum fun mi r ↦ r • mi) = m

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Defs

Goal state before:
pp: ι' : Type u_2
ι : Type u_10
R : Type u_11
M : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
e : ι ≃ ι'
⊢ (b.reindex e).sumCoords = b.sumCoords

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 : Disjoint s t
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ map valEmbedding univ = Iio n

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ ↑(Ioi 0) = ↑(map (succEmb n) univ)

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ ↑(Iio (last n)) = ↑(map castSuccEmb univ)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ Iio i.castSucc = map castSuccEmb (Iio i)

Tactic:
by

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

Goal state before:
pp: n m : ℕ
⊢ #{i | ↑i < m} = min n m

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
⊢ #{x | p x} = if p 0 then #{x | p x.succ} + 1 else #{x | p x.succ}

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 : Disjoint (s ∩ mulSupport f) (t ∩ mulSupport f)
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i =
    (∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f), f i) * ∏ᶠ (i : α) (_ : i ∈ t ∩ mulSupport f), f i

Tactic:
←
    finprod_mem_union hst hs ht,

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s t : Set α
hst : Disjoint (s ∩ mulSupport f) (t ∩ mulSupport f)
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = ∏ᶠ (i : α) (_ : i ∈ s ∩ mulSupport f ∪ t ∩ mulSupport f), f i
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
s : Set M
⊢ m ∈ span R s ↔ ∃ n f g, ∑ i, f i • ↑(g i) = m

Tactic:
by

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
⊢ #{x | p x} = (if p 0 then 1 else 0) + #{x | p x.succ}

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 : Disjoint (s ∩ mulSupport f) (t ∩ mulSupport f)
hs : (s ∩ mulSupport f).Finite
ht : (t ∩ mulSupport f).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i

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
a : α
⊢ ∏ᶠ (i : α) (_ : i ∈ {a}), f i = f a

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
a : α
⊢ ∏ᶠ (i : α) (_ : a = i), f i = f a

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ ↑(span R s) = ⋃ n, (fun f ↦ ∑ i, (f i).1 • (f i).2) '' {f | ∀ (i : Fin n), (f i).2 ∈ s}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
v : List.Vector α n
⊢ #{i | v.get i = a} = List.count a v.toList

Tactic:
by

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

Goal state before:
pp: n : ℕ
j : Fin n
p : Fin n → Prop
inst✝ : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
k : Fin n
hk : ¬p k
⊢ {i | p i} ⊆ Iio k

Tactic:
by

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

Goal state before:
pp: n : ℕ
j : Fin n
p : Fin n → Prop
inst✝ : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
k : Fin n
hk : ¬p k
⊢ #{i | p i} ≤ ↑k

Tactic:
by

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

Goal state before:
pp: n : ℕ
j : Fin n
p : Fin n → Prop
inst✝ : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
h1 : ∀ (k : Fin n), ¬p k → #{i | p i} ≤ ↑k
⊢ ↑j < #{i | p i} → p j

Tactic:
by

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

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

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
a : α
s : Set α
h : a ∉ s → f a = 1
⊢ ∏ᶠ (i : α) (_ : i ∈ insert a s), f i = ∏ᶠ (i : α) (_ : i ∈ s), f i

Tactic:
by

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

Goal state before:
pp: n✝ n : ℕ
a b : Fin n
⊢ ∀ (x : Fin n), x ∈ (Icc ↑a ↑b).attachFin ⋯ ↔ a ≤ x ∧ x ≤ b

Tactic:
by

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

Goal state before:
pp: n✝ n : ℕ
a b : Fin n
⊢ ∀ (x : Fin n), x ∈ (Ico ↑a ↑b).attachFin ⋯ ↔ a ≤ x ∧ x < b

Tactic:
by

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

Goal state before:
pp: n✝ n : ℕ
a b : Fin n
⊢ ∀ (x : Fin n), x ∈ (Ioc ↑a ↑b).attachFin ⋯ ↔ a < x ∧ x ≤ b

Tactic:
by

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

Goal state before:
pp: n : ℕ
j : Fin n
p : Fin n → Prop
inst✝ : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
h1 : ∀ (k : Fin n), ¬p k → #{i | p i} ≤ ↑k
h : p j
hc : #{i | p i} ≤ ↑j
q : Fin n → Prop := fun x ↦ ↑x < #{i | p i}
⊢ filter q univ ⊆ filter p univ

Tactic:
by

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

Goal state before:
pp: n✝ n : ℕ
a b : Fin n
⊢ ∀ (x : Fin n), x ∈ (Ioo ↑a ↑b).attachFin ⋯ ↔ a < x ∧ x < b

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ (Ico (↑a) n).attachFin ⋯ = Ici a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
N : Type u_6
inst✝ : CommMonoid N
f : α → N
a : α
hf : HasFiniteMulSupport f
⊢ f a ∣ finprod f

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ (Ioo (↑a) n).attachFin ⋯ = Ioi a

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ (Iic ↑a).attachFin ⋯ = Iic a

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ (Iio ↑a).attachFin ⋯ = Iio a

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ image val (Ici a) = Ico (↑a) n

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ image val (Ioi a) = Ioo (↑a) n

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ image val (Iic a) = Iic ↑a

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ map valEmbedding (Ici a) = Ico (↑a) n

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ map valEmbedding (Ioi a) = Ioo (↑a) n

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
a b : α
h : a ≠ b
⊢ ∏ᶠ (i : α) (_ : i ∈ {a, b}), f i = f a * f b

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ map valEmbedding (Iic a) = Iic ↑a

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ map valEmbedding (Iio a) = Iio ↑a

Tactic:
by

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

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ image (castLE h) (Icc a b) = Icc (castLE h a) (castLE h b)

Tactic:
by

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

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ image (castLE h) (Ico a b) = Ico (castLE h a) (castLE h b)

Tactic:
by

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

Goal state before:
pp: n : ℕ
j : Fin n
p : Fin n → Prop
inst✝ : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
h1 : ∀ (k : Fin n), ¬p k → #{i | p i} ≤ ↑k
h : p j
hc : #{i | p i} ≤ ↑j
q : Fin n → Prop := fun x ↦ ↑x < #{i | p i}
⊢ #(filter p univ) ≤ #(filter q univ)

Tactic:
by

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

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ image (castLE h) (Ioc a b) = Ioc (castLE h a) (castLE h b)

Tactic:
by

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

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ image (castLE h) (Ioo a b) = Ioo (castLE h a) (castLE h b)

Tactic:
by

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

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ image (castLE h) (uIcc a b) = uIcc (castLE h a) (castLE h b)

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))
hs : (s ∩ mulSupport (f ∘ g)).Finite
⊢ ∀ x ∈ hs.toFinset, ∀ y ∈ hs.toFinset, g x = g y → x = y

Tactic:
by

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

Goal state before:
pp: n m : ℕ
a : Fin n
h : n ≤ m
⊢ image (castLE h) (Iic a) = Iic (castLE h a)

Tactic:
by

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

Goal state before:
pp: n m : ℕ
a : Fin n
h : n ≤ m
⊢ image (castLE h) (Iio a) = Iio (castLE h a)

Tactic:
by

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

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ map (castLEEmb h) (Icc a b) = Icc (castLE h a) (castLE h b)

Tactic:
by

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

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ map (castLEEmb h) (Ico a b) = Ico (castLE h a) (castLE h b)

Tactic:
by

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

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ map (castLEEmb h) (Ioc a b) = Ioc (castLE h a) (castLE h b)

Tactic:
by

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

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ map (castLEEmb h) (Ioo a b) = Ioo (castLE h a) (castLE h b)

Tactic:
by

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

Goal state before:
pp: n m : ℕ
a b : Fin n
h : n ≤ m
⊢ map (castLEEmb h) (uIcc a b) = uIcc (castLE h a) (castLE h b)

Tactic:
by

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

Goal state before:
pp: n : ℕ
j : Fin n
p : Fin n → Prop
inst✝ : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
h1 : ∀ (k : Fin n), ¬p k → #{i | p i} ≤ ↑k
h : p j
hc : #{i | p i} ≤ ↑j
q : Fin n → Prop := fun x ↦ ↑x < #{i | p i}
this : filter q univ = filter p univ
⊢ j ∈ filter p univ

Tactic:
by

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

Goal state before:
pp: n m : ℕ
a : Fin n
h : n ≤ m
⊢ map (castLEEmb h) (Iic a) = Iic (castLE h a)

Tactic:
by

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

Goal state before:
pp: n m : ℕ
a : Fin n
h : n ≤ m
⊢ map (castLEEmb h) (Iio a) = Iio (castLE h a)

Tactic:
by

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

Goal state before:
pp: n m : ℕ
inst✝ : NeZero m
i : Fin n
⊢ image (castAdd m) (Ici i) = Ico (castAdd m i) (natAdd n 0)

Tactic:
by

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

Goal state before:
pp: n m : ℕ
inst✝ : NeZero m
i : Fin n
⊢ image (castAdd m) (Ioi i) = Ioo (castAdd m i) (natAdd n 0)

Tactic:
by

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

Goal state before:
pp: n m : ℕ
inst✝ : NeZero m
i : Fin n
⊢ map (castAddEmb m) (Ici i) = Ico (castAdd m i) (natAdd n 0)

Tactic:
by

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

Goal state before:
pp: n m : ℕ
inst✝ : NeZero m
i : Fin n
⊢ map (castAddEmb m) (Ioi i) = Ioo (castAdd m i) (natAdd n 0)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
j : Fin n
p : Fin n → Prop
inst✝ : DecidablePred p
hp : ∀ (i j : Fin n), j ≤ i → p i → p j
⊢ ↑j < #{i | p i} ↔ p j

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ image val univ = range n

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
N : Type u_3
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R✝ N
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ι
c : ι → R
h₀ : c i = 0
⊢ (ι →₀ R) ≃ₗ[R] ι →₀ R

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
n : ℕ
f : ℕ → α
⊢ (univ.sup fun n_1 ↦ f ↑n_1) = (range n).sup f

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

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 (Ici i) = Ici (Fin.cast h i)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ι
c : ι → R
h₀ : c i = 0
v : ι → M
⊢ linearCombination R v ∘ₗ ↑(addSingleEquiv i c h₀) = linearCombination R (v + fun x ↦ c x • v i)

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 (Ioi i) = Ioi (Fin.cast h i)

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 (Iic i) = Iic (Fin.cast h i)

Tactic:
by

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

Goal state before:
pp: α : Type u
m : ℕ
x : α
u : Fin m → α
i : Fin m
⊢ vecCons x u i.succ = u i

Tactic:
by

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

Goal state before:
pp: α : Type u
m i : ℕ
h : i.succ < m.succ
x : α
u : Fin m → α
⊢ vecCons x u ⟨i.succ, h⟩ = u ⟨i, ⋯⟩

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x : α
⊢ Fin.cons x ![] = ![x]

Tactic:
by

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

Goal state before:
pp: α : Type u_1
x : α
⊢ Fin.snoc ![] x = ![x]

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Type u_1
x y : α
p : Fin n → α
⊢ Fin.cons x (vecCons y p) = vecCons x (vecCons y p)

Tactic:
by

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

Goal state before:
pp: α : Type u
m : ℕ
x : α
u : Fin m → α
⊢ vecTail (vecCons x u) = u

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
x : α
u : Fin n → α
y : α
⊢ y ∈ Set.range (vecCons x u) ↔ y ∈ {x} ∪ Set.range u

Tactic:
by

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

Goal state before:
pp: α : Type u
x : α
u : Fin 0 → α
⊢ Set.range (vecCons x u) = {x}

Tactic:
by

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

Goal state before:
pp: α : Type u
x y : α
u : Fin 0 → α
⊢ Set.range (vecCons x (vecCons y u)) = {x, y}

Tactic:
by

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

Goal state before:
pp: α : Type u
x : α
u : Fin 0 → α
⊢ ∀ (i : Fin 1), vecCons x u i = x

Tactic:
by

Goal state after: