awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
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₁)
a :
  ∀ (x x_1 : M₂),
    Eq.{uN₁ + 1} (α := N₁)
      ((((AlgebraTensorModule.curry
                    ((((AlgebraTensorModule.curry (Q₁.polarBilin (R := A) (M := A ⊗[R] M₂) (N := N₁)) :
                              A →ₗ[A] M₂ →ₗ[R] A ⊗[R] M₂ →ₗ[A] N₁) :
                            (a : A) → M₂ →ₗ[R] A ⊗[R] M₂ →ₗ[A] N₁)
                          1 :
                        (a : M₂) → A ⊗[R] M₂ →ₗ[A] N₁)
                      x) :
                  A →ₗ[A] M₂ →ₗ[R] N₁) :
                (a : A) → M₂ →ₗ[R] N₁)
              1 :
            (a : M₂) → N₁)
          x_1 :
        N₁)
      ((((AlgebraTensorModule.curry
                    ((((AlgebraTensorModule.curry (Q₂.polarBilin (R := A) (M := A ⊗[R] M₂) (N := N₁)) :
                              A →ₗ[A] M₂ →ₗ[R] A ⊗[R] M₂ →ₗ[A] N₁) :
                            (a : A) → M₂ →ₗ[R] A ⊗[R] M₂ →ₗ[A] N₁)
                          1 :
                        (a : M₂) → A ⊗[R] M₂ →ₗ[A] N₁)
                      x) :
                  A →ₗ[A] M₂ →ₗ[R] N₁) :
                (a : A) → M₂ →ₗ[R] N₁)
              1 :
            (a : M₂) → N₁)
          x_1 :
        N₁)
⊢ 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:
ext
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
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₁) (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₁)
⊢ Eq.{uN₁ + 1} (α := N₁)
    ((((AlgebraTensorModule.curry
                  ((((AlgebraTensorModule.curry (Q₁.polarBilin (R := A) (M := A ⊗[R] M₂) (N := N₁)) :
                            A →ₗ[A] M₂ →ₗ[R] A ⊗[R] M₂ →ₗ[A] N₁) :
                          (a : A) → M₂ →ₗ[R] A ⊗[R] M₂ →ₗ[A] N₁)
                        1 :
                      (a : M₂) → A ⊗[R] M₂ →ₗ[A] N₁)
                    x_1) :
                A →ₗ[A] M₂ →ₗ[R] N₁) :
              (a : A) → M₂ →ₗ[R] N₁)
            1 :
          (a : M₂) → N₁)
        x_2 :
      N₁)
    ((((AlgebraTensorModule.curry
                  ((((AlgebraTensorModule.curry (Q₂.polarBilin (R := A) (M := A ⊗[R] M₂) (N := N₁)) :
                            A →ₗ[A] M₂ →ₗ[R] A ⊗[R] M₂ →ₗ[A] N₁) :
                          (a : A) → M₂ →ₗ[R] A ⊗[R] M₂ →ₗ[A] N₁)
                        1 :
                      (a : M₂) → A ⊗[R] M₂ →ₗ[A] N₁)
                    x_1) :
                A →ₗ[A] M₂ →ₗ[R] N₁) :
              (a : A) → M₂ →ₗ[R] N₁)
            1 :
          (a : M₂) → N₁)
        x_2 :
      N₁)

Tactic:
dsimp [polar]

Premises used: QuadraticMap.polar
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
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 (α := 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]
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
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₁.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)
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
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₁)
⊢ 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:
module
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
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₁)
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
⊢ Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) (x + y) : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) (x + y) : N₁)

