awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := BilinForm R M ≃ₗ[R] BilinForm R M) (flipHom ≪≫ₗ flipHom) (LinearEquiv.refl R (BilinForm R M))
have h : ∀ (A : BilinForm R M) (x y : M),
  Eq.{u_1 + 1} (α := R)
    ((((((flipHom ≪≫ₗ flipHom : (a : BilinForm R M) → BilinForm R M) A : BilinForm R M) : (a : M) → M →ₗ[R] R) x :
            M →ₗ[R] R) :
          (a : M) → R)
        y :
      R)
    ((((((LinearEquiv.refl R (BilinForm R M) : (a : BilinForm R M) → BilinForm R M) A : BilinForm R M) :
                (a : M) → M →ₗ[R] R)
              x :
            M →ₗ[R] R) :
          (a : M) → R)
        y :
      R)
Tactic: ext A
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
N : Submodule R M
y : M
h : y ∈ N
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Submodule R S) 1 (((B : (a : M) → M →ₗ[S] S) 0 : (a : M) → S) y : S)
have rw : Membership.mem (γ := Submodule R S) 1 0
Tactic: rw [B.zero_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
N : Submodule R M
r : R
a : M
ha :
  Membership.mem (γ := Set M)
    {x : M |
      ∀ y ∈ N,
        Membership.mem.{u_2, u_2} (α := S) (γ := Submodule R S) 1
          ((((B : (a : M) → M →ₗ[S] S) x : M →ₗ[S] S) : (a : M) → S) y : S)}
    a
y : M
hy : y ∈ N
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Submodule R S) 1
    ((((B : (a : M) → M →ₗ[S] S) (r • a) : M →ₗ[S] S) : (a : M) → S) y : S)
have h : (((B : (a : M) → M →ₗ[S] S) (r • a) : M →ₗ[S] S) : (a : M) → S) y =
  HSMul.hSMul (β := S) r ((((B : (a : M) → M →ₗ[S] S) a : M →ₗ[S] S) : (a : M) → S) y : S)
Tactic: convert! (1 : Submodule R S).smul_mem r (ha y hy)
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
N : Submodule R M
r : R
a : M
ha :
  Membership.mem (γ := Set M)
    {x : M |
      ∀ y ∈ N,
        Membership.mem.{u_2, u_2} (α := S) (γ := Submodule R S) 1
          ((((B : (a : M) → M →ₗ[S] S) x : M →ₗ[S] S) : (a : M) → S) y : S)}
    a
y : M
hy : y ∈ N
⊢ (((B : (a : M) → M →ₗ[S] S) (r • a) : M →ₗ[S] S) : (a : M) → S) y =
    HSMul.hSMul (β := S) r ((((B : (a : M) → M →ₗ[S] S) a : M →ₗ[S] S) : (a : M) → S) y : S)
have h : (((B : (a : M) → M →ₗ[S] S) (HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) r : S) a) :
        M →ₗ[S] S) :
      (a : M) → S)
    y =
  HSMul.hSMul (β := S) r ((((B : (a : M) → M →ₗ[S] S) a : M →ₗ[S] S) : (a : M) → S) y : S)
Tactic: rw [← IsScalarTower.algebraMap_smul S r a]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_1
S : Type u_3
M : Type u_2
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
N₁ N₂ : Submodule R M
⊢ (∀ x ∈ N₁, x ∈ B.flip.dualSubmodule N₂) ↔ ∀ x ∈ N₂, x ∈ B.dualSubmodule N₁
have simp : (∀ x ∈ N₁,
    ∀ y ∈ N₂,
      ∃ (y_1 : R),
        Eq.{u_3 + 1} (α := S) ((algebraMap R S : (a : R) → S) y_1 : S)
          ((((B : (a : M) → M →ₗ[S] S) y : M →ₗ[S] S) : (a : M) → S) x : S)) ↔
  ∀ x ∈ N₂,
    ∀ y ∈ N₁,
      ∃ (y_1 : R),
        Eq.{u_3 + 1} (α := S) ((algebraMap R S : (a : R) → S) y_1 : S)
          ((((B : (a : M) → M →ₗ[S] S) x : M →ₗ[S] S) : (a : M) → S) y : S)
