awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
h : 0 = norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)
⊢ 0 ≤ ‖x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
h : 0 < norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)
⊢ norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) ≤ ‖x‖

Tactic:
le_of_mul_le_mul_right ?_ h

Premises used: le_of_mul_le_mul_right
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
h : 0 < norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)
refine_1 :
  norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) *
      norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) ≤
    ‖x‖ * norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)
⊢ norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) ≤ ‖x‖

Tactic:
refine le_of_mul_le_mul_right ?_ h

Premises used: le_of_mul_le_mul_right
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
h : 0 < norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)
refine_1 :
  (((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) ≤
    ‖x‖ * norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)
⊢ norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) *
      norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) ≤
    ‖x‖ * norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)

Tactic:
rw [← real_inner_self_eq_norm_mul_norm, o.inner_rightAngleRotationAux₁_left]

Premises used: real_inner_self_eq_norm_mul_norm, Orientation.inner_rightAngleRotationAux₁_left
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
h : 0 < norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)
⊢ (((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) ≤
    ‖x‖ * norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)

Tactic:
o.areaForm_le x (o.rightAngleRotationAux₁ x)

Premises used: Orientation.areaForm_le, Orientation.rightAngleRotationAux₁, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
h : 0 < norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)
⊢ (((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) ≤
    ‖x‖ * norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)

Tactic:
exact o.areaForm_le x (o.rightAngleRotationAux₁ x)

Premises used: Orientation.areaForm_le, Orientation.rightAngleRotationAux₁, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
K : Submodule ℝ E := ℝ ∙ x
apply : 0 < finrank.{0, u_1} ℝ ↥Kᗮ
⊢ Nontrivial.{u_1} ↥Kᗮ

Tactic:
apply nontrivial_of_finrank_pos (R := ℝ)

Premises used: Module.nontrivial_of_finrank_pos
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
K : Submodule ℝ E := ℝ ∙ x
rw : finrank.{0, u_1} ℝ ↥K ≤ Finset.card (α := E) (Set.toFinset {x})
⊢ finrank.{0, u_1} ℝ ↥K ≤ Finset.card (α := E) {x}

Tactic:
rw [← Set.toFinset_singleton]

Premises used: Set.toFinset_singleton
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
K : Submodule ℝ E := ℝ ∙ x
⊢ finrank.{0, u_1} ℝ ↥K ≤ Finset.card (α := E) (Set.toFinset {x})

Tactic:
finrank_span_le_card ({x} : Set E)

Premises used: Set.Mem, finrank_span_le_card, Singleton.singleton
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
K : Submodule ℝ E := ℝ ∙ x
⊢ finrank.{0, u_1} ℝ ↥K ≤ Finset.card (α := E) (Set.toFinset {x})

Tactic:
exact finrank_span_le_card ({x} : Set E)

Premises used: finrank_span_le_card, Singleton.singleton
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
K : Submodule ℝ E := ℝ ∙ x
⊢ finrank.{0, u_1} ℝ ↥K ≤ Finset.card (α := E) {x}

Tactic:
have : finrank ℝ K ≤ Finset.card {x} := by
            rw [← Set.toFinset_singleton]
            exact finrank_span_le_card ({x} : Set E)
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
K : Submodule ℝ E := ℝ ∙ x
this : finrank.{0, u_1} ℝ ↥K ≤ Finset.card (α := E) {x}
⊢ Finset.card (α := E) {x} = 1

Tactic:
have : Finset.card {x} = 1 := Finset.card_singleton x
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
K : Submodule ℝ E := ℝ ∙ x
this_1 : finrank.{0, u_1} ℝ ↥K ≤ Finset.card (α := E) {x}
this : Finset.card (α := E) {x} = 1
⊢ finrank.{0, u_1} ℝ ↥K + finrank.{0, u_1} ℝ ↥Kᗮ = finrank ℝ E

Tactic:
have : finrank ℝ K + finrank ℝ Kᗮ = finrank ℝ E := K.finrank_add_finrank_orthogonal
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
K : Submodule ℝ E := ℝ ∙ x
this_1 : finrank.{0, u_1} ℝ ↥K ≤ Finset.card (α := E) {x}
this_2 : Finset.card (α := E) {x} = 1
this : finrank.{0, u_1} ℝ ↥K + finrank.{0, u_1} ℝ ↥Kᗮ = finrank ℝ E
⊢ finrank ℝ E = 2

Tactic:
have : finrank ℝ E = 2 := Fact.out
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
K : Submodule ℝ E := ℝ ∙ x
this_1 : finrank.{0, u_1} ℝ ↥K ≤ Finset.card (α := E) {x}
this_2 : Finset.card (α := E) {x} = 1
this_3 : finrank.{0, u_1} ℝ ↥K + finrank.{0, u_1} ℝ ↥Kᗮ = finrank ℝ E
this : finrank ℝ E = 2
⊢ 0 < finrank.{0, u_1} ℝ ↥Kᗮ

Tactic:
lia
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
K : Submodule ℝ E := ℝ ∙ x
⊢ Nontrivial.{u_1} ↥Kᗮ

Tactic:
have : Nontrivial Kᗮ := by
          apply nontrivial_of_finrank_pos (R := ℝ)
          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
          lia
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
K : Submodule ℝ E := ℝ ∙ x
this : Nontrivial.{u_1} ↥Kᗮ
⊢ ∃ (w : ↥Kᗮ), w ≠ 0

Tactic:
exists_ne 0

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
K : Submodule ℝ E := ℝ ∙ x
this : Nontrivial.{u_1} ↥Kᗮ
refine_2 : ∀ (w : ↥Kᗮ) (hw₀ : w ≠ 0), ‖x‖ ≤ norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)
⊢ ‖x‖ ≤ norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)

