mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
v : ι → M
x✝ y : M
hli : LinearIndependent R v
x : ↥(span R (range v))
a✝ : x ∈ ⊤
this : ∀ (i : ι), v i ∈ span R (range v)
h₁ : (Subtype.val '' range fun i ↦ ⟨v i, ⋯⟩) = range v
h₂ : map (span R (range v)).subtype (span R (range fun i ↦ ⟨v i, ⋯⟩)) = span R (range v)
⊢ ↑x ∈ map (span R (range v)).subtype (span R (range fun i ↦ ⟨v i, ⋯⟩))

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
v : ι → M
x✝ y✝ : M
hli : LinearIndependent R v
x : ↥(span R (range v))
a✝ : x ∈ ⊤
this : ∀ (i : ι), v i ∈ span R (range v)
h₁ : (Subtype.val '' range fun i ↦ ⟨v i, ⋯⟩) = range v
h₂ : map (span R (range v)).subtype (span R (range fun i ↦ ⟨v i, ⋯⟩)) = span R (range v)
h₃ : ↑x ∈ map (span R (range v)).subtype (span R (range fun i ↦ ⟨v i, ⋯⟩))
y : ↥(span R (range v))
hy₁ : y ∈ span R (range fun i ↦ ⟨v i, ⋯⟩)
hy₂ : (span R (range v)).subtype y = ↑x
⊢ x = y

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
v : ι → M
x y : M
hli : LinearIndependent R v
⊢ ⊤ ≤ span R (range fun i ↦ ⟨v i, ⋯⟩)

Tactic:
by

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

Goal state before:
pp: ι : 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
i : ι
⊢ (Basis.span hli) i = ⟨v i, ⋯⟩

Tactic:
by

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

Goal state before:
pp: ι : 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
i : ι
⊢ ↑((Basis.span hli) i) = v i

Tactic:
by

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

Goal state before:
pp: ι : 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
i : ι
hi : v i ∈ span R (range v)
⊢ (Basis.span hli).repr ⟨v i, hi⟩ = single i 1

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : Type u_7
M : Type u_8
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hli : LinearIndependent R v
h : span R (range v) = span R (range (-v))
⊢ Basis.span ⋯ =
    (Basis.span hli).map (LinearEquiv.neg R ≪≫ₗ LinearEquiv.ofEq (span R (range v)) (span R (range (-v))) h)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : range ⇑b ⊆ w
x : M
p : x ∈ w
q : x ∉ range ⇑b
e : (linearCombination R ⇑b) (b.repr x) = x
i i' : ι
r : (fun i ↦ ⟨b i, ⋯⟩) i = (fun i ↦ ⟨b i, ⋯⟩) i'
⊢ b i = b i'

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent R Subtype.val
h : range ⇑b ⊆ w
⊢ range ⇑b = w

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
b✝ : Basis ι R M
v : ι → M
x y : M
inst✝ : Subsingleton R
x✝ : Basis ι R M
b : M ≃ₗ[R] ι →₀ R
⊢ { repr := b } = default

Tactic:
by

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

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁶ : Semiring R✝
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R✝ M
inst✝³ : AddCommMonoid M'
inst✝² : Module R✝ M'
b✝ : Basis ι✝ R✝ M
v : ι✝ → M
x✝ y✝ : M
b : Basis ι✝ R✝ M
ι : Type u_7
R : Type u_8
inst✝¹ : Unique ι
inst✝ : Semiring R
x y : R
⊢ single default (x + y) = single default x + single default y

Tactic:
by

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

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁶ : Semiring R✝
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R✝ M
inst✝³ : AddCommMonoid M'
inst✝² : Module R✝ M'
b✝ : Basis ι✝ R✝ M
v : ι✝ → M
x✝ y : M
b : Basis ι✝ R✝ M
ι : Type u_7
R : Type u_8
inst✝¹ : Unique ι
inst✝ : Semiring R
c x : R
⊢ single default (c • x) = (RingHom.id R) c • single default x

