mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.BigOperators.Ring.List

Goal state before:
pp: α : Type u_2
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : α
xs : List α
⊢ 0 < x * xs.prod ↔ 0 < x ∧ ∀ (x : α), x ∈ xs → 0 < x

Tactic:
CanonicallyOrderedAdd.mul_pos,

Goal state after:
α : Type u_2
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : α
xs : List α
⊢ 0 < x ∧ 0 < xs.prod ↔ 0 < x ∧ ∀ (x : α), x ∈ xs → 0 < x
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
x : α →₀ M
a : α
h : ¬(mapDomain (⇑f) x) (f a) = 0
⊢ ¬x a = 0 ∧ f a = f a

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α ↪ β
x : α →₀ M
a : α
h : ¬(mapDomain (⇑f) x) (f a) = 0
⊢ ¬x a = 0
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
⊢ ∑ a_1 ∈ x.support, (single (f a_1) (x a_1)) (f a) = x a

Tactic:
single_apply

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : ↑x.support ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
⊢ (∑ x_1 ∈ x.support, if f x_1 = f a then x x_1 else 0) = x a
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
a a✝ : α
⊢ (if a = a✝ then f a✝ else 0) = (single a (f a)) a✝

Tactic:
single_apply

Goal state after:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
a a✝ : α
⊢ (if a = a✝ then f a✝ else 0) = if a = a✝ then f a else 0
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α : Type u_1
M : Type u_5
N : Type u_6
inst✝² : Zero M
p : α → Prop
inst✝¹ : DecidablePred p
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
⊢ (filter p f).prod g = ∏ x ∈ (filter p f).support, g x (f x)

Tactic:
refine Finset.prod_congr rfl fun x hx => ?_

Goal state after:
α : Type u_1
M : Type u_5
N : Type u_6
inst✝² : Zero M
p : α → Prop
inst✝¹ : DecidablePred p
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
x : α
hx : x ∈ (filter p f).support
⊢ g x ((filter p f) x) = g x (f x)
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : Preorder N
f : ι → N
s : Finset ι
inst✝ : MulLeftMono N
i j : ι
hf : ∀ i ∈ s, 1 ≤ f i
hi : i ∈ s
hj : j ∈ s
hne : i ≠ j
⊢ ∏ k ∈ cons i {j} ⋯, f k ≤ ∏ k ∈ s, f k

Tactic:
by
      refine prod_le_prod_of_subset_of_one_le' ?_ fun k hk _ ↦ hf k hk
      simp [cons_subset, *]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: case refine_1
ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : Preorder N
inst✝ : MulLeftMono N
s : Finset ι
f : ι → N
n : N
h : ∀ x ∈ s, f x ≤ n
⊢ ∀ x ∈ Multiset.map f s.val, x ≤ n

Tactic:
simpa using

Goal state after:
case refine_1
ι : Type u_1
N : Type u_5
inst✝² : CommMonoid N
inst✝¹ : Preorder N
inst✝ : MulLeftMono N
s : Finset ι
f : ι → N
n : N
h : ∀ x ∈ s, f x ≤ n
⊢ ∀ a ∈ s, f a ≤ n
Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : ∑ i ∈ s, g i = 0
i : ι
hi : i ∈ s
⊢ r i = 0

Tactic:
simpa using

Goal state after:
ι : Type u_1
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 ≤ f i * g i
h : ∑ i ∈ s, g i = 0
i : ι
hi : i ∈ s
⊢ r i = 0
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : DecidableEq ι
⊢ Disjoint (t \ s) (s ∩ t)

Tactic:
simpa using

Goal state after:
ι : Type u_1
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : Preorder M
inst✝¹ : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst✝ : DecidableEq ι
⊢ Disjoint (t \ s) (s ∩ t)
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : DecidableEq β
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
t : β
⊢ ¬(mapDomain f x) t = 0 → ∃ a ∈ x.support, f a = t

Tactic:
simpa using

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : DecidableEq β
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
t : β
⊢ ∀ (x_1 : α), ¬x x_1 = 0 → f x_1 = t → ¬x x_1 = 0 → ∃ a, ¬x a = 0 ∧ f a = t
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : DecidableEq β
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
t : β
x✝ : ∃ a ∈ x.support, f a = t
i : α
i_in : i ∈ x.support
hi : f i = t
⊢ ¬(mapDomain f x) t = 0

