awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ Eq.{u_1 + 1} (α := R) ((ε i : (a : M) → R) (lc e l) : R) ((l : (a : ι) → R) i : R)
have h₁ : Eq.{u_1 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R) →
  Eq.{u_1 + 1} (α := R) ((ε i : (a : M) → R) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (e i)) : R) (0 : 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
⊢ h.coeffs (lc e l) = l
have h₁ : ∀ (i : ι), Eq.{u_1 + 1} (α := R) ((h.coeffs (lc e l) : (a : ι) → R) i : R) ((l : (a : ι) → R) i : R)
Tactic: ext i
-- 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) ((h.coeffs (lc e l) : (a : ι) → R) i : R) ((l : (a : ι) → R) i : R)
have h₁ : Eq.{u_1 + 1} (α := R) ((ε i : (a : M) → R) (lc e l) : R) ((l : (a : ι) → R) i : R)
Tactic: rw [h.coeffs_apply, h.dual_lc]
-- 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 : ι
h₁ : Eq.{u_1 + 1} (α := R) ((ε i : (a : M) → R) (lc e l) : R) ((l : (a : ι) → R) i : R)
⊢ Eq.{u_1 + 1} (α := R) ((h.coeffs (lc e l) : (a : ι) → R) i : R) ((l : (a : ι) → R) i : R)
have h₂ : Eq.{u_1 + 1} (α := R) ((l : (a : ι) → R) i : R) ((l : (a : ι) → R) i : R)
Tactic: rw [h.coeffs_apply, h.dual_lc]
-- 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 ε
v w : M
⊢ h.coeffs (v + w) = h.coeffs v + h.coeffs w
have h₁ : ∀ (i : ι),
  Eq.{u_1 + 1} (α := R) ((h.coeffs (v + w) : (a : ι) → R) i : R) ((h.coeffs v + h.coeffs w : (a : ι) → R) i : R)
Tactic: ext i
-- 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 ε
c : R
v : M
⊢ h.coeffs (c • v) = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (h.coeffs v)
have h₁ : ∀ (i : ι),
  Eq.{u_1 + 1} (α := R) ((h.coeffs (c • v) : (a : ι) → R) i : R)
    ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (h.coeffs v) : (a : ι) → R) i : R)
Tactic: ext i
-- 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 ε
⊢ (⇑h.basis : (a : ι) → M) = e
have h₁ : ∀ (i : ι), (h.basis : (a : ι) → M) i = e i
Tactic: ext i
-- 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 ε
i : ι
⊢ (h.basis : (a : ι) → M) i = e i
have h₁ : Eq (α := ι →₀ R) ((h.basis.repr : (a : M) → ι →₀ R) (e i) : ι →₀ R) (Finsupp.single i 1 : ι →₀ R)
Tactic: rw [Basis.apply_eq_iff]
-- 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 ε
i : ι
⊢ Eq (α := ι →₀ R) ((h.basis.repr : (a : M) → ι →₀ R) (e i) : ι →₀ R) (Finsupp.single i 1 : ι →₀ R)
have h₁ : ∀ (j : ι),
  Eq.{u_1 + 1} (α := R) ((((h.basis.repr : (a : M) → ι →₀ R) (e i) : ι →₀ R) : (a : ι) → R) j : R)
    ((Finsupp.single i 1 : (a : ι) → R) j : R)
Tactic: ext j
-- 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 ε
i j : ι
⊢ Eq.{u_1 + 1} (α := R) ((((h.basis.repr : (a : M) → ι →₀ R) (e i) : ι →₀ R) : (a : ι) → R) j : R)
    ((Finsupp.single i 1 : (a : ι) → R) j : R)
have h₁ : Eq.{u_1 + 1} (α := R) ((((h.basis.repr : (a : M) → ι →₀ R) (e i) : ι →₀ R) : (a : ι) → R) i : R)
  ((Finsupp.single i 1 : (a : ι) → R) i : R)
Tactic: rcases eq_or_ne i j with rfl | hne
Cleared hypotheses: j
-- 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 ε
i j : ι
h₁ :
  Eq.{u_1 + 1} (α := R) ((((h.basis.repr : (a : M) → ι →₀ R) (e i) : ι →₀ R) : (a : ι) → R) i : R)
    ((Finsupp.single i 1 : (a : ι) → R) i : R)
