awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Subspace K V
x_1 : ℙ K V
x : V
hx : x ≠ 0
⊢ Membership.mem (γ := Set (ℙ K V))
      (carrier
        ((fun (s : Submodule K V) ↦
            { carrier := setOf (Projectivization.lift (fun (x : { v : V // v ≠ 0 }) ↦ (↑x : V) ∈ s) ⋯), mem_add' := ⋯ :
              Subspace K V })
          ((fun (s : Subspace K V) ↦
              ({ carrier := {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}, add_mem' := ⋯,
                  zero_mem' := ⋯, smul_mem' := ⋯ } :
                Submodule K V))
            s)))
      (Quot.mk (⇑(projectivizationSetoid K V) : { v : V // v ≠ 0 } → { v : V // v ≠ 0 } → Prop)
        (Subtype.mk (p := fun (v : V) ↦ v ≠ 0) x hx)) ↔
    Quot.mk (⇑(projectivizationSetoid K V) : { v : V // v ≠ 0 } → { v : V // v ≠ 0 } → Prop)
        (Subtype.mk (p := fun (v : V) ↦ v ≠ 0) x hx) ∈
      s.carrier

Tactic:
exact ⟨fun h => h hx, fun h _ => h⟩
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Submodule K V
h :
  ∀ (x : V),
    Membership.mem (γ := Submodule K V)
        ((fun (s : Subspace K V) ↦
            ({ carrier := {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}, add_mem' := ⋯, zero_mem' := ⋯,
                smul_mem' := ⋯ } :
              Submodule K V))
          ((fun (s : Submodule K V) ↦
              { carrier := setOf (Projectivization.lift (fun (x : { v : V // v ≠ 0 }) ↦ (↑x : V) ∈ s) ⋯),
                mem_add' := ⋯ : Subspace K V })
            s))
        x ↔
      x ∈ s
⊢ (fun (s : Subspace K V) ↦
        ({ carrier := {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}, add_mem' := ⋯, zero_mem' := ⋯,
            smul_mem' := ⋯ } :
          Submodule K V))
      ((fun (s : Submodule K V) ↦
          { carrier := setOf (Projectivization.lift (fun (x : { v : V // v ≠ 0 }) ↦ (↑x : V) ∈ s) ⋯), mem_add' := ⋯ :
            Subspace K V })
        s) =
    s

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Submodule K V
x : V
this : x = 0 → x ∈ s
⊢ Membership.mem (γ := Submodule K V)
      ((fun (s : Subspace K V) ↦
          ({ carrier := {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}, add_mem' := ⋯, zero_mem' := ⋯,
              smul_mem' := ⋯ } :
            Submodule K V))
        ((fun (s : Submodule K V) ↦
            { carrier := setOf (Projectivization.lift (fun (x : { v : V // v ≠ 0 }) ↦ (↑x : V) ∈ s) ⋯), mem_add' := ⋯ :
              Subspace K V })
          s))
      x ↔
    x ∈ s

Tactic:
simpa [imp_iff_not_or]

Premises used: imp_iff_not_or
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Submodule K V
x : V
h : x = 0 → x ∈ s
⊢ Membership.mem (γ := Submodule K V)
      ((fun (s : Subspace K V) ↦
          ({ carrier := {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}, add_mem' := ⋯, zero_mem' := ⋯,
              smul_mem' := ⋯ } :
            Submodule K V))
        ((fun (s : Submodule K V) ↦
            { carrier := setOf (Projectivization.lift (fun (x : { v : V // v ≠ 0 }) ↦ (↑x : V) ∈ s) ⋯), mem_add' := ⋯ :
              Subspace K V })
          s))
      x ↔
    x ∈ s

Tactic:
suffices x = 0 → x ∈ s by
      simpa [imp_iff_not_or]
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Submodule K V
⊢ 0 ∈ s

Tactic:
s.zero_mem

Premises used: Set.Mem, Submodule.zero_mem
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Submodule K V
⊢ 0 ∈ s

Tactic:
exact s.zero_mem

Premises used: Submodule.zero_mem
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Subspace K V
v : V
hv : v ≠ 0
⊢ Membership.mem (γ := Submodule K V) ((submodule : (a : Subspace K V) → Submodule K V) s : Submodule K V) v ↔
    Projectivization.mk K v hv ∈ s

Tactic:
⟨fun h => h hv, fun h _ => h⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Submodule K V
v : V
hv : v ≠ 0
⊢ Membership.mem (γ := Projectivization.Subspace K V)
      ((projectivization : (a : Submodule K V) → Projectivization.Subspace K V) s : Projectivization.Subspace K V)
      (Projectivization.mk K v hv) ↔
    v ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Projectivization.lift
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Submodule K V
x : ℙ K V
h :
  ∀ (v : V) (h : v ≠ 0),
    Membership.mem (γ := Projectivization.Subspace K V)
        ((projectivization : (a : Submodule K V) → Projectivization.Subspace K V) s : Projectivization.Subspace K V)
        (Projectivization.mk K v h) ↔
      Projectivization.submodule (Projectivization.mk K v h) ≤ s
⊢ Membership.mem (γ := Projectivization.Subspace K V)
      ((projectivization : (a : Submodule K V) → Projectivization.Subspace K V) s : Projectivization.Subspace K V) x ↔
    x.submodule ≤ s

Tactic:
cases x
-- Module: Mathlib.LinearAlgebra.Projectivization.Subspace
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Submodule K V
v : V
h_1 : v ≠ 0
h : v ∈ s ↔ Projectivization.submodule (Projectivization.mk K v h_1) ≤ s
h₁ : v ∈ s ↔ K ∙ v ≤ s
h₂ h₃ : v ∈ s ↔ v ∈ s
⊢ Membership.mem (γ := Projectivization.Subspace K V)
      ((projectivization : (a : Submodule K V) → Projectivization.Subspace K V) s : Projectivization.Subspace K V)
      (Projectivization.mk K v h_1) ↔
    Projectivization.submodule (Projectivization.mk K v h_1) ≤ s

Tactic:
rw [mk_mem_projectivization_iff, Projectivization.submodule_mk,
    Submodule.span_singleton_le_iff_mem]

Premises used: Submodule.mk_mem_projectivization_iff, Projectivization.submodule_mk, Submodule.span_singleton_le_iff_mem
-- Module: Mathlib.LinearAlgebra.QuadraticForm.AlgClosed
Goal:
ι : Type u_1
inst : Fintype ι
K : Type u_2
inst_1 : Field K
inst_2 : IsAlgClosed K
inst_3 : DecidableEq K
w : ι → K
i : ι
h : ¬w i = 0
rw : w i ≠ 0
⊢ Exists.choose (p := fun (z : K) ↦ w i = z * z) ⋯ ≠ 0

Tactic:
rw [← mul_self_eq_zero.ne, ← (IsAlgClosed.exists_eq_mul_self (w i)).choose_spec]

Premises used: mul_self_eq_zero, Exists.choose_spec, Iff.ne, IsAlgClosed.exists_eq_mul_self
-- Module: Mathlib.LinearAlgebra.QuadraticForm.AlgClosed
Goal:
ι : Type u_1
inst : Fintype ι
K : Type u_2
inst_1 : Field K
inst_2 : IsAlgClosed K
inst_3 : DecidableEq K
w : ι → K
i : ι
h : ¬w i = 0
⊢ w i ≠ 0

Tactic:
simpa using h
-- Module: Mathlib.LinearAlgebra.QuadraticForm.AlgClosed
Goal:
ι : Type u_1
inst : Fintype ι
K : Type u_2
inst_1 : Field K
inst_2 : IsAlgClosed K
inst_3 : DecidableEq K
w : ι → K
refine :
  ∀ (i : ι),
    (if w i = 0 then 0 else 1) *
        HPow.hPow (α := K) (β := ℕ)
          (↑((fun (i : ι) ↦
                  (if h : w i = 0 then 1 else Units.mk0 (Exists.choose (p := fun (z : K) ↦ w i = z * z) ⋯) ⋯ : Kˣ))
                i) :
            K)
          2 =
      w i
⊢ IsometryEquiv (M₂ := ι → K) (weightedSumSquares K w)
    (weightedSumSquares (S := K) K fun (i : ι) ↦ if w i = 0 then 0 else 1)

Tactic:
refine isometryEquivWeightedSumSquaresWeightedSumSquares (fun i => if h : w i = 0 then 1 else
    Units.mk0 (IsAlgClosed.exists_eq_mul_self (w i)).choose (by
      rw [← mul_self_eq_zero.ne, ← (IsAlgClosed.exists_eq_mul_self (w i)).choose_spec]
      simpa using h)) ?_

Premises used: dite, Units.mk0, QuadraticForm.isometryEquivWeightedSumSquaresWeightedSumSquares, Exists.choose, OfNat.ofNat, Eq, IsAlgClosed.exists_eq_mul_self
-- Module: Mathlib.LinearAlgebra.QuadraticForm.AlgClosed
Goal:
ι : Type u_1
inst : Fintype ι
K : Type u_2
inst_1 : Field K
inst_2 : IsAlgClosed K
inst_3 : DecidableEq K
w : ι → K
i : ι
pos :
  ∀ (h : w i = 0),
    0 *
        HPow.hPow (α := K) (β := ℕ)
          (↑((fun (i : ι) ↦
                  (if h : w i = 0 then 1 else Units.mk0 (Exists.choose (p := fun (z : K) ↦ w i = z * z) ⋯) ⋯ : Kˣ))
                i) :
            K)
          2 =
      w i
neg :
  ∀ (h : ¬w i = 0),
    1 *
        HPow.hPow (α := K) (β := ℕ)
          (↑((fun (i : ι) ↦
                  (if h : w i = 0 then 1 else Units.mk0 (Exists.choose (p := fun (z : K) ↦ w i = z * z) ⋯) ⋯ : Kˣ))
                i) :
            K)
          2 =
      w i
⊢ (if w i = 0 then 0 else 1) *
      HPow.hPow (α := K) (β := ℕ)
        (↑((fun (i : ι) ↦
                (if h : w i = 0 then 1 else Units.mk0 (Exists.choose (p := fun (z : K) ↦ w i = z * z) ⋯) ⋯ : Kˣ))
              i) :
          K)
        2 =
    w i

Tactic:
split_ifs with h
-- Module: Mathlib.LinearAlgebra.QuadraticForm.AlgClosed
Goal:
ι : Type u_1
inst : Fintype ι
K : Type u_2
inst_1 : Field K
inst_2 : IsAlgClosed K
inst_3 : DecidableEq K
w : ι → K
i : ι
h : w i = 0
⊢ 0 *
      HPow.hPow (α := K) (β := ℕ)
        (↑((fun (i : ι) ↦
                (if h : w i = 0 then 1 else Units.mk0 (Exists.choose (p := fun (z : K) ↦ w i = z * z) ⋯) ⋯ : Kˣ))
              i) :
          K)
        2 =
    w i

Tactic:
simp [h, pow_two, ← (IsAlgClosed.exists_eq_mul_self (w i : K)).choose_spec]

Premises used: Exists.choose_spec, pow_two, IsAlgClosed.exists_eq_mul_self
-- Module: Mathlib.LinearAlgebra.QuadraticForm.AlgClosed
Goal:
ι : Type u_1
inst : Fintype ι
K : Type u_2
inst_1 : Field K
inst_2 : IsAlgClosed K
inst_3 : DecidableEq K
w : ι → K
i : ι
h : ¬w i = 0
⊢ 1 *
      HPow.hPow (α := K) (β := ℕ)
        (↑((fun (i : ι) ↦
                (if h : w i = 0 then 1 else Units.mk0 (Exists.choose (p := fun (z : K) ↦ w i = z * z) ⋯) ⋯ : Kˣ))
              i) :
          K)
        2 =
    w i

Tactic:
simp [h, pow_two, ← (IsAlgClosed.exists_eq_mul_self (w i : K)).choose_spec]

Premises used: Exists.choose_spec, pow_two, IsAlgClosed.exists_eq_mul_self
-- Module: Mathlib.LinearAlgebra.QuadraticForm.AlgClosed
Goal:
ι : Type u_1
inst : Fintype ι
K : Type u_2
inst_1 : Field K
inst_2 : IsAlgClosed K
inst_3 : DecidableEq K
w : ι → Kˣ
h : ∀ (x : ι), Eq.{u_2 + 1} (α := K) (if (↑(w x) : K) = 0 then 0 else 1) (1 x)
⊢ Eq (α := ι → K) (fun (i : ι) ↦ if (↑(w i) : K) = 0 then 0 else 1) 1

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.QuadraticForm.AlgClosed
Goal:
ι : Type u_1
inst : Fintype ι
K : Type u_2
inst_1 : Field K
inst_2 : IsAlgClosed K
inst_3 : DecidableEq K
w : ι → Kˣ
x : ι
⊢ Eq.{u_2 + 1} (α := K) (if (↑(w x) : K) = 0 then 0 else 1) (1 x)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.QuadraticForm.AlgClosed
Goal:
K : Type u_2
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : Invertible (α := K) 2
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module K M
inst_5 : FiniteDimensional K M
Q : QuadraticForm K M
hQ :
  LinearMap.SeparatingLeft.{u_2, u_2, u_2, u_2, u_3, u_3} (R := K) (R₁ := K) (R₂ := K) (M := K) (M₁ := M) (M₂ := M)
    (I₁ := RingHom.id K) (I₂ := RingHom.id K)
    (((associated.{u_2, u_3, u_2} (R := K) (M := M) (N := K) : QuadraticMap K M K →ₗ[K] LinearMap.BilinMap K M K) :
        (a : QuadraticMap K M K) → LinearMap.BilinMap K M K)
      Q)
⊢ Equivalent (M₂ := Fin (Module.finrank K M) → K) Q (weightedSumSquares (S := K) K 1)

Tactic:
open Classical in
  let ⟨w, ⟨hw₁⟩⟩ := Q.equivalent_weightedSumSquares_units_of_nondegenerate' hQ
  ⟨hw₁.trans (isometryEquivSumSquaresUnits w)⟩

Premises used: Nonempty.intro, QuadraticForm.isometryEquivSumSquaresUnits, QuadraticMap.weightedSumSquares, OfNat.ofNat, QuadraticMap.IsometryEquiv.trans, _private.0.QuadraticForm.equivalent_weightedSumSquares_of_isAlgClosed.match_1, QuadraticMap.Equivalent, QuadraticForm.equivalent_weightedSumSquares_units_of_nondegenerate'
-- Module: Mathlib.LinearAlgebra.QuadraticForm.AlgClosed
Goal:
K : Type u_2
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : Invertible (α := K) 2
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module K M
inst_5 : FiniteDimensional K M
Q₁ Q₂ : QuadraticForm K M
hQ₁ :
  LinearMap.SeparatingLeft.{u_2, u_2, u_2, u_2, u_3, u_3} (R := K) (R₁ := K) (R₂ := K) (M := K) (M₁ := M) (M₂ := M)
    (I₁ := RingHom.id K) (I₂ := RingHom.id K)
    (((associated.{u_2, u_3, u_2} (R := K) (M := M) (N := K) : QuadraticMap K M K →ₗ[K] LinearMap.BilinMap K M K) :
        (a : QuadraticMap K M K) → LinearMap.BilinMap K M K)
      Q₁)
hQ₂ :
  LinearMap.SeparatingLeft.{u_2, u_2, u_2, u_2, u_3, u_3} (R := K) (R₁ := K) (R₂ := K) (M := K) (M₁ := M) (M₂ := M)
    (I₁ := RingHom.id K) (I₂ := RingHom.id K)
    (((associated.{u_2, u_3, u_2} (R := K) (M := M) (N := K) : QuadraticMap K M K →ₗ[K] LinearMap.BilinMap K M K) :
        (a : QuadraticMap K M K) → LinearMap.BilinMap K M K)
      Q₂)
⊢ Equivalent Q₁ Q₂

Tactic:
open Classical in
  (Q₁.equivalent_weightedSumSquares_of_isAlgClosed hQ₁).trans
  (Q₂.equivalent_weightedSumSquares_of_isAlgClosed hQ₂).symm

Premises used: QuadraticMap.Equivalent.trans, QuadraticForm.equivalent_weightedSumSquares_of_isAlgClosed, QuadraticMap.Equivalent.symm
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
f : M → N
x y : M
rw : f (x + y) = f x + f y + (f (x + y) - f x - f y)
⊢ f (x + y) = f x + f y + polar f x y

Tactic:
rw [polar]

Premises used: QuadraticMap.polar
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
f : M → N
x y : M
⊢ f (x + y) = f x + f y + (f (x + y) - f x - f y)

Tactic:
abel
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
f g : M → N
x y : M
simp : f (x + y) + g (x + y) - (f x + g x) - (f y + g y) = f (x + y) - f x - f y + (g (x + y) - g x - g y)
⊢ polar (f + g) x y = polar f x y + polar g x y

Tactic:
simp only [polar, Pi.add_apply]

Premises used: QuadraticMap.polar, Pi.add_apply
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
f g : M → N
x y : M
⊢ f (x + y) + g (x + y) - (f x + g x) - (f y + g y) = f (x + y) - f x - f y + (g (x + y) - g x - g y)

Tactic:
abel
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
f : M → N
x y : M
⊢ polar (-f) x y = -polar f x y

Tactic:
simp only [polar, Pi.neg_apply, sub_eq_add_neg, neg_add]

Premises used: sub_eq_add_neg, neg_add, QuadraticMap.polar, Pi.neg_apply
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
S : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
inst_2 : Monoid S
inst_3 : DistribMulAction S N
f : M → N
s : S
x y : M
⊢ polar (s • f) x y = s • polar f x y

Tactic:
simp only [polar, Pi.smul_apply, smul_sub]

Premises used: QuadraticMap.polar, smul_sub, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
f : M → N
x y : M
rw : f (x + y) - f x - f y = polar f y x
rw₁ : f (x + y) - f x - f y = f (y + x) - f y - f x
rw₂ : f (y + x) - f x - f y = f (y + x) - f y - f x
rw₃ : f (y + x) - (f x + f y) = f (y + x) - f y - f x
rw₄ : f (y + x) - (f x + f y) = f (y + x) - (f y + f x)
rw₅ rw₆ : f (y + x) - (f y + f x) = f (y + x) - (f y + f x)
⊢ polar f x y = polar f y x

Tactic:
rw [polar, polar, add_comm, sub_sub, sub_sub, add_comm (f x) (f y)]

Premises used: QuadraticMap.polar, add_comm, sub_sub
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
f : M → N
x x' y : M
simp :
  polar f (x + x') y = polar f x y + polar f x' y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (y + x)
⊢ polar f (x + x') y = polar f x y + polar f x' y ↔
    f (x + x' + y) + (f x + f x' + f y) = f (x + x') + f (x' + y) + f (y + x)

Tactic:
simp only [← add_assoc]

Premises used: add_assoc
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
f : M → N
x x' y : M
simp :
  f (x + x' + y) + f y + f x' + f y + f x = f (x + y) + f (x' + y) + f y + f (x + x') ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (y + x)
⊢ polar f (x + x') y = polar f x y + polar f x' y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (y + x)

Tactic:
simp only [polar, sub_eq_iff_eq_add, eq_sub_iff_add_eq, sub_add_eq_add_sub, add_sub]

Premises used: add_sub, eq_sub_iff_add_eq, QuadraticMap.polar, sub_eq_iff_eq_add, sub_add_eq_add_sub
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
f : M → N
x x' y : M
simp :
  f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x' + y) + f (x + x') + f y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (y + x)
⊢ f (x + x' + y) + f y + f x' + f y + f x = f (x + y) + f (x' + y) + f y + f (x + x') ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (y + x)

Tactic:
simp only [add_right_comm _ (f y) _, add_right_comm _ (f x') (f x)]

Premises used: add_right_comm
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
f : M → N
x x' y : M
rw :
  f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x' + y) + f (x + x') + f y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (x + y)
rw₁ :
  f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x' + y) + f (x + x') + f y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x + y) + f (x' + y)
rw₂ :
  f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x' + y) + f (x + x') + f y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + y) + f (x + x') + f (x' + y)
rw₃ :
  f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x + x') + f (x' + y) + f y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + y) + f (x + x') + f (x' + y)
rw₄ rw₅ :
  f (x + x' + y) + f x + f x' + f y = f (x + y) + f (x + x') + f (x' + y) ↔
    f (x + x' + y) + f x + f x' + f y = f (x + y) + f (x + x') + f (x' + y)
⊢ f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x' + y) + f (x + x') + f y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (y + x)

Tactic:
rw [add_comm y x, add_right_comm _ _ (f (x + y)), add_comm _ (f (x + y)),
    add_right_comm (f (x + y)), add_left_inj]

Premises used: add_right_comm, add_left_inj, add_comm, HAdd.hAdd
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
S : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
F : Type u_8
inst_2 : AddCommGroup S
inst_3 : FunLike F N S
inst_4 : AddMonoidHomClass F N S
f : M → N
g : F
x y : M
⊢ Eq.{u_1 + 1} (α := S) (polar ((⇑g : (a : N) → S) ∘ f) x y : S) ((g : (a : N) → S) (polar f x y) : S)

Tactic:
simp only [polar, Function.comp_apply, map_sub]

Premises used: map_sub, QuadraticMap.polar, Function.comp_apply
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
f : M → N
x y : M
⊢ polarSym2 f s(x, y) = polar f x y

Tactic:
rfl

Premises used: QuadraticMap.polar, rfl, QuadraticMap.polarSym2
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q Q' x y : QuadraticMap R M N
h : x.toFun = y.toFun
mk :
  ∀ (toFun : M → N) (toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x)
    (exists_companion' :
      ∃ (B : BilinMap R M N),
        ∀ (x y : M),
          toFun (x + y) =
            HAdd.hAdd (β := N) (toFun x + toFun y) ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N))
    (h :
      { toFun := toFun, toFun_smul := toFun_smul, exists_companion' := exists_companion' : QuadraticMap R M N }.toFun =
        y.toFun),
    { toFun := toFun, toFun_smul := toFun_smul, exists_companion' := exists_companion' : QuadraticMap R M N } = y
⊢ x = y

Tactic:
cases x
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q Q' y : QuadraticMap R M N
toFun : M → N
toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x
exists_companion' :
  ∃ (B : BilinMap R M N),
    ∀ (x y : M),
      toFun (x + y) =
        HAdd.hAdd (β := N) (toFun x + toFun y) ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
h :
  { toFun := toFun, toFun_smul := toFun_smul, exists_companion' := exists_companion' : QuadraticMap R M N }.toFun =
    y.toFun
mk :
  ∀ (toFun_1 : M → N) (toFun_smul_1 : ∀ (a : R) (x : M), toFun_1 (a • x) = (a * a) • toFun_1 x)
    (exists_companion'_1 :
      ∃ (B : BilinMap R M N),
        ∀ (x y : M),
          toFun_1 (x + y) =
            HAdd.hAdd (β := N) (toFun_1 x + toFun_1 y)
              ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N))
    (h :
      { toFun := toFun, toFun_smul := toFun_smul, exists_companion' := exists_companion' : QuadraticMap R M N }.toFun =
        { toFun := toFun_1, toFun_smul := toFun_smul_1, exists_companion' := exists_companion'_1 :
            QuadraticMap R M N }.toFun),
    { toFun := toFun, toFun_smul := toFun_smul, exists_companion' := exists_companion' : QuadraticMap R M N } =
      { toFun := toFun_1, toFun_smul := toFun_smul_1, exists_companion' := exists_companion'_1 }
⊢ { toFun := toFun, toFun_smul := toFun_smul, exists_companion' := exists_companion' : QuadraticMap R M N } = y

Tactic:
cases y
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
S : Type u_1
T : Type u_2
R : Type u_3
M : Type u_4
N : Type u_5
P : Type u_6
A : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q Q' : QuadraticMap R M N
toFun : M → N
toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = (a * a) • toFun x
exists_companion' :
  ∃ (B : BilinMap R M N),
    ∀ (x y : M),
      toFun (x + y) =
        HAdd.hAdd (β := N) (toFun x + toFun y) ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
toFun_1 : M → N
toFun_smul_1 : ∀ (a : R) (x : M), toFun_1 (a • x) = (a * a) • toFun_1 x
exists_companion'_1 :
  ∃ (B : BilinMap R M N),
    ∀ (x y : M),
      toFun_1 (x + y) =
        HAdd.hAdd (β := N) (toFun_1 x + toFun_1 y) ((((B : (a : M) → M →ₗ[R] N) x : M →ₗ[R] N) : (a : M) → N) y : N)
h :
  { toFun := toFun, toFun_smul := toFun_smul, exists_companion' := exists_companion' : QuadraticMap R M N }.toFun =
    { toFun := toFun_1, toFun_smul := toFun_smul_1, exists_companion' := exists_companion'_1 :
        QuadraticMap R M N }.toFun
⊢ { toFun := toFun, toFun_smul := toFun_smul, exists_companion' := exists_companion' : QuadraticMap R M N } =
    { toFun := toFun_1, toFun_smul := toFun_smul_1, exists_companion' := exists_companion'_1 }

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
Q : QuadraticMap R M N
⊢ Q.toFun = (⇑Q : (a : M) → N)

Tactic:
rfl

Premises used: rfl