awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.InformationTheory.Coding.KraftMcMillan (hypothesis)
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
h_kraft : LT.lt (α := ℝ) 1 (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length)
K : ℝ := ∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length
maxLen : ℕ := S.sup List.length
hAbs : |1 / K| < 1
⊢ ∃ r ≥ 1,
    HMul.hMul (α := ℝ) (↑r : ℝ) (↑(S.sup List.length) : ℝ) <
      HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) r
have this : Tendsto (β := ℝ) (fun (r : ℕ) ↦ HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ) / K ^ r) atTop (nhds 0)
Tactic: have : Tendsto (fun r : ℕ => r * maxLen / K ^ r) atTop (nhds 0) := by
    simpa [mul_left_comm, mul_div_assoc] using
      (tendsto_self_mul_const_pow_of_abs_lt_one hAbs).const_mul (maxLen : ℝ)
-- Lean 4 proof step from Mathlib.InformationTheory.Coding.KraftMcMillan (goal)
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
h_kraft : LT.lt (α := ℝ) 1 (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length)
K : ℝ := ∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length
maxLen : ℕ := S.sup List.length
hAbs : |1 / K| < 1
this : Tendsto (β := ℝ) (fun (r : ℕ) ↦ HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ) / K ^ r) atTop (nhds 0)
⊢ ∃ r ≥ 1,
    HMul.hMul (α := ℝ) (↑r : ℝ) (↑(S.sup List.length) : ℝ) <
      HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) r
have obtain : ∀ (r : ℕ) (hr : ∀ b ≥ r, HMul.hMul (α := ℝ) (↑b : ℝ) (↑maxLen : ℝ) / K ^ b < 1),
  ∃ r ≥ 1,
    HMul.hMul (α := ℝ) (↑r : ℝ) (↑(S.sup List.length) : ℝ) <
      HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) r
Tactic: obtain ⟨r, hr⟩ := eventually_atTop.mp <| this.eventually <| gt_mem_nhds zero_lt_one
-- Lean 4 proof step from Mathlib.InformationTheory.Coding.KraftMcMillan (goal)
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
h_kraft : LT.lt (α := ℝ) 1 (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length)
K : ℝ := ∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length
maxLen : ℕ := S.sup List.length
hAbs : |1 / K| < 1
this : Tendsto (β := ℝ) (fun (r : ℕ) ↦ HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ) / K ^ r) atTop (nhds 0)
r : ℕ
hr : ∀ b ≥ r, HMul.hMul (α := ℝ) (↑b : ℝ) (↑maxLen : ℝ) / K ^ b < 1
⊢ r + 1 ≥ 1
have linarith : r + 1 < 1 → -1 + HSub.hSub (α := ℤ) 0 (↑r : ℤ) + (HAdd.hAdd (α := ℤ) (↑r : ℤ) 1 + 1 - 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.InformationTheory.Coding.KraftMcMillan (goal)
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
h_kraft : LT.lt (α := ℝ) 1 (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length)
K : ℝ := ∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length
maxLen : ℕ := S.sup List.length
hAbs : |1 / K| < 1
this : Tendsto (β := ℝ) (fun (r : ℕ) ↦ HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ) / K ^ r) atTop (nhds 0)
r : ℕ
hr : ∀ b ≥ r, HMul.hMul (α := ℝ) (↑b : ℝ) (↑maxLen : ℝ) / K ^ b < 1
⊢ ∃ r ≥ 1,
    HMul.hMul (α := ℝ) (↑r : ℝ) (↑(S.sup List.length) : ℝ) <
      HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) r
have refine : HMul.hMul (α := ℝ) (↑(r + 1) : ℝ) (↑(S.sup List.length) : ℝ) <
  HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) (r + 1)
