internlm/Lean-Github huggingface dataset:
Theorem: QuadraticForm.baseChange.Equivalent
Proof state before:
case intro.val.Cp.intro
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x✝ y✝ : A ⊗[R] M
a✝¹ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝) = ↑(baseChange A Q) x✝
a✝ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) = ↑(baseChange A Q) y✝
B : BilinForm A (A ⊗[R] M₂)
hB : ∀ (x y : A ⊗[R] M₂), ↑(baseChange A S) (x + y) = ↑(baseChange A S) x + ↑(baseChange A S) y + BilinForm.bilin B x y
⊢ ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝) +
        ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) +
      BilinForm.bilin B (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝)
        (↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) =
    ↑(baseChange A Q) (x✝ + y✝)
Tactic:
simp [*]
Proof state after:
case intro.val.Cp.intro
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x✝ y✝ : A ⊗[R] M
a✝¹ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝) = ↑(baseChange A Q) x✝
a✝ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) = ↑(baseChange A Q) y✝
B : BilinForm A (A ⊗[R] M₂)
hB : ∀ (x y : A ⊗[R] M₂), ↑(baseChange A S) (x + y) = ↑(baseChange A S) x + ↑(baseChange A S) y + BilinForm.bilin B x y
⊢ ↑(baseChange A Q) x✝ + ↑(baseChange A Q) y✝ +
      BilinForm.bilin B (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝)
        (↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) =
    ↑(baseChange A Q) (x✝ + y✝)
Theorem: QuadraticForm.baseChange.Equivalent
Proof state before:
case intro.val.Cp.intro
R M : Type
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
A✝ : Type ?u.496082
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R A✝
inst✝² : Invertible 2
A : Type
inst✝¹ : CommRing A
inst✝ : Algebra R A
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x✝ y✝ : A ⊗[R] M
a✝¹ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝) = ↑(baseChange A Q) x✝
a✝ : ↑(baseChange A S) (↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) = ↑(baseChange A Q) y✝
B : BilinForm A (A ⊗[R] M₂)
hB : ∀ (x y : A ⊗[R] M₂), ↑(baseChange A S) (x + y) = ↑(baseChange A S) x + ↑(baseChange A S) y + BilinForm.bilin B x y
⊢ ↑(baseChange A Q) x✝ + ↑(baseChange A Q) y✝ +
      BilinForm.bilin B (↑(LinearEquiv.baseChange val.toLinearEquiv) x✝)
        (↑(LinearEquiv.baseChange val.toLinearEquiv) y✝) =
    ↑(baseChange A Q) (x✝ + y✝)
Tactic:
sorry
Proof state after:
no goals
Theorem: base_change_module_rank_preserved
Proof state before:
k : Type u_3
M : Type (max u_1 u_2)
A : Type u_1
inst✝¹⁰ : Field k
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module k M
inst✝⁷ : Ring A
inst✝⁶ : Algebra k A
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower k A M
inst✝³ : StrongRankCondition A
inst✝² : Module.Free k M
inst✝¹ : Module.Free A M
inst✝ : Module.Free k A
⊢ Module.rank k M = Module.rank A (A ⊗[k] M)
Tactic:
obtain ⟨⟨_, bM⟩⟩ := Module.Free.exists_basis (R := k) (M := M)
Proof state after:
case intro.mk
k : Type u_3
M : Type (max u_1 u_2)
A : Type u_1
inst✝¹⁰ : Field k
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module k M
inst✝⁷ : Ring A
inst✝⁶ : Algebra k A
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower k A M
inst✝³ : StrongRankCondition A
inst✝² : Module.Free k M
inst✝¹ : Module.Free A M
inst✝ : Module.Free k A
fst✝ : Type (max u_1 u_2)
bM : Basis fst✝ k M
⊢ Module.rank k M = Module.rank A (A ⊗[k] M)
Theorem: base_change_module_rank_preserved
Proof state before:
case intro.mk
k : Type u_3
M : Type (max u_1 u_2)
A : Type u_1
inst✝¹⁰ : Field k
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module k M
inst✝⁷ : Ring A
inst✝⁶ : Algebra k A
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower k A M
inst✝³ : StrongRankCondition A
inst✝² : Module.Free k M
inst✝¹ : Module.Free A M
inst✝ : Module.Free k A
fst✝ : Type (max u_1 u_2)
bM : Basis fst✝ k M
⊢ Module.rank k M = Module.rank A (A ⊗[k] M)
Tactic:
rw [← bM.mk_eq_rank'', (bM.base_change (A := A)).mk_eq_rank'']
Proof state after:
no goals
Theorem: BilinForm.baseChange_of_degenerate
Proof state before:
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
hB : ¬Nondegenerate B
⊢ ¬Nondegenerate (baseChange A B)
Tactic:
simp only [BilinForm.Nondegenerate, not_forall, exists_prop] at *
Proof state after:
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
hB : ∃ x, (∀ (n : M), bilin B x n = 0) ∧ ¬x = 0
⊢ ∃ x, (∀ (n : TensorProduct k A M), bilin (baseChange A B) x n = 0) ∧ ¬x = 0
Theorem: BilinForm.baseChange_of_degenerate
Proof state before:
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
hB : ∃ x, (∀ (n : M), bilin B x n = 0) ∧ ¬x = 0
⊢ ∃ x, (∀ (n : TensorProduct k A M), bilin (baseChange A B) x n = 0) ∧ ¬x = 0
Tactic:
obtain ⟨x, hn, hx⟩ := hB
Proof state after:
case intro.intro
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
⊢ ∃ x, (∀ (n : TensorProduct k A M), bilin (baseChange A B) x n = 0) ∧ ¬x = 0
Theorem: BilinForm.baseChange_of_degenerate
Proof state before:
case intro.intro
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
⊢ ∃ x, (∀ (n : TensorProduct k A M), bilin (baseChange A B) x n = 0) ∧ ¬x = 0
Tactic:
refine ⟨(1 ⊗ₜ x), ?_, ?_⟩
Proof state after:
case intro.intro.refine_1
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
⊢ ∀ (n : TensorProduct k A M), bilin (baseChange A B) (1 ⊗ₜ[k] x) n = 0

