awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dual.Basis
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₁ : ∀ (i : ι), (h.basis : (a : ι) → M) i = e i
⊢ (⇑h.basis : (a : ι) → M) = e

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Dual.Basis
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₁ : Eq (α := ι →₀ R) ((h.basis.repr : (a : M) → ι →₀ R) (e i) : ι →₀ R) (Finsupp.single i 1 : ι →₀ R)
⊢ (h.basis : (a : ι) → M) i = e i

Tactic:
rw [Basis.apply_eq_iff]

Premises used: Module.Basis.apply_eq_iff
-- Module: Mathlib.LinearAlgebra.Dual.Basis
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₁ :
  ∀ (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)
⊢ Eq (α := ι →₀ R) ((h.basis.repr : (a : M) → ι →₀ R) (e i) : ι →₀ R) (Finsupp.single i 1 : ι →₀ R)

Tactic:
ext j
-- Module: Mathlib.LinearAlgebra.Dual.Basis
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)
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)
⊢ 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

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Dual.Basis
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.{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:
simp [h.eval_same]

Premises used: Module.DualBases.eval_same
-- Module: Mathlib.LinearAlgebra.Dual.Basis
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 : ι
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:
simp [hne, h.eval_of_ne hne.symm]

Premises used: Module.DualBases.eval_of_ne, Ne.symm
-- Module: Mathlib.LinearAlgebra.Dual.Basis
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)
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
⊢ i ∈ H

Tactic:
rcases (Finsupp.mem_span_image_iff_linearCombination _).mp hmem with ⟨l, supp_l, rfl⟩

Premises used: Iff.mp, Finsupp.mem_span_image_iff_linearCombination, rfl
-- Module: Mathlib.LinearAlgebra.Dual.Basis
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)
apply : ¬Eq.{u_1 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R)
⊢ i ∈ H

Tactic:
apply not_imp_comm.mp ((Finsupp.mem_supported' _ _).mp supp_l i)

Premises used: not_imp_comm, Iff.mp, Finsupp.mem_supported'
-- Module: Mathlib.LinearAlgebra.Dual.Basis
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)
rwa₁ rwa₂ rwa₃ 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)
⊢ ¬Eq.{u_1 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R)

Tactic:
rwa [← lc_def, h.dual_lc] at hi

