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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ ⊥ = ⊥

pp: case h'
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ (subToSupQuotient p p').ker ≤ comap p.subtype (p ⊓ p')

Tactic:
]

Goal state after:
case h'
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ (subToSupQuotient p p').ker ≤ comap p.subtype (p ⊓ p')
Module: Mathlib.LinearAlgebra.Isomorphisms

Goal state before:
pp: case h'
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ comap (inclusion ⋯) (comap (p ⊔ p').subtype p') ≤ comap p.subtype (p ⊓ p')

Tactic:
]

Goal state after:
case h'
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ comap (inclusion ⋯) (comap (p ⊔ p').subtype p') ≤ comap p.subtype (p ⊓ p')
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval - l₂.eval = l.eval
⊢ -(r₂ • x) + l₁.eval = -(r₂ • x) + l₁.eval

Tactic:
]

Goal state after:
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
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
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Isomorphisms

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ ∀ (x : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'), x ∈ (subToSupQuotient p p').range

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
⊢ ∀ (x : ↥(p ⊔ p') ⧸ comap (p ⊔ p').subtype p'), x ∈ (subToSupQuotient p p').range
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a₁ a₂ : R × M
l₁ l₂ l : NF R M
h : (a₁ ::ᵣ l₁).eval - l₂.eval = l.eval
⊢ -(a₂.1 • a₂.2) + (a₁.1 • a₁.2 + l₁.eval) = -(a₂.1 • a₂.2) + (a₁.1 • a₁.2 + l₁.eval)

Tactic:
]

Goal state after:
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
R₁ : Type u_4
R₂ : Type u_5
S₁ : Type u_6
S₂ : Type u_7
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Ring R
inst✝⁸ : Module R M
inst✝⁷ : Semiring R₁
inst✝⁶ : Module R₁ M
inst✝⁵ : Semiring R₂
inst✝⁴ : Module R₂ M
inst✝³ : Semiring S₁
inst✝² : Module S₁ M
inst✝¹ : Semiring S₂
inst✝ : Module S₂ M
l₁ l₂ l : NF R M
l₁' : NF R₁ M
l₂' : NF R₂ M
l₁'' : NF S₁ M
l₂'' : NF S₂ M
x₁ x₂ : M
hx₁ : x₁ = l₁''.eval
hx₂ : x₂ = l₂''.eval
h₁' : l₁'.eval = l₁''.eval
h₂' : l₂'.eval = l₂''.eval
h₁ : l₁.eval = l₁'.eval
h₂ : l₂.eval = l₂'.eval
h : l₁.eval - l₂.eval = l.eval
⊢ l.eval = l.eval

Tactic:
]

Goal state after:
Module: Mathlib.Tactic.Module

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Semiring S
inst✝² : Module S M
inst✝¹ : Ring R
inst✝ : Module R M
l : NF R M
l₀ : NF S M
hl : l.eval = l₀.eval
x : M
h : x = l₀.eval
⊢ -l.eval = -l.eval

Tactic:
]

Goal state after:
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
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 • a • s = d • a • s

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

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

Tactic:
]

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

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Isomorphisms

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : Submodule R M
x : ↥(p ⊔ p')
hx : ↑x ∈ p
⊢ Submodule.Quotient.mk x = Submodule.Quotient.mk ⟨↑⟨↑x, hx⟩, ⋯⟩

Tactic:
]

Goal state after:
Module: Mathlib.Tactic.Module

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
R₀ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Semiring R
inst✝⁴ : Module R M
inst✝³ : Semiring R₀
inst✝² : Module R₀ M
inst✝¹ : Semiring S
inst✝ : Module S M
l : NF R M
l₀ : NF R₀ M
s : S
r : R
x : M
hx : x = l₀.eval
hl : l.eval = l₀.eval
hs : r • x = s • x
⊢ r • l.eval = r • ?m.57

pp: case h
S : Type u_1
R : Type u_2
M : Type u_3
R₀ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Semiring R
inst✝⁴ : Module R M
inst✝³ : Semiring R₀
inst✝² : Module R₀ M
inst✝¹ : Semiring S
inst✝ : Module S M
l : NF R M
l₀ : NF R₀ M
s : S
r : R
x : M
hx : x = l₀.eval
hl : l.eval = l₀.eval
hs : r • x = s • x
⊢ ?m.57 = l.eval

