awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_4
V : Type u_5
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Submodule K (Dual K V)
⊢ FiniteDimensional.{u_4, u_5} K (V ⧸ W.dualCoannihilator) ↔ FiniteDimensional K ↥W

Tactic:
⟨fun _ ↦ FiniteDimensional.of_injective _ W.flip_quotDualCoannihilatorToDual_injective,
    fun _ ↦ FiniteDimensional.of_injective _ W.quotDualCoannihilatorToDual_injective⟩

Premises used: Unit.unit, Submodule.quotDualCoannihilatorToDual, sorryAx, Lean.Name.num, FiniteDimensional.of_injective, Lean.Name.str, Lean.Name.anonymous, Bool.true, LinearMap.flip, Iff.intro, Function.const, Lean.Name, OfNat.ofNat, Submodule.flip_quotDualCoannihilatorToDual_injective
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_4
V : Type u_5
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
inst_3 : FiniteDimensional.{u_4, u_5} K ↥W
e1 : ↥W ≃ₗ[K] Dual K V ⧸ dualAnnihilator W :=
  Basis.toDualEquiv (ι := Free.ChooseBasisIndex K ↥W) (Free.chooseBasis K ↥W) ≪≫ₗ W.quotAnnihilatorEquiv.symm
⊢ FiniteDimensional K (Dual K V ⧸ dualAnnihilator W)

Tactic:
haveI := e1.finiteDimensional
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_4
V : Type u_5
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
inst_3 : FiniteDimensional.{u_4, u_5} K ↥W
e1 : ↥W ≃ₗ[K] Dual K V ⧸ dualAnnihilator W :=
  Basis.toDualEquiv (ι := Free.ChooseBasisIndex K ↥W) (Free.chooseBasis K ↥W) ≪≫ₗ W.quotAnnihilatorEquiv.symm
this : FiniteDimensional K (Dual K V ⧸ dualAnnihilator W)
e2 : (Dual K V ⧸ dualAnnihilator W) ≃ₗ[K] ↥(dualAnnihilator W).dualAnnihilator :=
  Basis.toDualEquiv (ι := Free.ChooseBasisIndex K (Dual K V ⧸ dualAnnihilator W))
      (Free.chooseBasis K (Dual K V ⧸ dualAnnihilator W)) ≪≫ₗ
    (dualAnnihilator W).dualQuotEquivDualAnnihilator
⊢ FiniteDimensional K ↥(dualAnnihilator W).dualAnnihilator

Tactic:
haveI := LinearEquiv.finiteDimensional (V₂ := W.dualAnnihilator.dualAnnihilator) e2
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_4
V : Type u_5
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
inst_3 : FiniteDimensional.{u_4, u_5} K ↥W
e1 : ↥W ≃ₗ[K] Dual K V ⧸ dualAnnihilator W :=
  Basis.toDualEquiv (ι := Free.ChooseBasisIndex K ↥W) (Free.chooseBasis K ↥W) ≪≫ₗ W.quotAnnihilatorEquiv.symm
this_1 : FiniteDimensional K (Dual K V ⧸ dualAnnihilator W)
e2 : (Dual K V ⧸ dualAnnihilator W) ≃ₗ[K] ↥(dualAnnihilator W).dualAnnihilator :=
  Basis.toDualEquiv (ι := Free.ChooseBasisIndex K (Dual K V ⧸ dualAnnihilator W))
      (Free.chooseBasis K (Dual K V ⧸ dualAnnihilator W)) ≪≫ₗ
    (dualAnnihilator W).dualQuotEquivDualAnnihilator
this : FiniteDimensional K ↥(dualAnnihilator W).dualAnnihilator
rw : finrank K ↥(map (σ₁₂ := RingHom.id K) (Dual.eval K V) W) = finrank K ↥(dualAnnihilator W).dualAnnihilator
⊢ (dualAnnihilator W).dualAnnihilator = map (σ₁₂ := RingHom.id K) (Dual.eval K V) W

Tactic:
rw [eq_of_le_of_finrank_eq (map_le_dualAnnihilator_dualAnnihilator W)]

Premises used: Submodule.eq_of_le_of_finrank_eq, Subspace.map_le_dualAnnihilator_dualAnnihilator
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_4
V : Type u_5
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
inst_3 : FiniteDimensional.{u_4, u_5} K ↥W
e1 : ↥W ≃ₗ[K] Dual K V ⧸ dualAnnihilator W :=
  Basis.toDualEquiv (ι := Free.ChooseBasisIndex K ↥W) (Free.chooseBasis K ↥W) ≪≫ₗ W.quotAnnihilatorEquiv.symm
