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

Goal state before:
pp: case mp
R₁ : Type u_3
R₂ : Type u_4
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst✝¹¹ : AddCommMonoid Mₗ
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid Pₗ
inst✝⁸ : AddCommMonoid Qₗ
inst✝⁷ : AddCommMonoid Qₗ'
inst✝⁶ : Module R₁ Mₗ
inst✝⁵ : Module R₂ N
inst✝⁴ : Module R₂ Pₗ
inst✝³ : Module R₁ Pₗ
inst✝² : Module R₁ Qₗ
inst✝¹ : Module R₂ Qₗ'
inst✝ : SMulCommClass R₂ R₁ Pₗ
f₁ f₂ : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
g : Qₗ →ₗ[R₁] Mₗ
g' : Qₗ' →ₗ[R₂] N
hₗ : Surjective ⇑g
hᵣ : Surjective ⇑g'
h : f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
⊢ f₁ = f₂

pp: case mpr
R₁ : Type u_3
R₂ : Type u_4
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst✝¹¹ : AddCommMonoid Mₗ
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid Pₗ
inst✝⁸ : AddCommMonoid Qₗ
inst✝⁷ : AddCommMonoid Qₗ'
inst✝⁶ : Module R₁ Mₗ
inst✝⁵ : Module R₂ N
inst✝⁴ : Module R₂ Pₗ
inst✝³ : Module R₁ Pₗ
inst✝² : Module R₁ Qₗ
inst✝¹ : Module R₂ Qₗ'
inst✝ : SMulCommClass R₂ R₁ Pₗ
f₁ f₂ : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
g : Qₗ →ₗ[R₁] Mₗ
g' : Qₗ' →ₗ[R₂] N
hₗ : Surjective ⇑g
hᵣ : Surjective ⇑g'
h : f₁ = f₂
⊢ f₁.compl₁₂ g g' = f₂.compl₁₂ g g'

Tactic:
·

Goal state after:
case mp
R₁ : Type u_3
R₂ : Type u_4
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst✝¹¹ : AddCommMonoid Mₗ
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid Pₗ
inst✝⁸ : AddCommMonoid Qₗ
inst✝⁷ : AddCommMonoid Qₗ'
inst✝⁶ : Module R₁ Mₗ
inst✝⁵ : Module R₂ N
inst✝⁴ : Module R₂ Pₗ
inst✝³ : Module R₁ Pₗ
inst✝² : Module R₁ Qₗ
inst✝¹ : Module R₂ Qₗ'
inst✝ : SMulCommClass R₂ R₁ Pₗ
f₁ f₂ : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
g : Qₗ →ₗ[R₁] Mₗ
g' : Qₗ' →ₗ[R₂] N
hₗ : Surjective ⇑g
hᵣ : Surjective ⇑g'
h : f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
⊢ f₁ = f₂
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
h : ∀ (t : Finset ι) (g : ι → R), ↑t ⊆ {i, j} → (∀ i ∉ t, g i = 0) → ∑ i ∈ t, g i • f i = 0 → ∀ i ∈ t, g i = 0
c d : R
hcd : c • f i + d • f j = 0
⊢ c = 0 ∧ d = 0

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
⊢ ∀ i ∈ t, g i = 0

Tactic:
·

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
h : ∀ (t : Finset ι) (g : ι → R), ↑t ⊆ {i, j} → (∀ i ∉ t, g i = 0) → ∑ i ∈ t, g i • f i = 0 → ∀ i ∈ t, g i = 0
c d : R
hcd : c • f i + d • f j = 0
⊢ c = 0 ∧ d = 0
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: case mpr
R₁ : Type u_3
R₂ : Type u_4
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst✝¹¹ : AddCommMonoid Mₗ
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid Pₗ
inst✝⁸ : AddCommMonoid Qₗ
inst✝⁷ : AddCommMonoid Qₗ'
inst✝⁶ : Module R₁ Mₗ
inst✝⁵ : Module R₂ N
inst✝⁴ : Module R₂ Pₗ
inst✝³ : Module R₁ Pₗ
inst✝² : Module R₁ Qₗ
inst✝¹ : Module R₂ Qₗ'
inst✝ : SMulCommClass R₂ R₁ Pₗ
f₁ f₂ : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
g : Qₗ →ₗ[R₁] Mₗ
g' : Qₗ' →ₗ[R₂] N
hₗ : Surjective ⇑g
hᵣ : Surjective ⇑g'
h : f₁ = f₂
⊢ f₁.compl₁₂ g g' = f₂.compl₁₂ g g'

