awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
X : QuadraticModuleCat R
⊢ ModuleCat.ofHom
      (Isometry.toLinearMap (N := R) (Q₁ :=
        (MonoidalCategoryStruct.tensorObj (𝒞 := category) ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category)) X).form) (Q₂ :=
        X.form) (Hom.toIsometry (Iso.hom (λ_ X)))) =
    𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
          (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))) X.toModuleCat) ≫
      𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
            (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))) X.toModuleCat) ≫
        Iso.hom (λ_ X.toModuleCat)
have simp : Eq (α :=
  MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
      (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))) X.toModuleCat ⟶
    X.toModuleCat)
  (ModuleCat.ofHom
      (Isometry.toLinearMap (N := R) (Q₁ :=
        (MonoidalCategoryStruct.tensorObj (𝒞 := category) ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category)) X).form) (Q₂ :=
        X.form) (Hom.toIsometry (Iso.hom (λ_ X)))) :
    Quiver.Hom (V := ModuleCat R)
      (ModuleCat.of R
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
              (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))) X.toModuleCat) :
          Type u))
      (ModuleCat.of R (↑X.toModuleCat : Type u)))
  (Iso.hom (λ_ X.toModuleCat) :
    MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
        ((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)) X.toModuleCat ⟶
      X.toModuleCat)
Tactic: simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
X : QuadraticModuleCat R
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat R)
      (ModuleCat.of R
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := category) X
                ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))).toModuleCat :
          Type u))
      (ModuleCat.of R (↑X.toModuleCat : Type u)))
    (ModuleCat.ofHom (Isometry.toLinearMap (Hom.toIsometry (Iso.hom (ρ_ X)))))
    (𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) (ModuleCat.of R (↑X.toModuleCat : Type u))
          (ModuleCat.of R (↑(toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))) : Type u))) ≫
      ModuleCat.of R (↑X.toModuleCat : Type u) ◁ 𝟙 ((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)) ≫
        Iso.hom (ρ_ (ModuleCat.of R (↑X.toModuleCat : Type u))))
have dsimp : ModuleCat.ofHom
    (Isometry.toLinearMap (N := R) (Q₁ :=
      (MonoidalCategoryStruct.tensorObj (𝒞 := category) X ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))).form) (Q₂ :=
      X.form) (Hom.toIsometry (Iso.hom (ρ_ X)))) =
  𝟙
      (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
        (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category)))) ≫
    X.toModuleCat ◁ 𝟙 ((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)) ≫ Iso.hom (ρ_ X.toModuleCat)
Tactic: dsimp only [toModuleCat_tensor, ModuleCat.of_coe]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
X : QuadraticModuleCat R
⊢ ModuleCat.ofHom
      (Isometry.toLinearMap (N := R) (Q₁ :=
        (MonoidalCategoryStruct.tensorObj (𝒞 := category) X ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))).form) (Q₂ :=
        X.form) (Hom.toIsometry (Iso.hom (ρ_ X)))) =
    𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
          (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category)))) ≫
      X.toModuleCat ◁ 𝟙 ((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)) ≫ Iso.hom (ρ_ X.toModuleCat)
have erw : ModuleCat.ofHom
    (Isometry.toLinearMap (N := R) (Q₁ :=
      (MonoidalCategoryStruct.tensorObj (𝒞 := category) X ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))).form) (Q₂ :=
      X.form) (Hom.toIsometry (Iso.hom (ρ_ X)))) =
  𝟙
      (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
        (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category)))) ≫
    𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
          (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category)))) ≫
      Iso.hom (ρ_ X.toModuleCat)
Tactic: erw [MonoidalCategory.whiskerLeft_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Invertible (α := R) 2
X : QuadraticModuleCat R
⊢ ModuleCat.ofHom
      (Isometry.toLinearMap (N := R) (Q₁ :=
        (MonoidalCategoryStruct.tensorObj (𝒞 := category) X ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))).form) (Q₂ :=
        X.form) (Hom.toIsometry (Iso.hom (ρ_ X)))) =
    𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
          (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category)))) ≫
      𝟙
          (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
            (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category)))) ≫
        Iso.hom (ρ_ X.toModuleCat)
