awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent.{u_5, u_3, u_5} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M) ≤ w
x : M
p : x ∈ w
q : x ∉ range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)
u : Embedding.{u_1 + 1, u_5 + 1} ι (↑w : Type u_5) :=
  { toFun := fun (i : ι) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ w) ((b : (a : ι) → M) i) ⋯, inj' := ⋯ }
e :
  (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w)) : (a : (↑w : Type u_5) →₀ R) → M)
      (embDomain u ((b.repr : (a : M) → ι →₀ R) x)) =
    (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ w) x p) : M)
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ w) x p ∉
    Finsupp.support.{u_5, u_3} (M := R) (embDomain u ((b.repr : (a : M) → ι →₀ R) x))
have simp : ¬∃ (a : ι),
    Membership.mem (γ := Finset ι) (Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : M) → ι →₀ R) x)) a ∧
      (u : (a : ι) → { x : M // x ∈ w }) a = Subtype.mk (p := fun (x : M) ↦ x ∈ w) x p
Tactic: simp only [Finset.mem_map, Finsupp.support_embDomain]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (hypothesis)
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
b : Basis ι R M
w : Set M
hi : LinearIndependent.{u_5, u_3, u_5} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M) ≤ w
x : M
p : x ∈ w
q : x ∉ range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)
u : Embedding.{u_1 + 1, u_5 + 1} ι (↑w : Type u_5) :=
  { toFun := fun (i : ι) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ w) ((b : (a : ι) → M) i) ⋯, inj' := ⋯ }
e :
  (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ w)) : (a : (↑w : Type u_5) →₀ R) → M)
      (embDomain u ((b.repr : (a : M) → ι →₀ R) x)) =
    (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ w) x p) : M)
