mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case intro
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i ↦ ↑(t i))
⊢ ∏ x, ∏ i ∈ t x, f i = ∏ᶠ (i : ι) (a : α) (_ : a ∈ (fun i ↦ ↑(t i)) i), f a

pp: case intro
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i ↦ ↑(t i))
⊢ (↑Finset.univ).PairwiseDisjoint t

Tactic:
·

Goal state after:
case intro
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i ↦ ↑(t i))
⊢ ∏ x, ∏ i ∈ t x, f i = ∏ᶠ (i : ι) (a : α) (_ : a ∈ (fun i ↦ ↑(t i)) i), f a
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case intro
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i ↦ ↑(t i))
⊢ (↑Finset.univ).PairwiseDisjoint t

Tactic:
·

Goal state after:
case intro
α : Type u_1
ι : Type u_3
M : Type u_5
inst✝¹ : CommMonoid M
f : α → M
inst✝ : Finite ι
val✝ : Fintype ι
t : ι → Finset α
h : Pairwise (Disjoint on fun i ↦ ↑(t i))
⊢ (↑Finset.univ).PairwiseDisjoint t
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
m n o : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
⊢ m = n + n

Tactic:
by lia

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

Goal state before:
pp: case zero
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
hi : 0 < n + 1
⊢ vecCons x (vecCons y u) ⟨↑⟨0, hi⟩ + ↑⟨0, hi⟩, ⋯⟩ = vecCons x (vecAlt0 ⋯ u) ⟨0, hi⟩

pp: case succ
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : ℕ
hi : i + 1 < n + 1
⊢ vecCons x (vecCons y u) ⟨↑⟨i + 1, hi⟩ + ↑⟨i + 1, hi⟩, ⋯⟩ = vecCons x (vecAlt0 ⋯ u) ⟨i + 1, hi⟩

Tactic:
·

Goal state after:
case zero
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
hi : 0 < n + 1
⊢ vecCons x (vecCons y u) ⟨↑⟨0, hi⟩ + ↑⟨0, hi⟩, ⋯⟩ = vecCons x (vecAlt0 ⋯ u) ⟨0, hi⟩
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case succ
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : ℕ
hi : i + 1 < n + 1
⊢ vecCons x (vecCons y u) ⟨↑⟨i + 1, hi⟩ + ↑⟨i + 1, hi⟩, ⋯⟩ = vecCons x (vecAlt0 ⋯ u) ⟨i + 1, hi⟩

Tactic:
·

Goal state after:
case succ
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : ℕ
hi : i + 1 < n + 1
⊢ vecCons x (vecCons y u) ⟨↑⟨i + 1, hi⟩ + ↑⟨i + 1, hi⟩, ⋯⟩ = vecCons x (vecAlt0 ⋯ u) ⟨i + 1, hi⟩
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
t : Set (Set α)
h : t.PairwiseDisjoint id
ht₀ : t.Finite
ht₁ : ∀ x ∈ t, x.Finite
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃₀ t), f a = ∏ᶠ (s : Set α) (_ : s ∈ t) (a : α) (_ : a ∈ s), f a

Tactic:
rw [Set.sUnion_eq_biUnion]

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
t : Set (Set α)
h : t.PairwiseDisjoint id
ht₀ : t.Finite
ht₁ : ∀ x ∈ t, x.Finite
⊢ ∏ᶠ (a : α) (_ : a ∈ ⋃ i ∈ t, i), f a = ∏ᶠ (s : Set α) (_ : s ∈ t) (a : α) (_ : a ∈ s), f a
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case zero
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
hi : 0 < n + 1
⊢ vecCons x (vecCons y u) ⟨↑⟨0, hi⟩ + ↑⟨0, hi⟩ + 1, ⋯⟩ = vecCons y (vecAlt1 ⋯ u) ⟨0, hi⟩

pp: case succ
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : ℕ
hi : i + 1 < n + 1
⊢ vecCons x (vecCons y u) ⟨↑⟨i + 1, hi⟩ + ↑⟨i + 1, hi⟩ + 1, ⋯⟩ = vecCons y (vecAlt1 ⋯ u) ⟨i + 1, hi⟩

Tactic:
·

