awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct (goal)
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N₁
inst_4 : Algebra R A
inst_5 : Module R N₁
inst_6 : Module A N₁
inst_7 : IsScalarTower R A N₁
inst_8 : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h :
  ∀ (a : A) (m : M₂),
    Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁)
x y : A ⊗[R] M₂
hx : Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) x : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) x : N₁)
hy : Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) y : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) y : N₁)
x_1 x_2 : M₂
a :
  HSub.hSub (β := N₁)
      (HSub.hSub (α := N₁) (β := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] (x_1 + x_2)) : N₁)
        ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
      ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁) =
    HSub.hSub (β := N₁)
      (HSub.hSub (α := N₁) (β := N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] (x_1 + x_2)) : N₁)
        ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
      ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁)
⊢ HSub.hSub (β := N₁)
      (HSub.hSub (α := N₁) (β := N₁)
        ((Q₁ : (a : A ⊗[R] M₂) → N₁) (HAdd.hAdd (α := A ⊗[R] M₂) (1 ⊗ₜ[R] x_1) (1 ⊗ₜ[R] x_2)) : N₁)
        ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
      ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁) =
    HSub.hSub (β := N₁)
      (HSub.hSub (α := N₁) (β := N₁)
        ((Q₂ : (a : A ⊗[R] M₂) → N₁) (HAdd.hAdd (α := A ⊗[R] M₂) (1 ⊗ₜ[R] x_1) (1 ⊗ₜ[R] x_2)) : N₁)
        ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
      ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁)
have a₁ : HSub.hSub (β := N₁)
    (HSub.hSub (α := N₁) (β := N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] (x_1 + x_2)) : N₁)
      ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
    ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁) =
  HSub.hSub (β := N₁)
    (HSub.hSub (α := N₁) (β := N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] (x_1 + x_2)) : N₁)
      ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
    ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁)
Tactic: rw [← TensorProduct.tmul_add, h, h, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct (goal)
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N₁
inst_4 : Algebra R A
inst_5 : Module R N₁
inst_6 : Module A N₁
inst_7 : IsScalarTower R A N₁
inst_8 : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h :
  ∀ (a : A) (m : M₂),
    Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁)
x y : A ⊗[R] M₂
hx : Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) x : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) x : N₁)
hy : Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) y : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) y : N₁)
x_1 x_2 : M₂
a :
  HSub.hSub (β := N₁)
      (HSub.hSub (α := N₁) (β := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] (x_1 + x_2)) : N₁)
        ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
      ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁) =
    HSub.hSub (β := N₁)
      (HSub.hSub (α := N₁) (β := N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] (x_1 + x_2)) : N₁)
        ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
      ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁)
a₁ :
  HSub.hSub (β := N₁)
      (HSub.hSub (α := N₁) (β := N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] (x_1 + x_2)) : N₁)
        ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
      ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁) =
    HSub.hSub (β := N₁)
      (HSub.hSub (α := N₁) (β := N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] (x_1 + x_2)) : N₁)
        ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
      ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁)
⊢ HSub.hSub (β := N₁)
      (HSub.hSub (α := N₁) (β := N₁)
        ((Q₁ : (a : A ⊗[R] M₂) → N₁) (HAdd.hAdd (α := A ⊗[R] M₂) (1 ⊗ₜ[R] x_1) (1 ⊗ₜ[R] x_2)) : N₁)
        ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
      ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁) =
    HSub.hSub (β := N₁)
      (HSub.hSub (α := N₁) (β := N₁)
        ((Q₂ : (a : A ⊗[R] M₂) → N₁) (HAdd.hAdd (α := A ⊗[R] M₂) (1 ⊗ₜ[R] x_1) (1 ⊗ₜ[R] x_2)) : N₁)
        ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
      ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁)
have a₂ : HSub.hSub (β := N₁)
    (HSub.hSub (α := N₁) (β := N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] (x_1 + x_2)) : N₁)
      ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
    ((Q₁ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁) =
  HSub.hSub (β := N₁)
    (HSub.hSub (α := N₁) (β := N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] (x_1 + x_2)) : N₁)
      ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_1) : N₁))
    ((Q₂ : (a : A ⊗[R] M₂) → N₁) (1 ⊗ₜ[R] x_2) : N₁)
Tactic: rw [← TensorProduct.tmul_add, h, h, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct (hypothesis)
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N₁
inst_4 : Algebra R A
inst_5 : Module R N₁
inst_6 : Module A N₁
inst_7 : IsScalarTower R A N₁
inst_8 : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h :
  ∀ (a : A) (m : M₂),
    Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁)
