awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_1
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Finite ι
e : M ≃ₗ[R] ι → R
j : M
x : ι
⊢ Eq.{u_3 + 1} (α := R) (((ofEquivFun e).equivFun : (a : M) → ι → R) j x : R) ((e : (a : M) → ι → R) j x : R)
have h : Eq.{u_3 + 1} (α := R) (((((ofEquivFun e).repr : (a : M) → ι →₀ R) j : ι →₀ R) : (a : ι) → R) x : R)
  ((e : (a : M) → ι → R) j x : R)
Tactic: simp_rw [Basis.equivFun_apply, Basis.ofEquivFun_repr_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
R₁ : Type u_13
inst_3 : Semiring R₁
σ : R →+* R₁
M₁ : Type u_14
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
f₁ f₂ : M →ₛₗ[σ] M₁
h :
  ∀ (i : ι),
    Eq.{u_14 + 1} (α := M₁) ((f₁ : (a : M) → M₁) ((b : (a : ι) → M) i : M) : M₁)
      ((f₂ : (a : M) → M₁) ((b : (a : ι) → M) i : M) : M₁)
⊢ f₁ = f₂
have h₁ : ∀ (x : M), Eq.{u_14 + 1} (α := M₁) ((f₁ : (a : M) → M₁) x : M₁) ((f₂ : (a : M) → M₁) x : M₁)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
R₁ : Type u_13
inst_3 : Semiring R₁
σ : R →+* R₁
M₁ : Type u_14
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
f₁ f₂ : M →ₛₗ[σ] M₁
h :
  ∀ (i : ι),
    Eq.{u_14 + 1} (α := M₁) ((f₁ : (a : M) → M₁) ((b : (a : ι) → M) i : M) : M₁)
      ((f₂ : (a : M) → M₁) ((b : (a : ι) → M) i : M) : M₁)
x : M
⊢ Eq.{u_14 + 1} (α := M₁) ((f₁ : (a : M) → M₁) x : M₁) ((f₂ : (a : M) → M₁) x : M₁)
have h₁ : Eq.{u_14 + 1} (α := M₁)
  ((f₁ : (a : M) → M₁)
      (∑ a ∈ Finsupp.support.{u_10, u_11} (M := R) ((b.repr : (a : M) → ι →₀ R) x),
        HSMul.hSMul.{u_11, u_12, u_12} (α := R) (β := M)
          ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R) ((b : (a : ι) → M) a : M)) :
    M₁)
  ((f₂ : (a : M) → M₁)
      (∑ a ∈ Finsupp.support.{u_10, u_11} (M := R) ((b.repr : (a : M) → ι →₀ R) x),
        HSMul.hSMul.{u_11, u_12, u_12} (α := R) (β := M)
          ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R) ((b : (a : ι) → M) a : M)) :
    M₁)