⊢ Eq.{u_1 + 1} (α := R) ((((h.basis.repr : (a : M) → ι →₀ R) (e i) : ι →₀ R) : (a : ι) → R) j : R)
    ((Finsupp.single i 1 : (a : ι) → R) j : R)
have h₂ : ∀ (hne : i ≠ j),
  Eq.{u_1 + 1} (α := R) ((((h.basis.repr : (a : M) → ι →₀ R) (e i) : ι →₀ R) : (a : ι) → R) j : R)
    ((Finsupp.single i 1 : (a : ι) → R) j : R)
Tactic: rcases eq_or_ne i j with rfl | hne
-- 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 ε
H : Set ι
x : M
hmem : Membership.mem (γ := Submodule R M) (span R (e '' H)) x
i : ι
hi : Ne.{u_1 + 1} (α := R) ((ε i : (a : M) → R) x : R) (0 : R)
⊢ i ∈ H
have rcases : ∀ (l : ι →₀ R) (supp_l : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R H) l)
  (hmem :
    Membership.mem (α := M) (γ := Submodule R M) (span R (e '' H))
      ((Finsupp.linearCombination R e : (a : ι →₀ R) → M) l : M))
  (hi :
    Ne.{u_1 + 1} (α := R) ((ε i : (a : M) → R) ((Finsupp.linearCombination R e : (a : ι →₀ R) → M) l : M) : R) (0 : R)),
  i ∈ H
Tactic: rcases (Finsupp.mem_span_image_iff_linearCombination _).mp hmem with ⟨l, supp_l, rfl⟩
Cleared hypotheses: x, hmem, hi
-- 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 ε
H : Set ι
i : ι
l : ι →₀ R
supp_l : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R H) l
hmem :
  Membership.mem (α := M) (γ := Submodule R M) (span R (e '' H))
    ((Finsupp.linearCombination R e : (a : ι →₀ R) → M) l : M)
hi : Ne.{u_1 + 1} (α := R) ((ε i : (a : M) → R) ((Finsupp.linearCombination R e : (a : ι →₀ R) → M) l : M) : R) (0 : R)
⊢ i ∈ H
have apply : ¬Eq.{u_1 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R)
Tactic: apply not_imp_comm.mp ((Finsupp.mem_supported' _ _).mp supp_l i)
-- 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 ε
H : Set ι
i : ι
l : ι →₀ R
supp_l : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R H) l
hmem :
  Membership.mem (α := M) (γ := Submodule R M) (span R (e '' H))
    ((Finsupp.linearCombination R e : (a : ι →₀ R) → M) l : M)
hi : Ne.{u_1 + 1} (α := R) ((ε i : (a : M) → R) ((Finsupp.linearCombination R e : (a : ι →₀ R) → M) l : M) : R) (0 : R)
⊢ ¬Eq.{u_1 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R)
have rwa : ∀ (hi : Ne.{u_1 + 1} (α := R) ((ε i : (a : M) → R) (lc e l) : R) (0 : R)),
  ¬Eq.{u_1 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R)
Tactic: rwa [← lc_def, h.dual_lc] at hi
Cleared hypotheses: hi
-- 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 ε
H : Set ι
i : ι
l : ι →₀ R
supp_l : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R H) l
hmem :
  Membership.mem (α := M) (γ := Submodule R M) (span R (e '' H))
    ((Finsupp.linearCombination R e : (a : ι →₀ R) → M) l : M)
hi : Ne.{u_1 + 1} (α := R) ((ε i : (a : M) → R) ((Finsupp.linearCombination R e : (a : ι →₀ R) → M) l : M) : R) (0 : R)
rwa :
  ∀ (hi : Ne.{u_1 + 1} (α := R) ((ε i : (a : M) → R) (lc e l) : R) (0 : R)),
    ¬Eq.{u_1 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R)
⊢ ¬Eq.{u_1 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R)
have rwa₁ : ∀ (hi : Ne.{u_1 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R)),
  ¬Eq.{u_1 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R)