Premises used: Module.DualBases.dual_lc, Module.DualBases.lc_def
-- Module: Mathlib.LinearAlgebra.Dual.Basis
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 ε
inst_3 : DecidableEq ι
inst_4 : Finite ι
i j : ι
⊢ Eq.{u_1 + 1} (α := R)
    ((((h.basis.dualBasis : (a : ι) → Dual R M) i : Dual R M) : (a : M) → R) ((h.basis : (a : ι) → M) j : M) : R)
    ((ε i : (a : M) → R) ((h.basis : (a : ι) → M) j : M) : R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
M : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : Dual R M
x : M
⊢ Eq.{u_1 + 1} (α := R) ((((dualPairing R M : (a : Dual R M) → M →ₗ[R] R) v : M →ₗ[R] R) : (a : M) → R) x : R)
    ((v : (a : M) → R) x : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
M : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : M
a : Dual R M
⊢ Eq.{u_1 + 1} (α := R) ((((eval R M : (a : M) → Dual R (Dual R M)) v : Dual R (Dual R M)) : (a : Dual R M) → R) a : R)
    ((a : (a : M) → R) v : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
M : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_4
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
u : M →ₗ[R] M'
l : Dual R M'
⊢ (((transpose : (a : M →ₗ[R] M') → Dual R M' →ₗ[R] Dual R M) u : Dual R M' →ₗ[R] Dual R M) :
        (a : Dual R M') → Dual R M)
      l =
    l ∘ₗ u

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
M : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_4
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
M'' : Type u_5
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
u : M' →ₗ[R] M''
v : M →ₗ[R] M'
⊢ Eq (α := Dual R M'' →ₗ[R] Dual R M)
    ((transpose : (a : M →ₗ[R] M'') → Dual R M'' →ₗ[R] Dual R M) (u ∘ₗ v) : Dual R M'' →ₗ[R] Dual R M)
    ((transpose : (a : M →ₗ[R] M') → Dual R M' →ₗ[R] Dual R M) v ∘ₗ
        (transpose : (a : M' →ₗ[R] M'') → Dual R M'' →ₗ[R] Dual R M') u :
      Dual R M'' →ₗ[R] Dual R M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Dual.Defs
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₂
⊢ f.dualMap = lcomp R R f

Tactic:
rfl

Premises used: LinearMap.mk₂'ₛₗ, LinearMap.lcomp, LinearMap.flip, LinearMap.dualMap, rfl, LinearMap.lcompₛₗ
-- Module: Mathlib.LinearAlgebra.Dual.Defs
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₂
⊢ f.dualMap = (Dual.transpose : (a : M₁ →ₗ[R] M₂) → Dual R M₂ →ₗ[R] Dual R M₁) f

Tactic:
rfl

Premises used: LinearMap.dualMap, rfl
-- Module: Mathlib.LinearAlgebra.Dual.Defs
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₂
g : Dual R M₂
⊢ (f.dualMap : (a : Dual R M₂) → Dual R M₁) g = g ∘ₗ f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Dual.Defs
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₂
g : Dual R M₂
x : M₁
⊢ Eq.{u_1 + 1} (α := R) ((((f.dualMap : (a : Dual R M₂) → Dual R M₁) g : Dual R M₁) : (a : M₁) → R) x : R)
    ((g : (a : M₂) → R) ((f : (a : M₁) → M₂) x : M₂) : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
M₁ : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
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)
⊢ Eq (α := Dual R M₁ →ₗ[R] Dual R M₁) (dualMap id) id

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
M₁ : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
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:
rfl
-- Module: Mathlib.LinearAlgebra.Dual.Defs
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₂
M₃ : Type u_4
inst_5 : AddCommMonoid M₃
inst_6 : Module R M₃
f : M₁ →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
⊢ f.dualMap ∘ₗ g.dualMap = (g ∘ₗ f).dualMap

Tactic:
rfl

Premises used: LinearMap.dualMap, rfl
-- Module: Mathlib.LinearAlgebra.Dual.Defs
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₁)
h₁ : ∀ (x : M₂), Eq.{u_1 + 1} (α := R) ((φ : (a : M₂) → R) x : R) ((ψ : (a : M₂) → R) x : R)
⊢ φ = ψ

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Dual.Defs
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₂
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)
⊢ Eq.{u_1 + 1} (α := R) ((φ : (a : M₂) → R) x : R) ((ψ : (a : M₂) → R) x : R)

Tactic:
obtain ⟨y, rfl⟩ := hf x

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Dual.Defs
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₁)
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:
congr_arg (fun g : Module.Dual R M₁ => g y) h

Premises used: congr_arg, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dual.Defs
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₁)
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:
exact congr_arg (fun g : Module.Dual R M₁ => g y) h

Premises used: congr_arg, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dual.Defs
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₂
g : Dual R M₂
x : M₁
⊢ Eq.{u_1 + 1} (α := R) ((((f.dualMap : (a : Dual R M₂) → Dual R M₁) g : Dual R M₁) : (a : M₁) → R) x : R)
    ((g : (a : M₂) → R) ((f : (a : M₁) → M₂) x : M₂) : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
M₁ : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
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)
⊢ Eq (α := Dual R M₁ ≃ₗ[R] Dual R M₁) (dualMap (refl R M₁)) (refl R (Dual R M₁))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
M₁ : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M₁
inst_2 : Module R M₁
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:
rfl
-- Module: Mathlib.LinearAlgebra.Dual.Defs
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₂
⊢ f.dualMap.symm = f.symm.dualMap

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearEquiv.dualMap, LinearMap.dualMap, rfl
-- Module: Mathlib.LinearAlgebra.Dual.Defs
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₂
M₃ : Type u_4
inst_5 : AddCommMonoid M₃
inst_6 : Module R M₃
f : M₁ ≃ₗ[R] M₂
g : M₂ ≃ₗ[R] M₃
⊢ g.dualMap ≪≫ₗ f.dualMap = dualMap (f ≪≫ₗ g)

Tactic:
rfl

Premises used: LinearEquiv.dualMap, LinearEquiv.trans, LinearMap.dualMap, rfl
-- Module: Mathlib.LinearAlgebra.Dual.Defs
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₂
⊢ f.dualMap.dualMap ∘ₗ eval R M₁ = eval R M₂ ∘ₗ f

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
inst : CommSemiring R
f : Dual R R
r : R
rw : ((f : (a : R) → R) (HSMul.hSMul (β := R) r 1) : R)
| ((f : (a : R) → R) r : R)

Tactic:
rw [← mul_one r, ← smul_eq_mul]

Premises used: smul_eq_mul, mul_one
-- Module: Mathlib.LinearAlgebra.Dual.Defs
Goal:
R : Type u_1
inst : CommSemiring R
f : Dual R R
r : R
conv_rhs : HMul.hMul (α := R) ((f : (a : R) → R) 1 : R) r = (f : (a : R) → R) (HSMul.hSMul (β := R) r 1)
⊢ HMul.hMul (α := R) ((f : (a : R) → R) 1 : R) r = (f : (a : R) → R) r

Tactic:
conv_rhs => rw [← mul_one r, ← smul_eq_mul]

Premises used: smul_eq_mul, mul_one
-- Module: Mathlib.LinearAlgebra.Dual.Defs
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)
rw₂ rw₃ : HMul.hMul (β := R) r ((f : (a : R) → R) 1 : 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)

Tactic:
rw [map_smul, smul_eq_mul, mul_comm]

Premises used: mul_comm, smul_eq_mul, map_smul
-- Module: Mathlib.LinearAlgebra.Dual.Defs
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₁
h : ∀ (m : Dual R M₁), m ∈ (dualMap f).range ↔ Membership.mem (γ := Submodule R (Dual R M₁)) (R ∙ f) m
⊢ (dualMap f).range = R ∙ f

Tactic:
ext m
-- Module: Mathlib.LinearAlgebra.Dual.Defs
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 ↔ ∃ (a : R), a • f = m
⊢ m ∈ (dualMap f).range ↔ Membership.mem (γ := Submodule R (Dual R M₁)) (R ∙ f) m

Tactic:
rw [Submodule.mem_span_singleton]

Premises used: Submodule.mem_span_singleton
-- Module: Mathlib.LinearAlgebra.Dual.Defs
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

Tactic:
⟨fun ⟨r, hr⟩ ↦ ⟨r 1, ?_⟩, fun ⟨r, hr⟩ ↦ ⟨r • LinearMap.id, ?_⟩⟩

Premises used: LinearMap.id, _private.0.LinearMap.range_dualMap_dual_eq_span_singleton.match_1, _private.0.LinearMap.range_dualMap_dual_eq_span_singleton.match_2, Membership.mem, Exists, LinearMap.range, Iff.intro, Exists.intro, HSMul.hSMul, OfNat.ofNat, Eq, DFunLike.coe, LinearMap.dualMap
-- Module: Mathlib.LinearAlgebra.Dual.Defs
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
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
⊢ m ∈ (dualMap f).range ↔ ∃ (a : R), a • f = m

Tactic:
refine ⟨fun ⟨r, hr⟩ ↦ ⟨r 1, ?_⟩, fun ⟨r, hr⟩ ↦ ⟨r • LinearMap.id, ?_⟩⟩
-- Module: Mathlib.LinearAlgebra.Dual.Defs
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_1 : m ∈ (dualMap f).range
r : Dual R R
hr : (dualMap f : (a : Dual R R) → Dual R M₁) r = m
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)
⊢ HSMul.hSMul (α := R) ((r : (a : R) → R) 1 : R) f = m

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Dual.Defs
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
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:
simp [dualMap_apply', ← hr]

Premises used: LinearMap.dualMap_apply'
-- Module: Mathlib.LinearAlgebra.Dual.Defs
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_1 : ∃ (a : R), a • f = m
r : R
hr : r • f = m
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)
⊢ (dualMap f : (a : Dual R R) → Dual R M₁) (HSMul.hSMul (β := R →ₗ[R] R) r id) = m

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Dual.Defs
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
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:
simp [dualMap_apply', ← hr]

Premises used: LinearMap.dualMap_apply'
-- Module: Mathlib.LinearAlgebra.Dual.Defs
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
⊢ Bijective (α := M) (β := Dual R (Dual R M)) (⇑(Dual.eval R M) : (a : M) → Dual R (Dual R M))

Tactic:
IsReflexive.bijective_dual_eval'

Premises used: Module.IsReflexive.bijective_dual_eval'
-- Module: Mathlib.LinearAlgebra.Dual.Defs
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 (α := Submodule R (Dual R (Dual R M))) (range (Dual.eval R M)) ⊤

Tactic:
range_eq_top.mpr (bijective_dual_eval _ _).2

Premises used: Iff.mpr, LinearMap.range_eq_top, And.right, Module.bijective_dual_eval
-- Module: Mathlib.LinearAlgebra.Dual.Defs
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 (α := M →ₗ[R] Dual R (Dual R M)) (↑(evalEquiv R M) : M →ₗ[R] Dual R (Dual R M)) (Dual.eval R M)

Tactic:
rfl

Premises used: LinearMap.mk₂'ₛₗ, LinearMap.flip, Module.Dual.eval, rfl
-- Module: Mathlib.LinearAlgebra.Dual.Defs
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 : M
⊢ Eq (α := Dual R (Dual R M)) ((evalEquiv 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))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Dual.Defs
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)
set :
  let 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)
⊢ Eq.{u_3 + 1} (α := R) ((f : (a : M) → R) ((LinearEquiv.symm (evalEquiv R M) : (a : Dual R (Dual R M)) → M) g : M) : R)
    ((g : (a : Dual R M) → R) f : R)

Tactic:
set m := (evalEquiv R M).symm g

Premises used: LinearEquiv.symm, Module.evalEquiv, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dual.Defs
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)
rw₂ 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)
⊢ Eq.{u_3 + 1} (α := R) ((f : (a : M) → R) m : R) ((g : (a : Dual R M) → R) f : R)

Tactic:
rw [← (evalEquiv R M).apply_symm_apply g, evalEquiv_apply, Dual.eval_apply]

Premises used: Module.Dual.eval_apply, Module.evalEquiv_apply, LinearEquiv.apply_symm_apply, Module.evalEquiv