this_1 : FiniteDimensional K (Dual K V ⧸ dualAnnihilator W)
e2 : (Dual K V ⧸ dualAnnihilator W) ≃ₗ[K] ↥(dualAnnihilator W).dualAnnihilator :=
  Basis.toDualEquiv (ι := Free.ChooseBasisIndex K (Dual K V ⧸ dualAnnihilator W))
      (Free.chooseBasis K (Dual K V ⧸ dualAnnihilator W)) ≪≫ₗ
    (dualAnnihilator W).dualQuotEquivDualAnnihilator
this : FiniteDimensional K ↥(dualAnnihilator W).dualAnnihilator
rw : finrank K (Dual K V ⧸ dualAnnihilator W) = finrank K ↥(dualAnnihilator W).dualAnnihilator
⊢ finrank K ↥(map (σ₁₂ := RingHom.id K) (Dual.eval K V) W) = finrank K ↥(dualAnnihilator W).dualAnnihilator

Tactic:
rw [← (equivMapOfInjective _ (eval_apply_injective K (V := V)) W).finrank_eq, e1.finrank_eq]

Premises used: Module.eval_apply_injective, Submodule.equivMapOfInjective, LinearEquiv.finrank_eq
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_4
V : Type u_5
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
inst_3 : FiniteDimensional.{u_4, u_5} K ↥W
e1 : ↥W ≃ₗ[K] Dual K V ⧸ dualAnnihilator W :=
  Basis.toDualEquiv (ι := Free.ChooseBasisIndex K ↥W) (Free.chooseBasis K ↥W) ≪≫ₗ W.quotAnnihilatorEquiv.symm
this_1 : FiniteDimensional K (Dual K V ⧸ dualAnnihilator W)
e2 : (Dual K V ⧸ dualAnnihilator W) ≃ₗ[K] ↥(dualAnnihilator W).dualAnnihilator :=
  Basis.toDualEquiv (ι := Free.ChooseBasisIndex K (Dual K V ⧸ dualAnnihilator W))
      (Free.chooseBasis K (Dual K V ⧸ dualAnnihilator W)) ≪≫ₗ
    (dualAnnihilator W).dualQuotEquivDualAnnihilator
this : FiniteDimensional K ↥(dualAnnihilator W).dualAnnihilator
⊢ finrank K (Dual K V ⧸ dualAnnihilator W) = finrank K ↥(dualAnnihilator W).dualAnnihilator

Tactic:
e2.finrank_eq

Premises used: Set.Mem, LinearEquiv.finrank_eq
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_4
V : Type u_5
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
inst_3 : FiniteDimensional.{u_4, u_5} K ↥W
e1 : ↥W ≃ₗ[K] Dual K V ⧸ dualAnnihilator W :=
  Basis.toDualEquiv (ι := Free.ChooseBasisIndex K ↥W) (Free.chooseBasis K ↥W) ≪≫ₗ W.quotAnnihilatorEquiv.symm
this_1 : FiniteDimensional K (Dual K V ⧸ dualAnnihilator W)
e2 : (Dual K V ⧸ dualAnnihilator W) ≃ₗ[K] ↥(dualAnnihilator W).dualAnnihilator :=
  Basis.toDualEquiv (ι := Free.ChooseBasisIndex K (Dual K V ⧸ dualAnnihilator W))
      (Free.chooseBasis K (Dual K V ⧸ dualAnnihilator W)) ≪≫ₗ
    (dualAnnihilator W).dualQuotEquivDualAnnihilator
this : FiniteDimensional K ↥(dualAnnihilator W).dualAnnihilator
⊢ finrank K (Dual K V ⧸ dualAnnihilator W) = finrank K ↥(dualAnnihilator W).dualAnnihilator

Tactic:
exact e2.finrank_eq

Premises used: LinearEquiv.finrank_eq
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
K : Type u_4
V : Type u_5
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K (Dual K V)
inst_3 : FiniteDimensional K V
rw : (dualCoannihilator W).dualAnnihilator.dualAnnihilator = dualAnnihilator W
rw₁ rw₂ : Eq (α := Submodule K (Dual K (Dual K V))) (dualAnnihilator W) (dualAnnihilator W)
⊢ map (Dual.eval K V) (dualCoannihilator W) = dualAnnihilator W