Tactic:
·

Goal state after:
case mpr
R₁ : Type u_3
R₂ : Type u_4
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
Mₗ : Type u_6
N : Type u_7
Pₗ : Type u_9
Qₗ : Type u_10
Qₗ' : Type u_11
inst✝¹¹ : AddCommMonoid Mₗ
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid Pₗ
inst✝⁸ : AddCommMonoid Qₗ
inst✝⁷ : AddCommMonoid Qₗ'
inst✝⁶ : Module R₁ Mₗ
inst✝⁵ : Module R₂ N
inst✝⁴ : Module R₂ Pₗ
inst✝³ : Module R₁ Pₗ
inst✝² : Module R₁ Qₗ
inst✝¹ : Module R₂ Qₗ'
inst✝ : SMulCommClass R₂ R₁ Pₗ
f₁ f₂ : Mₗ →ₗ[R₁] N →ₗ[R₂] Pₗ
g : Qₗ →ₗ[R₁] Mₗ
g' : Qₗ' →ₗ[R₂] N
hₗ : Surjective ⇑g
hᵣ : Surjective ⇑g'
h : f₁ = f₂
⊢ f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
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 : g i • f i + g j • f j = 0
ht' : t ⊆ {i, j}
⊢ ∀ i ∈ t, g i = 0

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}
⊢ ∀ x ∈ {i, j}, x ∉ t → g x • f x = 0

Tactic:
·

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 : g i • f i + g j • f j = 0
ht' : t ⊆ {i, j}
⊢ ∀ i ∈ t, g i = 0
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
⊢ (∀ (i : ι), ∀ x ∈ p i, x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j → x = 0) →
    ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0

pp: case mpr
ι : 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
⊢ (∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0) →
    ∀ (i : ι), ∀ x ∈ p i, x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j → x = 0

Tactic:
·

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
⊢ (∀ (i : ι), ∀ x ∈ p i, x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j → x = 0) →
    ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 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
u v : R
hu : IsUnit u
hv : IsUnit v
h : ∀ (s t : R), s • u • x + t • v • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • x + t • y = 0
⊢ s = 0 ∧ t = 0

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
u v : R
hu : IsUnit u
hv : IsUnit v
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • v • y = 0
⊢ s = 0 ∧ t = 0

Tactic:
·

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
u v : R
hu : IsUnit u
hv : IsUnit v
h : ∀ (s t : R), s • u • x + t • v • 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: case refine_2
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
u v : R
hu : IsUnit u
hv : IsUnit v
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • v • y = 0
⊢ s = 0 ∧ t = 0

Tactic:
·

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
u v : R
hu : IsUnit u
hv : IsUnit v
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • v • y = 0
⊢ s = 0 ∧ t = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mpr
ι : 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
⊢ (∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0) →
    ∀ (i : ι), ∀ x ∈ p i, x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j → x = 0

Tactic:
·

Goal state after:
case mpr
ι : 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
⊢ (∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0) →
    ∀ (i : ι), ∀ x ∈ p i, x ∈ ⨆ j, ⨆ (_ : j ≠ i), p j → 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
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • u • x + t • u • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • x + t • y = 0
⊢ s = 0 ∧ t = 0

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
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • u • y = 0
⊢ s = 0 ∧ t = 0

Tactic:
·

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
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • u • x + t • u • 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: case refine_2
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • u • y = 0
⊢ s = 0 ∧ t = 0

Tactic:
·

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
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • u • x + t • u • y = 0
⊢ s = 0 ∧ t = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case h.refine_1
ι : 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
⊢ (fun j ↦ if j = i then -f.sum fun x x_1 ↦ x_1 else f j) j ∈ p j

pp: case h.refine_2
ι : 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
⊢ ∑ i_1 ∈ insert i f.support, (fun j ↦ if j = i then -f.sum fun x x_1 ↦ x_1 else f j) i_1 = 0

