Theorem: QuadraticForm.anisotropic_of_Equivalent (AntLorentz/Diagonalize.lean)

State before:
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
h : Equivalent Q S
⊢ Anisotropic Q → Anisotropic S
Tactic:
rcases h with ⟨val⟩
State after:
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
⊢ Anisotropic Q → Anisotropic S

State before:
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
⊢ Anisotropic Q → Anisotropic S
Tactic:
intro h
State after:
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
h : Anisotropic Q
⊢ Anisotropic S

State before:
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
h : Anisotropic Q
⊢ Anisotropic S
Tactic:
simp only [Anisotropic] at *
State after:
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
h : ∀ (x : M), ↑Q x = 0 → x = 0
⊢ ∀ (x : M₂), ↑S x = 0 → x = 0

State before:
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
h : ∀ (x : M), ↑Q x = 0 → x = 0
⊢ ∀ (x : M₂), ↑S x = 0 → x = 0
Tactic:
intro x hx
State after:
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
h : ∀ (x : M), ↑Q x = 0 → x = 0
x : M₂
hx : ↑S x = 0
⊢ x = 0

State before:
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
h : ∀ (x : M), ↑Q x = 0 → x = 0
x : M₂
hx : ↑S x = 0
⊢ x = 0
Tactic:
specialize h (val.symm x)
State after:
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x : M₂
hx : ↑S x = 0
h : ↑Q (↑(Isometry.symm val) x) = 0 → ↑(Isometry.symm val) x = 0
⊢ x = 0

State before:
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x : M₂
hx : ↑S x = 0
h : ↑Q (↑(Isometry.symm val) x) = 0 → ↑(Isometry.symm val) x = 0
⊢ x = 0
Tactic:
simp only [Isometry.map_app, AddEquivClass.map_eq_zero_iff] at h
State after:
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x : M₂
hx : ↑S x = 0
h : ↑S x = 0 → x = 0
⊢ x = 0

State before:
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x : M₂
hx : ↑S x = 0
h : ↑S x = 0 → x = 0
⊢ x = 0
Tactic:
specialize h hx
State after:
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x : M₂
hx : ↑S x = 0
h : x = 0
⊢ x = 0

State before:
case intro
ι : Type ?u.84107
R✝ : Type ?u.84110
K : Type ?u.84113
M✝ : Type ?u.84116
M₁ : Type ?u.84119
M₂ : Type u_1
M₃ : Type ?u.84125
V : Type ?u.84128
R : Type u_2
M : Type u_3
inst✝⁶ : Field R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : FiniteDimensional R M
inst✝² : Invertible 2
Q✝ : QuadraticForm R M
inst✝¹ : AddCommGroup M₂
inst✝ : Module R M₂
Q : QuadraticForm R M
S : QuadraticForm R M₂
val : Isometry Q S
x : M₂
hx : ↑S x = 0
h : x = 0
⊢ x = 0
Tactic:
simpa using h
State after:
no goals