Tactic: refine ⟨r + 1, by linarith, ?_⟩
-- Lean 4 proof step from Mathlib.InformationTheory.Coding.KraftMcMillan (goal)
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
h_kraft : LT.lt (α := ℝ) 1 (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length)
K : ℝ := ∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length
maxLen : ℕ := S.sup List.length
hAbs : |1 / K| < 1
this : Tendsto (β := ℝ) (fun (r : ℕ) ↦ HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ) / K ^ r) atTop (nhds 0)
r : ℕ
hr : ∀ b ≥ r, HMul.hMul (α := ℝ) (↑b : ℝ) (↑maxLen : ℝ) / K ^ b < 1
⊢ r + 1 ≥ r
have linarith : r + 1 < r → HMul.hMul (α := ℤ) 2 (-1) + (HAdd.hAdd (α := ℤ) (↑r : ℤ) 1 + 1 - (↑r : ℤ)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.InformationTheory.Coding.KraftMcMillan (goal)
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
h_kraft : LT.lt (α := ℝ) 1 (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length)
K : ℝ := ∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length
maxLen : ℕ := S.sup List.length
hAbs : |1 / K| < 1
this : Tendsto (β := ℝ) (fun (r : ℕ) ↦ HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ) / K ^ r) atTop (nhds 0)
r : ℕ
hr : ∀ b ≥ r, HMul.hMul (α := ℝ) (↑b : ℝ) (↑maxLen : ℝ) / K ^ b < 1
linarith : r + 1 < r → HMul.hMul (α := ℤ) 2 (-1) + (HAdd.hAdd (α := ℤ) (↑r : ℤ) 1 + 1 - (↑r : ℤ)) = 0
⊢ r + 1 ≥ r
have linarith₁ : r + 1 < r → GT.gt (α := ℤ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.InformationTheory.Coding.KraftMcMillan (hypothesis)
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
h_kraft : LT.lt (α := ℝ) 1 (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length)
K : ℝ := ∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length
maxLen : ℕ := S.sup List.length
hAbs : |1 / K| < 1
this : Tendsto (β := ℝ) (fun (r : ℕ) ↦ HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ) / K ^ r) atTop (nhds 0)
r : ℕ
hr : ∀ b ≥ r, HMul.hMul (α := ℝ) (↑b : ℝ) (↑maxLen : ℝ) / K ^ b < 1
⊢ HMul.hMul (α := ℝ) (↑(r + 1) : ℝ) (↑(S.sup List.length) : ℝ) <
    HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) (r + 1)
have this₁ : HMul.hMul (α := ℝ) (↑(r + 1) : ℝ) (↑maxLen : ℝ) / K ^ (r + 1) < 1
Tactic: have := hr (r + 1) (by linarith)
-- Lean 4 proof step from Mathlib.InformationTheory.Coding.KraftMcMillan (hypothesis)
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
h_kraft : LT.lt (α := ℝ) 1 (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length)
K : ℝ := ∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length
maxLen : ℕ := S.sup List.length
hAbs : |1 / K| < 1
this_1 : Tendsto (β := ℝ) (fun (r : ℕ) ↦ HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ) / K ^ r) atTop (nhds 0)
r : ℕ
hr : ∀ b ≥ r, HMul.hMul (α := ℝ) (↑b : ℝ) (↑maxLen : ℝ) / K ^ b < 1
this : HMul.hMul (α := ℝ) (↑(r + 1) : ℝ) (↑maxLen : ℝ) / K ^ (r + 1) < 1
⊢ HMul.hMul (α := ℝ) (↑(r + 1) : ℝ) (↑(S.sup List.length) : ℝ) <
    HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) (r + 1)
