awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.BaseChange (hypothesis)
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) ⋯
⊢ LinearIndependent L (M := ι' → L) fun (i : ι) ↦ (⇑(algebraMap K L) : (a : K) → L) ∘ v i
have hv' : 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.BaseChange (hypothesis)
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
⊢ i = j
have this₁ : Injective v
Tactic: have : Injective v := hv.injective
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.BaseChange (hypothesis)
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
⊢ LinearIndependent L (M := ι' → L) fun (i : ι) ↦ (⇑(algebraMap K L) : (a : K) → L) ∘ v i
have h_inj : Injective v'
Tactic: have h_inj : Injective v' := fun i j hij ↦ by have : Injective v := hv.injective; aesop
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.BaseChange (goal)
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) fun (i : ι) ↦ (⇑(algebraMap K L) : (a : K) → L) ∘ v i
have rw : LinearIndependent L (M := ι' → L) ((⇑b' : (a : (↑I : Type (max u_2 u_3))) → ι' → L) ∘ v')
Tactic: rw [← hv']
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.BaseChange (goal)
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
let let₁ let₂ let₃ let₄ let₅ let₆ :
  LinearIndependent L (M := ι' → L) fun (i : ι) ↦ (⇑(algebraMap K L) : (a : K) → L) ∘ v i
⊢ LinearIndependent L (M := ι' → L) fun (i : ι) ↦ (⇑(algebraMap K L) : (a : K) → L) ∘ v i
have let₇ : let this := Fintype.ofFinite ι';
let I := sorry.extend (K := K) (V := ι' → K) (v := id) (s := range v) (t := univ) sorry;
let b : Module.Basis (↑I : Type (max u_2 u_3)) K (ι' → K) := Module.Basis.extend (s := range v) sorry;
let 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 ι');
let v' : (i : ι) → (↑I : Type (max u_2 u_3)) := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι' → K) ↦ x ∈ I) (v i) sorry;
∀
  (hv' :
    Eq (α := ι → ι' → L) ((⇑b' : (a : (↑I : Type (max u_2 u_3))) → ι' → L) ∘ v') fun (i : ι) ↦
      (⇑(algebraMap K L) : (a : K) → L) ∘ v i),
  LinearIndependent L (M := ι' → L) fun (i : ι) ↦ (⇑(algebraMap K L) : (a : K) → L) ∘ v i
Tactic: classical
  let : Fintype ι' := .ofFinite ι'
  let I : Set (ι' → K) := hv.linearIndepOn_id.extend (subset_univ _)
  let b : Module.Basis I K (ι' → K) := .extend hv.linearIndepOn_id
  let b' : Module.Basis I L (ι' → L) := (b.baseChange L).map (TensorProduct.piScalarRight K L L ι')
  let v' (i : ι) : I := ⟨v i, hv.linearIndepOn_id.subset_extend _ <| mem_range_self i⟩
  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]
  have h_inj : Injective v' := fun i j hij ↦ by have : Injective v := hv.injective; aesop
  rw [← hv']
  exact b'.linearIndependent.comp _ h_inj
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.BaseChange (goal)
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
let let₁ let₂ let₃ let₄ let₅ let₆ :
  LinearIndependent L (M := ι' → L) fun (i : ι) ↦ (⇑(algebraMap K L) : (a : K) → L) ∘ v i
let₇ :
  let this := Fintype.ofFinite ι';
  let I := ⋯.extend (K := K) (V := ι' → K) (v := id) (s := range v) (t := univ) ⋯;
  let b : Module.Basis (↑I : Type (max u_2 u_3)) K (ι' → K) := Module.Basis.extend (s := range v) ⋯;
  let 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 ι');
  let 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),
    LinearIndependent L (M := ι' → L) fun (i : ι) ↦ (⇑(algebraMap K L) : (a : K) → L) ∘ v i
⊢ LinearIndependent L (M := ι' → L) fun (i : ι) ↦ (⇑(algebraMap K L) : (a : K) → L) ∘ v i
have let₈ : let this := Fintype.ofFinite ι';
let I := sorry.extend (K := K) (V := ι' → K) (v := id) (s := range v) (t := univ) sorry;
let b : Module.Basis (↑I : Type (max u_2 u_3)) K (ι' → K) := Module.Basis.extend (s := range v) sorry;
let 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 ι');
let v' : (i : ι) → (↑I : Type (max u_2 u_3)) := fun (i : ι) ↦ Subtype.mk (p := fun (x : ι' → K) ↦ x ∈ I) (v i) sorry;
∀
  (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) fun (i : ι) ↦ (⇑(algebraMap K L) : (a : K) → L) ∘ v i
Tactic: classical
  let : Fintype ι' := .ofFinite ι'
  let I : Set (ι' → K) := hv.linearIndepOn_id.extend (subset_univ _)
  let b : Module.Basis I K (ι' → K) := .extend hv.linearIndepOn_id
  let b' : Module.Basis I L (ι' → L) := (b.baseChange L).map (TensorProduct.piScalarRight K L L ι')
  let v' (i : ι) : I := ⟨v i, hv.linearIndepOn_id.subset_extend _ <| mem_range_self i⟩
  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]
  have h_inj : Injective v' := fun i j hij ↦ by have : Injective v := hv.injective; aesop
  rw [← hv']
  exact b'.linearIndependent.comp _ h_inj
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.BaseChange (goal)
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) fun (i : ι) ↦ (⇑(algebraMap R S) : (a : R) → S) ∘ v i) ↔ LinearIndependent R v
have change : LinearIndependent S (M := ι' → S) ((⇑(Pi.algebraMap ι' R S) : (a : ι' → R) → ι' → S) ∘ v) ↔ LinearIndependent R v
Tactic: change LinearIndependent S (Pi.algebraMap ι' R S ∘ v) ↔ LinearIndependent R v
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.BaseChange (goal)
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
have refine : ∀ (h : LinearIndependent R v), LinearIndependent S (M := ι' → S) ((⇑(Pi.algebraMap ι' R S) : (a : ι' → R) → ι' → S) ∘ v)
Tactic: refine ⟨fun h ↦ (h.restrict_scalars' R).of_comp, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.BaseChange (hypothesis)
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
⊢ LinearIndependent S (M := ι' → S) ((⇑(Pi.algebraMap ι' R S) : (a : ι' → R) → ι' → S) ∘ v)
have this : IsDomain R
Tactic: have : IsDomain R := .of_faithfulSMul R S
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.BaseChange (goal)
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)
have rw : LinearIndependent R (M := ι' → K) ((⇑(Pi.algebraMap ι' R K) : (a : ι' → R) → ι' → K) ∘ v)
Tactic: rw [← LinearIndependent.iff_fractionRing (R := R)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.BaseChange (goal)
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)
have 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
Tactic: rw [← LinearMap.ker_eq_bot, Submodule.eq_bot_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.BaseChange (goal)
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
⊢ v = 0
have h₁ : ∀ (i : ι'), v i = 0 i
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.BaseChange (hypothesis)
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 R (M := ι' → K) ((⇑(Pi.algebraMap ι' R K) : (a : ι' → R) → ι' → K) ∘ v)
have this₁ : 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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.BaseChange (hypothesis)
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 S (M := ι' → S) ((⇑(Pi.algebraMap ι' R S) : (a : ι' → R) → ι' → S) ∘ v)
have h₁ : 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]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.BaseChange (hypothesis)
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 := ι' → S) ((⇑(Pi.algebraMap ι' R S) : (a : ι' → R) → ι' → S) ∘ v)
have this₁ : LinearIndependent S (M := ι' → L) ((⇑(Pi.algebraMap ι' R L) : (a : ι' → R) → ι' → L) ∘ v)
Tactic: rw [← LinearIndependent.iff_fractionRing (R := S)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.BaseChange (goal)
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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.BaseChange (hypothesis)
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)
⊢ LinearIndependent S (M := ι' → S) ((⇑(Pi.algebraMap ι' R S) : (a : ι' → R) → ι' → S) ∘ v)
have 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))
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.BaseChange (hypothesis)
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 := ι' → S) ((⇑(Pi.algebraMap ι' R S) : (a : ι' → R) → ι' → S) ∘ v)
have this₁ : 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
Cleared hypotheses: this, aux
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.BaseChange (goal)
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
⊢ LinearIndependent S (M := ι' → S) ((⇑(Pi.algebraMap ι' R S) : (a : ι' → R) → ι' → S) ∘ v)
have suffices : LinearIndependent L (M := ι' → L) ((⇑(Pi.algebraMap ι' R L) : (a : ι' → R) → ι' → L) ∘ 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.BaseChange (goal)
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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.BaseChange (hypothesis)
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
⊢ LinearIndependent L (M := ι' → L) ((⇑(Pi.algebraMap ι' R L) : (a : ι' → R) → ι' → L) ∘ v)
have 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))
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.BaseChange (goal)
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) ((⇑(Pi.algebraMap ι' R L) : (a : ι' → R) → ι' → L) ∘ v)
have rw : LinearIndependent L (M := ι' → L)
  (comp (β := ι' → K) (⇑(Pi.algebraMap ι' K L) : (a : ι' → K) → ι' → L)
    ((⇑(Pi.algebraMap ι' R K) : (a : ι' → R) → ι' → K) ∘ v))
Tactic: rw [aux]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.BaseChange (hypothesis)
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)
    (comp (β := ι' → K) (⇑(Pi.algebraMap ι' K L) : (a : ι' → K) → ι' → L)
      ((⇑(Pi.algebraMap ι' R K) : (a : ι' → R) → ι' → K) ∘ v))
have 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)
Tactic: replace h := h.linearIndependent_algebraMap_comp_aux L
Cleared hypotheses: h