j : ι
W : (u : (a : ι) → { x : M // x ∈ w }) j = Subtype.mk (p := fun (x : M) ↦ x ∈ w) x p
⊢ False
have W₁ : (b : (a : ι) → M) j = x
Tactic: simp only [u, Embedding.coeFn_mk, Subtype.mk_eq_mk] at W
Cleared hypotheses: W
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b_1 : Basis ι R M
v : ι → M
x y : M
inst_5 : Subsingleton R
x_1 : Basis ι R M
b : M ≃ₗ[R] ι →₀ R
⊢ { repr := b : Basis ι R M } = default
have rw : Eq (α := Basis ι R M) { repr := repr default } default
Tactic: rw [Subsingleton.elim b]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_7
R : Type u_8
inst : Unique ι
inst_1 : Semiring R
⊢ Eq (α := (a : ι) → R) (⇑(Basis.singleton ι R) : (a : ι) → R) 1
have h : ∀ (x : ι), Eq.{u_8 + 1} (α := R) ((Basis.singleton ι R : (a : ι) → R) x : R) (1 x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (hypothesis)
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsDomain R
b : Basis ι R M
c : R
x : M
⊢ c • x = 0 ↔ c = 0 ∨ x = 0
have this : IsTorsionFree R M
Tactic: have := b.isTorsionFree
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
⊢ Nonempty (Basis ι R M) ↔ ∃ (x : M), x ≠ 0 ∧ ∀ (y : M), ∃ (r : R), r • x = y
have mp : Nonempty (Basis ι R M) → ∃ (x : M), x ≠ 0 ∧ ∀ (y : M), ∃ (r : R), r • x = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
mp : Nonempty (Basis ι R M) → ∃ (x : M), x ≠ 0 ∧ ∀ (y : M), ∃ (r : R), r • x = y
⊢ Nonempty (Basis ι R M) ↔ ∃ (x : M), x ≠ 0 ∧ ∀ (y : M), ∃ (r : R), r • x = y
have mpr : (∃ (x : M), x ≠ 0 ∧ ∀ (y : M), ∃ (r : R), r • x = y) → Nonempty (Basis ι R M)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
b : Basis ι R M
⊢ ∃ (x : M), x ≠ 0 ∧ ∀ (y : M), ∃ (r : R), r • x = y
have mp : ∀ (y : M), ∃ (r : R), HSMul.hSMul (β := M) r ((b : (a : ι) → M) default : M) = y
Tactic: refine ⟨b default, b.linearIndependent.ne_zero _, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ (r : R), r • x = y
⊢ Nonempty (Basis ι R M)
have mpr : ∀ (y z : ι →₀ R),
  HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((y + z : (a : ι) → R) default : R) x =
    HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((y : (a : ι) → R) default : R) x +
      HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((z : (a : ι) → R) default : R) x
Tactic: refine ⟨ofRepr <| LinearEquiv.symm
      { toFun := fun f => f default • x
        invFun := fun y => Finsupp.single default (w y).choose
        left_inv := fun f => Finsupp.unique_ext ?_
        right_inv := fun y => ?_
        map_add' := fun y z => ?_
        map_smul' := fun c y => ?_ }⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ (r : R), r • x = y
mpr :
  ∀ (y z : ι →₀ R),
    HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((y + z : (a : ι) → R) default : R) x =
      HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((y : (a : ι) → R) default : R) x +
        HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((z : (a : ι) → R) default : R) x
⊢ Nonempty (Basis ι R M)
have mpr₁ : ∀ (c : R) (y : ι →₀ R),
  HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((c • y : (a : ι) → R) default : R) x =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R)
      (HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((y : (a : ι) → R) default : R) x)
Tactic: refine ⟨ofRepr <| LinearEquiv.symm
      { toFun := fun f => f default • x
        invFun := fun y => Finsupp.single default (w y).choose
        left_inv := fun f => Finsupp.unique_ext ?_
        right_inv := fun y => ?_
        map_add' := fun y z => ?_
        map_smul' := fun c y => ?_ }⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ (r : R), r • x = y
mpr :
  ∀ (y z : ι →₀ R),
    HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((y + z : (a : ι) → R) default : R) x =
      HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((y : (a : ι) → R) default : R) x +
        HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((z : (a : ι) → R) default : R) x
mpr₁ :
  ∀ (c : R) (y : ι →₀ R),
    HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((c • y : (a : ι) → R) default : R) x =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R)
        (HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((y : (a : ι) → R) default : R) x)
⊢ Nonempty (Basis ι R M)
have mpr₂ : ∀ (f : ι →₀ R),
  Eq.{u_7 + 1} (α := R)
    (((fun (y : M) ↦ (single default (sorry.choose (p := fun (r : R) ↦ r • x = y)) : ι →₀ R))
            ((fun (f : ι →₀ R) ↦ HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((f : (a : ι) → R) default : R) x) f) :
          (a : ι) → R)
        default :
      R)
    ((f : (a : ι) → R) default : R)
Tactic: refine ⟨ofRepr <| LinearEquiv.symm
      { toFun := fun f => f default • x
        invFun := fun y => Finsupp.single default (w y).choose
        left_inv := fun f => Finsupp.unique_ext ?_
        right_inv := fun y => ?_
        map_add' := fun y z => ?_
        map_smul' := fun c y => ?_ }⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ (r : R), r • x = y
mpr :
  ∀ (y z : ι →₀ R),
    HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((y + z : (a : ι) → R) default : R) x =
      HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((y : (a : ι) → R) default : R) x +
        HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((z : (a : ι) → R) default : R) x
mpr₁ :
  ∀ (c : R) (y : ι →₀ R),
    HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((c • y : (a : ι) → R) default : R) x =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R)
        (HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((y : (a : ι) → R) default : R) x)
mpr₂ :
  ∀ (f : ι →₀ R),
    Eq.{u_7 + 1} (α := R)
      (((fun (y : M) ↦ (single default (⋯.choose (p := fun (r : R) ↦ r • x = y)) : ι →₀ R))
              ((fun (f : ι →₀ R) ↦ HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((f : (a : ι) → R) default : R) x) f) :
            (a : ι) → R)
          default :
        R)
      ((f : (a : ι) → R) default : R)
⊢ Nonempty (Basis ι R M)
have mpr₃ : ∀ (y : M),
  (fun (f : ι →₀ R) ↦ HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((f : (a : ι) → R) default : R) x)
      ((fun (y : M) ↦ (single default (sorry.choose (p := fun (r : R) ↦ r • x = y)) : ι →₀ R)) y) =
    y
Tactic: refine ⟨ofRepr <| LinearEquiv.symm
      { toFun := fun f => f default • x
        invFun := fun y => Finsupp.single default (w y).choose
        left_inv := fun f => Finsupp.unique_ext ?_
        right_inv := fun y => ?_
        map_add' := fun y z => ?_
        map_smul' := fun c y => ?_ }⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ (r : R), r • x = y
c : R
y : ι →₀ R
⊢ HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((c • y : (a : ι) → R) default : R) x =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R)
      (HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((y : (a : ι) → R) default : R) x)
have mpr : HSMul.hSMul (β := R) c ((y : (a : ι) → R) default : R) • x =
  c • HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((y : (a : ι) → R) default : R) x
Tactic: simp only [Finsupp.coe_smul, Pi.smul_apply, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ (r : R), r • x = y
c : R
y : ι →₀ R
⊢ HSMul.hSMul (β := R) c ((y : (a : ι) → R) default : R) • x =
    c • HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((y : (a : ι) → R) default : R) x
have mpr : HSMul.hSMul (β := R) c ((y : (a : ι) → R) default : R) • x = HSMul.hSMul (β := R) c ((y : (a : ι) → R) default : R) • x
Tactic: rw [← smul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ (r : R), r • x = y
f : ι →₀ R
⊢ Eq.{u_7 + 1} (α := R)
    (((fun (y : M) ↦ (single default (⋯.choose (p := fun (r : R) ↦ r • x = y)) : ι →₀ R))
            ((fun (f : ι →₀ R) ↦ HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((f : (a : ι) → R) default : R) x) f) :
          (a : ι) → R)
        default :
      R)
    ((f : (a : ι) → R) default : R)
have mpr : Eq.{u_8 + 1} (α := M)
  ((fun (x_1 : R) ↦ x_1 • x)
    (((fun (y : M) ↦ (single default (sorry.choose (p := fun (r : R) ↦ r • x = y)) : ι →₀ R))
          ((fun (f : ι →₀ R) ↦ HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((f : (a : ι) → R) default : R) x) f) :
        (a : ι) → R)
      default))
  ((fun (x_1 : R) ↦ x_1 • x) ((f : (a : ι) → R) default))
Tactic: refine smul_left_injective _ nz ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ (r : R), r • x = y
f : ι →₀ R
⊢ Eq.{u_8 + 1} (α := M)
    ((fun (x_1 : R) ↦ x_1 • x)
      (((fun (y : M) ↦ (single default (⋯.choose (p := fun (r : R) ↦ r • x = y)) : ι →₀ R))
            ((fun (f : ι →₀ R) ↦ HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((f : (a : ι) → R) default : R) x) f) :
          (a : ι) → R)
        default))
    ((fun (x_1 : R) ↦ x_1 • x) ((f : (a : ι) → R) default))
have mpr : Exists.choose (p := fun (r : R) ↦ r • x = HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((f : (a : ι) → R) default : R) x) sorry •
    x =
  HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((f : (a : ι) → R) default : R) x
Tactic: simp only [Finsupp.single_eq_same]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
R : Type u_7
M : Type u_8
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTorsionFree R M
ι : Type u_9
inst_5 : Unique ι
x : M
nz : x ≠ 0
w : ∀ (y : M), ∃ (r : R), r • x = y
y : M
⊢ (fun (f : ι →₀ R) ↦ HSMul.hSMul.{u_7, u_8, u_8} (α := R) ((f : (a : ι) → R) default : R) x)
      ((fun (y : M) ↦ (single default (⋯.choose (p := fun (r : R) ↦ r • x = y)) : ι →₀ R)) y) =
    y
have mpr : sorry.choose (p := fun (r : R) ↦ r • x = y) • x = y
Tactic: simp only [Finsupp.single_eq_same]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι
b : Basis ι R M
inst_4 : Fintype R
inst_5 : Fintype M
⊢ card M = card R ^ card ι
have card : card (ι → R) = card R ^ card ι
Tactic: calc
      card M = card (ι → R) := card_congr b.equivFun.toEquiv
      _ = card R ^ card ι := by simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Basic (goal)
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Fintype ι
b : Basis ι R M
inst_4 : Fintype R
inst_5 : Fintype M
⊢ card M = card R ^ card ι
have card : card (ι → R) = card R ^ card ι
Tactic: classical
    calc
      card M = card (ι → R) := card_congr b.equivFun.toEquiv
      _ = card R ^ card ι := by simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Bilinear (goal)
Goal:
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring R₂
inst_3 : Semiring S₂
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : AddCommMonoid P
inst_7 : Module R M
inst_8 : Module S N
inst_9 : Module R₂ P
inst_10 : Module S₂ P
inst_11 : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
x : M
y : N
| ((((B : (a : M) → N →ₛₗ[σ₁₂] P) x : N →ₛₗ[σ₁₂] P) : (a : N) → P) y : P)
have rw : ((((B : (a : M) → N →ₛₗ[σ₁₂] P)
          ((Finsupp.linearCombination R (⇑b₁ : (a : ι₁) → M) : (a : ι₁ →₀ R) → M)
            ((b₁.repr : (a : M) → ι₁ →₀ R) x : ι₁ →₀ R)) :
        N →ₛₗ[σ₁₂] P) :
      (a : N) → P)
    ((Finsupp.linearCombination S (⇑b₂ : (a : ι₂) → N) : (a : ι₂ →₀ S) → N)
        ((b₂.repr : (a : N) → ι₂ →₀ S) y : ι₂ →₀ S) :
      N) :
  P)
Tactic: rw [← b₁.linearCombination_repr x, ← b₂.linearCombination_repr y]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Bilinear (goal)
Goal:
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring R₂
inst_3 : Semiring S₂
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : AddCommMonoid P
inst_7 : Module R M
inst_8 : Module S N
inst_9 : Module R₂ P
inst_10 : Module S₂ P
inst_11 : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
x : M
y : N
⊢ Eq.{u_9 + 1} (α := P)
    (Finsupp.sum ((b₁.repr : (a : M) → ι₁ →₀ R) x) fun (i : ι₁) (xi : R) ↦
        Finsupp.sum ((b₂.repr : (a : N) → ι₂ →₀ S) y) fun (j : ι₂) (yj : S) ↦
          HSMul.hSMul.{u_4, u_9, u_9} (α := R₂) ((ρ₁₂ : (a : R) → R₂) xi : R₂)
            (HSMul.hSMul.{u_6, u_9, u_9} (α := S₂) (β := P) ((σ₁₂ : (a : S) → S₂) yj : S₂)
              ((((B : (a : M) → N →ₛₗ[σ₁₂] P) ((b₁ : (a : ι₁) → M) i) : N →ₛₗ[σ₁₂] P) : (a : N) → P)
                  ((b₂ : (a : ι₂) → N) j : N) :
                P)) :
      P)
    ((((B : (a : M) → N →ₛₗ[σ₁₂] P) x : N →ₛₗ[σ₁₂] P) : (a : N) → P) y : P)
have conv_rhs : Eq.{u_9 + 1} (α := P)
  (Finsupp.sum ((b₁.repr : (a : M) → ι₁ →₀ R) x) fun (i : ι₁) (xi : R) ↦
      Finsupp.sum ((b₂.repr : (a : N) → ι₂ →₀ S) y) fun (j : ι₂) (yj : S) ↦
        HSMul.hSMul.{u_4, u_9, u_9} (α := R₂) ((ρ₁₂ : (a : R) → R₂) xi : R₂)
          (HSMul.hSMul.{u_6, u_9, u_9} (α := S₂) (β := P) ((σ₁₂ : (a : S) → S₂) yj : S₂)
            ((((B : (a : M) → N →ₛₗ[σ₁₂] P) ((b₁ : (a : ι₁) → M) i) : N →ₛₗ[σ₁₂] P) : (a : N) → P)
                ((b₂ : (a : ι₂) → N) j : N) :
              P)) :
    P)
  ((((B : (a : M) → N →ₛₗ[σ₁₂] P)
            ((Finsupp.linearCombination R (⇑b₁ : (a : ι₁) → M) : (a : ι₁ →₀ R) → M)
              ((b₁.repr : (a : M) → ι₁ →₀ R) x : ι₁ →₀ R)) :
          N →ₛₗ[σ₁₂] P) :
        (a : N) → P)
      ((Finsupp.linearCombination S (⇑b₂ : (a : ι₂) → N) : (a : ι₂ →₀ S) → N)
          ((b₂.repr : (a : N) → ι₂ →₀ S) y : ι₂ →₀ S) :
        N) :
    P)
Tactic: conv_rhs => rw [← b₁.linearCombination_repr x, ← b₂.linearCombination_repr y]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Bilinear (goal)
Goal:
ι₁ : Type u_1
ι₂ : Type u_2
R : Type u_3
R₂ : Type u_4
S : Type u_5
S₂ : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring R₂
inst_3 : Semiring S₂
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : AddCommMonoid P
inst_7 : Module R M
inst_8 : Module S N
inst_9 : Module R₂ P
inst_10 : Module S₂ P
inst_11 : SMulCommClass S₂ R₂ P
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
b₁ : Basis ι₁ R M
b₂ : Basis ι₂ S N
B : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
x : M
y : N
⊢ Eq.{u_9 + 1} (α := P)
    (Finsupp.sum ((b₁.repr : (a : M) → ι₁ →₀ R) x) fun (i : ι₁) (xi : R) ↦
        Finsupp.sum ((b₂.repr : (a : N) → ι₂ →₀ S) y) fun (j : ι₂) (yj : S) ↦
          HSMul.hSMul.{u_4, u_9, u_9} (α := R₂) ((ρ₁₂ : (a : R) → R₂) xi : R₂)
            (HSMul.hSMul.{u_6, u_9, u_9} (α := S₂) (β := P) ((σ₁₂ : (a : S) → S₂) yj : S₂)
              ((((B : (a : M) → N →ₛₗ[σ₁₂] P) ((b₁ : (a : ι₁) → M) i) : N →ₛₗ[σ₁₂] P) : (a : N) → P)
                  ((b₂ : (a : ι₂) → N) j : N) :
                P)) :
      P)
    ((((B : (a : M) → N →ₛₗ[σ₁₂] P)
              ((Finsupp.linearCombination R (⇑b₁ : (a : ι₁) → M) : (a : ι₁ →₀ R) → M)
                ((b₁.repr : (a : M) → ι₁ →₀ R) x : ι₁ →₀ R)) :
            N →ₛₗ[σ₁₂] P) :
          (a : N) → P)
        ((Finsupp.linearCombination S (⇑b₂ : (a : ι₂) → N) : (a : ι₂ →₀ S) → N)
            ((b₂.repr : (a : N) → ι₂ →₀ S) y : ι₂ →₀ S) :
          N) :
      P)
have simp_rw : Eq.{u_9 + 1} (α := P)
  (Finsupp.sum ((b₁.repr : (a : M) → ι₁ →₀ R) x) fun (i : ι₁) (xi : R) ↦
      Finsupp.sum ((b₂.repr : (a : N) → ι₂ →₀ S) y) fun (j : ι₂) (yj : S) ↦
        HSMul.hSMul.{u_4, u_9, u_9} (α := R₂) ((ρ₁₂ : (a : R) → R₂) xi : R₂)
          (HSMul.hSMul.{u_6, u_9, u_9} (α := S₂) (β := P) ((σ₁₂ : (a : S) → S₂) yj : S₂)
            ((((B : (a : M) → N →ₛₗ[σ₁₂] P) ((b₁ : (a : ι₁) → M) i) : N →ₛₗ[σ₁₂] P) : (a : N) → P)
                ((b₂ : (a : ι₂) → N) j : N) :
              P)) :
    P)
  (((B : (a : M) → N →ₛₗ[σ₁₂] P)
          (Finsupp.sum ((b₁.repr : (a : M) → ι₁ →₀ R) x) fun (i : ι₁) (a : R) ↦
            HSMul.hSMul (β := M) a ((b₁ : (a : ι₁) → M) i : M)) :
        (a : N) → P)
      (Finsupp.sum ((b₂.repr : (a : N) → ι₂ →₀ S) y) fun (i : ι₂) (a : S) ↦
        HSMul.hSMul (β := N) a ((b₂ : (a : ι₂) → N) i : N)) :
    P)
Tactic: simp_rw [Finsupp.linearCombination_apply, Finsupp.sum, map_sum₂, map_sum, map_smulₛₗ₂, map_smulₛₗ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Bilinear (goal)
Goal:
ι₁ : Type u_1
ι₂ : Type u_2
Rₗ : Type u_10
Mₗ : Type u_11
Nₗ : Type u_12
Pₗ : Type u_13
inst : CommSemiring Rₗ
inst_1 : AddCommMonoid Mₗ
inst_2 : AddCommMonoid Nₗ
inst_3 : AddCommMonoid Pₗ
inst_4 : Module Rₗ Mₗ
inst_5 : Module Rₗ Nₗ
inst_6 : Module Rₗ Pₗ
b₁' : Basis ι₁ Rₗ Mₗ
b₂' : Basis ι₂ Rₗ Nₗ
B : Mₗ →ₗ[Rₗ] Nₗ →ₗ[Rₗ] Pₗ
x : Mₗ
y : Nₗ
| ((((B : (a : Mₗ) → Nₗ →ₗ[Rₗ] Pₗ) x : Nₗ →ₗ[Rₗ] Pₗ) : (a : Nₗ) → Pₗ) y : Pₗ)
have rw : ((((B : (a : Mₗ) → Nₗ →ₗ[Rₗ] Pₗ)
          ((Finsupp.linearCombination Rₗ (⇑b₁' : (a : ι₁) → Mₗ) : (a : ι₁ →₀ Rₗ) → Mₗ)
            ((b₁'.repr : (a : Mₗ) → ι₁ →₀ Rₗ) x : ι₁ →₀ Rₗ)) :
        Nₗ →ₗ[Rₗ] Pₗ) :
      (a : Nₗ) → Pₗ)
    ((Finsupp.linearCombination Rₗ (⇑b₂' : (a : ι₂) → Nₗ) : (a : ι₂ →₀ Rₗ) → Nₗ)
        ((b₂'.repr : (a : Nₗ) → ι₂ →₀ Rₗ) y : ι₂ →₀ Rₗ) :
      Nₗ) :
  Pₗ)
Tactic: rw [← b₁'.linearCombination_repr x, ← b₂'.linearCombination_repr y]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Bilinear (goal)
Goal:
ι₁ : Type u_1
ι₂ : Type u_2
Rₗ : Type u_10
Mₗ : Type u_11
Nₗ : Type u_12
Pₗ : Type u_13
inst : CommSemiring Rₗ
inst_1 : AddCommMonoid Mₗ
inst_2 : AddCommMonoid Nₗ
inst_3 : AddCommMonoid Pₗ
inst_4 : Module Rₗ Mₗ
inst_5 : Module Rₗ Nₗ
inst_6 : Module Rₗ Pₗ
b₁' : Basis ι₁ Rₗ Mₗ
b₂' : Basis ι₂ Rₗ Nₗ
B : Mₗ →ₗ[Rₗ] Nₗ →ₗ[Rₗ] Pₗ
x : Mₗ
y : Nₗ
⊢ Eq.{u_13 + 1} (α := Pₗ)
    (Finsupp.sum ((b₁'.repr : (a : Mₗ) → ι₁ →₀ Rₗ) x) fun (i : ι₁) (xi : Rₗ) ↦
        Finsupp.sum ((b₂'.repr : (a : Nₗ) → ι₂ →₀ Rₗ) y) fun (j : ι₂) (yj : Rₗ) ↦
          xi •
            HSMul.hSMul (β := Pₗ) yj
              ((((B : (a : Mₗ) → Nₗ →ₗ[Rₗ] Pₗ) ((b₁' : (a : ι₁) → Mₗ) i) : Nₗ →ₗ[Rₗ] Pₗ) : (a : Nₗ) → Pₗ)
                  ((b₂' : (a : ι₂) → Nₗ) j : Nₗ) :
                Pₗ) :
      Pₗ)
    ((((B : (a : Mₗ) → Nₗ →ₗ[Rₗ] Pₗ) x : Nₗ →ₗ[Rₗ] Pₗ) : (a : Nₗ) → Pₗ) y : Pₗ)
have conv_rhs : Eq.{u_13 + 1} (α := Pₗ)
  (Finsupp.sum ((b₁'.repr : (a : Mₗ) → ι₁ →₀ Rₗ) x) fun (i : ι₁) (xi : Rₗ) ↦
      Finsupp.sum ((b₂'.repr : (a : Nₗ) → ι₂ →₀ Rₗ) y) fun (j : ι₂) (yj : Rₗ) ↦
        xi •
          HSMul.hSMul (β := Pₗ) yj
            ((((B : (a : Mₗ) → Nₗ →ₗ[Rₗ] Pₗ) ((b₁' : (a : ι₁) → Mₗ) i) : Nₗ →ₗ[Rₗ] Pₗ) : (a : Nₗ) → Pₗ)
                ((b₂' : (a : ι₂) → Nₗ) j : Nₗ) :
              Pₗ) :
    Pₗ)
  ((((B : (a : Mₗ) → Nₗ →ₗ[Rₗ] Pₗ)
            ((Finsupp.linearCombination Rₗ (⇑b₁' : (a : ι₁) → Mₗ) : (a : ι₁ →₀ Rₗ) → Mₗ)
              ((b₁'.repr : (a : Mₗ) → ι₁ →₀ Rₗ) x : ι₁ →₀ Rₗ)) :
          Nₗ →ₗ[Rₗ] Pₗ) :
        (a : Nₗ) → Pₗ)
      ((Finsupp.linearCombination Rₗ (⇑b₂' : (a : ι₂) → Nₗ) : (a : ι₂ →₀ Rₗ) → Nₗ)
          ((b₂'.repr : (a : Nₗ) → ι₂ →₀ Rₗ) y : ι₂ →₀ Rₗ) :
        Nₗ) :
    Pₗ)
Tactic: conv_rhs => rw [← b₁'.linearCombination_repr x, ← b₂'.linearCombination_repr y]