mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsReflexive R M
M' : Type u_6
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ eval R M' ∘ₗ f = eval R M' ∘ₗ f

Tactic:
]

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

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsReflexive R M
M' : Type u_6
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f g : M →ₗ[R] M'
h : Injective ⇑(Dual.eval R M')
hfg : f = g
⊢ f = g

Tactic:
]

Goal state after:
R : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : IsReflexive R M
M' : Type u_6
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f g : M →ₗ[R] M'
h : Injective ⇑(Dual.eval R M')
hfg : f = g
⊢ f = g
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
U V : Submodule R M
⊢ U ⊓ V ≤ U.dualAnnihilator.dualCoannihilator ⊓ V.dualAnnihilator.dualCoannihilator

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
U V : Submodule R M
⊢ U ⊓ V ≤ U.dualAnnihilator.dualCoannihilator ⊓ V.dualAnnihilator.dualCoannihilator
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_3
U : ι → Submodule R M
⊢ ⨅ i, U i ≤ ⨅ i, (U i).dualAnnihilator.dualCoannihilator

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_3
U : ι → Submodule R M
⊢ ⨅ i, U i ≤ ⨅ i, (U i).dualAnnihilator.dualCoannihilator
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
⊢ f.dualMap.ker = f.range.dualAnnihilator

Tactic:
ext
  simp_rw [mem_ker, LinearMap.ext_iff, Submodule.mem_dualAnnihilator,
    ← SetLike.mem_coe, coe_range, Set.forall_mem_range, dualMap_apply, zero_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h0
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
F : (i : ι) → M i →ₗ[R] N
c : R
f : Π₀ (i : ι), M i
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case ha
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
F : (i : ι) → M i →ₗ[R] N
c : R
f✝ : Π₀ (i : ι), M i
a : ι
b : M a
f : Π₀ (i : ι), M i
a✝¹ : f a = 0
a✝ : b ≠ 0
hf : (sumAddHom fun i ↦ (F i).toAddMonoidHom) (c • f) = c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) f
⊢ c • (F a) b + c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) f =
    c • (F a) b + c • (sumAddHom fun i ↦ (F i).toAddMonoidHom) f

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
F G : (i : ι) → M i →ₗ[R] N
⊢ { toFun := ⇑(sumAddHom fun i ↦ ((F + G) i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ } =
    { toFun := ⇑(sumAddHom fun i ↦ (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ } +
      { toFun := ⇑(sumAddHom fun i ↦ (G i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by
    refine DFinsupp.lhom_ext' (fun i ↦ ?_)
    ext
    simp

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
c : S
F : (i : ι) → M i →ₗ[R] N
⊢ { toFun := ⇑(sumAddHom fun i ↦ ((c • F) i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id S) c • { toFun := ⇑(sumAddHom fun i ↦ (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
by
    refine DFinsupp.lhom_ext' (fun i ↦ ?_)
    ext
    simp

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M i)
inst✝⁶ : (i : ι) → Module R (M i)
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : DecidableEq ι
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
F : (Π₀ (i : ι), M i) →ₗ[R] N
⊢ (fun F ↦ { toFun := ⇑(sumAddHom fun i ↦ (F i).toAddMonoidHom), map_add' := ⋯, map_smul' := ⋯ })
      ((fun F i ↦ F ∘ₗ lsingle i) F) =
    F

Tactic:
by
    refine DFinsupp.lhom_ext' (fun i ↦ ?_)
    ext
    simp

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
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ LinearIndependent R v ↔ Injective ⇑((LinearMap.lsum R (fun x ↦ R) ℕ) fun i ↦ LinearMap.id.smulRight (v i))

Tactic:
simp [Fintype.linearIndependent_iffₛ, Injective, funext_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : ι → Type u_5
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
m : Π₀ (i : ι), M i
x✝ : m ∈ ⊤
⊢ ((lsum ℕ) lsingle) m ∈ ⨆ i, (lsingle i).range

Tactic:
]

Goal state after:
ι : Type u_1
R : Type u_3
M : ι → Type u_5
inst✝³ : Semiring R
inst✝² : (i : ι) → AddCommMonoid (M i)
inst✝¹ : (i : ι) → Module R (M i)
inst✝ : DecidableEq ι
m : Π₀ (i : ι), M i
x✝ : m ∈ ⊤
⊢ ((lsum ℕ) lsingle) m ∈ ⨆ i, (lsingle i).range
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case pos
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₁ i)
inst✝ : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
x : Π₀ (i : ι), β₂ i
h : ⇑x ∈ AddSubmonoid.pi Set.univ fun i ↦ AddMonoidHom.mrange (f i)
g : (i : ι) → β₁ i
hg : ∀ (i : ι), (f i) (g i) = x i
i : ι
mem : i ∈ x.support
⊢ x i = x i

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case neg
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₁ i)
inst✝ : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
x : Π₀ (i : ι), β₂ i
h : ⇑x ∈ AddSubmonoid.pi Set.univ fun i ↦ AddMonoidHom.mrange (f i)
g : (i : ι) → β₁ i
hg : ∀ (i : ι), (f i) (g i) = x i
i : ι
mem : i ∉ x.support
⊢ 0 = 0

Tactic:
]

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

Tactic:
]

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
⊢ LinearIndepOn R v (⋃ i, ↑i)
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)
⊢ LinearIndepOn R v (⋃ x, t ↑x)

Tactic:
]

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)
⊢ LinearIndepOn R v (⋃ x, t ↑x)
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case a
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
i : ι
hi : p i
y : N
hy : y ∈ S i
⊢ ((lsum ℕ) fun i ↦ (S i).subtype) (single i ⟨y, hy⟩) = y

Tactic:
]

Goal state after:
case a
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
i : ι
hi : p i
y : N
hy : y ∈ S i
⊢ ((lsum ℕ) fun i ↦ (S i).subtype) (single i ⟨y, hy⟩) = y
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
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'
f : M →ₗ[R] M'
inj : Injective ⇑f
m : ι → Submodule R M
ind : ∀ (i : ι), m i ⊓ ⨆ j, ⨆ (_ : j ≠ i), m j ≤ ⊥
i : ι
x : M
hxi : x ∈ ↑(m i)
hx : f x ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), map f (m j))
⊢ f 0 ∈ ⊥

pp: ι : Type u'
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'
f : M →ₗ[R] M'
inj : Injective ⇑f
m : ι → Submodule R M
ind : ∀ (i : ι), m i ⊓ ⨆ j, ⨆ (_ : j ≠ i), m j ≤ ⊥
i : ι
x : M
hxi : x ∈ ↑(m i)
hx : f x ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), map f (m j))
⊢ x ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), m j)