Tactic:
·

Goal state after:
case h.refine_1
ι : 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
⊢ (fun j ↦ if j = i then -f.sum fun x x_1 ↦ x_1 else f j) j ∈ p j
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case pos
ι : 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.sum fun x x_1 ↦ x_1) ∈ p j

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:
·

Goal state after:
case pos
ι : 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.sum fun x x_1 ↦ x_1) ∈ p j
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:
·

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 h.refine_2
ι : 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
⊢ ∑ i_1 ∈ insert i f.support, (fun j ↦ if j = i then -f.sum fun x x_1 ↦ x_1 else f j) i_1 = 0

Tactic:
·

Goal state after:
case h.refine_2
ι : 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
⊢ ∑ i_1 ∈ insert i f.support, (fun j ↦ if j = i then -f.sum fun x x_1 ↦ x_1 else f j) i_1 = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case left
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ s = 0

pp: case right
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ t = 0

Tactic:
·

Goal state after:
case left
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ s = 0
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
⊢ (∀ (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), (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → ∑ i ∈ s, v i = ∑ i ∈ s, w i → ∀ i ∈ s, v i = w i

pp: case mpr
ι : 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
⊢ (∀ (s : Finset ι) (v w : ι → N),
      (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → ∑ i ∈ s, v i = ∑ i ∈ s, w i → ∀ i ∈ s, v i = w i) →
    ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0

Tactic:
·

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
⊢ (∀ (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), (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → ∑ i ∈ s, v i = ∑ i ∈ s, w i → ∀ i ∈ s, v i = w i
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case left
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ -(d • c • t) = (b * c) • s

Tactic:
·

Goal state after:
case left
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ -(d • c • t) = (b * c) • s
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mpr
ι : 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
⊢ (∀ (s : Finset ι) (v w : ι → N),
      (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → ∑ i ∈ s, v i = ∑ i ∈ s, w i → ∀ i ∈ s, v i = w i) →
    ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0

Tactic:
·

Goal state after:
case mpr
ι : 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
⊢ (∀ (s : Finset ι) (v w : ι → N),
      (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → ∑ i ∈ s, v i = ∑ i ∈ s, w i → ∀ i ∈ s, v i = w i) →
    ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case right
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ t = 0

Tactic:
·

Goal state after:
case right
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ t = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case right
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ -(a • b • s) = (b * c) • t

Tactic:
·

Goal state after:
case right
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ -(a • b • s) = (b * c) • t
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case inl
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
⊢ LinearIndependent R ![a • x + b • y, c • x + d • y] ↔ LinearIndependent R ![x, y] ∧ a * d ≠ b * c

pp: case inr
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d ≠ b * c
⊢ LinearIndependent R ![a • x + b • y, c • x + d • y] ↔ LinearIndependent R ![x, y] ∧ a * d ≠ b * c

Tactic:
·

Goal state after:
case inl
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
⊢ LinearIndependent R ![a • x + b • y, c • x + d • y] ↔ LinearIndependent R ![x, y] ∧ a * d ≠ b * c
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case pos
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
hbd : b = 0 ∧ d = 0
⊢ ∃ s t, s • (a • x + b • y) + t • (c • x + d • y) = 0 ∧ (s = 0 → t ≠ 0)

pp: case neg
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
hbd : ¬(b = 0 ∧ d = 0)
⊢ ∃ s t, s • (a • x + b • y) + t • (c • x + d • y) = 0 ∧ (s = 0 → t ≠ 0)

Tactic:
·

Goal state after:
case pos
R : Type u_2
M : Type u_4
inst✝¹⁰ : Ring R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
x y : M
S : Type u_6
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Module S R
inst✝⁴ : Module S M
inst✝³ : SMulCommClass S R M
inst✝² : IsScalarTower S R M
inst✝¹ : IsTorsionFree S R
a b c d : S
inst✝ : Nontrivial R
h : a * d = b * c
hbd : b = 0 ∧ d = 0
⊢ ∃ s t, s • (a • x + b • y) + t • (c • x + d • y) = 0 ∧ (s = 0 → t ≠ 0)