Tactic: simp only [mem_dualSubmodule, Submodule.mem_one, flip_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
inst_7 : IsDomain R
hB : B.Nondegenerate
inst_8 : IsTorsionFree R S
N : Submodule R M
hN : Eq (α := Submodule S M) (Submodule.span S (↑N : Set M)) ⊤
x y : ↥(B.dualSubmodule N)
e :
  Eq (α := Dual.{u_1, u_3} R ↥N)
    ((B.dualSubmoduleToDual N : (a : ↥(B.dualSubmodule N)) → Dual R ↥N) x : Dual.{u_1, u_3} R ↥N)
    ((B.dualSubmoduleToDual N : (a : ↥(B.dualSubmodule N)) → Dual R ↥N) y : Dual.{u_1, u_3} R ↥N)
⊢ x = y
have a : (↑x : M) = (↑y : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
inst_7 : IsDomain R
hB : B.Nondegenerate
inst_8 : IsTorsionFree R S
N : Submodule R M
hN : Eq (α := Submodule S M) (Submodule.span S (↑N : Set M)) ⊤
x y : ↥(B.dualSubmodule N)
e :
  Eq (α := Dual.{u_1, u_3} R ↥N)
    ((B.dualSubmoduleToDual N : (a : ↥(B.dualSubmodule N)) → Dual R ↥N) x : Dual.{u_1, u_3} R ↥N)
    ((B.dualSubmoduleToDual N : (a : ↥(B.dualSubmodule N)) → Dual R ↥N) y : Dual.{u_1, u_3} R ↥N)
⊢ (↑x : M) = (↑y : M)
have a : Eq (α := M →ₗ[S] S) ((B : (a : M) → M →ₗ[S] S) (↑x : M) : M →ₗ[S] S) ((B : (a : M) → M →ₗ[S] S) (↑y : M) : M →ₗ[S] S)
Tactic: apply LinearMap.ker_eq_bot.mp hB.ker_eq_bot
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
inst_7 : IsDomain R
hB : B.Nondegenerate
inst_8 : IsTorsionFree R S
N : Submodule R M
hN : Eq (α := Submodule S M) (Submodule.span S (↑N : Set M)) ⊤
x y : ↥(B.dualSubmodule N)
e :
  Eq (α := Dual.{u_1, u_3} R ↥N)
    ((B.dualSubmoduleToDual N : (a : ↥(B.dualSubmodule N)) → Dual R ↥N) x : Dual.{u_1, u_3} R ↥N)
    ((B.dualSubmoduleToDual N : (a : ↥(B.dualSubmodule N)) → Dual R ↥N) y : Dual.{u_1, u_3} R ↥N)
⊢ Eq (α := M →ₗ[S] S) ((B : (a : M) → M →ₗ[S] S) (↑x : M) : M →ₗ[S] S) ((B : (a : M) → M →ₗ[S] S) (↑y : M) : M →ₗ[S] S)
have a : Set.EqOn.{u_3, u_2} (β := S) (⇑((B : (a : M) → M →ₗ[S] S) (↑x : M) : M →ₗ[S] S) : (a : M) → S)
  (⇑((B : (a : M) → M →ₗ[S] S) (↑y : M) : M →ₗ[S] S) : (a : M) → S) (↑N : Set M)
Tactic: apply LinearMap.ext_on hN
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
inst_8 : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
⊢ Eq (α := Submodule R M) (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
have intro : ∀ (val : Fintype ι),
  Eq (α := Submodule R M) (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
inst_8 : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val : Fintype ι
⊢ Eq (α := Submodule R M) (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
have intro : LE.le (α := Submodule R M) (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))))
  (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
inst_8 : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val : Fintype ι
intro :
  LE.le (α := Submodule R M) (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
⊢ Eq (α := Submodule R M) (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
have intro₁ : LE.le (α := Submodule R M) (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
  (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
inst_8 : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val : Fintype ι
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))) x
⊢ Membership.mem (γ := Submodule R M)
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M))) x
have intro : Membership.mem (γ := Submodule R M)
  (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
  (∑ i : ι,
    HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := M)
      (((((B.dualBasis hB b).repr : (a : M) → ι →₀ S) x : ι →₀ S) : (a : ι) → S) i : S)
      ((B.dualBasis hB b : (a : ι) → M) i : M))
Tactic: rw [← (B.dualBasis hB b).sum_repr x]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
inst_8 : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val : Fintype ι
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))) x
⊢ Membership.mem (γ := Submodule R M)
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
    (∑ i : ι,
      HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := M)
        (((((B.dualBasis hB b).repr : (a : M) → ι →₀ S) x : ι →₀ S) : (a : ι) → S) i : S)
        ((B.dualBasis hB b : (a : ι) → M) i : M))
have intro : ∀ (c : ι),
  Membership.mem (γ := Finset ι) Finset.univ c →
    Membership.mem (γ := Submodule R M)
      (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
      (HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := M)
        (((((B.dualBasis hB b).repr : (a : M) → ι →₀ S) x : ι →₀ S) : (a : ι) → S) c : S)
        ((B.dualBasis hB b : (a : ι) → M) c : M))
