awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
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
⊢ 0 < 1 / K

Tactic:
positivity
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
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
grw : 1 < K
grw₁ : 0 < K
⊢ |1 / K| < 1

Tactic:
grw [abs_of_pos (by positivity), div_lt_one]

Premises used: div_lt_one, abs_of_pos
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
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
⊢ 1 < K

Tactic:
grind
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
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
⊢ 0 < K

Tactic:
grind
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
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
⊢ |1 / K| < 1

Tactic:
have hAbs : |1 / K| < 1 := by
    grw [abs_of_pos (by positivity), div_lt_one] <;> grind
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
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
⊢ Tendsto (β := ℝ) (fun (r : ℕ) ↦ HMul.hMul (α := ℝ) (↑r : ℝ) (↑maxLen : ℝ) / K ^ r) atTop (nhds 0)

Tactic:
simpa [mul_left_comm, mul_div_assoc] using
      (tendsto_self_mul_const_pow_of_abs_lt_one hAbs).const_mul (maxLen : ℝ)

Premises used: mul_div_assoc, mul_left_comm, Nat.cast, Filter.Tendsto.const_mul, tendsto_self_mul_const_pow_of_abs_lt_one
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
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
⊢ 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 : ℝ)
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
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)
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
⊢ ∃ 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

Premises used: gt_mem_nhds, zero_lt_one, Filter.Tendsto.eventually, Iff.mp, Filter.eventually_atTop
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
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 < 1 → -1 + HSub.hSub (α := ℤ) 0 (↑r : ℤ) + (HAdd.hAdd (α := ℤ) (↑r : ℤ) 1 + 1 - 1) = 0
⊢ r + 1 ≥ 1

Tactic:
linarith
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
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
refine :
  HMul.hMul (α := ℝ) (↑(r + 1) : ℝ) (↑(S.sup List.length) : ℝ) <
    HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) (r + 1)
⊢ ∃ r ≥ 1,
    HMul.hMul (α := ℝ) (↑r : ℝ) (↑(S.sup List.length) : ℝ) <
      HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) r

Tactic:
refine ⟨r + 1, by linarith, ?_⟩
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
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
linarith₁ : r + 1 < r → GT.gt (α := ℤ) 2 0
⊢ r + 1 ≥ r

Tactic:
linarith
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
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) : ℝ) (↑maxLen : ℝ) / K ^ (r + 1) < 1

Tactic:
have := hr (r + 1) (by linarith)
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
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
⊢ 0 < K ^ (r + 1)

Tactic:
positivity
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
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) : ℝ) (↑maxLen : ℝ) < 1 * K ^ (r + 1)

Tactic:
rw [div_lt_iff₀ (by positivity)] at this

Premises used: div_lt_iff₀
-- Module: Mathlib.InformationTheory.Coding.KraftMcMillan
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
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
⊢ HMul.hMul (α := ℝ) (↑(r + 1) : ℝ) (↑(S.sup List.length) : ℝ) <
    HPow.hPow (α := ℝ) (∑ w ∈ S, HDiv.hDiv (α := ℝ) 1 (↑(Fintype.card α) : ℝ) ^ w.length) (r + 1)

Tactic:
linarith
-- Module: Mathlib.LinearAlgebra.Basis.Defs
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
ofRepr :
  ∀ (repr : M ≃ₗ[R] ι →₀ R) (h : { repr := repr : Basis ι R M }.repr = g.repr), { repr := repr : Basis ι R M } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.LinearAlgebra.Basis.Defs
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
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 }
⊢ { repr := repr : Basis ι R M } = g

Tactic:
cases g
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_1
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
repr 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:
congr
-- Module: Mathlib.LinearAlgebra.Basis.Defs
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)
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)
⊢ (↑f.repr.symm : (ι →₀ R) →ₗ[R] M) = (↑g.repr.symm : (ι →₀ R) →ₗ[R] M)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Basis.Defs
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)
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:
congr_fun h _

Premises used: congr_fun, Finsupp.single
-- Module: Mathlib.LinearAlgebra.Basis.Defs
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)
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:
exact congr_fun h _

Premises used: congr_fun
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_1
R : Type u_3
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : M ≃ₗ[R] ι →₀ R
⊢ Eq (α := (a : ι) → M) (⇑{ repr := e : Basis ι R M } : (a : ι) → M) fun (i : ι) ↦
    (e.symm : (a : ι →₀ R) → M) (single i 1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Basis.Defs
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
inst_3 : Nontrivial R
⊢ Injective.{u_1 + 1, u_6 + 1} (α := ι) (β := M) (⇑b : (a : ι) → M)

Tactic:
b.repr.symm.injective.comp fun _ _ => (Finsupp.single_left_inj (one_ne_zero : (1 : R) ≠ 0)).mp

Premises used: LinearEquiv.symm, Module.Basis.repr, Function.Injective.comp, Iff.mp, Finsupp.single_left_inj, LinearEquiv.injective, one_ne_zero
-- Module: Mathlib.LinearAlgebra.Basis.Defs
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 : ι
⊢ Eq.{u_6 + 1} (α := M) ((b.repr.symm : (a : ι →₀ R) → M) (single i 1) : M) ((b : (a : ι) → M) i : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Basis.Defs
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)
rw₁ 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)
⊢ 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)

Tactic:
rw [Finsupp.smul_single', mul_one]

Premises used: Finsupp.smul_single', mul_one
-- Module: Mathlib.LinearAlgebra.Basis.Defs
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)
rw₁ 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)
⊢ 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)