Tactic: rwa [← lc_def, h.dual_lc] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_1
M₁ : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
⊢ Eq (α := Dual R M₁ →ₗ[R] Dual R M₁) (dualMap id) id
have h : ∀ (x : Dual R M₁) (x_1 : M₁),
  Eq.{u_1 + 1} (α := R) ((((dualMap id : (a : Dual R M₁) → Dual R M₁) x : Dual R M₁) : (a : M₁) → R) x_1 : R)
    ((((id : (a : Dual R M₁) → Dual R M₁) x : Dual R M₁) : (a : M₁) → R) x_1 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
f : M₁ →ₗ[R] M₂
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M₁) (β := M₂) (⇑f : (a : M₁) → M₂)
φ ψ : Dual R M₂
h :
  Eq (α := Dual R M₁) ((f.dualMap : (a : Dual R M₂) → Dual R M₁) φ : Dual R M₁)
    ((f.dualMap : (a : Dual R M₂) → Dual R M₁) ψ : Dual R M₁)
⊢ φ = ψ
have h₁ : ∀ (x : M₂), Eq.{u_1 + 1} (α := R) ((φ : (a : M₂) → R) x : R) ((ψ : (a : M₂) → R) x : R)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R M₂
f : M₁ →ₗ[R] M₂
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M₁) (β := M₂) (⇑f : (a : M₁) → M₂)
φ ψ : Dual R M₂
h :
  Eq (α := Dual R M₁) ((f.dualMap : (a : Dual R M₂) → Dual R M₁) φ : Dual R M₁)
    ((f.dualMap : (a : Dual R M₂) → Dual R M₁) ψ : Dual R M₁)
x : M₂
⊢ Eq.{u_1 + 1} (α := R) ((φ : (a : M₂) → R) x : R) ((ψ : (a : M₂) → R) x : R)
have h₁ : ∀ (y : M₁),
  Eq.{u_1 + 1} (α := R) ((φ : (a : M₂) → R) ((f : (a : M₁) → M₂) y : M₂) : R)
    ((ψ : (a : M₂) → R) ((f : (a : M₁) → M₂) y : M₂) : R)
