awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
H₂ : LE.le (α := Submodule K V) ⊤ (span K n)
b : Basis (↑n : Type u_7) K V := Basis.mk H₁ ⋯
i : (↑n : Type u_7) := Subtype.mk (p := fun (x : V) ↦ x ∈ n) v ⋯
hi : (b : (a : (↑n : Type u_7)) → V) i = v
j : (↑n : Type u_7)
h : i = j
⊢ Eq.{u_6 + 1} (α := K) ((f : (a : V) → K) ((b : (a : (↑n : Type u_7)) → V) j : V) : K)
    ((HSMul.hSMul (α := K) ((f : (a : V) → K) ((b : (a : (↑n : Type u_7)) → V) i : V) : K) (b.coord i) : (a : V) → K)
        ((b : (a : (↑n : Type u_7)) → V) j : V) :
      K)

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
H₂ : LE.le (α := Submodule K V) ⊤ (span K n)
b : Basis (↑n : Type u_7) K V := Basis.mk H₁ ⋯
i : (↑n : Type u_7) := Subtype.mk (p := fun (x : V) ↦ x ∈ n) v ⋯
hi : (b : (a : (↑n : Type u_7)) → V) i = v
j : (↑n : Type u_7)
h : ¬i = j
this : Eq.{u_6 + 1} (α := K) ((f : (a : V) → K) ((b : (a : (↑n : Type u_7)) → V) j : V) : K) (0 : K)
⊢ Eq.{u_6 + 1} (α := K) ((f : (a : V) → K) ((b : (a : (↑n : Type u_7)) → V) j : V) : K)
    ((HSMul.hSMul (α := K) ((f : (a : V) → K) ((b : (a : (↑n : Type u_7)) → V) i : V) : K) (b.coord i) : (a : V) → K)
        ((b : (a : (↑n : Type u_7)) → V) j : V) :
      K)

Tactic:
simp [Finsupp.single_eq_of_ne h, this]

Premises used: Finsupp.single_eq_of_ne
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
H₂ : LE.le (α := Submodule K V) ⊤ (span K n)
b : Basis (↑n : Type u_7) K V := Basis.mk H₁ ⋯
i : (↑n : Type u_7) := Subtype.mk (p := fun (x : V) ↦ x ∈ n) v ⋯
hi : (b : (a : (↑n : Type u_7)) → V) i = v
j : (↑n : Type u_7)
h : ¬i = j
neg : Eq.{u_6 + 1} (α := K) ((f : (a : V) → K) ((b : (a : (↑n : Type u_7)) → V) j : V) : K) (0 : K)
⊢ Eq.{u_6 + 1} (α := K) ((f : (a : V) → K) ((b : (a : (↑n : Type u_7)) → V) j : V) : K)
    ((HSMul.hSMul (α := K) ((f : (a : V) → K) ((b : (a : (↑n : Type u_7)) → V) i : V) : K) (b.coord i) : (a : V) → K)
        ((b : (a : (↑n : Type u_7)) → V) j : V) :
      K)

Tactic:
suffices f (b j) = 0 by
      simp [Finsupp.single_eq_of_ne h, this]
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
H₂ : LE.le (α := Submodule K V) ⊤ (span K n)
b : Basis (↑n : Type u_7) K V := Basis.mk H₁ ⋯
i : (↑n : Type u_7) := Subtype.mk (p := fun (x : V) ↦ x ∈ n) v ⋯
hi : (b : (a : (↑n : Type u_7)) → V) i = v
j : (↑n : Type u_7)
h : ¬i = j
neg : Membership.mem (γ := Submodule K V) (span K s) (_root_.id (↑j : V))
⊢ Eq.{u_6 + 1} (α := K) ((f : (a : V) → K) ((b : (a : (↑n : Type u_7)) → V) j : V) : K) (0 : K)

Tactic:
rw [← mem_ker, ← hs, Basis.coe_mk]

Premises used: LinearMap.mem_ker, Module.Basis.coe_mk
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
H₂ : LE.le (α := Submodule K V) ⊤ (span K n)
b : Basis (↑n : Type u_7) K V := Basis.mk H₁ ⋯
i : (↑n : Type u_7) := Subtype.mk (p := fun (x : V) ↦ x ∈ n) v ⋯
hi : (b : (a : (↑n : Type u_7)) → V) i = v
j : (↑n : Type u_7)
h : ¬i = j
neg : _root_.id (↑j : V) ∈ s
⊢ Membership.mem (γ := Submodule K V) (span K s) (_root_.id (↑j : V))

Tactic:
apply subset_span

