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 y : E
h : ![x, y] = ![y, x] ∘ (⇑(Equiv.swap 0 1) : (a : Fin 2) → Fin 2)
convert! : Ne (α := Fin 2) 0 1
⊢ Eq (α := ℝ) ((o.volumeForm : (a : Fin 2 → E) → ℝ) ![x, y] : ℝ) (-(o.volumeForm : (a : Fin 2 → E) → ℝ) ![y, x] : ℝ)

Tactic:
convert! o.volumeForm.map_swap ![y, x] (_ : (0 : Fin 2) ≠ 1)

Premises used: Matrix.vecEmpty, AlternatingMap.map_swap, Matrix.vecCons, Orientation.volumeForm
-- 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
h : ∀ (i : Fin (Nat.succ 1)), ![x, y] i = (![y, x] ∘ (⇑(Equiv.swap 0 1) : (a : Fin 2) → Fin 2)) i
⊢ ![x, y] = ![y, x] ∘ (⇑(Equiv.swap 0 1) : (a : Fin 2) → Fin 2)

Tactic:
ext i
-- 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
i : Fin (Nat.succ 1)
h :
  ![x, y] ((fun (i : Fin (Nat.succ 1)) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 1))) =
    Function.comp (α := Fin 2) ![y, x] (⇑(Equiv.swap 0 1) : (a : Fin 2) → Fin 2)
      ((fun (i : Fin (Nat.succ 1)) ↦ i) ⟨0, ⋯⟩)
h₁ :
  ![x, y] ((fun (i : Fin (Nat.succ 1)) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 1))) =
    Function.comp (α := Fin 2) ![y, x] (⇑(Equiv.swap 0 1) : (a : Fin 2) → Fin 2)
      ((fun (i : Fin (Nat.succ 1)) ↦ i) ⟨1, ⋯⟩)
⊢ ![x, y] i = (![y, x] ∘ (⇑(Equiv.swap 0 1) : (a : Fin 2) → Fin 2)) i

Tactic:
fin_cases i
-- 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, y] ((fun (i : Fin (Nat.succ 1)) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 1))) =
    Function.comp (α := Fin 2) ![y, x] (⇑(Equiv.swap 0 1) : (a : Fin 2) → Fin 2)
      ((fun (i : Fin (Nat.succ 1)) ↦ i) ⟨0, ⋯⟩)

Tactic:
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 y : E
⊢ ![x, y] ((fun (i : Fin (Nat.succ 1)) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 1))) =
    Function.comp (α := Fin 2) ![y, x] (⇑(Equiv.swap 0 1) : (a : Fin 2) → Fin 2)
      ((fun (i : Fin (Nat.succ 1)) ↦ i) ⟨1, ⋯⟩)

Tactic:
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 y : E
⊢ Ne (α := Fin 2) 0 1