Tactic:
rw [← dualAnnihilator_dualAnnihilator_eq_map, dualCoannihilator_dualAnnihilator_eq]

Premises used: Subspace.dualAnnihilator_dualAnnihilator_eq_map, Subspace.dualCoannihilator_dualAnnihilator_eq
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_1
α : Type u_2
F : Type u_3
inst : Finite ι
inst_1 : Field F
f : ι → α → F
rw :
  dualCoannihilator (map (↑(Finsupp.llift F F F ι) : (ι → F) →ₗ[F] (ι →₀ F) →ₗ[F] F) (span F (Set.range (flip f)))) =
      ⊥ ↔
    Eq (α := Submodule F (ι →₀ F)) (LinearMap.ker (Finsupp.linearCombination F f)) ⊥
⊢ Eq (α := Submodule F (ι → F)) (span F (Set.range (flip f))) ⊤ ↔ LinearIndependent F f

Tactic:
rw [linearIndependent_iff_ker, ← Submodule.map_eq_top_iff (e := Finsupp.llift F F F ι),
    ← Subspace.dualCoannihilator_dualAnnihilator_eq (W := map ..), dualAnnihilator_eq_top_iff]

Premises used: Subspace.dualCoannihilator_dualAnnihilator_eq, Submodule.dualAnnihilator_eq_top_iff, linearIndependent_iff_ker, Submodule.map_eq_top_iff
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_1
α : Type u_2
F : Type u_3
inst : Finite ι
inst_1 : Field F
f : ι → α → F
a :
  dualCoannihilator (map (↑(Finsupp.llift F F F ι) : (ι → F) →ₗ[F] (ι →₀ F) →ₗ[F] F) (span F (Set.range (flip f)))) =
    LinearMap.ker (Finsupp.linearCombination F f)
⊢ dualCoannihilator (map (↑(Finsupp.llift F F F ι) : (ι → F) →ₗ[F] (ι →₀ F) →ₗ[F] F) (span F (Set.range (flip f)))) =
      ⊥ ↔
    Eq (α := Submodule F (ι →₀ F)) (LinearMap.ker (Finsupp.linearCombination F f)) ⊥

Tactic:
congr!
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_1
α : Type u_2
F : Type u_3
inst : Finite ι
inst_1 : Field F
f : ι → α → F
a :
  {x : ι →₀ F |
      ∀ (f_1 : Dual F (ι →₀ F)),
        Membership.mem (γ := Set (Dual F (ι →₀ F)))
            (Set.range
              ((⇑(↑(Finsupp.llift F F F ι) : (ι → F) →ₗ[F] (ι →₀ F) →ₗ[F] F) : (a : ι → F) → Dual F (ι →₀ F)) ∘ flip f))
            f_1 →
          Eq.{u_3 + 1} (α := F) ((f_1 : (a : ι →₀ F) → F) x : F) (0 : F)} =
    (↑(LinearMap.ker (Finsupp.linearCombination F f)) : Set (ι →₀ F))
⊢ dualCoannihilator (map (↑(Finsupp.llift F F F ι) : (ι → F) →ₗ[F] (ι →₀ F) →ₗ[F] F) (span F (Set.range (flip f)))) =
    LinearMap.ker (Finsupp.linearCombination F f)