Premises used: Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
H₂ : LE.le (α := Submodule K V) ⊤ (span K n)
b : Basis (↑n : Type u_7) K V := Basis.mk H₁ ⋯
i : (↑n : Type u_7) := Subtype.mk (p := fun (x : V) ↦ x ∈ n) v ⋯
hi : (b : (a : (↑n : Type u_7)) → V) i = v
j : (↑n : Type u_7)
h : ¬i = j
neg : ¬(↑j : V) = v
⊢ _root_.id (↑j : V) ∈ s

Tactic:
apply Or.resolve_left (Set.mem_insert_iff.mpr j.prop)

Premises used: Iff.mpr, Or.resolve_left, Subtype.prop, Set.mem_insert_iff
-- Module: Mathlib.LinearAlgebra.Basis.VectorSpace
Goal:
K : Type u_6
V : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : V →ₗ[K] K
v : V
hfv : Ne.{u_6 + 1} (α := K) ((f : (a : V) → K) v : K) (0 : K)
b₁ : Basis.{u_7, u_6, u_7} (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7) K ↥f.ker := Basis.ofVectorSpace K ↥f.ker
s : Set V :=
  image (α := ↥f.ker) (⇑f.ker.subtype : (a : ↥f.ker) → V)
    (Set.range (ι := (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7))
      (⇑b₁ : (a : (↑(Basis.ofVectorSpaceIndex K ↥f.ker) : Type u_7)) → ↥f.ker))
hs : span K s = f.ker
n : Set V := insert v s
H₁ : LinearIndepOn K _root_.id n
H₂ : LE.le (α := Submodule K V) ⊤ (span K n)
b : Basis (↑n : Type u_7) K V := Basis.mk H₁ ⋯
i : (↑n : Type u_7) := Subtype.mk (p := fun (x : V) ↦ x ∈ n) v ⋯
hi : (b : (a : (↑n : Type u_7)) → V) i = v
j : (↑n : Type u_7)
h : ¬i = j
⊢ ¬(↑j : V) = v

Tactic:
simp [← hi, b, Subtype.coe_inj, Ne.symm h]

Premises used: Subtype.coe_inj, Ne.symm
-- Module: Mathlib.LinearAlgebra.BilinearForm.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
x y z : M
⊢ (((B : (a : M) → M →ₗ[R] R) (x + y) : M →ₗ[R] R) : (a : M) → R) z =
    HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) z : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) z : R)

Tactic:
map_add₂ _ _ _ _

Premises used: LinearMap.map_add₂
-- Module: Mathlib.LinearAlgebra.BilinearForm.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
a : R
x y : M
⊢ (((B : (a : M) → M →ₗ[R] R) (a • x) : M →ₗ[R] R) : (a : M) → R) y =
    HMul.hMul (β := R) a ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)

Tactic:
map_smul₂ _ _ _ _

Premises used: LinearMap.map_smul₂
-- Module: Mathlib.LinearAlgebra.BilinearForm.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
x y z : M
⊢ (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) (y + z) =
    HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) z : R)

Tactic:
map_add _ _ _

Premises used: map_add
-- Module: Mathlib.LinearAlgebra.BilinearForm.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
a : R
x y : M
⊢ (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) (a • y) =
    HMul.hMul (β := R) a ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)

Tactic:
map_smul _ _ _

Premises used: map_smul
-- Module: Mathlib.LinearAlgebra.BilinearForm.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
x : M
⊢ Eq.{u_1 + 1} (α := R) (((B : (a : M) → M →ₗ[R] R) 0 : (a : M) → R) x : R) (0 : R)

Tactic:
map_zero₂ _ _

Premises used: LinearMap.map_zero₂
-- Module: Mathlib.LinearAlgebra.BilinearForm.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
x : M
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) 0 : R) (0 : R)

Tactic:
map_zero _