have this₁ : HMul.hMul (α := ℝ) (↑(r + 1) : ℝ) (↑maxLen : ℝ) < 1 * K ^ (r + 1)
Tactic: rw [div_lt_iff₀ (by positivity)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.InformationTheory.Coding.KraftMcMillan (goal)
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
h_kraft : LT.lt (α := ℝ) 1 (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length)
K : ℝ := ∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length
maxLen : ℕ := S.sup List.length
hAbs : |1 / K| < 1
this_1 : Tendsto (β := ℝ) (fun (r : ℕ) ↦ HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ) / K ^ r) atTop (nhds 0)
r : ℕ
hr : ∀ b ≥ r, HMul.hMul (α := ℝ) (↑b : ℝ) (↑maxLen : ℝ) / K ^ b < 1
this : HMul.hMul (α := ℝ) (↑(r + 1) : ℝ) (↑maxLen : ℝ) < 1 * K ^ (r + 1)
⊢ HMul.hMul (α := ℝ) (↑(r + 1) : ℝ) (↑(S.sup List.length) : ℝ) <
    HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) (r + 1)
have linarith : HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) (r + 1) ≤
    HMul.hMul (α := ℝ) (↑(r + 1) : ℝ) (↑(S.sup List.length) : ℝ) →
  HMul.hMul (α := ℝ) 1 1 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.InformationTheory.Coding.KraftMcMillan (goal)
Goal:
α : Type u_1
S : Finset (List α)
inst : Fintype α
inst_1 : Nonempty α
h : UniquelyDecodable (↑S : Set (List α))
h_kraft : LT.lt (α := ℝ) 1 (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length)
K : ℝ := ∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length
maxLen : ℕ := S.sup List.length
hAbs : |1 / K| < 1
this_1 : Tendsto (β := ℝ) (fun (r : ℕ) ↦ HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ) / K ^ r) atTop (nhds 0)
r : ℕ
hr : ∀ b ≥ r, HMul.hMul (α := ℝ) (↑b : ℝ) (↑maxLen : ℝ) / K ^ b < 1
this : HMul.hMul (α := ℝ) (↑(r + 1) : ℝ) (↑maxLen : ℝ) < 1 * K ^ (r + 1)
linarith :
  HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) (r + 1) ≤
      HMul.hMul (α := ℝ) (↑(r + 1) : ℝ) (↑(S.sup List.length) : ℝ) →
    HMul.hMul (α := ℝ) 1 1 = 1
⊢ HMul.hMul (α := ℝ) (↑(r + 1) : ℝ) (↑(S.sup List.length) : ℝ) <
    HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) (r + 1)
have linarith₁ : HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) (r + 1) ≤
    HMul.hMul (α := ℝ) (↑(r + 1) : ℝ) (↑(S.sup List.length) : ℝ) →
  HMul.hMul (α := ℝ) (↑(r + 1) : ℝ) (↑maxLen : ℝ) - 1 * K ^ (r + 1) +
      (1 * HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) (r + 1) -
        HMul.hMul (α := ℝ) 1 (↑(r + 1) : ℝ) * HMul.hMul (α := ℝ) 1 (↑(S.sup List.length) : ℝ)) =
    0