Tactic:
rw [SetLike.ext'_iff, map_span, Submodule.coe_dualCoannihilator_span, ← Set.range_comp]

Premises used: Set.range_comp, Submodule.coe_dualCoannihilator_span, SetLike.ext'_iff, Submodule.map_span
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_1
α : Type u_2
F : Type u_3
inst : Finite ι
inst_1 : Field F
f : ι → α → F
a :
  ∀ (x : ι →₀ F),
    Membership.mem (γ := Set (ι →₀ F))
        {x : ι →₀ F |
          ∀ (f_1 : Dual F (ι →₀ F)),
            Membership.mem (γ := Set (Dual F (ι →₀ F)))
                (Set.range
                  ((⇑(↑(Finsupp.llift F F F ι) : (ι → F) →ₗ[F] (ι →₀ F) →ₗ[F] F) : (a : ι → F) → Dual F (ι →₀ F)) ∘
                    flip f))
                f_1 →
              Eq.{u_3 + 1} (α := F) ((f_1 : (a : ι →₀ F) → F) x : F) (0 : F)}
        x ↔
      x ∈ (↑(LinearMap.ker (Finsupp.linearCombination F f)) : Set (ι →₀ F))
⊢ {x : ι →₀ F |
      ∀ (f_1 : Dual F (ι →₀ F)),
        Membership.mem (γ := Set (Dual F (ι →₀ F)))
            (Set.range
              ((⇑(↑(Finsupp.llift F F F ι) : (ι → F) →ₗ[F] (ι →₀ F) →ₗ[F] F) : (a : ι → F) → Dual F (ι →₀ F)) ∘ flip f))
            f_1 →
          Eq.{u_3 + 1} (α := F) ((f_1 : (a : ι →₀ F) → F) x : F) (0 : F)} =
    (↑(LinearMap.ker (Finsupp.linearCombination F f)) : Set (ι →₀ F))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_1
α : Type u_2
F : Type u_3
inst : Finite ι
inst_1 : Field F
f : ι → α → F
x : ι →₀ F
⊢ Membership.mem (γ := Set (ι →₀ F))
      {x : ι →₀ F |
        ∀ (f_1 : Dual F (ι →₀ F)),
          Membership.mem (γ := Set (Dual F (ι →₀ F)))
              (Set.range
                ((⇑(↑(Finsupp.llift F F F ι) : (ι → F) →ₗ[F] (ι →₀ F) →ₗ[F] F) : (a : ι → F) → Dual F (ι →₀ F)) ∘
                  flip f))
              f_1 →
            Eq.{u_3 + 1} (α := F) ((f_1 : (a : ι →₀ F) → F) x : F) (0 : F)}
      x ↔
    x ∈ (↑(LinearMap.ker (Finsupp.linearCombination F f)) : Set (ι →₀ F))

Tactic:
simp [funext_iff, Finsupp.linearCombination, Finsupp.sum, Finset.sum_apply, flip]

Premises used: Finset.sum_apply, Finsupp.sum, funext_iff, flip, Finsupp.linearCombination
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set ι
v : ι → V
hli : LinearIndepOn K v s
⊢ LinearIndepOn K id (v '' s)

Tactic:
replace hli : LinearIndepOn K id (v '' s) := LinearIndepOn.id_image hli
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set ι
v : ι → V
hli : LinearIndepOn K id (v '' s)
⊢ LE.le.{u_3} (α := Submodule K V) ⊤
    (span K
      (Set.range
        fun
          (x :
            (↑(LinearIndepOn.extend.{u_3, u_3, u_2} (K := K) (V := V) (v := id) (s := v '' s) (t := Set.univ) hli ⋯) :
              Type u_3)) ↦
        id (↑x : V)))

Tactic:
simpa using hli.span_extend_eq_span <| Set.subset_univ _

Premises used: Set.subset_univ, LinearIndepOn.span_extend_eq_span
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set ι
v : ι → V
hli : LinearIndepOn K id (v '' s)
b : Basis
  (↑(LinearIndepOn.extend.{u_3, u_3, u_2} (K := K) (V := V) (v := id) (s := v '' s) (t := Set.univ) hli ⋯) : Type u_3) K
  V :=
  Basis.mk ⋯ ⋯
⊢ ∃ (f : Dual K V), ∀ i ∈ s, Eq.{u_2 + 1} (α := K) ((f : (a : V) → K) (v i) : K) (1 : K)

Tactic:
⟨b.constr K 1, fun i hi ↦ ?_⟩

Premises used: Exists.intro, OfNat.ofNat, DFunLike.coe, Module.Basis.constr
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set ι
v : ι → V
hli : LinearIndepOn K id (v '' s)
b : Basis
  (↑(LinearIndepOn.extend.{u_3, u_3, u_2} (K := K) (V := V) (v := id) (s := v '' s) (t := Set.univ) hli ⋯) : Type u_3) K
  V :=
  Basis.mk ⋯ ⋯
refine :
  ∀ (i : ι) (hi : i ∈ s),
    Eq.{u_2 + 1} (α := K)
      (((b.constr K : (a : (↑(hli.extend ⋯) : Type u_3) → K) → V →ₗ[K] K) 1 : (a : V) → K) (v i) : K) (1 : K)
⊢ ∃ (f : Dual K V), ∀ i ∈ s, Eq.{u_2 + 1} (α := K) ((f : (a : V) → K) (v i) : K) (1 : K)

Tactic:
refine ⟨b.constr K 1, fun i hi ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set ι
v : ι → V
hli : LinearIndepOn K id (v '' s)
b : Basis
  (↑(LinearIndepOn.extend.{u_3, u_3, u_2} (K := K) (V := V) (v := id) (s := v '' s) (t := Set.univ) hli ⋯) : Type u_3) K
  V :=
  Basis.mk ⋯ ⋯
i : ι
hi : i ∈ s
⊢ v i ∈ LinearIndepOn.extend.{u_3, u_3, u_2} (K := K) (V := V) (v := id) (s := v '' s) (t := Set.univ) hli ⋯

Tactic:
replace hi : v i ∈ hli.extend (Set.subset_univ _) :=
    hli.subset_extend _ <| Set.mem_image_of_mem v hi
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set ι
v : ι → V
hli : LinearIndepOn K id (v '' s)
b : Basis
  (↑(LinearIndepOn.extend.{u_3, u_3, u_2} (K := K) (V := V) (v := id) (s := v '' s) (t := Set.univ) hli ⋯) : Type u_3) K
  V :=
  Basis.mk ⋯ ⋯
i : ι
hi : v i ∈ LinearIndepOn.extend.{u_3, u_3, u_2} (K := K) (V := V) (v := id) (s := v '' s) (t := Set.univ) hli ⋯
ri : (↑(LinearIndepOn.extend.{u_3, u_3, u_2} (K := K) (V := V) (v := id) (s := v '' s) (t := Set.univ) hli ⋯) :
  Type u_3) :=
  Subtype.mk (p := fun (x : V) ↦
    x ∈ LinearIndepOn.extend.{u_3, u_3, u_2} (K := K) (V := V) (v := id) (s := v '' s) (t := Set.univ) hli ⋯) (v i) hi
⊢ (b : (a : (↑(hli.extend ⋯) : Type u_3)) → V) ri = v i

Tactic:
simp [b, ri]
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set ι
v : ι → V
hli : LinearIndepOn K id (v '' s)
b : Basis
  (↑(LinearIndepOn.extend.{u_3, u_3, u_2} (K := K) (V := V) (v := id) (s := v '' s) (t := Set.univ) hli ⋯) : Type u_3) K
  V :=
  Basis.mk ⋯ ⋯
i : ι
hi : v i ∈ LinearIndepOn.extend.{u_3, u_3, u_2} (K := K) (V := V) (v := id) (s := v '' s) (t := Set.univ) hli ⋯
ri : (↑(LinearIndepOn.extend.{u_3, u_3, u_2} (K := K) (V := V) (v := id) (s := v '' s) (t := Set.univ) hli ⋯) :
  Type u_3) :=
  Subtype.mk (p := fun (x : V) ↦
    x ∈ LinearIndepOn.extend.{u_3, u_3, u_2} (K := K) (V := V) (v := id) (s := v '' s) (t := Set.univ) hli ⋯) (v i) hi
⊢ (b : (a : (↑(hli.extend ⋯) : Type u_3)) → V) ri = v i

Tactic:
have : b ri = v i := by simp [b, ri]
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_1
K : Type u_2
V : Type u_3
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set ι
v : ι → V
hli : LinearIndepOn K id (v '' s)
b : Basis
  (↑(LinearIndepOn.extend.{u_3, u_3, u_2} (K := K) (V := V) (v := id) (s := v '' s) (t := Set.univ) hli ⋯) : Type u_3) K
  V :=
  Basis.mk ⋯ ⋯
i : ι
hi : v i ∈ LinearIndepOn.extend.{u_3, u_3, u_2} (K := K) (V := V) (v := id) (s := v '' s) (t := Set.univ) hli ⋯
ri : (↑(LinearIndepOn.extend.{u_3, u_3, u_2} (K := K) (V := V) (v := id) (s := v '' s) (t := Set.univ) hli ⋯) :
  Type u_3) :=
  Subtype.mk (p := fun (x : V) ↦
    x ∈ LinearIndepOn.extend.{u_3, u_3, u_2} (K := K) (V := V) (v := id) (s := v '' s) (t := Set.univ) hli ⋯) (v i) hi
this : (b : (a : (↑(hli.extend ⋯) : Type u_3)) → V) ri = v i
⊢ Eq.{u_2 + 1} (α := K) (((b.constr K : (a : (↑(hli.extend ⋯) : Type u_3) → K) → V →ₗ[K] K) 1 : (a : V) → K) (v i) : K)
    (1 : K)

Tactic:
simp [← this]
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
f : Dual R M
g : Dual R N
m : M
n : N
⊢ (((dualDistrib R M N : (a : Dual R M ⊗[R] Dual R N) → Dual R (M ⊗[R] N)) (f ⊗ₜ[R] g) : Dual R (M ⊗[R] N)) :
        (a : M ⊗[R] N) → R)
      (m ⊗ₜ[R] n) =
    HMul.hMul (α := R) (β := R) ((f : (a : M) → R) m : R) ((g : (a : N) → R) n : R)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
⊢ Eq.{u_1 + 1} (α := R)
    (((dualDistrib R N M : (a : Dual R N ⊗[R] Dual R M) → Dual R (N ⊗[R] M)) 0 : (a : N ⊗[R] M) → R)
        ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) 0) :
      R)
    (((dualDistrib R M N : (a : Dual R M ⊗[R] Dual R N) → Dual R (M ⊗[R] N))
            ((TensorProduct.comm R (Dual R N) (Dual R M) : (a : Dual R N ⊗[R] Dual R M) → Dual R M ⊗[R] Dual R N) 0) :
          (a : M ⊗[R] N) → R)
        0 :
      R)