have simp : Eq (α :=
  MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
      (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))) ⟶
    X.toModuleCat)
  (ModuleCat.ofHom
      (Isometry.toLinearMap (N := R) (Q₁ :=
        (MonoidalCategoryStruct.tensorObj (𝒞 := category) X ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category))).form) (Q₂ :=
        X.form) (Hom.toIsometry (Iso.hom (ρ_ X)))) :
    Quiver.Hom (V := ModuleCat R)
      (ModuleCat.of R
        (↑(MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
              (toModuleCat ((𝟙_ (QuadraticModuleCat R)) (𝒞 := category)))) :
          Type u))
      (ModuleCat.of R (↑X.toModuleCat : Type u)))
  (Iso.hom (ρ_ X.toModuleCat) :
    MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R) X.toModuleCat
        ((𝟙_ (ModuleCat R)) (𝒞 := ModuleCat.moduleCategory R)) ⟶
      X.toModuleCat)
Tactic: simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat (goal)
Goal:
R : Type u
inst : CommRing R
X Y Z : QuadraticModuleCat.{v, u} R
i : X ≅ Y
x : (↑X.toModuleCat : Type v)
⊢ (QuadraticModuleCat.Hom.toIsometry i.inv : (a : (↑Y.toModuleCat : Type v)) → (↑X.toModuleCat : Type v))
      ((QuadraticModuleCat.Hom.toIsometry i.hom : (a : (↑X.toModuleCat : Type v)) → (↑Y.toModuleCat : Type v)) x :
        (↑Y.toModuleCat : Type v)) =
    x
have change : (QuadraticModuleCat.Hom.toIsometry (i.hom ≫ i.inv) : (a : (↑X.toModuleCat : Type v)) → (↑X.toModuleCat : Type v)) x = x
Tactic: change (i.hom ≫ i.inv).toIsometry x = x
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat (goal)
Goal:
R : Type u
inst : CommRing R
X Y Z : QuadraticModuleCat.{v, u} R
i : X ≅ Y
x : (↑Y.toModuleCat : Type v)
⊢ (QuadraticModuleCat.Hom.toIsometry i.hom : (a : (↑X.toModuleCat : Type v)) → (↑Y.toModuleCat : Type v))
      ((QuadraticModuleCat.Hom.toIsometry i.inv : (a : (↑Y.toModuleCat : Type v)) → (↑X.toModuleCat : Type v)) x :
        (↑X.toModuleCat : Type v)) =
    x
have change : (QuadraticModuleCat.Hom.toIsometry (i.inv ≫ i.hom) : (a : (↑Y.toModuleCat : Type v)) → (↑Y.toModuleCat : Type v)) x = x
Tactic: change (i.inv ≫ i.hom).toIsometry x = x
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : AddCommGroup P
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R P
Q : QuadraticMap R M P
x y : M
hx :
  Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    x
hy :
  Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    y
⊢ Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    (x + y)
have refine : Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) (x + y) : P) (0 : P)
Tactic: refine ⟨?_, by simp [hx.2, hy.2]⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (hypothesis)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : AddCommGroup P
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R P
Q : QuadraticMap R M P
x y : M
hx :
  Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    x
hy :
  Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    y
⊢ Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) (x + y) : P) (0 : P)
have this : Eq.{u_4 + 1} (α := P) ((fun (x : M →ₗ[R] P) ↦ ((x : (a : M) → P) y : P)) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x))
  ((fun (x : M →ₗ[R] P) ↦ ((x : (a : M) → P) y : P)) 0)
Tactic: have := congr_arg (· y) hx.2
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (hypothesis)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : AddCommGroup P
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R P
Q : QuadraticMap R M P
x y : M
hx :
  Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    x