Tactic:
simpa using

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
M : Type u_5
inst✝² : DecidableEq β
inst✝¹ : AddCommMonoid M
f : α → β
inst✝ : Subsingleton (AddUnits M)
x : α →₀ M
t : β
x✝ : ∃ a ∈ x.support, f a = t
i : α
i_in : i ∈ x.support
hi : f i = t
⊢ ∃ x_1, ¬x x_1 = 0 ∧ f x_1 = f i ∧ ¬x x_1 = 0
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_9
M : Type u_10
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ Disjoint (t \ s) (s ∩ t)

Tactic:
simpa using

Goal state after:
ι : Type u_9
M : Type u_10
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ Disjoint (t \ s) (s ∩ t)
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : SemilatticeSup α
inst✝³ : OrderBot α
inst✝² : AddCommMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
f : α → β
zero : f ⊥ = 0
ih : ∀ {s t : α}, f (s ⊔ t) ≤ f s + f t
s : ι → α
t✝ : Finset ι
i : ι
t : Finset ι
it : i ∉ t
h : f (t.sup s) ≤ ∑ i ∈ t, f (s i)
⊢ f ((insert i t).sup s) ≤ ∑ i ∈ insert i t, f (s i)

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : SemilatticeSup α
inst✝³ : OrderBot α
inst✝² : AddCommMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
f : α → β
zero : f ⊥ = 0
ih : ∀ {s t : α}, f (s ⊔ t) ≤ f s + f t
s : ι → α
t✝ : Finset ι
i : ι
t : Finset ι
it : i ∉ t
h : f (t.sup s) ≤ ∑ i ∈ t, f (s i)
⊢ f (s i ⊔ t.sup s) ≤ f (s i) + ∑ i ∈ t, f (s i)
Module: Mathlib.Data.Finsupp.SMul

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst✝³ : Nonempty α
inst✝² : Zero M
inst✝¹ : SMulZeroClass R M
inst✝ : FaithfulSMul R M
m₁✝ m₂✝ : R
h : ∀ (a : α →₀ M), m₁✝ • a = m₂✝ • a
a : α
m : M
⊢ m₁✝ • m = m₂✝ • m

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
G : Type u_5
R : Type u_6
inst✝³ : Nonempty α
inst✝² : Zero M
inst✝¹ : SMulZeroClass R M
inst✝ : FaithfulSMul R M
m₁✝ m₂✝ : R
h : ∀ (a : α →₀ M), m₁✝ • a = m₂✝ • a
a : α
m : M
⊢ m₁✝ • m = m₂✝ • m
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
hf : 1 < f
⊢ ∃ i ∈ Finset.univ, 1 < f i

Tactic:
simpa using

Goal state after:
ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
hf : 1 < f
⊢ ∃ i, 1 < f i
Module: Mathlib.Algebra.Order.BigOperators.Group.Finset

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
hf : f < 1
⊢ ∃ i ∈ Finset.univ, f i < 1

Tactic:
simpa using

Goal state after:
ι : Type u_1
M : Type u_4
inst✝³ : Fintype ι
inst✝² : CommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedCancelMonoid M
f : ι → M
hf : f < 1
⊢ ∃ i, f i < 1
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
R : Type u_5
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : α
s : Set α
h : ↑{a} ⊆ s
⊢ a ∈ s

Tactic:
simpa using

Goal state after:
α : Type u_1
R : Type u_5
inst✝¹ : Semiring R
inst✝ : Nontrivial R
a : α
s : Set α
h : ↑{a} ⊆ s
⊢ a ∈ s
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: case neg
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
l : ↥(supported M R s)
a : α
h : a ∉ s
⊢ ↑((restrictDom M R s ∘ₗ (supported M R s).subtype) l) a = ↑(LinearMap.id l) a

Tactic:
simpa using

Goal state after:
case neg
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
l : ↥(supported M R s)
a : α
h : a ∉ s
⊢ 0 = ↑l a
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial M
s t : Set α
h : ∀ (x : α →₀ M), x ∈ supported M R (s ∪ t)
a : α
x : M
hx : x ≠ 0
⊢ a ∈ ⊤ → a ∈ s ⊔ t

Tactic:
simpa using

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial M
s t : Set α
h : ∀ (x : α →₀ M), x ∈ supported M R (s ∪ t)
a : α
x : M
hx : x ≠ 0
⊢ a ∈ s ∨ a ∈ t
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
x : PLift α
⊢ x ∉ ↑{{ down := a }} → x ∉ mulSupport (f ∘ PLift.down)

Tactic:
simpa using

