awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring K
inst_4 : SMulWithZero R K
inst_5 : Module K M
inst_6 : IsScalarTower R K M
hinj : Injective.{u_2 + 1, u_3 + 1} (β := K) fun (r : R) ↦ HSMul.hSMul (β := K) r 1
li : LinearIndependent K v
x y : ι →₀ R
hxy :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) x : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) y : M)
f : (r : R) → K := fun (r : R) ↦ HSMul.hSMul (β := K) r 1
⊢ x = y
have refine_2 : ∀ (this : Finsupp.mapRange f sorry x = Finsupp.mapRange f sorry y), x = y
Tactic: have := @li (x.mapRange f (by simp [f])) (y.mapRange f (by simp [f])) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring K
inst_4 : SMulWithZero R K
inst_5 : Module K M
inst_6 : IsScalarTower R K M
hinj : Injective.{u_2 + 1, u_3 + 1} (β := K) fun (r : R) ↦ HSMul.hSMul (β := K) r 1
li : LinearIndependent K v
x y : ι →₀ R
hxy :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) x : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) y : M)
f : (r : R) → K := fun (r : R) ↦ HSMul.hSMul (β := K) r 1
refine_2 : ∀ (this : Finsupp.mapRange f ⋯ x = Finsupp.mapRange f ⋯ y), x = y
⊢ x = y
have refine_1 : Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination K v : (a : ι →₀ K) → M) (Finsupp.mapRange f sorry x) : M)
  ((Finsupp.linearCombination K v : (a : ι →₀ K) → M) (Finsupp.mapRange f sorry y) : M)
