mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: case inl.inr
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x : δ ⟨i, j⟩.fst ⟨i, j⟩.snd
j' : α i
hj : j' ≠ j
⊢ ⟨i, j'⟩ ≠ ⟨i, j⟩

Tactic:
simpa using

Goal state after:
case inl.inr
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x : δ ⟨i, j⟩.fst ⟨i, j⟩.snd
j' : α i
hj : j' ≠ j
⊢ ¬j' = j
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : (i : ι) → β i
s : Multiset ι
h : ∀ (i : ι), i ∈ s ∨ f i = 0
i : ι
H : i ∈ { toFun := f, support' := Trunc.mk ⟨s, h⟩ }.support
⊢ i ∈ s.toFinset.val.toFinset

Tactic:
simpa using

Goal state after:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : (i : ι) → β i
s : Multiset ι
h : ∀ (i : ι), i ∈ s ∨ f i = 0
i : ι
H : i ∈ { toFun := f, support' := Trunc.mk ⟨s, h⟩ }.support
⊢ i ∈ s
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case h
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : (i : ι) → β i
s : { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
⊢ i ∈ { toFun := f, support' := Trunc.mk s }.support ↔ { toFun := f, support' := Trunc.mk s } i ≠ 0

Tactic:
dsimp only [support, Trunc.lift_mk]

Goal state after:
case h
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
f : (i : ι) → β i
s : { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
⊢ i ∈ {i ∈ (↑s).toFinset | { toFun := f, support' := Trunc.mk s } i ≠ 0} ↔ { toFun := f, support' := Trunc.mk s } i ≠ 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
⊢ ↑((fun f_1 ↦ ⟨mk f.support fun i ↦ ↑(f_1 i), ⋯⟩)
          ((fun x ↦
              match (motive := { f_1 // f_1.support = f.support } → (i : ↥f.support) → { x // x ≠ 0 }) x with
              | ⟨f_1, hf⟩ => fun x ↦
                match x with
                | ⟨i, hi⟩ => ⟨f_1 i, ⋯⟩)
            ⟨f, ⋯⟩))
      i =
    ↑⟨f, ⋯⟩ i

Tactic:
simpa using

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
⊢ f i = 0 → 0 = f i
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
H : f.support = ∅
⊢ ∀ (i : ι), f i = 0 i

Tactic:
simpa using

Goal state after:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
H : f.support = ∅
⊢ ∀ (i : ι), f i = 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β i) → Decidable (x = 0)
f : Π₀ (i : ι), β i
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
⊢ (∀ i ∈ ↑s, f i = 0) → f = 0

Tactic:
intro hs₁; ext i
        -- This instance prevent consuming `DecidableEq ι` in the next `by_cases`.
        let := Classical.propDecidable
        by_cases hs₂ : i ∈ s.val
        case pos => exact hs₁ _ hs₂
        case neg => exact (s.prop i).resolve_left hs₂

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
s : Set ι
f : Π₀ (i : ι), β i
⊢ ↑f.support ⊆ s ↔ ∀ i ∉ s, f i = 0

Tactic:
simpa using

Goal state after:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
s : Set ι
f : Π₀ (i : ι), β i
⊢ (∀ (x : ι), ¬f x = 0 → x ∈ s) ↔ ∀ i ∉ s, f i = 0
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: case inl.inr
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → (j : α i) → Zero (δ i j)
inst✝ : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
j' : α i
hj : j' ≠ j
⊢ ⟨i, j'⟩ ≠ ⟨i, j⟩

Tactic:
simpa using

Goal state after:
case inl.inr
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → (j : α i) → Zero (δ i j)
inst✝ : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
j' : α i
hj : j' ≠ j
⊢ ¬j' = j
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
i : ι
b : β₁ i
i' : ι
⊢ (mapRange f hf (single i b)) i' = (single i (f i b)) i'

Tactic:
by_cases h : i = i'
    · subst i'
      simp
    · simp [h, hf]

Goal state after:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝⁵ : DecidableEq ι
ι₁ : Type u₁
inst✝⁴ : DecidableEq ι₁
β₁ : ι₁ → Type v₁
inst✝³ : (i₁ : ι₁) → Zero (β₁ i₁)
inst✝² : (i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i₁ : ι₁), β₁ i₁
g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i
this : ∀ (i₁ : ι), (f.sum fun i b ↦ (g i b) i₁) ≠ 0 → ∃ i, f i ≠ 0 ∧ ¬(g i (f i)) i₁ = 0
⊢ (f.sum g).support ⊆ f.support.biUnion fun i ↦ (g i (f i)).support

Tactic:
simpa using

Goal state after:
ι : Type u
β : ι → Type v
inst✝⁵ : DecidableEq ι
ι₁ : Type u₁
inst✝⁴ : DecidableEq ι₁
β₁ : ι₁ → Type v₁
inst✝³ : (i₁ : ι₁) → Zero (β₁ i₁)
inst✝² : (i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i₁ : ι₁), β₁ i₁
g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i
this : ∀ (i₁ : ι), (f.sum fun i b ↦ (g i b) i₁) ≠ 0 → ∃ i, f i ≠ 0 ∧ ¬(g i (f i)) i₁ = 0
⊢ ∀ ⦃x : ι⦄, ¬(f.sum fun i₁ b ↦ (g i₁ b) x) = 0 → ∃ a, ¬f a = 0 ∧ ¬(g a (f a)) x = 0
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : (x : ι) × α x), δ i.fst i.snd
i : ι
j : α i
⊢ f.sigmaCurry.sigmaUncurry ⟨i, j⟩ = f ⟨i, j⟩

Tactic:
sigmaUncurry_apply,

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : (x : ι) × α x), δ i.fst i.snd
i : ι
j : α i
⊢ (f.sigmaCurry i) j = f ⟨i, j⟩
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
h : Function.Injective (mapRange f hf)
i : ι
x y : β₁ i
eq : f i x = f i y
⊢ mapRange f hf (single i x) = mapRange f hf (single i y)

Tactic:
simpa using

Goal state after:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
h : Function.Injective (mapRange f hf)
i : ι
x y : β₁ i
eq : f i x = f i y
⊢ single i (f i x) = single i (f i y)
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
h : Function.Surjective (mapRange f hf)
i : ι
u : β₂ i
x : Π₀ (i : ι), β₁ i
hx : mapRange f hf x = single i u
⊢ f i (x i) = u

Tactic:
simpa using

Goal state after:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
h : Function.Surjective (mapRange f hf)
i : ι
u : β₂ i
x : Π₀ (i : ι), β₁ i
hx : mapRange f hf x = single i u
⊢ f i (x i) = u
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
⊢ ∏ i ∈ v.support, f i (v i) = ∏ i, f i (v i)

Tactic:
apply Finset.prod_subset v.support.subset_univ

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : CommMonoid γ
v : Π₀ (i : ι), β i
f : (i : ι) → β i → γ
hf : ∀ (i : ι), f i 0 = 1
⊢ ∀ x ∈ Finset.univ, x ∉ v.support → f x (v x) = 1
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
i : ι
φ : ZeroHom (β i) γ
f : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
hi : i ∉ sf.toFinset
⊢ i ∉ sf

Tactic:
simpa using

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
i : ι
φ : ZeroHom (β i) γ
f : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
hi : i ∉ sf.toFinset
⊢ i ∉ sf
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: case mk.mk
ι₁ : Type u_4
ι₂ : Type u_5
β₁ : ι₁ → Type u_1
β₂ : ι₂ → Type u_2
γ : Type u_3
inst✝⁴ : DecidableEq ι₁
inst✝³ : DecidableEq ι₂
inst✝² : (i : ι₁) → AddZeroClass (β₁ i)
inst✝¹ : (i : ι₂) → AddZeroClass (β₂ i)
inst✝ : AddCommMonoid γ
h : (i : ι₁) → (j : ι₂) → β₁ i →+ β₂ j →+ γ
f₁ : (i : ι₁) → β₁ i
support'✝¹ : Trunc { s // ∀ (i : ι₁), i ∈ s ∨ f₁ i = 0 }
s₁ : Multiset ι₁
h₁ : ∀ (i : ι₁), i ∈ s₁ ∨ f₁ i = 0
f₂ : (i : ι₂) → β₂ i
support'✝ : Trunc { s // ∀ (i : ι₂), i ∈ s ∨ f₂ i = 0 }
s₂ : Multiset ι₂
h₂ : ∀ (i : ι₂), i ∈ s₂ ∨ f₂ i = 0
⊢ (sumAddHom fun i₂ ↦ (sumAddHom fun i₁ ↦ h i₁ i₂) { toFun := f₁, support' := Quot.mk ⇑trueSetoid ⟨s₁, h₁⟩ })
      { toFun := f₂, support' := Quot.mk ⇑trueSetoid ⟨s₂, h₂⟩ } =
    (sumAddHom fun i₁ ↦ (sumAddHom fun i₂ ↦ (h i₁ i₂).flip) { toFun := f₂, support' := Quot.mk ⇑trueSetoid ⟨s₂, h₂⟩ })
      { toFun := f₁, support' := Quot.mk ⇑trueSetoid ⟨s₁, h₁⟩ }

Tactic:
simpa using

Goal state after:
case mk.mk
ι₁ : Type u_4
ι₂ : Type u_5
β₁ : ι₁ → Type u_1
β₂ : ι₂ → Type u_2
γ : Type u_3
inst✝⁴ : DecidableEq ι₁
inst✝³ : DecidableEq ι₂
inst✝² : (i : ι₁) → AddZeroClass (β₁ i)
inst✝¹ : (i : ι₂) → AddZeroClass (β₂ i)
inst✝ : AddCommMonoid γ
h : (i : ι₁) → (j : ι₂) → β₁ i →+ β₂ j →+ γ
f₁ : (i : ι₁) → β₁ i
support'✝¹ : Trunc { s // ∀ (i : ι₁), i ∈ s ∨ f₁ i = 0 }
s₁ : Multiset ι₁
h₁ : ∀ (i : ι₁), i ∈ s₁ ∨ f₁ i = 0
f₂ : (i : ι₂) → β₂ i
support'✝ : Trunc { s // ∀ (i : ι₂), i ∈ s ∨ f₂ i = 0 }
s₂ : Multiset ι₂
h₂ : ∀ (i : ι₂), i ∈ s₂ ∨ f₂ i = 0
⊢ ∑ x ∈ s₂.toFinset,
      ∑ x_1 ∈ s₁.toFinset,
        ((h x_1 x) ({ toFun := f₁, support' := Quot.mk ⇑trueSetoid ⟨s₁, h₁⟩ } x_1))
          ({ toFun := f₂, support' := Quot.mk ⇑trueSetoid ⟨s₂, h₂⟩ } x) =
    ∑ i ∈ s₁.toFinset,
      ∑ x ∈ s₂.toFinset,
        ((h i x) ({ toFun := f₁, support' := Quot.mk ⇑trueSetoid ⟨s₁, h₁⟩ } i))
          ({ toFun := f₂, support' := Quot.mk ⇑trueSetoid ⟨s₂, h₂⟩ } x)
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁸ : CommSemiring K
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module K V
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : IsReflexive R M
r : R
hr : IsRegular r
m₁ m₂ : M
hm : (fun x ↦ r • x) m₁ = (fun x ↦ r • x) m₂
n : Dual R M
⊢ ((Dual.eval R M) m₁) n = ((Dual.eval R M) m₂) n

Tactic:
simpa using

Goal state after:
K : Type u_1
V : Type u_2
inst✝⁸ : CommSemiring K
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module K V
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : IsReflexive R M
r : R
hr : IsRegular r
m₁ m₂ : M
hm : (fun x ↦ r • x) m₁ = (fun x ↦ r • x) m₂
n : Dual R M
⊢ n m₁ = n m₂
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : LinearIndependent R ![x, y]
s t : R
h' : s • x = t • y
⊢ s • x + 0 • y = 0 • x + t • y

Tactic:
simpa using

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : LinearIndependent R ![x, y]
s t : R
h' : s • x = t • y
⊢ s • x = t • y
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
s t : R
h' : s • x + t • y = 0
h : Finsupp.single 0 s + Finsupp.single 1 t = 0
⊢ s = 0

Tactic:
simpa using

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
s t : R
h' : s • x + t • y = 0
h : Finsupp.single 0 s + Finsupp.single 1 t = 0
⊢ s = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
s t : R
h' : s • x + t • y = 0
h : Finsupp.single 0 s + Finsupp.single 1 t = 0
⊢ t = 0

Tactic:
simpa using

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
s t : R
h' : s • x + t • y = 0
h : Finsupp.single 0 s + Finsupp.single 1 t = 0
⊢ t = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

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 : Set (Set ι)
hs : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v a
⊢ ∀ (i : ↑s), LinearIndepOn R v ↑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 : Set (Set ι)
hs : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v a
⊢ ∀ a ∈ s, LinearIndepOn R v a
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝² : Semiring R
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₂ i)
inst✝ : (i : ι) → Module R (β₂ i)
x✝ : Π₀ (i : ι), β₂ i
i✝ : ι
⊢ ((linearMap fun i ↦ LinearMap.id) x✝) i✝ = (LinearMap.id x✝) i✝

Tactic:
simp [linearMap]

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

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
η : Type u_6
s : Set η
t : η → Set ι
hs : DirectedOn (t ⁻¹'o fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v (t a)
⊢ ∀ (i : ↑s), LinearIndepOn R v (t ↑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
η : Type u_6
s : Set η
t : η → Set ι
hs : DirectedOn (t ⁻¹'o fun x1 x2 ↦ x1 ⊆ x2) s
h : ∀ a ∈ s, LinearIndepOn R v (t a)
⊢ ∀ a ∈ s, LinearIndepOn R v (t a)
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
this :
  linearCombination R (Sum.elim (⇑(inl R M M') ∘ v) (⇑(inr R M M') ∘ v')) =
    (linearCombination R v).prodMap (linearCombination R v') ∘ₗ ↑(sumFinsuppLEquivProdFinsupp R)
⊢ Injective ⇑((linearCombination R v).prodMap (linearCombination R v') ∘ₗ ↑(sumFinsuppLEquivProdFinsupp R))

Tactic:
simpa using

Goal state after:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
this :
  linearCombination R (Sum.elim (⇑(inl R M M') ∘ v) (⇑(inr R M M') ∘ v')) =
    (linearCombination R v).prodMap (linearCombination R v') ∘ₗ ↑(sumFinsuppLEquivProdFinsupp R)
⊢ Injective ⇑(linearCombination R v) ∧ Injective ⇑(linearCombination R v')
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
indep : Set ι → Prop := fun s ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I // indep I }
r : X → X → Prop := fun I J ↦ ↑I ⊆ ↑J
c : Set X
hc : IsChain r c
⊢ LinearIndepOn R v (⋃ I ∈ c, ↑I)

Tactic:
rw [linearIndepOn_iffₛ]

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
indep : Set ι → Prop := fun s ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I // indep I }
r : X → X → Prop := fun I J ↦ ↑I ⊆ ↑J
c : Set X
hc : IsChain r c
⊢ ∀ f ∈ Finsupp.supported R R (⋃ I ∈ c, ↑I),
    ∀ g ∈ Finsupp.supported R R (⋃ I ∈ c, ↑I),
      (Finsupp.linearCombination R v) f = (Finsupp.linearCombination R v) g → f = g
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
h : Function.Injective ⇑((lsum ℕ) fun i ↦ (p i).subtype)
i : ι
x : ↥(p i)
v : Π₀ (i : ι), ↥(p i)
hv : ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ((lsum ℕ) fun i ↦ (p i).subtype) (single i x)
this : (erase i v) i = (single i x) i
⊢ x = 0

Tactic:
simpa [eq_comm] using! this

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

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
f : ι → M
hij : i ≠ j
c d : R
h :
  ↑{i, j} ⊆ {i, j} →
    (∀ i_1 ∉ {i, j}, (Pi.single i c + Pi.single j d) i_1 = 0) →
      ∑ i_1 ∈ {i, j}, (Pi.single i c + Pi.single j d) i_1 • f i_1 = 0 →
        ∀ i_1 ∈ {i, j}, (Pi.single i c + Pi.single j d) i_1 = 0
hcd : c • f i + d • f j = 0
⊢ c = 0 ∧ d = 0

Tactic:
simpa using

Goal state after:
case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
f : ι → M
hij : i ≠ j
c d : R
h :
  ↑{i, j} ⊆ {i, j} →
    (∀ i_1 ∉ {i, j}, (Pi.single i c + Pi.single j d) i_1 = 0) →
      ∑ i_1 ∈ {i, j}, (Pi.single i c + Pi.single j d) i_1 • f i_1 = 0 →
        ∀ i_1 ∈ {i, j}, (Pi.single i c + Pi.single j d) i_1 = 0
hcd : c • f i + d • f j = 0
⊢ c = 0 ∧ d = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : ↑t ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : ∑ i ∈ t, g i • f i = 0
ht' : t ⊆ {i, j}
⊢ ∀ i ∈ t, g i = 0

Tactic:
Finset.sum_subset ht',

Goal state after:
case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : ↑t ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : ∑ x ∈ {i, j}, g x • f x = 0
ht' : t ⊆ {i, j}
⊢ ∀ i ∈ t, g i = 0

case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : ↑t ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : ∑ i ∈ t, g i • f i = 0
ht' : t ⊆ {i, j}
⊢ ∀ x ∈ {i, j}, x ∉ t → g x • f x = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case refine_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
h : ∀ (s t : R), s • -x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • x + t • y = 0
⊢ s = 0 ∧ t = 0

Tactic:
simpa using

Goal state after:
case refine_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
h : ∀ (s t : R), s • -x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • x + t • y = 0
⊢ s = 0 ∧ t = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
h : ∀ (s t : R), s • -x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • x + t • y = 0
⊢ -s • -x + t • y = 0

Tactic:
simpa using

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
h : ∀ (s t : R), s • -x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • x + t • y = 0
⊢ s • x + t • y = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case refine_2
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • -x + t • y = 0
⊢ s = 0 ∧ t = 0

Tactic:
simpa using

Goal state after:
case refine_2
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • -x + t • y = 0
⊢ s = 0 ∧ t = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • -x + t • y = 0
⊢ -s • x + t • y = 0

Tactic:
simpa using

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • -x + t • y = 0
⊢ -(s • x) + t • y = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case neg
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
i : ι
f : ι →₀ N
hf : ∀ (i_1 : ι), f i_1 ∈ ⨆ (_ : i_1 ≠ i), p i_1
hx : (f.sum fun _i xi ↦ xi) ∈ p i
hsup : (f.sum fun _i xi ↦ xi) ∈ ⨆ j, ⨆ (_ : j ≠ i), p j
h✝ : (f.sum fun _i xi ↦ xi) ≠ 0
j : ι
hj : j ∈ insert i f.support
h : ¬j = i
⊢ f j ∈ p j

Tactic:
simpa using

Goal state after:
case neg
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
i : ι
f : ι →₀ N
hf : ∀ (i_1 : ι), f i_1 ∈ ⨆ (_ : i_1 ≠ i), p i_1
hx : (f.sum fun _i xi ↦ xi) ∈ p i
hsup : (f.sum fun _i xi ↦ xi) ∈ ⨆ j, ⨆ (_ : j ≠ i), p j
h✝ : (f.sum fun _i xi ↦ xi) ≠ 0
j : ι
hj : j ∈ insert i f.support
h : ¬j = i
⊢ f j ∈ p j
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mp
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0
s : Finset ι
v w : ι → N
hvw : ∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i
⊢ ∑ i ∈ s, v i = ∑ i ∈ s, w i → ∀ i ∈ s, v i = w i

Tactic:
simpa using

Goal state after:
case mp
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0
s : Finset ι
v w : ι → N
hvw : ∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i
⊢ ∑ i ∈ s, v i = ∑ i ∈ s, w i → ∀ i ∈ s, v i = w i