Goal state after:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
x : PLift α
⊢ ¬x.down = a → f x.down = 1
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
h✝ : Nonempty α
l : α' →₀ M
hl : l ∈ supported M R (f '' s)
c : α'
hc : c ∈ l.support
hx : Function.invFunOn f s c ∈ ↑((lmapDomain M R (Function.invFunOn f s)) l).support
⊢ ∃ a ∈ s, f a = c

Tactic:
simpa using

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
h✝ : Nonempty α
l : α' →₀ M
hl : l ∈ supported M R (f '' s)
c : α'
hc : c ∈ l.support
hx : Function.invFunOn f s c ∈ ↑((lmapDomain M R (Function.invFunOn f s)) l).support
⊢ ∃ a ∈ s, f a = c
Module: Mathlib.LinearAlgebra.Finsupp.Supported

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
h✝ : Nonempty α
l : α' →₀ M
hl : l ∈ supported M R (f '' s)
c : α'
hc : c ∈ l.support
⊢ ∃ a ∈ s, f a = c

Tactic:
simpa using

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α' : Type u_7
f : α → α'
s : Set α
h✝ : Nonempty α
l : α' →₀ M
hl : l ∈ supported M R (f '' s)
c : α'
hc : c ∈ l.support
⊢ ∃ a ∈ s, f a = c
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ val '' uIoc i j = uIoc ↑i ↑j

Tactic:
by simp [uIoc]

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 α
inst✝ : Fintype ↑s
⊢ s ∩ mulSupport f = ↑s.toFinset ∩ mulSupport f

Tactic:
simp_rw [coe_toFinset s]

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
⊢ Disjoint {a} s

pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
a : α
s : Set α
f : α → M
h : a ∉ s
hs : (s ∩ mulSupport f).Finite
⊢ ({a} ∩ mulSupport f).Finite

Tactic:
· rwa [disjoint_singleton_left]

Goal state after:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
a : α
s : Set α
f : α → M
h : a ∉ s
hs : (s ∩ mulSupport f).Finite
⊢ ({a} ∩ mulSupport f).Finite
Module: Mathlib.Logic.Equiv.Fin.Basic

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

Tactic:
simpa using