Tactic:
obtain ⟨w, hw₀⟩ : ∃ w : Kᗮ, w ≠ 0 := exists_ne 0

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
K : Submodule ℝ E := ℝ ∙ x
this : Nontrivial.{u_1} ↥Kᗮ
w : ↥Kᗮ
hw₀ : w ≠ 0
⊢ ⟪x, (↑w : E)⟫ = 0

Tactic:
have hw' : ⟪x, (w : E)⟫ = 0 := Submodule.mem_orthogonal_singleton_iff_inner_right.mp w.2
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
K : Submodule ℝ E := ℝ ∙ x
this : Nontrivial.{u_1} ↥Kᗮ
w : ↥Kᗮ
hw₀ : w ≠ 0
hw' : ⟪x, (↑w : E)⟫ = 0
⊢ (↑w : E) ≠ 0

Tactic:
have hw : (w : E) ≠ 0 := fun h => hw₀ (Submodule.coe_eq_zero.mp h)
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
K : Submodule ℝ E := ℝ ∙ x
this : Nontrivial.{u_1} ↥Kᗮ
w : ↥Kᗮ
hw₀ : w ≠ 0
hw' : ⟪x, (↑w : E)⟫ = 0
hw : (↑w : E) ≠ 0
rwa rwa₁ rwa₂ rwa₃ : (↑w : E) ≠ 0
⊢ 0 < ‖(↑w : E)‖

Tactic:
rwa [norm_pos_iff]

Premises used: norm_pos_iff
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
K : Submodule ℝ E := ℝ ∙ x
this : Nontrivial.{u_1} ↥Kᗮ
w : ↥Kᗮ
hw₀ : w ≠ 0
hw' : ⟪x, (↑w : E)⟫ = 0
hw : (↑w : E) ≠ 0
refine_2 : ‖x‖ * ‖(↑w : E)‖ ≤ norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) * ‖(↑w : E)‖
⊢ ‖x‖ ≤ norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)

Tactic:
refine le_of_mul_le_mul_right ?_ (by rwa [norm_pos_iff] : 0 < ‖(w : E)‖)

Premises used: le_of_mul_le_mul_right
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
K : Submodule ℝ E := ℝ ∙ x
this : Nontrivial.{u_1} ↥Kᗮ
w : ↥Kᗮ
hw₀ : w ≠ 0
hw' : ⟪x, (↑w : E)⟫ = 0
hw : (↑w : E) ≠ 0
refine_2 :
  |(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) (↑w : E)| ≤
    norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) * ‖(↑w : E)‖
⊢ ‖x‖ * ‖(↑w : E)‖ ≤ norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) * ‖(↑w : E)‖

Tactic:
rw [← o.abs_areaForm_of_orthogonal hw']

Premises used: Orientation.abs_areaForm_of_orthogonal
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
K : Submodule ℝ E := ℝ ∙ x
this : Nontrivial.{u_1} ↥Kᗮ
w : ↥Kᗮ
hw₀ : w ≠ 0
hw' : ⟪x, (↑w : E)⟫ = 0
hw : (↑w : E) ≠ 0
refine_2 :
  |⟪(o.rightAngleRotationAux₁ : (a : E) → E) x, (↑w : E)⟫| ≤
    norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) * ‖(↑w : E)‖
