awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Invertible (α := R) 2
f g : M →ₗ[R] R
x x_1 : M
⊢ Eq.{u_3 + 1} (α := R)
    (((((((associated.{u_3, u_4, u_3} (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                      (a : QuadraticMap R M R) → BilinMap R M R)
                    (linMulLin f g) :
                  BilinMap R M R) :
                (a : M) → M →ₗ[R] R)
              x :
            M →ₗ[R] R) :
          (a : M) → R)
        x_1 :
      R)
    ((((HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
                  (compl₁₂ (mul R R) f g + compl₁₂ (mul R R) g f) :
                (a : M) → M →ₗ[R] R)
              x :
            M →ₗ[R] R) :
          (a : M) → R)
        x_1 :
      R)
have h : HAdd.hAdd (α := R) (β := R) ((f : (a : M) → R) x : R) ((f : (a : M) → R) x_1 : R) *
        HAdd.hAdd (α := R) (β := R) ((g : (a : M) → R) x : R) ((g : (a : M) → R) x_1 : R) -
      HMul.hMul (α := R) (β := R) ((f : (a : M) → R) x : R) ((g : (a : M) → R) x : R) -
    HMul.hMul (α := R) (β := R) ((f : (a : M) → R) x_1 : R) ((g : (a : M) → R) x_1 : R) =
  HSMul.hSMul (α := Module.End R R) 2
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
        HMul.hMul (α := R) (β := R) ((f : (a : M) → R) x : R) ((g : (a : M) → R) x_1 : R)) +
    HSMul.hSMul (α := Module.End R R) 2
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
        HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) x_1 : R))
Tactic: simp only [associated_apply, linMulLin_apply, map_add, smul_add, LinearMap.add_apply,
    LinearMap.smul_apply, compl₁₂_apply, mul_apply', smul_eq_mul, invOf_smul_eq_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Invertible (α := R) 2
f g : M →ₗ[R] R
x x_1 : M
⊢ HAdd.hAdd (α := R) (β := R) ((f : (a : M) → R) x : R) ((f : (a : M) → R) x_1 : R) *
          HAdd.hAdd (α := R) (β := R) ((g : (a : M) → R) x : R) ((g : (a : M) → R) x_1 : R) -
        HMul.hMul (α := R) (β := R) ((f : (a : M) → R) x : R) ((g : (a : M) → R) x : R) -
      HMul.hMul (α := R) (β := R) ((f : (a : M) → R) x_1 : R) ((g : (a : M) → R) x_1 : R) =
    HSMul.hSMul (α := Module.End R R) 2
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
          HMul.hMul (α := R) (β := R) ((f : (a : M) → R) x : R) ((g : (a : M) → R) x_1 : R)) +
      HSMul.hSMul (α := Module.End R R) 2
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
          HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) x_1 : R))
have h : HAdd.hAdd (α := R) (β := R) ((f : (a : M) → R) x : R) ((f : (a : M) → R) x_1 : R) *
        HAdd.hAdd (α := R) (β := R) ((g : (a : M) → R) x : R) ((g : (a : M) → R) x_1 : R) -
      HMul.hMul (α := R) (β := R) ((f : (a : M) → R) x : R) ((g : (a : M) → R) x : R) -
    HMul.hMul (α := R) (β := R) ((f : (a : M) → R) x_1 : R) ((g : (a : M) → R) x_1 : R) =
  HMul.hMul (α := R) (β := R) ((f : (a : M) → R) x : R) ((g : (a : M) → R) x_1 : R) +
    HMul.hMul (α := R) (β := R) ((g : (a : M) → R) x : R) ((f : (a : M) → R) x_1 : R)
Tactic: simp only [Module.End.smul_def, Module.End.ofNat_apply, nsmul_eq_mul, Nat.cast_ofNat,
    mul_invOf_cancel_left']
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
inst : CommRing R
inst_1 : Invertible (α := R) 2
⊢ HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HAdd.hAdd (α := R →ₗ[R] R →ₗ[R] R) (compl₁₂ (mul R R) LinearMap.id LinearMap.id)
        (compl₁₂ (mul R R) LinearMap.id LinearMap.id)) =
    mul R R