Tactic:
simp
-- 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 y : E),
    Eq (α := ℝ) (((((-o).areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
      ((((-o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
⊢ (-o).areaForm = -o.areaForm

Tactic:
ext x y
-- 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
⊢ Eq (α := ℝ) (((((-o).areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
    ((((-o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)

Tactic:
simp [areaForm_to_volumeForm]

Premises used: Orientation.areaForm_to_volumeForm
-- 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 →L[ℝ] ℝ) ((o.areaForm' : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ)
    (((LinearMap.toContinuousLinearMap : (E →ₗ[ℝ] ℝ) ≃ₗ[ℝ] E →L[ℝ] ℝ) : (a : E →ₗ[ℝ] ℝ) → E →L[ℝ] ℝ)
        ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) :
      E →L[ℝ] ℝ)

Tactic:
rfl

Premises used: 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 y : E
⊢ |(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y| ≤ ‖x‖ * ‖y‖

Tactic:
simpa [areaForm_to_volumeForm, Fin.prod_univ_succ] using o.abs_volumeForm_apply_le ![x, y]

Premises used: Orientation.areaForm_to_volumeForm, Fin.prod_univ_succ, Matrix.vecEmpty, Matrix.vecCons, Orientation.abs_volumeForm_apply_le
-- 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
⊢ (((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y ≤ ‖x‖ * ‖y‖

Tactic:
simpa [areaForm_to_volumeForm, Fin.prod_univ_succ] using o.volumeForm_apply_le ![x, y]

Premises used: Orientation.areaForm_to_volumeForm, Fin.prod_univ_succ, Matrix.vecEmpty, Orientation.volumeForm_apply_le, Matrix.vecCons
-- 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
h : ⟪x, y⟫ = 0
rw : ∏ i : Fin 2, ‖![x, y] i‖ = ‖x‖ * ‖y‖
rw₁ : Pairwise fun (i j : Fin 2) ↦ ⟪![x, y] i, ![x, y] j⟫ = 0
⊢ |(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y| = ‖x‖ * ‖y‖

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

Premises used: Orientation.areaForm_to_volumeForm, Orientation.abs_volumeForm_apply_of_pairwise_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 y : E
h : ⟪x, y⟫ = 0
⊢ ∏ i : Fin 2, ‖![x, y] i‖ = ‖x‖ * ‖y‖

Tactic:
simp [Fin.prod_univ_succ]

Premises used: Fin.prod_univ_succ
-- 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
h : ⟪x, y⟫ = 0
i j : Fin 2
hij : i ≠ j
0 : ∀ (hij : (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩ ≠ j), ⟪![x, y] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)), ![x, y] j⟫ = 0
1 : ∀ (hij : (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩ ≠ j), ⟪![x, y] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)), ![x, y] j⟫ = 0
⊢ ⟪![x, y] i, ![x, y] j⟫ = 0

Tactic:
fin_cases i
-- 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
h : ⟪x, y⟫ = 0
j : Fin 2
hij : (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩ ≠ j
0 :
  ∀ (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)),
    ⟪![x, y] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)), ![x, y] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))⟫ = 0
h_1 :
  ∀ (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)),
    ⟪![x, y] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)), ![x, y] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))⟫ = 0
⊢ ⟪![x, y] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)), ![x, y] j⟫ = 0

Tactic:
fin_cases j
-- 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
h : ⟪x, y⟫ = 0
j : Fin 2
hij : (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩ ≠ j
1 :
  ∀ (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)),
    ⟪![x, y] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)), ![x, y] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))⟫ = 0
h_1 :
  ∀ (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)),
    ⟪![x, y] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)), ![x, y] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))⟫ = 0
⊢ ⟪![x, y] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)), ![x, y] j⟫ = 0

Tactic:
fin_cases j
-- 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
h : ⟪x, y⟫ = 0
hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ ⟪![x, y] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)), ![x, y] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))⟫ = 0

Tactic:
simp_all
-- 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
h : ⟪x, y⟫ = 0
hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ ⟪![x, y] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)), ![x, y] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))⟫ = 0

Tactic:
simpa using 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 y : E
h : ⟪x, y⟫ = 0
hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ ⟪![x, y] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)), ![x, y] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))⟫ = 0

Tactic:
simpa [real_inner_comm] using h

Premises used: real_inner_comm
-- 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
h : ⟪x, y⟫ = 0
hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ ⟪![x, y] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)), ![x, y] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))⟫ = 0

Tactic:
simp_all
-- 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)
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
h :
  ∀ (i : Fin (Nat.succ 0).succ),
    Eq.{u_1 + 1} (α := E) (((⇑φ.symm : (a : F) → E) ∘ ![x, y]) i : E)
      (![(φ.symm : (a : F) → E) x, (φ.symm : (a : F) → E) y] i : E)
⊢ Eq.{u_1 + 1} (α := Fin (Nat.succ 0).succ → E) ((⇑φ.symm : (a : F) → E) ∘ ![x, y] : Fin (Nat.succ 0).succ → E)
    (![(φ.symm : (a : F) → E) x, (φ.symm : (a : F) → E) y] : Fin (Nat.succ 0).succ → E)

Tactic:
ext i
-- 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)
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
i : Fin (Nat.succ 0).succ
h :
  Eq.{u_1 + 1} (α := E) (((⇑φ.symm : (a : F) → E) ∘ ![x, y]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩) : E)
    (Matrix.vecCons (n := Nat.succ 0) ((φ.symm : (a : F) → E) x) ![(φ.symm : (a : F) → E) y]
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩) :
      E)
h₁ :
  Eq.{u_1 + 1} (α := E) (((⇑φ.symm : (a : F) → E) ∘ ![x, y]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩) : E)
    (Matrix.vecCons (n := Nat.succ 0) ((φ.symm : (a : F) → E) x) ![(φ.symm : (a : F) → E) y]
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩) :
      E)
⊢ Eq.{u_1 + 1} (α := E) (((⇑φ.symm : (a : F) → E) ∘ ![x, y]) i : E)
    (![(φ.symm : (a : F) → E) x, (φ.symm : (a : F) → E) y] i : E)

Tactic:
fin_cases i
-- 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)
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ Eq.{u_1 + 1} (α := E) (((⇑φ.symm : (a : F) → E) ∘ ![x, y]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩) : E)
    (Matrix.vecCons (n := Nat.succ 0) ((φ.symm : (a : F) → E) x) ![(φ.symm : (a : F) → E) y]
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩) :
      E)