⊢ |(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) (↑w : E)| ≤
    norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) * ‖(↑w : E)‖

Tactic:
rw [← o.inner_rightAngleRotationAux₁_left x w]

Premises used: Orientation.inner_rightAngleRotationAux₁_left, Subtype.val
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
K : Submodule ℝ E := ℝ ∙ x
this : Nontrivial.{u_1} ↥Kᗮ
w : ↥Kᗮ
hw₀ : w ≠ 0
hw' : ⟪x, (↑w : E)⟫ = 0
hw : (↑w : E) ≠ 0
⊢ |⟪(o.rightAngleRotationAux₁ : (a : E) → E) x, (↑w : E)⟫| ≤
    norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) * ‖(↑w : E)‖

Tactic:
abs_real_inner_le_norm (o.rightAngleRotationAux₁ x) w

Premises used: abs_real_inner_le_norm, Orientation.rightAngleRotationAux₁, Subtype.val, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
K : Submodule ℝ E := ℝ ∙ x
this : Nontrivial.{u_1} ↥Kᗮ
w : ↥Kᗮ
hw₀ : w ≠ 0
hw' : ⟪x, (↑w : E)⟫ = 0
hw : (↑w : E) ≠ 0
⊢ |⟪(o.rightAngleRotationAux₁ : (a : E) → E) x, (↑w : E)⟫| ≤
    norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) * ‖(↑w : E)‖

Tactic:
exact abs_real_inner_le_norm (o.rightAngleRotationAux₁ x) w

Premises used: abs_real_inner_le_norm, Orientation.rightAngleRotationAux₁, Subtype.val, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
apply :
  ∀ (v : E), ⟪v, (o.rightAngleRotationAux₁ : (a : E) → E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)⟫ = ⟪v, -x⟫
⊢ (o.rightAngleRotationAux₁ : (a : E) → E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) = -x

Tactic:
apply ext_inner_left ℝ

Premises used: Real, ext_inner_left
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ inner ℝ (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) y : E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) =
    ⟪y, x⟫

Tactic:
have : ⟪o.rightAngleRotationAux₁ y, o.rightAngleRotationAux₁ x⟫ = ⟪y, x⟫ :=
    LinearIsometry.inner_map_map o.rightAngleRotationAux₂ y x
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
this :
  inner ℝ (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) y : E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) =
    ⟪y, x⟫
rw :
  -(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) y : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) =
    ⟪y, -x⟫
rw₁ :
  -inner ℝ (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) y : E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) =
    ⟪y, -x⟫
rw₂ : -⟪y, x⟫ = ⟪y, -x⟫
rw₃ rw₄ : -⟪y, x⟫ = -⟪y, x⟫
⊢ ⟪y, (o.rightAngleRotationAux₁ : (a : E) → E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)⟫ = ⟪y, -x⟫

Tactic:
rw [o.inner_rightAngleRotationAux₁_right, ← o.inner_rightAngleRotationAux₁_left, this,
    inner_neg_right]

Premises used: inner_neg_right, Orientation.inner_rightAngleRotationAux₁_right, Orientation.inner_rightAngleRotationAux₁_left
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
h :
  ∀ (x : E),
    Eq (α := E) ((o.rightAngleRotationAux₂.toLinearMap ∘ₗ (-o.rightAngleRotationAux₁) : (a : E) → E) x : E)
      ((LinearMap.id : (a : E) → E) x : E)
⊢ o.rightAngleRotationAux₂.toLinearMap ∘ₗ (-o.rightAngleRotationAux₁) = LinearMap.id

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ Eq (α := E) ((o.rightAngleRotationAux₂.toLinearMap ∘ₗ (-o.rightAngleRotationAux₁) : (a : E) → E) x : E)
    ((LinearMap.id : (a : E) → E) x : E)

Tactic:
simp [rightAngleRotationAux₂]

Premises used: Orientation.rightAngleRotationAux₂
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
h :
  ∀ (x : E),
    Eq (α := E) (((-o.rightAngleRotationAux₁) ∘ₗ o.rightAngleRotationAux₂.toLinearMap : (a : E) → E) x : E)
      ((LinearMap.id : (a : E) → E) x : E)