x y : A ⊗[R] M₂
hx : Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) x : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) x : N₁)
hy : Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) y : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) y : N₁)
⊢ Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (x + y) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (x + y) : N₁)
have this : Eq (α := BilinMap A (A ⊗[R] M₂) N₁) (Q₁.polarBilin (R := A) (M := A ⊗[R] M₂) (N := N₁) : BilinMap A (A ⊗[R] M₂) N₁)
  (Q₂.polarBilin (R := A) (M := A ⊗[R] M₂) (N := N₁) : BilinMap A (A ⊗[R] M₂) N₁)
Tactic: have : Q₁.polarBilin = Q₂.polarBilin := by
      ext
      dsimp [polar]
      rw [← TensorProduct.tmul_add, h, h, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct (hypothesis)
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N₁
inst_4 : Algebra R A
inst_5 : Module R N₁
inst_6 : Module A N₁
inst_7 : IsScalarTower R A N₁
inst_8 : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h :
  ∀ (a : A) (m : M₂),
    Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁)
x y : A ⊗[R] M₂
hx : Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) x : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) x : N₁)
hy : Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) y : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) y : N₁)
this :
  Eq (α := BilinMap A (A ⊗[R] M₂) N₁) (Q₁.polarBilin (R := A) (M := A ⊗[R] M₂) (N := N₁) : BilinMap A (A ⊗[R] M₂) N₁)
    (Q₂.polarBilin (R := A) (M := A ⊗[R] M₂) (N := N₁) : BilinMap A (A ⊗[R] M₂) N₁)
⊢ Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (x + y) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (x + y) : N₁)
have this₁ : Eq.{uN₁ + 1} (α := N₁)
  (((((Q₁.polarBilin (R := A) (M := A ⊗[R] M₂) (N := N₁) : BilinMap A (A ⊗[R] M₂) N₁) :
              (a : A ⊗[R] M₂) → A ⊗[R] M₂ →ₗ[A] N₁)
            x :
          A ⊗[R] M₂ →ₗ[A] N₁) :
        (a : A ⊗[R] M₂) → N₁)
      y :
    N₁)
  (((((Q₂.polarBilin (R := A) (M := A ⊗[R] M₂) (N := N₁) : BilinMap A (A ⊗[R] M₂) N₁) :
              (a : A ⊗[R] M₂) → A ⊗[R] M₂ →ₗ[A] N₁)
            x :
          A ⊗[R] M₂ →ₗ[A] N₁) :
        (a : A ⊗[R] M₂) → N₁)
      y :
    N₁)
Tactic: replace := congr($this x y)
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct (goal)
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N₁
inst_4 : Algebra R A
inst_5 : Module R N₁
inst_6 : Module A N₁
inst_7 : IsScalarTower R A N₁
inst_8 : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h :
  ∀ (a : A) (m : M₂),
    Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁)
x y : A ⊗[R] M₂
hx : Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) x : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) x : N₁)
hy : Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) y : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) y : N₁)
this :
  HSub.hSub (β := N₁)
      (HSub.hSub (α := N₁) (β := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (x + y) : N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) x : N₁))
      ((Q₁ : (a : A ⊗[R] M₂) → N₁) y : N₁) =
    HSub.hSub (β := N₁)
      (HSub.hSub (α := N₁) (β := N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (x + y) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) x : N₁))
      ((Q₂ : (a : A ⊗[R] M₂) → N₁) y : N₁)
⊢ Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (x + y) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (x + y) : N₁)
have a : HAdd.hAdd (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (x + y) : N₁)
      (HAdd.hAdd (β := N₁)
        (HAdd.hAdd (β := N₁)
          (HSub.hSub (β := N₁)
            (HSub.hSub (α := N₁) (β := N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (x + y) : N₁)
              ((Q₂ : (a : A ⊗[R] M₂) → N₁) x : N₁))
            ((Q₂ : (a : A ⊗[R] M₂) → N₁) y : N₁))
          ((Q₂ : (a : A ⊗[R] M₂) → N₁) x : N₁))
        ((Q₂ : (a : A ⊗[R] M₂) → N₁) y : N₁)) -
    HAdd.hAdd (α := N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (x + y) : N₁)
      (HAdd.hAdd (β := N₁)
        (HAdd.hAdd (β := N₁)
          (HSub.hSub (β := N₁)
            (HSub.hSub (α := N₁) (β := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (x + y) : N₁)
              ((Q₁ : (a : A ⊗[R] M₂) → N₁) x : N₁))
            ((Q₁ : (a : A ⊗[R] M₂) → N₁) y : N₁))
          ((Q₁ : (a : A ⊗[R] M₂) → N₁) x : N₁))
        ((Q₁ : (a : A ⊗[R] M₂) → N₁) y : N₁)) =
  0
