awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst_5 : IsReflexive K V₂
⊢ B.ker.dualAnnihilator = B.flip.range
have change : B.ker.dualAnnihilator = (B.dualMap ∘ₗ (↑(evalEquiv K V₂) : V₂ →ₗ[K] Dual K (Dual K V₂))).range
Tactic: change _ = range (B.dualMap.comp (Module.evalEquiv K V₂).toLinearMap)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst_5 : IsReflexive K V₂
⊢ B.ker.dualAnnihilator = (B.dualMap ∘ₗ (↑(evalEquiv K V₂) : V₂ →ₗ[K] Dual K (Dual K V₂))).range
have rw : B.dualMap.range = (B.dualMap ∘ₗ (↑(evalEquiv K V₂) : V₂ →ₗ[K] Dual K (Dual K V₂))).range
Tactic: rw [← range_dualMap_eq_dualAnnihilator_ker, range_comp_of_range_eq_top _ (LinearEquiv.range _)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst_5 : IsReflexive K V₂
rw : B.dualMap.range = (B.dualMap ∘ₗ (↑(evalEquiv K V₂) : V₂ →ₗ[K] Dual K (Dual K V₂))).range
⊢ B.ker.dualAnnihilator = (B.dualMap ∘ₗ (↑(evalEquiv K V₂) : V₂ →ₗ[K] Dual K (Dual K V₂))).range
have rw₁ : B.dualMap.range = B.dualMap.range
Tactic: rw [← range_dualMap_eq_dualAnnihilator_ker, range_comp_of_range_eq_top _ (LinearEquiv.range _)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst_5 : FiniteDimensional K V₁
⊢ Injective (α := V₂) (β := V₁ →ₗ[K] K) (⇑B.flip : (a : V₂) → V₁ →ₗ[K] K) ↔
    Surjective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K)
have rw : Surjective (α := V₁) (β := Dual K V₂)
    (Function.comp (β := Dual K (Dual K V₁)) (⇑B.flip.dualMap : (a : Dual K (V₁ →ₗ[K] K)) → Dual K V₂)
      (⇑(LinearEquiv.toEquiv (evalEquiv K V₁)) : (a : V₁) → Dual K (Dual K V₁))) ↔
  Surjective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K)
Tactic: rw [← dualMap_surjective_iff, ← (evalEquiv K V₁).toEquiv.surjective_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst_5 : FiniteDimensional K V₂
⊢ Injective (α := V₂) (β := V₁ →ₗ[K] K) (⇑B.flip : (a : V₂) → V₁ →ₗ[K] K) ↔
    Surjective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K)
have rw : Injective (α := V₂) (β := V₁ →ₗ[K] K) (⇑B.flip : (a : V₂) → V₁ →ₗ[K] K) ↔
  Injective (α := Dual K (V₂ →ₗ[K] K)) (β := Dual K V₁) (⇑B.dualMap : (a : Dual K (V₂ →ₗ[K] K)) → Dual K V₁)
Tactic: rw [← dualMap_injective_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst_5 : FiniteDimensional K V₁
⊢ Bijective (α := V₂) (β := V₁ →ₗ[K] K) (⇑B.flip : (a : V₂) → V₁ →ₗ[K] K) ↔
    Bijective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K)
have simp_rw : Injective (α := V₂) (β := V₁ →ₗ[K] K) (⇑B.flip : (a : V₂) → V₁ →ₗ[K] K) ∧
    Surjective (α := V₂) (β := V₁ →ₗ[K] K) (⇑B.flip : (a : V₂) → V₁ →ₗ[K] K) ↔
  Injective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K) ∧
    Surjective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K)
Tactic: simp_rw [Bijective, flip_injective_iff₁, flip_surjective_iff₁, and_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst_5 : FiniteDimensional K V₁
simp_rw :
  Injective (α := V₂) (β := V₁ →ₗ[K] K) (⇑B.flip : (a : V₂) → V₁ →ₗ[K] K) ∧
      Surjective (α := V₂) (β := V₁ →ₗ[K] K) (⇑B.flip : (a : V₂) → V₁ →ₗ[K] K) ↔
    Injective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K) ∧
      Surjective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K)