Goal state after:
n : ℕ
p : Fin (n + 1)
h : p ≠ Fin.last n
x : { x // x ≠ p }
⊢ ↑x = p.succAbove ((p.castLT ⋯).predAbove ↑x)
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ i < (finRotate (n + 1)) i ↔ i ≠ Fin.last n

Tactic:
simpa using

Goal state after:
n : ℕ
i : Fin (n + 1)
⊢ i < Fin.last n ↔ ¬i = Fin.last n
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
p : Submodule R M
h : range ⇑b ⊆ ↑p
⊢ p = ⊤

Tactic:
simpa using

Goal state after:
ι : 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
p : Submodule R M
h : range ⇑b ⊆ ↑p
⊢ p = ⊤
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
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
inst✝² : Semiring R₂
inst✝¹ : Module R₂ M'
inst✝ : SMulCommClass R R₂ M'
v : ι → M'
hv : LinearIndependent R v
x✝¹ x✝ : M
hab : ((b.constr R₂) v) x✝¹ = ((b.constr R₂) v) x✝
⊢ (linearCombination R v) (b.repr x✝¹) = (linearCombination R v) (b.repr x✝)

Tactic:
simpa using

Goal state after:
ι : Type u_1
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
inst✝² : Semiring R₂
inst✝¹ : Module R₂ M'
inst✝ : SMulCommClass R R₂ M'
v : ι → M'
hv : LinearIndependent R v
x✝¹ x✝ : M
hab : ((b.constr R₂) v) x✝¹ = ((b.constr R₂) v) x✝
⊢ (linearCombination R v) (b.repr x✝¹) = (linearCombination R v) (b.repr x✝)
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_5
inst✝² : AddCommMonoid M
R : Type u_7
inst✝¹ : CommSemiring R
inst✝ : Module R M
b : Basis ι R M
s : Finset ι
l₁ l₂ : ι → R
h : ∑ i ∈ s, l₁ i • b.coord i = ∑ i ∈ s, l₂ i • b.coord i
j : ι
hj : j ∈ s
⊢ l₁ j = l₂ j

Tactic:
simpa using

Goal state after:
ι : Type u_1
M : Type u_5
inst✝² : AddCommMonoid M
R : Type u_7
inst✝¹ : CommSemiring R
inst✝ : Module R M
b : Basis ι R M
s : Finset ι
l₁ l₂ : ι → R
h : ∑ i ∈ s, l₁ i • b.coord i = ∑ i ∈ s, l₂ i • b.coord i
j : ι
hj : j ∈ s
⊢ l₁ j = l₂ j
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
hsp : ⊤ ≤ span R (range v)
inst✝ : DecidableEq ι
i j : ι
⊢ ((Basis.mk hli hsp).coord i) (v j) = if j = i then 1 else 0

Tactic:
rcases eq_or_ne j i with h | h
  · simp only [h, if_true, mk_coord_apply_eq i]
  · simp only [h, if_false, mk_coord_apply_ne h]

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:
simpa using

Goal state after:
ι : 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'
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 ι
b : Basis ι R M
⊢ ∀ (y : M), ∃ r, r • b default = y

Tactic:
simpa using

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 ι
b : Basis ι R M
⊢ ∀ (y : M), ∃ r, r • b default = 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
inst✝ : Nontrivial R
hv : LinearIndependent R v
⊢ Injective v

Tactic:
simpa using

Goal state after:
ι : 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
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:
simpa using

Goal state after:
ι : 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
⊢ v i = 0
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:
simpa using

Goal state after:
ι : 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
⊢ ∑ x ∈ s, f x • v x = ∑ x ∈ s, g x • v x
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case coe
x : ℕ∞
n : ℕ
⊢ x ^ ↑n = if ↑n < ⊤ then x ^ (↑n).toNat else if x = 0 then 0 else if x = 1 then 1 else ⊤

Tactic:
| coe n =>

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

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

Tactic:
simpa using

Goal state after:
x y : ℕ∞
h : x ≠ 0
⊢ 1 ≤ x ^ y
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 using

Goal state after:
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → M
⊢ ∏ i, f i = f (last n) * ∏ i, f i.castSucc
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:
simpa using

Goal state after:
ι : 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
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
s : Finset ι
⊢ (LinearIndependent R fun (x : ↑↑s) ↦ v ↑x) ↔
    ∀ (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i

Tactic:
Fintype.linearIndependent_iffₛ

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

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

Tactic:
simpa using

Goal state after:
case mpr
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
hv : ∀ (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
f g : ↑↑s → R
hfg : ∑ i, f i • v ↑i = ∑ i, g i • v ↑i
i : ↑↑s
⊢ f i = g i
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
s : Finset ι
⊢ ¬LinearIndepOn R v ↑s ↔ ∃ f g, ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i ∧ ∃ i ∈ s, f i ≠ g i

Tactic:
simpa using

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
⊢ ¬LinearIndepOn R v ↑s ↔ ∃ f g, ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i ∧ ∃ i ∈ s, ¬f i = g i
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case h
M : Type u_1
inst✝³ : AddCommMonoid M
a b p : M
N : Type u_2
F : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
m n : ℕ
h : m • p + a = n • p + b
⊢ m • f p + f a = n • f p + f b

Tactic:
simpa using

Goal state after:
case h
M : Type u_1
inst✝³ : AddCommMonoid M
a b p : M
N : Type u_2
F : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
m n : ℕ
h : m • p + a = n • p + b
⊢ m • f p + f a = n • f p + f b
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCancelCommMonoid M
a b c d p : M
h : c ≡ d [PMOD p]
⊢ a + c ≡ b + d [PMOD p] ↔ a ≡ b [PMOD p]

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝ : AddCancelCommMonoid M
a b c d p : M
h : c ≡ d [PMOD p]
⊢ a + c ≡ b + d [PMOD p] ↔ a ≡ b [PMOD p]
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: M : Type u_1
inst✝ : AddCancelCommMonoid M
a b p : M
⊢ a + b ≡ a [PMOD p] ↔ b ≡ 0 [PMOD p]

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝ : AddCancelCommMonoid M
a b p : M
⊢ a + b ≡ a [PMOD p] ↔ b ≡ 0 [PMOD p]
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a ↦ a • v i) = g.sum fun i a ↦ a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a ↦ a • v ↑i) = l₂.sum fun i a ↦ a • v ↑i
⊢ ∀ x ∈ (Finsupp.embDomain (Embedding.subtype fun x ↦ x ∈ s) l₁).support, x ∈ s

Tactic:
simpa using

Goal state after:
case refine_1
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a ↦ a • v i) = g.sum fun i a ↦ a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a ↦ a • v ↑i) = l₂.sum fun i a ↦ a • v ↑i
⊢ ∀ (x : ι) (x_1 : x ∈ s), ¬l₁ ⟨x, ⋯⟩ = 0 → x ∈ s