awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange
Goal:
ι : Type u_1
ι' : Type u_2
inst : Finite ι'
K : Type u_3
L : Type u_4
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
v : ι → ι' → K
hv : LinearIndependent K v
this : Fintype ι' := Fintype.ofFinite ι'
I : Set (ι' → K) := ⋯.extend (K := K) (V := ι' → K) (v := id) (s := range v) (t := univ) ⋯
b : Module.Basis (↑I : Type (max u_2 u_3)) K (ι' → K) := Module.Basis.extend (s := range v) ⋯
b' : Module.Basis (↑I : Type (max u_2 u_3)) L (ι' → L) :=
  Module.Basis.map (M := L ⊗[K] (ι' → K)) (Module.Basis.baseChange L b) (piScalarRight K L L ι')
v' : (i : ι) → (↑I : Type (max u_2 u_3)) := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι' → K) ↦ x ∈ I) (v i) ⋯
⊢ Eq (α := ι → ι' → L) ((⇑b' : (a : (↑I : Type (max u_2 u_3))) → ι' → L) ∘ v') fun (i : ι) ↦
    (⇑(algebraMap K L) : (a : K) → L) ∘ v i

Tactic:
have hv' : b' ∘ v' = fun i ↦ algebraMap K L ∘ v i := by
    ext; simp [b', b, v', Module.Basis.extend, Algebra.algebraMap_eq_smul_one]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange
Goal:
ι : Type u_1
ι' : Type u_2
inst : Finite ι'
K : Type u_3
L : Type u_4
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
v : ι → ι' → K
hv : LinearIndependent K v
this : Fintype ι' := Fintype.ofFinite ι'
I : Set (ι' → K) := ⋯.extend (K := K) (V := ι' → K) (v := id) (s := range v) (t := univ) ⋯
b : Module.Basis (↑I : Type (max u_2 u_3)) K (ι' → K) := Module.Basis.extend (s := range v) ⋯
b' : Module.Basis (↑I : Type (max u_2 u_3)) L (ι' → L) :=
  Module.Basis.map (M := L ⊗[K] (ι' → K)) (Module.Basis.baseChange L b) (piScalarRight K L L ι')
v' : (i : ι) → (↑I : Type (max u_2 u_3)) := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι' → K) ↦ x ∈ I) (v i) ⋯
hv' :
  Eq (α := ι → ι' → L) ((⇑b' : (a : (↑I : Type (max u_2 u_3))) → ι' → L) ∘ v') fun (i : ι) ↦
    (⇑(algebraMap K L) : (a : K) → L) ∘ v i
i j : ι
hij : v' i = v' j
⊢ Injective v

Tactic:
have : Injective v := hv.injective
-- Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange
Goal:
ι : Type u_1
ι' : Type u_2
inst : Finite ι'
K : Type u_3
L : Type u_4
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
v : ι → ι' → K
hv : LinearIndependent K v
this_1 : Fintype ι' := Fintype.ofFinite ι'
I : Set (ι' → K) := ⋯.extend (K := K) (V := ι' → K) (v := id) (s := range v) (t := univ) ⋯
b : Module.Basis (↑I : Type (max u_2 u_3)) K (ι' → K) := Module.Basis.extend (s := range v) ⋯
b' : Module.Basis (↑I : Type (max u_2 u_3)) L (ι' → L) :=
  Module.Basis.map (M := L ⊗[K] (ι' → K)) (Module.Basis.baseChange L b) (piScalarRight K L L ι')
v' : (i : ι) → (↑I : Type (max u_2 u_3)) := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι' → K) ↦ x ∈ I) (v i) ⋯
hv' :
  Eq (α := ι → ι' → L) ((⇑b' : (a : (↑I : Type (max u_2 u_3))) → ι' → L) ∘ v') fun (i : ι) ↦
    (⇑(algebraMap K L) : (a : K) → L) ∘ v i
