-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem abs_areaForm_of_orthogonal {x y : E} (h : ⟪x, y⟫ = 0) : |ω x y| = ‖x‖ * ‖y‖

Proof state:
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
⊢ |(o.areaForm x) y| = ‖x‖ * ‖y‖

Tactic:
rw [o.areaForm_to_volumeForm, o.abs_volumeForm_apply_of_pairwise_orthogonal]

Result:
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 : Fin 2, ‖![x, y] i‖ = ‖x‖ * ‖y‖

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 (![x, y] i) (![x, y] j) = 0

Proof state:
case «1».«0»
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 : (fun i => i) ⟨1, ⋯⟩ ≠ (fun i => i) ⟨0, ⋯⟩
⊢ inner (![x, y] ((fun i => i) ⟨1, ⋯⟩)) (![x, y] ((fun i => i) ⟨0, ⋯⟩)) = 0

Tactic:
simpa [real_inner_comm] using h

Result:
no goals

Proof state:
case «1».«1»
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 : (fun i => i) ⟨1, ⋯⟩ ≠ (fun i => i) ⟨1, ⋯⟩
⊢ inner (![x, y] ((fun i => i) ⟨1, ⋯⟩)) (![x, y] ((fun i => i) ⟨1, ⋯⟩)) = 0

Tactic:
simp_all

Result:
no goals

Proof state:
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 (![x, y] i) (![x, y] j) = 0

Tactic:
intro i j hij

Result:
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 (![x, y] i) (![x, y] j) = 0

Proof state:
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 (![x, y] i) (![x, y] j) = 0

Tactic:
fin_cases i <;> fin_cases j

Result:
case «0».«0»
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 : (fun i => i) ⟨0, ⋯⟩ ≠ (fun i => i) ⟨0, ⋯⟩
⊢ inner (![x, y] ((fun i => i) ⟨0, ⋯⟩)) (![x, y] ((fun i => i) ⟨0, ⋯⟩)) = 0

case «0».«1»
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 : (fun i => i) ⟨0, ⋯⟩ ≠ (fun i => i) ⟨1, ⋯⟩
⊢ inner (![x, y] ((fun i => i) ⟨0, ⋯⟩)) (![x, y] ((fun i => i) ⟨1, ⋯⟩)) = 0

case «1».«0»
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 : (fun i => i) ⟨1, ⋯⟩ ≠ (fun i => i) ⟨0, ⋯⟩
⊢ inner (![x, y] ((fun i => i) ⟨1, ⋯⟩)) (![x, y] ((fun i => i) ⟨0, ⋯⟩)) = 0

case «1».«1»
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 : (fun i => i) ⟨1, ⋯⟩ ≠ (fun i => i) ⟨1, ⋯⟩
⊢ inner (![x, y] ((fun i => i) ⟨1, ⋯⟩)) (![x, y] ((fun i => i) ⟨1, ⋯⟩)) = 0

Proof state:
case «0».«1»
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 : (fun i => i) ⟨0, ⋯⟩ ≠ (fun i => i) ⟨1, ⋯⟩
⊢ inner (![x, y] ((fun i => i) ⟨0, ⋯⟩)) (![x, y] ((fun i => i) ⟨1, ⋯⟩)) = 0

Tactic:
simpa using h

Result:
no goals

Proof state:
case «0».«0»
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 : (fun i => i) ⟨0, ⋯⟩ ≠ (fun i => i) ⟨0, ⋯⟩
⊢ inner (![x, y] ((fun i => i) ⟨0, ⋯⟩)) (![x, y] ((fun i => i) ⟨0, ⋯⟩)) = 0

Tactic:
simp_all

Result:
no goals

Proof state:
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 : Fin 2, ‖![x, y] i‖ = ‖x‖ * ‖y‖

Tactic:
simp [Fin.prod_univ_succ]

Result:
no goals