awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Bilinear (goal)
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst : Ring R
inst_1 : Ring R₂
inst_2 : Ring S
inst_3 : Ring S₂
inst_4 : AddCommGroup M
inst_5 : AddCommGroup N
inst_6 : AddCommGroup P
inst_7 : Module R M
inst_8 : Module S N
inst_9 : Module R₂ P
inst_10 : Module S₂ P
inst_11 : SMulCommClass R₂ S₂ P
ρ : R →+* R₂
σ : S →+* S₂
M' : Submodule R M
N' : Submodule S N
f : M →ₛₗ[ρ] N →ₛₗ[σ] P
hM' : M' ≤ f.ker
hN' : N' ≤ f.flip.ker
n : N
hn : n ∈ N'
⊢ n ∈ (M'.liftQ f hM').flip.ker
have simp_rw : Eq (α := LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P)
  (((M'.liftQ f hM').flip : (a : N) → M ⧸ M' →ₛₗ[ρ] P) n : LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P)
  (0 : LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P)
Tactic: simp_rw [LinearMap.mem_ker, LinearMap.ext_iff, LinearMap.flip_apply, Submodule.Quotient.forall,
      Submodule.liftQ_apply, ← f.flip_apply, show f.flip n = 0 from hN' hn, LinearMap.zero_apply,
      forall_true_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Bilinear (goal)
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst : Ring R
inst_1 : Ring R₂
inst_2 : Ring S
inst_3 : Ring S₂
inst_4 : AddCommGroup M
inst_5 : AddCommGroup N
inst_6 : AddCommGroup P
inst_7 : Module R M
inst_8 : Module S N
inst_9 : Module R₂ P
inst_10 : Module S₂ P
inst_11 : SMulCommClass R₂ S₂ P
ρ : R →+* R₂
σ : S →+* S₂
M' : Submodule R M
N' : Submodule S N
f : M →ₛₗ[ρ] N →ₛₗ[σ] P
hM' : M' ≤ f.ker
hN' : N' ≤ f.flip.ker
n : N
hn : n ∈ N'
simp_rw :
  Eq (α := LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P)
    (((M'.liftQ f hM').flip : (a : N) → M ⧸ M' →ₛₗ[ρ] P) n : LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P)
    (0 : LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P)
⊢ n ∈ (M'.liftQ f hM').flip.ker
have simp_rw₁ : ∀ (x : M ⧸ M'),
  Eq.{u_7 + 1} (α := P)
    (((((M'.liftQ f hM').flip : (a : N) → M ⧸ M' →ₛₗ[ρ] P) n : LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P) :
          (a : M ⧸ M') → P)
        x :
      P)
    ((0 : (a : M ⧸ M') → P) x : P)
Tactic: simp_rw [LinearMap.mem_ker, LinearMap.ext_iff, LinearMap.flip_apply, Submodule.Quotient.forall,
      Submodule.liftQ_apply, ← f.flip_apply, show f.flip n = 0 from hN' hn, LinearMap.zero_apply,
      forall_true_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Bilinear (goal)
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst : Ring R
inst_1 : Ring R₂
inst_2 : Ring S
inst_3 : Ring S₂
inst_4 : AddCommGroup M
inst_5 : AddCommGroup N
inst_6 : AddCommGroup P
inst_7 : Module R M
inst_8 : Module S N
inst_9 : Module R₂ P
inst_10 : Module S₂ P
inst_11 : SMulCommClass R₂ S₂ P
ρ : R →+* R₂
σ : S →+* S₂
M' : Submodule R M
N' : Submodule S N
f : M →ₛₗ[ρ] N →ₛₗ[σ] P
hM' : M' ≤ f.ker
hN' : N' ≤ f.flip.ker
n : N
hn : n ∈ N'
simp_rw :
  Eq (α := LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P)
    (((M'.liftQ f hM').flip : (a : N) → M ⧸ M' →ₛₗ[ρ] P) n : LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P)
    (0 : LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P)
simp_rw₁ :
  ∀ (x : M ⧸ M'),
    Eq.{u_7 + 1} (α := P)
      (((((M'.liftQ f hM').flip : (a : N) → M ⧸ M' →ₛₗ[ρ] P) n : LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P) :
            (a : M ⧸ M') → P)
          x :
        P)
      ((0 : (a : M ⧸ M') → P) x : P)
⊢ n ∈ (M'.liftQ f hM').flip.ker
have simp_rw₂ : ∀ (x : M ⧸ M'),
  Eq.{u_7 + 1} (α := P) ((((M'.liftQ f hM' : (a : M ⧸ M') → N →ₛₗ[σ] P) x : N →ₛₗ[σ] P) : (a : N) → P) n : P)
    ((0 : (a : M ⧸ M') → P) x : P)
Tactic: simp_rw [LinearMap.mem_ker, LinearMap.ext_iff, LinearMap.flip_apply, Submodule.Quotient.forall,
      Submodule.liftQ_apply, ← f.flip_apply, show f.flip n = 0 from hN' hn, LinearMap.zero_apply,
      forall_true_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Bilinear (goal)
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst : Ring R
inst_1 : Ring R₂
inst_2 : Ring S
inst_3 : Ring S₂
inst_4 : AddCommGroup M
inst_5 : AddCommGroup N
inst_6 : AddCommGroup P
inst_7 : Module R M
inst_8 : Module S N
inst_9 : Module R₂ P
inst_10 : Module S₂ P
inst_11 : SMulCommClass R₂ S₂ P
ρ : R →+* R₂
σ : S →+* S₂
M' : Submodule R M
N' : Submodule S N
f : M →ₛₗ[ρ] N →ₛₗ[σ] P
hM' : M' ≤ f.ker
hN' : N' ≤ f.flip.ker
n : N
hn : n ∈ N'
simp_rw :
  Eq (α := LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P)
    (((M'.liftQ f hM').flip : (a : N) → M ⧸ M' →ₛₗ[ρ] P) n : LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P)
    (0 : LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P)
simp_rw₁ :
  ∀ (x : M ⧸ M'),
    Eq.{u_7 + 1} (α := P)
      (((((M'.liftQ f hM').flip : (a : N) → M ⧸ M' →ₛₗ[ρ] P) n : LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P) :
            (a : M ⧸ M') → P)
          x :
        P)
      ((0 : (a : M ⧸ M') → P) x : P)
simp_rw₂ :
  ∀ (x : M ⧸ M'),
    Eq.{u_7 + 1} (α := P) ((((M'.liftQ f hM' : (a : M ⧸ M') → N →ₛₗ[σ] P) x : N →ₛₗ[σ] P) : (a : N) → P) n : P)
      ((0 : (a : M ⧸ M') → P) x : P)
⊢ n ∈ (M'.liftQ f hM').flip.ker
have simp_rw₃ : ∀ (a : M),
  Eq.{u_7 + 1} (α := P)
    ((((M'.liftQ f hM' : (a : M ⧸ M') → N →ₛₗ[σ] P) (Submodule.Quotient.mk a) : N →ₛₗ[σ] P) : (a : N) → P) n : P)
    ((0 : (a : M ⧸ M') → P) (Submodule.Quotient.mk a) : P)
Tactic: simp_rw [LinearMap.mem_ker, LinearMap.ext_iff, LinearMap.flip_apply, Submodule.Quotient.forall,
      Submodule.liftQ_apply, ← f.flip_apply, show f.flip n = 0 from hN' hn, LinearMap.zero_apply,
      forall_true_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Bilinear (goal)
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst : Ring R
inst_1 : Ring R₂
inst_2 : Ring S
inst_3 : Ring S₂
inst_4 : AddCommGroup M
inst_5 : AddCommGroup N
inst_6 : AddCommGroup P
inst_7 : Module R M
inst_8 : Module S N
inst_9 : Module R₂ P
inst_10 : Module S₂ P
inst_11 : SMulCommClass R₂ S₂ P
ρ : R →+* R₂
σ : S →+* S₂
M' : Submodule R M
N' : Submodule S N
f : M →ₛₗ[ρ] N →ₛₗ[σ] P
hM' : M' ≤ f.ker
hN' : N' ≤ f.flip.ker
n : N
hn : n ∈ N'
simp_rw :
  Eq (α := LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P)
    (((M'.liftQ f hM').flip : (a : N) → M ⧸ M' →ₛₗ[ρ] P) n : LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P)
    (0 : LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P)
simp_rw₁ :
  ∀ (x : M ⧸ M'),
    Eq.{u_7 + 1} (α := P)
      (((((M'.liftQ f hM').flip : (a : N) → M ⧸ M' →ₛₗ[ρ] P) n : LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P) :
            (a : M ⧸ M') → P)
          x :
        P)
      ((0 : (a : M ⧸ M') → P) x : P)
simp_rw₂ :
  ∀ (x : M ⧸ M'),
    Eq.{u_7 + 1} (α := P) ((((M'.liftQ f hM' : (a : M ⧸ M') → N →ₛₗ[σ] P) x : N →ₛₗ[σ] P) : (a : N) → P) n : P)
      ((0 : (a : M ⧸ M') → P) x : P)
simp_rw₃ :
  ∀ (a : M),
    Eq.{u_7 + 1} (α := P)
      ((((M'.liftQ f hM' : (a : M ⧸ M') → N →ₛₗ[σ] P) (Submodule.Quotient.mk a) : N →ₛₗ[σ] P) : (a : N) → P) n : P)
      ((0 : (a : M ⧸ M') → P) (Submodule.Quotient.mk a) : P)
⊢ n ∈ (M'.liftQ f hM').flip.ker
have simp_rw₄ : ∀ (a : M),
  Eq.{u_7 + 1} (α := P) ((((f : (a : M) → N →ₛₗ[σ] P) a : N →ₛₗ[σ] P) : (a : N) → P) n : P)
    ((0 : (a : M ⧸ M') → P) (Submodule.Quotient.mk a) : P)
Tactic: simp_rw [LinearMap.mem_ker, LinearMap.ext_iff, LinearMap.flip_apply, Submodule.Quotient.forall,
      Submodule.liftQ_apply, ← f.flip_apply, show f.flip n = 0 from hN' hn, LinearMap.zero_apply,
      forall_true_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Bilinear (goal)
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst : Ring R
inst_1 : Ring R₂
inst_2 : Ring S
inst_3 : Ring S₂
inst_4 : AddCommGroup M
inst_5 : AddCommGroup N
inst_6 : AddCommGroup P
inst_7 : Module R M
inst_8 : Module S N
inst_9 : Module R₂ P
inst_10 : Module S₂ P
inst_11 : SMulCommClass R₂ S₂ P
ρ : R →+* R₂
σ : S →+* S₂
M' : Submodule R M
N' : Submodule S N
f : M →ₛₗ[ρ] N →ₛₗ[σ] P
hM' : M' ≤ f.ker
hN' : N' ≤ f.flip.ker
n : N
hn : n ∈ N'
simp_rw :
  Eq (α := LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P)
    (((M'.liftQ f hM').flip : (a : N) → M ⧸ M' →ₛₗ[ρ] P) n : LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P)
    (0 : LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P)
simp_rw₁ :
  ∀ (x : M ⧸ M'),
    Eq.{u_7 + 1} (α := P)
      (((((M'.liftQ f hM').flip : (a : N) → M ⧸ M' →ₛₗ[ρ] P) n : LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P) :
            (a : M ⧸ M') → P)
          x :
        P)
      ((0 : (a : M ⧸ M') → P) x : P)
simp_rw₂ :
  ∀ (x : M ⧸ M'),
    Eq.{u_7 + 1} (α := P) ((((M'.liftQ f hM' : (a : M ⧸ M') → N →ₛₗ[σ] P) x : N →ₛₗ[σ] P) : (a : N) → P) n : P)
      ((0 : (a : M ⧸ M') → P) x : P)
simp_rw₃ :
  ∀ (a : M),
    Eq.{u_7 + 1} (α := P)
      ((((M'.liftQ f hM' : (a : M ⧸ M') → N →ₛₗ[σ] P) (Submodule.Quotient.mk a) : N →ₛₗ[σ] P) : (a : N) → P) n : P)
      ((0 : (a : M ⧸ M') → P) (Submodule.Quotient.mk a) : P)
simp_rw₄ :
  ∀ (a : M),
    Eq.{u_7 + 1} (α := P) ((((f : (a : M) → N →ₛₗ[σ] P) a : N →ₛₗ[σ] P) : (a : N) → P) n : P)
      ((0 : (a : M ⧸ M') → P) (Submodule.Quotient.mk a) : P)
⊢ n ∈ (M'.liftQ f hM').flip.ker
have simp_rw₅ : ∀ (a : M),
  Eq.{u_7 + 1} (α := P) ((((f.flip : (a : N) → M →ₛₗ[ρ] P) n : M →ₛₗ[ρ] P) : (a : M) → P) a : P)
    ((0 : (a : M ⧸ M') → P) (Submodule.Quotient.mk a) : P)
Tactic: simp_rw [LinearMap.mem_ker, LinearMap.ext_iff, LinearMap.flip_apply, Submodule.Quotient.forall,
      Submodule.liftQ_apply, ← f.flip_apply, show f.flip n = 0 from hN' hn, LinearMap.zero_apply,
      forall_true_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Bilinear (goal)
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst : Ring R
inst_1 : Ring R₂
inst_2 : Ring S
inst_3 : Ring S₂
inst_4 : AddCommGroup M
inst_5 : AddCommGroup N
inst_6 : AddCommGroup P
inst_7 : Module R M
inst_8 : Module S N
inst_9 : Module R₂ P
inst_10 : Module S₂ P
inst_11 : SMulCommClass R₂ S₂ P
ρ : R →+* R₂
σ : S →+* S₂
M' : Submodule R M
N' : Submodule S N
f : M →ₛₗ[ρ] N →ₛₗ[σ] P
hM' : M' ≤ f.ker
hN' : N' ≤ f.flip.ker
n : N
hn : n ∈ N'
simp_rw :
  Eq (α := LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P)
    (((M'.liftQ f hM').flip : (a : N) → M ⧸ M' →ₛₗ[ρ] P) n : LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P)
    (0 : LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P)
simp_rw₁ :
  ∀ (x : M ⧸ M'),
    Eq.{u_7 + 1} (α := P)
      (((((M'.liftQ f hM').flip : (a : N) → M ⧸ M' →ₛₗ[ρ] P) n : LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P) :
            (a : M ⧸ M') → P)
          x :
        P)
      ((0 : (a : M ⧸ M') → P) x : P)
simp_rw₂ :
  ∀ (x : M ⧸ M'),
    Eq.{u_7 + 1} (α := P) ((((M'.liftQ f hM' : (a : M ⧸ M') → N →ₛₗ[σ] P) x : N →ₛₗ[σ] P) : (a : N) → P) n : P)
      ((0 : (a : M ⧸ M') → P) x : P)
simp_rw₃ :
  ∀ (a : M),
    Eq.{u_7 + 1} (α := P)
      ((((M'.liftQ f hM' : (a : M ⧸ M') → N →ₛₗ[σ] P) (Submodule.Quotient.mk a) : N →ₛₗ[σ] P) : (a : N) → P) n : P)
      ((0 : (a : M ⧸ M') → P) (Submodule.Quotient.mk a) : P)
simp_rw₄ :
  ∀ (a : M),
    Eq.{u_7 + 1} (α := P) ((((f : (a : M) → N →ₛₗ[σ] P) a : N →ₛₗ[σ] P) : (a : N) → P) n : P)
      ((0 : (a : M ⧸ M') → P) (Submodule.Quotient.mk a) : P)
simp_rw₅ :
  ∀ (a : M),
    Eq.{u_7 + 1} (α := P) ((((f.flip : (a : N) → M →ₛₗ[ρ] P) n : M →ₛₗ[ρ] P) : (a : M) → P) a : P)
      ((0 : (a : M ⧸ M') → P) (Submodule.Quotient.mk a) : P)
⊢ n ∈ (M'.liftQ f hM').flip.ker
have simp_rw₆ : ∀ (a : M), Eq.{u_7 + 1} (α := P) ((0 : (a : M) → P) a : P) ((0 : (a : M ⧸ M') → P) (Submodule.Quotient.mk a) : P)
Tactic: simp_rw [LinearMap.mem_ker, LinearMap.ext_iff, LinearMap.flip_apply, Submodule.Quotient.forall,
      Submodule.liftQ_apply, ← f.flip_apply, show f.flip n = 0 from hN' hn, LinearMap.zero_apply,
      forall_true_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Bilinear (goal)
Goal:
R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst : Ring R
inst_1 : Ring R₂
inst_2 : Ring S
inst_3 : Ring S₂
inst_4 : AddCommGroup M
inst_5 : AddCommGroup N
inst_6 : AddCommGroup P
inst_7 : Module R M
inst_8 : Module S N
inst_9 : Module R₂ P
inst_10 : Module S₂ P
inst_11 : SMulCommClass R₂ S₂ P
ρ : R →+* R₂
σ : S →+* S₂
M' : Submodule R M
N' : Submodule S N
f : M →ₛₗ[ρ] N →ₛₗ[σ] P
hM' : M' ≤ f.ker
hN' : N' ≤ f.flip.ker
n : N
hn : n ∈ N'
simp_rw :
  Eq (α := LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P)
    (((M'.liftQ f hM').flip : (a : N) → M ⧸ M' →ₛₗ[ρ] P) n : LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P)
    (0 : LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P)
simp_rw₁ :
  ∀ (x : M ⧸ M'),
    Eq.{u_7 + 1} (α := P)
      (((((M'.liftQ f hM').flip : (a : N) → M ⧸ M' →ₛₗ[ρ] P) n : LinearMap.{u_1, u_2, u_5, u_7} ρ (M ⧸ M') P) :
            (a : M ⧸ M') → P)
          x :
        P)
      ((0 : (a : M ⧸ M') → P) x : P)
simp_rw₂ :
  ∀ (x : M ⧸ M'),
    Eq.{u_7 + 1} (α := P) ((((M'.liftQ f hM' : (a : M ⧸ M') → N →ₛₗ[σ] P) x : N →ₛₗ[σ] P) : (a : N) → P) n : P)
      ((0 : (a : M ⧸ M') → P) x : P)
simp_rw₃ :
  ∀ (a : M),
    Eq.{u_7 + 1} (α := P)
      ((((M'.liftQ f hM' : (a : M ⧸ M') → N →ₛₗ[σ] P) (Submodule.Quotient.mk a) : N →ₛₗ[σ] P) : (a : N) → P) n : P)
      ((0 : (a : M ⧸ M') → P) (Submodule.Quotient.mk a) : P)
simp_rw₄ :
  ∀ (a : M),
    Eq.{u_7 + 1} (α := P) ((((f : (a : M) → N →ₛₗ[σ] P) a : N →ₛₗ[σ] P) : (a : N) → P) n : P)
      ((0 : (a : M ⧸ M') → P) (Submodule.Quotient.mk a) : P)
simp_rw₅ :
  ∀ (a : M),
    Eq.{u_7 + 1} (α := P) ((((f.flip : (a : N) → M →ₛₗ[ρ] P) n : M →ₛₗ[ρ] P) : (a : M) → P) a : P)
      ((0 : (a : M ⧸ M') → P) (Submodule.Quotient.mk a) : P)
simp_rw₆ :
  ∀ (a : M), Eq.{u_7 + 1} (α := P) ((0 : (a : M) → P) a : P) ((0 : (a : M ⧸ M') → P) (Submodule.Quotient.mk a) : P)
⊢ n ∈ (M'.liftQ f hM').flip.ker
have simp_rw₇ : ∀ (a : M), True
Tactic: simp_rw [LinearMap.mem_ker, LinearMap.ext_iff, LinearMap.flip_apply, Submodule.Quotient.forall,
      Submodule.liftQ_apply, ← f.flip_apply, show f.flip n = 0 from hN' hn, LinearMap.zero_apply,
      forall_true_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Card (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submodule R M
⊢ Nat.card M = Nat.card.{u_2} ↥S * Nat.card.{u_2} (M ⧸ S)
have rw : Nat.card M = Nat.card.{u_2} ((M ⧸ S) × ↥S)
Tactic: rw [mul_comm, ← Nat.card_prod]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Defs (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
x y : M
⊢ (p.quotientRel : M → M → Prop) x y ↔ -(x - y) ∈ p
have rw : -x + y ∈ p.toAddSubgroup ↔ -x + y ∈ p
Tactic: rw [leftRel_apply, sub_eq_add_neg, neg_add, neg_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Defs (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' : 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₂
h : p = p'
a b : M
⊢ (p.quotientRel : M → M → Prop) a b ↔
    (p'.quotientRel : M → M → Prop) ((Equiv.refl M : (a : M) → M) a : M) ((Equiv.refl M : (a : M) → M) b : M)
have subst : (p.quotientRel : M → M → Prop) a b ↔
  (p.quotientRel : M → M → Prop) ((Equiv.refl M : (a : M) → M) a : M) ((Equiv.refl M : (a : M) → M) b : M)
Tactic: subst h
Cleared hypotheses: p', h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Pi (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
Ms : ι → Type u_3
inst_1 : (i : ι) → AddCommGroup (Ms i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (Ms i)
N : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Fintype ι
inst_6 : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) (Ms i) N
hf : ∀ (i : ι), p i ≤ comap (f i) q
x : (i : ι) → Ms i
⊢ Eq.{u_4 + 1} (α := N ⧸ q)
    ((piQuotientLift (Ms := Ms) p q f hf : (a : (i : ι) → Ms i ⧸ p i) → N ⧸ q) fun (i : ι) ↦ Quotient.mk (x i) : N ⧸ q)
    (Quotient.mk
        ((((lsum R Ms R : (a : (i : ι) → Ms i →ₗ[R] N) → ((i : ι) → Ms i) →ₗ[R] N) f : ((i : ι) → Ms i) →ₗ[R] N) :
            (a : (i : ι) → Ms i) → N)
          x) :
      N ⧸ q)
have rw : Eq.{u_4 + 1} (α := N ⧸ q)
  (∑ d : ι,
    ((p d).mapQ q (f d) sorry ∘ₗ proj (φ := fun (i : ι) ↦ Ms i ⧸ p i) d : (a : (i : ι) → Ms i ⧸ p i) → N ⧸ q) fun (i : ι) ↦
      Quotient.mk (x i))
  (∑ x_1 : ι, (q.mkQ : (a : N) → N ⧸ q) ((f x_1 ∘ₗ proj (φ := Ms) x_1 : (a : (i : ι) → Ms i) → N) x))
Tactic: rw [piQuotientLift, lsum_apply, sum_apply, ← mkQ_apply, lsum_apply, sum_apply, _root_.map_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Pi (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
Ms : ι → Type u_3
inst_1 : (i : ι) → AddCommGroup (Ms i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (Ms i)
N : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Fintype ι
inst_6 : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) (Ms i) N
hf : ∀ (i : ι), p i ≤ comap (f i) q
i : ι
x : Ms i ⧸ p i
⊢ Eq.{u_4 + 1} (α := N ⧸ q)
    ((piQuotientLift (Ms := Ms) p q f hf : (a : (i : ι) → Ms i ⧸ p i) → N ⧸ q)
        (Pi.single (M := fun (i : ι) ↦ Ms i ⧸ p i) i x) :
      N ⧸ q)
    (((p i).mapQ q (f i) ⋯ : (a : Ms i ⧸ p i) → N ⧸ q) x : N ⧸ q)
have simp_rw : Eq.{u_4 + 1} (α := N ⧸ q)
  (∑ x_1 : ι,
      ((p x_1).mapQ q (f x_1) sorry : (a : Ms x_1 ⧸ p x_1) → N ⧸ q) (Pi.single (M := fun (i : ι) ↦ Ms i ⧸ p i) i x x_1) :
    N ⧸ q)
  (((p i).mapQ q (f i) sorry : (a : Ms i ⧸ p i) → N ⧸ q) x : N ⧸ q)
Tactic: simp_rw [piQuotientLift, lsum_apply, sum_apply, comp_apply, proj_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Pi (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
Ms : ι → Type u_3
inst_1 : (i : ι) → AddCommGroup (Ms i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (Ms i)
N : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Fintype ι
inst_6 : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) (Ms i) N
hf : ∀ (i : ι), p i ≤ comap (f i) q
i : ι
x : Ms i ⧸ p i
⊢ Eq.{u_4 + 1} (α := N ⧸ q)
    (∑ x_1 : ι,
        ((p x_1).mapQ q (f x_1) ⋯ : (a : Ms x_1 ⧸ p x_1) → N ⧸ q) (Pi.single (M := fun (i : ι) ↦ Ms i ⧸ p i) i x x_1) :
      N ⧸ q)
    (((p i).mapQ q (f i) ⋯ : (a : Ms i ⧸ p i) → N ⧸ q) x : N ⧸ q)
have rw : Eq.{u_4 + 1} (α := N ⧸ q)
  (((p i).mapQ q (f i) sorry : (a : Ms i ⧸ p i) → N ⧸ q) (Pi.single (M := fun (i : ι) ↦ Ms i ⧸ p i) i x i) : N ⧸ q)
  (((p i).mapQ q (f i) sorry : (a : Ms i ⧸ p i) → N ⧸ q) x : N ⧸ q)
Tactic: rw [Finset.sum_eq_single i]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Pi (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
Ms : ι → Type u_3
inst_1 : (i : ι) → AddCommGroup (Ms i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (Ms i)
N : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Fintype ι
inst_6 : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) (Ms i) N
hf : ∀ (i : ι), p i ≤ comap (f i) q
i : ι
x : Ms i ⧸ p i
rw :
  Eq.{u_4 + 1} (α := N ⧸ q)
    (((p i).mapQ q (f i) ⋯ : (a : Ms i ⧸ p i) → N ⧸ q) (Pi.single (M := fun (i : ι) ↦ Ms i ⧸ p i) i x i) : N ⧸ q)
    (((p i).mapQ q (f i) ⋯ : (a : Ms i ⧸ p i) → N ⧸ q) x : N ⧸ q)
⊢ Eq.{u_4 + 1} (α := N ⧸ q)
    (∑ x_1 : ι,
        ((p x_1).mapQ q (f x_1) ⋯ : (a : Ms x_1 ⧸ p x_1) → N ⧸ q) (Pi.single (M := fun (i : ι) ↦ Ms i ⧸ p i) i x x_1) :
      N ⧸ q)
    (((p i).mapQ q (f i) ⋯ : (a : Ms i ⧸ p i) → N ⧸ q) x : N ⧸ q)
have h₀ : ∀ (b : ι),
  Membership.mem (γ := Finset ι) Finset.univ b →
    b ≠ i →
      Eq.{u_4 + 1} (α := N ⧸ q)
        (((p b).mapQ q (f b) sorry : (a : Ms b ⧸ p b) → N ⧸ q) (Pi.single (M := fun (i : ι) ↦ Ms i ⧸ p i) i x b) : N ⧸ q)
        (0 : N ⧸ q)
Tactic: rw [Finset.sum_eq_single i]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Pi (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
Ms : ι → Type u_3
inst_1 : (i : ι) → AddCommGroup (Ms i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (Ms i)
N : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Fintype ι
inst_6 : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) (Ms i) N
hf : ∀ (i : ι), p i ≤ comap (f i) q
i : ι
x : Ms i ⧸ p i
rw :
  Eq.{u_4 + 1} (α := N ⧸ q)
    (((p i).mapQ q (f i) ⋯ : (a : Ms i ⧸ p i) → N ⧸ q) (Pi.single (M := fun (i : ι) ↦ Ms i ⧸ p i) i x i) : N ⧸ q)
    (((p i).mapQ q (f i) ⋯ : (a : Ms i ⧸ p i) → N ⧸ q) x : N ⧸ q)
h₀ :
  ∀ (b : ι),
    Membership.mem (γ := Finset ι) Finset.univ b →
      b ≠ i →
        Eq.{u_4 + 1} (α := N ⧸ q)
          (((p b).mapQ q (f b) ⋯ : (a : Ms b ⧸ p b) → N ⧸ q) (Pi.single (M := fun (i : ι) ↦ Ms i ⧸ p i) i x b) : N ⧸ q)
          (0 : N ⧸ q)
⊢ Eq.{u_4 + 1} (α := N ⧸ q)
    (∑ x_1 : ι,
        ((p x_1).mapQ q (f x_1) ⋯ : (a : Ms x_1 ⧸ p x_1) → N ⧸ q) (Pi.single (M := fun (i : ι) ↦ Ms i ⧸ p i) i x x_1) :
      N ⧸ q)
    (((p i).mapQ q (f i) ⋯ : (a : Ms i ⧸ p i) → N ⧸ q) x : N ⧸ q)
have h₁ : i ∉ Finset.univ →
  Eq.{u_4 + 1} (α := N ⧸ q)
    (((p i).mapQ q (f i) sorry : (a : Ms i ⧸ p i) → N ⧸ q) (Pi.single (M := fun (i : ι) ↦ Ms i ⧸ p i) i x i) : N ⧸ q)
    (0 : N ⧸ q)
Tactic: rw [Finset.sum_eq_single i]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Pi (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
Ms : ι → Type u_3
inst_1 : (i : ι) → AddCommGroup (Ms i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (Ms i)
N : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Fintype ι
inst_6 : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) (Ms i) N
hf : ∀ (i : ι), p i ≤ comap (f i) q
i : ι
x : Ms i ⧸ p i
⊢ Eq.{u_4 + 1} (α := N ⧸ q)
    (((p i).mapQ q (f i) ⋯ : (a : Ms i ⧸ p i) → N ⧸ q) (Pi.single (M := fun (i : ι) ↦ Ms i ⧸ p i) i x i) : N ⧸ q)
    (((p i).mapQ q (f i) ⋯ : (a : Ms i ⧸ p i) → N ⧸ q) x : N ⧸ q)
have rw : Eq.{u_4 + 1} (α := N ⧸ q) (((p i).mapQ q (f i) sorry : (a : Ms i ⧸ p i) → N ⧸ q) x : N ⧸ q)
  (((p i).mapQ q (f i) sorry : (a : Ms i ⧸ p i) → N ⧸ q) x : N ⧸ q)
Tactic: rw [Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Pi (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
Ms : ι → Type u_3
inst_1 : (i : ι) → AddCommGroup (Ms i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (Ms i)
N : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Fintype ι
inst_6 : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) (Ms i) N
hf : ∀ (i : ι), p i ≤ comap (f i) q
i : ι
x : Ms i ⧸ p i
j : ι
hj : j ≠ i
⊢ Eq.{u_4 + 1} (α := N ⧸ q)
    (((p j).mapQ q (f j) ⋯ : (a : Ms j ⧸ p j) → N ⧸ q) (Pi.single (M := fun (i : ι) ↦ Ms i ⧸ p i) i x j) : N ⧸ q)
    (0 : N ⧸ q)
have h₀ : Eq.{u_4 + 1} (α := N ⧸ q) (((p j).mapQ q (f j) sorry : (a : Ms j ⧸ p j) → N ⧸ q) 0) 0
Tactic: rw [Pi.single_eq_of_ne hj, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Quotient.Pi (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
Ms : ι → Type u_3
inst_1 : (i : ι) → AddCommGroup (Ms i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (Ms i)
N : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Fintype ι
inst_6 : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) (Ms i) N
hf : ∀ (i : ι), p i ≤ comap (f i) q
i : ι
x : Ms i ⧸ p i
j : ι
hj : j ≠ i
h₀ : Eq.{u_4 + 1} (α := N ⧸ q) (((p j).mapQ q (f j) ⋯ : (a : Ms j ⧸ p j) → N ⧸ q) 0) 0
⊢ Eq.{u_4 + 1} (α := N ⧸ q)
    (((p j).mapQ q (f j) ⋯ : (a : Ms j ⧸ p j) → N ⧸ q) (Pi.single (M := fun (i : ι) ↦ Ms i ⧸ p i) i x j) : N ⧸ q)
    (0 : N ⧸ q)
have h₁ : Eq.{u_4 + 1} (α := N ⧸ q) 0 0
Tactic: rw [Pi.single_eq_of_ne hj, map_zero]