awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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)
⊢ 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)
have h₁ : Eq.{u_1 + 1} (α := E) (((⇑φ.symm : (a : F) → E) ∘ ![x, y]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, sorry⟩) : 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, sorry⟩) :
    E)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (hypothesis)
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 (α := ℝ)
    ((((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) :
      ℝ)
have 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)
Tactic: have : φ.symm ∘ ![x, y] = ![φ.symm x, φ.symm y] := by
    ext i
    fin_cases i <;> rfl
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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 (α := ℝ)
    ((((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 : ℝ)
have h : o = (map (Fin 2) φ.toLinearEquiv : (a : Orientation ℝ E (Fin 2)) → Orientation ℝ E (Fin 2)) o
Tactic: convert! o.areaForm_map φ (φ x) (φ y)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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
⊢ 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 : ℝ)
have h₁ : x = (φ.symm : (a : E) → E) ((φ : (a : E) → E) x : E)
Tactic: convert! o.areaForm_map φ (φ x) (φ y)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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)
⊢ 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 : ℝ)
have h₂ : y = (φ.symm : (a : E) → E) ((φ : (a : E) → E) y : E)
Tactic: convert! o.areaForm_map φ (φ x) (φ y)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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
⊢ o = (map (Fin 2) φ.toLinearEquiv : (a : Orientation ℝ E (Fin 2)) → Orientation ℝ E (Fin 2)) o
have h : (map (Fin 2) φ.toLinearEquiv : (a : Orientation ℝ E (Fin 2)) → Orientation ℝ E (Fin 2)) o = o
Tactic: symm
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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
⊢ (map (Fin 2) φ.toLinearEquiv : (a : Orientation ℝ E (Fin 2)) → Orientation ℝ E (Fin 2)) o = o
have h : Fintype.card (Fin 2) = finrank ℝ E
Tactic: rwa [← o.map_eq_iff_det_pos φ.toLinearEquiv] at hφ
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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
⊢ Fintype.card (Fin 2) = finrank ℝ E
have h : Fintype.card (Fin 2) = 2
Tactic: rw [@Fact.out (finrank ℝ E = 2), Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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
⊢ Fintype.card (Fin 2) = finrank ℝ E
have h₁ : Eq (α := ℕ) 2 2
Tactic: rw [@Fact.out (finrank ℝ E = 2), Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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) x, y⟫ = (((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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.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
have 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 : ℝ)
Tactic: rw [InnerProductSpace.toDual_symm_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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, (o.rightAngleRotationAux₁ : (a : E) → E) y⟫ =
    -(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y
have rw : ⟪(o.rightAngleRotationAux₁ : (a : E) → E) y, x⟫ = -(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y
Tactic: rw [real_inner_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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‖
have refine_1 : norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) ≤ ‖x‖
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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‖
⊢ norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) = ‖x‖
have refine_2 : ‖x‖ ≤ norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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‖
have 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‖
Tactic: rcases eq_or_lt_of_le (norm_nonneg (o.rightAngleRotationAux₁ x)) with h | h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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‖
⊢ norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) ≤ ‖x‖
have 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‖
Tactic: rcases eq_or_lt_of_le (norm_nonneg (o.rightAngleRotationAux₁ x)) with h | h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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‖
have refine_1 : 0 ≤ ‖x‖
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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‖
have 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)
Tactic: refine le_of_mul_le_mul_right ?_ h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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) *
      norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) ≤
    ‖x‖ * norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)
have 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)
Tactic: rw [← real_inner_self_eq_norm_mul_norm, o.inner_rightAngleRotationAux₁_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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ᗮ
have apply : 0 < finrank.{0, u_1} ℝ ↥Kᗮ
Tactic: apply nontrivial_of_finrank_pos (R := ℝ)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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}
have rw : finrank.{0, u_1} ℝ ↥K ≤ Finset.card (α := E) (Set.toFinset {x})
Tactic: rw [← Set.toFinset_singleton]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (hypothesis)
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
⊢ 0 < finrank.{0, u_1} ℝ ↥Kᗮ
have this : 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)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (hypothesis)
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}
⊢ 0 < finrank.{0, u_1} ℝ ↥Kᗮ
have this₁ : Finset.card (α := E) {x} = 1
Tactic: have : Finset.card {x} = 1 := Finset.card_singleton x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (hypothesis)
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
⊢ 0 < finrank.{0, u_1} ℝ ↥Kᗮ
have this₁ : 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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (hypothesis)
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
⊢ 0 < finrank.{0, u_1} ℝ ↥Kᗮ
have this₁ : finrank ℝ E = 2
Tactic: have : finrank ℝ E = 2 := Fact.out
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (hypothesis)
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
⊢ ‖x‖ ≤ norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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ᗮ
⊢ ‖x‖ ≤ norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)
have refine_2 : ∀ (w : ↥Kᗮ) (hw₀ : w ≠ 0), ‖x‖ ≤ norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)
Tactic: obtain ⟨w, hw₀⟩ : ∃ w : Kᗮ, w ≠ 0 := exists_ne 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (hypothesis)
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‖ ≤ norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)
have hw' : ⟪x, (↑w : E)⟫ = 0
Tactic: have hw' : ⟪x, (w : E)⟫ = 0 := Submodule.mem_orthogonal_singleton_iff_inner_right.mp w.2
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (hypothesis)
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
⊢ ‖x‖ ≤ norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)
have hw : (↑w : E) ≠ 0
Tactic: have hw : (w : E) ≠ 0 := fun h => hw₀ (Submodule.coe_eq_zero.mp h)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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
⊢ ‖x‖ ≤ norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)
have refine_2 : ‖x‖ * ‖(↑w : E)‖ ≤ norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) * ‖(↑w : E)‖
Tactic: refine le_of_mul_le_mul_right ?_ (by rwa [norm_pos_iff] : 0 < ‖(w : E)‖)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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
⊢ ‖x‖ * ‖(↑w : E)‖ ≤ norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) * ‖(↑w : E)‖
have 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)‖
Tactic: rw [← o.abs_areaForm_of_orthogonal hw']
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) (↑w : E)| ≤
    norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) * ‖(↑w : E)‖