Tactic: apply sum_mem
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
inst_8 : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val : Fintype ι
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))) x
i : ι
⊢ Membership.mem (γ := Submodule R M)
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
    (HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := M)
      (((((B.dualBasis hB b).repr : (a : M) → ι →₀ S) x : ι →₀ S) : (a : ι) → S) i : S)
      ((B.dualBasis hB b : (a : ι) → M) i : M))
have intro : ∀ (r : R)
  (hr :
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) r : S)
      ((((B : (a : M) → M →ₗ[S] S) x : M →ₗ[S] S) : (a : M) → S) ((b : (a : ι) → M) i : M) : S)),
  Membership.mem (γ := Submodule R M)
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
    (HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := M)
      (((((B.dualBasis hB b).repr : (a : M) → ι →₀ S) x : ι →₀ S) : (a : ι) → S) i : S)
      ((B.dualBasis hB b : (a : ι) → M) i : M))
Tactic: obtain ⟨r, hr⟩ := Submodule.mem_one.mp <| hx (b i) (Submodule.subset_span ⟨_, rfl⟩)
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
inst_8 : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val : Fintype ι
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))) x
i : ι
r : R
hr :
  Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) r : S)
    ((((B : (a : M) → M →ₗ[S] S) x : M →ₗ[S] S) : (a : M) → S) ((b : (a : ι) → M) i : M) : S)
⊢ Membership.mem (γ := Submodule R M)
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
    (HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := M)
      (((((B.dualBasis hB b).repr : (a : M) → ι →₀ S) x : ι →₀ S) : (a : ι) → S) i : S)
      ((B.dualBasis hB b : (a : ι) → M) i : M))
have intro : Membership.mem (γ := Submodule R M)
  (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
  (HSMul.hSMul (β := M) r ((B.dualBasis hB b : (a : ι) → M) i : M))
Tactic: simp only [dualBasis_repr_apply, ← hr, algebraMap_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
inst_8 : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val : Fintype ι
x : M
hx :
  Membership.mem (γ := Submodule R M)
    (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))) x
i : ι
r : R
hr :
  Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) r : S)
    ((((B : (a : M) → M →ₗ[S] S) x : M →ₗ[S] S) : (a : M) → S) ((b : (a : ι) → M) i : M) : S)
⊢ Membership.mem (γ := Submodule R M)
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
    (HSMul.hSMul (β := M) r ((B.dualBasis hB b : (a : ι) → M) i : M))
have intro : Membership.mem.{u_3, u_3} (α := M) (γ := Submodule R M)
  (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
  ((B.dualBasis hB b : (a : ι) → M) i : M)
Tactic: apply Submodule.smul_mem
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
inst_8 : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val : Fintype ι
⊢ LE.le (α := Submodule R M) (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M)))
    (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))))
have intro : Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.dualBasis hB b) : (a : ι) → M) ⊆
  (↑(B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))) : Set M)
Tactic: rw [Submodule.span_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
inst_8 : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val : Fintype ι
i : ι
y : M
hy : Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))) y
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Submodule R S) 1
    ((((B : (a : M) → M →ₗ[S] S) ((B.dualBasis hB b : (a : ι) → M) i) : M →ₗ[S] S) : (a : M) → S) y : S)
have intro : ∀ (f : ι → R)
  (hy :
    Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
      (∑ i : ι, HSMul.hSMul (β := M) (f i) ((b : (a : ι) → M) i : M))),
  Membership.mem.{u_2, u_2} (α := S) (γ := Submodule R S) 1
    ((((B : (a : M) → M →ₗ[S] S) ((B.dualBasis hB b : (a : ι) → M) i) : M →ₗ[S] S) : (a : M) → S)
        (∑ i : ι, HSMul.hSMul (β := M) (f i) ((b : (a : ι) → M) i : M)) :
      S)
Tactic: obtain ⟨f, rfl⟩ := (Submodule.mem_span_range_iff_exists_fun _).mp hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
inst_8 : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val : Fintype ι
i : ι
f : ι → R
hy :
  Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    (∑ i : ι, HSMul.hSMul (β := M) (f i) ((b : (a : ι) → M) i : M))
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Submodule R S) 1
    ((((B : (a : M) → M →ₗ[S] S) ((B.dualBasis hB b : (a : ι) → M) i) : M →ₗ[S] S) : (a : M) → S)
        (∑ i : ι, HSMul.hSMul (β := M) (f i) ((b : (a : ι) → M) i : M)) :
      S)