Tactic: rw [← b.linearCombination_repr x, Finsupp.linearCombination_apply, Finsupp.sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
R₁ : Type u_13
inst_3 : Semiring R₁
σ : R →+* R₁
σ' : R₁ →+* R
inst_4 : RingHomInvPair σ σ'
inst_5 : RingHomInvPair σ' σ
M₁ : Type u_14
inst_6 : AddCommMonoid M₁
inst_7 : Module R₁ M₁
f₁ f₂ : M ≃ₛₗ[σ] M₁
h :
  ∀ (i : ι),
    Eq.{u_14 + 1} (α := M₁) ((f₁ : (a : M) → M₁) ((b : (a : ι) → M) i : M) : M₁)
      ((f₂ : (a : M) → M₁) ((b : (a : ι) → M) i : M) : M₁)
⊢ f₁ = f₂
have h₁ : ∀ (x : M), Eq.{u_14 + 1} (α := M₁) ((f₁ : (a : M) → M₁) x : M₁) ((f₂ : (a : M) → M₁) x : M₁)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
R₁ : Type u_13
inst_3 : Semiring R₁
σ : R →+* R₁
σ' : R₁ →+* R
inst_4 : RingHomInvPair σ σ'
inst_5 : RingHomInvPair σ' σ
M₁ : Type u_14
inst_6 : AddCommMonoid M₁
inst_7 : Module R₁ M₁
f₁ f₂ : M ≃ₛₗ[σ] M₁
h :
  ∀ (i : ι),
    Eq.{u_14 + 1} (α := M₁) ((f₁ : (a : M) → M₁) ((b : (a : ι) → M) i : M) : M₁)
      ((f₂ : (a : M) → M₁) ((b : (a : ι) → M) i : M) : M₁)
x : M
⊢ Eq.{u_14 + 1} (α := M₁) ((f₁ : (a : M) → M₁) x : M₁) ((f₂ : (a : M) → M₁) x : M₁)
have h₁ : Eq.{u_14 + 1} (α := M₁)
  ((f₁ : (a : M) → M₁)
      (∑ a ∈ Finsupp.support.{u_10, u_11} (M := R) ((b.repr : (a : M) → ι →₀ R) x),
        HSMul.hSMul.{u_11, u_12, u_12} (α := R) (β := M)
          ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R) ((b : (a : ι) → M) a : M)) :
    M₁)
  ((f₂ : (a : M) → M₁)
      (∑ a ∈ Finsupp.support.{u_10, u_11} (M := R) ((b.repr : (a : M) → ι →₀ R) x),
        HSMul.hSMul.{u_11, u_12, u_12} (α := R) (β := M)
          ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R) ((b : (a : ι) → M) a : M)) :
    M₁)
