awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange
Goal:
ι : Type u_1
ι' : Type u_2
inst : Finite ι'
R : Type u_3
S : Type u_4
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : FaithfulSMul R S
inst_5 : IsDomain S
v : ι → ι' → R
this_1 : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
h : LinearIndependent K (M := ι' → K) ((⇑(Pi.algebraMap ι' R K) : (a : ι' → R) → ι' → K) ∘ v)
this : Algebra K L := FractionRing.liftAlgebra R L
x : ι
x_1 : ι'
⊢ Eq.{u_4 + 1} (α := L) (((⇑(Pi.algebraMap ι' R L) : (a : ι' → R) → ι' → L) ∘ v) x x_1)
    (comp (β := ι' → K) (⇑(Pi.algebraMap ι' K L) : (a : ι' → K) → ι' → L)
      ((⇑(Pi.algebraMap ι' R K) : (a : ι' → R) → ι' → K) ∘ v) x x_1)

Tactic:
simp [Pi.algebraMap, ← IsScalarTower.algebraMap_apply]

Premises used: Pi.algebraMap, IsScalarTower.algebraMap_apply
-- Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange
Goal:
ι : Type u_1
ι' : Type u_2
inst : Finite ι'
R : Type u_3
S : Type u_4
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : FaithfulSMul R S
inst_5 : IsDomain S
v : ι → ι' → R
this_1 : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
h : LinearIndependent K (M := ι' → K) ((⇑(Pi.algebraMap ι' R K) : (a : ι' → R) → ι' → K) ∘ v)
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ Eq (α := ι → ι' → L) ((⇑(Pi.algebraMap ι' R L) : (a : ι' → R) → ι' → L) ∘ v)
    (comp (β := ι' → K) (⇑(Pi.algebraMap ι' K L) : (a : ι' → K) → ι' → L)
      ((⇑(Pi.algebraMap ι' R K) : (a : ι' → R) → ι' → K) ∘ v))

Tactic:
have aux : Pi.algebraMap ι' R L ∘ v = Pi.algebraMap ι' K L ∘ Pi.algebraMap ι' R K ∘ v := by
    ext; simp [Pi.algebraMap, ← IsScalarTower.algebraMap_apply]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange
Goal:
ι : Type u_1
ι' : Type u_2
inst : Finite ι'
R : Type u_3
S : Type u_4
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : FaithfulSMul R S
inst_5 : IsDomain S
v : ι → ι' → R
this_1 : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
h : LinearIndependent K (M := ι' → K) ((⇑(Pi.algebraMap ι' R K) : (a : ι' → R) → ι' → K) ∘ v)
this : Algebra K L := FractionRing.liftAlgebra R L
aux :
  Eq (α := ι → ι' → L) ((⇑(Pi.algebraMap ι' R L) : (a : ι' → R) → ι' → L) ∘ v)
    (comp (β := ι' → K) (⇑(Pi.algebraMap ι' K L) : (a : ι' → K) → ι' → L)
      ((⇑(Pi.algebraMap ι' R K) : (a : ι' → R) → ι' → K) ∘ v))
rw :
  LinearIndependent L (M := ι' → L)
    (comp (β := ι' → K) (⇑(Pi.algebraMap ι' K L) : (a : ι' → K) → ι' → L)
      ((⇑(Pi.algebraMap ι' R K) : (a : ι' → R) → ι' → K) ∘ v))
⊢ LinearIndependent L (M := ι' → L) ((⇑(Pi.algebraMap ι' R L) : (a : ι' → R) → ι' → L) ∘ v)

Tactic:
rw [aux]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange
Goal:
ι : Type u_1
ι' : Type u_2
inst : Finite ι'
R : Type u_3
S : Type u_4
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : FaithfulSMul R S
inst_5 : IsDomain S
v : ι → ι' → R
this_1 : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
h : LinearIndependent K (M := ι' → K) ((⇑(Pi.algebraMap ι' R K) : (a : ι' → R) → ι' → K) ∘ v)
this : Algebra K L := FractionRing.liftAlgebra R L
aux :
  Eq (α := ι → ι' → L) ((⇑(Pi.algebraMap ι' R L) : (a : ι' → R) → ι' → L) ∘ v)
    (comp (β := ι' → K) (⇑(Pi.algebraMap ι' K L) : (a : ι' → K) → ι' → L)
      ((⇑(Pi.algebraMap ι' R K) : (a : ι' → R) → ι' → K) ∘ v))
⊢ LinearIndependent L (M := ι' → L) fun (i : ι) ↦
    comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := K) (⇑(algebraMap K L) : (a : K) → L)
      (((⇑(Pi.algebraMap ι' R K) : (a : ι' → R) → ι' → K) ∘ v) i)

Tactic:
replace h := h.linearIndependent_algebraMap_comp_aux L
-- Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange
Goal:
ι : Type u_1
ι' : Type u_2
inst : Finite ι'
R : Type u_3
S : Type u_4
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : FaithfulSMul R S
inst_5 : IsDomain S
v : ι → ι' → R
this_1 : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
aux :
  Eq (α := ι → ι' → L) ((⇑(Pi.algebraMap ι' R L) : (a : ι' → R) → ι' → L) ∘ v)
    (comp (β := ι' → K) (⇑(Pi.algebraMap ι' K L) : (a : ι' → K) → ι' → L)
      ((⇑(Pi.algebraMap ι' R K) : (a : ι' → R) → ι' → K) ∘ v))
h :
  LinearIndependent L (M := ι' → L) fun (i : ι) ↦
    comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := K) (⇑(algebraMap K L) : (a : K) → L)
      (((⇑(Pi.algebraMap ι' R K) : (a : ι' → R) → ι' → K) ∘ v) i)
⊢ LinearIndependent L (M := ι' → L)
    (comp (β := ι' → K) (⇑(Pi.algebraMap ι' K L) : (a : ι' → K) → ι' → L)
      ((⇑(Pi.algebraMap ι' R K) : (a : ι' → R) → ι' → K) ∘ v))

Tactic:
h
-- Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange
Goal:
ι : Type u_1
ι' : Type u_2
inst : Finite ι'
R : Type u_3
S : Type u_4
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : FaithfulSMul R S
inst_5 : IsDomain S
v : ι → ι' → R
this_1 : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
aux :
  Eq (α := ι → ι' → L) ((⇑(Pi.algebraMap ι' R L) : (a : ι' → R) → ι' → L) ∘ v)
    (comp (β := ι' → K) (⇑(Pi.algebraMap ι' K L) : (a : ι' → K) → ι' → L)
      ((⇑(Pi.algebraMap ι' R K) : (a : ι' → R) → ι' → K) ∘ v))
h :
  LinearIndependent L (M := ι' → L) fun (i : ι) ↦
    comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := K) (⇑(algebraMap K L) : (a : K) → L)
      (((⇑(Pi.algebraMap ι' R K) : (a : ι' → R) → ι' → K) ∘ v) i)
⊢ LinearIndependent L (M := ι' → L)
    (comp (β := ι' → K) (⇑(Pi.algebraMap ι' K L) : (a : ι' → K) → ι' → L)
      ((⇑(Pi.algebraMap ι' R K) : (a : ι' → R) → ι' → K) ∘ v))

Tactic:
exact h
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
⊢ f 0 = 0

Tactic:
simp [f]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
refine_1 :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination K v : (a : ι →₀ K) → M) (Finsupp.mapRange f ⋯ x) : M)
    ((Finsupp.linearCombination K v : (a : ι →₀ K) → M) (Finsupp.mapRange f ⋯ y) : M)
⊢ x = y

Tactic:
have := @li (x.mapRange f (by simp [f])) (y.mapRange f (by simp [f])) ?_
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
refine_2 : ∀ (i : ι), Eq.{u_2 + 1} (α := R) ((x : (a : ι) → R) i : R) ((y : (a : ι) → R) i : R)
⊢ x = y

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
i : ι
⊢ Eq.{u_2 + 1} (α := R) ((x : (a : ι) → R) i : R) ((y : (a : ι) → R) i : R)

Tactic:
hinj congr($this i)

Premises used: congrArg, id, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
i : ι
⊢ Eq.{u_2 + 1} (α := R) ((x : (a : ι) → R) i : R) ((y : (a : ι) → R) i : R)

Tactic:
exact hinj congr($this i)

Premises used: congrArg, id, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
⊢ Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination K v : (a : ι →₀ K) → M) (Finsupp.mapRange f ⋯ x) : M)
    ((Finsupp.linearCombination K v : (a : ι →₀ K) → M) (Finsupp.mapRange f ⋯ y) : M)

Tactic:
simpa [Finsupp.linearCombination, f, Finsupp.sum_mapRange_index]

Premises used: Finsupp.sum_mapRange_index, Finsupp.linearCombination
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
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
inst_7 : FaithfulSMul R K
inst_8 : IsScalarTower R K K
v : ι → M
li : LinearIndependent K v
⊢ LinearIndependent R v

Tactic:
restrict_scalars ((faithfulSMul_iff_injective_smul_one R K).mp inferInstance) li

Premises used: inferInstance, Iff.mp, faithfulSMul_iff_injective_smul_one, LinearIndependent.restrict_scalars
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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)
⊢ Injective (α := ι →₀ R) (β := M') (⇑(f ∘ₗ Finsupp.linearCombination R v) : (a : ι →₀ R) → M')

Tactic:
rw [LinearIndependent, Finsupp.linearCombination_linear_comp] at hv

Premises used: Finsupp.linearCombination_linear_comp, LinearIndependent
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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) ⊥) ⊥
rw₆ rw₇ : LE.le.{u_4} (α := Submodule R M) ⊥ ⊥
⊢ Disjoint (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]

Premises used: Set.image_univ, Finsupp.span_image_eq_map_linearCombination, Submodule.map_bot, Submodule.map_inf_eq_map_inf_comap, LinearMap.ker_comp, inf_bot_eq, LinearMap.ker_eq_bot_of_injective, disjoint_iff_inf_le, Eq.symm, Eq.trans
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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')
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
⊢ LinearIndependent.{u', u_6, u_7} R' (M := M') ((⇑j : (a : M) → M') ∘ v)

Tactic:
rw [linearIndependent_iff'ₛ] at hv ⊢

Premises used: linearIndependent_iff'ₛ
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
⊢ 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

Premises used: map_sum, Function.comp_apply
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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'
s : ι
hs : s ∈ S
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')
⊢ r₁ s = r₂ s

Tactic:
hi <| hv _ _ _ (hj H) s hs
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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'
s : ι
hs : s ∈ S
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')
⊢ r₁ s = r₂ s

Tactic:
exact hi <| hv _ _ _ (hj H) s hs
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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')
obtain :
  ∀ (i' : R' → R) (hi' : RightInverse i' i), LinearIndependent.{u', u_6, u_7} R' (M := M') ((⇑j : (a : M) → M') ∘ v)
⊢ LinearIndependent.{u', u_6, u_7} R' (M := M') ((⇑j : (a : M) → M') ∘ v)

Tactic:
obtain ⟨i', hi'⟩ := hi.hasRightInverse

Premises used: Function.Surjective.hasRightInverse
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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)

Tactic:
hv.map_of_injective_injectiveₛ i' j (fun _ _ h ↦ ?_) hj fun r m ↦ ?_

Premises used: LinearIndependent.map_of_injective_injectiveₛ
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
refine_2 : ∀ (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)

Tactic:
refine hv.map_of_injective_injectiveₛ i' j (fun _ _ h ↦ ?_) hj fun r m ↦ ?_

Premises used: LinearIndependent.map_of_injective_injectiveₛ
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
⊢ i (i' x) = i (i' x_1)

Tactic:
apply_fun i at h
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : ∀ (h : x = x_1), x = x_1
⊢ x = x_1

Tactic:
rwa [hi', hi'] at h
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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')
refine_2₁ refine_2₂ :
  HSMul.hSMul (β := M') 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')

Tactic:
rw [hc (i' r) m, hi']
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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'
hv : LinearIndependent R v
f : M →ₗ[R] M'
hf_inj : InjOn.{u_4, u_5} (β := M') (⇑f : (a : M) → M') (↑(span R (range v)) : Set M)
⊢ LinearIndependent.{u', u_2, u_5} R (M := M') ((⇑f : (a : M) → M') ∘ v)

Tactic:
(f.linearIndependent_iff_of_injOn hf_inj).mpr hv

Premises used: Iff.mpr, LinearMap.linearIndependent_iff_of_injOn
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
R : Type u_2
s : Set ι
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'
hv : LinearIndepOn R v s
f : M →ₗ[R] M'
hf_inj : InjOn.{u_4, u_5} (β := M') (⇑f : (a : M) → M') (↑(span R (v '' s)) : Set M)
⊢ LinearIndepOn.{u', u_2, u_5} R (M := M') ((⇑f : (a : M) → M') ∘ v) s

Tactic:
(f.linearIndepOn_iff_of_injOn hf_inj).mpr hv

Premises used: Iff.mpr, LinearMap.linearIndepOn_iff_of_injOn
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set ι'
f : ι' → ι
h : LinearIndepOn R v (f '' s)
hf : InjOn f s
⊢ LinearIndepOn R (v ∘ f) s

Tactic:
LinearIndependent.comp h _ (Equiv.Set.imageOfInjOn _ _ hf).injective

Premises used: Equiv.Set.imageOfInjOn, Equiv.injective, LinearIndependent.comp, LinearIndepOn
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
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
⊢ InjOn f s

Tactic:
have : InjOn f s := injOn_iff_injective.2 hs.injective.of_comp