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)
a x y : E
a₁ :
  (⟪x, a⟫ +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a : ℝ)
              (0 : ℝ) -
            HMul.hMul (α := ℝ) 0 1)) *
        (0 +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
              (1 : ℝ) +
            HMul.hMul (α := ℝ) 0 0)) +
      (0 +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a : ℝ)
              (1 : ℝ) +
            HMul.hMul (α := ℝ) 0 0)) *
        (⟪a, y⟫ +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
              (0 : ℝ) -
            HMul.hMul (α := ℝ) 0 1)) =
    HPow.hPow (β := ℕ) ‖a‖ 2 *
        (0 +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
              (1 : ℝ) +
            HMul.hMul (α := ℝ) 0 0)) +
      0 *
        (⟪x, y⟫ +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
              (0 : ℝ) -
            HMul.hMul (α := ℝ) 0 1))
⊢ (HMul.hMul (α := ℂ) (β := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) a : ℂ)
        ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) a : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)).im =
    (HMul.hMul (β := ℂ) (↑(HPow.hPow (β := ℕ) ‖a‖ 2) : ℂ)
        ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)).im

Tactic:
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]

Premises used: Complex.mul_im, Complex.real_smul, Complex.add_im, Complex.mul_re, Complex.add_re, Complex.I_re, Complex.I_im, Complex.ofReal_re, Orientation.kahler_apply_apply, Complex.ofReal_im
-- 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)
a x y : E
a₁ :
  (⟪a, x⟫ +
          (HMul.hMul (α := ℝ) (β := ℝ) (-(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
              (0 : ℝ) -
            HMul.hMul (α := ℝ) 0 1)) *
        (0 +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
              (1 : ℝ) +
            HMul.hMul (α := ℝ) 0 0)) +
      (0 +
          (HMul.hMul (α := ℝ) (β := ℝ) (-(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
              (1 : ℝ) +
            HMul.hMul (α := ℝ) 0 0)) *
        (⟪a, y⟫ +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
              (0 : ℝ) -
            HMul.hMul (α := ℝ) 0 1)) =
    HPow.hPow (β := ℕ) ‖a‖ 2 *
        (0 +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
              (1 : ℝ) +
            HMul.hMul (α := ℝ) 0 0)) +
      0 *
        (⟪x, y⟫ +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
              (0 : ℝ) -
            HMul.hMul (α := ℝ) 0 1))
⊢ (⟪x, a⟫ +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a : ℝ)
              (0 : ℝ) -
            HMul.hMul (α := ℝ) 0 1)) *
        (0 +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
              (1 : ℝ) +
            HMul.hMul (α := ℝ) 0 0)) +
      (0 +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) a : ℝ)
              (1 : ℝ) +
            HMul.hMul (α := ℝ) 0 0)) *
        (⟪a, y⟫ +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
              (0 : ℝ) -
            HMul.hMul (α := ℝ) 0 1)) =
    HPow.hPow (β := ℕ) ‖a‖ 2 *
        (0 +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
              (1 : ℝ) +
            HMul.hMul (α := ℝ) 0 0)) +
      0 *
        (⟪x, y⟫ +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
              (0 : ℝ) -
            HMul.hMul (α := ℝ) 0 1))

Tactic:
rw [real_inner_comm a x, o.areaForm_swap x a]

Premises used: Orientation.areaForm_swap, 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)
a x y : E
⊢ (⟪a, x⟫ +
          (HMul.hMul (α := ℝ) (β := ℝ) (-(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
              (0 : ℝ) -
            HMul.hMul (α := ℝ) 0 1)) *
        (0 +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
              (1 : ℝ) +
            HMul.hMul (α := ℝ) 0 0)) +
      (0 +
          (HMul.hMul (α := ℝ) (β := ℝ) (-(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
              (1 : ℝ) +
            HMul.hMul (α := ℝ) 0 0)) *
        (⟪a, y⟫ +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) a : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
              (0 : ℝ) -
            HMul.hMul (α := ℝ) 0 1)) =
    HPow.hPow (β := ℕ) ‖a‖ 2 *
        (0 +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
              (1 : ℝ) +
            HMul.hMul (α := ℝ) 0 0)) +
      0 *
        (⟪x, y⟫ +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
              (0 : ℝ) -
            HMul.hMul (α := ℝ) 0 1))