hy :
  Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    y
this :
  Eq.{u_4 + 1} (α := P) ((fun (x : M →ₗ[R] P) ↦ ((x : (a : M) → P) y : P)) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x))
    ((fun (x : M →ₗ[R] P) ↦ ((x : (a : M) → P) y : P)) 0)
⊢ Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) (x + y) : P) (0 : P)
have this₁ : (Q : (a : M) → P) (x + y) = HAdd.hAdd (α := P) (β := P) ((Q : (a : M) → P) x : P) ((Q : (a : M) → P) y : P)
Tactic: simp only [QuadraticMap.polarBilin_apply_apply, QuadraticMap.polar,
      LinearMap.zero_apply, sub_sub, sub_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : AddCommGroup P
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R P
Q : QuadraticMap R M P
x y : M
hx :
  Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    x
hy :
  Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    y
this : (Q : (a : M) → P) (x + y) = HAdd.hAdd (α := P) (β := P) ((Q : (a : M) → P) x : P) ((Q : (a : M) → P) y : P)
⊢ Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) (x + y) : P) (0 : P)
have rw : HAdd.hAdd (α := P) (β := P) ((Q : (a : M) → P) x : P) ((Q : (a : M) → P) y : P) = 0
Tactic: rw [this, hx.1, hy.1, zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : AddCommGroup P
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R P
Q : QuadraticMap R M P
x y : M
hx :
  Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    x
hy :
  Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    y
this : (Q : (a : M) → P) (x + y) = HAdd.hAdd (α := P) (β := P) ((Q : (a : M) → P) x : P) ((Q : (a : M) → P) y : P)
rw : HAdd.hAdd (α := P) (β := P) ((Q : (a : M) → P) x : P) ((Q : (a : M) → P) y : P) = 0
⊢ Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) (x + y) : P) (0 : P)
have rw₁ : HAdd.hAdd (α := P) (β := P) (0 : P) ((Q : (a : M) → P) y : P) = 0
Tactic: rw [this, hx.1, hy.1, zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : AddCommGroup P
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R P
Q : QuadraticMap R M P
x y : M
hx :
  Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    x
hy :
  Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    y
this : (Q : (a : M) → P) (x + y) = HAdd.hAdd (α := P) (β := P) ((Q : (a : M) → P) x : P) ((Q : (a : M) → P) y : P)
rw : HAdd.hAdd (α := P) (β := P) ((Q : (a : M) → P) x : P) ((Q : (a : M) → P) y : P) = 0
rw₁ : HAdd.hAdd (α := P) (β := P) (0 : P) ((Q : (a : M) → P) y : P) = 0
⊢ Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) (x + y) : P) (0 : P)
have rw₂ : HAdd.hAdd (α := P) 0 0 = 0
Tactic: rw [this, hx.1, hy.1, zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : AddCommGroup P
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R P
Q : QuadraticMap R M P
x y : M
hx :
  Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    x
hy :
  Membership.mem (γ := Set M)
    {x : M |
      Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) x : P) (0 : P) ∧
        Eq (α := M →ₗ[R] P) ((Q.polarBilin : (a : M) → M →ₗ[R] P) x : M →ₗ[R] P) (0 : M →ₗ[R] P)}
    y