⊢ Bijective (α := V₂) (β := V₁ →ₗ[K] K) (⇑B.flip : (a : V₂) → V₁ →ₗ[K] K) ↔
    Bijective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K)
have simp_rw₁ : Surjective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K) ∧
    Surjective (α := V₂) (β := V₁ →ₗ[K] K) (⇑B.flip : (a : V₂) → V₁ →ₗ[K] K) ↔
  Injective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K) ∧
    Surjective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K)
Tactic: simp_rw [Bijective, flip_injective_iff₁, flip_surjective_iff₁, and_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst : Field K
inst_1 : AddCommGroup V₁
inst_2 : Module K V₁
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst_5 : FiniteDimensional K V₁
simp_rw :
  Injective (α := V₂) (β := V₁ →ₗ[K] K) (⇑B.flip : (a : V₂) → V₁ →ₗ[K] K) ∧
      Surjective (α := V₂) (β := V₁ →ₗ[K] K) (⇑B.flip : (a : V₂) → V₁ →ₗ[K] K) ↔
    Injective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K) ∧
      Surjective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K)
simp_rw₁ :
  Surjective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K) ∧
      Surjective (α := V₂) (β := V₁ →ₗ[K] K) (⇑B.flip : (a : V₂) → V₁ →ₗ[K] K) ↔
    Injective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K) ∧
      Surjective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K)
⊢ Bijective (α := V₂) (β := V₁ →ₗ[K] K) (⇑B.flip : (a : V₂) → V₁ →ₗ[K] K) ↔
    Bijective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K)
have simp_rw₂ : Surjective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K) ∧
    Injective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K) ↔
  Injective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K) ∧
    Surjective (α := V₁) (β := V₂ →ₗ[K] K) (⇑B : (a : V₁) → V₂ →ₗ[K] K)
Tactic: simp_rw [Bijective, flip_injective_iff₁, flip_surjective_iff₁, and_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
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
⊢ (dualAnnihilator W).dualAnnihilator = map (σ₁₂ := RingHom.id K) (Dual.eval K V) W
have this : FiniteDimensional K (Dual K V ⧸ dualAnnihilator W)
Tactic: haveI := e1.finiteDimensional
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
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
⊢ (dualAnnihilator W).dualAnnihilator = map (σ₁₂ := RingHom.id K) (Dual.eval K V) W
have this₁ : FiniteDimensional K ↥(dualAnnihilator W).dualAnnihilator
Tactic: haveI := LinearEquiv.finiteDimensional (V₂ := W.dualAnnihilator.dualAnnihilator) e2
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
⊢ (dualAnnihilator W).dualAnnihilator = map (σ₁₂ := RingHom.id K) (Dual.eval K V) W
have rw : finrank K ↥(map (σ₁₂ := RingHom.id K) (Dual.eval K V) W) = finrank K ↥(dualAnnihilator W).dualAnnihilator
Tactic: rw [eq_of_le_of_finrank_eq (map_le_dualAnnihilator_dualAnnihilator W)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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 ↥(map (σ₁₂ := RingHom.id K) (Dual.eval K V) W) = finrank K ↥(dualAnnihilator W).dualAnnihilator
have rw : finrank K (Dual K V ⧸ dualAnnihilator W) = finrank K ↥(dualAnnihilator W).dualAnnihilator
Tactic: rw [← (equivMapOfInjective _ (eval_apply_injective K (V := V)) W).finrank_eq, e1.finrank_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
⊢ map (Dual.eval K V) (dualCoannihilator W) = dualAnnihilator W
have rw : (dualCoannihilator W).dualAnnihilator.dualAnnihilator = dualAnnihilator W
Tactic: rw [← dualAnnihilator_dualAnnihilator_eq_map, dualCoannihilator_dualAnnihilator_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
⊢ map (Dual.eval K V) (dualCoannihilator W) = dualAnnihilator W
have rw₁ : Eq (α := Submodule K (Dual K (Dual K V))) (dualAnnihilator W) (dualAnnihilator W)
Tactic: rw [← dualAnnihilator_dualAnnihilator_eq_map, dualCoannihilator_dualAnnihilator_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
ι : Type u_1
α : Type u_2
F : Type u_3
inst : Finite ι
inst_1 : Field F
f : ι → α → F
⊢ Eq (α := Submodule F (ι → F)) (span F (Set.range (flip f))) ⊤ ↔ LinearIndependent F f
have 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)) ⊥
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
ι : Type u_1
α : Type u_2
F : Type u_3
inst : Finite ι
inst_1 : Field F
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)) ⊥
have 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)
Tactic: congr!
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
ι : Type u_1
α : Type u_2
F : Type u_3
inst : Finite ι
inst_1 : Field F
f : ι → α → 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)
have 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))
Tactic: rw [SetLike.ext'_iff, map_span, Submodule.coe_dualCoannihilator_span, ← Set.range_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
ι : Type u_1
α : Type u_2
F : Type u_3
inst : Finite ι
inst_1 : Field F
f : ι → α → 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))
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
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
⊢ ∃ (f : Dual K V), ∀ i ∈ s, Eq.{u_2 + 1} (α := K) ((f : (a : V) → K) (v i) : K) (1 : K)
have hli₁ : LinearIndepOn K id (v '' s)
Tactic: replace hli : LinearIndepOn K id (v '' s) := LinearIndepOn.id_image hli
Cleared hypotheses: hli
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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)
have refine : ∀ (i : ι) (hi : i ∈ s),
  Eq.{u_2 + 1} (α := K) (((b.constr K : (a : (↑(hli.extend sorry) : Type u_3) → K) → V →ₗ[K] K) 1 : (a : V) → K) (v i) : K)
    (1 : K)