pp: S : Type u_1
R : Type u_2
M : Type u_3
R₀ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Semiring R
inst✝⁴ : Module R M
inst✝³ : Semiring R₀
inst✝² : Module R₀ M
inst✝¹ : Semiring S
inst✝ : Module S M
l : NF R M
l₀ : NF R₀ M
s : S
r : R
x : M
hx : x = l₀.eval
hl : l.eval = l₀.eval
hs : r • x = s • x
⊢ M

Tactic:
]

Goal state after:
case h
S : Type u_1
R : Type u_2
M : Type u_3
R₀ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Semiring R
inst✝⁴ : Module R M
inst✝³ : Semiring R₀
inst✝² : Module R₀ M
inst✝¹ : Semiring S
inst✝ : Module S M
l : NF R M
l₀ : NF R₀ M
s : S
r : R
x : M
hx : x = l₀.eval
hl : l.eval = l₀.eval
hs : r • x = s • x
⊢ l.eval = l.eval
Module: Mathlib.LinearAlgebra.Isomorphisms

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h✝ h : S ≤ T
x : M
hx : x ∈ ↑T
⊢ Quotient.mk (LinearMap.id x) = 0

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h✝ h : S ≤ T
x : M
hx : x ∈ ↑T
⊢ Quotient.mk (LinearMap.id x) = 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
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
R₁ : Type u_4
R₂ : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Semiring R
inst✝⁴ : Module R M
inst✝³ : Semiring R₁
inst✝² : Module R₁ M
inst✝¹ : Semiring R₂
inst✝ : Module R₂ M
l₁ l₂ : NF R M
l₁' : NF R₁ M
l₂' : NF R₂ M
x₁ x₂ : M
hx₁ : x₁ = l₁'.eval
hx₂ : x₂ = l₂'.eval
h₁ : l₁.eval = l₁'.eval
h₂ : l₂.eval = l₂'.eval
h : l₁.eval = l₂.eval
⊢ l₂.eval = l₂.eval

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Isomorphisms

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h : S ≤ T
⊢ map S.mkQ T = map S.mkQ T

Tactic:
]

Goal state after:
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
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 • d • t = a • d • t

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.Isomorphisms

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S T : Submodule R M
hST : T ≤ S
⊢ Nat.card ↥(map T.mkQ S) * Nat.card (M ⧸ S) = Nat.card ↥(map T.mkQ S) * Nat.card (M ⧸ S)

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✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
ind : iSupIndep p
iSup_top : ⨆ i, p i = ⊤
⊢ iSup p = ⊤

Tactic:
]

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
ind : iSupIndep p
iSup_top : ⨆ i, p i = ⊤
⊢ iSup p = ⊤
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: R : Type u_3
N : Type u_6
inst✝⁴ : Ring R
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
⊢ ∀ (l : ι →₀ R), (Finsupp.linearCombination R v) l = 0 → l = 0

Tactic:
]

Goal state after:
R : Type u_3
N : Type u_6
inst✝⁴ : Ring R
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
⊢ ∀ (l : ι →₀ R), (Finsupp.linearCombination R v) l = 0 → l = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: R : Type u_3
N : Type u_6
inst✝⁴ : Ring R
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
l : ι →₀ R
hl :
  (((lsum ℕ) fun i ↦ (p i).subtype) ∘ₗ
        (mapRange.linearMap fun i ↦ LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) ∘ₗ ↑(finsuppLequivDFinsupp R))
      l =
    0
a : Π₀ (i : ι), ↥(p i) := (mapRange.linearMap fun i ↦ LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) l.toDFinsupp
⊢ ((lsum ℕ) fun i ↦ (p i).subtype) a = ((lsum ℕ) fun i ↦ (p i).subtype) 0

Tactic:
]

Goal state after:
R : Type u_3
N : Type u_6
inst✝⁴ : Ring R
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
l : ι →₀ R
hl :
  (((lsum ℕ) fun i ↦ (p i).subtype) ∘ₗ
        (mapRange.linearMap fun i ↦ LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) ∘ₗ ↑(finsuppLequivDFinsupp R))
      l =
    0
a : Π₀ (i : ι), ↥(p i) := (mapRange.linearMap fun i ↦ LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) l.toDFinsupp
⊢ ((lsum ℕ) fun i ↦ (p i).subtype) a = ((lsum ℕ) fun i ↦ (p i).subtype) 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
⊢ 0 = 0