Tactic: rw [← b.linearCombination_repr x, Finsupp.linearCombination_apply, Finsupp.sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f ((b : (a : ι) → M) i) = (⇑(single i 1) : (a : ι) → R)
x : M
i : ι
x_1 x_2 : M
⊢ f (x_1 + x_2) i = f x_1 i + f x_2 i
have rw : (f x_1 + f x_2) i = f x_1 i + f x_2 i
Tactic: rw [hadd, Pi.add_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f ((b : (a : ι) → M) i) = (⇑(single i 1) : (a : ι) → R)
x : M
i : ι
x_1 x_2 : M
rw : (f x_1 + f x_2) i = f x_1 i + f x_2 i
⊢ f (x_1 + x_2) i = f x_1 i + f x_2 i
have rw₁ : f x_1 i + f x_2 i = f x_1 i + f x_2 i
Tactic: rw [hadd, Pi.add_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f ((b : (a : ι) → M) i) = (⇑(single i 1) : (a : ι) → R)
x : M
i : ι
f_i : M →ₗ[R] R := { toFun := fun (x : M) ↦ f x i, map_add' := ⋯, map_smul' := ⋯ }
⊢ lapply i ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) = f_i
have refine : ∀ (j : ι),
  Eq.{u_11 + 1} (α := R) ((lapply i ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → R) ((b : (a : ι) → M) j : M) : R)
    ((f_i : (a : M) → R) ((b : (a : ι) → M) j : M) : R)
Tactic: refine b.ext fun j => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f ((b : (a : ι) → M) i) = (⇑(single i 1) : (a : ι) → R)
x : M
i : ι
f_i : M →ₗ[R] R := { toFun := fun (x : M) ↦ f x i, map_add' := ⋯, map_smul' := ⋯ }
j : ι
⊢ Eq.{u_11 + 1} (α := R) ((lapply i ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → R) ((b : (a : ι) → M) j : M) : R)
    ((f_i : (a : M) → R) ((b : (a : ι) → M) j : M) : R)
have change : (((b.repr : (a : M) → ι →₀ R) ((b : (a : ι) → M) j) : ι →₀ R) : (a : ι) → R) i = f ((b : (a : ι) → M) j) i
Tactic: change b.repr (b j) i = f (b j) i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f ((b : (a : ι) → M) i) = (⇑(single i 1) : (a : ι) → R)
x : M
i : ι
f_i : M →ₗ[R] R := { toFun := fun (x : M) ↦ f x i, map_add' := ⋯, map_smul' := ⋯ }
j : ι
⊢ (((b.repr : (a : M) → ι →₀ R) ((b : (a : ι) → M) j) : ι →₀ R) : (a : ι) → R) i = f ((b : (a : ι) → M) j) i
have rw : (single j 1 : (a : ι) → R) i = f ((b : (a : ι) → M) j) i
Tactic: rw [b.repr_self, f_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f ((b : (a : ι) → M) i) = (⇑(single i 1) : (a : ι) → R)
x : M
i : ι
f_i : M →ₗ[R] R := { toFun := fun (x : M) ↦ f x i, map_add' := ⋯, map_smul' := ⋯ }
j : ι
rw : (single j 1 : (a : ι) → R) i = f ((b : (a : ι) → M) j) i
⊢ (((b.repr : (a : M) → ι →₀ R) ((b : (a : ι) → M) j) : ι →₀ R) : (a : ι) → R) i = f ((b : (a : ι) → M) j) i
have rw₁ : Eq.{u_11 + 1} (α := R) ((single j 1 : (a : ι) → R) i : R) ((single j 1 : (a : ι) → R) i : R)
Tactic: rw [b.repr_self, f_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (hypothesis)
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f ((b : (a : ι) → M) i) = (⇑(single i 1) : (a : ι) → R)
x : M
i : ι
f_i : M →ₗ[R] R := { toFun := fun (x : M) ↦ f x i, map_add' := ⋯, map_smul' := ⋯ }
⊢ (((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i = f x i
have this : lapply i ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) = f_i
Tactic: have : Finsupp.lapply i ∘ₗ ↑b.repr = f_i := by
    refine b.ext fun j => ?_
    change b.repr (b j) i = f (b j) i
    rw [b.repr_self, f_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f ((b : (a : ι) → M) i) = (⇑(single i 1) : (a : ι) → R)
x : M
i : ι
f_i : M →ₗ[R] R := { toFun := fun (x : M) ↦ f x i, map_add' := ⋯, map_smul' := ⋯ }
this : lapply i ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) = f_i
⊢ Eq.{u_11 + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) ((f_i : (a : M) → R) x : R)
have rw : Eq.{u_11 + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R)
  ((lapply i ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → R) x : R)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f ((b : (a : ι) → M) i) = (⇑(single i 1) : (a : ι) → R)
x : M
i : ι
f_i : M →ₗ[R] R := { toFun := fun (x : M) ↦ f x i, map_add' := ⋯, map_smul' := ⋯ }
this : lapply i ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) = f_i
⊢ Eq.{u_11 + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) ((f_i : (a : M) → R) x : R)
have rw : Eq.{u_11 + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R)
  ((lapply i ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → R) x : R)
Tactic: { rw [← this]
        rfl }
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
f : M → ι → R
hadd : ∀ (x y : M), f (x + y) = f x + f y
hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x
f_eq : ∀ (i : ι), f ((b : (a : ι) → M) i) = (⇑(single i 1) : (a : ι) → R)
x : M
i : ι
f_i : M →ₗ[R] R := { toFun := fun (x : M) ↦ f x i, map_add' := ⋯, map_smul' := ⋯ }
this : lapply i ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) = f_i
⊢ (((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i = f x i
have x₁ : Eq.{u_11 + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R) ((f_i : (a : M) → R) x : R)
Tactic: calc
    b.repr x i = f_i x := by
      { rw [← this]
        rfl }
    _ = f x i := rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι_1 : Type u_1
ι' : Type u_2
R_1 : Type u_3
R₂ : Type u_4
K : Type u_5
M_1 : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid M'
inst_4 : Module R_1 M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
b : Basis ι R M
R' : Type u_13
inst_8 : Semiring R'
inst_9 : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), HSMul.hSMul.{u_13, u_12, u_12} (α := R') ((f : (a : R) → R') c : R') x = c • x
this : Module R' R := compHom R (↑f.symm : R' →+* R)
x : R'
y : R
z : M
⊢ (x • y) • z = x • y • z
have change : HMul.hMul (α := R) ((f.symm : (a : R') → R) x : R) y • z = x • y • z
Tactic: change (f.symm x * y) • z = x • (y • z)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι_1 : Type u_1
ι' : Type u_2
R_1 : Type u_3
R₂ : Type u_4
K : Type u_5
M_1 : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid M'
inst_4 : Module R_1 M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
b : Basis ι R M
R' : Type u_13
inst_8 : Semiring R'
inst_9 : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), HSMul.hSMul.{u_13, u_12, u_12} (α := R') ((f : (a : R) → R') c : R') x = c • x
this : Module R' R := compHom R (↑f.symm : R' →+* R)
x : R'
y : R
z : M
⊢ HMul.hMul (α := R) ((f.symm : (a : R') → R) x : R) y • z = x • y • z
have rw : HSMul.hSMul.{u_11, u_12, u_12} (α := R) ((f.symm : (a : R') → R) x : R) (y • z) = x • y • z
Tactic: rw [mul_smul, ← h, f.apply_symm_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι_1 : Type u_1
ι' : Type u_2
R_1 : Type u_3
R₂ : Type u_4
K : Type u_5
M_1 : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid M'
inst_4 : Module R_1 M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
b : Basis ι R M
R' : Type u_13
inst_8 : Semiring R'
inst_9 : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), HSMul.hSMul.{u_13, u_12, u_12} (α := R') ((f : (a : R) → R') c : R') x = c • x
this : Module R' R := compHom R (↑f.symm : R' →+* R)
x : R'
y : R
z : M
rw : HSMul.hSMul.{u_11, u_12, u_12} (α := R) ((f.symm : (a : R') → R) x : R) (y • z) = x • y • z
⊢ HMul.hMul (α := R) ((f.symm : (a : R') → R) x : R) y • z = x • y • z
have rw₁ : HSMul.hSMul.{u_13, u_12, u_12} (α := R') ((f : (a : R) → R') ((f.symm : (a : R') → R) x : R) : R') (y • z) = x • y • z
Tactic: rw [mul_smul, ← h, f.apply_symm_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι_1 : Type u_1
ι' : Type u_2
R_1 : Type u_3
R₂ : Type u_4
K : Type u_5
M_1 : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid M'
inst_4 : Module R_1 M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
b : Basis ι R M
R' : Type u_13
inst_8 : Semiring R'
inst_9 : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), HSMul.hSMul.{u_13, u_12, u_12} (α := R') ((f : (a : R) → R') c : R') x = c • x
this : Module R' R := compHom R (↑f.symm : R' →+* R)
x : R'
y : R
z : M
rw : HSMul.hSMul.{u_11, u_12, u_12} (α := R) ((f.symm : (a : R') → R) x : R) (y • z) = x • y • z
rw₁ :
  HSMul.hSMul.{u_13, u_12, u_12} (α := R') ((f : (a : R) → R') ((f.symm : (a : R') → R) x : R) : R') (y • z) = x • y • z
⊢ HMul.hMul (α := R) ((f.symm : (a : R') → R) x : R) y • z = x • y • z
have rw₂ : x • y • z = x • y • z
Tactic: rw [mul_smul, ← h, f.apply_symm_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (hypothesis)
Goal:
ι_1 : Type u_1
ι' : Type u_2
R_1 : Type u_3
R₂ : Type u_4
K : Type u_5
M_1 : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid M'
inst_4 : Module R_1 M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
b : Basis ι R M
R' : Type u_13
inst_8 : Semiring R'
inst_9 : Module R' M
f : R ≃+* R'
h : ∀ (c : R) (x : M), HSMul.hSMul.{u_13, u_12, u_12} (α := R') ((f : (a : R) → R') c : R') x = c • x
this : Module R' R := compHom R (↑f.symm : R' →+* R)
⊢ Basis ι R' M
have this₁ : IsScalarTower R' R M
Tactic: haveI : IsScalarTower R' R M :=
    { smul_assoc := fun x y z => by
        change (f.symm x * y) • z = x • (y • z)
        rw [mul_smul, ← h, f.apply_symm_apply] }
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
i : ι
h :
  Membership.mem.{u_12, u_12} (α := M) (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M))
    ((b : (a : ι) → M) i : M)
⊢ Eq.{u_12 + 1} (α := M)
    ((b.reindexRange : (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → M)
        (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x) ((b : (a : ι) → M) i)
            h :
          { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
      M)
    ((b : (a : ι) → M) i : M)
have inl : Subsingleton R →
  Eq.{u_12 + 1} (α := M)
    ((b.reindexRange : (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → M)
        (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x) ((b : (a : ι) → M) i)
            h :
          { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
      M)
    ((b : (a : ι) → M) i : M)
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
i : ι
h :
  Membership.mem.{u_12, u_12} (α := M) (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M))
    ((b : (a : ι) → M) i : M)
inl :
  Subsingleton R →
    Eq.{u_12 + 1} (α := M)
      ((b.reindexRange : (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → M)
          (Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x) ((b : (a : ι) → M) i)
              h :
            { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
        M)
      ((b : (a : ι) → M) i : M)
⊢ Eq.{u_12 + 1} (α := M)
    ((b.reindexRange : (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → M)
        (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x) ((b : (a : ι) → M) i)
            h :
          { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
      M)
    ((b : (a : ι) → M) i : M)
have inr : Nontrivial R →
  Eq.{u_12 + 1} (α := M)
    ((b.reindexRange : (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → M)
        (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x) ((b : (a : ι) → M) i)
            h :
          { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
      M)
    ((b : (a : ι) → M) i : M)
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
x : (↑(range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) : Type u_12)
⊢ (b.reindexRange : (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → M) x = (↑x : M)
have rcases : ∀ (i : ι),
  Eq.{u_12 + 1} (α := M)
    ((b.reindexRange : (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → M)
        (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x) ((b : (a : ι) → M) i)
            sorry :
          { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
      M)
    ((↑(Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x) ((b : (a : ι) → M) i)
            sorry) :
        M) :
      M)
Tactic: rcases x with ⟨bi, ⟨i, rfl⟩⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (hypothesis)
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
x bi : M
i : ι
h : (b : (a : ι) → M) i = bi
⊢ Eq.{u_11 + 1} (α := R)
    ((((b.reindexRange.repr : (a : M) → (↑(range (⇑b : (a : ι) → M)) : Type u_12) →₀ R) x :
            Finsupp.{u_12, u_11} (↑(range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) : Type u_12) R) :
          (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → R)
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x) bi ⋯) :
      R)
    ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R)
have a : Nontrivial R
Tactic: nontriviality
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
x bi : M
i : ι
h : (b : (a : ι) → M) i = bi
h_1 : Nontrivial R
⊢ Eq.{u_11 + 1} (α := R)
    ((((b.reindexRange.repr : (a : M) → (↑(range (⇑b : (a : ι) → M)) : Type u_12) →₀ R) x :
            Finsupp.{u_12, u_11} (↑(range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) : Type u_12) R) :
          (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → R)
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x) bi ⋯) :
      R)
    ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R)
have subst : Eq.{u_11 + 1} (α := R)
  ((((b.reindexRange.repr : (a : M) → (↑(range (⇑b : (a : ι) → M)) : Type u_12) →₀ R) x :
          Finsupp.{u_12, u_11} (↑(range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) : Type u_12) R) :
        (a : (↑(range (⇑b : (a : ι) → M)) : Type u_12)) → R)
      (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x) ((b : (a : ι) → M) i) sorry :
        { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
    R)
  ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R)
Tactic: subst h
Cleared hypotheses: bi, h