Tactic:
simp_all [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x : M
y : N
⊢ Eq.{u_1 + 1} (α := R)
    (((dualDistrib R N M : (a : Dual R N ⊗[R] Dual R M) → Dual R (N ⊗[R] M)) 0 : (a : N ⊗[R] M) → R)
        ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) (x ⊗ₜ[R] y) : N ⊗[R] M) :
      R)
    (((dualDistrib R M N : (a : Dual R M ⊗[R] Dual R N) → Dual R (M ⊗[R] N))
            ((TensorProduct.comm R (Dual R N) (Dual R M) : (a : Dual R N ⊗[R] Dual R M) → Dual R M ⊗[R] Dual R N) 0) :
          (a : M ⊗[R] N) → R)
        (x ⊗ₜ[R] y) :
      R)

Tactic:
simp_all [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x y : M ⊗[R] N
h :
  Eq.{u_1 + 1} (α := R)
    (((dualDistrib R N M : (a : Dual R N ⊗[R] Dual R M) → Dual R (N ⊗[R] M)) 0 : (a : N ⊗[R] M) → R)
        ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) x : N ⊗[R] M) :
      R)
    (((dualDistrib R M N : (a : Dual R M ⊗[R] Dual R N) → Dual R (M ⊗[R] N))
            ((TensorProduct.comm R (Dual R N) (Dual R M) : (a : Dual R N ⊗[R] Dual R M) → Dual R M ⊗[R] Dual R N) 0) :
          (a : M ⊗[R] N) → R)
        x :
      R)