Tactic:
]

Goal state after:
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
⊢ ¬∀ (s t : R), s • (a • x + b • y) + t • (c • x + d • y) = 0 → s = 0 ∧ t = 0

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
⊢ ¬∀ (s t : R), s • (a • x + b • y) + t • (c • x + d • 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
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
h' : LinearIndependent R ![a • x + b • y, c • x + d • y]
this : LinearIndependent R ![x, y]
⊢ LinearIndependent R ![x, y]

Tactic:
]

Goal state after:
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
h' : LinearIndependent R ![a • x + b • y, c • x + d • y]
this : LinearIndependent R ![x, y]
⊢ LinearIndependent R ![x, y]
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
x : X
⊢ toFinsupp (of x) = Finsupp.single x 1

Tactic:
by
  simp [toFinsupp]

Goal state after:
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
x✝ : X
⊢ of x✝ = of x✝

Tactic:
]

Goal state after:
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✝ x y : M
h : ∀ (s t : R), s • x + t • (x + y) = 0 → s = 0 ∧ t = 0
s t : R
h' : s • x + t • y = 0
⊢ s • x - t • x + (t • x + t • y) = s • x + t • y

Tactic:
]

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

Goal state before:
pp: X : Type u_2
x : FreeAbelianGroup X
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
f : X →₀ ℤ
⊢ f = f

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ (toFinsupp a) x ≠ 0 ↔ (coeff x) a ≠ 0

Tactic:
]

Goal state after:
X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ (toFinsupp a) x ≠ 0 ↔ (coeff x) a ≠ 0
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ (toFinsupp a) x = 0 ↔ (coeff x) a = 0

Tactic:
]

Goal state after:
X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ (toFinsupp a) x = 0 ↔ (coeff x) a = 0
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
x : X
⊢ {x} = {x}

Tactic:
]

Goal state after:
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✝ x y : M
h : ∀ (s t : R), s • x + t • (x + y) = 0 → s = 0 ∧ t = 0
s t : R
h' : s • x + t • y = 0
h₁ : s = 0
h₂ : t = 0
⊢ s = 0 ∧ t = 0

Tactic:
]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (span R (f i)) (⨆ i ∈ t, span R (f i))
⊢ LinearIndepOn R id (⋃ t, ⋃ i ∈ t, f i)

Tactic:
]

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (span R (f i)) (⨆ i ∈ t, span R (f i))
⊢ LinearIndepOn R id (⋃ t, ⋃ i ∈ t, f i)
Module: Mathlib.Algebra.Module.BigOperators

Goal state before:
pp: α : Type u_3
R : Type u_5
inst✝ : NonAssocSemiring R
s : Finset α
⊢ ↑(#s) = ↑(#s)

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : AddCommMonoid α
f : κ → α
s : Finset κ
i : ι
⊢ ∑ b ∈ image (fun g ↦ g i) (piFinset fun x ↦ s), #({a ∈ piFinset fun x ↦ s | a i = b}) • f b =
    #s ^ (card ι - 1) • ∑ b ∈ s, f b

Tactic:
]

Goal state after:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : AddCommMonoid α
f : κ → α
s : Finset κ
i : ι
⊢ ∑ b ∈ image (fun g ↦ g i) (piFinset fun x ↦ s), #({a ∈ piFinset fun x ↦ s | a i = b}) • f b =
    #s ^ (card ι - 1) • ∑ b ∈ s, f b
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case h.insert
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (span R (f i)) (⨆ i ∈ t, span R (f i))
i : ι
s : Finset ι
his : i ∉ s
ih : LinearIndepOn R id (⋃ i ∈ s, f i)
⊢ LinearIndepOn R id (f i ∪ ⋃ x ∈ s, f x)

Tactic:
]

Goal state after:
case h.insert
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (span R (f i)) (⨆ i ∈ t, span R (f i))
i : ι
s : Finset ι
his : i ∉ s
ih : LinearIndepOn R id (⋃ i ∈ s, f i)
⊢ LinearIndepOn R id (f i ∪ ⋃ x ∈ s, f x)
Module: Mathlib.Algebra.Module.BigOperators

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : AddCommMonoid α
R : Type u_7
inst✝¹ : Semiring R
inst✝ : Module R α
f : ι → α
r : R
i₀ : ι
⊢ r • f i₀ = r • f i₀