Tactic: refine ⟨b.constr K 1, fun i hi ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
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
⊢ 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)
have hi₁ : v i ∈ LinearIndepOn.extend.{u_3, u_3, u_2} (K := K) (V := V) (v := id) (s := v '' s) (t := Set.univ) hli sorry
Tactic: replace hi : v i ∈ hli.extend (Set.subset_univ _) :=
    hli.subset_extend _ <| Set.mem_image_of_mem v hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
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
⊢ 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)
have this : (b : (a : (↑(hli.extend sorry) : Type u_3)) → V) ri = v i
Tactic: have : b ri = v i := by simp [b, ri]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
w : Dual R N ⊗[R] Dual R M
z : M ⊗[R] N
⊢ Eq.{u_1 + 1} (α := R)
    ((((dualDistrib R N M : (a : Dual R N ⊗[R] Dual R M) → Dual R (N ⊗[R] M)) w : Dual R (N ⊗[R] M)) :
          (a : N ⊗[R] M) → R)
        ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) z : 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) w) :
            Dual R (M ⊗[R] N)) :
          (a : M ⊗[R] N) → R)
        z :
      R)
have zero : 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) z : 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)
      z :
    R)
Tactic: induction w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
w : Dual R N ⊗[R] Dual R M
z : M ⊗[R] N
zero :
  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) z : 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)
        z :
      R)
⊢ Eq.{u_1 + 1} (α := R)
    ((((dualDistrib R N M : (a : Dual R N ⊗[R] Dual R M) → Dual R (N ⊗[R] M)) w : Dual R (N ⊗[R] M)) :
          (a : N ⊗[R] M) → R)
        ((TensorProduct.comm R M N : (a : M ⊗[R] N) → N ⊗[R] M) z : 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) w) :
            Dual R (M ⊗[R] N)) :
          (a : M ⊗[R] N) → R)
        z :
      R)
have tmul : ∀ (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) z : 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)
        z :
      R)
Tactic: induction w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
z : M ⊗[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) z : 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)
        z :
      R)
have zero : 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: induction z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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
z : M ⊗[R] N
zero :
  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)
⊢ 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) z : 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)
        z :
      R)
have zero₁ : ∀ (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: induction z
Cleared hypotheses: z