Goal state after:
case zero
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
hi : 0 < n + 1
⊢ vecCons x (vecCons y u) ⟨↑⟨0, hi⟩ + ↑⟨0, hi⟩ + 1, ⋯⟩ = vecCons y (vecAlt1 ⋯ u) ⟨0, hi⟩
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case succ
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : ℕ
hi : i + 1 < n + 1
⊢ vecCons x (vecCons y u) ⟨↑⟨i + 1, hi⟩ + ↑⟨i + 1, hi⟩ + 1, ⋯⟩ = vecCons y (vecAlt1 ⋯ u) ⟨i + 1, hi⟩

Tactic:
·

Goal state after:
case succ
α : Type u
m n : ℕ
h : m + 1 + 1 = n + 1 + (n + 1)
x y : α
u : Fin m → α
i : ℕ
hi : i + 1 < n + 1
⊢ vecCons x (vecCons y u) ⟨↑⟨i + 1, hi⟩ + ↑⟨i + 1, hi⟩ + 1, ⋯⟩ = vecCons y (vecAlt1 ⋯ u) ⟨i + 1, hi⟩
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case e'_2
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
x✝ : Option α
⊢ f x✝ = ∏ᶠ (_ : x✝ ∈ insert none (range some)), f x✝

pp: case e'_3
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
⊢ ∏ᶠ (a : α), f (some a) = ∏ᶠ (i : Option α) (_ : i ∈ range some), f i

Tactic:
·

Goal state after:
case e'_2
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
x✝ : Option α
⊢ f x✝ = ∏ᶠ (_ : x✝ ∈ insert none (range some)), f x✝
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case e'_3
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
⊢ ∏ᶠ (a : α), f (some a) = ∏ᶠ (i : Option α) (_ : i ∈ range some), f i

Tactic:
·

Goal state after:
case e'_3
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : Option α → M
hf : (mulSupport f).Finite
⊢ ∏ᶠ (a : α), f (some a) = ∏ᶠ (i : Option α) (_ : i ∈ range some), f i
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
n : ℕ
a b : α
x : Fin n → α
j : Fin n.succ.succ
i : ℕ
h : i + 2 < n.succ.succ
⊢ i < n

Tactic:
by lia

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

Goal state before:
pp: case inl
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
⊢ vecCons a (x ∘ ⇑(Equiv.swap i j)) 0 = (vecCons a x ∘ ⇑(Equiv.swap i.succ j.succ)) 0

pp: case inr
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
⊢ vecCons a (x ∘ ⇑(Equiv.swap i j)) k = (vecCons a x ∘ ⇑(Equiv.swap i.succ j.succ)) k

Tactic:
·

Goal state after:
case inl
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
⊢ vecCons a (x ∘ ⇑(Equiv.swap i j)) 0 = (vecCons a x ∘ ⇑(Equiv.swap i.succ j.succ)) 0
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case inr.inl
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
hk₀ : i.succ ≠ 0
⊢ vecCons a (x ∘ ⇑(Equiv.swap i j)) i.succ = (vecCons a x ∘ ⇑(Equiv.swap i.succ j.succ)) i.succ

pp: case inr.inr
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
⊢ vecCons a (x ∘ ⇑(Equiv.swap i j)) k = (vecCons a x ∘ ⇑(Equiv.swap i.succ j.succ)) k

Tactic:
·

Goal state after:
case inr.inl
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
hk₀ : i.succ ≠ 0
⊢ vecCons a (x ∘ ⇑(Equiv.swap i j)) i.succ = (vecCons a x ∘ ⇑(Equiv.swap i.succ j.succ)) i.succ
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case inr.inr.inl
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
hk₀ : j.succ ≠ 0
hki : j.succ ≠ i.succ
⊢ vecCons a (x ∘ ⇑(Equiv.swap i j)) j.succ = (vecCons a x ∘ ⇑(Equiv.swap i.succ j.succ)) j.succ

pp: case inr.inr.inr
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
⊢ vecCons a (x ∘ ⇑(Equiv.swap i j)) k = (vecCons a x ∘ ⇑(Equiv.swap i.succ j.succ)) k

Tactic:
·

Goal state after:
case inr.inr.inl
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
hk₀ : j.succ ≠ 0
hki : j.succ ≠ i.succ
⊢ vecCons a (x ∘ ⇑(Equiv.swap i j)) j.succ = (vecCons a x ∘ ⇑(Equiv.swap i.succ j.succ)) j.succ
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case pos
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
ha : a ∈ mulSupport f
⊢ f a * ∏ i ∈ (Finite.toFinset hf).erase a, f i = ∏ i ∈ Finite.toFinset hf, f i

