Theorem: QuadraticForm.HasseMinkowski_global_to_local (AntLorentz/HasseMinkowski.lean)

State before:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
h : Isotropic F
⊢ EverywhereLocallyIsotropic F
Tactic:
rw [EverywhereLocallyIsotropic]
State after:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
h : Isotropic F
⊢ (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] F)) ∧ Isotropic (baseChange ℝ F)

State before:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
h : Isotropic F
⊢ (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], Isotropic (baseChange ℚ_[p] F)) ∧ Isotropic (baseChange ℝ F)
Tactic:
simp only [Isotropic, Anisotropic, not_forall, exists_prop] at h ⊢
State after:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
h : ∃ x, ↑F x = 0 ∧ ¬x = 0
⊢ (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ∃ x, ↑(baseChange ℚ_[p] F) x = 0 ∧ ¬x = 0) ∧
    ∃ x, ↑(baseChange ℝ F) x = 0 ∧ ¬x = 0

State before:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
h : ∃ x, ↑F x = 0 ∧ ¬x = 0
⊢ (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ∃ x, ↑(baseChange ℚ_[p] F) x = 0 ∧ ¬x = 0) ∧
    ∃ x, ↑(baseChange ℝ F) x = 0 ∧ ¬x = 0
Tactic:
push_neg at h
State after:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
h : ∃ x, ↑F x = 0 ∧ x ≠ 0
⊢ (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ∃ x, ↑(baseChange ℚ_[p] F) x = 0 ∧ ¬x = 0) ∧
    ∃ x, ↑(baseChange ℝ F) x = 0 ∧ ¬x = 0

State before:
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
h : ∃ x, ↑F x = 0 ∧ x ≠ 0
⊢ (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ∃ x, ↑(baseChange ℚ_[p] F) x = 0 ∧ ¬x = 0) ∧
    ∃ x, ↑(baseChange ℝ F) x = 0 ∧ ¬x = 0
Tactic:
obtain ⟨x, hx, hne⟩ := h
State after:
case intro.intro
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
x : V
hx : ↑F x = 0
hne : x ≠ 0
⊢ (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ∃ x, ↑(baseChange ℚ_[p] F) x = 0 ∧ ¬x = 0) ∧
    ∃ x, ↑(baseChange ℝ F) x = 0 ∧ ¬x = 0

State before:
case intro.intro
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
x : V
hx : ↑F x = 0
hne : x ≠ 0
⊢ (∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ∃ x, ↑(baseChange ℚ_[p] F) x = 0 ∧ ¬x = 0) ∧
    ∃ x, ↑(baseChange ℝ F) x = 0 ∧ ¬x = 0
Tactic:
constructor
State after:
case intro.intro.left
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
x : V
hx : ↑F x = 0
hne : x ≠ 0
⊢ ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ∃ x, ↑(baseChange ℚ_[p] F) x = 0 ∧ ¬x = 0

case intro.intro.right
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
x : V
hx : ↑F x = 0
hne : x ≠ 0
⊢ ∃ x, ↑(baseChange ℝ F) x = 0 ∧ ¬x = 0

State before:
case intro.intro.left
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
x : V
hx : ↑F x = 0
hne : x ≠ 0
⊢ ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ∃ x, ↑(baseChange ℚ_[p] F) x = 0 ∧ ¬x = 0

case intro.intro.right
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
x : V
hx : ↑F x = 0
hne : x ≠ 0
⊢ ∃ x, ↑(baseChange ℝ F) x = 0 ∧ ¬x = 0
Tactic:
. intro p hp
  use (1 ⊗ₜ x)
  simp only [baseChange_eval, mul_one, hx, _root_.map_zero, mul_zero, true_and]
  sorry
State after:
case intro.intro.right
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
x : V
hx : ↑F x = 0
hne : x ≠ 0
⊢ ∃ x, ↑(baseChange ℝ F) x = 0 ∧ ¬x = 0

State before:
case intro.intro.right
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
x : V
hx : ↑F x = 0
hne : x ≠ 0
⊢ ∃ x, ↑(baseChange ℝ F) x = 0 ∧ ¬x = 0
Tactic:
. use (1 ⊗ₜ x)
  simp only [baseChange_eval, mul_one, hx, _root_.map_zero, mul_zero, true_and]
  sorry
State after:
no goals

State before:
case intro.intro.left
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
x : V
hx : ↑F x = 0
hne : x ≠ 0
⊢ ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ∃ x, ↑(baseChange ℚ_[p] F) x = 0 ∧ ¬x = 0
Tactic:
intro p hp
State after:
case intro.intro.left
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
x : V
hx : ↑F x = 0
hne : x ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∃ x, ↑(baseChange ℚ_[p] F) x = 0 ∧ ¬x = 0

State before:
case intro.intro.left
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
x : V
hx : ↑F x = 0
hne : x ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∃ x, ↑(baseChange ℚ_[p] F) x = 0 ∧ ¬x = 0
Tactic:
use (1 ⊗ₜ x)
State after:
case intro.intro.left
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
x : V
hx : ↑F x = 0
hne : x ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑(baseChange ℚ_[p] F) (1 ⊗ₜ[ℚ] x) = 0 ∧ ¬1 ⊗ₜ[ℚ] x = 0

State before:
case intro.intro.left
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
x : V
hx : ↑F x = 0
hne : x ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ↑(baseChange ℚ_[p] F) (1 ⊗ₜ[ℚ] x) = 0 ∧ ¬1 ⊗ₜ[ℚ] x = 0
Tactic:
simp only [baseChange_eval, mul_one, hx, _root_.map_zero, mul_zero, true_and]
State after:
case intro.intro.left
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
x : V
hx : ↑F x = 0
hne : x ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ¬1 ⊗ₜ[ℚ] x = 0

State before:
case intro.intro.left
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
x : V
hx : ↑F x = 0
hne : x ≠ 0
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ¬1 ⊗ₜ[ℚ] x = 0
Tactic:
sorry
State after:
no goals

State before:
case intro.intro.right
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
x : V
hx : ↑F x = 0
hne : x ≠ 0
⊢ ∃ x, ↑(baseChange ℝ F) x = 0 ∧ ¬x = 0
Tactic:
use (1 ⊗ₜ x)
State after:
case intro.intro.right
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
x : V
hx : ↑F x = 0
hne : x ≠ 0
⊢ ↑(baseChange ℝ F) (1 ⊗ₜ[ℚ] x) = 0 ∧ ¬1 ⊗ₜ[ℚ] x = 0

State before:
case intro.intro.right
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
x : V
hx : ↑F x = 0
hne : x ≠ 0
⊢ ↑(baseChange ℝ F) (1 ⊗ₜ[ℚ] x) = 0 ∧ ¬1 ⊗ₜ[ℚ] x = 0
Tactic:
simp only [baseChange_eval, mul_one, hx, _root_.map_zero, mul_zero, true_and]
State after:
case intro.intro.right
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
x : V
hx : ↑F x = 0
hne : x ≠ 0
⊢ ¬1 ⊗ₜ[ℚ] x = 0

State before:
case intro.intro.right
V : Type
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℚ V
V₂ : Type ?u.23512
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module ℚ V₂
inst✝² : FiniteDimensional ℚ V
F✝ : QuadraticForm ℚ V
k W : Type
inst✝¹ : Field k
inst✝ : AddCommGroup W
F : QuadraticForm ℚ V
x : V
hx : ↑F x = 0
hne : x ≠ 0
⊢ ¬1 ⊗ₜ[ℚ] x = 0
Tactic:
sorry
State after:
no goals