i j : ι
hij : v' i = v' j
this : Injective v
⊢ i = j

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange
Goal:
ι : Type u_1
ι' : Type u_2
inst : Finite ι'
K : Type u_3
L : Type u_4
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
v : ι → ι' → K
hv : LinearIndependent K v
this : Fintype ι' := Fintype.ofFinite ι'
I : Set (ι' → K) := ⋯.extend (K := K) (V := ι' → K) (v := id) (s := range v) (t := univ) ⋯
b : Module.Basis (↑I : Type (max u_2 u_3)) K (ι' → K) := Module.Basis.extend (s := range v) ⋯
b' : Module.Basis (↑I : Type (max u_2 u_3)) L (ι' → L) :=
  Module.Basis.map (M := L ⊗[K] (ι' → K)) (Module.Basis.baseChange L b) (piScalarRight K L L ι')
v' : (i : ι) → (↑I : Type (max u_2 u_3)) := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι' → K) ↦ x ∈ I) (v i) ⋯
hv' :
  Eq (α := ι → ι' → L) ((⇑b' : (a : (↑I : Type (max u_2 u_3))) → ι' → L) ∘ v') fun (i : ι) ↦
    (⇑(algebraMap K L) : (a : K) → L) ∘ v i
⊢ Injective v'

Tactic:
have h_inj : Injective v' := fun i j hij ↦ by have : Injective v := hv.injective; aesop
-- Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange
Goal:
ι : Type u_1
ι' : Type u_2
inst : Finite ι'
K : Type u_3
L : Type u_4
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
v : ι → ι' → K
hv : LinearIndependent K v
this : Fintype ι' := Fintype.ofFinite ι'
I : Set (ι' → K) := ⋯.extend (K := K) (V := ι' → K) (v := id) (s := range v) (t := univ) ⋯
b : Module.Basis (↑I : Type (max u_2 u_3)) K (ι' → K) := Module.Basis.extend (s := range v) ⋯
b' : Module.Basis (↑I : Type (max u_2 u_3)) L (ι' → L) :=
  Module.Basis.map (M := L ⊗[K] (ι' → K)) (Module.Basis.baseChange L b) (piScalarRight K L L ι')
v' : (i : ι) → (↑I : Type (max u_2 u_3)) := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι' → K) ↦ x ∈ I) (v i) ⋯
hv' :
  Eq (α := ι → ι' → L) ((⇑b' : (a : (↑I : Type (max u_2 u_3))) → ι' → L) ∘ v') fun (i : ι) ↦
    (⇑(algebraMap K L) : (a : K) → L) ∘ v i
h_inj : Injective v'
rw : LinearIndependent L (M := ι' → L) ((⇑b' : (a : (↑I : Type (max u_2 u_3))) → ι' → L) ∘ v')
⊢ LinearIndependent L (M := ι' → L) fun (i : ι) ↦ (⇑(algebraMap K L) : (a : K) → L) ∘ v i

Tactic:
rw [← hv']
-- Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange
Goal:
ι : Type u_1
ι' : Type u_2
inst : Finite ι'
K : Type u_3
L : Type u_4
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
v : ι → ι' → K
hv : LinearIndependent K v
this : Fintype ι' := Fintype.ofFinite ι'
I : Set (ι' → K) := ⋯.extend (K := K) (V := ι' → K) (v := id) (s := range v) (t := univ) ⋯
b : Module.Basis (↑I : Type (max u_2 u_3)) K (ι' → K) := Module.Basis.extend (s := range v) ⋯
b' : Module.Basis (↑I : Type (max u_2 u_3)) L (ι' → L) :=
  Module.Basis.map (M := L ⊗[K] (ι' → K)) (Module.Basis.baseChange L b) (piScalarRight K L L ι')
v' : (i : ι) → (↑I : Type (max u_2 u_3)) := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι' → K) ↦ x ∈ I) (v i) ⋯
hv' :
  Eq (α := ι → ι' → L) ((⇑b' : (a : (↑I : Type (max u_2 u_3))) → ι' → L) ∘ v') fun (i : ι) ↦
    (⇑(algebraMap K L) : (a : K) → L) ∘ v i
h_inj : Injective v'
⊢ LinearIndependent L (M := ι' → L) ((⇑b' : (a : (↑I : Type (max u_2 u_3))) → ι' → L) ∘ v')

Tactic:
b'.linearIndependent.comp _ h_inj

Premises used: Module.Basis.linearIndependent, LinearIndependent.comp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.BaseChange
Goal:
ι : Type u_1
ι' : Type u_2
inst : Finite ι'
K : Type u_3
L : Type u_4
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
v : ι → ι' → K
hv : LinearIndependent K v
this : Fintype ι' := Fintype.ofFinite ι'
I : Set (ι' → K) := ⋯.extend (K := K) (V := ι' → K) (v := id) (s := range v) (t := univ) ⋯
b : Module.Basis (↑I : Type (max u_2 u_3)) K (ι' → K) := Module.Basis.extend (s := range v) ⋯
b' : Module.Basis (↑I : Type (max u_2 u_3)) L (ι' → L) :=
  Module.Basis.map (M := L ⊗[K] (ι' → K)) (Module.Basis.baseChange L b) (piScalarRight K L L ι')
v' : (i : ι) → (↑I : Type (max u_2 u_3)) := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι' → K) ↦ x ∈ I) (v i) ⋯
hv' :
  Eq (α := ι → ι' → L) ((⇑b' : (a : (↑I : Type (max u_2 u_3))) → ι' → L) ∘ v') fun (i : ι) ↦
    (⇑(algebraMap K L) : (a : K) → L) ∘ v i