pp: case neg
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
ha : a ∉ mulSupport f
⊢ f a * ∏ i ∈ (Finite.toFinset hf).erase a, f i = ∏ i ∈ Finite.toFinset hf, f i

Tactic:
·

Goal state after:
case pos
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
ha : a ∈ mulSupport f
⊢ f a * ∏ i ∈ (Finite.toFinset hf).erase a, f i = ∏ i ∈ Finite.toFinset hf, f i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case neg
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
ha : a ∉ mulSupport f
⊢ f a * ∏ i ∈ (Finite.toFinset hf).erase a, f i = ∏ i ∈ Finite.toFinset hf, f i

Tactic:
·

Goal state after:
case neg
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
a : α
hf : HasFiniteMulSupport f
h : ∀ (x : α), f x ≠ 1 → (x ≠ a ↔ x ∈ Finite.toFinset hf \ {a})
ha : a ∉ mulSupport f
⊢ f a * ∏ i ∈ (Finite.toFinset hf).erase a, f i = ∏ i ∈ Finite.toFinset hf, f i
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
⊢ ↑k - 1 < n

Tactic:
by lia

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
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ ∏ i ∈ ?s, ∏ y ∈ s with f y = i, g y = ∏ k ∈ s, g k

pp: case s
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ Finset α

pp: case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ (mulSupport fun x ↦ ∏ y ∈ s with f y = x, g y) ⊆ ↑?s

Tactic:
·

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ ∏ i ∈ ?s, ∏ y ∈ s with f y = i, g y = ∏ k ∈ s, g k
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ (mulSupport fun x ↦ ∏ y ∈ s with f y = x, g y) ⊆ ↑(Finset.image f s)

Tactic:
·

Goal state after:
case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : β → α
s : Finset β
g : β → M
⊢ (mulSupport fun x ↦ ∏ y ∈ s with f y = x, g y) ⊆ ↑(Finset.image f s)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case pos
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
hr : r = 0
⊢ r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a

pp: case neg
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
⊢ r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a

Tactic:
·

Goal state after:
case pos
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
hr : r = 0
⊢ r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case pos
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
h : (support f).Finite
⊢ r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a

pp: case neg
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
h : ¬(support f).Finite
⊢ r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a

Tactic:
·