⊢ (-o.rightAngleRotationAux₁) ∘ₗ o.rightAngleRotationAux₂.toLinearMap = LinearMap.id

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ Eq (α := E) (((-o.rightAngleRotationAux₁) ∘ₗ o.rightAngleRotationAux₂.toLinearMap : (a : E) → E) x : E)
    ((LinearMap.id : (a : E) → E) x : E)

Tactic:
simp [rightAngleRotationAux₂]

Premises used: Orientation.rightAngleRotationAux₂
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
rw :
  ⟪(LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯ : (a : E) → E) x, y⟫ =
    (((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y
⊢ ⟪(o.rightAngleRotation : (a : E) → E) x, y⟫ = (((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y

Tactic:
rw [rightAngleRotation]

Premises used: Orientation.rightAngleRotation
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ⟪(LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯ : (a : E) → E) x, y⟫ =
    (((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y

Tactic:
o.inner_rightAngleRotationAux₁_left x y

Premises used: Orientation.inner_rightAngleRotationAux₁_left
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ⟪(LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯ : (a : E) → E) x, y⟫ =
    (((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y

Tactic:
exact o.inner_rightAngleRotationAux₁_left x y

Premises used: Orientation.inner_rightAngleRotationAux₁_left
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
rw :
  ⟪x, (LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯ : (a : E) → E) y⟫ =
    -(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y
⊢ ⟪x, (o.rightAngleRotation : (a : E) → E) y⟫ = -(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y

Tactic:
rw [rightAngleRotation]

Premises used: Orientation.rightAngleRotation
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ⟪x, (LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯ : (a : E) → E) y⟫ =
    -(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y

Tactic:
o.inner_rightAngleRotationAux₁_right x y

Premises used: Orientation.inner_rightAngleRotationAux₁_right
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ⟪x, (LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯ : (a : E) → E) y⟫ =
    -(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y

Tactic:
exact o.inner_rightAngleRotationAux₁_right x y

Premises used: Orientation.inner_rightAngleRotationAux₁_right
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
rw :
  (LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯ : (a : E) → E)
      ((LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯ : (a : E) → E) x :
        E) =
    -x
⊢ (o.rightAngleRotation : (a : E) → E) ((o.rightAngleRotation : (a : E) → E) x : E) = -x

Tactic:
rw [rightAngleRotation]

Premises used: Orientation.rightAngleRotation
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ (LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯ : (a : E) → E)
      ((LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯ : (a : E) → E) x :
        E) =
    -x

Tactic:
o.rightAngleRotationAux₁_rightAngleRotationAux₁ x

Premises used: Orientation.rightAngleRotationAux₁_rightAngleRotationAux₁
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ (LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯ : (a : E) → E)
      ((LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯ : (a : E) → E) x :
        E) =
    -x

Tactic:
exact o.rightAngleRotationAux₁_rightAngleRotationAux₁ x

Premises used: Orientation.rightAngleRotationAux₁_rightAngleRotationAux₁
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
rw :
  Eq (α := E ≃ₗᵢ[ℝ] E)
    (LinearIsometryEquiv.symm
      (LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯))
    (LinearIsometryEquiv.trans
      (LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯)
      (LinearIsometryEquiv.neg ℝ))
⊢ o.rightAngleRotation.symm = o.rightAngleRotation.trans (LinearIsometryEquiv.neg ℝ)

Tactic:
rw [rightAngleRotation]

Premises used: Orientation.rightAngleRotation
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
⊢ Eq (α := E ≃ₗᵢ[ℝ] E)
    (LinearIsometryEquiv.symm
      (LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯))
    (LinearIsometryEquiv.trans
      (LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯)
      (LinearIsometryEquiv.neg ℝ))

Tactic:
LinearIsometryEquiv.toLinearIsometry_injective rfl

Premises used: LinearIsometryEquiv.toLinearIsometry_injective, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
⊢ Eq (α := E ≃ₗᵢ[ℝ] E)
    (LinearIsometryEquiv.symm
      (LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯))
    (LinearIsometryEquiv.trans
      (LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯)
      (LinearIsometryEquiv.neg ℝ))

Tactic:
exact LinearIsometryEquiv.toLinearIsometry_injective rfl

Premises used: LinearIsometryEquiv.toLinearIsometry_injective, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ ⟪(o.rightAngleRotation : (a : E) → E) x, x⟫ = 0

Tactic:
simp