h_1 :
  Eq.{u_1 + 1} (α := R)
    (((dualDistrib R N M : (a : Dual R N ⊗[R] Dual R M) → Dual R (N ⊗[R] M)) 0 : (a : N ⊗[R] M) → R)
        ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) y : N ⊗[R] M) :
      R)
    (((dualDistrib R M N : (a : Dual R M ⊗[R] Dual R N) → Dual R (M ⊗[R] N))
            ((TensorProduct.comm R (Dual R N) (Dual R M) : (a : Dual R N ⊗[R] Dual R M) → Dual R M ⊗[R] Dual R N) 0) :
          (a : M ⊗[R] N) → R)
        y :
      R)
⊢ Eq.{u_1 + 1} (α := R)
    (((dualDistrib R N M : (a : Dual R N ⊗[R] Dual R M) → Dual R (N ⊗[R] M)) 0 : (a : N ⊗[R] M) → R)
        ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) (x + y) : N ⊗[R] M) :
      R)
    (((dualDistrib R M N : (a : Dual R M ⊗[R] Dual R N) → Dual R (M ⊗[R] N))
            ((TensorProduct.comm R (Dual R N) (Dual R M) : (a : Dual R N ⊗[R] Dual R M) → Dual R M ⊗[R] Dual R N) 0) :
          (a : M ⊗[R] N) → R)
        (x + y) :
      R)