have refine_2 : |⟪(o.rightAngleRotationAux₁ : (a : E) → E) x, (↑w : E)⟫| ≤
  norm (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) * ‖(↑w : E)‖
Tactic: rw [← o.inner_rightAngleRotationAux₁_left x w]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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.rightAngleRotationAux₁ : (a : E) → E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) = -x
have apply : ∀ (v : E), ⟪v, (o.rightAngleRotationAux₁ : (a : E) → E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)⟫ = ⟪v, -x⟫
Tactic: apply ext_inner_left ℝ
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (hypothesis)
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
⊢ ⟪y, (o.rightAngleRotationAux₁ : (a : E) → E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)⟫ = ⟪y, -x⟫
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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⟫
⊢ ⟪y, (o.rightAngleRotationAux₁ : (a : E) → E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)⟫ = ⟪y, -x⟫
have rw : -(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) y : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) =
  ⟪y, -x⟫
Tactic: rw [o.inner_rightAngleRotationAux₁_right, ← o.inner_rightAngleRotationAux₁_left, this,
    inner_neg_right]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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⟫
⊢ ⟪y, (o.rightAngleRotationAux₁ : (a : E) → E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)⟫ = ⟪y, -x⟫
have rw₁ : -inner ℝ (E := E) ((o.rightAngleRotationAux₁ : (a : E) → E) y : E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E) =
  ⟪y, -x⟫
Tactic: rw [o.inner_rightAngleRotationAux₁_right, ← o.inner_rightAngleRotationAux₁_left, this,
    inner_neg_right]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
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⟫
⊢ ⟪y, (o.rightAngleRotationAux₁ : (a : E) → E) ((o.rightAngleRotationAux₁ : (a : E) → E) x : E)⟫ = ⟪y, -x⟫
have rw₂ : -⟪y, x⟫ = ⟪y, -x⟫
Tactic: rw [o.inner_rightAngleRotationAux₁_right, ← o.inner_rightAngleRotationAux₁_left, this,
    inner_neg_right]