Tactic:
by

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

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁶ : Semiring R✝
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R✝ M
inst✝³ : AddCommMonoid M'
inst✝² : Module R✝ M'
b✝ : Basis ι✝ R✝ M
v : ι✝ → M
x✝ y : M
b : Basis ι✝ R✝ M
ι : Type u_7
R : Type u_8
inst✝¹ : Unique ι
inst✝ : Semiring R
x : R
⊢ (fun f ↦ f default) ((fun x ↦ single default x) x) = x

Tactic:
by

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

Goal state before:
pp: ι✝ : Type u_1
ι' : Type u_2
R✝ : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁶ : Semiring R✝
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R✝ M
inst✝³ : AddCommMonoid M'
inst✝² : Module R✝ M'
b✝ : Basis ι✝ R✝ M
v : ι✝ → M
x y : M
b : Basis ι✝ R✝ M
ι : Type u_7
R : Type u_8
inst✝¹ : Unique ι
inst✝ : Semiring R
f : ι →₀ R
⊢ ((fun x ↦ single default x) ((fun f ↦ f default) f)) default = f default

Tactic:
by

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

Goal state before:
pp: ι : Type u_7
R : Type u_8
inst✝¹ : Unique ι
inst✝ : Semiring R
i : ι
⊢ (Basis.singleton ι R).repr 1 = single i 1

Tactic:
by

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

Goal state before:
pp: ι : Type u_7
R : Type u_8
inst✝¹ : Unique ι
inst✝ : Semiring R
x : R
i : ι
⊢ ((Basis.singleton ι R).repr x) i = x

Tactic:
by

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

Goal state before:
pp: ι : Type u_7
R : Type u_8
inst✝¹ : Unique ι
inst✝ : Semiring R
⊢ ⇑(Basis.singleton ι R) = 1

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
⊢ ∀ (r : R) (m : M), b.repr (r • m) = r • b.repr m

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsDomain R
b : Basis ι R M
c : R
x : M
⊢ c • x = 0 ↔ c = 0 ∨ x = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype ι
⊢ LinearIndependent R v ↔ Injective ⇑(Fintype.linearCombination R v)

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
⊢ Injective v

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
i : ι
⊢ Injective fun r ↦ r • v i

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
i : ι
hv : LinearIndependent R v
h : v i = 0
⊢ (Finsupp.linearCombination R v) (Finsupp.single i 1) = (Finsupp.linearCombination R v) 0

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
i : ι
hv : LinearIndependent R v
⊢ v i ≠ 0

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : Subsingleton M
f : ι → M
⊢ LinearIndependent R f ↔ IsEmpty ι

Tactic:
by

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

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : LinearIndependent R v
f : ι' → ι
hf : Injective f
⊢ LinearIndependent R (v ∘ f)

Tactic:
by

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

