Is there a way to automate this proof?

Stream: new members

[Ilmārs Cīrulis]

Or maybe I just need more patience to do it step by step?

import Mathlib

namespace InnerProductGeometry
open scoped RealInnerProductSpace

variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V]

lemma aux (x z : V) (kx kz : ℝ) (H : kx • x + kz • z ≠ 0) (H0: kx ≠ 0) :
    x - (‖kx • x + kz • z‖⁻¹ * ⟪x, kx • x + kz • z⟫) • ‖kx • x + kz • z‖⁻¹ • (kx • x + kz • z) =
    -(kz / kx) • (z - (‖kx • x + kz • z‖⁻¹ * ⟪z, kx • x + kz • z⟫) • ‖kx • x + kz • z‖⁻¹ • (kx • x + kz • z)) := by
  sorry

[Ilmārs Cīrulis]

Discovered Rediscovered module tactic that simplifies the proof a bit.

[Ilmārs Cīrulis]

Here it is, messy but working

import Mathlib

namespace InnerProductGeometry
open scoped RealInnerProductSpace

variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V]

lemma aux00 (x y : V) (k : ℝ) (Hk : k ≠ 0) :
    x = y ↔ k • x = k • y := by
  constructor <;> intro H7
  · rw [H7]
  · have H8 : k⁻¹ • (k • x) = k⁻¹ • (k • y) := by
      rw [H7]
    rw [← smul_assoc, ← smul_assoc, smul_eq_mul] at H8
    field_simp at H8
    simp at H8
    exact H8

lemma aux01 (x z : V) (kx kz : ℝ) (H : kx • x + kz • z ≠ 0) (H0: kx ≠ 0) :
    x - (‖kx • x + kz • z‖⁻¹ * ⟪x, kx • x + kz • z⟫) • ‖kx • x + kz • z‖⁻¹ • (kx • x + kz • z) =
    -(kz / kx) • (z - (‖kx • x + kz • z‖⁻¹ * ⟪z, kx • x + kz • z⟫) • ‖kx • x + kz • z‖⁻¹ • (kx • x + kz • z)) := by
  set w := kx • x + kz • z
  have Hw : ‖w‖ ≠ 0 := norm_ne_zero_iff.mpr H
  rw [aux00 _ _ _ H0, aux00 _ _ _ Hw, aux00 _ _ _ Hw, ← sub_eq_zero]
  repeat rw [<- smul_assoc]
  repeat rw [smul_eq_mul]
  repeat rw [smul_sub]
  repeat rw [<- smul_assoc]
  repeat rw [smul_eq_mul]
  field_simp
  abel_nf
  simp
  rw [← sub_eq_add_neg, ← add_assoc, ← sub_eq_add_neg]
  rw [← smul_eq_mul (‖w‖ ^ 2) kx, ← smul_eq_mul (‖w‖ ^ 2) kz]
  rw [smul_assoc, smul_assoc]
  have H1 (u1 u2 u3 u4 : V) : u1 - u2 + (u3 - u4) = u1 + u3 - (u2 + u4) := by module
  rw [H1]
  have H2 : ‖w‖ ^ 2 • kx • x + ‖w‖ ^ 2 • kz • z = ‖w‖ ^ 2 • w := by
    unfold w
    module
  have H3 : (kx * ⟪x, w⟫) • w + (kz * ⟪z, w⟫) • w =
            (kx * ⟪x, w⟫ + kz * ⟪z, w⟫) • w := by module
  rw [H2, H3]
  rw [← real_inner_smul_left, ← real_inner_smul_left, ← inner_add_left]
  rw [← real_inner_self_eq_norm_sq w]
  module

[Jovan Gerbscheid]

You can use mathlib's powerful tactics to your advantage:

import Mathlib

namespace InnerProductGeometry
open scoped RealInnerProductSpace

variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V]

lemma aux01 (x z : V) (kx kz : ℝ) (H : kx • x + kz • z ≠ 0) (H0: kx ≠ 0) :
    x - (‖kx • x + kz • z‖⁻¹ * ⟪x, kx • x + kz • z⟫) • ‖kx • x + kz • z‖⁻¹ • (kx • x + kz • z) =
    -(kz / kx) • (z - (‖kx • x + kz • z‖⁻¹ * ⟪z, kx • x + kz • z⟫) • ‖kx • x + kz • z‖⁻¹ • (kx • x + kz • z)) := by
  rw [neg_smul, smul_sub]
  simp [smul_smul]
  match_scalars <;>
  · field_simp
    rw [← real_inner_self_eq_norm_sq]
    simp [inner_add_left, inner_smul_left]
    ring

[Ilmārs Cīrulis]

Wow!

[Jovan Gerbscheid]

The doc-string of module also mentions the match_scalars tactic.

[Jovan Gerbscheid]

The brand new field_simp tactic is really great for these kinds of goals.

[Ilmārs Cīrulis]

Thank you!

[Heather Macbeth]

@Jovan Gerbscheid In fact you can eliminate the

  rw [neg_smul, smul_sub]
  simp [smul_smul]

:)