h_inj : Injective v'
⊢ LinearIndependent L (M := ι' → L) ((⇑b' : (a : (↑I : Type (max u_2 u_3))) → ι' → L) ∘ v')

Tactic:
exact b'.linearIndependent.comp _ h_inj

Premises used: Module.Basis.linearIndependent, LinearIndependent.comp
-- 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
change :
  LinearIndependent S (M := ι' → S) ((⇑(Pi.algebraMap ι' R S) : (a : ι' → R) → ι' → S) ∘ v) ↔ LinearIndependent R v
⊢ (LinearIndependent S (M := ι' → S) fun (i : ι) ↦ (⇑(algebraMap R S) : (a : R) → S) ∘ v i) ↔ LinearIndependent R v

Tactic:
change LinearIndependent S (Pi.algebraMap ι' R S ∘ v) ↔ LinearIndependent R v

Premises used: Function.comp, Pi.algebraMap, LinearIndependent, DFunLike.coe
-- 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
⊢ LinearIndependent S (M := ι' → S) ((⇑(Pi.algebraMap ι' R S) : (a : ι' → R) → ι' → S) ∘ v) ↔ LinearIndependent R v

Tactic:
⟨fun h ↦ (h.restrict_scalars' R).of_comp, fun h ↦ ?_⟩

Premises used: Pi.algebraMap, LinearIndependent.restrict_scalars', LinearIndependent.of_comp, Iff.intro
-- 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
refine :
  ∀ (h : LinearIndependent R v),
    LinearIndependent S (M := ι' → S) ((⇑(Pi.algebraMap ι' R S) : (a : ι' → R) → ι' → S) ∘ v)
⊢ LinearIndependent S (M := ι' → S) ((⇑(Pi.algebraMap ι' R S) : (a : ι' → R) → ι' → S) ∘ v) ↔ LinearIndependent R v

Tactic:
refine ⟨fun h ↦ (h.restrict_scalars' R).of_comp, fun 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
h : LinearIndependent R v
⊢ IsDomain R

Tactic:
have : IsDomain R := .of_faithfulSMul R S
-- 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
h : LinearIndependent R v
this : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
rw : LinearIndependent R (M := ι' → K) ((⇑(Pi.algebraMap ι' R K) : (a : ι' → R) → ι' → K) ∘ v)
⊢ LinearIndependent K (M := ι' → K) ((⇑(Pi.algebraMap ι' R K) : (a : ι' → R) → ι' → K) ∘ v)

Tactic:
rw [← LinearIndependent.iff_fractionRing (R := R)]