Tactic:
]

Goal state after:
ι : Type u'
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'
f : M →ₗ[R] M'
inj : Injective ⇑f
m : ι → Submodule R M
ind : ∀ (i : ι), m i ⊓ ⨆ j, ⨆ (_ : j ≠ i), m j ≤ ⊥
i : ι
x : M
hxi : x ∈ ↑(m i)
hx : f x ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), map f (m j))
⊢ f 0 ∈ ⊥

ι : Type u'
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'
f : M →ₗ[R] M'
inj : Injective ⇑f
m : ι → Submodule R M
ind : ∀ (i : ι), m i ⊓ ⨆ j, ⨆ (_ : j ≠ i), m j ≤ ⊥
i : ι
x : M
hxi : x ∈ ↑(m i)
hx : f x ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), map f (m j))
⊢ x ∈ ↑(⨆ j, ⨆ (_ : j ≠ i), m j)
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Submodule R N
inst✝ : (i : ι) → (x : ↥(p i)) → Decidable (x ≠ 0)
x : N
⊢ (∃ f, ((lsum ℕ) fun i ↦ (p i).subtype) f = x) ↔ ∃ f, (f.sum fun x xi ↦ ↑xi) = x

Tactic:
]

Goal state after:
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Submodule R N
inst✝ : (i : ι) → (x : ↥(p i)) → Decidable (x ≠ 0)
x : N
⊢ (∃ f, ((lsum ℕ) fun i ↦ (p i).subtype) f = x) ↔ ∃ f, (f.sum fun x xi ↦ ↑xi) = x
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
x : N
⊢ (∃ f, (f.sum fun x xi ↦ ↑xi) = x) ↔ ∃ f, (∀ (i : ι), f i ∈ p i) ∧ (f.sum fun _i xi ↦ xi) = x

Tactic:
]

Goal state after:
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
x : N
⊢ (∃ f, (f.sum fun x xi ↦ ↑xi) = x) ↔ ∃ f, (∀ (i : ι), f i ∈ p i) ∧ (f.sum fun _i xi ↦ xi) = x
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
⊢ (∃ f, (f.sum fun x xi ↦ ↑xi) = a) ↔ ∃ μ, ∑ i ∈ s, ↑(μ i) = a

Tactic:
]

Goal state after:
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
⊢ (∃ f, (f.sum fun x xi ↦ ↑xi) = a) ↔ ∃ μ, ∑ i ∈ s, ↑(μ i) = 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:
]

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).prodMap (linearCombination R v') ∘ₗ ↑(sumFinsuppLEquivProdFinsupp R))
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
⊢ ∑ i ∈ s, ↑((fun i ↦ ⟨↑(μ i), ⋯⟩) i) = μ.sum fun x xi ↦ ↑xi

Tactic:
]

Goal state after:
case h
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
⊢ ∑ i ∈ s, ↑((fun i ↦ ⟨↑(μ i), ⋯⟩) i) = μ.sum fun x xi ↦ ↑xi
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h.h
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
x : ι
hx : x ∉ s
⊢ μ x = 0

Tactic:
]

Goal state after:
case h.h
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
x : ι
hx : x ∉ s
⊢ μ x = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h.h
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
x : ι
hx : x ∉ s
⊢ ↑(μ x) ∈ ⊥

