Theorem: BilinForm.baseChange_of_degenerate (AntLorentz/BaseChange.lean)

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 *
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

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
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

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), ?_, ?_⟩
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

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 [*]
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

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
State after:
no goals

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
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

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
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

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
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

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]
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

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 [*]
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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 [*]
State after:
no goals

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
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

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
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

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
State after:
no goals