this : (Q : (a : M) → P) (x + y) = HAdd.hAdd (α := P) (β := P) ((Q : (a : M) → P) x : P) ((Q : (a : M) → P) y : P)
rw : HAdd.hAdd (α := P) (β := P) ((Q : (a : M) → P) x : P) ((Q : (a : M) → P) y : P) = 0
rw₁ : HAdd.hAdd (α := P) (β := P) (0 : P) ((Q : (a : M) → P) y : P) = 0
rw₂ : HAdd.hAdd (α := P) 0 0 = 0
⊢ Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) (x + y) : P) (0 : P)
have rw₃ : Eq.{u_4 + 1} (α := P) 0 0
Tactic: rw [this, hx.1, hy.1, zero_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : AddCommGroup P
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R P
Q : QuadraticMap R M P
Q' : QuadraticMap R M' P
e : Q.IsometryEquiv Q'
⊢ Submodule.map (↑e.toLinearEquiv : M →ₗ[R] M') Q.radical = Q'.radical
have h : ∀ (x : M'), x ∈ Submodule.map (↑e.toLinearEquiv : M →ₗ[R] M') Q.radical ↔ x ∈ Q'.radical
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : AddCommGroup P
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R P
Q : QuadraticMap R M P
Q' : QuadraticMap R M' P
h : Q.Equivalent Q'
⊢ Module.finrank.{u_1, u_2} R ↥Q.radical = Module.finrank.{u_1, u_3} R ↥Q'.radical
have obtain : ∀ (e : Q.IsometryEquiv Q'), Module.finrank.{u_1, u_2} R ↥Q.radical = Module.finrank.{u_1, u_3} R ↥Q'.radical
Tactic: obtain ⟨e⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : AddCommGroup P
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R P
Q : QuadraticMap R M P
Q' : QuadraticMap R M' P
e : Q.IsometryEquiv Q'
⊢ Module.finrank.{u_1, u_2} R ↥Q.radical = Module.finrank.{u_1, u_3} R ↥Q'.radical
have rw : Module.finrank.{u_1, u_2} R ↥Q.radical =
  Module.finrank.{u_1, u_3} R ↥(Submodule.map (↑e.toLinearEquiv : M →ₗ[R] M') Q.radical)
Tactic: rw [← e.map_radical, LinearEquiv.finrank_map_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : AddCommGroup P
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R P
Q : QuadraticMap R M P
Q' : QuadraticMap R M' P
e : Q.IsometryEquiv Q'
rw :
  Module.finrank.{u_1, u_2} R ↥Q.radical =
    Module.finrank.{u_1, u_3} R ↥(Submodule.map (↑e.toLinearEquiv : M →ₗ[R] M') Q.radical)
⊢ Module.finrank.{u_1, u_2} R ↥Q.radical = Module.finrank.{u_1, u_3} R ↥Q'.radical
have rw₁ : Module.finrank.{u_1, u_2} R ↥Q.radical = Module.finrank.{u_1, u_2} R ↥Q.radical
Tactic: rw [← e.map_radical, LinearEquiv.finrank_map_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (hypothesis)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup P
inst_2 : CommRing R
inst_3 : Module R M
inst_4 : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
m m' : M
hmm' : (N.quotientRel : M → M → Prop) m m'
⊢ Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) ((Q : (a : M) → P) m' : P)
have hmm'₁ : m - m' ∈ N
Tactic: rw [Submodule.quotientRel_def] at hmm'
Cleared hypotheses: hmm'
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup P
inst_2 : CommRing R
inst_3 : Module R M
inst_4 : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
m m' : M
hmm' : m - m' ∈ N
⊢ Eq.{u_4 + 1} (α := P) ((Q : (a : M) → P) m : P) ((Q : (a : M) → P) m' : P)
have rw : HAdd.hAdd (α := P) (β := P) ((Q : (a : M) → P) m' : P)
    ((((Q.polarBilin : (a : M) → M →ₗ[R] P) (m - m') : M →ₗ[R] P) : (a : M) → P) m' : P) =
  (Q : (a : M) → P) m'
Tactic: rw [(by simp : m = m' + (m - m')), QuadraticMap.map_add Q m' (m - m'),
    (hN hmm').1, add_zero, polar_comm, ← polarBilin_apply_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : AddCommGroup P
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
⊢ QuadraticMap.{u_1, u_2, u_4} R (M ⧸ N) P
have refine : ∃ (B : LinearMap.BilinMap.{u_1, u_2, u_4} R (M ⧸ N) P),
  ∀ (x y : M ⧸ N),
    Quotient.lift (⇑Q : (a : M) → P) sorry (x + y) =
      HAdd.hAdd (β := P) (Quotient.lift (⇑Q : (a : M) → P) sorry x + Quotient.lift (⇑Q : (a : M) → P) sorry y)
        ((((B : (a : M ⧸ N) → M ⧸ N →ₗ[R] P) x : LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) (M ⧸ N) P) :
              (a : M ⧸ N) → P)
            y :
          P)
Tactic: refine QuadraticMap.mk (Quotient.lift Q <| by exact lift_aux hN)
    (fun a m ↦ m.inductionOn (Q.map_smul a)) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : AddCommGroup P
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
⊢ ∃ (B : LinearMap.BilinMap.{u_1, u_2, u_4} R (M ⧸ N) P),
    ∀ (x y : M ⧸ N),
      Quotient.lift (⇑Q : (a : M) → P) ⋯ (x + y) =
        HAdd.hAdd (β := P) (Quotient.lift (⇑Q : (a : M) → P) ⋯ x + Quotient.lift (⇑Q : (a : M) → P) ⋯ y)
          ((((B : (a : M ⧸ N) → M ⧸ N →ₗ[R] P) x : LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) (M ⧸ N) P) :
                (a : M ⧸ N) → P)
              y :
            P)
have h : ∀ (x y : M ⧸ N),
  Quotient.lift (⇑Q : (a : M) → P) sorry (x + y) =
    HAdd.hAdd (β := P) (Quotient.lift (⇑Q : (a : M) → P) sorry x + Quotient.lift (⇑Q : (a : M) → P) sorry y)
      (((((LinearMap.liftQ₂ N N Q.polarBilin sorry sorry :
                    M ⧸ N →ₗ[R] LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) (M ⧸ N) P) :
                  (a : M ⧸ N) → M ⧸ N →ₗ[R] P)
                x :
              LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) (M ⧸ N) P) :
            (a : M ⧸ N) → P)
          y :
        P)
Tactic: use Q.polarBilin.liftQ₂ N N (fun n hn ↦ (hN hn).2) (fun n hn ↦ ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Radical (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
P : Type u_4
inst : AddCommGroup M
inst_1 : AddCommGroup M'
inst_2 : AddCommGroup P
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R M'
inst_6 : Module R P
Q : QuadraticMap R M P
N : Submodule R M
hN : N ≤ Q.radical
h :
  ∀ (x y : M ⧸ N),
    Quotient.lift (⇑Q : (a : M) → P) ⋯ (x + y) =
      HAdd.hAdd (β := P) (Quotient.lift (⇑Q : (a : M) → P) ⋯ x + Quotient.lift (⇑Q : (a : M) → P) ⋯ y)
        (((((LinearMap.liftQ₂ N N Q.polarBilin ⋯ ⋯ :
                      M ⧸ N →ₗ[R] LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) (M ⧸ N) P) :
                    (a : M ⧸ N) → M ⧸ N →ₗ[R] P)
                  x :
                LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) (M ⧸ N) P) :
              (a : M ⧸ N) → P)
            y :
          P)
⊢ ∃ (B : LinearMap.BilinMap.{u_1, u_2, u_4} R (M ⧸ N) P),
    ∀ (x y : M ⧸ N),
      Quotient.lift (⇑Q : (a : M) → P) ⋯ (x + y) =
        HAdd.hAdd (β := P) (Quotient.lift (⇑Q : (a : M) → P) ⋯ x + Quotient.lift (⇑Q : (a : M) → P) ⋯ y)
          ((((B : (a : M ⧸ N) → M ⧸ N →ₗ[R] P) x : LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) (M ⧸ N) P) :
                (a : M ⧸ N) → P)
              y :
            P)
have w : ∀ (n : M) (hn : n ∈ N), n ∈ (LinearMap.flip Q.polarBilin).ker
Tactic: use Q.polarBilin.liftQ₂ N N (fun n hn ↦ (hN hn).2) (fun n hn ↦ ?_)