Tactic:
{ rw [Finsupp.smul_single', mul_one] }

Premises used: Finsupp.smul_single', mul_one
-- Module: Mathlib.LinearAlgebra.Basis.Defs
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)
rw₁ rw₂ : HSMul.hSMul (β := M) c ((b : (a : ι) → M) i : 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)

Tactic:
rw [map_smul, repr_symm_single_one]

Premises used: Module.Basis.repr_symm_single_one, map_smul
-- Module: Mathlib.LinearAlgebra.Basis.Defs
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 : ι
⊢ Eq (α := ι →₀ R) ((b.repr : (a : M) → ι →₀ R) ((b : (a : ι) → M) i) : ι →₀ R) (single i 1 : ι →₀ R)

Tactic:
LinearEquiv.apply_symm_apply _ _

Premises used: LinearEquiv.apply_symm_apply
-- Module: Mathlib.LinearAlgebra.Basis.Defs
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)
rw₁ rw₂ : Eq.{u_3 + 1} (α := R) (if i = j then 1 else 0) (if i = j then 1 else 0)
⊢ 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 [repr_self, Finsupp.single_apply]

Premises used: Finsupp.single_apply, Module.Basis.repr_self
-- Module: Mathlib.LinearAlgebra.Basis.Defs
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
⊢ Eq.{u_6 + 1} (α := M) ((b.repr.symm : (a : ι →₀ R) → M) v : M) ((b.repr.symm : (a : ι →₀ R) → M) (v.sum single) : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Basis.Defs
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
⊢ Eq.{u_6 + 1} (α := M) (v.sum fun (i : ι) (vi : R) ↦ (b.repr.symm : (a : ι →₀ R) → M) (single i vi) : M)
    ((linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) v : M)

Tactic:
simp only [repr_symm_single,
                                                         Finsupp.linearCombination_apply]

Premises used: Module.Basis.repr_symm_single, Finsupp.linearCombination_apply
-- Module: Mathlib.LinearAlgebra.Basis.Defs
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
⊢ (↑b.repr.symm : (ι →₀ R) →ₗ[R] M) = linearCombination R (⇑b : (a : ι) → M)

Tactic:
LinearMap.ext fun v => b.repr_symm_apply v

Premises used: LinearMap.ext, Module.Basis.repr_symm_apply
-- Module: Mathlib.LinearAlgebra.Basis.Defs
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
rw : (b.repr : (a : M) → ι →₀ R) (((↑b.repr.symm : (ι →₀ R) →ₗ[R] M) : (a : ι →₀ R) → M) v) = v
⊢ (b.repr : (a : M) → ι →₀ R) ((linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) v) = v

Tactic:
rw [← b.coe_repr_symm]

Premises used: Module.Basis.coe_repr_symm
-- Module: Mathlib.LinearAlgebra.Basis.Defs
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) (((↑b.repr.symm : (ι →₀ R) →ₗ[R] M) : (a : ι →₀ R) → M) v) = v

Tactic:
b.repr.apply_symm_apply v

Premises used: Module.Basis.repr, LinearEquiv.apply_symm_apply
-- Module: Mathlib.LinearAlgebra.Basis.Defs
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) (((↑b.repr.symm : (ι →₀ R) →ₗ[R] M) : (a : ι →₀ R) → M) v) = v

Tactic:
exact b.repr.apply_symm_apply v

Premises used: Module.Basis.repr, LinearEquiv.apply_symm_apply
-- Module: Mathlib.LinearAlgebra.Basis.Defs
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
rw : ((↑b.repr.symm : (ι →₀ R) →ₗ[R] M) : (a : ι →₀ R) → M) ((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) = x
⊢ (linearCombination R (⇑b : (a : ι) → M) : (a : ι →₀ R) → M) ((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) = x

Tactic:
rw [← b.coe_repr_symm]

Premises used: Module.Basis.coe_repr_symm
-- Module: Mathlib.LinearAlgebra.Basis.Defs
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
⊢ ((↑b.repr.symm : (ι →₀ R) →ₗ[R] M) : (a : ι →₀ R) → M) ((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) = x

Tactic:
b.repr.symm_apply_apply x

Premises used: LinearEquiv.symm_apply_apply, Module.Basis.repr
-- Module: Mathlib.LinearAlgebra.Basis.Defs
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
⊢ ((↑b.repr.symm : (ι →₀ R) →ₗ[R] M) : (a : ι →₀ R) → M) ((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) = x

Tactic:
exact b.repr.symm_apply_apply x

Premises used: LinearEquiv.symm_apply_apply, Module.Basis.repr
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_1
R : Type u_3
M : Type u_6
M' : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b : Basis ι R M
f : M ≃ₗ[R] M'
i : ι
⊢ Eq.{u_7 + 1} (α := M') ((b.map f : (a : ι) → M') i : M') ((f : (a : M) → M') ((b : (a : ι) → M) i : M) : M')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_1
R : Type u_3
M : Type u_6
M' : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b : Basis ι R M
f : M ≃ₗ[R] M'
⊢ Eq (α := (a : ι) → M') (⇑(b.map f) : (a : ι) → M')
    (comp.{u_1 + 1, u_6 + 1, u_7 + 1} (β := M) (⇑f : (a : M) → M') (⇑b : (a : ι) → M))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Basis.Defs
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)
rw₂ 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)
⊢ 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)

Tactic:
rw [LinearEquiv.symm_trans_apply, Finsupp.domLCongr_symm, Finsupp.domLCongr_single]

Premises used: LinearEquiv.symm_trans_apply, Finsupp.domLCongr_symm, Finsupp.domLCongr_single