have simp : Eq (α := BilinMap R R R) (compl₁₂ (mul R R) LinearMap.id LinearMap.id) (mul R R)
Tactic: simp only [smul_add, invOf_two_smul_add_invOf_two_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsCancelAdd R
inst_4 : NoZeroDivisors R
inst_5 : CharZero R
B : BilinMap R M R
x y : M
h : LinearMap.IsSymm B
this : AddCancelMonoid R :=
  let __src := inst_3;
  let __src_1 : AddCommMonoid R := inferInstance;
  { toAddMonoid := __src_1.toAddMonoid, toIsLeftCancelAdd := ⋯, toIsRightCancelAdd := ⋯ }
⊢ B.toQuadraticMap.IsOrtho x y ↔ LinearMap.IsOrtho B x y
have simp_rw : HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) +
      HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
    HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) ↔
  Eq.{u_3 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
Tactic: simp_rw [isOrtho_def, LinearMap.isOrtho_def, B.toQuadraticMap_apply, map_add,
    LinearMap.add_apply, add_comm _ (B y y), add_add_add_comm _ _ (B y y), add_comm (B y y)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsCancelAdd R
inst_4 : NoZeroDivisors R
inst_5 : CharZero R
B : BilinMap R M R
x y : M
h : LinearMap.IsSymm B
this : AddCancelMonoid R :=
  let __src := inst_3;
  let __src_1 : AddCommMonoid R := inferInstance;
  { toAddMonoid := __src_1.toAddMonoid, toIsLeftCancelAdd := ⋯, toIsRightCancelAdd := ⋯ }
⊢ HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
          ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) +
        HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
          ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
      HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) ↔
    Eq.{u_3 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
have rw : HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
      ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
    0 ↔
  Eq.{u_3 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
Tactic: rw [add_eq_left (a := B x x + B y y), ← h.eq, RingHom.id_apply, add_self_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsCancelAdd R
inst_4 : NoZeroDivisors R
inst_5 : CharZero R
B : BilinMap R M R
x y : M
h : LinearMap.IsSymm B
this : AddCancelMonoid R :=
  let __src := inst_3;
  let __src_1 : AddCommMonoid R := inferInstance;
  { toAddMonoid := __src_1.toAddMonoid, toIsLeftCancelAdd := ⋯, toIsRightCancelAdd := ⋯ }
rw :
  HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
      0 ↔
    Eq.{u_3 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
⊢ HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
          ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) +
        HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
          ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
      HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) ↔
    Eq.{u_3 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
have rw₁ : HAdd.hAdd (α := R) (β := R)
      ((RingHom.id R : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) : R)
      ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
    0 ↔
  Eq.{u_3 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
Tactic: rw [add_eq_left (a := B x x + B y y), ← h.eq, RingHom.id_apply, add_self_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsCancelAdd R
inst_4 : NoZeroDivisors R
inst_5 : CharZero R
B : BilinMap R M R
x y : M
h : LinearMap.IsSymm B
this : AddCancelMonoid R :=
  let __src := inst_3;
  let __src_1 : AddCommMonoid R := inferInstance;
  { toAddMonoid := __src_1.toAddMonoid, toIsLeftCancelAdd := ⋯, toIsRightCancelAdd := ⋯ }
rw :
  HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
      0 ↔
    Eq.{u_3 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
rw₁ :
  HAdd.hAdd (α := R) (β := R)
        ((RingHom.id R : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) : R)
        ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
      0 ↔
    Eq.{u_3 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
⊢ HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
          ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) +
        HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
          ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
      HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) ↔
    Eq.{u_3 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
have rw₂ : HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
    0 ↔
  Eq.{u_3 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
Tactic: rw [add_eq_left (a := B x x + B y y), ← h.eq, RingHom.id_apply, add_self_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsCancelAdd R
inst_4 : NoZeroDivisors R
inst_5 : CharZero R
B : BilinMap R M R
x y : M
h : LinearMap.IsSymm B
this : AddCancelMonoid R :=
  let __src := inst_3;
  let __src_1 : AddCommMonoid R := inferInstance;
  { toAddMonoid := __src_1.toAddMonoid, toIsLeftCancelAdd := ⋯, toIsRightCancelAdd := ⋯ }
rw :
  HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
      0 ↔
    Eq.{u_3 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
rw₁ :
  HAdd.hAdd (α := R) (β := R)
        ((RingHom.id R : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) : R)
        ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
      0 ↔
    Eq.{u_3 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
rw₂ :
  HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
        ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
      0 ↔
    Eq.{u_3 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
⊢ HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
          ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) +
        HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
          ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
      HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) ↔
    Eq.{u_3 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
have rw₃ : Eq.{u_3 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R) ↔
  Eq.{u_3 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
Tactic: rw [add_eq_left (a := B x x + B y y), ← h.eq, RingHom.id_apply, add_self_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
Q : QuadraticMap R M N
x y : M
⊢ LinearMap.IsOrtho Q.polarBilin x y ↔ Q.IsOrtho x y
have simp_rw : LinearMap.IsOrtho Q.polarBilin x y ↔
  (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
Tactic: simp_rw [isOrtho_def, LinearMap.isOrtho_def, polarBilin_apply_apply, polar, sub_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
Q : QuadraticMap R M N
x y : M
simp_rw :
  LinearMap.IsOrtho Q.polarBilin x y ↔
    (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
⊢ LinearMap.IsOrtho Q.polarBilin x y ↔ Q.IsOrtho x y
have simp_rw₁ : Eq.{u_5 + 1} (α := N) ((((Q.polarBilin : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N) (0 : N) ↔
  (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
Tactic: simp_rw [isOrtho_def, LinearMap.isOrtho_def, polarBilin_apply_apply, polar, sub_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
Q : QuadraticMap R M N
x y : M
simp_rw :
  LinearMap.IsOrtho Q.polarBilin x y ↔
    (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
simp_rw₁ :
  Eq.{u_5 + 1} (α := N) ((((Q.polarBilin : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N) (0 : N) ↔
    (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
⊢ LinearMap.IsOrtho Q.polarBilin x y ↔ Q.IsOrtho x y
have simp_rw₂ : Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) x y) 0 ↔
  (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
Tactic: simp_rw [isOrtho_def, LinearMap.isOrtho_def, polarBilin_apply_apply, polar, sub_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
Q : QuadraticMap R M N
x y : M
simp_rw :
  LinearMap.IsOrtho Q.polarBilin x y ↔
    (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
simp_rw₁ :
  Eq.{u_5 + 1} (α := N) ((((Q.polarBilin : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N) (0 : N) ↔
    (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
simp_rw₂ :
  Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) x y) 0 ↔
    (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
⊢ LinearMap.IsOrtho Q.polarBilin x y ↔ Q.IsOrtho x y
have simp_rw₃ : HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q : (a : M) → N) x : N))
      ((Q : (a : M) → N) y : N) =
    0 ↔
  (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
Tactic: simp_rw [isOrtho_def, LinearMap.isOrtho_def, polarBilin_apply_apply, polar, sub_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
Q : QuadraticMap R M N
x y : M
simp_rw :
  LinearMap.IsOrtho Q.polarBilin x y ↔
    (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
simp_rw₁ :
  Eq.{u_5 + 1} (α := N) ((((Q.polarBilin : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N) (0 : N) ↔
    (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
simp_rw₂ :
  Eq.{u_5 + 1} (α := N) (polar (⇑Q : (a : M) → N) x y) 0 ↔
    (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
simp_rw₃ :
  HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) y : N) =
      0 ↔
    (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
⊢ LinearMap.IsOrtho Q.polarBilin x y ↔ Q.IsOrtho x y
have simp_rw₄ : HSub.hSub (α := N) ((Q : (a : M) → N) (x + y) : N)
      (HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)) =
    0 ↔
  (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
Tactic: simp_rw [isOrtho_def, LinearMap.isOrtho_def, polarBilin_apply_apply, polar, sub_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
Q : QuadraticMap R M N
inst_5 : Invertible (α := R) 2
x y : M
⊢ LinearMap.IsOrtho.{u_3, u_3, u_3, u_5, u_4, u_4} (R := R) (R₁ := R) (R₂ := R) (M := N) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R) ((associated : (a : QuadraticMap R M N) → BilinMap R M N) Q) x y ↔
    Q.IsOrtho x y
have simp_rw : LinearMap.IsOrtho.{u_3, u_3, u_3, u_5, u_4, u_4} (R := R) (R₁ := R) (R₂ := R) (M := N) (I₁ := RingHom.id R) (I₂ :=
    RingHom.id R) ((associated : (a : QuadraticMap R M N) → BilinMap R M N) Q) x y ↔
  (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
Tactic: simp_rw [isOrtho_def, LinearMap.isOrtho_def, associated_apply, invOf_smul_eq_iff,
    smul_zero, sub_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
Q : QuadraticMap R M N
inst_5 : Invertible (α := R) 2
x y : M
simp_rw :
  LinearMap.IsOrtho.{u_3, u_3, u_3, u_5, u_4, u_4} (R := R) (R₁ := R) (R₂ := R) (M := N) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R) ((associated : (a : QuadraticMap R M N) → BilinMap R M N) Q) x y ↔
    (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
⊢ LinearMap.IsOrtho.{u_3, u_3, u_3, u_5, u_4, u_4} (R := R) (R₁ := R) (R₂ := R) (M := N) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R) ((associated : (a : QuadraticMap R M N) → BilinMap R M N) Q) x y ↔
    Q.IsOrtho x y
have simp_rw₁ : Eq.{u_5 + 1} (α := N)
    ((((((associated : (a : QuadraticMap R M N) → BilinMap R M N) Q : BilinMap R M N) : (a : M) → M →ₗ[R] N) x :
            M →ₗ[R] N) :
          (a : M) → N)
        y :
      N)
    (0 : N) ↔
  (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
Tactic: simp_rw [isOrtho_def, LinearMap.isOrtho_def, associated_apply, invOf_smul_eq_iff,
    smul_zero, sub_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
Q : QuadraticMap R M N
inst_5 : Invertible (α := R) 2
x y : M
simp_rw :
  LinearMap.IsOrtho.{u_3, u_3, u_3, u_5, u_4, u_4} (R := R) (R₁ := R) (R₂ := R) (M := N) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R) ((associated : (a : QuadraticMap R M N) → BilinMap R M N) Q) x y ↔
    (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
simp_rw₁ :
  Eq.{u_5 + 1} (α := N)
      ((((((associated : (a : QuadraticMap R M N) → BilinMap R M N) Q : BilinMap R M N) : (a : M) → M →ₗ[R] N) x :
              M →ₗ[R] N) :
            (a : M) → N)
          y :
        N)
      (0 : N) ↔
    (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
⊢ LinearMap.IsOrtho.{u_3, u_3, u_3, u_5, u_4, u_4} (R := R) (R₁ := R) (R₂ := R) (M := N) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R) ((associated : (a : QuadraticMap R M N) → BilinMap R M N) Q) x y ↔
    Q.IsOrtho x y
have simp_rw₂ : HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q : (a : M) → N) x : N))
        ((Q : (a : M) → N) y : N)) =
    0 ↔
  (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
Tactic: simp_rw [isOrtho_def, LinearMap.isOrtho_def, associated_apply, invOf_smul_eq_iff,
    smul_zero, sub_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
Q : QuadraticMap R M N
inst_5 : Invertible (α := R) 2
x y : M
simp_rw :
  LinearMap.IsOrtho.{u_3, u_3, u_3, u_5, u_4, u_4} (R := R) (R₁ := R) (R₂ := R) (M := N) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R) ((associated : (a : QuadraticMap R M N) → BilinMap R M N) Q) x y ↔
    (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
simp_rw₁ :
  Eq.{u_5 + 1} (α := N)
      ((((((associated : (a : QuadraticMap R M N) → BilinMap R M N) Q : BilinMap R M N) : (a : M) → M →ₗ[R] N) x :
              M →ₗ[R] N) :
            (a : M) → N)
          y :
        N)
      (0 : N) ↔
    (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
simp_rw₂ :
  HSMul.hSMul (α := Module.End R N) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
        (HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q : (a : M) → N) x : N))
          ((Q : (a : M) → N) y : N)) =
      0 ↔
    (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
⊢ LinearMap.IsOrtho.{u_3, u_3, u_3, u_5, u_4, u_4} (R := R) (R₁ := R) (R₂ := R) (M := N) (I₁ := RingHom.id R) (I₂ :=
      RingHom.id R) ((associated : (a : QuadraticMap R M N) → BilinMap R M N) Q) x y ↔
    Q.IsOrtho x y
have simp_rw₃ : HSub.hSub (β := N) (HSub.hSub (α := N) (β := N) ((Q : (a : M) → N) (x + y) : N) ((Q : (a : M) → N) x : N))
      ((Q : (a : M) → N) y : N) =
    HSMul.hSMul (α := Module.End R N) (β := N) 2 0 ↔
  (Q : (a : M) → N) (x + y) = HAdd.hAdd (α := N) (β := N) ((Q : (a : M) → N) x : N) ((Q : (a : M) → N) y : N)
Tactic: simp_rw [isOrtho_def, LinearMap.isOrtho_def, associated_apply, invOf_smul_eq_iff,
    smul_zero, sub_sub, sub_eq_zero]