Tactic:
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)
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ Eq.{u_1 + 1} (α := E) (((⇑φ.symm : (a : F) → E) ∘ ![x, y]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩) : E)
    (Matrix.vecCons (n := Nat.succ 0) ((φ.symm : (a : F) → E) x) ![(φ.symm : (a : F) → E) y]
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩) :
      E)

Tactic:
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)
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ Eq.{u_1 + 1} (α := Fin (Nat.succ 0).succ → E) ((⇑φ.symm : (a : F) → E) ∘ ![x, y] : Fin (Nat.succ 0).succ → E)
    (![(φ.symm : (a : F) → E) x, (φ.symm : (a : F) → E) y] : Fin (Nat.succ 0).succ → E)

Tactic:
have : φ.symm ∘ ![x, y] = ![φ.symm x, φ.symm y] := by
    ext i
    fin_cases i <;> 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)
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
this :
  Eq.{u_1 + 1} (α := Fin (Nat.succ 0).succ → E) ((⇑φ.symm : (a : F) → E) ∘ ![x, y] : Fin (Nat.succ 0).succ → E)
    (![(φ.symm : (a : F) → E) x, (φ.symm : (a : F) → E) y] : Fin (Nat.succ 0).succ → E)
⊢ Eq (α := ℝ)
    ((((areaForm
                  (((map (Fin 2) φ.toLinearEquiv :
                        Equiv.{u_1 + 1, u_2 + 1} (Orientation ℝ E (Fin 2)) (Orientation ℝ F (Fin 2))) :
                      (a : Orientation ℝ E (Fin 2)) → Orientation ℝ F (Fin 2))
                    o) :
                (a : F) → F →ₗ[ℝ] ℝ)
              x :
            F →ₗ[ℝ] ℝ) :
          (a : F) → ℝ)
        y :
      ℝ)
    ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) ((φ.symm : (a : F) → E) x : E) : E →ₗ[ℝ] ℝ) : (a : E) → ℝ)
        ((φ.symm : (a : F) → E) y : E) :
      ℝ)

Tactic:
simp [areaForm_to_volumeForm, volumeForm_map, this]

Premises used: Orientation.volumeForm_map, Orientation.areaForm_to_volumeForm
-- 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)
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
x y : E
⊢ Eq (α := ℝ)
    ((((areaForm ((map (Fin 2) φ.toLinearEquiv : (a : Orientation ℝ E (Fin 2)) → Orientation ℝ E (Fin 2)) o) :
                (a : E) → E →ₗ[ℝ] ℝ)
              ((φ : (a : E) → E) x : E) :
            E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        ((φ : (a : E) → E) y : E) :
      ℝ)
    ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) ((φ.symm : (a : E) → E) ((φ : (a : E) → E) x : E) : E) : E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        ((φ.symm : (a : E) → E) ((φ : (a : E) → E) y : E) : E) :
      ℝ)

Tactic:
o.areaForm_map φ (φ x) (φ y)

Premises used: Orientation.areaForm_map, 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)
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
x y : E
h : o = (map (Fin 2) φ.toLinearEquiv : (a : Orientation ℝ E (Fin 2)) → Orientation ℝ E (Fin 2)) o
h₁ : x = (φ.symm : (a : E) → E) ((φ : (a : E) → E) x : E)
h₂ : y = (φ.symm : (a : E) → E) ((φ : (a : E) → E) y : E)
⊢ Eq (α := ℝ)
    ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) ((φ : (a : E) → E) x : E) : E →ₗ[ℝ] ℝ) : (a : E) → ℝ)
        ((φ : (a : E) → E) y : E) :
      ℝ)
    ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)

Tactic:
convert! o.areaForm_map φ (φ x) (φ y)

Premises used: Orientation.areaForm_map, 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)
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
x y : E
h : (map (Fin 2) φ.toLinearEquiv : (a : Orientation ℝ E (Fin 2)) → Orientation ℝ E (Fin 2)) o = o
⊢ o = (map (Fin 2) φ.toLinearEquiv : (a : Orientation ℝ E (Fin 2)) → Orientation ℝ E (Fin 2)) o

Tactic:
symm
-- 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)
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
x y : E
h : Fintype.card (Fin 2) = finrank ℝ E
⊢ (map (Fin 2) φ.toLinearEquiv : (a : Orientation ℝ E (Fin 2)) → Orientation ℝ E (Fin 2)) o = o

Tactic:
rwa [← o.map_eq_iff_det_pos φ.toLinearEquiv] at hφ