Tactic: obtain ⟨y, rfl⟩ := hf x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_1
M₁ : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
⊢ Eq (α := Dual R M₁ ≃ₗ[R] Dual R M₁) (dualMap (refl R M₁)) (refl R (Dual R M₁))
have h : ∀ (x : Dual R M₁) (x_1 : M₁),
  Eq.{u_1 + 1} (α := R) ((((dualMap (refl R M₁) : (a : Dual R M₁) → Dual R M₁) x : Dual R M₁) : (a : M₁) → R) x_1 : R)
    ((((refl R (Dual R M₁) : (a : Dual R M₁) → Dual R M₁) x : Dual R M₁) : (a : M₁) → R) x_1 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : Dual R R
r : R
| ((f : (a : R) → R) r : R)
have rw : ((f : (a : R) → R) (HSMul.hSMul (β := R) r 1) : R)
Tactic: rw [← mul_one r, ← smul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : Dual R R
r : R
⊢ HMul.hMul (α := R) ((f : (a : R) → R) 1 : R) r = (f : (a : R) → R) r
have conv_rhs : HMul.hMul (α := R) ((f : (a : R) → R) 1 : R) r = (f : (a : R) → R) (HSMul.hSMul (β := R) r 1)
Tactic: conv_rhs => rw [← mul_one r, ← smul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : Dual R R
r : R
⊢ HMul.hMul (α := R) ((f : (a : R) → R) 1 : R) r = (f : (a : R) → R) (HSMul.hSMul (β := R) r 1)
have rw : HMul.hMul (α := R) ((f : (a : R) → R) 1 : R) r = HSMul.hSMul (β := R) r ((f : (a : R) → R) 1 : R)
Tactic: rw [map_smul, smul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : Dual R R
r : R
rw : HMul.hMul (α := R) ((f : (a : R) → R) 1 : R) r = HSMul.hSMul (β := R) r ((f : (a : R) → R) 1 : R)
⊢ HMul.hMul (α := R) ((f : (a : R) → R) 1 : R) r = (f : (a : R) → R) (HSMul.hSMul (β := R) r 1)
have rw₁ : HMul.hMul (α := R) ((f : (a : R) → R) 1 : R) r = HMul.hMul (β := R) r ((f : (a : R) → R) 1 : R)
Tactic: rw [map_smul, smul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : Dual R R
r : R
rw : HMul.hMul (α := R) ((f : (a : R) → R) 1 : R) r = HSMul.hSMul (β := R) r ((f : (a : R) → R) 1 : R)
rw₁ : HMul.hMul (α := R) ((f : (a : R) → R) 1 : R) r = HMul.hMul (β := R) r ((f : (a : R) → R) 1 : R)
⊢ HMul.hMul (α := R) ((f : (a : R) → R) 1 : R) r = (f : (a : R) → R) (HSMul.hSMul (β := R) r 1)
have rw₂ : HMul.hMul (β := R) r ((f : (a : R) → R) 1 : R) = HMul.hMul (β := R) r ((f : (a : R) → R) 1 : R)
Tactic: rw [map_smul, smul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_1
M₁ : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
f : Dual R M₁
⊢ (dualMap f).range = R ∙ f
have h : ∀ (m : Dual R M₁), m ∈ (dualMap f).range ↔ Membership.mem (γ := Submodule R (Dual R M₁)) (R ∙ f) m
Tactic: ext m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_1
M₁ : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
f m : Dual R M₁
⊢ m ∈ (dualMap f).range ↔ Membership.mem (γ := Submodule R (Dual R M₁)) (R ∙ f) m
have h : m ∈ (dualMap f).range ↔ ∃ (a : R), a • f = m
Tactic: rw [Submodule.mem_span_singleton]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_1
M₁ : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
f m : Dual R M₁
⊢ m ∈ (dualMap f).range ↔ ∃ (a : R), a • f = m
have h : m ∈ (dualMap f).range →
  ∀ (r : Dual R R) (hr : (dualMap f : (a : Dual R R) → Dual R M₁) r = m),
    HSMul.hSMul (α := R) ((r : (a : R) → R) 1 : R) f = m
Tactic: refine ⟨fun ⟨r, hr⟩ ↦ ⟨r 1, ?_⟩, fun ⟨r, hr⟩ ↦ ⟨r • LinearMap.id, ?_⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_1
M₁ : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
f m : Dual R M₁
h :
  m ∈ (dualMap f).range →
    ∀ (r : Dual R R) (hr : (dualMap f : (a : Dual R R) → Dual R M₁) r = m),
      HSMul.hSMul (α := R) ((r : (a : R) → R) 1 : R) f = m
⊢ m ∈ (dualMap f).range ↔ ∃ (a : R), a • f = m
have h₁ : (∃ (a : R), a • f = m) →
  ∀ (r : R) (hr : r • f = m), (dualMap f : (a : Dual R R) → Dual R M₁) (HSMul.hSMul (β := R →ₗ[R] R) r id) = m
Tactic: refine ⟨fun ⟨r, hr⟩ ↦ ⟨r 1, ?_⟩, fun ⟨r, hr⟩ ↦ ⟨r • LinearMap.id, ?_⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_1
M₁ : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
f m : Dual R M₁
h : m ∈ (dualMap f).range
r : Dual R R
hr : (dualMap f : (a : Dual R R) → Dual R M₁) r = m
⊢ HSMul.hSMul (α := R) ((r : (a : R) → R) 1 : R) f = m
have h : ∀ (x : M₁),
  Eq.{u_1 + 1} (α := R) ((HSMul.hSMul (α := R) ((r : (a : R) → R) 1 : R) f : (a : M₁) → R) x : R)
    ((m : (a : M₁) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_1
M₁ : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
f m : Dual R M₁
h : ∃ (a : R), a • f = m
r : R
hr : r • f = m
⊢ (dualMap f : (a : Dual R R) → Dual R M₁) (HSMul.hSMul (β := R →ₗ[R] R) r id) = m
have h : ∀ (x : M₁),
  Eq.{u_1 + 1} (α := R)
    ((((dualMap f : (a : Dual R R) → Dual R M₁) (HSMul.hSMul (β := R →ₗ[R] R) r id) : Dual R M₁) : (a : M₁) → R) x : R)
    ((m : (a : M₁) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsReflexive R M
f : Dual R M
g : Dual R (Dual R M)
m : M := (LinearEquiv.symm (evalEquiv R M) : (a : Dual R (Dual R M)) → M) g
⊢ Eq.{u_3 + 1} (α := R) ((f : (a : M) → R) m : R) ((g : (a : Dual R M) → R) f : R)
have rw : Eq.{u_3 + 1} (α := R) ((f : (a : M) → R) m : R)
  ((((evalEquiv R M : (a : M) → Dual R (Dual R M))
            ((LinearEquiv.symm (evalEquiv R M) : (a : Dual R (Dual R M)) → M) g) :
          Dual R (Dual R M)) :
        (a : Dual R M) → R)
      f :
    R)
Tactic: rw [← (evalEquiv R M).apply_symm_apply g, evalEquiv_apply, Dual.eval_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsReflexive R M
f : Dual R M
g : Dual R (Dual R M)
m : M := (LinearEquiv.symm (evalEquiv R M) : (a : Dual R (Dual R M)) → M) g
rw :
  Eq.{u_3 + 1} (α := R) ((f : (a : M) → R) m : R)
    ((((evalEquiv R M : (a : M) → Dual R (Dual R M))
              ((LinearEquiv.symm (evalEquiv R M) : (a : Dual R (Dual R M)) → M) g) :
            Dual R (Dual R M)) :
          (a : Dual R M) → R)
        f :
      R)
⊢ Eq.{u_3 + 1} (α := R) ((f : (a : M) → R) m : R) ((g : (a : Dual R M) → R) f : R)
have rw₁ : Eq.{u_3 + 1} (α := R) ((f : (a : M) → R) m : R)
  ((((Dual.eval R M : (a : M) → Dual R (Dual R M))
            ((LinearEquiv.symm (evalEquiv R M) : (a : Dual R (Dual R M)) → M) g) :
          Dual R (Dual R M)) :
        (a : Dual R M) → R)
      f :
    R)
Tactic: rw [← (evalEquiv R M).apply_symm_apply g, evalEquiv_apply, Dual.eval_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsReflexive R M
f : Dual R M
g : Dual R (Dual R M)
m : M := (LinearEquiv.symm (evalEquiv R M) : (a : Dual R (Dual R M)) → M) g
rw :
  Eq.{u_3 + 1} (α := R) ((f : (a : M) → R) m : R)
    ((((evalEquiv R M : (a : M) → Dual R (Dual R M))
              ((LinearEquiv.symm (evalEquiv R M) : (a : Dual R (Dual R M)) → M) g) :
            Dual R (Dual R M)) :
          (a : Dual R M) → R)
        f :
      R)
rw₁ :
  Eq.{u_3 + 1} (α := R) ((f : (a : M) → R) m : R)
    ((((Dual.eval R M : (a : M) → Dual R (Dual R M))
              ((LinearEquiv.symm (evalEquiv R M) : (a : Dual R (Dual R M)) → M) g) :
            Dual R (Dual R M)) :
          (a : Dual R M) → R)
        f :
      R)
⊢ Eq.{u_3 + 1} (α := R) ((f : (a : M) → R) m : R) ((g : (a : Dual R M) → R) f : R)
have rw₂ : Eq.{u_3 + 1} (α := R) ((f : (a : M) → R) m : R)
  ((f : (a : M) → R) ((LinearEquiv.symm (evalEquiv R M) : (a : Dual R (Dual R M)) → M) g : M) : R)
Tactic: rw [← (evalEquiv R M).apply_symm_apply g, evalEquiv_apply, Dual.eval_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsReflexive R M
⊢ Eq (α := Dual R M →ₗ[R] Dual R (Dual R (Dual R M)))
    (↑(LinearEquiv.dualMap (LinearEquiv.symm (evalEquiv R M))) : Dual R M →ₗ[R] Dual R (Dual R (Dual R M)))
    (Dual.eval R (Dual R M))
have h : ∀ (x : Dual R M) (x_1 : Dual R (Dual R M)),
  Eq.{u_3 + 1} (α := R)
    (((((↑(LinearEquiv.dualMap (LinearEquiv.symm (evalEquiv R M))) : Dual R M →ₗ[R] Dual R (Dual R (Dual R M))) :
                (a : Dual R M) → Dual R (Dual R (Dual R M)))
              x :
            Dual R (Dual R (Dual R M))) :
          (a : Dual R (Dual R M)) → R)
        x_1 :
      R)
    ((((Dual.eval R (Dual R M) : (a : Dual R M) → Dual R (Dual R (Dual R M))) x : Dual R (Dual R (Dual R M))) :
          (a : Dual R (Dual R M)) → R)
        x_1 :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsReflexive R M
M' : Type u_6
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
f : M →ₗ[R] M'
⊢ eval R M' ∘ₗ f ∘ₗ (↑(LinearEquiv.symm (evalEquiv R M)) : Dual R (Dual R M) →ₗ[R] M) = f.dualMap.dualMap
have rw : (eval R M' ∘ₗ f) ∘ₗ (↑(LinearEquiv.symm (evalEquiv R M)) : Dual R (Dual R M) →ₗ[R] M) = f.dualMap.dualMap
Tactic: rw [← LinearMap.comp_assoc, LinearEquiv.comp_toLinearMap_symm_eq,
    evalEquiv_toLinearMap, eval_naturality]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsReflexive R M
M' : Type u_6
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
f : M →ₗ[R] M'
rw : (eval R M' ∘ₗ f) ∘ₗ (↑(LinearEquiv.symm (evalEquiv R M)) : Dual R (Dual R M) →ₗ[R] M) = f.dualMap.dualMap
⊢ eval R M' ∘ₗ f ∘ₗ (↑(LinearEquiv.symm (evalEquiv R M)) : Dual R (Dual R M) →ₗ[R] M) = f.dualMap.dualMap
have rw₁ : eval R M' ∘ₗ f = f.dualMap.dualMap ∘ₗ (↑(evalEquiv R M) : M →ₗ[R] Dual R (Dual R M))
Tactic: rw [← LinearMap.comp_assoc, LinearEquiv.comp_toLinearMap_symm_eq,
    evalEquiv_toLinearMap, eval_naturality]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsReflexive R M
M' : Type u_6
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
f : M →ₗ[R] M'
rw : (eval R M' ∘ₗ f) ∘ₗ (↑(LinearEquiv.symm (evalEquiv R M)) : Dual R (Dual R M) →ₗ[R] M) = f.dualMap.dualMap
rw₁ : eval R M' ∘ₗ f = f.dualMap.dualMap ∘ₗ (↑(evalEquiv R M) : M →ₗ[R] Dual R (Dual R M))
⊢ eval R M' ∘ₗ f ∘ₗ (↑(LinearEquiv.symm (evalEquiv R M)) : Dual R (Dual R M) →ₗ[R] M) = f.dualMap.dualMap
have rw₂ : eval R M' ∘ₗ f = f.dualMap.dualMap ∘ₗ eval R M
Tactic: rw [← LinearMap.comp_assoc, LinearEquiv.comp_toLinearMap_symm_eq,
    evalEquiv_toLinearMap, eval_naturality]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsReflexive R M
M' : Type u_6
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
f : M →ₗ[R] M'
rw : (eval R M' ∘ₗ f) ∘ₗ (↑(LinearEquiv.symm (evalEquiv R M)) : Dual R (Dual R M) →ₗ[R] M) = f.dualMap.dualMap
rw₁ : eval R M' ∘ₗ f = f.dualMap.dualMap ∘ₗ (↑(evalEquiv R M) : M →ₗ[R] Dual R (Dual R M))
rw₂ : eval R M' ∘ₗ f = f.dualMap.dualMap ∘ₗ eval R M
⊢ eval R M' ∘ₗ f ∘ₗ (↑(LinearEquiv.symm (evalEquiv R M)) : Dual R (Dual R M) →ₗ[R] M) = f.dualMap.dualMap
have rw₃ : eval R M' ∘ₗ f = eval R M' ∘ₗ f
Tactic: rw [← LinearMap.comp_assoc, LinearEquiv.comp_toLinearMap_symm_eq,
    evalEquiv_toLinearMap, eval_naturality]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Defs (goal)
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsReflexive R M
M' : Type u_6
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
f g : M →ₗ[R] M'
h : Injective (α := M') (β := Dual R (Dual R M')) (⇑(Dual.eval R M') : (a : M') → Dual R (Dual R M'))
⊢ f.dualMap.dualMap = g.dualMap.dualMap ↔ f = g
have simp : Dual.eval R M' ∘ₗ f ∘ₗ (↑(LinearEquiv.symm (evalEquiv R M)) : Dual R (Dual R M) →ₗ[R] M) =
    Dual.eval R M' ∘ₗ g ∘ₗ (↑(LinearEquiv.symm (evalEquiv R M)) : Dual R (Dual R M) →ₗ[R] M) ↔
  f = g
Tactic: simp only [← Dual.eval_comp_comp_evalEquiv_eq]