Tactic: linear_combination (norm := module) this + hx + hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct (goal)
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N₁
inst_4 : Algebra R A
inst_5 : Module R N₁
inst_6 : Module A N₁
inst_7 : IsScalarTower R A N₁
inst_8 : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h :
  ∀ (a : A) (m : M₂),
    Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁)
x : A ⊗[R] M₂
H :
  ∀ (x : A) (y : M₂),
    Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (x ⊗ₜ[R] y) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (x ⊗ₜ[R] y) : N₁)
⊢ Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) x : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) x : N₁)
have H₁ : Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) 0 : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) 0 : N₁)
Tactic: induction x with
  | tmul => simp [h]
  | zero => simp
  | add x y hx hy =>
    have : Q₁.polarBilin = Q₂.polarBilin := by
      ext
      dsimp [polar]
      rw [← TensorProduct.tmul_add, h, h, h]
    replace := congr($this x y)
    dsimp [polar] at this
    linear_combination (norm := module) this + hx + hy
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.TensorProduct (goal)
Goal:
R : Type uR
A : Type uA
M₂ : Type uM₂
N₁ : Type uN₁
inst : CommRing R
inst_1 : CommRing A
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup N₁
inst_4 : Algebra R A
inst_5 : Module R N₁
inst_6 : Module A N₁
inst_7 : IsScalarTower R A N₁
inst_8 : Module R M₂
Q₁ Q₂ : QuadraticMap A (A ⊗[R] M₂) N₁
h :
  ∀ (a : A) (m : M₂),
    Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (a ⊗ₜ[R] m) : N₁)
x : A ⊗[R] M₂
H :
  ∀ (x : A) (y : M₂),
    Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (x ⊗ₜ[R] y) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (x ⊗ₜ[R] y) : N₁)
H₁ : Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) 0 : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) 0 : N₁)
⊢ Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) x : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) x : N₁)
have H₂ : ∀ (x y : A ⊗[R] M₂)
  (hx : Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) x : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) x : N₁))
  (hy : Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) y : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) y : N₁)),
  Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (x + y) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (x + y) : N₁)