Goal state after:
case pos
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
h : (support f).Finite
⊢ r * ∑ᶠ (a : α), f a = ∑ᶠ (a : α), r * f a
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case pos
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
hr : r = 0
⊢ (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r

pp: case neg
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
⊢ (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r

Tactic:
·

Goal state after:
case pos
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
hr : r = 0
⊢ (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: case zero
a : Fin (0 + 1)
⊢ ↑(a - 1) = if a = 0 then 0 else ↑a - 1

pp: case succ
n✝ : ℕ
a : Fin (n✝ + 1 + 1)
⊢ ↑(a - 1) = if a = 0 then n✝ + 1 else ↑a - 1

Tactic:
·

Goal state after:
case zero
a : Fin (0 + 1)
⊢ ↑(a - 1) = if a = 0 then 0 else ↑a - 1
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case pos
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
h : (support f).Finite
⊢ (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r

pp: case neg
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
h : ¬(support f).Finite
⊢ (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r

Tactic:
·

Goal state after:
case pos
α : Type u_1
R : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NoZeroDivisors R
f : α → R
r : R
hr : ¬r = 0
h : (support f).Finite
⊢ (∑ᶠ (a : α), f a) * r = ∑ᶠ (a : α), f a * r
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: case pos
n✝ : ℕ
a : Fin (n✝ + 1 + 1)
h : a = 0
⊢ ↑(a - 1) = n✝ + 1

pp: case neg
n✝ : ℕ
a : Fin (n✝ + 1 + 1)
h : ¬a = 0
⊢ ↑(a - 1) = ↑a - 1

Tactic:
·

Goal state after:
case pos
n✝ : ℕ
a : Fin (n✝ + 1 + 1)
h : a = 0
⊢ ↑(a - 1) = n✝ + 1
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: case zero
k : Fin (0 + 1)
⊢ k ≤ k - 1 ↔ k = 0

pp: case succ
n✝ : ℕ
k : Fin (n✝ + 1 + 1)
⊢ k ≤ k - 1 ↔ k = 0

Tactic:
·

Goal state after:
case zero
k : Fin (0 + 1)
⊢ k ≤ k - 1 ↔ k = 0
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: case zero
a b : Fin 0
⊢ (a + b).rev = a.rev - b

pp: case succ
n✝ : ℕ
a b : Fin (n✝ + 1)
⊢ (a + b).rev = a.rev - b

Tactic:
·

Goal state after:
case zero
a b : Fin 0
⊢ (a + b).rev = a.rev - b
Module: Mathlib.Logic.Equiv.Fin.Rotate

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

Tactic:
by lia

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

Goal state before:
pp: case pos
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : i < n
⊢ snoc v a ⟨i, h⟩ = cons a v ((finRotate (n + 1)) ⟨i, h⟩)

pp: case neg
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
⊢ snoc v a ⟨i, h⟩ = cons a v ((finRotate (n + 1)) ⟨i, h⟩)

Tactic:
·

Goal state after:
case pos
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : i < n
⊢ snoc v a ⟨i, h⟩ = cons a v ((finRotate (n + 1)) ⟨i, h⟩)
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: case neg
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
⊢ snoc v a ⟨i, h⟩ = cons a v ((finRotate (n + 1)) ⟨i, h⟩)

Tactic:
·

Goal state after:
case neg
n : ℕ
α : Type u_1
v : Fin n → α
a : α
i : ℕ
h : i < n + 1
h' : ¬i < n
⊢ snoc v a ⟨i, h⟩ = cons a v ((finRotate (n + 1)) ⟨i, h⟩)
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: case inl
n✝ n : ℕ
⊢ (finRotate (n + 2)) (Fin.last (n + 1)) = Fin.last (n + 1) + 1

pp: case inr
n✝ n : ℕ
i : Fin (n + 2)
h : i < Fin.last (n + 1)
⊢ (finRotate (n + 2)) i = i + 1

Tactic:
·

Goal state after:
case inl
n✝ n : ℕ
⊢ (finRotate (n + 2)) (Fin.last (n + 1)) = Fin.last (n + 1) + 1
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: case inr
n✝ n : ℕ
i : Fin (n + 2)
h : i < Fin.last (n + 1)
⊢ (finRotate (n + 2)) i = i + 1

Tactic:
·

Goal state after:
case inr
n✝ n : ℕ
i : Fin (n + 2)
h : i < Fin.last (n + 1)
⊢ (finRotate (n + 2)) i = i + 1
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this : ∀ (a : α), ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f
⊢ ∏ i ∈ s, f i = ∏ i ∈ Finset.image Prod.fst s, ∏ a ∈ s with a.1 = i, f a

Tactic:
← Finset.prod_fiberwise_of_maps_to (t := Finset.image Prod.fst s) _ f

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this : ∀ (a : α), ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f
⊢ ∏ j ∈ Finset.image Prod.fst s, ∏ i ∈ s with ?m.136 i = j, f i =
    ∏ i ∈ Finset.image Prod.fst s, ∏ a ∈ s with a.1 = i, f a

α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this : ∀ (a : α), ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f
⊢ α × β → α

α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset (α × β)
f : α × β → M
this : ∀ (a : α), ∏ i ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a}), f (a, i) = {x ∈ s | x.1 = a}.prod f
⊢ ∀ i ∈ s, ?m.136 i ∈ Finset.image Prod.fst s
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case pos
ι : Type u_3
R : Type u_7
inst✝¹ : CommSemiring R
inst✝ : CharZero R
f : ι → ℕ
hf : HasFiniteMulSupport f
⊢ ↑(∏ᶠ (x : ι), f x) = ∏ᶠ (x : ι), ↑(f x)

pp: case neg
ι : Type u_3
R : Type u_7
inst✝¹ : CommSemiring R
inst✝ : CharZero R
f : ι → ℕ
hf : ¬HasFiniteMulSupport f
⊢ ↑(∏ᶠ (x : ι), f x) = ∏ᶠ (x : ι), ↑(f x)

Tactic:
·

Goal state after:
case pos
ι : Type u_3
R : Type u_7
inst✝¹ : CommSemiring R
inst✝ : CharZero R
f : ι → ℕ
hf : HasFiniteMulSupport f
⊢ ↑(∏ᶠ (x : ι), f x) = ∏ᶠ (x : ι), ↑(f x)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: case neg
ι : Type u_3
R : Type u_7
inst✝¹ : CommSemiring R
inst✝ : CharZero R
f : ι → ℕ
hf : ¬HasFiniteMulSupport f
⊢ ↑(∏ᶠ (x : ι), f x) = ∏ᶠ (x : ι), ↑(f x)

Tactic:
·

Goal state after:
case neg
ι : Type u_3
R : Type u_7
inst✝¹ : CommSemiring R
inst✝ : CharZero R
f : ι → ℕ
hf : ¬HasFiniteMulSupport f
⊢ ↑(∏ᶠ (x : ι), f x) = ∏ᶠ (x : ι), ↑(f x)
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: case inl
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (range v)
inst✝ : DecidableEq ι
i j : ι
h : j = i
⊢ ((Basis.mk hli hsp).coord i) (v j) = if j = i then 1 else 0

pp: case inr
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (range v)
inst✝ : DecidableEq ι
i j : ι
h : j ≠ i
⊢ ((Basis.mk hli hsp).coord i) (v j) = if j = i then 1 else 0

Tactic:
·

Goal state after:
case inl
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (range v)
inst✝ : DecidableEq ι
i j : ι
h : j = i
⊢ ((Basis.mk hli hsp).coord i) (v j) = if j = i then 1 else 0
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: case inr
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (range v)
inst✝ : DecidableEq ι
i j : ι
h : j ≠ i
⊢ ((Basis.mk hli hsp).coord i) (v j) = if j = i then 1 else 0

Tactic:
·

Goal state after:
case inr
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
v : ι → M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (range v)
inst✝ : DecidableEq ι
i j : ι
h : j ≠ i
⊢ ((Basis.mk hli hsp).coord i) (v j) = if j = i then 1 else 0
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: case mp
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
⊢ Nonempty (Basis ι R M) → ∃ x, x ≠ 0 ∧ ∀ (y : M), ∃ r, r • x = y

pp: case mpr
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
⊢ (∃ x, x ≠ 0 ∧ ∀ (y : M), ∃ r, r • x = y) → Nonempty (Basis ι R M)

Tactic:
·

Goal state after:
case mp
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
⊢ Nonempty (Basis ι R M) → ∃ x, x ≠ 0 ∧ ∀ (y : M), ∃ r, r • x = y
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: case mpr
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
⊢ (∃ x, x ≠ 0 ∧ ∀ (y : M), ∃ r, r • x = y) → Nonempty (Basis ι R M)

Tactic:
·

Goal state after:
case mpr
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
⊢ (∃ x, x ≠ 0 ∧ ∀ (y : M), ∃ r, r • x = y) → Nonempty (Basis ι R M)
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: case mpr.refine_1
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
y z : ι →₀ R
⊢ (y + z) default • x = y default • x + z default • x

pp: case mpr.refine_2
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
c : R
y : ι →₀ R
⊢ (c • y) default • x = (RingHom.id R) c • y default • x

pp: case mpr.refine_3
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
f : ι →₀ R
⊢ ((fun y ↦ single default ⋯.choose) ((fun f ↦ f default • x) f)) default = f default

pp: case mpr.refine_4
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
y : M
⊢ (fun f ↦ f default • x) ((fun y ↦ single default ⋯.choose) y) = y

Tactic:
·

Goal state after:
case mpr.refine_1
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
y z : ι →₀ R
⊢ (y + z) default • x = y default • x + z default • x
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: case mpr.refine_2
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
c : R
y : ι →₀ R
⊢ (c • y) default • x = (RingHom.id R) c • y default • x

pp: case mpr.refine_3
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
f : ι →₀ R
⊢ ((fun y ↦ single default ⋯.choose) ((fun f ↦ f default • x) f)) default = f default

pp: case mpr.refine_4
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
y : M
⊢ (fun f ↦ f default • x) ((fun y ↦ single default ⋯.choose) y) = y

Tactic:
·

Goal state after:
case mpr.refine_2
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTorsionFree R M
ι : Type u_9
inst✝ : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ r, r • x = y
c : R
y : ι →₀ R
⊢ (c • y) default • x = (RingHom.id R) c • y default • x