Tactic:
linear_combination o.inner_mul_areaForm_sub a x y

Premises used: Orientation.inner_mul_areaForm_sub
-- 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)
a x y : E
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  HMul.hMul (β := ℂ) (↑(HPow.hPow (β := ℕ) ‖a‖ 2) : ℂ)
      ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) =
    HMul.hMul (β := ℂ) (↑(HPow.hPow (β := ℕ) ‖a‖ 2) : ℂ)
      ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
⊢ HMul.hMul (β := ℂ) (↑(HPow.hPow (β := ℕ) ‖a‖ 2) : ℂ)
      ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) =
    HMul.hMul (β := ℂ) (HPow.hPow (β := ℕ) (↑‖a‖ : ℂ) 2)
      ((((o.kahler : (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
⊢ (Complex.normSq : (a : ℂ) → ℝ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) =
    HPow.hPow (β := ℕ) ‖x‖ 2 * HPow.hPow (β := ℕ) ‖y‖ 2

Tactic:
simpa [kahler_apply_apply, Complex.normSq, sq] using o.inner_sq_add_areaForm_sq x y

Premises used: Complex.normSq, sq, Orientation.inner_sq_add_areaForm_sq, Orientation.kahler_apply_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
rw :
  (Complex.normSq : (a : ℂ) → ℝ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) =
    HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2
ha : 0 ≤ norm (E := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
hb : 0 ≤ ‖x‖ * ‖y‖
⊢ norm (E := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) = ‖x‖ * ‖y‖

Tactic:
rw [← sq_eq_sq₀, Complex.sq_norm]

Premises used: Complex.sq_norm, sq_eq_sq₀
-- 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
⊢ (Complex.normSq : (a : ℂ) → ℝ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) =
    HPow.hPow (β := ℕ) (‖x‖ * ‖y‖) 2

Tactic:
linear_combination o.normSq_kahler x y

Premises used: Orientation.normSq_kahler
-- 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
⊢ 0 ≤ norm (E := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)

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 y : E
⊢ 0 ≤ ‖x‖ * ‖y‖

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 y : E
hx : Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ)
⊢ ‖x‖ * ‖y‖ = 0

Tactic:
simpa [hx] using (o.norm_kahler x y).symm

Premises used: Eq.symm, Orientation.norm_kahler
-- 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
hx : Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ)
⊢ ‖x‖ * ‖y‖ = 0

Tactic:
have : ‖x‖ * ‖y‖ = 0 := by simpa [hx] using (o.norm_kahler x y).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)
x y : E
hx : Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ)
this : ‖x‖ * ‖y‖ = 0
inl : ∀ (h : ‖x‖ = 0), x = 0 ∨ y = 0
inr : ∀ (h : ‖y‖ = 0), x = 0 ∨ y = 0
⊢ x = 0 ∨ y = 0

Tactic:
rcases eq_zero_or_eq_zero_of_mul_eq_zero this with h | h

Premises used: NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero
-- 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
hx : Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ)
this : ‖x‖ * ‖y‖ = 0
h : ‖x‖ = 0
inl : x = 0
⊢ x = 0 ∨ y = 0

Tactic:
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
hx : Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ)
this : ‖x‖ * ‖y‖ = 0
h : ‖x‖ = 0
⊢ x = 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
hx : Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ)
this : ‖x‖ * ‖y‖ = 0
h : ‖y‖ = 0
inr : y = 0
⊢ x = 0 ∨ y = 0

Tactic:
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
hx : Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ)
this : ‖x‖ * ‖y‖ = 0
h : ‖y‖ = 0
⊢ y = 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
⊢ Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ) ↔ x = 0 ∨ y = 0

Tactic:
⟨o.eq_zero_or_eq_zero_of_kahler_eq_zero, ?_⟩

Premises used: Orientation.eq_zero_or_eq_zero_of_kahler_eq_zero, Iff.intro
-- 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
refine : x = 0 ∨ y = 0 → Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ)
⊢ Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ) ↔ x = 0 ∨ y = 0

Tactic:
refine ⟨o.eq_zero_or_eq_zero_of_kahler_eq_zero, ?_⟩
-- 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)
y : E
⊢ Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) 0 : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ)

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 : E
⊢ Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) 0 : ℂ) (0 : ℂ)

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
hx : x ≠ 0
hy : y ≠ 0
apply : ¬(x = 0 ∨ y = 0)
⊢ Ne (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ)

