awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Subspace (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Set (ℙ K V)
W : Subspace K V
⊢ W ⊔ span S = span ((↑W : Set (ℙ K V)) ∪ S)
have rw : W ⊔ span S = span (↑W : Set (ℙ K V)) ⊔ span S
Tactic: rw [span_union, span_coe]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Subspace (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Set (ℙ K V)
W : Subspace K V
rw : W ⊔ span S = span (↑W : Set (ℙ K V)) ⊔ span S
⊢ W ⊔ span S = span ((↑W : Set (ℙ K V)) ∪ S)
have rw₁ : W ⊔ span S = W ⊔ span S
Tactic: rw [span_union, span_coe]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Subspace (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Set (ℙ K V)
W : Subspace K V
⊢ span S ⊔ W = span (S ∪ (↑W : Set (ℙ K V)))
have rw : span S ⊔ W = span S ⊔ span (↑W : Set (ℙ K V))
Tactic: rw [span_union, span_coe]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Subspace (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Set (ℙ K V)
W : Subspace K V
rw : span S ⊔ W = span S ⊔ span (↑W : Set (ℙ K V))
⊢ span S ⊔ W = span (S ∪ (↑W : Set (ℙ K V)))
have rw₁ : span S ⊔ W = span S ⊔ W
Tactic: rw [span_union, span_coe]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Subspace (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Set (ℙ K V)
u : ℙ K V
⊢ u ∈ span S ↔ ∀ (W : Subspace K V), S ⊆ (↑W : Set (ℙ K V)) → u ∈ W
have simp_rw : u ∈ span S ↔ ∀ (W : Subspace K V), span S ≤ W → u ∈ W
Tactic: simp_rw [← span_le_subspace_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Subspace (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Set (ℙ K V)
⊢ span S = sInf {W : Subspace K V | S ⊆ (↑W : Set (ℙ K V))}
have carrier : ∀ (x : ℙ K V),
  x ∈ (span S).carrier ↔
    Membership.mem (γ := Set (ℙ K V)) (carrier (sInf {W : Subspace K V | S ⊆ (↑W : Set (ℙ K V))})) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Subspace (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Set (ℙ K V)
x : ℙ K V
⊢ x ∈ (span S).carrier ↔
    Membership.mem (γ := Set (ℙ K V)) (carrier (sInf {W : Subspace K V | S ⊆ (↑W : Set (ℙ K V))})) x
have carrier : (∀ (W : Subspace K V), S ⊆ (↑W : Set (ℙ K V)) → x ∈ W) ↔
  Membership.mem (γ := Subspace K V) (sInf {W : Subspace K V | S ⊆ (↑W : Set (ℙ K V))}) x
Tactic: simp_rw [mem_carrier_iff, mem_span x]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Subspace (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Set (ℙ K V)
x : ℙ K V
⊢ (∀ (W : Subspace K V), S ⊆ (↑W : Set (ℙ K V)) → x ∈ W) ↔
    Membership.mem (γ := Subspace K V) (sInf {W : Subspace K V | S ⊆ (↑W : Set (ℙ K V))}) x
have carrier : ∀ (hx : ∀ (W : Subspace K V), S ⊆ (↑W : Set (ℙ K V)) → x ∈ W),
  Membership.mem (γ := Subspace K V) (sInf {W : Subspace K V | S ⊆ (↑W : Set (ℙ K V))}) x
Tactic: refine ⟨fun hx => ?_, fun hx W hW => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Subspace (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
S : Set (ℙ K V)
x : ℙ K V
carrier :
  ∀ (hx : ∀ (W : Subspace K V), S ⊆ (↑W : Set (ℙ K V)) → x ∈ W),
    Membership.mem (γ := Subspace K V) (sInf {W : Subspace K V | S ⊆ (↑W : Set (ℙ K V))}) x
⊢ (∀ (W : Subspace K V), S ⊆ (↑W : Set (ℙ K V)) → x ∈ W) ↔
    Membership.mem (γ := Subspace K V) (sInf {W : Subspace K V | S ⊆ (↑W : Set (ℙ K V))}) x
have carrier₁ : ∀ (hx : Membership.mem (γ := Subspace K V) (sInf {W : Subspace K V | S ⊆ (↑W : Set (ℙ K V))}) x) (W : Subspace K V)
  (hW : S ⊆ (↑W : Set (ℙ K V))), x ∈ W
Tactic: refine ⟨fun hx => ?_, fun hx W hW => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Subspace (goal)
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 y : V
hx₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} x
hy₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} y
⊢ Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} (x + y)
have inl : ∀ (hx₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} 0),
  Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} (0 + y)
Tactic: rcases eq_or_ne x 0 with rfl | hx₂
Cleared hypotheses: x, hx₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Subspace (goal)
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 y : V
hx₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} x
hy₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} y
inl :
  ∀ (hx₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} 0),
    Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} (0 + y)
⊢ Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} (x + y)
have inr : ∀ (hx₂ : x ≠ 0), Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} (x + y)
Tactic: rcases eq_or_ne x 0 with rfl | hx₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Subspace (goal)
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 y : V
hx₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} x
hy₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} y
hx₂ : x ≠ 0
⊢ Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} (x + y)
have inr : ∀ (hy₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} 0),
  Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} (x + 0)