Premises used: LinearIndependent.iff_fractionRing
-- 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
h : LinearIndependent R v
this : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
rw :
  ∀ (x : ι' → R),
    Membership.mem (γ := Submodule R (ι' → R))
        (LinearMap.ker (R₂ := R) (M₂ := ι' → K) (τ₁₂ := RingHom.id R) (Pi.algebraMap ι' R K) : Submodule R (ι' → R)) x →
      x = 0
⊢ Injective (α := ι' → R) (β := ι' → K) (⇑(Pi.algebraMap ι' R K) : (a : ι' → R) → ι' → K)

Tactic:
rw [← LinearMap.ker_eq_bot, Submodule.eq_bot_iff]

Premises used: LinearMap.ker_eq_bot, Submodule.eq_bot_iff
-- 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_1 : ι → ι' → R
h : LinearIndependent R v_1
this : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
v : ι' → R
hv :
  Membership.mem (γ := Submodule R (ι' → R))
    (LinearMap.ker (R₂ := R) (M₂ := ι' → K) (τ₁₂ := RingHom.id R) (Pi.algebraMap ι' R K) : Submodule R (ι' → R)) v
h₁ : ∀ (i : ι'), v i = 0 i
⊢ v = 0

Tactic:
ext i
-- 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_1 : ι → ι' → R
h : LinearIndependent R v_1
this : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
v : ι' → R
hv :
  Membership.mem (γ := Submodule R (ι' → R))
    (LinearMap.ker (R₂ := R) (M₂ := ι' → K) (τ₁₂ := RingHom.id R) (Pi.algebraMap ι' R K) : Submodule R (ι' → R)) v
i : ι'
⊢ v i = 0 i

Tactic:
simpa [Pi.algebraMap] using congr($hv i)

Premises used: Pi.algebraMap
-- 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
h : LinearIndependent R v
this : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
⊢ Injective (α := ι' → R) (β := ι' → K) (⇑(Pi.algebraMap ι' R K) : (a : ι' → R) → ι' → K)

Tactic:
have : Function.Injective (Pi.algebraMap ι' R K) := by
      rw [← LinearMap.ker_eq_bot, Submodule.eq_bot_iff]
      intro v hv; ext i; simpa [Pi.algebraMap] using congr($hv i)
-- 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
h : LinearIndependent R v
this_1 : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
this : Injective (α := ι' → R) (β := ι' → K) (⇑(Pi.algebraMap ι' R K) : (a : ι' → R) → ι' → K)
rwa rwa₁ rwa₂ rwa₃ : LinearIndependent R v
⊢ LinearIndependent R (M := ι' → K) ((⇑(Pi.algebraMap ι' R K) : (a : ι' → R) → ι' → K) ∘ v)

Tactic:
rwa [LinearMap.linearIndependent_iff_of_injOn _ this.injOn]

Premises used: Function.Injective.injOn, LinearMap.linearIndependent_iff_of_injOn
-- 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
h : LinearIndependent R v
this : IsDomain R
K : Type u_3 := FractionRing R
L : Type u_4 := FractionRing S
⊢ LinearIndependent K (M := ι' → K) ((⇑(Pi.algebraMap ι' R K) : (a : ι' → R) → ι' → K) ∘ v)

Tactic:
replace h : LinearIndependent K (Pi.algebraMap ι' R K ∘ v) := by
    rw [← LinearIndependent.iff_fractionRing (R := R)]
    have : Function.Injective (Pi.algebraMap ι' R K) := by
      rw [← LinearMap.ker_eq_bot, Submodule.eq_bot_iff]
      intro v hv; ext i; simpa [Pi.algebraMap] using congr($hv i)
    rwa [LinearMap.linearIndependent_iff_of_injOn _ this.injOn]
-- 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_2 : Algebra K L := FractionRing.liftAlgebra R L
this : LinearIndependent L (M := ι' → L) ((⇑(Pi.algebraMap ι' R L) : (a : ι' → R) → ι' → L) ∘ v)
⊢ LinearIndependent S (M := ι' → L) ((⇑(Pi.algebraMap ι' R L) : (a : ι' → R) → ι' → L) ∘ v)

Tactic:
rw [← LinearIndependent.iff_fractionRing (R := S)] at this

Premises used: LinearIndependent.iff_fractionRing
-- 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_2 : Algebra K L := FractionRing.liftAlgebra R L
this : LinearIndependent S (M := ι' → L) ((⇑(Pi.algebraMap ι' R L) : (a : ι' → R) → ι' → L) ∘ v)
h₁ :
  ∀ (x : ι) (x_1 : ι'),
    Eq.{u_4 + 1} (α := L) (((⇑(Pi.algebraMap ι' R L) : (a : ι' → R) → ι' → L) ∘ v) x x_1)
      (comp (β := ι' → S) (⇑(Pi.algebraMap ι' S L) : (a : ι' → S) → ι' → L)
        ((⇑(Pi.algebraMap ι' R S) : (a : ι' → R) → ι' → S) ∘ v) x x_1)
⊢ Eq (α := ι → ι' → L) ((⇑(Pi.algebraMap ι' R L) : (a : ι' → R) → ι' → L) ∘ v)
    (comp (β := ι' → S) (⇑(Pi.algebraMap ι' S L) : (a : ι' → S) → ι' → L)
      ((⇑(Pi.algebraMap ι' R S) : (a : ι' → R) → ι' → S) ∘ v))

Tactic:
ext
-- 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_2 : Algebra K L := FractionRing.liftAlgebra R L
this : LinearIndependent S (M := ι' → L) ((⇑(Pi.algebraMap ι' R L) : (a : ι' → R) → ι' → L) ∘ v)
x : ι
x_1 : ι'
⊢ Eq.{u_4 + 1} (α := L) (((⇑(Pi.algebraMap ι' R L) : (a : ι' → R) → ι' → L) ∘ v) x x_1)
    (comp (β := ι' → S) (⇑(Pi.algebraMap ι' S L) : (a : ι' → S) → ι' → L)
      ((⇑(Pi.algebraMap ι' R S) : (a : ι' → R) → ι' → S) ∘ 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_2 : Algebra K L := FractionRing.liftAlgebra R L
this : LinearIndependent S (M := ι' → L) ((⇑(Pi.algebraMap ι' R L) : (a : ι' → R) → ι' → L) ∘ v)
⊢ Eq (α := ι → ι' → L) ((⇑(Pi.algebraMap ι' R L) : (a : ι' → R) → ι' → L) ∘ v)
    (comp (β := ι' → S) (⇑(Pi.algebraMap ι' S L) : (a : ι' → S) → ι' → L)
      ((⇑(Pi.algebraMap ι' R S) : (a : ι' → R) → ι' → S) ∘ v))

Tactic:
have aux : Pi.algebraMap ι' R L ∘ v = Pi.algebraMap ι' S L ∘ Pi.algebraMap ι' R S ∘ 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_2 : Algebra K L := FractionRing.liftAlgebra R L
this : LinearIndependent S (M := ι' → L) ((⇑(Pi.algebraMap ι' R L) : (a : ι' → R) → ι' → L) ∘ v)
aux :
  Eq (α := ι → ι' → L) ((⇑(Pi.algebraMap ι' R L) : (a : ι' → R) → ι' → L) ∘ v)
    (comp (β := ι' → S) (⇑(Pi.algebraMap ι' S L) : (a : ι' → S) → ι' → L)
      ((⇑(Pi.algebraMap ι' R S) : (a : ι' → R) → ι' → S) ∘ v))
⊢ LinearIndependent S (M := ι' → L)
    (comp (β := ι' → S) (⇑(Pi.algebraMap ι' S L) : (a : ι' → S) → ι' → L)
      ((⇑(Pi.algebraMap ι' R S) : (a : ι' → R) → ι' → S) ∘ v))

Tactic:
rw [aux] at this
-- 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_2 : Algebra K L := FractionRing.liftAlgebra R L
this : LinearIndependent S (M := ι' → L) ((⇑(Pi.algebraMap ι' R L) : (a : ι' → R) → ι' → L) ∘ v)
aux :
  Eq (α := ι → ι' → L) ((⇑(Pi.algebraMap ι' R L) : (a : ι' → R) → ι' → L) ∘ v)
    (comp (β := ι' → S) (⇑(Pi.algebraMap ι' S L) : (a : ι' → S) → ι' → L)
      ((⇑(Pi.algebraMap ι' R S) : (a : ι' → R) → ι' → S) ∘ v))
this₁ :
  LinearIndependent S (M := ι' → L)
    (comp (β := ι' → S) (⇑(Pi.algebraMap ι' S L) : (a : ι' → S) → ι' → L)
      ((⇑(Pi.algebraMap ι' R S) : (a : ι' → R) → ι' → S) ∘ v))
⊢ Eq (α := ι → ι' → L) ((⇑(Pi.algebraMap ι' R L) : (a : ι' → R) → ι' → L) ∘ v)
    (comp (β := ι' → S) (⇑(Pi.algebraMap ι' S L) : (a : ι' → S) → ι' → L)
      ((⇑(Pi.algebraMap ι' R S) : (a : ι' → R) → ι' → S) ∘ v))

Tactic:
rw [aux] at this
-- 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_2 : Algebra K L := FractionRing.liftAlgebra R L
this :
  LinearIndependent S (M := ι' → L)
    (comp (β := ι' → S) (⇑(Pi.algebraMap ι' S L) : (a : ι' → S) → ι' → L)
      ((⇑(Pi.algebraMap ι' R S) : (a : ι' → R) → ι' → S) ∘ v))
aux :
  Eq (α := ι → ι' → L) ((⇑(Pi.algebraMap ι' R L) : (a : ι' → R) → ι' → L) ∘ v)
    (comp (β := ι' → S) (⇑(Pi.algebraMap ι' S L) : (a : ι' → S) → ι' → L)
      ((⇑(Pi.algebraMap ι' R S) : (a : ι' → R) → ι' → S) ∘ v))
⊢ LinearIndependent S (M := ι' → S) ((⇑(Pi.algebraMap ι' R S) : (a : ι' → R) → ι' → S) ∘ v)

Tactic:
this.of_comp

Premises used: LinearIndependent.of_comp
-- 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_2 : Algebra K L := FractionRing.liftAlgebra R L
this :
  LinearIndependent S (M := ι' → L)
    (comp (β := ι' → S) (⇑(Pi.algebraMap ι' S L) : (a : ι' → S) → ι' → L)
      ((⇑(Pi.algebraMap ι' R S) : (a : ι' → R) → ι' → S) ∘ v))
aux :
  Eq (α := ι → ι' → L) ((⇑(Pi.algebraMap ι' R L) : (a : ι' → R) → ι' → L) ∘ v)
    (comp (β := ι' → S) (⇑(Pi.algebraMap ι' S L) : (a : ι' → S) → ι' → L)
      ((⇑(Pi.algebraMap ι' R S) : (a : ι' → R) → ι' → S) ∘ v))
⊢ LinearIndependent S (M := ι' → S) ((⇑(Pi.algebraMap ι' R S) : (a : ι' → R) → ι' → S) ∘ v)

Tactic:
exact this.of_comp

Premises used: LinearIndependent.of_comp
-- 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
suffices : LinearIndependent L (M := ι' → L) ((⇑(Pi.algebraMap ι' R L) : (a : ι' → R) → ι' → L) ∘ v)
⊢ LinearIndependent S (M := ι' → S) ((⇑(Pi.algebraMap ι' R S) : (a : ι' → R) → ι' → S) ∘ v)

Tactic:
suffices LinearIndependent L (Pi.algebraMap ι' R L ∘ v) by
    rw [← LinearIndependent.iff_fractionRing (R := S)] at this
    have aux : Pi.algebraMap ι' R L ∘ v = Pi.algebraMap ι' S L ∘ Pi.algebraMap ι' R S ∘ v := by
      ext; simp [Pi.algebraMap, ← IsScalarTower.algebraMap_apply]
    rw [aux] at this
    exact this.of_comp
-- 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
h₁ :
  ∀ (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)
⊢ 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:
ext