Tactic:
apply mt o.eq_zero_or_eq_zero_of_kahler_eq_zero

Premises used: Orientation.eq_zero_or_eq_zero_of_kahler_eq_zero, mt
-- 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
hx : x ≠ 0
hy : y ≠ 0
inl : x = 0 → False
inr : y = 0 → False
⊢ ¬(x = 0 ∨ y = 0)

Tactic:
tauto
-- 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 (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ) ↔ x ≠ 0 ∧ y ≠ 0

Tactic:
⟨?_, fun h => o.kahler_ne_zero h.1 h.2⟩

Premises used: Orientation.kahler_ne_zero, And.right, And.left, Iff.intro
-- 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
refine : Ne (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ) → x ≠ 0 ∧ y ≠ 0
⊢ Ne (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ) ↔ x ≠ 0 ∧ y ≠ 0

Tactic:
refine ⟨?_, fun h => o.kahler_ne_zero h.1 h.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 y : E
contrapose :
  ¬(x ≠ 0 ∧ y ≠ 0) → Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ)
⊢ Ne (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ) → x ≠ 0 ∧ y ≠ 0

Tactic:
contrapose
-- 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 :
  x = 0 ∨ y = 0 →
    (↑⟪x, y⟫ : ℂ) + (↑((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y) : ℂ) * Complex.I = 0
⊢ ¬(x ≠ 0 ∧ y ≠ 0) → Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ)

Tactic:
simp only [not_and_or, Classical.not_not, kahler_apply_apply, Complex.real_smul]

Premises used: Complex.real_smul, Classical.not_not, not_and_or, Orientation.kahler_apply_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)
y : E
⊢ (↑⟪0, y⟫ : ℂ) + (↑((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) 0 : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y) : ℂ) * Complex.I = 0

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 : E
⊢ (↑⟪x, 0⟫ : ℂ) + (↑((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) 0) : ℂ) * Complex.I = 0

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)
F : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ Eq (α := ℂ)
    ((((kahler
                  (((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.kahler : (a : E) → E →ₗ[ℝ] ℂ) ((φ.symm : (a : F) → E) x : E) : E →ₗ[ℝ] ℂ) : (a : E) → ℂ)
        ((φ.symm : (a : F) → E) y : E) :
      ℂ)

Tactic:
simp [kahler_apply_apply, areaForm_map]

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

Tactic:
simp [kahler_apply_apply, o.areaForm_comp_linearIsometryEquiv φ hφ]

Premises used: Orientation.areaForm_comp_linearIsometryEquiv, Orientation.kahler_apply_apply
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
w z : ℂ
o : Orientation ℝ ℂ (Fin 2) := Complex.orientation
simp : w.re * z.im - z.re * w.im = w.re * z.im + -w.im * z.re
⊢ (((Complex.orientation.areaForm : (a : ℂ) → ℂ →ₗ[ℝ] ℝ) w : ℂ →ₗ[ℝ] ℝ) : (a : ℂ) → ℝ) z =
    (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z).im

Tactic:
simp only [o, 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, mul_im, conj_re, conj_im]

Premises used: Complex.mul_im, Complex.toBasis_orthonormalBasisOneI, Orientation.areaForm_to_volumeForm, Matrix.cons_val_one, Orientation.volumeForm_robust, Matrix.cons_val_zero, Complex.orthonormalBasisOneI, Complex.conj_im, Complex.coe_basisOneI_repr, Module.Basis.toMatrix_apply, Complex.conj_re, Matrix.det_fin_two, Module.Basis.det_apply, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
w z : ℂ
o : Orientation ℝ ℂ (Fin 2) := Complex.orientation
⊢ w.re * z.im - z.re * w.im = w.re * z.im + -w.im * z.re

Tactic:
ring
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
z : ℂ
apply : ∀ (v : ℂ), ⟪(Complex.orientation.rightAngleRotation : (a : ℂ) → ℂ) z, v⟫ = ⟪I * z, v⟫
⊢ (Complex.orientation.rightAngleRotation : (a : ℂ) → ℂ) z = I * z

Tactic:
apply ext_inner_right ℝ

Premises used: Real, ext_inner_right
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
z w : ℂ
rw : (((Complex.orientation.areaForm : (a : ℂ) → ℂ →ₗ[ℝ] ℝ) z : ℂ →ₗ[ℝ] ℝ) : (a : ℂ) → ℝ) w = ⟪I * z, w⟫
⊢ ⟪(Complex.orientation.rightAngleRotation : (a : ℂ) → ℂ) z, w⟫ = ⟪I * z, w⟫

Tactic:
rw [Orientation.inner_rightAngleRotation_left]

Premises used: Orientation.inner_rightAngleRotation_left
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
z w : ℂ
simp : z.re * w.im + -z.im * w.re = w.re * (-0 * z.re - -1 * -z.im) - w.im * (-0 * -z.im + -1 * z.re)
⊢ (((Complex.orientation.areaForm : (a : ℂ) → ℂ →ₗ[ℝ] ℝ) z : ℂ →ₗ[ℝ] ℝ) : (a : ℂ) → ℝ) w = ⟪I * z, w⟫

Tactic:
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]

Premises used: Complex.mul_im, Complex.areaForm, Complex.mul_re, Complex.conj_im, Complex.I_re, Complex.I_im, map_mul, Complex.inner, Complex.neg_re, Complex.conj_re, Complex.conj_I, Complex.neg_im
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
z w : ℂ
⊢ z.re * w.im + -z.im * w.re = w.re * (-0 * z.re - -1 * -z.im) - w.im * (-0 * -z.im + -1 * z.re)

Tactic:
ring
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
w z : ℂ
a :
  ((↑⟪w, z⟫ : ℂ) +
        HSMul.hSMul (α := ℝ)
          ((((Complex.orientation.areaForm : (a : ℂ) → ℂ →ₗ[ℝ] ℝ) w : ℂ →ₗ[ℝ] ℝ) : (a : ℂ) → ℝ) z : ℝ) I).re =
    (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)).re
a₁ :
  ((↑⟪w, z⟫ : ℂ) +
        HSMul.hSMul (α := ℝ)
          ((((Complex.orientation.areaForm : (a : ℂ) → ℂ →ₗ[ℝ] ℝ) w : ℂ →ₗ[ℝ] ℝ) : (a : ℂ) → ℝ) z : ℝ) I).im =
    (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)).im