Tactic:
simp_all [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x : Dual R N
y : Dual R M
⊢ Eq.{u_1 + 1} (α := R)
    ((((dualDistrib R N M : (a : Dual R N ⊗[R] Dual R M) → Dual R (N ⊗[R] M)) (x ⊗ₜ[R] y) : Dual R (N ⊗[R] M)) :
          (a : N ⊗[R] M) → R)
        ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) 0) :
      R)
    ((((dualDistrib R M N : (a : Dual R M ⊗[R] Dual R N) → Dual R (M ⊗[R] N))
              ((TensorProduct.comm R (Dual R N) (Dual R M) : (a : Dual R N ⊗[R] Dual R M) → Dual R M ⊗[R] Dual R N)
                (x ⊗ₜ[R] y)) :
            Dual R (M ⊗[R] N)) :
          (a : M ⊗[R] N) → R)
        0 :
      R)

Tactic:
simp_all [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x : Dual R N
y : Dual R M
x_1 : M
y_1 : N
⊢ Eq.{u_1 + 1} (α := R)
    ((((dualDistrib R N M : (a : Dual R N ⊗[R] Dual R M) → Dual R (N ⊗[R] M)) (x ⊗ₜ[R] y) : Dual R (N ⊗[R] M)) :
          (a : N ⊗[R] M) → R)
        ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) (x_1 ⊗ₜ[R] y_1) : N ⊗[R] M) :
      R)
    ((((dualDistrib R M N : (a : Dual R M ⊗[R] Dual R N) → Dual R (M ⊗[R] N))
              ((TensorProduct.comm R (Dual R N) (Dual R M) : (a : Dual R N ⊗[R] Dual R M) → Dual R M ⊗[R] Dual R N)
                (x ⊗ₜ[R] y)) :
            Dual R (M ⊗[R] N)) :
          (a : M ⊗[R] N) → R)
        (x_1 ⊗ₜ[R] y_1) :
      R)

Tactic:
simp_all [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x : Dual R N
y : Dual R M
x_1 y_1 : M ⊗[R] N
h :
  Eq.{u_1 + 1} (α := R)
    ((((dualDistrib R N M : (a : Dual R N ⊗[R] Dual R M) → Dual R (N ⊗[R] M)) (x ⊗ₜ[R] y) : Dual R (N ⊗[R] M)) :
          (a : N ⊗[R] M) → R)
        ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) x_1 : N ⊗[R] M) :
      R)
    ((((dualDistrib R M N : (a : Dual R M ⊗[R] Dual R N) → Dual R (M ⊗[R] N))
              ((TensorProduct.comm R (Dual R N) (Dual R M) : (a : Dual R N ⊗[R] Dual R M) → Dual R M ⊗[R] Dual R N)
                (x ⊗ₜ[R] y)) :
            Dual R (M ⊗[R] N)) :
          (a : M ⊗[R] N) → R)
        x_1 :
      R)
h_1 :
  Eq.{u_1 + 1} (α := R)
    ((((dualDistrib R N M : (a : Dual R N ⊗[R] Dual R M) → Dual R (N ⊗[R] M)) (x ⊗ₜ[R] y) : Dual R (N ⊗[R] M)) :
          (a : N ⊗[R] M) → R)
        ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) y_1 : N ⊗[R] M) :
      R)
    ((((dualDistrib R M N : (a : Dual R M ⊗[R] Dual R N) → Dual R (M ⊗[R] N))
              ((TensorProduct.comm R (Dual R N) (Dual R M) : (a : Dual R N ⊗[R] Dual R M) → Dual R M ⊗[R] Dual R N)
                (x ⊗ₜ[R] y)) :
            Dual R (M ⊗[R] N)) :
          (a : M ⊗[R] N) → R)
        y_1 :
      R)
⊢ Eq.{u_1 + 1} (α := R)
    ((((dualDistrib R N M : (a : Dual R N ⊗[R] Dual R M) → Dual R (N ⊗[R] M)) (x ⊗ₜ[R] y) : Dual R (N ⊗[R] M)) :
          (a : N ⊗[R] M) → R)
        ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) (x_1 + y_1) : N ⊗[R] M) :
      R)
    ((((dualDistrib R M N : (a : Dual R M ⊗[R] Dual R N) → Dual R (M ⊗[R] N))
              ((TensorProduct.comm R (Dual R N) (Dual R M) : (a : Dual R N ⊗[R] Dual R M) → Dual R M ⊗[R] Dual R N)
                (x ⊗ₜ[R] y)) :
            Dual R (M ⊗[R] N)) :
          (a : M ⊗[R] N) → R)
        (x_1 + y_1) :
      R)

Tactic:
simp_all [mul_comm]

Premises used: mul_comm