Tactic:
linear_combination (norm := module) this + hx + hy
-- Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
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₁)
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₁)
⊢ Eq.{uN₁ + 1} (α := N₁) ((Q₁ : (a : A ⊗[R] M₂) → N₁) x : N₁) ((Q₂ : (a : A ⊗[R] M₂) → N₁) x : 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

Premises used: QuadraticMap.polar, TensorProduct.tmul
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_3
inst_3 : Ring S
inst_4 : SMul S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
P : Submodule R M
x : M
⊢ Eq (α := M ⧸ P) ((restrictScalarsEquiv S P : (a : M ⧸ restrictScalars S P) → M ⧸ P) (mk x) : M ⧸ P) (mk x : M ⧸ P)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, Submodule.restrictScalars, Quot.map, rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Type u_3
inst_3 : Ring S
inst_4 : SMul S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
P : Submodule R M
x : M
⊢ Eq (α := HasQuotient.Quotient M (B := Submodule S M) (restrictScalars S P))
    ((LinearEquiv.symm (restrictScalarsEquiv S P) : (a : M ⧸ P) → M ⧸ restrictScalars S P) (mk x) :
      HasQuotient.Quotient M (B := Submodule S M) (restrictScalars S P))
    (mk x : HasQuotient.Quotient M (B := Submodule S M) (restrictScalars S P))

Tactic:
rfl

Premises used: Submodule.Quotient.mk, Quot.map, rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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.toAddSubgroup ≠ ⊤ ↔ p ≠ ⊤

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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.toAddSubgroup = ⊤ ↔ p = ⊤

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
inst_3 : Subsingleton M
⊢ Subsingleton.{u_2 + 1} (M ⧸ p)

Tactic:
simpa using Subsingleton.elim ..

Premises used: Subsingleton.elim
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
inst_3 : Infinite M
⊢ Infinite.{u_2 + 1} (HasQuotient.Quotient M (B := Submodule R M) ⊥)

Tactic:
Infinite.of_injective Submodule.Quotient.mk fun _x _y h =>
    sub_eq_zero.mp <| (Submodule.Quotient.eq ⊥).mp h

Premises used: Submodule.Quotient.eq, Infinite.of_injective, sub_eq_zero, Submodule.Quotient.mk, Bot.bot, Iff.mp
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Nonempty.{max 1 (u_2 + 1)} (Unique (HasQuotient.Quotient M (B := Submodule R M) ⊤))

Tactic:
⟨QuotientTop.unique⟩

Premises used: Submodule.QuotientTop.unique, Nonempty.intro
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Nonempty.{max 1 (u_2 + 1)} (Unique (HasQuotient.Quotient M (B := Submodule R M) ⊤))

Tactic:
exact ⟨QuotientTop.unique⟩
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
⊢ StrictMono (β := Submodule R ↥p × Submodule R (M ⧸ p)) fun (m : Submodule R M) ↦ (comap p.subtype m, map p.mkQ m)

Tactic:
fun m₁ m₂ ↦ QuotientAddGroup.strictMono_comap_prod_map
    p.toAddSubgroup (a := m₁.toAddSubgroup) (b := m₂.toAddSubgroup)

Premises used: StrictMono, Set.Mem, Submodule.Quotient.mk, QuotientAddGroup.strictMono_comap_prod_map, Submodule.toAddSubgroup, Submodule.quotientRel
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
a : R
x_2 : M ⧸ p
x : M
⊢ ZeroHom.toFun (↑(lift p.toAddSubgroup f.toAddMonoidHom h) : ZeroHom (M ⧸ p.toAddSubgroup) M₂)
      (HSMul.hSMul (β := M ⧸ p) a (Quot.mk (⇑p.quotientRel : M → M → Prop) x)) =
    HSMul.hSMul.{u_3, u_4, u_4} (α := R₂) ((τ₁₂ : (a : R) → R₂) a : R₂)
      (ZeroHom.toFun (↑(lift p.toAddSubgroup f.toAddMonoidHom h) : ZeroHom (M ⧸ p.toAddSubgroup) M₂)
        (Quot.mk (⇑p.quotientRel : M → M → Prop) x))

Tactic:
f.map_smulₛₗ a x

Premises used: Quotient.liftOn', AddCon.liftOn, LinearMap.map_smulₛₗ
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
a : R
x_2 : M ⧸ p
x : M
⊢ ZeroHom.toFun (↑(lift p.toAddSubgroup f.toAddMonoidHom h) : ZeroHom (M ⧸ p.toAddSubgroup) M₂)
      (HSMul.hSMul (β := M ⧸ p) a (Quot.mk (⇑p.quotientRel : M → M → Prop) x)) =
    HSMul.hSMul.{u_3, u_4, u_4} (α := R₂) ((τ₁₂ : (a : R) → R₂) a : R₂)
      (ZeroHom.toFun (↑(lift p.toAddSubgroup f.toAddMonoidHom h) : ZeroHom (M ⧸ p.toAddSubgroup) M₂)
        (Quot.mk (⇑p.quotientRel : M → M → Prop) x))

Tactic:
exact f.map_smulₛₗ a x

Premises used: LinearMap.map_smulₛₗ
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
x : M
⊢ Eq.{u_4 + 1} (α := M₂) ((p.liftQ f h : (a : M ⧸ p) → M₂) (Quotient.mk x) : M₂) ((f : (a : M) → M₂) x : M₂)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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₁ : ∀ (x : M), Eq.{u_4 + 1} (α := M₂) ((p.liftQ f h ∘ₛₗ p.mkQ : (a : M) → M₂) x : M₂) ((f : (a : M) → M₂) x : M₂)
⊢ p.liftQ f h ∘ₛₗ p.mkQ = f

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
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:
rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
h₁ :
  ∀ (x : M) (i : ι),
    Eq.{u_6 + 1} (α := N i)
      ((((LinearMap.pi (φ := N) fun (i : ι) ↦ p.liftQ (f i) ⋯) ∘ₗ 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) ⋯ ∘ₗ p.mkQ :
              M →ₗ[R] (i : ι) → N i) :
            (a : M) → (i : ι) → N i)
          x i :
        N i)