have intro : Membership.mem (γ := Submodule R S) 1
  (∑ x : ι,
    (((B : (a : M) → M →ₗ[S] S) ((B.dualBasis hB b : (a : ι) → M) i) : M →ₗ[S] S) : (a : M) → S)
      (HSMul.hSMul (β := M) (f x) ((b : (a : ι) → M) x : M)))
Tactic: simp only [map_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
inst_8 : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val : Fintype ι
i : ι
f : ι → R
hy :
  Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    (∑ i : ι, HSMul.hSMul (β := M) (f i) ((b : (a : ι) → M) i : M))
⊢ Membership.mem (γ := Submodule R S) 1
    (∑ x : ι,
      (((B : (a : M) → M →ₗ[S] S) ((B.dualBasis hB b : (a : ι) → M) i) : M →ₗ[S] S) : (a : M) → S)
        (HSMul.hSMul (β := M) (f x) ((b : (a : ι) → M) x : M)))
have intro : ∀ (c : ι),
  Membership.mem (γ := Finset ι) Finset.univ c →
    Membership.mem.{u_2, u_2} (α := S) (γ := Submodule R S) 1
      ((((B : (a : M) → M →ₗ[S] S) ((B.dualBasis hB b : (a : ι) → M) i) : M →ₗ[S] S) : (a : M) → S)
          (HSMul.hSMul (β := M) (f c) ((b : (a : ι) → M) c : M)) :
        S)
Tactic: apply sum_mem
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
inst_8 : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val : Fintype ι
i : ι
f : ι → R
hy :
  Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    (∑ i : ι, HSMul.hSMul (β := M) (f i) ((b : (a : ι) → M) i : M))
j : ι
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Submodule R S) 1
    ((((B : (a : M) → M →ₗ[S] S) ((B.dualBasis hB b : (a : ι) → M) i) : M →ₗ[S] S) : (a : M) → S)
        (HSMul.hSMul (β := M) (f j) ((b : (a : ι) → M) j : M)) :
      S)
have intro : Membership.mem (γ := Submodule R S) 1
  (HSMul.hSMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (f j) : S)
    ((((B : (a : M) → M →ₗ[S] S) ((B.dualBasis hB b : (a : ι) → M) i) : M →ₗ[S] S) : (a : M) → S)
        ((b : (a : ι) → M) j : M) :
      S))
Tactic: rw [← IsScalarTower.algebraMap_smul S (f j), map_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
inst_8 : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val : Fintype ι
i : ι
f : ι → R
hy :
  Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    (∑ i : ι, HSMul.hSMul (β := M) (f i) ((b : (a : ι) → M) i : M))
j : ι
⊢ Membership.mem (γ := Submodule R S) 1
    (HSMul.hSMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (f j) : S)
      ((((B : (a : M) → M →ₗ[S] S) ((B.dualBasis hB b : (a : ι) → M) i) : M →ₗ[S] S) : (a : M) → S)
          ((b : (a : ι) → M) j : M) :
        S))
have intro : Membership.mem (γ := Submodule R S) 1
  (HSMul.hSMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (f j) : S) (if j = i then 1 else 0))
Tactic: simp_rw [apply_dualBasis_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
inst_8 : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val : Fintype ι
i : ι
f : ι → R
hy :
  Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
    (∑ i : ι, HSMul.hSMul (β := M) (f i) ((b : (a : ι) → M) i : M))
j : ι
⊢ Membership.mem (γ := Submodule R S) 1
    (HSMul.hSMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (f j) : S) (if j = i then 1 else 0))
have intro : Membership.mem.{u_2, u_2} (α := S) (γ := Submodule R S) 1
  ((algebraMap R S : (a : R) → S) (if j = i then f j else 0) : S)
Tactic: rw [smul_eq_mul, mul_ite, mul_one, mul_zero, ← (algebraMap R S).map_zero, ← apply_ite]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.DualLattice (goal)
Goal:
R : Type u_4
S : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : Field S
inst_2 : AddCommGroup M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst_7 : Finite ι
hB : B.Nondegenerate
b : Basis ι S M
this : FiniteDimensional S M := ⋯
⊢ Eq (α := Submodule R M)
    (B.dualSubmodule (B.flip.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))))
    (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
have rw : Eq (α := Submodule R M)
  (B.dualSubmodule (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑(B.flip.dualBasis sorry b) : (a : ι) → M))))
  (Submodule.span R (Set.range.{u_3, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
Tactic: rw [dualSubmodule_span_of_basis _ hB.flip, dualSubmodule_span_of_basis B hB,
    dualBasis_dualBasis_flip hB]