pp: case h₀
ι : Type u_1
α : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : AddCommMonoid α
R : Type u_7
inst✝¹ : Semiring R
inst✝ : Module R α
f : ι → α
r : R
i₀ : ι
⊢ ∀ b ∈ univ, b ≠ i₀ → Pi.single i₀ r b • f b = 0

pp: case h₁
ι : Type u_1
α : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : AddCommMonoid α
R : Type u_7
inst✝¹ : Semiring R
inst✝ : Module R α
f : ι → α
r : R
i₀ : ι
⊢ i₀ ∉ univ → Pi.single i₀ r i₀ • f i₀ = 0

Tactic:
]

Goal state after:
case h₀
ι : Type u_1
α : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : AddCommMonoid α
R : Type u_7
inst✝¹ : Semiring R
inst✝ : Module R α
f : ι → α
r : R
i₀ : ι
⊢ ∀ b ∈ univ, b ≠ i₀ → Pi.single i₀ r b • f b = 0

case h₁
ι : Type u_1
α : Type u_3
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : AddCommMonoid α
R : Type u_7
inst✝¹ : Semiring R
inst✝ : Module R α
f : ι → α
r : R
i₀ : ι
⊢ i₀ ∉ univ → Pi.single i₀ r i₀ • f i₀ = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case h.insert
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (span R (f i)) (⨆ i ∈ t, span R (f i))
i : ι
s : Finset ι
his : i ∉ s
ih : LinearIndepOn R id (⋃ i ∈ s, f i)
⊢ Disjoint (span R (f i)) (⨆ i ∈ s, span R (f i))

Tactic:
]

Goal state after:
case h.insert
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (span R (f i)) (⨆ i ∈ t, span R (f i))
i : ι
s : Finset ι
his : i ∉ s
ih : LinearIndepOn R id (⋃ i ∈ s, f i)
⊢ Disjoint (span R (f i)) (⨆ i ∈ s, span R (f i))
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case h.insert
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (span R (f i)) (⨆ i ∈ t, span R (f i))
i : ι
s : Finset ι
his : i ∉ s
ih : LinearIndepOn R id (⋃ i ∈ s, f i)
⊢ Disjoint (span R (f i)) (span R (⋃ x ∈ s, f x))

Tactic:
rw [span_iUnion₂]

Goal state after:
case h.insert
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (span R (f i)) (⨆ i ∈ t, span R (f i))
i : ι
s : Finset ι
his : i ∉ s
ih : LinearIndepOn R id (⋃ i ∈ s, f i)
⊢ Disjoint (span R (f i)) (⨆ i ∈ s, span R (f i))
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
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd : ∀ (i : η) (t : Set η), t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
x₁ : η
x₂ y₂ : ιs x₁
hxy : (fun ji ↦ f ji.fst ji.snd) ⟨x₁, x₂⟩ = (fun ji ↦ f ji.fst ji.snd) ⟨x₁, y₂⟩
⊢ Eq.recOn ⋯ ⟨x₁, y₂⟩.snd = ⟨x₁, y₂⟩.snd

Tactic:
]

Goal state after:
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
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd : ∀ (i : η) (t : Set η), t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji ↦ f ji.fst ji.snd) ⟨x₁, x₂⟩ = (fun ji ↦ f ji.fst ji.snd) ⟨y₁, y₂⟩
h_cases : ¬x₁ = y₁
⊢ f x₁ x₂ ∈ span R (range (f y₁))

Tactic:
]

Goal state after:
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
η : Type u_6
ιs : η → Type u_7
f : (j : η) → ιs j → M
hindep : ∀ (j : η), LinearIndependent R (f j)
hd : ∀ (i : η) (t : Set η), t.Finite → i ∉ t → Disjoint (span R (range (f i))) (⨆ i ∈ t, span R (range (f i)))
a✝ : Nontrivial R
x₁ : η
x₂ : ιs x₁
y₁ : η
y₂ : ιs y₁
hxy : (fun ji ↦ f ji.fst ji.snd) ⟨x₁, x₂⟩ = (fun ji ↦ f ji.fst ji.snd) ⟨y₁, y₂⟩
h_cases : ¬x₁ = y₁
⊢ f x₁ x₂ ∈ span R (range (f y₁))