Premises used: LinearIsometryEquiv.toLinearEquiv, Orientation.map_eq_iff_det_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)
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
x y : E
h : Fintype.card (Fin 2) = 2
h₁ h₂ : Eq (α := ℕ) 2 2
⊢ Fintype.card (Fin 2) = finrank ℝ E

Tactic:
rw [@Fact.out (finrank ℝ E = 2), Fintype.card_fin]

Premises used: Fintype.card_fin, 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)
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
x y : E
⊢ x = (φ.symm : (a : E) → E) ((φ : (a : E) → E) x : E)

Tactic:
simp
-- 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)
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
x y : E
⊢ y = (φ.symm : (a : E) → E) ((φ : (a : E) → E) y : E)

Tactic:
simp
-- 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
simp :
  ⟪(LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E) : (a : StrongDual ℝ E) → E)
        (((LinearMap.toContinuousLinearMap : (E →ₗ[ℝ] ℝ) ≃ₗ[ℝ] E →L[ℝ] ℝ) : (a : E →ₗ[ℝ] ℝ) → StrongDual ℝ E)
            ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x) :
          StrongDual ℝ E),
      y⟫ =
    (((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y
⊢ ⟪(o.rightAngleRotationAux₁ : (a : E) → E) x, y⟫ = (((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y

Tactic:
simp only [rightAngleRotationAux₁, LinearEquiv.trans_symm, LinearEquiv.symm_symm,
    LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, LinearEquiv.trans_apply,
    LinearIsometryEquiv.coe_symm_toLinearEquiv]

Premises used: Orientation.rightAngleRotationAux₁, LinearEquiv.trans_apply, LinearIsometryEquiv.coe_symm_toLinearEquiv, LinearEquiv.symm_symm, LinearMap.coe_comp, Function.comp_apply, LinearEquiv.trans_symm, LinearEquiv.coe_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 y : E
rw :
  Eq (α := ℝ)
    (((((LinearMap.toContinuousLinearMap : (E →ₗ[ℝ] ℝ) ≃ₗ[ℝ] E →L[ℝ] ℝ) : (a : E →ₗ[ℝ] ℝ) → StrongDual ℝ E)
              ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x) :
            StrongDual ℝ E) :
          (a : E) → ℝ)
        y :
      ℝ)
    ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
⊢ ⟪(LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E) : (a : StrongDual ℝ E) → E)
        (((LinearMap.toContinuousLinearMap : (E →ₗ[ℝ] ℝ) ≃ₗ[ℝ] E →L[ℝ] ℝ) : (a : E →ₗ[ℝ] ℝ) → StrongDual ℝ E)
            ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x) :
          StrongDual ℝ E),
      y⟫ =
    (((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y

Tactic:
rw [InnerProductSpace.toDual_symm_apply]

Premises used: InnerProductSpace.toDual_symm_apply
-- 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
⊢ Eq (α := ℝ)
    (((((LinearMap.toContinuousLinearMap : (E →ₗ[ℝ] ℝ) ≃ₗ[ℝ] E →L[ℝ] ℝ) : (a : E →ₗ[ℝ] ℝ) → StrongDual ℝ E)
              ((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x) :
            StrongDual ℝ E) :
          (a : E) → ℝ)
        y :
      ℝ)
    ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)

Tactic:
norm_cast
-- 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 :
  ⟪(o.rightAngleRotationAux₁ : (a : E) → E) y, x⟫ =
    -(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y
⊢ ⟪x, (o.rightAngleRotationAux₁ : (a : E) → E) y⟫ =
    -(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y

Tactic:
rw [real_inner_comm]

Premises used: real_inner_comm
-- 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
⊢ ⟪(o.rightAngleRotationAux₁ : (a : E) → E) y, x⟫ =
    -(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y

Tactic:
simp [o.areaForm_swap y x]

Premises used: Orientation.areaForm_swap
-- 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
⊢ norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) = ‖x‖

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- 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
refine_1 : norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) ≤ ‖x‖
refine_2 : ‖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_antisymm ?_ ?_

Premises used: le_antisymm
-- 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
refine_1 :
  ∀ (h : 0 = norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)),
    norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) ≤ ‖x‖
refine_1₁ :
  ∀ (h : 0 < 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) ≤ ‖x‖

Tactic:
rcases eq_or_lt_of_le (norm_nonneg (o.rightAngleRotationAux₁ x)) with h | h

Premises used: Orientation.rightAngleRotationAux₁, eq_or_lt_of_le, DFunLike.coe, norm_nonneg
-- 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 : 0 ≤ ‖x‖
⊢ norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) ≤ ‖x‖

Tactic:
rw [← h]