case intro.intro.refine_2
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
⊢ ¬1 ⊗ₜ[k] x = 0
Theorem: BilinForm.baseChange_of_degenerate
Proof state before:
case intro.intro.refine_1
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
⊢ ∀ (n : TensorProduct k A M), bilin (baseChange A B) (1 ⊗ₜ[k] x) n = 0

case intro.intro.refine_2
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
⊢ ¬1 ⊗ₜ[k] x = 0
Tactic:
. intro n
  induction n using TensorProduct.induction_on
  . simp
  . simp [hn]
  . simp [*]
Proof state after:
case intro.intro.refine_2
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
⊢ ¬1 ⊗ₜ[k] x = 0
Theorem: BilinForm.baseChange_of_degenerate
Proof state before:
case intro.intro.refine_2
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
⊢ ¬1 ⊗ₜ[k] x = 0
Tactic:
. simp
  intro h
  apply hx
  sorry
Proof state after:
no goals
Theorem: BilinForm.baseChange_of_degenerate
Proof state before:
case intro.intro.refine_1
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
⊢ ∀ (n : TensorProduct k A M), bilin (baseChange A B) (1 ⊗ₜ[k] x) n = 0
Tactic:
intro n
Proof state after:
case intro.intro.refine_1
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
n : TensorProduct k A M
⊢ bilin (baseChange A B) (1 ⊗ₜ[k] x) n = 0
Theorem: BilinForm.baseChange_of_degenerate
Proof state before:
case intro.intro.refine_1
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
n : TensorProduct k A M
⊢ bilin (baseChange A B) (1 ⊗ₜ[k] x) n = 0
Tactic:
induction n using TensorProduct.induction_on
Proof state after:
case intro.intro.refine_1.C0
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
⊢ bilin (baseChange A B) (1 ⊗ₜ[k] x) 0 = 0

case intro.intro.refine_1.C1
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
x✝ : A
y✝ : M
⊢ bilin (baseChange A B) (1 ⊗ₜ[k] x) (x✝ ⊗ₜ[k] y✝) = 0

case intro.intro.refine_1.Cp
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
x✝ y✝ : TensorProduct k A M
a✝¹ : bilin (baseChange A B) (1 ⊗ₜ[k] x) x✝ = 0
a✝ : bilin (baseChange A B) (1 ⊗ₜ[k] x) y✝ = 0
⊢ bilin (baseChange A B) (1 ⊗ₜ[k] x) (x✝ + y✝) = 0
Theorem: BilinForm.baseChange_of_degenerate
Proof state before:
case intro.intro.refine_1.C0
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
⊢ bilin (baseChange A B) (1 ⊗ₜ[k] x) 0 = 0

case intro.intro.refine_1.C1
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
x✝ : A
y✝ : M
⊢ bilin (baseChange A B) (1 ⊗ₜ[k] x) (x✝ ⊗ₜ[k] y✝) = 0

case intro.intro.refine_1.Cp
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
x✝ y✝ : TensorProduct k A M
a✝¹ : bilin (baseChange A B) (1 ⊗ₜ[k] x) x✝ = 0
a✝ : bilin (baseChange A B) (1 ⊗ₜ[k] x) y✝ = 0
⊢ bilin (baseChange A B) (1 ⊗ₜ[k] x) (x✝ + y✝) = 0
Tactic:
. simp
Proof state after:
case intro.intro.refine_1.C1
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
x✝ : A
y✝ : M
⊢ bilin (baseChange A B) (1 ⊗ₜ[k] x) (x✝ ⊗ₜ[k] y✝) = 0

case intro.intro.refine_1.Cp
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
x✝ y✝ : TensorProduct k A M
a✝¹ : bilin (baseChange A B) (1 ⊗ₜ[k] x) x✝ = 0
a✝ : bilin (baseChange A B) (1 ⊗ₜ[k] x) y✝ = 0
⊢ bilin (baseChange A B) (1 ⊗ₜ[k] x) (x✝ + y✝) = 0
Theorem: BilinForm.baseChange_of_degenerate
Proof state before:
case intro.intro.refine_1.C1
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
x✝ : A
y✝ : M
⊢ bilin (baseChange A B) (1 ⊗ₜ[k] x) (x✝ ⊗ₜ[k] y✝) = 0