⊢ 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) ⋯)

Tactic:
ext x i
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
x : M
i : ι
⊢ Eq.{u_6 + 1} (α := N i)
    ((((LinearMap.pi (φ := N) fun (i : ι) ↦ p.liftQ (f i) ⋯) ∘ₗ 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) ⋯ ∘ₗ p.mkQ :
            M →ₗ[R] (i : ι) → N i) :
          (a : M) → (i : ι) → N i)
        x i :
      N i)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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₂)
rw₂ rw₃ : Eq.{u_4 + 1} (α := M₂) 0 0
⊢ R ∙ x ≤ f.ker

Tactic:
rw [span_singleton_le_iff_mem, LinearMap.mem_ker, h]

Premises used: LinearMap.mem_ker, Submodule.span_singleton_le_iff_mem
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module 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₂)
y : M
⊢ Eq.{u_4 + 1} (α := M₂) ((liftQSpanSingleton x f h : (a : M ⧸ R ∙ x) → M₂) (Quotient.mk y) : M₂)
    ((f : (a : M) → M₂) y : M₂)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
x_1 : M ⧸ p
x : M
⊢ Quot.mk (⇑p.quotientRel : M → M → Prop) x ∈ p.mkQ.range

Tactic:
⟨x, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
x_1 : M ⧸ p
x : M
⊢ Quot.mk (⇑p.quotientRel : M → M → Prop) x ∈ p.mkQ.range

Tactic:
exact ⟨x, rfl⟩
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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 : ∀ (x : M), x ∈ p.mkQ.ker ↔ x ∈ p
⊢ p.mkQ.ker = p

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
x : M
⊢ x ∈ p.mkQ.ker ↔ x ∈ p

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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' : Submodule R (M ⧸ p)
⊢ p ≤ comap p.mkQ p'

Tactic:
simpa using (comap_mono bot_le : ker p.mkQ ≤ comap p.mkQ p')

Premises used: Submodule.comap_mono, bot_le
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
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
rw₃ rw₄ : p ≤ p
⊢ map p.mkQ p = ⊥

Tactic:
rw [eq_bot_iff, map_le_iff_le_comap, comap_bot, ker_mkQ]

Premises used: Submodule.ker_mkQ, Submodule.map_le_iff_le_comap, eq_bot_iff, Submodule.comap_bot
-- Module: Mathlib.LinearAlgebra.Quotient.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' : Submodule R M
⊢ comap p.mkQ (map p.mkQ p') = p ⊔ p'

Tactic:
simp [comap_map_eq, sup_comm]

Premises used: sup_comm, Submodule.comap_map_eq