Tactic: linarith
-- 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
f g : Basis ι R M
h : f.repr = g.repr
⊢ f = g
have ofRepr : ∀ (repr : M ≃ₗ[R] ι →₀ R) (h : { repr := repr : Basis ι R M }.repr = g.repr), { repr := repr : Basis ι R M } = g
Tactic: cases f
Cleared hypotheses: f, h
-- 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
g : Basis ι R M
repr : M ≃ₗ[R] ι →₀ R
h : { repr := repr : Basis ι R M }.repr = g.repr
⊢ { repr := repr : Basis ι R M } = g
have ofRepr : ∀ (repr_1 : M ≃ₗ[R] ι →₀ R) (h : { repr := repr : Basis ι R M }.repr = { repr := repr_1 }.repr),
  { repr := repr : Basis ι R M } = { repr := repr_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
K : Type u_5
M : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b b₁ : Basis ι R M
i : ι
c : R
x : M
f g : Basis ι R M
h :
  Eq (α := (a : ι) → M) ((fun (b : Basis ι R M) (i : ι) ↦ ((b.repr.symm : (a : ι →₀ R) → M) (single i 1) : M)) f)
    ((fun (b : Basis ι R M) (i : ι) ↦ ((b.repr.symm : (a : ι →₀ R) → M) (single i 1) : M)) g)
⊢ (↑f.repr.symm : (ι →₀ R) →ₗ[R] M) = (↑g.repr.symm : (ι →₀ R) →ₗ[R] M)
have h₁ : ∀ (a : ι),
  Eq.{u_6 + 1} (α := M) (((↑f.repr.symm : (ι →₀ R) →ₗ[R] M) ∘ₗ lsingle a : (a : R) → M) 1 : M)
    (((↑g.repr.symm : (ι →₀ R) →ₗ[R] M) ∘ₗ lsingle a : (a : R) → M) 1 : M)
Tactic: ext
-- 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
b : Basis ι R M
i : ι
c : R
⊢ Eq.{u_6 + 1} (α := M) ((b.repr.symm : (a : ι →₀ R) → M) (single i c) : M)
    ((b.repr.symm : (a : ι →₀ R) → M) (HSMul.hSMul (β := ι →₀ R) c (single i 1)) : M)
have rw : Eq.{u_6 + 1} (α := M) ((b.repr.symm : (a : ι →₀ R) → M) (single i c) : M)
  ((b.repr.symm : (a : ι →₀ R) → M) (single i (c * 1)) : M)
Tactic: rw [Finsupp.smul_single', mul_one]
-- 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
b : Basis ι R M
i : ι
c : R
rw :
  Eq.{u_6 + 1} (α := M) ((b.repr.symm : (a : ι →₀ R) → M) (single i c) : M)
    ((b.repr.symm : (a : ι →₀ R) → M) (single i (c * 1)) : M)
⊢ Eq.{u_6 + 1} (α := M) ((b.repr.symm : (a : ι →₀ R) → M) (single i c) : M)
    ((b.repr.symm : (a : ι →₀ R) → M) (HSMul.hSMul (β := ι →₀ R) c (single i 1)) : M)
have rw₁ : Eq.{u_6 + 1} (α := M) ((b.repr.symm : (a : ι →₀ R) → M) (single i c) : M)
  ((b.repr.symm : (a : ι →₀ R) → M) (single i c) : M)
Tactic: rw [Finsupp.smul_single', mul_one]
-- 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
b : Basis ι R M
i : ι
c : R
⊢ Eq.{u_6 + 1} (α := M) ((b.repr.symm : (a : ι →₀ R) → M) (single i c) : M)
    ((b.repr.symm : (a : ι →₀ R) → M) (HSMul.hSMul (β := ι →₀ R) c (single i 1)) : M)
have rw : Eq.{u_6 + 1} (α := M) ((b.repr.symm : (a : ι →₀ R) → M) (single i c) : M)
  ((b.repr.symm : (a : ι →₀ R) → M) (single i (c * 1)) : M)
Tactic: { rw [Finsupp.smul_single', mul_one] }
-- 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
b : Basis ι R M
i : ι
c : R
rw :
  Eq.{u_6 + 1} (α := M) ((b.repr.symm : (a : ι →₀ R) → M) (single i c) : M)
    ((b.repr.symm : (a : ι →₀ R) → M) (single i (c * 1)) : M)
⊢ Eq.{u_6 + 1} (α := M) ((b.repr.symm : (a : ι →₀ R) → M) (single i c) : M)
    ((b.repr.symm : (a : ι →₀ R) → M) (HSMul.hSMul (β := ι →₀ R) c (single i 1)) : M)
have rw₁ : Eq.{u_6 + 1} (α := M) ((b.repr.symm : (a : ι →₀ R) → M) (single i c) : M)
  ((b.repr.symm : (a : ι →₀ R) → M) (single i c) : M)
Tactic: { rw [Finsupp.smul_single', mul_one] }
-- 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
b : Basis ι R M
i : ι
c : R
⊢ (b.repr.symm : (a : ι →₀ R) → M) (HSMul.hSMul (β := ι →₀ R) c (single i 1)) =
    HSMul.hSMul (β := M) c ((b : (a : ι) → M) i : M)
have rw : HSMul.hSMul (β := M) c ((b.repr.symm : (a : ι →₀ R) → M) (single i 1) : M) =
  HSMul.hSMul (β := M) c ((b : (a : ι) → M) i : M)
Tactic: rw [map_smul, repr_symm_single_one]
-- 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
b : Basis ι R M
i : ι
c : R
rw :
  HSMul.hSMul (β := M) c ((b.repr.symm : (a : ι →₀ R) → M) (single i 1) : M) =
    HSMul.hSMul (β := M) c ((b : (a : ι) → M) i : M)
⊢ (b.repr.symm : (a : ι →₀ R) → M) (HSMul.hSMul (β := ι →₀ R) c (single i 1)) =
    HSMul.hSMul (β := M) c ((b : (a : ι) → M) i : M)
have rw₁ : HSMul.hSMul (β := M) c ((b : (a : ι) → M) i : M) = HSMul.hSMul (β := M) c ((b : (a : ι) → M) i : M)
Tactic: rw [map_smul, repr_symm_single_one]
-- 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
b : Basis ι R M
i j : ι
inst_3 : Decidable (i = j)
⊢ Eq.{u_3 + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) ((b : (a : ι) → M) i) : ι →₀ R) : (a : ι) → R) j : R)
    (if i = j then 1 else 0 : R)
have rw : Eq.{u_3 + 1} (α := R) ((single i 1 : (a : ι) → R) j : R) (if i = j then 1 else 0 : R)
Tactic: rw [repr_self, Finsupp.single_apply]
-- 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
b : Basis ι R M
i j : ι
inst_3 : Decidable (i = j)
rw : Eq.{u_3 + 1} (α := R) ((single i 1 : (a : ι) → R) j : R) (if i = j then 1 else 0 : R)
⊢ Eq.{u_3 + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) ((b : (a : ι) → M) i) : ι →₀ R) : (a : ι) → R) j : R)
    (if i = j then 1 else 0 : R)
have rw₁ : Eq.{u_3 + 1} (α := R) (if i = j then 1 else 0) (if i = j then 1 else 0)
Tactic: rw [repr_self, Finsupp.single_apply]
-- 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
b : Basis ι R M
v : ι →₀ R
⊢ (b.repr : (a : M) → ι →₀ R) ((linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) v) = v
have rw : (b.repr : (a : M) → ι →₀ R) (((↑b.repr.symm : (ι →₀ R) →ₗ[R] M) : (a : ι →₀ R) → M) v) = v
Tactic: rw [← b.coe_repr_symm]
-- 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
b : Basis ι R M
x : M
⊢ (linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) ((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) = x
have rw : ((↑b.repr.symm : (ι →₀ R) →ₗ[R] M) : (a : ι →₀ R) → M) ((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) = x
Tactic: rw [← b.coe_repr_symm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
e : ι ≃ ι'
i' : ι'
⊢ Eq.{u_6 + 1} (α := M) ((LinearEquiv.symm (b.repr ≪≫ₗ Finsupp.domLCongr e) : (a : ι' →₀ R) → M) (single i' 1) : M)
    ((b.repr.symm : (a : ι →₀ R) → M) (single ((e.symm : (a : ι') → ι) i') 1 : ι →₀ R) : M)
have rw : Eq.{u_6 + 1} (α := M)
  ((b.repr.symm : (a : ι →₀ R) → M)
      ((LinearEquiv.symm (Finsupp.domLCongr e) : (a : ι' →₀ R) → ι →₀ R) (single i' 1) : ι →₀ R) :
    M)
  ((b.repr.symm : (a : ι →₀ R) → M) (single ((e.symm : (a : ι') → ι) i') 1 : ι →₀ R) : M)
Tactic: rw [LinearEquiv.symm_trans_apply, Finsupp.domLCongr_symm, Finsupp.domLCongr_single]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
e : ι ≃ ι'
i' : ι'
rw :
  Eq.{u_6 + 1} (α := M)
    ((b.repr.symm : (a : ι →₀ R) → M)
        ((LinearEquiv.symm (Finsupp.domLCongr e) : (a : ι' →₀ R) → ι →₀ R) (single i' 1) : ι →₀ R) :
      M)
    ((b.repr.symm : (a : ι →₀ R) → M) (single ((e.symm : (a : ι') → ι) i') 1 : ι →₀ R) : M)
⊢ Eq.{u_6 + 1} (α := M) ((LinearEquiv.symm (b.repr ≪≫ₗ Finsupp.domLCongr e) : (a : ι' →₀ R) → M) (single i' 1) : M)
    ((b.repr.symm : (a : ι →₀ R) → M) (single ((e.symm : (a : ι') → ι) i') 1 : ι →₀ R) : M)
have rw₁ : Eq.{u_6 + 1} (α := M)
  ((b.repr.symm : (a : ι →₀ R) → M) ((Finsupp.domLCongr e.symm : (a : ι' →₀ R) → ι →₀ R) (single i' 1) : ι →₀ R) : M)
  ((b.repr.symm : (a : ι →₀ R) → M) (single ((e.symm : (a : ι') → ι) i') 1 : ι →₀ R) : M)
Tactic: rw [LinearEquiv.symm_trans_apply, Finsupp.domLCongr_symm, Finsupp.domLCongr_single]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
e : ι ≃ ι'
i' : ι'
rw :
  Eq.{u_6 + 1} (α := M)
    ((b.repr.symm : (a : ι →₀ R) → M)
        ((LinearEquiv.symm (Finsupp.domLCongr e) : (a : ι' →₀ R) → ι →₀ R) (single i' 1) : ι →₀ R) :
      M)
    ((b.repr.symm : (a : ι →₀ R) → M) (single ((e.symm : (a : ι') → ι) i') 1 : ι →₀ R) : M)
rw₁ :
  Eq.{u_6 + 1} (α := M)
    ((b.repr.symm : (a : ι →₀ R) → M) ((Finsupp.domLCongr e.symm : (a : ι' →₀ R) → ι →₀ R) (single i' 1) : ι →₀ R) : M)
    ((b.repr.symm : (a : ι →₀ R) → M) (single ((e.symm : (a : ι') → ι) i') 1 : ι →₀ R) : M)
⊢ Eq.{u_6 + 1} (α := M) ((LinearEquiv.symm (b.repr ≪≫ₗ Finsupp.domLCongr e) : (a : ι' →₀ R) → M) (single i' 1) : M)
    ((b.repr.symm : (a : ι →₀ R) → M) (single ((e.symm : (a : ι') → ι) i') 1 : ι →₀ R) : M)
have rw₂ : Eq.{u_6 + 1} (α := M) ((b.repr.symm : (a : ι →₀ R) → M) (single ((e.symm : (a : ι') → ι) i') 1 : ι →₀ R) : M)
  ((b.repr.symm : (a : ι →₀ R) → M) (single ((e.symm : (a : ι') → ι) i') 1 : ι →₀ R) : M)
Tactic: rw [LinearEquiv.symm_trans_apply, Finsupp.domLCongr_symm, Finsupp.domLCongr_single]
-- 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 : Fintype ι
b : Basis ι R M
u : M
⊢ ∑ i : ι,
      HSMul.hSMul.{u_3, u_6, u_6} (α := R) (β := M) ((b.equivFun : (a : M) → ι → R) u i : R) ((b : (a : ι) → M) i : M) =
    u
have rw : (b.equivFun.symm : (a : ι → R) → M) ((b.equivFun : (a : M) → ι → R) u : ι → R) = u
Tactic: rw [← b.equivFun_symm_apply, b.equivFun.symm_apply_apply]
-- 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 : Fintype ι
b : Basis ι R M
u : M
rw : (b.equivFun.symm : (a : ι → R) → M) ((b.equivFun : (a : M) → ι → R) u : ι → R) = u
⊢ ∑ i : ι,
      HSMul.hSMul.{u_3, u_6, u_6} (α := R) (β := M) ((b.equivFun : (a : M) → ι → R) u i : R) ((b : (a : ι) → M) i : M) =
    u
have rw₁ : u = u
Tactic: rw [← b.equivFun_symm_apply, b.equivFun.symm_apply_apply]
-- 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 ι
inst_4 : DecidableEq ι
b : Basis ι R M
i j : ι
⊢ Eq.{u_3 + 1} (α := R) ((b.equivFun : (a : M) → ι → R) ((b : (a : ι) → M) i : M) j : R) (if i = j then 1 else 0 : R)
have rw : Eq.{u_3 + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) ((b : (a : ι) → M) i) : ι →₀ R) : (a : ι) → R) j : R)
  (if i = j then 1 else 0 : R)
Tactic: rw [b.equivFun_apply, b.repr_self_apply]
-- 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 ι
inst_4 : DecidableEq ι
b : Basis ι R M
i j : ι
rw :
  Eq.{u_3 + 1} (α := R) ((((b.repr : (a : M) → ι →₀ R) ((b : (a : ι) → M) i) : ι →₀ R) : (a : ι) → R) j : R)
    (if i = j then 1 else 0 : R)
⊢ Eq.{u_3 + 1} (α := R) ((b.equivFun : (a : M) → ι → R) ((b : (a : ι) → M) i : M) j : R) (if i = j then 1 else 0 : R)
have rw₁ : Eq.{u_3 + 1} (α := R) (if i = j then 1 else 0) (if i = j then 1 else 0)
Tactic: rw [b.equivFun_apply, b.repr_self_apply]
-- 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 : Fintype ι
b : Basis ι R M
c : ι → R
⊢ (⇑((b.repr : (a : M) → ι →₀ R) (∑ i : ι, HSMul.hSMul (β := M) (c i) ((b : (a : ι) → M) i : M))) : (a : ι) → R) = c
have simp_rw : (⇑((b.repr : (a : M) → ι →₀ R) ((b.equivFun.symm : (a : ι → R) → M) c) : ι →₀ R) : (a : ι) → R) = c
Tactic: simp_rw [← b.equivFun_symm_apply, ← b.equivFun_apply, b.equivFun.apply_symm_apply]
-- 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 : Fintype ι
b : Basis ι R M
c : ι → R
simp_rw : (⇑((b.repr : (a : M) → ι →₀ R) ((b.equivFun.symm : (a : ι → R) → M) c) : ι →₀ R) : (a : ι) → R) = c
⊢ (⇑((b.repr : (a : M) → ι →₀ R) (∑ i : ι, HSMul.hSMul (β := M) (c i) ((b : (a : ι) → M) i : M))) : (a : ι) → R) = c
have simp_rw₁ : (b.equivFun : (a : M) → ι → R) ((b.equivFun.symm : (a : ι → R) → M) c : M) = c
Tactic: simp_rw [← b.equivFun_symm_apply, ← b.equivFun_apply, b.equivFun.apply_symm_apply]
-- 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 ι
v : Basis ι R M
⊢ (ofEquivFun v.equivFun).repr = v.repr
have h : ∀ (x : M) (a : ι),
  Eq.{u_3 + 1} (α := R) (((((ofEquivFun v.equivFun).repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R)
    ((((v.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) a : R)
Tactic: ext
-- 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
⊢ (ofEquivFun e).equivFun = e
have h : ∀ (j : M) (x : ι),
  Eq.{u_3 + 1} (α := R) (((ofEquivFun e).equivFun : (a : M) → ι → R) j x : R) ((e : (a : M) → ι → R) j x : R)
Tactic: ext j