case intro.intro.refine_1.Cp
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
x✝ y✝ : TensorProduct k A M
a✝¹ : bilin (baseChange A B) (1 ⊗ₜ[k] x) x✝ = 0
a✝ : bilin (baseChange A B) (1 ⊗ₜ[k] x) y✝ = 0
⊢ bilin (baseChange A B) (1 ⊗ₜ[k] x) (x✝ + y✝) = 0
Tactic:
. simp [hn]
Proof state after:
case intro.intro.refine_1.Cp
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
x✝ y✝ : TensorProduct k A M
a✝¹ : bilin (baseChange A B) (1 ⊗ₜ[k] x) x✝ = 0
a✝ : bilin (baseChange A B) (1 ⊗ₜ[k] x) y✝ = 0
⊢ bilin (baseChange A B) (1 ⊗ₜ[k] x) (x✝ + y✝) = 0
Theorem: BilinForm.baseChange_of_degenerate
Proof state before:
case intro.intro.refine_1.Cp
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
x✝ y✝ : TensorProduct k A M
a✝¹ : bilin (baseChange A B) (1 ⊗ₜ[k] x) x✝ = 0
a✝ : bilin (baseChange A B) (1 ⊗ₜ[k] x) y✝ = 0
⊢ bilin (baseChange A B) (1 ⊗ₜ[k] x) (x✝ + y✝) = 0
Tactic:
. simp [*]
Proof state after:
no goals
Theorem: BilinForm.baseChange_of_degenerate
Proof state before:
case intro.intro.refine_1.C0
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
⊢ bilin (baseChange A B) (1 ⊗ₜ[k] x) 0 = 0
Tactic:
simp
Proof state after:
no goals
Theorem: BilinForm.baseChange_of_degenerate
Proof state before:
case intro.intro.refine_1.C1
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
x✝ : A
y✝ : M
⊢ bilin (baseChange A B) (1 ⊗ₜ[k] x) (x✝ ⊗ₜ[k] y✝) = 0
Tactic:
simp [hn]
Proof state after:
no goals
Theorem: BilinForm.baseChange_of_degenerate
Proof state before:
case intro.intro.refine_1.Cp
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
x✝ y✝ : TensorProduct k A M
a✝¹ : bilin (baseChange A B) (1 ⊗ₜ[k] x) x✝ = 0
a✝ : bilin (baseChange A B) (1 ⊗ₜ[k] x) y✝ = 0
⊢ bilin (baseChange A B) (1 ⊗ₜ[k] x) (x✝ + y✝) = 0
Tactic:
simp [*]
Proof state after:
no goals
Theorem: BilinForm.baseChange_of_degenerate
Proof state before:
case intro.intro.refine_2
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
⊢ ¬1 ⊗ₜ[k] x = 0
Tactic:
intro h
Proof state after:
case intro.intro.refine_2
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
h : 1 ⊗ₜ[k] x = 0
⊢ False
Theorem: BilinForm.baseChange_of_degenerate
Proof state before:
case intro.intro.refine_2
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
h : 1 ⊗ₜ[k] x = 0
⊢ False
Tactic:
apply hx
Proof state after:
case intro.intro.refine_2
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
h : 1 ⊗ₜ[k] x = 0
⊢ x = 0
Theorem: BilinForm.baseChange_of_degenerate
Proof state before:
case intro.intro.refine_2
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
B : BilinForm k M
x : M
hn : ∀ (n : M), bilin B x n = 0
hx : ¬x = 0
h : 1 ⊗ₜ[k] x = 0
⊢ x = 0
Tactic:
sorry
Proof state after:
no goals
Theorem: baseChange_of_degenerate
Proof state before:
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q : QuadraticForm k M
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
⊢ ¬BilinForm.Nondegenerate (↑associated (baseChange A Q))
Tactic:
simp only [baseChange_associated]
Proof state after:
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q : QuadraticForm k M
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
⊢ ¬BilinForm.Nondegenerate (BilinForm.baseChange A (↑associated Q))
Theorem: baseChange_of_degenerate
Proof state before:
M k A : Type
inst✝¹² : Field k
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module k M
inst✝⁹ : CommRing A
inst✝⁸ : Algebra k A
inst✝⁷ : Module A M
inst✝⁶ : IsScalarTower k A M
inst✝⁵ : StrongRankCondition A
inst✝⁴ : Module.Free k M
inst✝³ : Module.Free A M
inst✝² : Module.Free k A
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q : QuadraticForm k M
hQ : ¬BilinForm.Nondegenerate (↑associated Q)
⊢ ¬BilinForm.Nondegenerate (BilinForm.baseChange A (↑associated Q))
Tactic:
exact BilinForm.baseChange_of_degenerate _ hQ
Proof state after:
no goals