⊢ (↑⟪w, z⟫ : ℂ) +
      HSMul.hSMul (α := ℝ) ((((Complex.orientation.areaForm : (a : ℂ) → ℂ →ₗ[ℝ] ℝ) w : ℂ →ₗ[ℝ] ℝ) : (a : ℂ) → ℝ) z : ℝ)
        I =
    HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)

Tactic:
apply Complex.ext

Premises used: Complex.ext
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
w z : ℂ
⊢ ((↑⟪w, z⟫ : ℂ) +
        HSMul.hSMul (α := ℝ)
          ((((Complex.orientation.areaForm : (a : ℂ) → ℂ →ₗ[ℝ] ℝ) w : ℂ →ₗ[ℝ] ℝ) : (a : ℂ) → ℝ) z : ℝ) I).re =
    (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)).re

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.InnerProductSpace.TwoDim
Goal:
w z : ℂ
⊢ ((↑⟪w, z⟫ : ℂ) +
        HSMul.hSMul (α := ℝ)
          ((((Complex.orientation.areaForm : (a : ℂ) → ℂ →ₗ[ℝ] ℝ) w : ℂ →ₗ[ℝ] ℝ) : (a : ℂ) → ℝ) z : ℝ) I).im =
    (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)).im

Tactic:
simp [mul_comm]

Premises used: mul_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)
f : E ≃ₗᵢ[ℝ] ℂ
hf :
  ((map (Fin 2) f.toLinearEquiv : Orientation ℝ E (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
        (a : Orientation ℝ E (Fin 2)) → Orientation ℝ ℂ (Fin 2))
      o =
    Complex.orientation
x y : E
rw :
  Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
    ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) x : ℂ) : E) : E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) y : ℂ) : E) :
      ℝ)
⊢ (((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y =
    (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : E) → ℂ) x : ℂ) : ℂ)
        ((f : (a : E) → ℂ) y : ℂ)).im

Tactic:
rw [← Complex.areaForm, ← hf, areaForm_map]

Premises used: Complex.areaForm, Orientation.areaForm_map