awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
Goal:
R : Type uR
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : DecidableEq ι
b : Basis ι R M
inst_4 : Finite ι
i j : ι
rw :
  Eq.{uR + 1} (α := R)
    ((((b.dualBasis.toDual : (a : Dual R M) → Dual R (Dual R M))
              ((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i)) :
            Dual R (Dual R M)) :
          (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
rw₁ :
  Eq.{uR + 1} (α := R)
    ((((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) ((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i)) : ι →₀ R) :
          (a : ι) → R)
        j :
      R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
rw₂ :
  Eq.{uR + 1} (α := R) ((((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) (b.coord i) : ι →₀ R) : (a : ι) → R) j : R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
⊢ Eq.{uR + 1} (α := R)
    ((((b.dualBasis.toDual ∘ₗ b.toDual : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) :
          (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
have rw₃ : Eq.{uR + 1} (α := R)
  ((((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) ((b.dualBasis : (a : ι) → Dual R M) i) : ι →₀ R) : (a : ι) → R) j : R)
  ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
      ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
    R)
Tactic: rw [LinearMap.comp_apply, toDual_apply_left, coe_toDual_self, ← coe_dualBasis,
    Dual.eval_apply, Basis.repr_self, Finsupp.single_apply, dualBasis_apply_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
Goal:
R : Type uR
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : DecidableEq ι
b : Basis ι R M
inst_4 : Finite ι
i j : ι
rw :
  Eq.{uR + 1} (α := R)
    ((((b.dualBasis.toDual : (a : Dual R M) → Dual R (Dual R M))
              ((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i)) :
            Dual R (Dual R M)) :
          (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
rw₁ :
  Eq.{uR + 1} (α := R)
    ((((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) ((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i)) : ι →₀ R) :
          (a : ι) → R)
        j :
      R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
rw₂ :
  Eq.{uR + 1} (α := R) ((((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) (b.coord i) : ι →₀ R) : (a : ι) → R) j : R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
rw₃ :
  Eq.{uR + 1} (α := R)
    ((((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) ((b.dualBasis : (a : ι) → Dual R M) i) : ι →₀ R) : (a : ι) → R) j :
      R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
⊢ Eq.{uR + 1} (α := R)
    ((((b.dualBasis.toDual ∘ₗ b.toDual : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) :
          (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
have rw₄ : Eq.{uR + 1} (α := R)
  ((((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) ((b.dualBasis : (a : ι) → Dual R M) i) : ι →₀ R) : (a : ι) → R) j : R)
  ((((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
Tactic: rw [LinearMap.comp_apply, toDual_apply_left, coe_toDual_self, ← coe_dualBasis,
    Dual.eval_apply, Basis.repr_self, Finsupp.single_apply, dualBasis_apply_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
Goal:
R : Type uR
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : DecidableEq ι
b : Basis ι R M
inst_4 : Finite ι
i j : ι
rw :
  Eq.{uR + 1} (α := R)
    ((((b.dualBasis.toDual : (a : Dual R M) → Dual R (Dual R M))
              ((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i)) :
            Dual R (Dual R M)) :
          (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
rw₁ :
  Eq.{uR + 1} (α := R)
    ((((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) ((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i)) : ι →₀ R) :
          (a : ι) → R)
        j :
      R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
rw₂ :
  Eq.{uR + 1} (α := R) ((((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) (b.coord i) : ι →₀ R) : (a : ι) → R) j : R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
rw₃ :
  Eq.{uR + 1} (α := R)
    ((((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) ((b.dualBasis : (a : ι) → Dual R M) i) : ι →₀ R) : (a : ι) → R) j :
      R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
rw₄ :
  Eq.{uR + 1} (α := R)
    ((((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) ((b.dualBasis : (a : ι) → Dual R M) i) : ι →₀ R) : (a : ι) → R) j :
      R)
    ((((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
⊢ Eq.{uR + 1} (α := R)
    ((((b.dualBasis.toDual ∘ₗ b.toDual : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) :
          (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
have rw₅ : Eq.{uR + 1} (α := R) ((Finsupp.single i 1 : (a : ι) → R) j : R)
  ((((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
Tactic: rw [LinearMap.comp_apply, toDual_apply_left, coe_toDual_self, ← coe_dualBasis,
    Dual.eval_apply, Basis.repr_self, Finsupp.single_apply, dualBasis_apply_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
Goal:
R : Type uR
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : DecidableEq ι
b : Basis ι R M
inst_4 : Finite ι
i j : ι
rw :
  Eq.{uR + 1} (α := R)
    ((((b.dualBasis.toDual : (a : Dual R M) → Dual R (Dual R M))
              ((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i)) :
            Dual R (Dual R M)) :
          (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
rw₁ :
  Eq.{uR + 1} (α := R)
    ((((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) ((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i)) : ι →₀ R) :
          (a : ι) → R)
        j :
      R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
rw₂ :
  Eq.{uR + 1} (α := R) ((((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) (b.coord i) : ι →₀ R) : (a : ι) → R) j : R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
rw₃ :
  Eq.{uR + 1} (α := R)
    ((((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) ((b.dualBasis : (a : ι) → Dual R M) i) : ι →₀ R) : (a : ι) → R) j :
      R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
rw₄ :
  Eq.{uR + 1} (α := R)
    ((((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) ((b.dualBasis : (a : ι) → Dual R M) i) : ι →₀ R) : (a : ι) → R) j :
      R)
    ((((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
rw₅ :
  Eq.{uR + 1} (α := R) ((Finsupp.single i 1 : (a : ι) → R) j : R)
    ((((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
⊢ Eq.{uR + 1} (α := R)
    ((((b.dualBasis.toDual ∘ₗ b.toDual : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) :
          (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
have rw₆ : Eq.{uR + 1} (α := R) (if i = j then 1 else 0 : R)
  ((((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
Tactic: rw [LinearMap.comp_apply, toDual_apply_left, coe_toDual_self, ← coe_dualBasis,
    Dual.eval_apply, Basis.repr_self, Finsupp.single_apply, dualBasis_apply_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
Goal:
R : Type uR
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : DecidableEq ι
b : Basis ι R M
inst_4 : Finite ι
i j : ι
rw :
  Eq.{uR + 1} (α := R)
    ((((b.dualBasis.toDual : (a : Dual R M) → Dual R (Dual R M))
              ((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i)) :
            Dual R (Dual R M)) :
          (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
rw₁ :
  Eq.{uR + 1} (α := R)
    ((((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) ((b.toDual : (a : M) → Dual R M) ((b : (a : ι) → M) i)) : ι →₀ R) :
          (a : ι) → R)
        j :
      R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
rw₂ :
  Eq.{uR + 1} (α := R) ((((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) (b.coord i) : ι →₀ R) : (a : ι) → R) j : R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
rw₃ :
  Eq.{uR + 1} (α := R)
    ((((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) ((b.dualBasis : (a : ι) → Dual R M) i) : ι →₀ R) : (a : ι) → R) j :
      R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
rw₄ :
  Eq.{uR + 1} (α := R)
    ((((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) ((b.dualBasis : (a : ι) → Dual R M) i) : ι →₀ R) : (a : ι) → R) j :
      R)
    ((((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
rw₅ :
  Eq.{uR + 1} (α := R) ((Finsupp.single i 1 : (a : ι) → R) j : R)
    ((((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
rw₆ :
  Eq.{uR + 1} (α := R) (if i = j then 1 else 0 : R)
    ((((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
⊢ Eq.{uR + 1} (α := R)
    ((((b.dualBasis.toDual ∘ₗ b.toDual : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) :
          (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M)) ((b : (a : ι) → M) i) : Dual R (Dual R M)) : (a : Dual R M) → R)
        ((b.dualBasis : (a : ι) → Dual R M) j : Dual R M) :
      R)
have rw₇ : Eq.{uR + 1} (α := R) (if i = j then 1 else 0) (if i = j then 1 else 0)
Tactic: rw [LinearMap.comp_apply, toDual_apply_left, coe_toDual_self, ← coe_dualBasis,
    Dual.eval_apply, Basis.repr_self, Finsupp.single_apply, dualBasis_apply_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
Goal:
R : Type uR
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : DecidableEq ι
b : Basis ι R M
inst_4 : Finite ι
l : Dual R M
i : ι
⊢ Eq.{uR + 1} (α := R) ((b.dualBasis.equivFun : (a : Dual R M) → ι → R) l i : R)
    ((l : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
have rw : Eq.{uR + 1} (α := R) ((((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) l : ι →₀ R) : (a : ι) → R) i : R)
  ((l : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
Tactic: rw [Basis.equivFun_apply, dualBasis_repr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
Goal:
R : Type uR
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : DecidableEq ι
b : Basis ι R M
inst_4 : Finite ι
l : Dual R M
i : ι
rw :
  Eq.{uR + 1} (α := R) ((((b.dualBasis.repr : (a : Dual R M) → ι →₀ R) l : ι →₀ R) : (a : ι) → R) i : R)
    ((l : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
⊢ Eq.{uR + 1} (α := R) ((b.dualBasis.equivFun : (a : Dual R M) → ι → R) l i : R)
    ((l : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
have rw₁ : Eq.{uR + 1} (α := R) ((l : (a : M) → R) ((b : (a : ι) → M) i : M) : R) ((l : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
Tactic: rw [Basis.equivFun_apply, dualBasis_repr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (hypothesis)
Goal:
R : Type uR
M : Type uM
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_1
b : Basis ι R M
m m' : M
eq :
  Eq (α := Dual R (Dual R M)) ((Dual.eval R M : (a : M) → Dual R (Dual R M)) m : Dual R (Dual R M))
    ((Dual.eval R M : (a : M) → Dual R (Dual R M)) m' : Dual R (Dual R M))
⊢ m = m'
have eq₁ : ∀ (x : Dual R M), Eq.{uR + 1} (α := R) ((x : (a : M) → R) m : R) ((x : (a : M) → R) m' : R)
Tactic: simp_rw [LinearMap.ext_iff, Dual.eval_apply] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
Goal:
R : Type uR
M : Type uM
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_1
inst_3 : Finite ι
b : Basis ι R M
⊢ Eq (α := Submodule R (Dual R (Dual R M))) (range (Dual.eval R M)) ⊤
have intro : ∀ (val : Fintype ι), Eq (α := Submodule R (Dual R (Dual R M))) (range (Dual.eval R M)) ⊤
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
Goal:
R : Type uR
M : Type uM
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_1
inst_3 : Finite ι
b : Basis ι R M
val : Fintype ι
⊢ Eq (α := Submodule R (Dual R (Dual R M))) (range (Dual.eval R M)) ⊤
have intro : (b.dualBasis.toDual ∘ₗ b.toDual).range = ⊤
Tactic: rw [← b.toDual_toDual, range_comp, b.toDual_range, Submodule.map_top, toDual_range _]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
Goal:
R : Type uR
M : Type uM
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_1
inst_3 : Finite ι
b : Basis ι R M
val : Fintype ι
intro : (b.dualBasis.toDual ∘ₗ b.toDual).range = ⊤
⊢ Eq (α := Submodule R (Dual R (Dual R M))) (range (Dual.eval R M)) ⊤
have intro₁ : map b.dualBasis.toDual b.toDual.range = ⊤
Tactic: rw [← b.toDual_toDual, range_comp, b.toDual_range, Submodule.map_top, toDual_range _]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
Goal:
R : Type uR
M : Type uM
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_1
inst_3 : Finite ι
b : Basis ι R M
val : Fintype ι
intro : (b.dualBasis.toDual ∘ₗ b.toDual).range = ⊤
intro₁ : map b.dualBasis.toDual b.toDual.range = ⊤
⊢ Eq (α := Submodule R (Dual R (Dual R M))) (range (Dual.eval R M)) ⊤
have intro₂ : map b.dualBasis.toDual ⊤ = ⊤
Tactic: rw [← b.toDual_toDual, range_comp, b.toDual_range, Submodule.map_top, toDual_range _]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
Goal:
R : Type uR
M : Type uM
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_1
inst_3 : Finite ι
b : Basis ι R M
val : Fintype ι
intro : (b.dualBasis.toDual ∘ₗ b.toDual).range = ⊤
intro₁ : map b.dualBasis.toDual b.toDual.range = ⊤
intro₂ : map b.dualBasis.toDual ⊤ = ⊤
⊢ Eq (α := Submodule R (Dual R (Dual R M))) (range (Dual.eval R M)) ⊤
have intro₃ : b.dualBasis.toDual.range = ⊤
Tactic: rw [← b.toDual_toDual, range_comp, b.toDual_range, Submodule.map_top, toDual_range _]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
Goal:
R : Type uR
M : Type uM
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_1
inst_3 : Finite ι
b : Basis ι R M
val : Fintype ι
intro : (b.dualBasis.toDual ∘ₗ b.toDual).range = ⊤
intro₁ : map b.dualBasis.toDual b.toDual.range = ⊤
intro₂ : map b.dualBasis.toDual ⊤ = ⊤
intro₃ : b.dualBasis.toDual.range = ⊤
⊢ Eq (α := Submodule R (Dual R (Dual R M))) (range (Dual.eval R M)) ⊤
have intro₄ : Eq (α := Submodule R (Dual R (Dual R M))) ⊤ ⊤
Tactic: rw [← b.toDual_toDual, range_comp, b.toDual_range, Submodule.map_top, toDual_range _]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
Goal:
R : Type uR
M : Type uM
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_1
inst_3 : Finite ι
b : Basis ι R M
⊢ Eq (α := Submodule R (Dual R (Dual R M))) (range (Dual.eval R M)) ⊤
have intro : ∀ (val : Fintype ι), Eq (α := Submodule R (Dual R (Dual R M))) (range (Dual.eval R M)) ⊤
Tactic: classical
    cases nonempty_fintype ι
    rw [← b.toDual_toDual, range_comp, b.toDual_range, Submodule.map_top, toDual_range _]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
Goal:
R : Type uR
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Finite ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ Eq.{uR + 1} (α := R)
    ((((Finsupp.linearCombination R b.coord : (a : ι →₀ R) → M →ₗ[R] R) f : M →ₗ[R] R) : (a : M) → R)
        ((b : (a : ι) → M) i : M) :
      R)
    ((f : (a : ι) → R) i : R)
have haveI : ∀ (this : DecidableEq ι),
  Eq.{uR + 1} (α := R)
    ((((Finsupp.linearCombination R b.coord : (a : ι →₀ R) → M →ₗ[R] R) f : M →ₗ[R] R) : (a : M) → R)
        ((b : (a : ι) → M) i : M) :
      R)
    ((f : (a : ι) → R) i : R)
Tactic: haveI := Classical.decEq ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
Goal:
R : Type uR
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Finite ι
b : Basis ι R M
f : ι →₀ R
i : ι
this : DecidableEq ι
⊢ Eq.{uR + 1} (α := R)
    ((((Finsupp.linearCombination R b.coord : (a : ι →₀ R) → M →ₗ[R] R) f : M →ₗ[R] R) : (a : M) → R)
        ((b : (a : ι) → M) i : M) :
      R)
    ((f : (a : ι) → R) i : R)
have rw : Eq.{uR + 1} (α := R)
  ((((Finsupp.linearCombination R (⇑b.dualBasis : (a : ι) → Dual R M) : (a : ι →₀ R) → M →ₗ[R] R) f : M →ₗ[R] R) :
        (a : M) → R)
      ((b : (a : ι) → M) i : M) :
    R)
  ((f : (a : ι) → R) i : R)
Tactic: rw [← coe_dualBasis, linearCombination_dualBasis]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
Goal:
R : Type uR
M : Type uM
ι : Type uι
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Finite ι
b : Basis ι R M
f : ι →₀ R
i : ι
this : DecidableEq ι
rw :
  Eq.{uR + 1} (α := R)
    ((((Finsupp.linearCombination R (⇑b.dualBasis : (a : ι) → Dual R M) : (a : ι →₀ R) → M →ₗ[R] R) f : M →ₗ[R] R) :
          (a : M) → R)
        ((b : (a : ι) → M) i : M) :
      R)
    ((f : (a : ι) → R) i : R)
⊢ Eq.{uR + 1} (α := R)
    ((((Finsupp.linearCombination R b.coord : (a : ι →₀ R) → M →ₗ[R] R) f : M →ₗ[R] R) : (a : M) → R)
        ((b : (a : ι) → M) i : M) :
      R)
    ((f : (a : ι) → R) i : R)
have rw₁ : Eq.{uR + 1} (α := R) ((f : (a : ι) → R) i : R) ((f : (a : ι) → R) i : R)
Tactic: rw [← coe_dualBasis, linearCombination_dualBasis]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
m : M
i : ι
⊢ i ∈ ⋯.toFinset (s := {i : ι | Ne.{u_1 + 1} (α := R) ((ε i : (a : M) → R) m : R) (0 : R)}) ↔
    Ne.{u_1 + 1} (α := R) ((ε i : (a : M) → R) m : R) (0 : R)
have rw : Membership.mem (γ := Set ι) {i : ι | Ne.{u_1 + 1} (α := R) ((ε i : (a : M) → R) m : R) (0 : R)} i ↔
  Ne.{u_1 + 1} (α := R) ((ε i : (a : M) → R) m : R) (0 : R)
Tactic: rw [Set.Finite.mem_toFinset, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
m : M
i : ι
rw :
  Membership.mem (γ := Set ι) {i : ι | Ne.{u_1 + 1} (α := R) ((ε i : (a : M) → R) m : R) (0 : R)} i ↔
    Ne.{u_1 + 1} (α := R) ((ε i : (a : M) → R) m : R) (0 : R)
⊢ i ∈ ⋯.toFinset (s := {i : ι | Ne.{u_1 + 1} (α := R) ((ε i : (a : M) → R) m : R) (0 : R)}) ↔
    Ne.{u_1 + 1} (α := R) ((ε i : (a : M) → R) m : R) (0 : R)
have rw₁ : Ne.{u_1 + 1} (α := R) ((ε i : (a : M) → R) m : R) (0 : R) ↔ Ne.{u_1 + 1} (α := R) ((ε i : (a : M) → R) m : R) (0 : R)
Tactic: rw [Set.Finite.mem_toFinset, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ Eq.{u_1 + 1} (α := R) ((ε i : (a : M) → R) (lc e l) : R) ((l : (a : ι) → R) i : R)
have rw : Eq.{u_1 + 1} (α := R) ((ε i : (a : M) → R) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : ι) → R) i : R) (e i)) : R)
  ((l : (a : ι) → R) i : R)
Tactic: rw [lc, map_finsuppSum, Finsupp.sum_eq_single i (g := fun a b ↦ (ε i) (b • e a))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Basis (goal)
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : ι → M
ε : ι → Dual R M
h : DualBases e ε
l : ι →₀ R
i : ι
rw :
  Eq.{u_1 + 1} (α := R) ((ε i : (a : M) → R) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : ι) → R) i : R) (e i)) : R)
    ((l : (a : ι) → R) i : R)
⊢ Eq.{u_1 + 1} (α := R) ((ε i : (a : M) → R) (lc e l) : R) ((l : (a : ι) → R) i : R)
have h₀ : ∀ (b : ι),
  Ne.{u_1 + 1} (α := R) ((l : (a : ι) → R) b : R) (0 : R) →
    b ≠ i →
      Eq.{u_1 + 1} (α := R)
        ((ε i : (a : M) → R) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : ι) → R) b : R) (e b)) : R) (0 : R)
Tactic: rw [lc, map_finsuppSum, Finsupp.sum_eq_single i (g := fun a b ↦ (ε i) (b • e a))]