awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : M
i : ι
h : 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) ((b : (a : ι) → M) i)
            ⋯ :
          { 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)
have apply : ∀ (x y : M),
  (fun (x : M) (i : ι) ↦
        ((((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))
      (x + y) =
    HAdd.hAdd (α := ι → R)
      ((fun (x : M) (i : ι) ↦
          ((((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))
        x)
      ((fun (x : M) (i : ι) ↦
          ((((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))
        y)
Tactic: apply (b.repr_apply_eq (fun x i => b.reindexRange.repr x ⟨b i, _⟩) _ _ _ x i).symm
-- 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_1 : M
i : ι
h : Nontrivial R
c : R
x : M
⊢ (fun (x : M) (i : ι) ↦
        ((((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) ⋯ :
              { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
          R))
      (c • x) =
    HSMul.hSMul (β := ι → R) c
      ((fun (x : M) (i : ι) ↦
          ((((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) ⋯ :
                { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
            R))
        x)
have h : ∀ (i : ι),
  (fun (x : M) (i : ι) ↦
        ((((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))
      (c • x) i =
    HSMul.hSMul (β := ι → R) c
      ((fun (x : M) (i : ι) ↦
          ((((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))
        x)
      i
Tactic: ext 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
x : M
i_1 : ι
h : Nontrivial R
i : ι
⊢ Eq (α := ι → R)
    ((fun (x : M) (i : ι) ↦
        ((((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) ⋯ :
              { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
          R))
      ((b : (a : ι) → M) i))
    (⇑(single i 1) : (a : ι) → R)
have h : ∀ (j : ι),
  Eq.{u_11 + 1} (α := R)
    ((fun (x : M) (i : ι) ↦
          ((((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 : (a : ι) → M) i) j :
      R)
    ((single i 1 : (a : ι) → R) j : R)
Tactic: ext 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
x : M
i_1 : ι
h : Nontrivial R
i j : ι
⊢ Eq.{u_11 + 1} (α := R)
    ((fun (x : M) (i : ι) ↦
          ((((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) ⋯ :
                { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
            R))
        ((b : (a : ι) → M) i) j :
      R)
    ((single i 1 : (a : ι) → R) j : R)
have h : Eq.{u_11 + 1} (α := R)
  (((single
            (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)
            1 :
          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) j) sorry :
        { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
    R)
  ((single i 1 : (a : ι) → R) j : R)
Tactic: simp only [reindexRange_repr_self]
-- 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 : M
i_1 : ι
h : Nontrivial R
i j : ι
⊢ Eq.{u_11 + 1} (α := R)
    (((single
              (Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x)
                ((b : (a : ι) → M) i) ⋯)
              1 :
            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) j)
            ⋯ :
          { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) :
      R)
    ((single i 1 : (a : ι) → R) j : R)
have h : Injective.{u_10 + 1, u_12 + 1} (β :=
  { x : M // Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) x }) fun (i : ι) ↦
  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
Tactic: apply Finsupp.single_apply_left (f := fun i => (⟨b i, _⟩ : Set.range b))
-- 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
inst_3 : Fintype ι
inst_4 : DecidableEq M
i : ι
h :
  Membership.mem.{u_12, u_12} (α := M) (γ := Finset M)
    (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) ((b : (a : ι) → M) i : M)
⊢ Eq.{u_12 + 1} (α := M)
    ((b.reindexFinsetRange : (a : ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) → M)
        (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x)
            ((b : (a : ι) → M) i) h :
          ↥(Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) :
      M)
    ((b : (a : ι) → M) i : M)
have rw : Eq.{u_12 + 1} (α := M)
  ((↑((Equiv.symm
              ((Equiv.refl M).subtypeEquiv (p :=
                Membership.mem (γ := Set M) (range.{u_12, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M))) (q :=
                Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) sorry) :
            (a : ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) → (↑(range (⇑b : (a : ι) → M)) : Type u_12))
          (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x)
            ((b : (a : ι) → M) i) h)) :
      M) :
    M)
  ((b : (a : ι) → M) i : M)
Tactic: rw [reindexFinsetRange, reindex_apply, reindexRange_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
inst_3 : Fintype ι
inst_4 : DecidableEq M
x : ↥(Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ)
⊢ (b.reindexFinsetRange : (a : ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) → M) x = (↑x : M)
have rcases : ∀ (bi : M)
  (hbi : Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) bi),
  (b.reindexFinsetRange : (a : ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) → M)
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x) bi hbi) =
    (↑(Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x) bi
          hbi) :
      M)
Tactic: rcases x with ⟨bi, hbi⟩
Cleared hypotheses: 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
inst_3 : Fintype ι
inst_4 : DecidableEq M
bi : M
hbi : Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) bi
⊢ (b.reindexFinsetRange : (a : ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) → M)
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x) bi hbi) =
    (↑(Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x) bi
          hbi) :
      M)
have rcases : ∀ (i : ι)
  (hbi :
    Membership.mem.{u_12, u_12} (α := M) (γ := Finset M)
      (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) ((b : (a : ι) → M) i : M)),
  Eq.{u_12 + 1} (α := M)
    ((b.reindexFinsetRange : (a : ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) → M)
        (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x)
            ((b : (a : ι) → M) i) hbi :
          ↥(Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) :
      M)
    ((↑(Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x)
            ((b : (a : ι) → M) i) hbi) :
        M) :
      M)
Tactic: rcases Finset.mem_image.mp hbi with ⟨i, -, rfl⟩
Cleared hypotheses: bi, hbi
-- 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
inst_3 : Fintype ι
inst_4 : DecidableEq M
i : ι
⊢ Eq (α := Finsupp.{u_12, u_11} (↥(Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) R)
    ((repr b.reindexFinsetRange : (a : M) → ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ) →₀ R) ((b : (a : ι) → M) i) :
      Finsupp.{u_12, u_11} (↥(Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) R)
    (single
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x)
          ((b : (a : ι) → M) i) ⋯)
        1 :
      Finsupp.{u_12, u_11} (↥(Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) R)
have h : ∀ (bi : M)
  (hbi : Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) bi),
  Eq.{u_11 + 1} (α := R)
    ((((repr b.reindexFinsetRange : (a : M) → ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ) →₀ R)
              ((b : (a : ι) → M) i) :
            Finsupp.{u_12, u_11} (↥(Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) R) :
          (a : ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) → R)
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x) bi
          hbi) :
      R)
    (((single
              (Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x)
                ((b : (a : ι) → M) i) sorry)
              1 :
            Finsupp.{u_12, u_11} (↥(Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) R) :
          (a : ↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) → R)
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Finset M) (Finset.image.{u_10, u_12} (α := ι) (⇑b : (a : ι) → M) Finset.univ) x) bi
          hbi) :
      R)
Tactic: ext ⟨bi, hbi⟩
-- 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
inst_8 : Module R M'
S : Type u_13
inst_9 : Semiring S
inst_10 : Module S M'
inst_11 : SMulCommClass R S M'
f g : ι → M'
⊢ linearCombination R id ∘ₗ lmapDomain R R (f + g) ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) =
    HAdd.hAdd (α := M →ₗ[R] M') (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R))
      (linearCombination R id ∘ₗ lmapDomain R R g ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R))
have refine : ∀ (i : ι),
  Eq.{u_7 + 1} (α := M')
    ((linearCombination R id ∘ₗ lmapDomain R R (f + g) ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → M')
        ((b : (a : ι) → M) i : M) :
      M')
    ((HAdd.hAdd (α := M →ₗ[R] M') (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R))
            (linearCombination R id ∘ₗ lmapDomain R R g ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R)) :
          (a : M) → M')
        ((b : (a : ι) → M) i : M) :
      M')
Tactic: refine b.ext fun i => ?_
-- 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
inst_8 : Module R M'
S : Type u_13
inst_9 : Semiring S
inst_10 : Module S M'
inst_11 : SMulCommClass R S M'
c : S
f : ι → M'
⊢ linearCombination R id ∘ₗ lmapDomain R R (c • f) ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) =
    HSMul.hSMul (α := S) (β := M →ₗ[R] M') ((RingHom.id S : (a : S) → S) c : S)
      (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R))
have refine : ∀ (i : ι),
  Eq.{u_7 + 1} (α := M')
    ((linearCombination R id ∘ₗ lmapDomain R R (c • f) ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → M')
        ((b : (a : ι) → M) i : M) :
      M')
    ((HSMul.hSMul (α := S) (β := M →ₗ[R] M') ((RingHom.id S : (a : S) → S) c : S)
            (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R)) :
          (a : M) → M')
        ((b : (a : ι) → M) i : M) :
      M')
Tactic: refine b.ext fun i => ?_
-- 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
inst_8 : Module R M'
S : Type u_13
inst_9 : Semiring S
inst_10 : Module S M'
inst_11 : SMulCommClass R S M'
f : ι → M'
⊢ (fun (f : M →ₗ[R] M') (i : ι) ↦ ((f : (a : M) → M') ((b : (a : ι) → M) i : M) : M'))
      ((fun (f : ι → M') ↦ (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : M →ₗ[R] M')) f) =
    f
have h : ∀ (x : ι),
  (fun (f : M →ₗ[R] M') (i : ι) ↦ ((f : (a : M) → M') ((b : (a : ι) → M) i : M) : M'))
      ((fun (f : ι → M') ↦ (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : M →ₗ[R] M')) f)
      x =
    f x
Tactic: ext
-- 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
inst_8 : Module R M'
S : Type u_13
inst_9 : Semiring S
inst_10 : Module S M'
inst_11 : SMulCommClass R S M'
f : M →ₗ[R] M'
⊢ (fun (f : ι → M') ↦ (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : M →ₗ[R] M'))
      ((fun (f : M →ₗ[R] M') (i : ι) ↦ ((f : (a : M) → M') ((b : (a : ι) → M) i : M) : M')) f) =
    f
have refine : ∀ (i : ι),
  Eq.{u_7 + 1} (α := M')
    (((fun (f : ι → M') ↦ (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : M →ₗ[R] M'))
            ((fun (f : M →ₗ[R] M') (i : ι) ↦ ((f : (a : M) → M') ((b : (a : ι) → M) i : M) : M')) f) :
          (a : M) → M')
        ((b : (a : ι) → M) i : M) :
      M')
    ((f : (a : M) → M') ((b : (a : ι) → M) i : M) : M')
Tactic: refine b.ext fun i => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
b : Basis ι R M
inst_4 : Module R M'
S : Type u_13
inst_5 : Semiring S
inst_6 : Module S M'
inst_7 : SMulCommClass R S M'
f : ι → M'
x : M
⊢ Eq.{u_7 + 1} (α := M') ((((b.constr S : (a : ι → M') → M →ₗ[R] M') f : M →ₗ[R] M') : (a : M) → M') x : M')
    (sum ((b.repr : (a : M) → ι →₀ R) x) fun (b : ι) (a : R) ↦ a • f b : M')
have simp : Eq (α := M') (sum (mapDomain f (((↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ R) x)) fun (i : M') (a : R) ↦ a • id i)
  (sum ((b.repr : (a : M) → ι →₀ R) x) fun (b : ι) (a : R) ↦ a • f b)
Tactic: simp only [constr_def, LinearMap.comp_apply, lmapDomain_apply, linearCombination_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
b : Basis ι R M
inst_4 : Module R M'
S : Type u_13
inst_5 : Semiring S
inst_6 : Module S M'
inst_7 : SMulCommClass R S M'
f : ι → M'
x : M
⊢ Eq (α := M') (sum (mapDomain f (((↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ R) x)) fun (i : M') (a : R) ↦ a • id i)
    (sum ((b.repr : (a : M) → ι →₀ R) x) fun (b : ι) (a : R) ↦ a • f b)
have rw : Eq.{u_7 + 1} (α := M') (sum (((↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ R) x) fun (a : ι) (m : R) ↦ m • id (f a))
  (sum ((b.repr : (a : M) → ι →₀ R) x) fun (b : ι) (a : R) ↦ a • f b)
Tactic: rw [Finsupp.sum_mapDomain_index]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Defs (goal)
Goal:
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
b : Basis ι R M
inst_4 : Module R M'
S : Type u_13
inst_5 : Semiring S
inst_6 : Module S M'
inst_7 : SMulCommClass R S M'
f : ι → M'
x : M
rw :
  Eq.{u_7 + 1} (α := M') (sum (((↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ R) x) fun (a : ι) (m : R) ↦ m • id (f a))
    (sum ((b.repr : (a : M) → ι →₀ R) x) fun (b : ι) (a : R) ↦ a • f b)
⊢ Eq (α := M') (sum (mapDomain f (((↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ R) x)) fun (i : M') (a : R) ↦ a • id i)
    (sum ((b.repr : (a : M) → ι →₀ R) x) fun (b : ι) (a : R) ↦ a • f b)
have h_zero : ∀ (b : M'), HSMul.hSMul.{u_11, u_7, u_7} (α := R) 0 (id b) = 0
Tactic: rw [Finsupp.sum_mapDomain_index]