Premises used: map_zero
-- Module: Mathlib.LinearAlgebra.BilinearForm.Basic
Goal:
R₁ : Type u_4
M₁ : Type u_5
inst : CommRing R₁
inst_1 : AddCommGroup M₁
inst_2 : Module R₁ M₁
B₁ : BilinForm R₁ M₁
x y : M₁
⊢ Eq.{u_4 + 1} (α := R₁) ((((B₁ : (a : M₁) → M₁ →ₗ[R₁] R₁) (-x) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) y : R₁)
    (-(((B₁ : (a : M₁) → M₁ →ₗ[R₁] R₁) x : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) y : R₁)

Tactic:
map_neg₂ _ _ _

Premises used: LinearMap.map_neg₂
-- Module: Mathlib.LinearAlgebra.BilinearForm.Basic
Goal:
R₁ : Type u_4
M₁ : Type u_5
inst : CommRing R₁
inst_1 : AddCommGroup M₁
inst_2 : Module R₁ M₁
B₁ : BilinForm R₁ M₁
x y : M₁
⊢ Eq.{u_4 + 1} (α := R₁) ((((B₁ : (a : M₁) → M₁ →ₗ[R₁] R₁) x : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) (-y) : R₁)
    (-(((B₁ : (a : M₁) → M₁ →ₗ[R₁] R₁) x : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) y : R₁)

Tactic:
map_neg _ _

Premises used: map_neg
-- Module: Mathlib.LinearAlgebra.BilinearForm.Basic
Goal:
R₁ : Type u_4
M₁ : Type u_5
inst : CommRing R₁
inst_1 : AddCommGroup M₁
inst_2 : Module R₁ M₁
B₁ : BilinForm R₁ M₁
x y z : M₁
⊢ (((B₁ : (a : M₁) → M₁ →ₗ[R₁] R₁) (x - y) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) z =
    HSub.hSub (α := R₁) (β := R₁) ((((B₁ : (a : M₁) → M₁ →ₗ[R₁] R₁) x : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) z : R₁)
      ((((B₁ : (a : M₁) → M₁ →ₗ[R₁] R₁) y : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) z : R₁)

Tactic:
map_sub₂ _ _ _ _

Premises used: LinearMap.map_sub₂
-- Module: Mathlib.LinearAlgebra.BilinearForm.Basic
Goal:
R₁ : Type u_4
M₁ : Type u_5
inst : CommRing R₁
inst_1 : AddCommGroup M₁
inst_2 : Module R₁ M₁
B₁ : BilinForm R₁ M₁
x y z : M₁
⊢ (((B₁ : (a : M₁) → M₁ →ₗ[R₁] R₁) x : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) (y - z) =
    HSub.hSub (α := R₁) (β := R₁) ((((B₁ : (a : M₁) → M₁ →ₗ[R₁] R₁) x : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) y : R₁)
      ((((B₁ : (a : M₁) → M₁ →ₗ[R₁] R₁) x : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) z : R₁)

Tactic:
map_sub _ _ _

Premises used: map_sub
-- Module: Mathlib.LinearAlgebra.BilinearForm.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
B : BilinForm R M
r : S
x y : M
rw :
  (((B : (a : M) → M →ₗ[R] R) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((algebraMap S R : (a : S) → R) r : R) x) :
          M →ₗ[R] R) :
        (a : M) → R)
      y =
    HSMul.hSMul (β := R) r ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
rw₁ :
  HMul.hMul (α := R) (β := R) ((algebraMap S R : (a : S) → R) r : R)
      ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
    HSMul.hSMul (β := R) r ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
rw₂ rw₃ :
  HMul.hMul (α := R) (β := R) ((algebraMap S R : (a : S) → R) r : R)
      ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
    HMul.hMul (α := R) (β := R) ((algebraMap S R : (a : S) → R) r : R)
      ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
⊢ (((B : (a : M) → M →ₗ[R] R) (r • x) : M →ₗ[R] R) : (a : M) → R) y =
    HSMul.hSMul (β := R) r ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)

Tactic:
rw [← IsScalarTower.algebraMap_smul R r, smul_left, Algebra.smul_def]

Premises used: LinearMap.BilinForm.smul_left, IsScalarTower.algebraMap_smul, Algebra.smul_def
-- Module: Mathlib.LinearAlgebra.BilinearForm.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
B : BilinForm R M
r : S
x y : M
rw :
  (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((algebraMap S R : (a : S) → R) r : R) y) =
    HSMul.hSMul (β := R) r ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
rw₁ :
  HMul.hMul (α := R) (β := R) ((algebraMap S R : (a : S) → R) r : R)
      ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
    HSMul.hSMul (β := R) r ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
rw₂ rw₃ :
  HMul.hMul (α := R) (β := R) ((algebraMap S R : (a : S) → R) r : R)
      ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
    HMul.hMul (α := R) (β := R) ((algebraMap S R : (a : S) → R) r : R)
      ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
⊢ (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) (r • y) =
    HSMul.hSMul (β := R) r ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)

Tactic:
rw [← IsScalarTower.algebraMap_smul R r, smul_right, Algebra.smul_def]

Premises used: IsScalarTower.algebraMap_smul, LinearMap.BilinForm.smul_right, Algebra.smul_def
-- Module: Mathlib.LinearAlgebra.BilinearForm.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B D : BilinForm R M
h :
  Eq (α := (x y : M) → R)
    ((fun (B : BilinForm R M) (x y : M) ↦ ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)) B)
    ((fun (B : BilinForm R M) (x y : M) ↦ ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)) D)
h₁ :
  ∀ (x y : M),
    Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((D : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
⊢ B = D

Tactic:
ext x y
-- Module: Mathlib.LinearAlgebra.BilinearForm.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B D : BilinForm R M
h :
  Eq (α := (x y : M) → R)
    ((fun (B : BilinForm R M) (x y : M) ↦ ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)) B)
    ((fun (B : BilinForm R M) (x y : M) ↦ ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)) D)
x y : M
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
    ((((D : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)

Tactic:
apply congrFun₂ h

Premises used: congrFun₂
-- Module: Mathlib.LinearAlgebra.BilinearForm.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B D : BilinForm R M
H :
  ∀ (x y : M),
    Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((D : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
⊢ B = D

Tactic:
ext₂ H

Premises used: LinearMap.ext₂
-- Module: Mathlib.LinearAlgebra.BilinearForm.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B D : BilinForm R M
h : B = D
x y : M
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
    ((((D : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)

Tactic:
congr_fun₂ h _ _

Premises used: LinearMap.congr_fun₂
-- Module: Mathlib.LinearAlgebra.BilinearForm.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : M
⊢ Eq.{u_1 + 1} (α := R) ((((0 : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B D : BilinForm R M
x y : M
⊢ (((B + D : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y =
    HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((D : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Basic
Goal:
R₁ : Type u_4
M₁ : Type u_5
inst : CommRing R₁
inst_1 : AddCommGroup M₁
inst_2 : Module R₁ M₁
B₁ : BilinForm R₁ M₁
x y : M₁
⊢ Eq.{u_4 + 1} (α := R₁) ((((-B₁ : (a : M₁) → M₁ →ₗ[R₁] R₁) x : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) y : R₁)
    (-(((B₁ : (a : M₁) → M₁ →ₗ[R₁] R₁) x : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) y : R₁)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Basic
Goal:
R₁ : Type u_4
M₁ : Type u_5
inst : CommRing R₁
inst_1 : AddCommGroup M₁
inst_2 : Module R₁ M₁
B₁ D₁ : BilinForm R₁ M₁
x y : M₁
⊢ (((B₁ - D₁ : (a : M₁) → M₁ →ₗ[R₁] R₁) x : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) y =
    HSub.hSub (α := R₁) (β := R₁) ((((B₁ : (a : M₁) → M₁ →ₗ[R₁] R₁) x : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) y : R₁)
      ((((D₁ : (a : M₁) → M₁ →ₗ[R₁] R₁) x : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) y : R₁)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : BilinForm R M
x y : M
⊢ Eq.{u_1 + 1} (α := R)
    ((((((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)
    ((((A : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
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)
⊢ Eq (α := BilinForm R M ≃ₗ[R] BilinForm R M) (flipHom ≪≫ₗ flipHom) (LinearEquiv.refl R (BilinForm R M))

Tactic:
ext A
-- Module: Mathlib.LinearAlgebra.BilinearForm.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
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:
simp
-- Module: Mathlib.LinearAlgebra.BilinearForm.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
⊢ Eq (α := R →ₗ[R] M) ((flip (lsmul R M) : (a : M) → R →ₗ[R] M) m : R →ₗ[R] M) (toSpanSingleton R M m : R →ₗ[R] M)

Tactic:
rfl

Premises used: LinearMap.smulRight, LinearMap.toSpanSingleton, rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
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
a b : 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
hb :
  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)}
    b
y : M
hy : y ∈ N
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Submodule R S) 1
    ((((B : (a : M) → M →ₗ[S] S) (a + b) : M →ₗ[S] S) : (a : M) → S) y : S)

Tactic:
simpa using add_mem (ha y hy) (hb y hy)

Premises used: AddMemClass.add_mem
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
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
rw : Membership.mem (γ := Submodule R S) 1 0
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Submodule R S) 1 (((B : (a : M) → M →ₗ[S] S) 0 : (a : M) → S) y : S)

Tactic:
rw [B.zero_left]

Premises used: LinearMap.BilinForm.zero_left
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
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 (γ := Submodule R S) 1 0

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
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 (γ := Submodule R S) 1 0

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice
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 (γ := Submodule R S) 1
    (HSMul.hSMul (β := S) r ((((B : (a : M) → M →ₗ[S] S) a : M →ₗ[S] S) : (a : M) → S) y : S))

Tactic:
(1 : Submodule R S).smul_mem r (ha y hy)

Premises used: OfNat.ofNat, Submodule.smul_mem