Tactic: rcases eq_or_ne y 0 with rfl | hy₂
Cleared hypotheses: y, hy₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Subspace (goal)
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 y : V
hx₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} x
hy₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} y
hx₂ : x ≠ 0
inr :
  ∀ (hy₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} 0),
    Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} (x + 0)
⊢ Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} (x + y)
have inr₁ : ∀ (hy₂ : y ≠ 0), Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} (x + y)
Tactic: rcases eq_or_ne y 0 with rfl | hy₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Subspace (goal)
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
c : K
x : V
h₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} x
h₂ : c • x ≠ 0
⊢ Projectivization.mk K (c • x) h₂ ∈ s.carrier
have h : Eq (α := ℙ K V) (Projectivization.mk K (c • x) h₂) (Projectivization.mk K x sorry)
Tactic: convert! h₁ (right_ne_zero_of_smul h₂) using 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Subspace (goal)
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
c : K
x : V
h₁ : Membership.mem (γ := Set V) {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier} x
h₂ : c • x ≠ 0
⊢ Eq (α := ℙ K V) (Projectivization.mk K (c • x) h₂) (Projectivization.mk K x ⋯)
have h : ∃ (a : K), a • x = c • x
Tactic: rw [Projectivization.mk_eq_mk_iff']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Subspace (goal)
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
⊢ (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) =
    s
have carrier : ∀ (x : ℙ 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) sorry), mem_add' := sorry :
              Subspace K V })
          ((fun (s : Subspace K V) ↦
              ({ carrier := {x : V | ∀ (h : x ≠ 0), Projectivization.mk K x h ∈ s.carrier}, add_mem' := sorry,
                  zero_mem' := sorry, smul_mem' := sorry } :
                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: ext ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Subspace (goal)
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
⊢ (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
have 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' := sorry, zero_mem' := sorry,
              smul_mem' := sorry } :
            Submodule K V))
        ((fun (s : Submodule K V) ↦
            { carrier := setOf (Projectivization.lift (fun (x : { v : V // v ≠ 0 }) ↦ (↑x : V) ∈ s) sorry), mem_add' := sorry :
              Subspace K V })
          s))
      x ↔
    x ∈ s
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Subspace (goal)
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
⊢ 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
have h : x = 0 → x ∈ s
Tactic: suffices x = 0 → x ∈ s by
      simpa [imp_iff_not_or]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Subspace (goal)
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
⊢ Membership.mem (γ := Projectivization.Subspace K V)
      ((projectivization : (a : Submodule K V) → Projectivization.Subspace K V) s : Projectivization.Subspace K V) x ↔
    x.submodule ≤ s
have 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
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Subspace (goal)
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 : 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
have h : v ∈ s ↔ Projectivization.submodule (Projectivization.mk K v h) ≤ s
Tactic: rw [mk_mem_projectivization_iff, Projectivization.submodule_mk,
    Submodule.span_singleton_le_iff_mem]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Subspace (goal)
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
⊢ 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
have h₁ : v ∈ s ↔ K ∙ v ≤ s
Tactic: rw [mk_mem_projectivization_iff, Projectivization.submodule_mk,
    Submodule.span_singleton_le_iff_mem]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projectivization.Subspace (goal)
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
⊢ 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
have h₂ : v ∈ s ↔ v ∈ s
Tactic: rw [mk_mem_projectivization_iff, Projectivization.submodule_mk,
    Submodule.span_singleton_le_iff_mem]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.AlgClosed (goal)
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
⊢ Exists.choose (p := fun (z : K) ↦ w i = z * z) ⋯ ≠ 0
have rw : w i ≠ 0
Tactic: rw [← mul_self_eq_zero.ne, ← (IsAlgClosed.exists_eq_mul_self (w i)).choose_spec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.AlgClosed (goal)
Goal:
ι : Type u_1
inst : Fintype ι
K : Type u_2
inst_1 : Field K
inst_2 : IsAlgClosed K
inst_3 : DecidableEq K
w : ι → K
⊢ IsometryEquiv (M₂ := ι → K) (weightedSumSquares K w)
    (weightedSumSquares (S := K) K fun (i : ι) ↦ if w i = 0 then 0 else 1)
have 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) sorry) sorry : Kˣ))
              i) :
          K)
        2 =
    w i
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)) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.AlgClosed (goal)
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 : ι
⊢ (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
have 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) sorry) sorry : Kˣ))
              i) :
          K)
        2 =
    w i
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.AlgClosed (goal)
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
⊢ (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
have 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) sorry) sorry : Kˣ))
              i) :
          K)
        2 =
    w i
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.AlgClosed (goal)
Goal:
ι : Type u_1
inst : Fintype ι
K : Type u_2
inst_1 : Field K
inst_2 : IsAlgClosed K
inst_3 : DecidableEq K
w : ι → Kˣ
⊢ Eq (α := ι → K) (fun (i : ι) ↦ if (↑(w i) : K) = 0 then 0 else 1) 1
have h : ∀ (x : ι), Eq.{u_2 + 1} (α := K) (if (↑(w x) : K) = 0 then 0 else 1) (1 x)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
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 + polar f x y
have rw : f (x + y) = f x + f y + (f (x + y) - f x - f y)
Tactic: rw [polar]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
f g : M → N
x y : M
⊢ polar (f + g) x y = polar f x y + polar g x y
have 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)
Tactic: simp only [polar, Pi.add_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
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 y x
have rw : f (x + y) - f x - f y = polar f y x
Tactic: rw [polar, polar, add_comm, sub_sub, sub_sub, add_comm (f x) (f y)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
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
⊢ polar f x y = polar f y x
have rw₁ : f (x + y) - f x - f y = f (y + x) - f y - f x
Tactic: rw [polar, polar, add_comm, sub_sub, sub_sub, add_comm (f x) (f y)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
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
⊢ polar f x y = polar f y x
have rw₂ : f (y + x) - f x - f y = f (y + x) - f y - f x
Tactic: rw [polar, polar, add_comm, sub_sub, sub_sub, add_comm (f x) (f y)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
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
⊢ polar f x y = polar f y x
have rw₃ : f (y + x) - (f x + f y) = f (y + x) - f y - f x
Tactic: rw [polar, polar, add_comm, sub_sub, sub_sub, add_comm (f x) (f y)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
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
⊢ polar f x y = polar f y x
have rw₄ : f (y + x) - (f x + f y) = f (y + x) - (f y + f x)
Tactic: rw [polar, polar, add_comm, sub_sub, sub_sub, add_comm (f x) (f y)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
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)
⊢ polar f x y = polar f y x
have rw₅ : f (y + x) - (f y + f x) = f (y + x) - (f y + f x)
Tactic: rw [polar, polar, add_comm, sub_sub, sub_sub, add_comm (f x) (f y)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
f : M → N
x x' y : M
⊢ 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)
have 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)
Tactic: simp only [← add_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
f : M → N
x x' y : M
⊢ 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)
have 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)
Tactic: simp only [polar, sub_eq_iff_eq_add, eq_sub_iff_add_eq, sub_add_eq_add_sub, add_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
f : M → N
x x' y : M
⊢ 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)
have 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)
Tactic: simp only [add_right_comm _ (f y) _, add_right_comm _ (f x') (f x)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
f : M → N
x x' y : M
⊢ 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)
have 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)
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]