Goal state before:
pp: 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

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (l₁ l₂ : ι →₀ R), (Finsupp.linearCombination R v) l₁ = (Finsupp.linearCombination R v) l₂ → l₁ = l₂
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
his : i ∈ s
⊢ (Finsupp.linearCombination R v) (∑ i ∈ s, Finsupp.single i (f i)) =
    (Finsupp.linearCombination R v) (∑ i ∈ s, Finsupp.single i (g i))

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Fintype ι
b : Basis ι R M
inst✝¹ : Fintype R
inst✝ : Fintype M
⊢ card (ι → R) = card R ^ card ι

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Fintype ι
b : Basis ι R M
inst✝¹ : Fintype R
inst✝ : Fintype M
⊢ card M = card R ^ card ι

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (l₁ l₂ : ι →₀ R), (Finsupp.linearCombination R v) l₁ = (Finsupp.linearCombination R v) l₂ → l₁ = l₂
s : Finset ι
f✝ g : ι → R
eq : ∑ i ∈ s, f✝ i • v i = ∑ i ∈ s, g i • v i
i : ι
his : i ∈ s
h : ∑ i ∈ s, Finsupp.single i (f✝ i) = ∑ i ∈ s, Finsupp.single i (g i)
f : ι → R
⊢ f i = (Finsupp.lapply i) (Finsupp.single i (f i))

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x y : ℕ∞
⊢ x ^ y = if y < ⊤ then x ^ y.toNat else if x = 0 then 0 else if x = 1 then 1 else ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: y : ℕ∞
h : y ≠ 0
⊢ 0 ^ y = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: y : ℕ∞
⊢ 1 ^ y = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: y : ℕ∞
h : y ≠ 0
⊢ ⊤ ^ y = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x : ℕ∞
⊢ x ^ 0 = 1

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (l₁ l₂ : ι →₀ R), (Finsupp.linearCombination R v) l₁ = (Finsupp.linearCombination R v) l₂ → l₁ = l₂
s : Finset ι
f✝ g : ι → R
eq : ∑ i ∈ s, f✝ i • v i = ∑ i ∈ s, g i • v i
i : ι
his : i ∈ s
h : ∑ i ∈ s, Finsupp.single i (f✝ i) = ∑ i ∈ s, Finsupp.single i (g i)
f : ι → R
j : ι
_hjs : j ∈ s
hji : j ≠ i
⊢ (Finsupp.lapply i) (Finsupp.single j (f j)) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x : ℕ∞
⊢ x ^ 1 = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x : ℕ∞
h : 1 < x
this : 0 ≤ 1
⊢ x ^ ⊤ = ⊤

Tactic:
rw [epow_def, if_neg, if_neg, if_neg]

Goal state after:
case hnc
x : ℕ∞
h : 1 < x
this : 0 ≤ 1
⊢ ¬x = 1

case hnc
x : ℕ∞
h : 1 < x
this : 0 ≤ 1
⊢ ¬x = 0

case hnc
x : ℕ∞
h : 1 < x
this : 0 ≤ 1
⊢ ¬⊤ < ⊤
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x : ℕ∞
h : 1 < x
⊢ x ^ ⊤ = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x : ℕ∞
h : x ≠ 0
⊢ Monotone fun y ↦ x ^ y

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x y : ℕ∞
h : x ≠ 0
⊢ 1 ≤ x ^ y

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x y : ℕ∞
h : x ≠ 0
⊢ 0 < x ^ y

Tactic:
rw [← Order.one_le_iff_pos]; exact one_le_epow h

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x y : ℕ∞
h : x ≠ 0
⊢ 0 < x ^ y

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: y x z : ℕ∞
x_z : x ≤ z
⊢ (fun x ↦ x ^ y) x ≤ (fun x ↦ x ^ y) z

Tactic:
simp only

Goal state after:
y x z : ℕ∞
x_z : x ≤ z
⊢ x ^ y ≤ z ^ y
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (l₁ l₂ : ι →₀ R), (Finsupp.linearCombination R v) l₁ = (Finsupp.linearCombination R v) l₂ → l₁ = l₂
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
his : i ∈ s
⊢ f i = g i

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: y : ℕ∞
⊢ Monotone fun x ↦ x ^ y

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x y : ℕ∞
⊢ x ^ y = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x y : ℕ∞
h : x = 1 ∨ y = 0
⊢ x ^ y = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x y : ℕ∞
⊢ x ^ y = 1 ↔ x = 1 ∨ y = 0

Tactic:
by

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

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
hni : x✝ ∉ f.support ∧ x✝ ∉ g.support
⊢ f x✝ = g x✝

Tactic:
Finsupp.notMem_support_iff

Goal state after:
case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
hni : f x✝ = 0 ∧ g x✝ = 0
⊢ f x✝ = g x✝
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
hni : x✝ ∉ f.support ∪ g.support
⊢ f x✝ = g x✝