Tactic: induction x with
  | tmul => simp [h]
  | zero => simp
  | add x y hx hy =>
    have : Q₁.polarBilin = Q₂.polarBilin := by
      ext
      dsimp [polar]
      rw [← TensorProduct.tmul_add, h, h, h]
    replace := congr($this x y)
    dsimp [polar] at this
    linear_combination (norm := module) this + hx + hy
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst_3 : Ring R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
⊢ p.liftQ f h ∘ₛₗ p.mkQ = f
have h₁ : ∀ (x : M), Eq.{u_4 + 1} (α := M₂) ((p.liftQ f h ∘ₛₗ p.mkQ : (a : M) → M₂) x : M₂) ((f : (a : M) → M₂) x : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
N : ι → Type u_6
inst_3 : (i : ι) → AddCommGroup (N i)
inst_4 : (i : ι) → Module.{u_1, u_6} R (N i)
f : (i : ι) → LinearMap.{u_1, u_1, u_2, u_6} (RingHom.id R) M (N i)
p : Submodule R M
h : ∀ (i : ι), p ≤ (f i).ker
⊢ Eq (α := M ⧸ p →ₗ[R] (i : ι) → N i) (LinearMap.pi (φ := N) fun (i : ι) ↦ p.liftQ (f i) ⋯)
    (p.liftQ (R₂ := R) (M₂ := (i : ι) → N i) (τ₁₂ := RingHom.id R) (LinearMap.pi (φ := N) f) ⋯)
have h₁ : ∀ (x : M) (i : ι),
  Eq.{u_6 + 1} (α := N i)
    ((((LinearMap.pi (φ := N) fun (i : ι) ↦ p.liftQ (f i) sorry) ∘ₗ p.mkQ : M →ₗ[R] (i : ι) → N i) :
          (a : M) → (i : ι) → N i)
        x i :
      N i)
    (((p.liftQ (R₂ := R) (M₂ := (i : ι) → N i) (τ₁₂ := RingHom.id R) (LinearMap.pi (φ := N) f) sorry ∘ₗ p.mkQ :
            M →ₗ[R] (i : ι) → N i) :
          (a : M) → (i : ι) → N i)
        x i :
      N i)
Tactic: ext x i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
r : R
x_1 y : M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' p'' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst_3 : Ring R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
x : M
f : M →ₛₗ[τ₁₂] M₂
h : Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) (0 : M₂)
⊢ R ∙ x ≤ f.ker
have rw : x ∈ f.ker
Tactic: rw [span_singleton_le_iff_mem, LinearMap.mem_ker, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
r : R
x_1 y : M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' p'' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst_3 : Ring R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
x : M
f : M →ₛₗ[τ₁₂] M₂
h : Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) (0 : M₂)
rw : x ∈ f.ker
rw₁ : Eq.{u_4 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂) (0 : M₂)
⊢ R ∙ x ≤ f.ker
have rw₂ : Eq.{u_4 + 1} (α := M₂) 0 0
Tactic: rw [span_singleton_le_iff_mem, LinearMap.mem_ker, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
⊢ p.mkQ.ker = p
have h : ∀ (x : M), x ∈ p.mkQ.ker ↔ x ∈ p
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
⊢ map p.mkQ p = ⊥
have rw : map p.mkQ p ≤ ⊥
Tactic: rw [eq_bot_iff, map_le_iff_le_comap, comap_bot, ker_mkQ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
rw : map p.mkQ p ≤ ⊥
⊢ map p.mkQ p = ⊥
have rw₁ : p ≤ comap p.mkQ ⊥
Tactic: rw [eq_bot_iff, map_le_iff_le_comap, comap_bot, ker_mkQ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
rw : map p.mkQ p ≤ ⊥
rw₁ : p ≤ comap p.mkQ ⊥
⊢ map p.mkQ p = ⊥
have rw₂ : p ≤ p.mkQ.ker
Tactic: rw [eq_bot_iff, map_le_iff_le_comap, comap_bot, ker_mkQ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
rw : map p.mkQ p ≤ ⊥
rw₁ : p ≤ comap p.mkQ ⊥
rw₂ : p ≤ p.mkQ.ker
⊢ map p.mkQ p = ⊥
have rw₃ : p ≤ p
Tactic: rw [eq_bot_iff, map_le_iff_le_comap, comap_bot, ker_mkQ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst_3 : Ring R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ comap f q
⊢ p.mapQ q f h ∘ₛₗ p.mkQ = q.mkQ ∘ₛₗ f
have h₁ : ∀ (x : M),
  Eq.{u_4 + 1} (α := M₂ ⧸ q) ((p.mapQ q f h ∘ₛₗ p.mkQ : (a : M) → M₂ ⧸ q) x : M₂ ⧸ q)
    ((q.mkQ ∘ₛₗ f : (a : M) → M₂ ⧸ q) x : M₂ ⧸ q)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst_3 : Ring R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
h : p ≤ comap (σ₁₂ := τ₁₂) 0 q
⊢ p.mapQ q 0 h = 0
have h₁ : ∀ (x : M),
  Eq.{u_4 + 1} (α := M₂ ⧸ q) ((p.mapQ q 0 h ∘ₛₗ p.mkQ : (a : M) → M₂ ⧸ q) x : M₂ ⧸ q)
    ((comp (σ₂₃ := τ₁₂) 0 p.mkQ : (a : M) → M₂ ⧸ q) x : M₂ ⧸ q)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst_3 : Ring R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
R₃ : Type u_5
M₃ : Type u_6
inst_6 : Ring R₃
inst_7 : AddCommGroup M₃
inst_8 : Module R₃ M₃
p₂ : Submodule R₂ M₂
p₃ : Submodule R₃ M₃
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
hf : p ≤ comap f p₂
hg : p₂ ≤ comap g p₃
h : p ≤ comap f (comap g p₃)
⊢ p.mapQ p₃ (g ∘ₛₗ f) h = p₂.mapQ p₃ g hg ∘ₛₗ p.mapQ p₂ f hf
have h₁ : ∀ (x : M),
  Eq.{u_6 + 1} (α := M₃ ⧸ p₃) ((p.mapQ p₃ (g ∘ₛₗ f) h ∘ₛₗ p.mkQ : (a : M) → M₃ ⧸ p₃) x : M₃ ⧸ p₃)
    (((p₂.mapQ p₃ g hg ∘ₛₗ p.mapQ p₂ f hf) ∘ₛₗ p.mkQ : (a : M) → M₃ ⧸ p₃) x : M₃ ⧸ p₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
r : R
x y : M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' p'' : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst_3 : Ring R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
⊢ p ≤ comap LinearMap.id p
have rw : p ≤ p
Tactic: rw [comap_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
h : p ≤ comap LinearMap.id p
⊢ p.mapQ p LinearMap.id h = LinearMap.id
have h₁ : ∀ (x : M),
  Eq (α := M ⧸ p) ((p.mapQ p LinearMap.id h ∘ₗ p.mkQ : (a : M) → M ⧸ p) x : M ⧸ p)
    ((LinearMap.id ∘ₗ p.mkQ : (a : M) → M ⧸ p) x : M ⧸ p)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : ∀ (h' : p ≤ comap (f ^ k) p), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
h' : p ≤ comap (f ^ (k + 1)) p
⊢ p.mapQ p (f ^ (k + 1)) h' = p.mapQ p f h ^ (k + 1)
have succ : p.mapQ p ((f ^ k) ∘ₗ f) sorry = (p.mapQ p f h ^ k) ∘ₗ p.mapQ p f h
Tactic: simp only [Module.End.iterate_succ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
ih : ∀ (h' : p ≤ comap (f ^ k) p), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
h' : p ≤ comap (f ^ (k + 1)) p
⊢ p.mapQ p ((f ^ k) ∘ₗ f) ⋯ = (p.mapQ p f h ^ k) ∘ₗ p.mapQ p f h
have succ : p ≤ comap (f ^ k) p
Tactic: rw [mapQ_comp, ih]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
h' : p ≤ comap (f ^ k) p
⊢ p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
have zero : ∀ (h' : p ≤ comap (HPow.hPow (β := ℕ) f 0) p),
  p.mapQ p (HPow.hPow (β := ℕ) f 0) h' = HPow.hPow (β := ℕ) (p.mapQ p f h) 0
Tactic: induction k with
  | zero => simp [Module.End.one_eq_id]
  | succ k ih =>
    simp only [Module.End.iterate_succ]
    rw [mapQ_comp, ih]
    exact p.le_comap_pow_of_le_comap h k
Cleared hypotheses: k, h'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
h' : p ≤ comap (f ^ k) p
zero :
  ∀ (h' : p ≤ comap (HPow.hPow (β := ℕ) f 0) p),
    p.mapQ p (HPow.hPow (β := ℕ) f 0) h' = HPow.hPow (β := ℕ) (p.mapQ p f h) 0
⊢ p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k
have succ : ∀ (k : ℕ) (ih : ∀ (h' : p ≤ comap (f ^ k) p), p.mapQ p (f ^ k) h' = p.mapQ p f h ^ k) (h' : p ≤ comap (f ^ (k + 1)) p),
  p.mapQ p (f ^ (k + 1)) h' = p.mapQ p f h ^ (k + 1)
Tactic: induction k with
  | zero => simp [Module.End.one_eq_id]
  | succ k ih =>
    simp only [Module.End.iterate_succ]
    rw [mapQ_comp, ih]
    exact p.le_comap_pow_of_le_comap h k
Cleared hypotheses: k, h'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst_3 : Ring R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
⊢ map p.mkQ (comap f q) ≤ comap (p.liftQ f h) q
have rw : comap f q ≤ comap p.mkQ (comap (p.liftQ f h) q)
Tactic: rw [map_le_iff_le_comap, ← comap_comp, liftQ_mkQ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst_3 : Ring R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
rw : comap f q ≤ comap p.mkQ (comap (p.liftQ f h) q)
⊢ map p.mkQ (comap f q) ≤ comap (p.liftQ f h) q
have rw₁ : comap f q ≤ comap (p.liftQ f h ∘ₛₗ p.mkQ) q
Tactic: rw [map_le_iff_le_comap, ← comap_comp, liftQ_mkQ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst_3 : Ring R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
rw : comap f q ≤ comap p.mkQ (comap (p.liftQ f h) q)
rw₁ : comap f q ≤ comap (p.liftQ f h ∘ₛₗ p.mkQ) q
⊢ map p.mkQ (comap f q) ≤ comap (p.liftQ f h) q
have rw₂ : comap f q ≤ comap f q
Tactic: rw [map_le_iff_le_comap, ← comap_comp, liftQ_mkQ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst_3 : Ring R₂
inst_4 : AddCommGroup M₂
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
h' : f.ker ≤ p
⊢ (p.liftQ f h).ker = ⊥
have rw : map p.mkQ f.ker = ⊥
Tactic: rw [ker_liftQ, le_antisymm h h', mkQ_map_self]