Tactic:
]

Goal state after:
case h.h
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
x : ι
hx : x ∉ s
⊢ ↑(μ x) ∈ ⊥
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h.hf
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
x : ι
a✝ : x ∈ s
hx : μ x = 0
⊢ (fun x xi ↦ ↑xi) x (μ x) = 0

Tactic:
]

Goal state after:
case h.hf
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
x : ι
a✝ : x ∈ s
hx : μ x = 0
⊢ (fun x xi ↦ ↑xi) x (μ x) = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h.hf
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
x : ι
a✝ : x ∈ s
hx : μ x = 0
⊢ (fun x xi ↦ ↑xi) x 0 = 0

Tactic:
]

Goal state after:
case h.hf
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum fun x xi ↦ ↑xi) = a
x : ι
a✝ : x ∈ s
hx : μ x = 0
⊢ (fun x xi ↦ ↑xi) x 0 = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mpr.refine_1
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
i : ι
hi : i ∈ ↑s
⊢ ↑(μ i) ∈ p ↑⟨i, hi⟩

pp: case mpr.refine_1
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
i : ι
hi : i ∈ ↑s
⊢ ↑⟨i, hi⟩ ∈ s

Tactic:
]

Goal state after:
case mpr.refine_1
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
i : ι
hi : i ∈ ↑s
⊢ ↑(μ i) ∈ p ↑⟨i, hi⟩

case mpr.refine_1
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
i : ι
hi : i ∈ ↑s
⊢ ↑⟨i, hi⟩ ∈ s
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: 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'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
e : ↑s ⊕ ↑t ≃ ↑(⇑(inl R M M') '' s ∪ ⇑(inr R M M') '' t) :=
  Equiv.ofBijective (Sum.elim (fun i ↦ ⟨(inl R M M') ↑i, ⋯⟩) fun i ↦ ⟨(inr R M M') ↑i, ⋯⟩) ⋯
⊢ LinearIndependent R fun (x : ↑(⇑(inl R M M') '' s ∪ ⇑(inr R M M') '' t)) ↦ ↑x

Tactic:
refine (linearIndependent_equiv' e ?_).mp (linearIndependent_inl_union_inr' hs ht)

Goal state after:
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'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
e : ↑s ⊕ ↑t ≃ ↑(⇑(inl R M M') '' s ∪ ⇑(inr R M M') '' t) :=
  Equiv.ofBijective (Sum.elim (fun i ↦ ⟨(inl R M M') ↑i, ⋯⟩) fun i ↦ ⟨(inr R M M') ↑i, ⋯⟩) ⋯
⊢ (fun x ↦ ↑x) ∘ ⇑e = Sum.elim (⇑(inl R M M') ∘ fun x ↦ ↑x) (⇑(inr R M M') ∘ fun x ↦ ↑x)
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mpr.refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
⊢ ∑ x ∈ s, ↑((DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x) = ∑ i ∈ s, ↑(μ i)

pp: case mpr.refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
⊢ ∀ x ∈ s, x ∉ (DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩).support → ↑((DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x) = 0

Tactic:
]

Goal state after:
case mpr.refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
⊢ ∑ x ∈ s, ↑((DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x) = ∑ i ∈ s, ↑(μ i)

case mpr.refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
⊢ ∀ x ∈ s, x ∉ (DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩).support → ↑((DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x) = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
x : ι
hx : x ∈ s
⊢ ↑⟨↑(μ ↑⟨x, hx⟩), ⋯⟩ = ↑(μ x)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mpr.refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
x : ι
a✝ : x ∈ s
hx : (DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x = 0
⊢ ↑((DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x) = 0

Tactic:
]

Goal state after:
case mpr.refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
x : ι
a✝ : x ∈ s
hx : (DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x = 0
⊢ ↑((DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x) = 0
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
⊢ ∀ 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

Tactic:
]

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.BilinearMap

Goal state before:
pp: R : Type u_14
R₂ : Type u_15
R₃ : Type u_16
R₅ : Type u_18
M : Type u_19
N : Type u_20
P : Type u_21
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : Semiring R₃
inst✝⁸ : Semiring R₅
σ₂₃ : R₂ →+* R₃
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M
inst✝³ : Module R₂ N
inst✝² : Module R₃ P
inst✝¹ : Module R₅ P
inst✝ : SMulCommClass R₃ R₅ P
σ₁₅ : R →+* R₅
h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P
x✝¹ : M
x✝ : N
⊢ (h x✝¹) x✝ = (h x✝¹) x✝

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mpr.refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
x : ι
a✝ : x ∈ s
hx : (DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x = 0
⊢ ↑0 = 0

Tactic:
]

Goal state after:
case mpr.refine_2
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
x : ι
a✝ : x ∈ s
hx : (DFinsupp.mk s fun i ↦ ⟨↑(μ ↑i), ⋯⟩) x = 0
⊢ ↑0 = 0