Tactic: have := @li (x.mapRange f (by simp [f])) (y.mapRange f (by simp [f])) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring K
inst_4 : SMulWithZero R K
inst_5 : Module K M
inst_6 : IsScalarTower R K M
hinj : Injective.{u_2 + 1, u_3 + 1} (β := K) fun (r : R) ↦ HSMul.hSMul (β := K) r 1
li : LinearIndependent K v
x y : ι →₀ R
hxy :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) x : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) y : M)
f : (r : R) → K := fun (r : R) ↦ HSMul.hSMul (β := K) r 1
this : Finsupp.mapRange f ⋯ x = Finsupp.mapRange f ⋯ y
⊢ x = y
have refine_2 : ∀ (i : ι), Eq.{u_2 + 1} (α := R) ((x : (a : ι) → R) i : R) ((y : (a : ι) → R) i : R)
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
hv : LinearIndependent.{u', u_2, u_5} R (M := M') ((⇑f : (a : M) → M') ∘ v)
⊢ Disjoint (span R (range v)) f.ker
have hv₁ : Injective (α := ι →₀ R) (β := M') (⇑(f ∘ₗ Finsupp.linearCombination R v) : (a : ι →₀ R) → M')
Tactic: rw [LinearIndependent, Finsupp.linearCombination_linear_comp] at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
hv : Injective (α := ι →₀ R) (β := M') (⇑(f ∘ₗ Finsupp.linearCombination R v) : (a : ι →₀ R) → M')
⊢ Disjoint (span R (range v)) f.ker
have rw : span R (range v) ⊓ f.ker ≤ ⊥
Tactic: rw [disjoint_iff_inf_le, ← Set.image_univ, Finsupp.span_image_eq_map_linearCombination,
    map_inf_eq_map_inf_comap, (LinearMap.ker_comp _ _).symm.trans
      (LinearMap.ker_eq_bot_of_injective hv), inf_bot_eq, map_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
hv : Injective (α := ι →₀ R) (β := M') (⇑(f ∘ₗ Finsupp.linearCombination R v) : (a : ι →₀ R) → M')
rw : span R (range v) ⊓ f.ker ≤ ⊥
⊢ Disjoint (span R (range v)) f.ker
have rw₁ : span R (v '' univ) ⊓ f.ker ≤ ⊥
Tactic: rw [disjoint_iff_inf_le, ← Set.image_univ, Finsupp.span_image_eq_map_linearCombination,
    map_inf_eq_map_inf_comap, (LinearMap.ker_comp _ _).symm.trans
      (LinearMap.ker_eq_bot_of_injective hv), inf_bot_eq, map_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
hv : Injective (α := ι →₀ R) (β := M') (⇑(f ∘ₗ Finsupp.linearCombination R v) : (a : ι →₀ R) → M')
rw : span R (range v) ⊓ f.ker ≤ ⊥
rw₁ : span R (v '' univ) ⊓ f.ker ≤ ⊥
⊢ Disjoint (span R (range v)) f.ker
have rw₂ : map (Finsupp.linearCombination R v) (Finsupp.supported R R univ) ⊓ f.ker ≤ ⊥
Tactic: rw [disjoint_iff_inf_le, ← Set.image_univ, Finsupp.span_image_eq_map_linearCombination,
    map_inf_eq_map_inf_comap, (LinearMap.ker_comp _ _).symm.trans
      (LinearMap.ker_eq_bot_of_injective hv), inf_bot_eq, map_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
hv : Injective (α := ι →₀ R) (β := M') (⇑(f ∘ₗ Finsupp.linearCombination R v) : (a : ι →₀ R) → M')
rw : span R (range v) ⊓ f.ker ≤ ⊥
rw₁ : span R (v '' univ) ⊓ f.ker ≤ ⊥
rw₂ : map (Finsupp.linearCombination R v) (Finsupp.supported R R univ) ⊓ f.ker ≤ ⊥
⊢ Disjoint (span R (range v)) f.ker
have rw₃ : LE.le (α := Submodule R M)
  (map (Finsupp.linearCombination R v) (Finsupp.supported R R univ ⊓ comap (Finsupp.linearCombination R v) f.ker)) ⊥
Tactic: rw [disjoint_iff_inf_le, ← Set.image_univ, Finsupp.span_image_eq_map_linearCombination,
    map_inf_eq_map_inf_comap, (LinearMap.ker_comp _ _).symm.trans
      (LinearMap.ker_eq_bot_of_injective hv), inf_bot_eq, map_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
hv : Injective (α := ι →₀ R) (β := M') (⇑(f ∘ₗ Finsupp.linearCombination R v) : (a : ι →₀ R) → M')
rw : span R (range v) ⊓ f.ker ≤ ⊥
rw₁ : span R (v '' univ) ⊓ f.ker ≤ ⊥
rw₂ : map (Finsupp.linearCombination R v) (Finsupp.supported R R univ) ⊓ f.ker ≤ ⊥
rw₃ :
  LE.le (α := Submodule R M)
    (map (Finsupp.linearCombination R v) (Finsupp.supported R R univ ⊓ comap (Finsupp.linearCombination R v) f.ker)) ⊥
⊢ Disjoint (span R (range v)) f.ker
have rw₄ : LE.le (α := Submodule R M) (map (Finsupp.linearCombination R v) (Finsupp.supported R R univ ⊓ ⊥)) ⊥
Tactic: rw [disjoint_iff_inf_le, ← Set.image_univ, Finsupp.span_image_eq_map_linearCombination,
    map_inf_eq_map_inf_comap, (LinearMap.ker_comp _ _).symm.trans
      (LinearMap.ker_eq_bot_of_injective hv), inf_bot_eq, map_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
hv : Injective (α := ι →₀ R) (β := M') (⇑(f ∘ₗ Finsupp.linearCombination R v) : (a : ι →₀ R) → M')
rw : span R (range v) ⊓ f.ker ≤ ⊥
rw₁ : span R (v '' univ) ⊓ f.ker ≤ ⊥
rw₂ : map (Finsupp.linearCombination R v) (Finsupp.supported R R univ) ⊓ f.ker ≤ ⊥
rw₃ :
  LE.le (α := Submodule R M)
    (map (Finsupp.linearCombination R v) (Finsupp.supported R R univ ⊓ comap (Finsupp.linearCombination R v) f.ker)) ⊥
rw₄ : LE.le (α := Submodule R M) (map (Finsupp.linearCombination R v) (Finsupp.supported R R univ ⊓ ⊥)) ⊥
⊢ Disjoint (span R (range v)) f.ker
have rw₅ : LE.le (α := Submodule R M) (map (Finsupp.linearCombination R v) ⊥) ⊥
Tactic: rw [disjoint_iff_inf_le, ← Set.image_univ, Finsupp.span_image_eq_map_linearCombination,
    map_inf_eq_map_inf_comap, (LinearMap.ker_comp _ _).symm.trans
      (LinearMap.ker_eq_bot_of_injective hv), inf_bot_eq, map_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
hv : Injective (α := ι →₀ R) (β := M') (⇑(f ∘ₗ Finsupp.linearCombination R v) : (a : ι →₀ R) → M')
rw : span R (range v) ⊓ f.ker ≤ ⊥
rw₁ : span R (v '' univ) ⊓ f.ker ≤ ⊥
rw₂ : map (Finsupp.linearCombination R v) (Finsupp.supported R R univ) ⊓ f.ker ≤ ⊥
rw₃ :
  LE.le (α := Submodule R M)
    (map (Finsupp.linearCombination R v) (Finsupp.supported R R univ ⊓ comap (Finsupp.linearCombination R v) f.ker)) ⊥
rw₄ : LE.le (α := Submodule R M) (map (Finsupp.linearCombination R v) (Finsupp.supported R R univ ⊓ ⊥)) ⊥
rw₅ : LE.le (α := Submodule R M) (map (Finsupp.linearCombination R v) ⊥) ⊥
⊢ Disjoint (span R (range v)) f.ker
have rw₆ : LE.le.{u_4} (α := Submodule R M) ⊥ ⊥
Tactic: rw [disjoint_iff_inf_le, ← Set.image_univ, Finsupp.span_image_eq_map_linearCombination,
    map_inf_eq_map_inf_comap, (LinearMap.ker_comp _ _).symm.trans
      (LinearMap.ker_eq_bot_of_injective hv), inf_bot_eq, map_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R' : Type u_6
M' : Type u_7
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
hv : LinearIndependent R v
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective.{u_4 + 1, u_7 + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R') (m : M), (j : (a : M) → M') (i r • m) = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')
⊢ LinearIndependent.{u', u_6, u_7} R' (M := M') ((⇑j : (a : M) → M') ∘ v)
have rw : ∀
  (hv :
    ∀ (s : Finset ι) (f g : ι → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i)
  (i : R' → R) (j : M →+ M') (hi : Injective i)
  (hj : Injective.{u_4 + 1, u_7 + 1} (α := M) (β := M') (⇑j : (a : M) → M'))
  (hc : ∀ (r : R') (m : M), (j : (a : M) → M') (i r • m) = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M'))
  (s : Finset ι) (f g : ι → R'),
  Eq.{u_7 + 1} (α := M') (∑ i ∈ s, HSMul.hSMul (β := M') (f i) (((⇑j : (a : M) → M') ∘ v) i))
      (∑ i ∈ s, HSMul.hSMul (β := M') (g i) (((⇑j : (a : M) → M') ∘ v) i)) →
    ∀ i ∈ s, f i = g i
Tactic: rw [linearIndependent_iff'ₛ] at hv ⊢
Cleared hypotheses: hv, i, j, hi, hj, hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R' : Type u_6
M' : Type u_7
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
hv :
  ∀ (s : Finset ι) (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
i : R' → R
j : M →+ M'
hi : Injective i
hj : Injective.{u_4 + 1, u_7 + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R') (m : M), (j : (a : M) → M') (i r • m) = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')
S : Finset ι
r₁ r₂ : ι → R'
H :
  Eq.{u_7 + 1} (α := M') (∑ i ∈ S, HSMul.hSMul (β := M') (r₁ i) (((⇑j : (a : M) → M') ∘ v) i))
    (∑ i ∈ S, HSMul.hSMul (β := M') (r₂ i) (((⇑j : (a : M) → M') ∘ v) i))
s : ι
hs : s ∈ S
⊢ r₁ s = r₂ s
have H₁ : Eq.{u_7 + 1} (α := M') ((j : (a : M) → M') (∑ x ∈ S, i (r₁ x) • v x) : M')
  ((j : (a : M) → M') (∑ x ∈ S, i (r₂ x) • v x) : M')
Tactic: simp_rw [comp_apply, ← hc, ← map_sum] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R' : Type u_6
M' : Type u_7
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
hv : LinearIndependent R v
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective.{u_4 + 1, u_7 + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R) (m : M), (j : (a : M) → M') (r • m) = HSMul.hSMul (β := M') (i r) ((j : (a : M) → M') m : M')
⊢ LinearIndependent.{u', u_6, u_7} R' (M := M') ((⇑j : (a : M) → M') ∘ v)
have obtain : ∀ (i' : R' → R) (hi' : RightInverse i' i), LinearIndependent.{u', u_6, u_7} R' (M := M') ((⇑j : (a : M) → M') ∘ v)
Tactic: obtain ⟨i', hi'⟩ := hi.hasRightInverse
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R' : Type u_6
M' : Type u_7
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
hv : LinearIndependent R v
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective.{u_4 + 1, u_7 + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R) (m : M), (j : (a : M) → M') (r • m) = HSMul.hSMul (β := M') (i r) ((j : (a : M) → M') m : M')
i' : R' → R
hi' : RightInverse i' i
⊢ LinearIndependent.{u', u_6, u_7} R' (M := M') ((⇑j : (a : M) → M') ∘ v)
have refine_1 : ∀ (x x_1 : R') (h : i' x = i' x_1), x = x_1
Tactic: refine hv.map_of_injective_injectiveₛ i' j (fun _ _ h ↦ ?_) hj fun r m ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R' : Type u_6
M' : Type u_7
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
hv : LinearIndependent R v
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective.{u_4 + 1, u_7 + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R) (m : M), (j : (a : M) → M') (r • m) = HSMul.hSMul (β := M') (i r) ((j : (a : M) → M') m : M')
i' : R' → R
hi' : RightInverse i' i
refine_1 : ∀ (x x_1 : R') (h : i' x = i' x_1), x = x_1
⊢ LinearIndependent.{u', u_6, u_7} R' (M := M') ((⇑j : (a : M) → M') ∘ v)
have refine_2 : ∀ (r : R') (m : M), (j : (a : M) → M') (i' r • m) = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')
Tactic: refine hv.map_of_injective_injectiveₛ i' j (fun _ _ h ↦ ?_) hj fun r m ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R' : Type u_6
M' : Type u_7
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
hv : LinearIndependent R v
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective.{u_4 + 1, u_7 + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R) (m : M), (j : (a : M) → M') (r • m) = HSMul.hSMul (β := M') (i r) ((j : (a : M) → M') m : M')
i' : R' → R
hi' : RightInverse i' i
x x_1 : R'
h : i' x = i' x_1
⊢ x = x_1
have h₁ : i (i' x) = i (i' x_1)
Tactic: apply_fun i at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R' : Type u_6
M' : Type u_7
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
hv : LinearIndependent R v
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective.{u_4 + 1, u_7 + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R) (m : M), (j : (a : M) → M') (r • m) = HSMul.hSMul (β := M') (i r) ((j : (a : M) → M') m : M')
i' : R' → R
hi' : RightInverse i' i
x x_1 : R'
h : i (i' x) = i (i' x_1)
⊢ x = x_1
have refine_1 : ∀ (h : x = i (i' x_1)), x = x_1
Tactic: rwa [hi', hi'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R' : Type u_6
M' : Type u_7
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
hv : LinearIndependent R v
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective.{u_4 + 1, u_7 + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R) (m : M), (j : (a : M) → M') (r • m) = HSMul.hSMul (β := M') (i r) ((j : (a : M) → M') m : M')
i' : R' → R
hi' : RightInverse i' i
x x_1 : R'
h : i (i' x) = i (i' x_1)
refine_1 : ∀ (h : x = i (i' x_1)), x = x_1
⊢ x = x_1
have refine_1₁ : ∀ (h : x = x_1), x = x_1
Tactic: rwa [hi', hi'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R' : Type u_6
M' : Type u_7
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
hv : LinearIndependent R v
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective.{u_4 + 1, u_7 + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R) (m : M), (j : (a : M) → M') (r • m) = HSMul.hSMul (β := M') (i r) ((j : (a : M) → M') m : M')
i' : R' → R
hi' : RightInverse i' i
r : R'
m : M
⊢ (j : (a : M) → M') (i' r • m) = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')
have refine_2 : HSMul.hSMul (β := M') (i (i' r)) ((j : (a : M) → M') m : M') = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')
Tactic: rw [hc (i' r) m, hi']
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
R' : Type u_6
M' : Type u_7
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
hv : LinearIndependent R v
i : R → R'
j : M →+ M'
hi : Surjective i
hj : Injective.{u_4 + 1, u_7 + 1} (α := M) (β := M') (⇑j : (a : M) → M')
hc : ∀ (r : R) (m : M), (j : (a : M) → M') (r • m) = HSMul.hSMul (β := M') (i r) ((j : (a : M) → M') m : M')
i' : R' → R
hi' : RightInverse i' i
r : R'
m : M
refine_2 :
  HSMul.hSMul (β := M') (i (i' r)) ((j : (a : M) → M') m : M') = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')
⊢ (j : (a : M) → M') (i' r • m) = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')
have refine_2₁ : HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M') = HSMul.hSMul (β := M') r ((j : (a : M) → M') m : M')
Tactic: rw [hc (i' r) m, hi']
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
s : Set ι
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : ι → ι'
g : ι' → M
hs : LinearIndepOn R (g ∘ f) s
⊢ LinearIndepOn R g (f '' s)
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
s : Set ι
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : ι → ι'
g : ι' → M
hs : LinearIndepOn R (g ∘ f) s
h : Nontrivial R
⊢ LinearIndepOn R g (f '' s)
have this : InjOn f s
Tactic: have : InjOn f s := injOn_iff_injective.2 hs.injective.of_comp
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
w : ι → M
h : EqOn v w s
⊢ (LinearIndependent.{u', u_2, u_4} R (M := M) fun (x : (↑s : Type u')) ↦ v (↑x : ι)) ↔
    LinearIndependent.{u', u_2, u_4} R (M := M) fun (x : (↑s : Type u')) ↦ w (↑x : ι)
have h₁ : Eq (α := (↑s : Type u') → M) (fun (x : (↑s : Type u')) ↦ w (↑x : ι)) fun (x : (↑s : Type u')) ↦ v (↑x : ι)
Tactic: convert! Iff.rfl using 2
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
w : ι → M
h : EqOn v w s
⊢ Eq (α := (↑s : Type u') → M) (fun (x : (↑s : Type u')) ↦ w (↑x : ι)) fun (x : (↑s : Type u')) ↦ v (↑x : ι)
have h₁ : ∀ (x : (↑s : Type u')), w (↑x : ι) = v (↑x : ι)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_6
hG : Group G
inst_3 : MulAction G R
inst_4 : SMul G M
inst_5 : IsScalarTower G R M
inst_6 : SMulCommClass G R M
v : ι → M
hv : LinearIndependent R v
w : ι → G
⊢ LinearIndependent R (w • v)
have rw : ∀
  (hv :
    ∀ (s : Finset ι) (f g : ι → R),
      (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i)
  (w : ι → G) (s : Finset ι) (f g : ι → R),
  (∀ i ∉ s, f i = g i) →
    Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • (w • v) i) (∑ i ∈ s, g i • (w • v) i) → ∀ (i : ι), f i = g i
Tactic: rw [linearIndependent_iff''ₛ] at hv ⊢
Cleared hypotheses: hv, w
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_6
hG : Group G
inst_3 : MulAction G R
inst_4 : SMul G M
inst_5 : IsScalarTower G R M
inst_6 : SMulCommClass G R M
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i
w : ι → G
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g₁ i • (w • v) i) (∑ i ∈ s, g₂ i • (w • v) i)
i : ι
⊢ g₁ i = g₂ i
have refine : w i • g₁ i = w i • g₂ i
Tactic: refine (Group.isUnit (w i)).smul_left_cancel.mp ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_6
hG : Group G
inst_3 : MulAction G R
inst_4 : SMul G M
inst_5 : IsScalarTower G R M
inst_6 : SMulCommClass G R M
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i
w : ι → G
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g₁ i • (w • v) i) (∑ i ∈ s, g₂ i • (w • v) i)
i : ι
⊢ w i • g₁ i = w i • g₂ i
have refine_1 : ∀ (i : ι) (hi : i ∉ s), Eq.{u_2 + 1} (α := R) ((fun (i : ι) ↦ w i • g₁ i) i) ((fun (i : ι) ↦ w i • g₂ i) i)
Tactic: refine hv s (fun i ↦ w i • g₁ i) (fun i ↦ w i • g₂ i) (fun i hi ↦ ?_) ?_ i
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_6
hG : Group G
inst_3 : MulAction G R
inst_4 : SMul G M
inst_5 : IsScalarTower G R M
inst_6 : SMulCommClass G R M
v : ι → M
hv :
  ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i
w : ι → G
s : Finset ι
g₁ g₂ : ι → R
hgs : ∀ i ∉ s, g₁ i = g₂ i
hsum : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g₁ i • (w • v) i) (∑ i ∈ s, g₂ i • (w • v) i)
i : ι
refine_1 : ∀ (i : ι) (hi : i ∉ s), Eq.{u_2 + 1} (α := R) ((fun (i : ι) ↦ w i • g₁ i) i) ((fun (i : ι) ↦ w i • g₂ i) i)
⊢ w i • g₁ i = w i • g₂ i
have refine_2 : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ w i • g₁ i) i) (v i))
  (∑ i ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ w i • g₂ i) i) (v i))
Tactic: refine hv s (fun i ↦ w i • g₁ i) (fun i ↦ w i • g₂ i) (fun i hi ↦ ?_) ?_ i
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_6
hG : Group G
inst_3 : MulAction G R
inst_4 : MulAction G M
inst_5 : IsScalarTower G R M
inst_6 : SMulCommClass G R M
v : ι → M
w : ι → G
⊢ LinearIndependent R (w • v) ↔ LinearIndependent R v
have refine : ∀ (h : LinearIndependent R (w • v)), LinearIndependent R v
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h.group_smul w⟩