Tactic:
simp_rw [notMem_union, Finsupp.notMem_support_iff] at hni

Goal state after:
case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
hni : f x✝ = 0 ∧ g x✝ = 0
⊢ f x✝ = g x✝
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ι →₀ R
hl : (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g
x✝ : ι
⊢ f x✝ = g x✝

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x y z : ℕ∞
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
H :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s
⊢ ∑ i ∈ s, (if i ∈ s then f i else 0) • v i = ∑ i ∈ s, (if i ∈ s then g i else 0) • v i

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x y z : ℕ∞
⊢ (x * y) ^ z = x ^ z * y ^ z

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
H :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s
⊢ f i = g i

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin n → M
⊢ (List.ofFn f).prod = ∏ i, f i

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ LinearIndependent R v ↔
    ∀ (s : Finset ι) (f g : ι → R),
      (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin n → M
⊢ ∏ i, f i = (List.map f (List.finRange n)).prod

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ¬LinearIndependent R v ↔ ∃ s f g, ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i ∧ ∃ i ∈ s, f i ≠ g i

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
x : Fin (n + 1)
⊢ ∏ i, f i = f x * ∏ i, f (x.succAbove i)

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
⊢ ∏ i, f i = (∏ i, f i.castSucc) * f (last n)

Tactic:
simpa [mul_comm] using prod_univ_succAbove f (last n)

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
⊢ ∏ i, f i = (∏ i, f i.castSucc) * f (last n)

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype ι
⊢ LinearIndependent R v ↔ ∀ (f g : ι → R), ∑ i, f i • v i = ∑ i, g i • v i → ∀ (i : ι), f i = g i

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
l : List M
⊢ ∏ i, l[↑i] = l.prod

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype ι
⊢ LinearIndependent R v ↔ ∀ (f g : ι → R), ∑ i, f i • v i = ∑ i, g i • v i → ∀ (i : ι), f i = g i

Tactic:
by
  simp_rw [linearIndependent_iff_injective_fintypeLinearCombination,
    Injective, Fintype.linearCombination_apply, funext_iff]

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝ : CommMonoid M
l : List ι
f : ι → M
⊢ ∏ i, f l[↑i] = (List.map f l).prod

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
x : M
f : Fin n → M
⊢ ∏ i, cons x f i = x * ∏ i, f i

Tactic:
by

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x y z : ℕ∞
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
x : M
f : Fin n → M
⊢ ∏ i, snoc f x i = (∏ i, f i) * x

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : Fin 1 → M
⊢ ∏ i, f i = f 0

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : Fin 2 → M
⊢ ∏ i, f i = f 0 * f 1

Tactic:
by

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype ι
⊢ ¬LinearIndependent R v ↔ ∃ f g, ∑ i, f i • v i = ∑ i, g i • v i ∧ ∃ i, f i ≠ g i

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : Fin 3 → M
⊢ ∏ i, f i = f 0 * f 1 * f 2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b p : M
⊢ a ≡ b [PMOD p] ↔ ∃ m n, m • p + a = n • p + b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
p a : M
⊢ 0 • p + a = 0 • p + a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b p : M
h : a ≡ b [PMOD p]
⊢ b ≡ a [PMOD p]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b c p : M
hab : a ≡ b [PMOD p]
hbc : b ≡ c [PMOD p]
⊢ a ≡ c [PMOD p]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a b : M
⊢ a ≡ b [PMOD 0] ↔ a = b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
p : M
⊢ 0 • p + p = 1 • p + 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a p : M
n : ℕ
⊢ 0 • p + (a + n • p) = n • p + a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
a p : M
n : ℕ
⊢ 0 • p + (n • p + a) = n • p + a

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : Fin 4 → M
⊢ ∏ i, f i = f 0 * f 1 * f 2 * f 3

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : Fin 5 → M
⊢ ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4

Tactic:
by

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
f : Fin 6 → M
⊢ ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5

Tactic:
by

Goal state after: