[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
⊢ E →ₗ[ℝ] E →ₗ[ℝ] ℝ
[PROOFSTEP]
let z : AlternatingMap ℝ E ℝ (Fin 0) ≃ₗ[ℝ] ℝ := AlternatingMap.constLinearEquivOfIsEmpty.symm
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
z : AlternatingMap ℝ E ℝ (Fin 0) ≃ₗ[ℝ] ℝ := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
⊢ E →ₗ[ℝ] E →ₗ[ℝ] ℝ
[PROOFSTEP]
let y : AlternatingMap ℝ E ℝ (Fin 1) →ₗ[ℝ] E →ₗ[ℝ] ℝ :=
  LinearMap.llcomp ℝ E (AlternatingMap ℝ E ℝ (Fin 0)) ℝ z ∘ₗ AlternatingMap.curryLeftLinearMap
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
z : AlternatingMap ℝ E ℝ (Fin 0) ≃ₗ[ℝ] ℝ := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
y : AlternatingMap ℝ E ℝ (Fin 1) →ₗ[ℝ] E →ₗ[ℝ] ℝ :=
  LinearMap.comp (↑(LinearMap.llcomp ℝ E (AlternatingMap ℝ E ℝ (Fin 0)) ℝ) ↑z) AlternatingMap.curryLeftLinearMap
⊢ E →ₗ[ℝ] E →ₗ[ℝ] ℝ
[PROOFSTEP]
exact y ∘ₗ AlternatingMap.curryLeftLinearMap (R' := ℝ) o.volumeForm
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ↑(↑(areaForm o) x) y = ↑(volumeForm o) ![x, y]
[PROOFSTEP]
simp [areaForm]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ ↑(↑(areaForm o) x) x = 0
[PROOFSTEP]
rw [areaForm_to_volumeForm]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ ↑(volumeForm o) ![x, x] = 0
[PROOFSTEP]
refine' o.volumeForm.map_eq_zero_of_eq ![x, x] _ (_ : (0 : Fin 2) ≠ 1)
[GOAL]
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ Matrix.vecCons x ![x] 0 = Matrix.vecCons x ![x] 1
[PROOFSTEP]
simp
[GOAL]
case refine'_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ 0 ≠ 1
[PROOFSTEP]
norm_num
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ↑(↑(areaForm o) x) y = -↑(↑(areaForm o) y) x
[PROOFSTEP]
simp only [areaForm_to_volumeForm]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ↑(volumeForm o) ![x, y] = -↑(volumeForm o) ![y, x]
[PROOFSTEP]
convert o.volumeForm.map_swap ![y, x] (_ : (0 : Fin 2) ≠ 1)
[GOAL]
case h.e'_2.h.e'_6
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ![x, y] = ![y, x] ∘ ↑(Equiv.swap 0 1)
[PROOFSTEP]
ext i
[GOAL]
case h.e'_2.h.e'_6.h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
i : Fin (Nat.succ 1)
⊢ Matrix.vecCons x ![y] i = (![y, x] ∘ ↑(Equiv.swap 0 1)) i
[PROOFSTEP]
fin_cases i
[GOAL]
case h.e'_2.h.e'_6.h.head
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ Matrix.vecCons x ![y] { val := 0, isLt := (_ : 0 < Nat.succ 1) } =
    (![y, x] ∘ ↑(Equiv.swap 0 1)) { val := 0, isLt := (_ : 0 < Nat.succ 1) }
[PROOFSTEP]
rfl
[GOAL]
case h.e'_2.h.e'_6.h.tail.head
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ Matrix.vecCons x ![y] { val := 1, isLt := (_ : (fun a => a < Nat.succ 1) 1) } =
    (![y, x] ∘ ↑(Equiv.swap 0 1)) { val := 1, isLt := (_ : (fun a => a < Nat.succ 1) 1) }
[PROOFSTEP]
rfl
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ 0 ≠ 1
[PROOFSTEP]
norm_num
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
⊢ areaForm (-o) = -areaForm o
[PROOFSTEP]
ext x y
[GOAL]
case h.h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ↑(↑(areaForm (-o)) x) y = ↑(↑(-areaForm o) x) y
[PROOFSTEP]
simp [areaForm_to_volumeForm]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ |↑(↑(areaForm o) x) y| ≤ ‖x‖ * ‖y‖
[PROOFSTEP]
simpa [areaForm_to_volumeForm, Fin.prod_univ_succ] using o.abs_volumeForm_apply_le ![x, y]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ↑(↑(areaForm o) x) y ≤ ‖x‖ * ‖y‖
[PROOFSTEP]
simpa [areaForm_to_volumeForm, Fin.prod_univ_succ] using o.volumeForm_apply_le ![x, y]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
h : inner x y = 0
⊢ |↑(↑(areaForm o) x) y| = ‖x‖ * ‖y‖
[PROOFSTEP]
rw [o.areaForm_to_volumeForm, o.abs_volumeForm_apply_of_pairwise_orthogonal]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
h : inner x y = 0
⊢ (Finset.prod Finset.univ fun i => ‖Matrix.vecCons x ![y] i‖) = ‖x‖ * ‖y‖
[PROOFSTEP]
simp [Fin.prod_univ_succ]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
h : inner x y = 0
⊢ Pairwise fun i j => inner (Matrix.vecCons x ![y] i) (Matrix.vecCons x ![y] j) = 0
[PROOFSTEP]
intro i j hij
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
h : inner x y = 0
i j : Fin 2
hij : i ≠ j
⊢ inner (Matrix.vecCons x ![y] i) (Matrix.vecCons x ![y] j) = 0
[PROOFSTEP]
fin_cases i
[GOAL]
case head
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
h : inner x y = 0
j : Fin 2
hij : { val := 0, isLt := (_ : 0 < 2) } ≠ j
⊢ inner (Matrix.vecCons x ![y] { val := 0, isLt := (_ : 0 < 2) }) (Matrix.vecCons x ![y] j) = 0
[PROOFSTEP]
fin_cases j
[GOAL]
case tail.head
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
h : inner x y = 0
j : Fin 2
hij : { val := 1, isLt := (_ : (fun a => a < 2) 1) } ≠ j
⊢ inner (Matrix.vecCons x ![y] { val := 1, isLt := (_ : (fun a => a < 2) 1) }) (Matrix.vecCons x ![y] j) = 0
[PROOFSTEP]
fin_cases j
[GOAL]
case head.head
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
h : inner x y = 0
hij : { val := 0, isLt := (_ : 0 < 2) } ≠ { val := 0, isLt := (_ : 0 < 2) }
⊢ inner (Matrix.vecCons x ![y] { val := 0, isLt := (_ : 0 < 2) })
      (Matrix.vecCons x ![y] { val := 0, isLt := (_ : 0 < 2) }) =
    0
[PROOFSTEP]
simp_all
[GOAL]
case head.tail.head
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
h : inner x y = 0
hij : { val := 0, isLt := (_ : 0 < 2) } ≠ { val := 1, isLt := (_ : (fun a => a < 2) 1) }
⊢ inner (Matrix.vecCons x ![y] { val := 0, isLt := (_ : 0 < 2) })
      (Matrix.vecCons x ![y] { val := 1, isLt := (_ : (fun a => a < 2) 1) }) =
    0
[PROOFSTEP]
simpa using h
[GOAL]
case tail.head.head
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
h : inner x y = 0
hij : { val := 1, isLt := (_ : (fun a => a < 2) 1) } ≠ { val := 0, isLt := (_ : 0 < 2) }
⊢ inner (Matrix.vecCons x ![y] { val := 1, isLt := (_ : (fun a => a < 2) 1) })
      (Matrix.vecCons x ![y] { val := 0, isLt := (_ : 0 < 2) }) =
    0
[PROOFSTEP]
simpa [real_inner_comm] using h
[GOAL]
case tail.head.tail.head
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
h : inner x y = 0
hij : { val := 1, isLt := (_ : (fun a => a < 2) 1) } ≠ { val := 1, isLt := (_ : (fun a => a < 2) 1) }
⊢ inner (Matrix.vecCons x ![y] { val := 1, isLt := (_ : (fun a => a < 2) 1) })
      (Matrix.vecCons x ![y] { val := 1, isLt := (_ : (fun a => a < 2) 1) }) =
    0
[PROOFSTEP]
simp_all
[GOAL]
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ ↑(↑(areaForm (↑(map (Fin 2) φ.toLinearEquiv) o)) x) y =
    ↑(↑(areaForm o) (↑(LinearIsometryEquiv.symm φ) x)) (↑(LinearIsometryEquiv.symm φ) y)
[PROOFSTEP]
have : φ.symm ∘ ![x, y] = ![φ.symm x, φ.symm y] := by
  ext i
  fin_cases i <;> rfl
[GOAL]
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ ↑(LinearIsometryEquiv.symm φ) ∘ ![x, y] = ![↑(LinearIsometryEquiv.symm φ) x, ↑(LinearIsometryEquiv.symm φ) y]
[PROOFSTEP]
ext i
[GOAL]
case h
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
i : Fin (Nat.succ (Nat.succ 0))
⊢ (↑(LinearIsometryEquiv.symm φ) ∘ ![x, y]) i =
    Matrix.vecCons (↑(LinearIsometryEquiv.symm φ) x) ![↑(LinearIsometryEquiv.symm φ) y] i
[PROOFSTEP]
fin_cases i
[GOAL]
case h.head
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ (↑(LinearIsometryEquiv.symm φ) ∘ ![x, y]) { val := 0, isLt := (_ : 0 < Nat.succ (Nat.succ 0)) } =
    Matrix.vecCons (↑(LinearIsometryEquiv.symm φ) x) ![↑(LinearIsometryEquiv.symm φ) y]
      { val := 0, isLt := (_ : 0 < Nat.succ (Nat.succ 0)) }
[PROOFSTEP]
rfl
[GOAL]
case h.tail.head
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ (↑(LinearIsometryEquiv.symm φ) ∘ ![x, y]) { val := 1, isLt := (_ : (fun a => a < Nat.succ (Nat.succ 0)) 1) } =
    Matrix.vecCons (↑(LinearIsometryEquiv.symm φ) x) ![↑(LinearIsometryEquiv.symm φ) y]
      { val := 1, isLt := (_ : (fun a => a < Nat.succ (Nat.succ 0)) 1) }
[PROOFSTEP]
rfl
[GOAL]
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
this : ↑(LinearIsometryEquiv.symm φ) ∘ ![x, y] = ![↑(LinearIsometryEquiv.symm φ) x, ↑(LinearIsometryEquiv.symm φ) y]
⊢ ↑(↑(areaForm (↑(map (Fin 2) φ.toLinearEquiv) o)) x) y =
    ↑(↑(areaForm o) (↑(LinearIsometryEquiv.symm φ) x)) (↑(LinearIsometryEquiv.symm φ) y)
[PROOFSTEP]
simp [areaForm_to_volumeForm, volumeForm_map, this]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
x y : E
⊢ ↑(↑(areaForm o) (↑φ x)) (↑φ y) = ↑(↑(areaForm o) x) y
[PROOFSTEP]
convert o.areaForm_map φ (φ x) (φ y)
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_5
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
x y : E
⊢ o = ↑(map (Fin 2) φ.toLinearEquiv) o
[PROOFSTEP]
symm
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_5
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
x y : E
⊢ ↑(map (Fin 2) φ.toLinearEquiv) o = o
[PROOFSTEP]
rwa [← o.map_eq_iff_det_pos φ.toLinearEquiv] at hφ
[GOAL]
case h.e'_2.h.e'_5.h.e'_5.h.e'_5
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
x y : E
⊢ Fintype.card (Fin 2) = finrank ℝ E
[PROOFSTEP]
rw [@Fact.out (finrank ℝ E = 2), Fintype.card_fin]
[GOAL]
case h.e'_3.h.e'_5.h.e'_6
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
x y : E
⊢ x = ↑(LinearIsometryEquiv.symm φ) (↑φ x)
[PROOFSTEP]
simp
[GOAL]
case h.e'_3.h.e'_6
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
x y : E
⊢ y = ↑(LinearIsometryEquiv.symm φ) (↑φ y)
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ inner (↑(rightAngleRotationAux₁ o) x) y = ↑(↑(areaForm o) x) y
[PROOFSTEP]
simp only [rightAngleRotationAux₁, LinearEquiv.trans_symm, LinearIsometryEquiv.toLinearEquiv_symm, LinearMap.coe_comp,
  LinearEquiv.coe_coe, Function.comp_apply, LinearEquiv.trans_apply, LinearIsometryEquiv.coe_toLinearEquiv]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ inner
      (↑(LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E))
        (↑(LinearEquiv.symm (LinearEquiv.symm LinearMap.toContinuousLinearMap)) (↑(areaForm o) x)))
      y =
    ↑(↑(areaForm o) x) y
[PROOFSTEP]
rw [InnerProductSpace.toDual_symm_apply]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ↑(↑(LinearEquiv.symm (LinearEquiv.symm LinearMap.toContinuousLinearMap)) (↑(areaForm o) x)) y = ↑(↑(areaForm o) x) y
[PROOFSTEP]
norm_cast
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ inner x (↑(rightAngleRotationAux₁ o) y) = -↑(↑(areaForm o) x) y
[PROOFSTEP]
rw [real_inner_comm]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ inner (↑(rightAngleRotationAux₁ o) y) x = -↑(↑(areaForm o) x) y
[PROOFSTEP]
simp [o.areaForm_swap y x]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
src✝ : E →ₗ[ℝ] E := rightAngleRotationAux₁ o
x : E
⊢ ‖↑{ toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : ℝ) (x : E),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id ℝ) r • AddHom.toFun src✝.toAddHom x) }
        x‖ =
    ‖x‖
[PROOFSTEP]
dsimp
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
src✝ : E →ₗ[ℝ] E := rightAngleRotationAux₁ o
x : E
⊢ ‖↑(rightAngleRotationAux₁ o) x‖ = ‖x‖
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
src✝ : E →ₗ[ℝ] E := rightAngleRotationAux₁ o
x : E
⊢ ‖↑(rightAngleRotationAux₁ o) x‖ ≤ ‖x‖
[PROOFSTEP]
cases' eq_or_lt_of_le (norm_nonneg (o.rightAngleRotationAux₁ x)) with h h
[GOAL]
case refine'_1.inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
src✝ : E →ₗ[ℝ] E := rightAngleRotationAux₁ o
x : E
h : 0 = ‖↑(rightAngleRotationAux₁ o) x‖
⊢ ‖↑(rightAngleRotationAux₁ o) x‖ ≤ ‖x‖
[PROOFSTEP]
rw [← h]
[GOAL]
case refine'_1.inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
src✝ : E →ₗ[ℝ] E := rightAngleRotationAux₁ o
x : E
h : 0 = ‖↑(rightAngleRotationAux₁ o) x‖
⊢ 0 ≤ ‖x‖
[PROOFSTEP]
positivity
[GOAL]
case refine'_1.inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
src✝ : E →ₗ[ℝ] E := rightAngleRotationAux₁ o
x : E
h : 0 < ‖↑(rightAngleRotationAux₁ o) x‖
⊢ ‖↑(rightAngleRotationAux₁ o) x‖ ≤ ‖x‖
[PROOFSTEP]
refine' le_of_mul_le_mul_right _ h
[GOAL]
case refine'_1.inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
src✝ : E →ₗ[ℝ] E := rightAngleRotationAux₁ o
x : E
h : 0 < ‖↑(rightAngleRotationAux₁ o) x‖
⊢ ‖↑(rightAngleRotationAux₁ o) x‖ * ‖↑(rightAngleRotationAux₁ o) x‖ ≤ ‖x‖ * ‖↑(rightAngleRotationAux₁ o) x‖
[PROOFSTEP]
rw [← real_inner_self_eq_norm_mul_norm, o.inner_rightAngleRotationAux₁_left]
[GOAL]
case refine'_1.inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
src✝ : E →ₗ[ℝ] E := rightAngleRotationAux₁ o
x : E
h : 0 < ‖↑(rightAngleRotationAux₁ o) x‖
⊢ ↑(↑(areaForm o) x) (↑(rightAngleRotationAux₁ o) x) ≤ ‖x‖ * ‖↑(rightAngleRotationAux₁ o) x‖
[PROOFSTEP]
exact o.areaForm_le x (o.rightAngleRotationAux₁ x)
[GOAL]
case refine'_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
src✝ : E →ₗ[ℝ] E := rightAngleRotationAux₁ o
x : E
⊢ ‖x‖ ≤ ‖↑(rightAngleRotationAux₁ o) x‖
[PROOFSTEP]
let K : Submodule ℝ E := ℝ ∙ x
[GOAL]
case refine'_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
src✝ : E →ₗ[ℝ] E := rightAngleRotationAux₁ o
x : E
K : Submodule ℝ E := Submodule.span ℝ {x}
⊢ ‖x‖ ≤ ‖↑(rightAngleRotationAux₁ o) x‖
[PROOFSTEP]
have : Nontrivial Kᗮ := by
  apply @FiniteDimensional.nontrivial_of_finrank_pos ℝ
  have : finrank ℝ K ≤ Finset.card { x } := by
    rw [← Set.toFinset_singleton]
    exact finrank_span_le_card ({ x } : Set E)
  have : Finset.card { x } = 1 := Finset.card_singleton x
  have : finrank ℝ K + finrank ℝ Kᗮ = finrank ℝ E := K.finrank_add_finrank_orthogonal
  have : finrank ℝ E = 2 := Fact.out
  linarith
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
src✝ : E →ₗ[ℝ] E := rightAngleRotationAux₁ o
x : E
K : Submodule ℝ E := Submodule.span ℝ {x}
⊢ Nontrivial { x // x ∈ Kᗮ }
[PROOFSTEP]
apply @FiniteDimensional.nontrivial_of_finrank_pos ℝ
[GOAL]
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
src✝ : E →ₗ[ℝ] E := rightAngleRotationAux₁ o
x : E
K : Submodule ℝ E := Submodule.span ℝ {x}
⊢ 0 < finrank ℝ { x // x ∈ Kᗮ }
[PROOFSTEP]
have : finrank ℝ K ≤ Finset.card { x } := by
  rw [← Set.toFinset_singleton]
  exact finrank_span_le_card ({ x } : Set E)
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
src✝ : E →ₗ[ℝ] E := rightAngleRotationAux₁ o
x : E
K : Submodule ℝ E := Submodule.span ℝ {x}
⊢ finrank ℝ { x // x ∈ K } ≤ Finset.card {x}
[PROOFSTEP]
rw [← Set.toFinset_singleton]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
src✝ : E →ₗ[ℝ] E := rightAngleRotationAux₁ o
x : E
K : Submodule ℝ E := Submodule.span ℝ {x}
⊢ finrank ℝ { x // x ∈ K } ≤ Finset.card (Set.toFinset {x})
[PROOFSTEP]
exact finrank_span_le_card ({ x } : Set E)
[GOAL]
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
src✝ : E →ₗ[ℝ] E := rightAngleRotationAux₁ o
x : E
K : Submodule ℝ E := Submodule.span ℝ {x}
this : finrank ℝ { x // x ∈ K } ≤ Finset.card {x}
⊢ 0 < finrank ℝ { x // x ∈ Kᗮ }
[PROOFSTEP]
have : Finset.card { x } = 1 := Finset.card_singleton x
[GOAL]
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
src✝ : E →ₗ[ℝ] E := rightAngleRotationAux₁ o
x : E
K : Submodule ℝ E := Submodule.span ℝ {x}
this✝ : finrank ℝ { x // x ∈ K } ≤ Finset.card {x}
this : Finset.card {x} = 1
⊢ 0 < finrank ℝ { x // x ∈ Kᗮ }
[PROOFSTEP]
have : finrank ℝ K + finrank ℝ Kᗮ = finrank ℝ E := K.finrank_add_finrank_orthogonal
[GOAL]
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
src✝ : E →ₗ[ℝ] E := rightAngleRotationAux₁ o
x : E
K : Submodule ℝ E := Submodule.span ℝ {x}
this✝¹ : finrank ℝ { x // x ∈ K } ≤ Finset.card {x}
this✝ : Finset.card {x} = 1
this : finrank ℝ { x // x ∈ K } + finrank ℝ { x // x ∈ Kᗮ } = finrank ℝ E
⊢ 0 < finrank ℝ { x // x ∈ Kᗮ }
[PROOFSTEP]
have : finrank ℝ E = 2 := Fact.out
[GOAL]
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
src✝ : E →ₗ[ℝ] E := rightAngleRotationAux₁ o
x : E
K : Submodule ℝ E := Submodule.span ℝ {x}
this✝² : finrank ℝ { x // x ∈ K } ≤ Finset.card {x}
this✝¹ : Finset.card {x} = 1
this✝ : finrank ℝ { x // x ∈ K } + finrank ℝ { x // x ∈ Kᗮ } = finrank ℝ E
this : finrank ℝ E = 2
⊢ 0 < finrank ℝ { x // x ∈ Kᗮ }
[PROOFSTEP]
linarith
[GOAL]
case refine'_2
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
src✝ : E →ₗ[ℝ] E := rightAngleRotationAux₁ o
x : E
K : Submodule ℝ E := Submodule.span ℝ {x}
this : Nontrivial { x // x ∈ Kᗮ }
⊢ ‖x‖ ≤ ‖↑(rightAngleRotationAux₁ o) x‖
[PROOFSTEP]
obtain ⟨w, hw₀⟩ : ∃ w : Kᗮ, w ≠ 0 := exists_ne 0
[GOAL]
case refine'_2.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
src✝ : E →ₗ[ℝ] E := rightAngleRotationAux₁ o
x : E
K : Submodule ℝ E := Submodule.span ℝ {x}
this : Nontrivial { x // x ∈ Kᗮ }
w : { x // x ∈ Kᗮ }
hw₀ : w ≠ 0
⊢ ‖x‖ ≤ ‖↑(rightAngleRotationAux₁ o) x‖
[PROOFSTEP]
have hw' : ⟪x, (w : E)⟫ = 0 := Submodule.mem_orthogonal_singleton_iff_inner_right.mp w.2
[GOAL]
case refine'_2.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
src✝ : E →ₗ[ℝ] E := rightAngleRotationAux₁ o
x : E
K : Submodule ℝ E := Submodule.span ℝ {x}
this : Nontrivial { x // x ∈ Kᗮ }
w : { x // x ∈ Kᗮ }
hw₀ : w ≠ 0
hw' : inner x ↑w = 0
⊢ ‖x‖ ≤ ‖↑(rightAngleRotationAux₁ o) x‖
[PROOFSTEP]
have hw : (w : E) ≠ 0 := fun h => hw₀ (Submodule.coe_eq_zero.mp h)
[GOAL]
case refine'_2.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
src✝ : E →ₗ[ℝ] E := rightAngleRotationAux₁ o
x : E
K : Submodule ℝ E := Submodule.span ℝ {x}
this : Nontrivial { x // x ∈ Kᗮ }
w : { x // x ∈ Kᗮ }
hw₀ : w ≠ 0
hw' : inner x ↑w = 0
hw : ↑w ≠ 0
⊢ ‖x‖ ≤ ‖↑(rightAngleRotationAux₁ o) x‖
[PROOFSTEP]
refine' le_of_mul_le_mul_right _ (by rwa [norm_pos_iff] : 0 < ‖(w : E)‖)
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
src✝ : E →ₗ[ℝ] E := rightAngleRotationAux₁ o
x : E
K : Submodule ℝ E := Submodule.span ℝ {x}
this : Nontrivial { x // x ∈ Kᗮ }
w : { x // x ∈ Kᗮ }
hw₀ : w ≠ 0
hw' : inner x ↑w = 0
hw : ↑w ≠ 0
⊢ 0 < ‖↑w‖
[PROOFSTEP]
rwa [norm_pos_iff]
[GOAL]
case refine'_2.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
src✝ : E →ₗ[ℝ] E := rightAngleRotationAux₁ o
x : E
K : Submodule ℝ E := Submodule.span ℝ {x}
this : Nontrivial { x // x ∈ Kᗮ }
w : { x // x ∈ Kᗮ }
hw₀ : w ≠ 0
hw' : inner x ↑w = 0
hw : ↑w ≠ 0
⊢ ‖x‖ * ‖↑w‖ ≤ ‖↑(rightAngleRotationAux₁ o) x‖ * ‖↑w‖
[PROOFSTEP]
rw [← o.abs_areaForm_of_orthogonal hw']
[GOAL]
case refine'_2.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
src✝ : E →ₗ[ℝ] E := rightAngleRotationAux₁ o
x : E
K : Submodule ℝ E := Submodule.span ℝ {x}
this : Nontrivial { x // x ∈ Kᗮ }
w : { x // x ∈ Kᗮ }
hw₀ : w ≠ 0
hw' : inner x ↑w = 0
hw : ↑w ≠ 0
⊢ |↑(↑(areaForm o) x) ↑w| ≤ ‖↑(rightAngleRotationAux₁ o) x‖ * ‖↑w‖
[PROOFSTEP]
rw [← o.inner_rightAngleRotationAux₁_left x w]
[GOAL]
case refine'_2.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
src✝ : E →ₗ[ℝ] E := rightAngleRotationAux₁ o
x : E
K : Submodule ℝ E := Submodule.span ℝ {x}
this : Nontrivial { x // x ∈ Kᗮ }
w : { x // x ∈ Kᗮ }
hw₀ : w ≠ 0
hw' : inner x ↑w = 0
hw : ↑w ≠ 0
⊢ |inner (↑(rightAngleRotationAux₁ o) x) ↑w| ≤ ‖↑(rightAngleRotationAux₁ o) x‖ * ‖↑w‖
[PROOFSTEP]
exact abs_real_inner_le_norm (o.rightAngleRotationAux₁ x) w
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ ↑(rightAngleRotationAux₁ o) (↑(rightAngleRotationAux₁ o) x) = -x
[PROOFSTEP]
apply ext_inner_left ℝ
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ ∀ (v : (fun x => E) (↑(rightAngleRotationAux₁ o) x)),
    inner v (↑(rightAngleRotationAux₁ o) (↑(rightAngleRotationAux₁ o) x)) = inner v (-x)
[PROOFSTEP]
intro y
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
y : (fun x => E) (↑(rightAngleRotationAux₁ o) x)
⊢ inner y (↑(rightAngleRotationAux₁ o) (↑(rightAngleRotationAux₁ o) x)) = inner y (-x)
[PROOFSTEP]
have : ⟪o.rightAngleRotationAux₁ y, o.rightAngleRotationAux₁ x⟫ = ⟪y, x⟫ :=
  LinearIsometry.inner_map_map o.rightAngleRotationAux₂ y x
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
y : (fun x => E) (↑(rightAngleRotationAux₁ o) x)
this : inner (↑(rightAngleRotationAux₁ o) y) (↑(rightAngleRotationAux₁ o) x) = inner y x
⊢ inner y (↑(rightAngleRotationAux₁ o) (↑(rightAngleRotationAux₁ o) x)) = inner y (-x)
[PROOFSTEP]
rw [o.inner_rightAngleRotationAux₁_right, ← o.inner_rightAngleRotationAux₁_left, this, inner_neg_right]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
⊢ LinearMap.comp (rightAngleRotationAux₂ o).toLinearMap (-rightAngleRotationAux₁ o) = LinearMap.id
[PROOFSTEP]
ext
[GOAL]
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x✝ : E
⊢ ↑(LinearMap.comp (rightAngleRotationAux₂ o).toLinearMap (-rightAngleRotationAux₁ o)) x✝ = ↑LinearMap.id x✝
[PROOFSTEP]
simp [rightAngleRotationAux₂]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
⊢ LinearMap.comp (-rightAngleRotationAux₁ o) (rightAngleRotationAux₂ o).toLinearMap = LinearMap.id
[PROOFSTEP]
ext
[GOAL]
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x✝ : E
⊢ ↑(LinearMap.comp (-rightAngleRotationAux₁ o) (rightAngleRotationAux₂ o).toLinearMap) x✝ = ↑LinearMap.id x✝
[PROOFSTEP]
simp [rightAngleRotationAux₂]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ inner (↑(rightAngleRotation o) x) y = ↑(↑(areaForm o) x) y
[PROOFSTEP]
rw [rightAngleRotation]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ inner
      (↑(LinearIsometryEquiv.ofLinearIsometry (rightAngleRotationAux₂ o) (-rightAngleRotationAux₁ o)
            (_ : LinearMap.comp (rightAngleRotationAux₂ o).toLinearMap (-rightAngleRotationAux₁ o) = LinearMap.id)
            (_ : LinearMap.comp (-rightAngleRotationAux₁ o) (rightAngleRotationAux₂ o).toLinearMap = LinearMap.id))
        x)
      y =
    ↑(↑(areaForm o) x) y
[PROOFSTEP]
exact o.inner_rightAngleRotationAux₁_left x y
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ inner x (↑(rightAngleRotation o) y) = -↑(↑(areaForm o) x) y
[PROOFSTEP]
rw [rightAngleRotation]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ inner x
      (↑(LinearIsometryEquiv.ofLinearIsometry (rightAngleRotationAux₂ o) (-rightAngleRotationAux₁ o)
            (_ : LinearMap.comp (rightAngleRotationAux₂ o).toLinearMap (-rightAngleRotationAux₁ o) = LinearMap.id)
            (_ : LinearMap.comp (-rightAngleRotationAux₁ o) (rightAngleRotationAux₂ o).toLinearMap = LinearMap.id))
        y) =
    -↑(↑(areaForm o) x) y
[PROOFSTEP]
exact o.inner_rightAngleRotationAux₁_right x y
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ ↑(rightAngleRotation o) (↑(rightAngleRotation o) x) = -x
[PROOFSTEP]
rw [rightAngleRotation]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ ↑(LinearIsometryEquiv.ofLinearIsometry (rightAngleRotationAux₂ o) (-rightAngleRotationAux₁ o)
          (_ : LinearMap.comp (rightAngleRotationAux₂ o).toLinearMap (-rightAngleRotationAux₁ o) = LinearMap.id)
          (_ : LinearMap.comp (-rightAngleRotationAux₁ o) (rightAngleRotationAux₂ o).toLinearMap = LinearMap.id))
      (↑(LinearIsometryEquiv.ofLinearIsometry (rightAngleRotationAux₂ o) (-rightAngleRotationAux₁ o)
            (_ : LinearMap.comp (rightAngleRotationAux₂ o).toLinearMap (-rightAngleRotationAux₁ o) = LinearMap.id)
            (_ : LinearMap.comp (-rightAngleRotationAux₁ o) (rightAngleRotationAux₂ o).toLinearMap = LinearMap.id))
        x) =
    -x
[PROOFSTEP]
exact o.rightAngleRotationAux₁_rightAngleRotationAux₁ x
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
⊢ LinearIsometryEquiv.symm (rightAngleRotation o) =
    LinearIsometryEquiv.trans (rightAngleRotation o) (LinearIsometryEquiv.neg ℝ)
[PROOFSTEP]
rw [rightAngleRotation]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
⊢ LinearIsometryEquiv.symm
      (LinearIsometryEquiv.ofLinearIsometry (rightAngleRotationAux₂ o) (-rightAngleRotationAux₁ o)
        (_ : LinearMap.comp (rightAngleRotationAux₂ o).toLinearMap (-rightAngleRotationAux₁ o) = LinearMap.id)
        (_ : LinearMap.comp (-rightAngleRotationAux₁ o) (rightAngleRotationAux₂ o).toLinearMap = LinearMap.id)) =
    LinearIsometryEquiv.trans
      (LinearIsometryEquiv.ofLinearIsometry (rightAngleRotationAux₂ o) (-rightAngleRotationAux₁ o)
        (_ : LinearMap.comp (rightAngleRotationAux₂ o).toLinearMap (-rightAngleRotationAux₁ o) = LinearMap.id)
        (_ : LinearMap.comp (-rightAngleRotationAux₁ o) (rightAngleRotationAux₂ o).toLinearMap = LinearMap.id))
      (LinearIsometryEquiv.neg ℝ)
[PROOFSTEP]
exact LinearIsometryEquiv.toLinearIsometry_injective rfl
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ inner (↑(rightAngleRotation o) x) x = 0
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ inner x (↑(rightAngleRotation o) y) = -inner (↑(rightAngleRotation o) x) y
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ inner (↑(rightAngleRotation o) x) y = -inner x (↑(rightAngleRotation o) y)
[PROOFSTEP]
simp [o.inner_rightAngleRotation_swap x y]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ↑(↑(areaForm o) (↑(rightAngleRotation o) x)) y = -inner x y
[PROOFSTEP]
rw [← o.inner_comp_rightAngleRotation, o.inner_rightAngleRotation_right, neg_neg]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ↑(↑(areaForm o) x) (↑(rightAngleRotation o) y) = inner x y
[PROOFSTEP]
rw [← o.inner_rightAngleRotation_left, o.inner_comp_rightAngleRotation]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ↑(↑(areaForm o) (↑(rightAngleRotation o) x)) (↑(rightAngleRotation o) y) = ↑(↑(areaForm o) x) y
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
⊢ LinearIsometryEquiv.trans (rightAngleRotation o) (rightAngleRotation o) = LinearIsometryEquiv.neg ℝ
[PROOFSTEP]
ext
[GOAL]
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x✝ : E
⊢ ↑(LinearIsometryEquiv.trans (rightAngleRotation o) (rightAngleRotation o)) x✝ = ↑(LinearIsometryEquiv.neg ℝ) x✝
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ ↑(rightAngleRotation (-o)) x = -↑(rightAngleRotation o) x
[PROOFSTEP]
apply ext_inner_right ℝ
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ ∀ (v : E), inner (↑(rightAngleRotation (-o)) x) v = inner (-↑(rightAngleRotation o) x) v
[PROOFSTEP]
intro y
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ inner (↑(rightAngleRotation (-o)) x) y = inner (-↑(rightAngleRotation o) x) y
[PROOFSTEP]
rw [inner_rightAngleRotation_left]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ↑(↑(areaForm (-o)) x) y = inner (-↑(rightAngleRotation o) x) y
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x : F
⊢ ↑(rightAngleRotation (↑(map (Fin 2) φ.toLinearEquiv) o)) x =
    ↑φ (↑(rightAngleRotation o) (↑(LinearIsometryEquiv.symm φ) x))
[PROOFSTEP]
apply ext_inner_right ℝ
[GOAL]
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x : F
⊢ ∀ (v : F),
    inner (↑(rightAngleRotation (↑(map (Fin 2) φ.toLinearEquiv) o)) x) v =
      inner (↑φ (↑(rightAngleRotation o) (↑(LinearIsometryEquiv.symm φ) x))) v
[PROOFSTEP]
intro y
[GOAL]
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ inner (↑(rightAngleRotation (↑(map (Fin 2) φ.toLinearEquiv) o)) x) y =
    inner (↑φ (↑(rightAngleRotation o) (↑(LinearIsometryEquiv.symm φ) x))) y
[PROOFSTEP]
rw [inner_rightAngleRotation_left]
[GOAL]
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ ↑(↑(areaForm (↑(map (Fin 2) φ.toLinearEquiv) o)) x) y =
    inner (↑φ (↑(rightAngleRotation o) (↑(LinearIsometryEquiv.symm φ) x))) y
[PROOFSTEP]
trans ⟪J (φ.symm x), φ.symm y⟫
[GOAL]
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ ↑(↑(areaForm (↑(map (Fin 2) φ.toLinearEquiv) o)) x) y =
    inner (↑(rightAngleRotation o) (↑(LinearIsometryEquiv.symm φ) x)) (↑(LinearIsometryEquiv.symm φ) y)
[PROOFSTEP]
simp [o.areaForm_map]
[GOAL]
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ inner (↑(rightAngleRotation o) (↑(LinearIsometryEquiv.symm φ) x)) (↑(LinearIsometryEquiv.symm φ) y) =
    inner (↑φ (↑(rightAngleRotation o) (↑(LinearIsometryEquiv.symm φ) x))) y
[PROOFSTEP]
trans ⟪φ (J (φ.symm x)), φ (φ.symm y)⟫
[GOAL]
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ inner (↑(rightAngleRotation o) (↑(LinearIsometryEquiv.symm φ) x)) (↑(LinearIsometryEquiv.symm φ) y) =
    inner (↑φ (↑(rightAngleRotation o) (↑(LinearIsometryEquiv.symm φ) x))) (↑φ (↑(LinearIsometryEquiv.symm φ) y))
[PROOFSTEP]
rw [φ.inner_map_map]
[GOAL]
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ inner (↑φ (↑(rightAngleRotation o) (↑(LinearIsometryEquiv.symm φ) x))) (↑φ (↑(LinearIsometryEquiv.symm φ) y)) =
    inner (↑φ (↑(rightAngleRotation o) (↑(LinearIsometryEquiv.symm φ) x))) y
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
x : E
⊢ ↑φ (↑(rightAngleRotation o) x) = ↑(rightAngleRotation o) (↑φ x)
[PROOFSTEP]
convert (o.rightAngleRotation_map φ (φ x)).symm
[GOAL]
case h.e'_2.h.e'_6.h.e'_6
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
x : E
⊢ x = ↑(LinearIsometryEquiv.symm φ) (↑φ x)
[PROOFSTEP]
simp
[GOAL]
case h.e'_3.h.e'_5.h.e'_5
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
x : E
⊢ o = ↑(map (Fin 2) φ.toLinearEquiv) o
[PROOFSTEP]
symm
[GOAL]
case h.e'_3.h.e'_5.h.e'_5
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
x : E
⊢ ↑(map (Fin 2) φ.toLinearEquiv) o = o
[PROOFSTEP]
rwa [← o.map_eq_iff_det_pos φ.toLinearEquiv] at hφ
[GOAL]
case h.e'_3.h.e'_5.h.e'_5
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
x : E
⊢ Fintype.card (Fin 2) = finrank ℝ E
[PROOFSTEP]
rw [@Fact.out (finrank ℝ E = 2), Fintype.card_fin]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
i : Fin 2
⊢ Matrix.vecCons x ![↑(rightAngleRotation o) x] i ≠ 0
[PROOFSTEP]
fin_cases i
[GOAL]
case head
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
⊢ Matrix.vecCons x ![↑(rightAngleRotation o) x] { val := 0, isLt := (_ : 0 < 2) } ≠ 0
[PROOFSTEP]
simp [hx]
[GOAL]
case tail.head
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
⊢ Matrix.vecCons x ![↑(rightAngleRotation o) x] { val := 1, isLt := (_ : (fun a => a < 2) 1) } ≠ 0
[PROOFSTEP]
simp [hx]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
⊢ ∀ (i j : Fin 2),
    i ≠ j →
      inner (Matrix.vecCons x ![↑(rightAngleRotation o) x] i) (Matrix.vecCons x ![↑(rightAngleRotation o) x] j) = 0
[PROOFSTEP]
intro i j hij
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
i j : Fin 2
hij : i ≠ j
⊢ inner (Matrix.vecCons x ![↑(rightAngleRotation o) x] i) (Matrix.vecCons x ![↑(rightAngleRotation o) x] j) = 0
[PROOFSTEP]
fin_cases i
[GOAL]
case head
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
j : Fin 2
hij : { val := 0, isLt := (_ : 0 < 2) } ≠ j
⊢ inner (Matrix.vecCons x ![↑(rightAngleRotation o) x] { val := 0, isLt := (_ : 0 < 2) })
      (Matrix.vecCons x ![↑(rightAngleRotation o) x] j) =
    0
[PROOFSTEP]
fin_cases j
[GOAL]
case tail.head
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
j : Fin 2
hij : { val := 1, isLt := (_ : (fun a => a < 2) 1) } ≠ j
⊢ inner (Matrix.vecCons x ![↑(rightAngleRotation o) x] { val := 1, isLt := (_ : (fun a => a < 2) 1) })
      (Matrix.vecCons x ![↑(rightAngleRotation o) x] j) =
    0
[PROOFSTEP]
fin_cases j
[GOAL]
case head.head
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
hij : { val := 0, isLt := (_ : 0 < 2) } ≠ { val := 0, isLt := (_ : 0 < 2) }
⊢ inner (Matrix.vecCons x ![↑(rightAngleRotation o) x] { val := 0, isLt := (_ : 0 < 2) })
      (Matrix.vecCons x ![↑(rightAngleRotation o) x] { val := 0, isLt := (_ : 0 < 2) }) =
    0
[PROOFSTEP]
simp_all
[GOAL]
case head.tail.head
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
hij : { val := 0, isLt := (_ : 0 < 2) } ≠ { val := 1, isLt := (_ : (fun a => a < 2) 1) }
⊢ inner (Matrix.vecCons x ![↑(rightAngleRotation o) x] { val := 0, isLt := (_ : 0 < 2) })
      (Matrix.vecCons x ![↑(rightAngleRotation o) x] { val := 1, isLt := (_ : (fun a => a < 2) 1) }) =
    0
[PROOFSTEP]
simp_all
[GOAL]
case tail.head.head
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
hij : { val := 1, isLt := (_ : (fun a => a < 2) 1) } ≠ { val := 0, isLt := (_ : 0 < 2) }
⊢ inner (Matrix.vecCons x ![↑(rightAngleRotation o) x] { val := 1, isLt := (_ : (fun a => a < 2) 1) })
      (Matrix.vecCons x ![↑(rightAngleRotation o) x] { val := 0, isLt := (_ : 0 < 2) }) =
    0
[PROOFSTEP]
simp_all
[GOAL]
case tail.head.tail.head
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : x ≠ 0
hij : { val := 1, isLt := (_ : (fun a => a < 2) 1) } ≠ { val := 1, isLt := (_ : (fun a => a < 2) 1) }
⊢ inner (Matrix.vecCons x ![↑(rightAngleRotation o) x] { val := 1, isLt := (_ : (fun a => a < 2) 1) })
      (Matrix.vecCons x ![↑(rightAngleRotation o) x] { val := 1, isLt := (_ : (fun a => a < 2) 1) }) =
    0
[PROOFSTEP]
simp_all
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
⊢ inner a x • ↑(innerₛₗ ℝ) a + ↑(↑(areaForm o) a) x • ↑(areaForm o) a = ‖a‖ ^ 2 • ↑(innerₛₗ ℝ) x
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : a = 0
⊢ inner a x • ↑(innerₛₗ ℝ) a + ↑(↑(areaForm o) a) x • ↑(areaForm o) a = ‖a‖ ^ 2 • ↑(innerₛₗ ℝ) x
[PROOFSTEP]
simp [ha]
[GOAL]
case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ inner a x • ↑(innerₛₗ ℝ) a + ↑(↑(areaForm o) a) x • ↑(areaForm o) a = ‖a‖ ^ 2 • ↑(innerₛₗ ℝ) x
[PROOFSTEP]
apply (o.basisRightAngleRotation a ha).ext
[GOAL]
case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ ∀ (i : Fin 2),
    ↑(inner a x • ↑(innerₛₗ ℝ) a + ↑(↑(areaForm o) a) x • ↑(areaForm o) a) (↑(basisRightAngleRotation o a ha) i) =
      ↑(‖a‖ ^ 2 • ↑(innerₛₗ ℝ) x) (↑(basisRightAngleRotation o a ha) i)
[PROOFSTEP]
intro i
[GOAL]
case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
i : Fin 2
⊢ ↑(inner a x • ↑(innerₛₗ ℝ) a + ↑(↑(areaForm o) a) x • ↑(areaForm o) a) (↑(basisRightAngleRotation o a ha) i) =
    ↑(‖a‖ ^ 2 • ↑(innerₛₗ ℝ) x) (↑(basisRightAngleRotation o a ha) i)
[PROOFSTEP]
fin_cases i
[GOAL]
case neg.head
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ ↑(inner a x • ↑(innerₛₗ ℝ) a + ↑(↑(areaForm o) a) x • ↑(areaForm o) a)
      (↑(basisRightAngleRotation o a ha) { val := 0, isLt := (_ : 0 < 2) }) =
    ↑(‖a‖ ^ 2 • ↑(innerₛₗ ℝ) x) (↑(basisRightAngleRotation o a ha) { val := 0, isLt := (_ : 0 < 2) })
[PROOFSTEP]
simp only [Fin.mk_zero, coe_basisRightAngleRotation, Matrix.cons_val_zero, LinearMap.add_apply, LinearMap.smul_apply,
  innerₛₗ_apply, real_inner_self_eq_norm_sq, smul_eq_mul, areaForm_apply_self, mul_zero, add_zero, Real.rpow_two,
  real_inner_comm]
[GOAL]
case neg.head
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ inner a x * ‖a‖ ^ 2 = ‖a‖ ^ 2 * inner a x
[PROOFSTEP]
ring
[GOAL]
case neg.tail.head
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ ↑(inner a x • ↑(innerₛₗ ℝ) a + ↑(↑(areaForm o) a) x • ↑(areaForm o) a)
      (↑(basisRightAngleRotation o a ha) { val := 1, isLt := (_ : (fun a => a < 2) 1) }) =
    ↑(‖a‖ ^ 2 • ↑(innerₛₗ ℝ) x) (↑(basisRightAngleRotation o a ha) { val := 1, isLt := (_ : (fun a => a < 2) 1) })
[PROOFSTEP]
simp only [Fin.mk_one, coe_basisRightAngleRotation, Matrix.cons_val_one, Matrix.head_cons, LinearMap.add_apply,
  LinearMap.smul_apply, innerₛₗ_apply, inner_rightAngleRotation_right, areaForm_apply_self, neg_zero, smul_eq_mul,
  mul_zero, areaForm_rightAngleRotation_right, real_inner_self_eq_norm_sq, zero_add, Real.rpow_two, mul_neg]
[GOAL]
case neg.tail.head
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ ↑(↑(areaForm o) a) x * ‖a‖ ^ 2 = -(‖a‖ ^ 2 * ↑(↑(areaForm o) x) a)
[PROOFSTEP]
rw [o.areaForm_swap]
[GOAL]
case neg.tail.head
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ -↑(↑(areaForm o) x) a * ‖a‖ ^ 2 = -(‖a‖ ^ 2 * ↑(↑(areaForm o) x) a)
[PROOFSTEP]
ring
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a b : E
⊢ inner a b ^ 2 + ↑(↑(areaForm o) a) b ^ 2 = ‖a‖ ^ 2 * ‖b‖ ^ 2
[PROOFSTEP]
simpa [sq, real_inner_self_eq_norm_sq] using o.inner_mul_inner_add_areaForm_mul_areaForm a b b
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
⊢ inner a x • ↑(areaForm o) a - ↑(↑(areaForm o) a) x • ↑(innerₛₗ ℝ) a = ‖a‖ ^ 2 • ↑(areaForm o) x
[PROOFSTEP]
by_cases ha : a = 0
[GOAL]
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : a = 0
⊢ inner a x • ↑(areaForm o) a - ↑(↑(areaForm o) a) x • ↑(innerₛₗ ℝ) a = ‖a‖ ^ 2 • ↑(areaForm o) x
[PROOFSTEP]
simp [ha]
[GOAL]
case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ inner a x • ↑(areaForm o) a - ↑(↑(areaForm o) a) x • ↑(innerₛₗ ℝ) a = ‖a‖ ^ 2 • ↑(areaForm o) x
[PROOFSTEP]
apply (o.basisRightAngleRotation a ha).ext
[GOAL]
case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ ∀ (i : Fin 2),
    ↑(inner a x • ↑(areaForm o) a - ↑(↑(areaForm o) a) x • ↑(innerₛₗ ℝ) a) (↑(basisRightAngleRotation o a ha) i) =
      ↑(‖a‖ ^ 2 • ↑(areaForm o) x) (↑(basisRightAngleRotation o a ha) i)
[PROOFSTEP]
intro i
[GOAL]
case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
i : Fin 2
⊢ ↑(inner a x • ↑(areaForm o) a - ↑(↑(areaForm o) a) x • ↑(innerₛₗ ℝ) a) (↑(basisRightAngleRotation o a ha) i) =
    ↑(‖a‖ ^ 2 • ↑(areaForm o) x) (↑(basisRightAngleRotation o a ha) i)
[PROOFSTEP]
fin_cases i
[GOAL]
case neg.head
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ ↑(inner a x • ↑(areaForm o) a - ↑(↑(areaForm o) a) x • ↑(innerₛₗ ℝ) a)
      (↑(basisRightAngleRotation o a ha) { val := 0, isLt := (_ : 0 < 2) }) =
    ↑(‖a‖ ^ 2 • ↑(areaForm o) x) (↑(basisRightAngleRotation o a ha) { val := 0, isLt := (_ : 0 < 2) })
[PROOFSTEP]
simp only [o.areaForm_swap a x, neg_smul, sub_neg_eq_add, Fin.mk_zero, coe_basisRightAngleRotation,
  Matrix.cons_val_zero, LinearMap.add_apply, LinearMap.smul_apply, areaForm_apply_self, smul_eq_mul, mul_zero,
  innerₛₗ_apply, real_inner_self_eq_norm_sq, zero_add, Real.rpow_two]
[GOAL]
case neg.head
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ ↑(↑(areaForm o) x) a * ‖a‖ ^ 2 = ‖a‖ ^ 2 * ↑(↑(areaForm o) x) a
[PROOFSTEP]
ring
[GOAL]
case neg.tail.head
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ ↑(inner a x • ↑(areaForm o) a - ↑(↑(areaForm o) a) x • ↑(innerₛₗ ℝ) a)
      (↑(basisRightAngleRotation o a ha) { val := 1, isLt := (_ : (fun a => a < 2) 1) }) =
    ↑(‖a‖ ^ 2 • ↑(areaForm o) x) (↑(basisRightAngleRotation o a ha) { val := 1, isLt := (_ : (fun a => a < 2) 1) })
[PROOFSTEP]
simp only [Fin.mk_one, coe_basisRightAngleRotation, Matrix.cons_val_one, Matrix.head_cons, LinearMap.sub_apply,
  LinearMap.smul_apply, areaForm_rightAngleRotation_right, real_inner_self_eq_norm_sq, smul_eq_mul, innerₛₗ_apply,
  inner_rightAngleRotation_right, areaForm_apply_self, neg_zero, mul_zero, sub_zero, Real.rpow_two, real_inner_comm]
[GOAL]
case neg.tail.head
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x : E
ha : ¬a = 0
⊢ inner a x * ‖a‖ ^ 2 = ‖a‖ ^ 2 * inner a x
[PROOFSTEP]
ring
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ 0 ≤ inner x y ∧ ↑(↑(areaForm o) x) y = 0 ↔ SameRay ℝ x y
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : x = 0
⊢ 0 ≤ inner x y ∧ ↑(↑(areaForm o) x) y = 0 ↔ SameRay ℝ x y
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
⊢ 0 ≤ inner x y ∧ ↑(↑(areaForm o) x) y = 0 ↔ SameRay ℝ x y
[PROOFSTEP]
constructor
[GOAL]
case neg.mp
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
⊢ 0 ≤ inner x y ∧ ↑(↑(areaForm o) x) y = 0 → SameRay ℝ x y
[PROOFSTEP]
let a : ℝ := (o.basisRightAngleRotation x hx).repr y 0
[GOAL]
case neg.mp
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
a : ℝ := ↑(↑(basisRightAngleRotation o x hx).repr y) 0
⊢ 0 ≤ inner x y ∧ ↑(↑(areaForm o) x) y = 0 → SameRay ℝ x y
[PROOFSTEP]
let b : ℝ := (o.basisRightAngleRotation x hx).repr y 1
[GOAL]
case neg.mp
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
a : ℝ := ↑(↑(basisRightAngleRotation o x hx).repr y) 0
b : ℝ := ↑(↑(basisRightAngleRotation o x hx).repr y) 1
⊢ 0 ≤ inner x y ∧ ↑(↑(areaForm o) x) y = 0 → SameRay ℝ x y
[PROOFSTEP]
suffices ↑0 ≤ a * ‖x‖ ^ 2 ∧ b * ‖x‖ ^ 2 = 0 → SameRay ℝ x (a • x + b • J x)
  by
  rw [← (o.basisRightAngleRotation x hx).sum_repr y]
  simp only [Fin.sum_univ_succ, coe_basisRightAngleRotation, Matrix.cons_val_zero, Fin.succ_zero_eq_one',
    Fintype.univ_of_isEmpty, Finset.sum_empty, areaForm_apply_self, map_smul, map_add, real_inner_smul_right,
    inner_add_right, Matrix.cons_val_one, Matrix.head_cons, Algebra.id.smul_eq_mul, areaForm_rightAngleRotation_right,
    mul_zero, add_zero, zero_add, neg_zero, inner_rightAngleRotation_right, real_inner_self_eq_norm_sq]
  exact this
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
a : ℝ := ↑(↑(basisRightAngleRotation o x hx).repr y) 0
b : ℝ := ↑(↑(basisRightAngleRotation o x hx).repr y) 1
this : 0 ≤ a * ‖x‖ ^ 2 ∧ b * ‖x‖ ^ 2 = 0 → SameRay ℝ x (a • x + b • ↑(rightAngleRotation o) x)
⊢ 0 ≤ inner x y ∧ ↑(↑(areaForm o) x) y = 0 → SameRay ℝ x y
[PROOFSTEP]
rw [← (o.basisRightAngleRotation x hx).sum_repr y]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
a : ℝ := ↑(↑(basisRightAngleRotation o x hx).repr y) 0
b : ℝ := ↑(↑(basisRightAngleRotation o x hx).repr y) 1
this : 0 ≤ a * ‖x‖ ^ 2 ∧ b * ‖x‖ ^ 2 = 0 → SameRay ℝ x (a • x + b • ↑(rightAngleRotation o) x)
⊢ 0 ≤
        inner x
          (Finset.sum Finset.univ fun i =>
            ↑(↑(basisRightAngleRotation o x hx).repr y) i • ↑(basisRightAngleRotation o x hx) i) ∧
      ↑(↑(areaForm o) x)
          (Finset.sum Finset.univ fun i =>
            ↑(↑(basisRightAngleRotation o x hx).repr y) i • ↑(basisRightAngleRotation o x hx) i) =
        0 →
    SameRay ℝ x
      (Finset.sum Finset.univ fun i =>
        ↑(↑(basisRightAngleRotation o x hx).repr y) i • ↑(basisRightAngleRotation o x hx) i)
[PROOFSTEP]
simp only [Fin.sum_univ_succ, coe_basisRightAngleRotation, Matrix.cons_val_zero, Fin.succ_zero_eq_one',
  Fintype.univ_of_isEmpty, Finset.sum_empty, areaForm_apply_self, map_smul, map_add, real_inner_smul_right,
  inner_add_right, Matrix.cons_val_one, Matrix.head_cons, Algebra.id.smul_eq_mul, areaForm_rightAngleRotation_right,
  mul_zero, add_zero, zero_add, neg_zero, inner_rightAngleRotation_right, real_inner_self_eq_norm_sq]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
a : ℝ := ↑(↑(basisRightAngleRotation o x hx).repr y) 0
b : ℝ := ↑(↑(basisRightAngleRotation o x hx).repr y) 1
this : 0 ≤ a * ‖x‖ ^ 2 ∧ b * ‖x‖ ^ 2 = 0 → SameRay ℝ x (a • x + b • ↑(rightAngleRotation o) x)
⊢ 0 ≤ ↑(↑(basisRightAngleRotation o x hx).repr y) 0 * ‖x‖ ^ 2 ∧
      ↑(↑(basisRightAngleRotation o x hx).repr y) 1 * ‖x‖ ^ 2 = 0 →
    SameRay ℝ x
      (↑(↑(basisRightAngleRotation o x hx).repr y) 0 • x +
        ↑(↑(basisRightAngleRotation o x hx).repr y) 1 • ↑(rightAngleRotation o) x)
[PROOFSTEP]
exact this
[GOAL]
case neg.mp
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
a : ℝ := ↑(↑(basisRightAngleRotation o x hx).repr y) 0
b : ℝ := ↑(↑(basisRightAngleRotation o x hx).repr y) 1
⊢ 0 ≤ a * ‖x‖ ^ 2 ∧ b * ‖x‖ ^ 2 = 0 → SameRay ℝ x (a • x + b • ↑(rightAngleRotation o) x)
[PROOFSTEP]
rintro ⟨ha, hb⟩
[GOAL]
case neg.mp.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
a : ℝ := ↑(↑(basisRightAngleRotation o x hx).repr y) 0
b : ℝ := ↑(↑(basisRightAngleRotation o x hx).repr y) 1
ha : 0 ≤ a * ‖x‖ ^ 2
hb : b * ‖x‖ ^ 2 = 0
⊢ SameRay ℝ x (a • x + b • ↑(rightAngleRotation o) x)
[PROOFSTEP]
have hx' : 0 < ‖x‖ := by simpa using hx
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
a : ℝ := ↑(↑(basisRightAngleRotation o x hx).repr y) 0
b : ℝ := ↑(↑(basisRightAngleRotation o x hx).repr y) 1
ha : 0 ≤ a * ‖x‖ ^ 2
hb : b * ‖x‖ ^ 2 = 0
⊢ 0 < ‖x‖
[PROOFSTEP]
simpa using hx
[GOAL]
case neg.mp.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
a : ℝ := ↑(↑(basisRightAngleRotation o x hx).repr y) 0
b : ℝ := ↑(↑(basisRightAngleRotation o x hx).repr y) 1
ha : 0 ≤ a * ‖x‖ ^ 2
hb : b * ‖x‖ ^ 2 = 0
hx' : 0 < ‖x‖
⊢ SameRay ℝ x (a • x + b • ↑(rightAngleRotation o) x)
[PROOFSTEP]
have ha' : 0 ≤ a := nonneg_of_mul_nonneg_left ha (by positivity)
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
a : ℝ := ↑(↑(basisRightAngleRotation o x hx).repr y) 0
b : ℝ := ↑(↑(basisRightAngleRotation o x hx).repr y) 1
ha : 0 ≤ a * ‖x‖ ^ 2
hb : b * ‖x‖ ^ 2 = 0
hx' : 0 < ‖x‖
⊢ 0 < ‖x‖ ^ 2
[PROOFSTEP]
positivity
[GOAL]
case neg.mp.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
a : ℝ := ↑(↑(basisRightAngleRotation o x hx).repr y) 0
b : ℝ := ↑(↑(basisRightAngleRotation o x hx).repr y) 1
ha : 0 ≤ a * ‖x‖ ^ 2
hb : b * ‖x‖ ^ 2 = 0
hx' : 0 < ‖x‖
ha' : 0 ≤ a
⊢ SameRay ℝ x (a • x + b • ↑(rightAngleRotation o) x)
[PROOFSTEP]
have hb' : b = 0 := eq_zero_of_ne_zero_of_mul_right_eq_zero (pow_ne_zero 2 hx'.ne') hb
[GOAL]
case neg.mp.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
a : ℝ := ↑(↑(basisRightAngleRotation o x hx).repr y) 0
b : ℝ := ↑(↑(basisRightAngleRotation o x hx).repr y) 1
ha : 0 ≤ a * ‖x‖ ^ 2
hb : b * ‖x‖ ^ 2 = 0
hx' : 0 < ‖x‖
ha' : 0 ≤ a
hb' : b = 0
⊢ SameRay ℝ x (a • x + b • ↑(rightAngleRotation o) x)
[PROOFSTEP]
simpa [hb'] using SameRay.sameRay_nonneg_smul_right x ha'
[GOAL]
case neg.mpr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
⊢ SameRay ℝ x y → 0 ≤ inner x y ∧ ↑(↑(areaForm o) x) y = 0
[PROOFSTEP]
intro h
[GOAL]
case neg.mpr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
h : SameRay ℝ x y
⊢ 0 ≤ inner x y ∧ ↑(↑(areaForm o) x) y = 0
[PROOFSTEP]
obtain ⟨r, hr, rfl⟩ := h.exists_nonneg_left hx
[GOAL]
case neg.mpr.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : ¬x = 0
r : ℝ
hr : 0 ≤ r
h : SameRay ℝ x (r • x)
⊢ 0 ≤ inner x (r • x) ∧ ↑(↑(areaForm o) x) (r • x) = 0
[PROOFSTEP]
simp only [inner_smul_right, real_inner_self_eq_norm_sq, LinearMap.map_smulₛₗ, areaForm_apply_self,
  Algebra.id.smul_eq_mul, mul_zero, eq_self_iff_true, and_true_iff]
[GOAL]
case neg.mpr.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
hx : ¬x = 0
r : ℝ
hr : 0 ≤ r
h : SameRay ℝ x (r • x)
⊢ 0 ≤ r * ‖x‖ ^ 2
[PROOFSTEP]
positivity
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ↑(↑(kahler o) x) y = ↑(starRingEnd ((fun x => ℂ) x)) (↑(↑(kahler o) y) x)
[PROOFSTEP]
have : ∀ r : ℝ, Complex.ofReal' r = @IsROrC.ofReal ℂ _ r := fun r => rfl
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
this : ∀ (r : ℝ), ↑r = ↑r
⊢ ↑(↑(kahler o) x) y = ↑(starRingEnd ((fun x => ℂ) x)) (↑(↑(kahler o) y) x)
[PROOFSTEP]
simp only [kahler_apply_apply]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
this : ∀ (r : ℝ), ↑r = ↑r
⊢ ↑(inner x y) + ↑(↑(areaForm o) x) y • Complex.I = ↑(starRingEnd ℂ) (↑(inner y x) + ↑(↑(areaForm o) y) x • Complex.I)
[PROOFSTEP]
rw [real_inner_comm, areaForm_swap]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
this : ∀ (r : ℝ), ↑r = ↑r
⊢ ↑(inner y x) + -↑(↑(areaForm o) y) x • Complex.I = ↑(starRingEnd ℂ) (↑(inner y x) + ↑(↑(areaForm o) y) x • Complex.I)
[PROOFSTEP]
simp [this]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ ↑(↑(kahler o) x) x = ↑(‖x‖ ^ 2)
[PROOFSTEP]
simp [kahler_apply_apply, real_inner_self_eq_norm_sq]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ↑(↑(kahler o) (↑(rightAngleRotation o) x)) y = -Complex.I * ↑(↑(kahler o) x) y
[PROOFSTEP]
simp only [o.areaForm_rightAngleRotation_left, o.inner_rightAngleRotation_left, o.kahler_apply_apply,
  Complex.ofReal_neg, Complex.real_smul]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ↑(↑(↑(areaForm o) x) y) + -↑(inner x y) * Complex.I =
    -Complex.I * (↑(inner x y) + ↑(↑(↑(areaForm o) x) y) * Complex.I)
[PROOFSTEP]
linear_combination ω x y * Complex.I_sq
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ↑(↑(kahler o) x) (↑(rightAngleRotation o) y) = Complex.I * ↑(↑(kahler o) x) y
[PROOFSTEP]
simp only [o.areaForm_rightAngleRotation_right, o.inner_rightAngleRotation_right, o.kahler_apply_apply,
  Complex.ofReal_neg, Complex.real_smul]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ -↑(↑(↑(areaForm o) x) y) + ↑(inner x y) * Complex.I = Complex.I * (↑(inner x y) + ↑(↑(↑(areaForm o) x) y) * Complex.I)
[PROOFSTEP]
linear_combination -ω x y * Complex.I_sq
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ↑(↑(kahler o) (↑(rightAngleRotation o) x)) (↑(rightAngleRotation o) y) = ↑(↑(kahler o) x) y
[PROOFSTEP]
simp only [kahler_rightAngleRotation_left, kahler_rightAngleRotation_right]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ Complex.I * (-Complex.I * ↑(↑(kahler o) x) y) = ↑(↑(kahler o) x) y
[PROOFSTEP]
linear_combination -o.kahler x y * Complex.I_sq
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ -(Complex.I * (Complex.I * ↑(↑(kahler o) x) y)) = ↑(↑(kahler o) x) y
[PROOFSTEP]
linear_combination -o.kahler x y * Complex.I_sq
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ↑(↑(kahler (-o)) x) y = ↑(starRingEnd ((fun x => ℂ) y)) (↑(↑(kahler o) x) y)
[PROOFSTEP]
have : ∀ r : ℝ, Complex.ofReal' r = @IsROrC.ofReal ℂ _ r := fun r => rfl
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
this : ∀ (r : ℝ), ↑r = ↑r
⊢ ↑(↑(kahler (-o)) x) y = ↑(starRingEnd ((fun x => ℂ) y)) (↑(↑(kahler o) x) y)
[PROOFSTEP]
simp [kahler_apply_apply, this]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ ↑(↑(kahler o) x) a * ↑(↑(kahler o) a) y = ↑(‖a‖ ^ 2) * ↑(↑(kahler o) x) y
[PROOFSTEP]
trans (↑(‖a‖ ^ 2) : ℂ) * o.kahler x y
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ ↑(↑(kahler o) x) a * ↑(↑(kahler o) a) y = ↑(‖a‖ ^ 2) * ↑(↑(kahler o) x) y
[PROOFSTEP]
ext
[GOAL]
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ (↑(↑(kahler o) x) a * ↑(↑(kahler o) a) y).re = (↑(‖a‖ ^ 2) * ↑(↑(kahler o) x) y).re
[PROOFSTEP]
simp only [o.kahler_apply_apply, Complex.add_im, Complex.add_re, Complex.I_im, Complex.I_re, Complex.mul_im,
  Complex.mul_re, Complex.ofReal_im, Complex.ofReal_re, Complex.real_smul]
[GOAL]
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ (inner x a + (↑(↑(areaForm o) x) a * 0 - 0 * 1)) * (inner a y + (↑(↑(areaForm o) a) y * 0 - 0 * 1)) -
      (0 + (↑(↑(areaForm o) x) a * 1 + 0 * 0)) * (0 + (↑(↑(areaForm o) a) y * 1 + 0 * 0)) =
    ‖a‖ ^ 2 * (inner x y + (↑(↑(areaForm o) x) y * 0 - 0 * 1)) - 0 * (0 + (↑(↑(areaForm o) x) y * 1 + 0 * 0))
[PROOFSTEP]
rw [real_inner_comm a x, o.areaForm_swap x a]
[GOAL]
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ (inner a x + (-↑(↑(areaForm o) a) x * 0 - 0 * 1)) * (inner a y + (↑(↑(areaForm o) a) y * 0 - 0 * 1)) -
      (0 + (-↑(↑(areaForm o) a) x * 1 + 0 * 0)) * (0 + (↑(↑(areaForm o) a) y * 1 + 0 * 0)) =
    ‖a‖ ^ 2 * (inner x y + (↑(↑(areaForm o) x) y * 0 - 0 * 1)) - 0 * (0 + (↑(↑(areaForm o) x) y * 1 + 0 * 0))
[PROOFSTEP]
linear_combination o.inner_mul_inner_add_areaForm_mul_areaForm a x y
[GOAL]
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ (↑(↑(kahler o) x) a * ↑(↑(kahler o) a) y).im = (↑(‖a‖ ^ 2) * ↑(↑(kahler o) x) y).im
[PROOFSTEP]
simp only [o.kahler_apply_apply, Complex.add_im, Complex.add_re, Complex.I_im, Complex.I_re, Complex.mul_im,
  Complex.mul_re, Complex.ofReal_im, Complex.ofReal_re, Complex.real_smul]
[GOAL]
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ (inner x a + (↑(↑(areaForm o) x) a * 0 - 0 * 1)) * (0 + (↑(↑(areaForm o) a) y * 1 + 0 * 0)) +
      (0 + (↑(↑(areaForm o) x) a * 1 + 0 * 0)) * (inner a y + (↑(↑(areaForm o) a) y * 0 - 0 * 1)) =
    ‖a‖ ^ 2 * (0 + (↑(↑(areaForm o) x) y * 1 + 0 * 0)) + 0 * (inner x y + (↑(↑(areaForm o) x) y * 0 - 0 * 1))
[PROOFSTEP]
rw [real_inner_comm a x, o.areaForm_swap x a]
[GOAL]
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ (inner a x + (-↑(↑(areaForm o) a) x * 0 - 0 * 1)) * (0 + (↑(↑(areaForm o) a) y * 1 + 0 * 0)) +
      (0 + (-↑(↑(areaForm o) a) x * 1 + 0 * 0)) * (inner a y + (↑(↑(areaForm o) a) y * 0 - 0 * 1)) =
    ‖a‖ ^ 2 * (0 + (↑(↑(areaForm o) x) y * 1 + 0 * 0)) + 0 * (inner x y + (↑(↑(areaForm o) x) y * 0 - 0 * 1))
[PROOFSTEP]
linear_combination o.inner_mul_areaForm_sub a x y
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
a x y : E
⊢ ↑(‖a‖ ^ 2) * ↑(↑(kahler o) x) y = ↑(‖a‖ ^ 2) * ↑(↑(kahler o) x) y
[PROOFSTEP]
norm_cast
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ↑Complex.normSq (↑(↑(kahler o) x) y) = ‖x‖ ^ 2 * ‖y‖ ^ 2
[PROOFSTEP]
simpa [kahler_apply_apply, Complex.normSq, sq] using o.inner_sq_add_areaForm_sq x y
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ↑Complex.abs (↑(↑(kahler o) x) y) = ‖x‖ * ‖y‖
[PROOFSTEP]
rw [← sq_eq_sq, Complex.sq_abs]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ↑Complex.normSq (↑(↑(kahler o) x) y) = (‖x‖ * ‖y‖) ^ 2
[PROOFSTEP]
linear_combination o.normSq_kahler x y
[GOAL]
case ha
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ 0 ≤ ↑Complex.abs (↑(↑(kahler o) x) y)
[PROOFSTEP]
positivity
[GOAL]
case hb
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ 0 ≤ ‖x‖ * ‖y‖
[PROOFSTEP]
positivity
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ‖↑(↑(kahler o) x) y‖ = ‖x‖ * ‖y‖
[PROOFSTEP]
simpa using o.abs_kahler x y
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ↑(↑(kahler o) x) y = 0
⊢ x = 0 ∨ y = 0
[PROOFSTEP]
have : ‖x‖ * ‖y‖ = 0 := by simpa [hx] using (o.norm_kahler x y).symm
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ↑(↑(kahler o) x) y = 0
⊢ ‖x‖ * ‖y‖ = 0
[PROOFSTEP]
simpa [hx] using (o.norm_kahler x y).symm
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ↑(↑(kahler o) x) y = 0
this : ‖x‖ * ‖y‖ = 0
⊢ x = 0 ∨ y = 0
[PROOFSTEP]
cases' eq_zero_or_eq_zero_of_mul_eq_zero this with h h
[GOAL]
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ↑(↑(kahler o) x) y = 0
this : ‖x‖ * ‖y‖ = 0
h : ‖x‖ = 0
⊢ x = 0 ∨ y = 0
[PROOFSTEP]
left
[GOAL]
case inl.h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ↑(↑(kahler o) x) y = 0
this : ‖x‖ * ‖y‖ = 0
h : ‖x‖ = 0
⊢ x = 0
[PROOFSTEP]
simpa using h
[GOAL]
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ↑(↑(kahler o) x) y = 0
this : ‖x‖ * ‖y‖ = 0
h : ‖y‖ = 0
⊢ x = 0 ∨ y = 0
[PROOFSTEP]
right
[GOAL]
case inr.h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ↑(↑(kahler o) x) y = 0
this : ‖x‖ * ‖y‖ = 0
h : ‖y‖ = 0
⊢ y = 0
[PROOFSTEP]
simpa using h
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ↑(↑(kahler o) x) y = 0 ↔ x = 0 ∨ y = 0
[PROOFSTEP]
refine' ⟨o.eq_zero_or_eq_zero_of_kahler_eq_zero, _⟩
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ x = 0 ∨ y = 0 → ↑(↑(kahler o) x) y = 0
[PROOFSTEP]
rintro (rfl | rfl)
[GOAL]
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
y : E
⊢ ↑(↑(kahler o) 0) y = 0
[PROOFSTEP]
simp
[GOAL]
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ ↑(↑(kahler o) x) 0 = 0
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑(↑(kahler o) x) y ≠ 0
[PROOFSTEP]
apply mt o.eq_zero_or_eq_zero_of_kahler_eq_zero
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : x ≠ 0
hy : y ≠ 0
⊢ ¬(x = 0 ∨ y = 0)
[PROOFSTEP]
tauto
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ↑(↑(kahler o) x) y ≠ 0 ↔ x ≠ 0 ∧ y ≠ 0
[PROOFSTEP]
refine' ⟨_, fun h => o.kahler_ne_zero h.1 h.2⟩
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ↑(↑(kahler o) x) y ≠ 0 → x ≠ 0 ∧ y ≠ 0
[PROOFSTEP]
contrapose
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ¬(x ≠ 0 ∧ y ≠ 0) → ¬↑(↑(kahler o) x) y ≠ 0
[PROOFSTEP]
simp only [not_and_or, Classical.not_not, kahler_apply_apply, Complex.real_smul]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ x = 0 ∨ y = 0 → ↑(inner x y) + ↑(↑(↑(areaForm o) x) y) * Complex.I = 0
[PROOFSTEP]
rintro (rfl | rfl)
[GOAL]
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
y : E
⊢ ↑(inner 0 y) + ↑(↑(↑(areaForm o) 0) y) * Complex.I = 0
[PROOFSTEP]
simp
[GOAL]
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ ↑(inner x 0) + ↑(↑(↑(areaForm o) x) 0) * Complex.I = 0
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ ↑(↑(kahler (↑(map (Fin 2) φ.toLinearEquiv) o)) x) y =
    ↑(↑(kahler o) (↑(LinearIsometryEquiv.symm φ) x)) (↑(LinearIsometryEquiv.symm φ) y)
[PROOFSTEP]
simp [kahler_apply_apply, areaForm_map]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
x y : E
⊢ ↑(↑(kahler o) (↑φ x)) (↑φ y) = ↑(↑(kahler o) x) y
[PROOFSTEP]
simp [kahler_apply_apply, o.areaForm_comp_linearIsometryEquiv φ hφ]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
w z : ℂ
⊢ ↑(↑(Orientation.areaForm Complex.orientation) w) z = (↑(starRingEnd ℂ) w * z).im
[PROOFSTEP]
let o := Complex.orientation
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o✝ : Orientation ℝ E (Fin 2)
w z : ℂ
o : Orientation ℝ ℂ (Fin 2) := Complex.orientation
⊢ ↑(↑(Orientation.areaForm Complex.orientation) w) z = (↑(starRingEnd ℂ) w * z).im
[PROOFSTEP]
simp only [o.areaForm_to_volumeForm, o.volumeForm_robust Complex.orthonormalBasisOneI rfl, (Basis.det_apply),
  Matrix.det_fin_two, (Basis.toMatrix_apply), toBasis_orthonormalBasisOneI, Matrix.cons_val_zero, coe_basisOneI_repr,
  Matrix.cons_val_one, Matrix.head_cons, mul_im, conj_re, conj_im]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o✝ : Orientation ℝ E (Fin 2)
w z : ℂ
o : Orientation ℝ ℂ (Fin 2) := Complex.orientation
⊢ w.re * z.im - z.re * w.im = w.re * z.im + -w.im * z.re
[PROOFSTEP]
ring
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
z : ℂ
⊢ ↑(Orientation.rightAngleRotation Complex.orientation) z = I * z
[PROOFSTEP]
apply ext_inner_right ℝ
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
z : ℂ
⊢ ∀ (v : ℂ), inner (↑(Orientation.rightAngleRotation Complex.orientation) z) v = inner (I * z) v
[PROOFSTEP]
intro w
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
z w : ℂ
⊢ inner (↑(Orientation.rightAngleRotation Complex.orientation) z) w = inner (I * z) w
[PROOFSTEP]
rw [Orientation.inner_rightAngleRotation_left]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
z w : ℂ
⊢ ↑(↑(Orientation.areaForm Complex.orientation) z) w = inner (I * z) w
[PROOFSTEP]
simp only [Complex.areaForm, Complex.inner, mul_re, mul_im, conj_re, conj_im, map_mul, conj_I, neg_re, neg_im, I_re,
  I_im]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
z w : ℂ
⊢ z.re * w.im + -z.im * w.re = (-0 * z.re - -1 * -z.im) * w.re - (-0 * -z.im + -1 * z.re) * w.im
[PROOFSTEP]
ring
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
w z : ℂ
⊢ ↑(↑(Orientation.kahler Complex.orientation) w) z = ↑(starRingEnd ℂ) w * z
[PROOFSTEP]
rw [Orientation.kahler_apply_apply]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
w z : ℂ
⊢ ↑(inner w z) + ↑(↑(Orientation.areaForm Complex.orientation) w) z • I = ↑(starRingEnd ℂ) w * z
[PROOFSTEP]
ext1
[GOAL]
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
w z : ℂ
⊢ (↑(inner w z) + ↑(↑(Orientation.areaForm Complex.orientation) w) z • I).re = (↑(starRingEnd ℂ) w * z).re
[PROOFSTEP]
simp
[GOAL]
case a
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
w z : ℂ
⊢ (↑(inner w z) + ↑(↑(Orientation.areaForm Complex.orientation) w) z • I).im = (↑(starRingEnd ℂ) w * z).im
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf : ↑(map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x y : E
⊢ ↑(↑(areaForm o) x) y = (↑(starRingEnd ℂ) (↑f x) * ↑f y).im
[PROOFSTEP]
rw [← Complex.areaForm, ← hf, areaForm_map (hF := _)]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf : ↑(map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x y : E
⊢ ↑(↑(areaForm o) x) y = ↑(↑(areaForm o) (↑(LinearIsometryEquiv.symm f) (↑f x))) (↑(LinearIsometryEquiv.symm f) (↑f y))
[PROOFSTEP]
iterate 2 rw [LinearIsometryEquiv.symm_apply_apply]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf : ↑(map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x y : E
⊢ ↑(↑(areaForm o) x) y = ↑(↑(areaForm o) (↑(LinearIsometryEquiv.symm f) (↑f x))) (↑(LinearIsometryEquiv.symm f) (↑f y))
[PROOFSTEP]
rw [LinearIsometryEquiv.symm_apply_apply]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf : ↑(map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x y : E
⊢ ↑(↑(areaForm o) x) y = ↑(↑(areaForm o) x) (↑(LinearIsometryEquiv.symm f) (↑f y))
[PROOFSTEP]
rw [LinearIsometryEquiv.symm_apply_apply]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf : ↑(map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x : E
⊢ ↑f (↑(rightAngleRotation o) x) = I * ↑f x
[PROOFSTEP]
rw [← Complex.rightAngleRotation, ← hf, rightAngleRotation_map (hF := _), LinearIsometryEquiv.symm_apply_apply]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf : ↑(map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x y : E
⊢ ↑(↑(kahler o) x) y = ↑(starRingEnd ℂ) (↑f x) * ↑f y
[PROOFSTEP]
rw [← Complex.kahler, ← hf, kahler_map (hF := _)]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf : ↑(map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x y : E
⊢ ↑(↑(kahler o) x) y = ↑(↑(kahler o) (↑(LinearIsometryEquiv.symm f) (↑f x))) (↑(LinearIsometryEquiv.symm f) (↑f y))
[PROOFSTEP]
iterate 2 rw [LinearIsometryEquiv.symm_apply_apply]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf : ↑(map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x y : E
⊢ ↑(↑(kahler o) x) y = ↑(↑(kahler o) (↑(LinearIsometryEquiv.symm f) (↑f x))) (↑(LinearIsometryEquiv.symm f) (↑f y))
[PROOFSTEP]
rw [LinearIsometryEquiv.symm_apply_apply]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf : ↑(map (Fin 2) f.toLinearEquiv) o = Complex.orientation
x y : E
⊢ ↑(↑(kahler o) x) y = ↑(↑(kahler o) x) (↑(LinearIsometryEquiv.symm f) (↑f y))
[PROOFSTEP]
rw [LinearIsometryEquiv.symm_apply_apply]


[GOAL]
M : Type u_1
G : Type u_2
α : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Group G
inst✝³ : TopologicalSpace α
inst✝² : MulAction M α
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul M α
⊢ IsMinimal M α ↔ ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ
[PROOFSTEP]
constructor
[GOAL]
case mp
M : Type u_1
G : Type u_2
α : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Group G
inst✝³ : TopologicalSpace α
inst✝² : MulAction M α
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul M α
⊢ IsMinimal M α → ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ
[PROOFSTEP]
intro _ _
[GOAL]
case mp
M : Type u_1
G : Type u_2
α : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Group G
inst✝³ : TopologicalSpace α
inst✝² : MulAction M α
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul M α
a✝ : IsMinimal M α
s✝ : Set α
⊢ IsClosed s✝ → (∀ (c : M), c • s✝ ⊆ s✝) → s✝ = ∅ ∨ s✝ = univ
[PROOFSTEP]
exact eq_empty_or_univ_of_smul_invariant_closed M
[GOAL]
case mpr
M : Type u_1
G : Type u_2
α : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Group G
inst✝³ : TopologicalSpace α
inst✝² : MulAction M α
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul M α
⊢ (∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ) → IsMinimal M α
[PROOFSTEP]
refine' fun H ↦ ⟨fun _ ↦ dense_iff_closure_eq.2 <| (H _ _ _).resolve_left _⟩
[GOAL]
case mpr.refine'_1
M : Type u_1
G : Type u_2
α : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Group G
inst✝³ : TopologicalSpace α
inst✝² : MulAction M α
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul M α
H : ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ
x✝ : α
⊢ IsClosed (closure (orbit M x✝))
case mpr.refine'_2
M : Type u_1
G : Type u_2
α : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Group G
inst✝³ : TopologicalSpace α
inst✝² : MulAction M α
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul M α
H : ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ
x✝ : α
⊢ ∀ (c : M), c • closure (orbit M x✝) ⊆ closure (orbit M x✝)
case mpr.refine'_3
M : Type u_1
G : Type u_2
α : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Group G
inst✝³ : TopologicalSpace α
inst✝² : MulAction M α
inst✝¹ : MulAction G α
inst✝ : ContinuousConstSMul M α
H : ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ
x✝ : α
⊢ ¬closure (orbit M x✝) = ∅
[PROOFSTEP]
exacts [isClosed_closure, fun _ ↦ smul_closure_orbit_subset _ _, (orbit_nonempty _).closure.ne_empty]


[GOAL]
α : Type u
β : Type v
f fa g : α → α
x✝ y : α
fb : β → β
m n k : ℕ
e : Perm α
x : α
hx : IsFixedPt f x
⊢ IsFixedPt f (f x)
[PROOFSTEP]
convert hx
[GOAL]
α : Type u
β : Type v
f fa g : α → α
x y : α
fb : β → β
m n✝ k : ℕ
e : Perm α
s : Set α
h : IsFixedPt (Set.preimage f) s
n : ℕ
⊢ IsFixedPt (Set.preimage f^[n]) s
[PROOFSTEP]
rw [Set.preimage_iterate_eq]
[GOAL]
α : Type u
β : Type v
f fa g : α → α
x y : α
fb : β → β
m n✝ k : ℕ
e : Perm α
s : Set α
h : IsFixedPt (Set.preimage f) s
n : ℕ
⊢ IsFixedPt (Set.preimage f)^[n] s
[PROOFSTEP]
exact h.iterate n
[GOAL]
α : Type u
β : Type v
f fa g : α → α
x y : α
fb : β → β
m n✝ k : ℕ
e : Perm α
h : IsFixedPt (↑e) x
n : ℕ
⊢ IsFixedPt (↑(e ^ n)) x
[PROOFSTEP]
rw [Equiv.Perm.coe_pow]
[GOAL]
α : Type u
β : Type v
f fa g : α → α
x y : α
fb : β → β
m n✝ k : ℕ
e : Perm α
h : IsFixedPt (↑e) x
n : ℕ
⊢ IsFixedPt (↑e)^[n] x
[PROOFSTEP]
exact h.iterate _
[GOAL]
α✝ : Type u
β : Type v
f✝ fa g : α✝ → α✝
x✝ y : α✝
fb : β → β
m n k : ℕ
e : Perm α✝
α : Type u_1
f : α → α
x : α
⊢ x ∈ fixedPoints f ↔ f x = x
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
f fa g : α → α
x y : α
fb : β → β
m n k : ℕ
e : Perm α
x✝ : α
⊢ x✝ ∈ fixedPoints id ↔ x✝ ∈ Set.univ
[PROOFSTEP]
simpa using isFixedPt_id _
[GOAL]
α : Type u
β : Type v
f fa g : α → α
x y : α
fb : β → β
m n k : ℕ
e : Perm α
h : Function.Commute f g
⊢ Set.InvOn f g (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))
[PROOFSTEP]
simpa only [h.comp_eq] using Function.invOn_fixedPoints_comp f g
[GOAL]
α : Type u
β : Type v
f fa g : α → α
x y : α
fb : β → β
m n k : ℕ
e : Perm α
h : Function.Commute f g
⊢ Set.BijOn f (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))
[PROOFSTEP]
simpa only [h.comp_eq] using bijOn_fixedPoints_comp g f
[GOAL]
α : Type u
β : Type v
f fa g : α → α
x y : α
fb : β → β
m n k : ℕ
e : Perm α
h : Function.Commute f g
⊢ Set.BijOn g (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))
[PROOFSTEP]
simpa only [h.comp_eq] using bijOn_fixedPoints_comp f g


[GOAL]
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : α → α
x y : α
hy : Tendsto (fun n => f^[n] x) atTop (𝓝 y)
hf : ContinuousAt f y
⊢ IsFixedPt f y
[PROOFSTEP]
refine' tendsto_nhds_unique ((tendsto_add_atTop_iff_nat 1).1 _) hy
[GOAL]
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : α → α
x y : α
hy : Tendsto (fun n => f^[n] x) atTop (𝓝 y)
hf : ContinuousAt f y
⊢ Tendsto (fun n => f^[n + 1] x) atTop (𝓝 (f y))
[PROOFSTEP]
simp only [iterate_succ' f]
[GOAL]
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : α → α
x y : α
hy : Tendsto (fun n => f^[n] x) atTop (𝓝 y)
hf : ContinuousAt f y
⊢ Tendsto (fun n => (f ∘ f^[n]) x) atTop (𝓝 (f y))
[PROOFSTEP]
exact hf.tendsto.comp hy