awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Quotient.Bilinear
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)
simp_rw₇ : ∀ (a : M), True
⊢ n ∈ (M'.liftQ f hM').flip.ker

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]

Premises used: LinearMap.zero_apply, Submodule.Quotient.forall, LinearMap.ext_iff, LinearMap.flip_apply, LinearMap.mem_ker, Submodule.liftQ_apply, forall_true_iff
-- Module: Mathlib.LinearAlgebra.Quotient.Bilinear
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
m : M
n : N
⊢ Eq.{u_7 + 1} (α := P)
    (((((liftQ₂ M' N' f hM' hN' : M ⧸ M' →ₛₗ[ρ] LinearMap.{u_3, u_4, u_6, u_7} σ (N ⧸ N') P) :
                (a : M ⧸ M') → N ⧸ N' →ₛₗ[σ] P)
              (Submodule.Quotient.mk m) :
            LinearMap.{u_3, u_4, u_6, u_7} σ (N ⧸ N') P) :
          (a : N ⧸ N') → P)
        (Submodule.Quotient.mk n) :
      P)
    ((((f : (a : M) → N →ₛₗ[σ] P) m : N →ₛₗ[σ] P) : (a : N) → P) n : P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Card
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
rw : Nat.card M = Nat.card.{u_2} ((M ⧸ S) × ↥S)
⊢ Nat.card M = Nat.card.{u_2} ↥S * Nat.card.{u_2} (M ⧸ S)

Tactic:
rw [mul_comm, ← Nat.card_prod]

Premises used: Nat.card_prod, mul_comm
-- Module: Mathlib.LinearAlgebra.Quotient.Card
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} ((M ⧸ S) × ↥S)

Tactic:
Nat.card_congr AddSubgroup.addGroupEquivQuotientProdAddSubgroup

Premises used: AddSubgroup.addGroupEquivQuotientProdAddSubgroup, Nat.card_congr
-- Module: Mathlib.LinearAlgebra.Quotient.Card
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} ((M ⧸ S) × ↥S)

Tactic:
exact Nat.card_congr AddSubgroup.addGroupEquivQuotientProdAddSubgroup

Premises used: AddSubgroup.addGroupEquivQuotientProdAddSubgroup, Nat.card_congr
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
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
rw : -x + y ∈ p.toAddSubgroup ↔ -x + y ∈ p
⊢ (p.quotientRel : M → M → Prop) x y ↔ -(x - y) ∈ p

Tactic:
rw [leftRel_apply, sub_eq_add_neg, neg_add, neg_neg]

Premises used: QuotientAddGroup.leftRel_apply, sub_eq_add_neg, neg_add, neg_neg
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
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
⊢ -x + y ∈ p.toAddSubgroup ↔ -x + y ∈ p

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
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
⊢ Eq (α := Quotient p.quotientRel) (Quotient.mk' x) (mk x)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, Quotient.mk', rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
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
⊢ Eq (α := Quotient p.quotientRel) (Quotient.mk'' x) (mk x)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
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
⊢ Eq (α := Quot (α := M) (⇑p.quotientRel : M → M → Prop)) (Quot.mk (⇑p.quotientRel : M → M → Prop) x) (mk x)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
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
⊢ Eq (α := M ⧸ p.toAddSubgroup) (↑x : M ⧸ p.toAddSubgroup) (mk x)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, Submodule.quotientRel, rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
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
⊢ Eq (α := M ⧸ p) (mk x) (mk y) ↔ -x + y ∈ p

Tactic:
QuotientAddGroup.eq

Premises used: QuotientAddGroup.eq, Set.Mem, Submodule.Quotient.mk, Submodule.quotientRel
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
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
⊢ Eq (α := M ⧸ p) (mk x) (mk y) ↔ x - y ∈ p

Tactic:
(Submodule.Quotient.eq' p).trans (leftRel_apply.symm.trans p.quotientRel_def)

Premises used: Submodule.quotientRel_def, QuotientAddGroup.leftRel_apply, Iff.trans, Submodule.Quotient.eq', Iff.symm
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
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
⊢ Eq.{u_2 + 1} (α := M ⧸ p) (mk 0) 0

Tactic:
rfl

Premises used: Submodule.Quotient.mk, rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
Goal:
R : Type u_1
M : Type u_2
x : M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
⊢ Eq (α := M ⧸ p) (mk x) 0 ↔ x ∈ p

Tactic:
simpa using (Quotient.eq' p : mk x = 0 ↔ _)

Premises used: Submodule.Quotient.eq'
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
Goal:
R : Type u_1
M : Type u_2
x y : M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
⊢ mk (x + y) = HAdd.hAdd (α := M ⧸ p) (mk x) (mk y)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, Quotient.map₂, rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
Goal:
R : Type u_1
M : Type u_2
x : M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
⊢ Eq (α := M ⧸ p) (mk (-x)) (-mk x)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, Quot.map, Quotient.map', rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
Goal:
R : Type u_1
M : Type u_2
x y : M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
⊢ mk (x - y) = HSub.hSub (α := M ⧸ p) (mk x) (mk y)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, Quotient.map₂, rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
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
m : M ⧸ p
⊢ mk (Quotient.out m) = m

Tactic:
Quotient.out_eq m

Premises used: Submodule.Quotient.mk, Quotient.out_eq
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
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 : M ⧸ p → Prop
⊢ (∀ (a : M ⧸ p), P a) ↔ ∀ (a : M), P (mk a)

Tactic:
Quotient.forall

Premises used: Quotient.forall, Submodule.Quotient.mk
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
Goal:
R : Type u_1
M : Type u_2
r : R
x_1 y_1 : M
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' : Submodule R M
S : Type u_3
inst_3 : SMul S R
inst_4 : SMul S M
inst_5 : IsScalarTower S R M
P : Submodule R M
a : S
x y : M
h : (P.quotientRel : M → M → Prop) x y
⊢ HAdd.hAdd (α := M) (-(fun (x : M) ↦ a • x) x) ((fun (x : M) ↦ a • x) y) ∈ P.toAddSubgroup

Tactic:
simpa using Submodule.smul_mem P (a • (1 : R)) (leftRel_apply.mp h)

Premises used: QuotientAddGroup.leftRel_apply, Iff.mp, HSMul.hSMul, OfNat.ofNat, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
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
S : Type u_3
inst_3 : SMul S R
inst_4 : SMul S M
inst_5 : IsScalarTower S R M
r : S
x : M
⊢ mk (r • x) = HSMul.hSMul (β := M ⧸ p) r (mk x)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, Quot.map, Quotient.map', rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
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
S : Type u_3
inst_3 : Semiring S
inst_4 : SMul S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
P : Submodule R M
⊢ Eq.{u_2 + 1} (α := M ⧸ P) (mk 0) 0

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
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
S : Type u_3
inst_3 : Semiring S
inst_4 : SMul S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
P : Submodule R M
x_1 x_2 : M
⊢ mk (x_1 + x_2) = HAdd.hAdd (α := M ⧸ P) (mk x_1) (mk x_2)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
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
C : M ⧸ p → Prop
x : M ⧸ p
H : ∀ (z : M), C (mk z)
⊢ C x

Tactic:
Quotient.inductionOn' x H

Premises used: Quotient.inductionOn'
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
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
b : M ⧸ p
x : M
⊢ ∃ (a : M), Eq (α := M ⧸ p) (mk a) (Quot.mk (⇑p.quotientRel : M → M → Prop) x)

Tactic:
⟨x, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
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
b : M ⧸ p
x : M
⊢ ∃ (a : M), Eq (α := M ⧸ p) (mk a) (Quot.mk (⇑p.quotientRel : M → M → Prop) x)

Tactic:
exact ⟨x, rfl⟩
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
Goal:
R_1 : Type u_1
M_1 : Type u_2
r : R_1
x y : M_1
inst : Ring R_1
inst_1 : AddCommGroup M_1
inst_2 : Module R_1 M_1
p p' : Submodule R_1 M_1
R : Type u_3
M : Type u_4
inst_3 : Ring R
inst_4 : AddCommGroup M
inst_5 : Module R M
N : Submodule R M
inst_6 : Small.{u, u_4} M
⊢ Small.{u, u_4} (M ⧸ N)

Tactic:
small_of_surjective (Submodule.Quotient.mk_surjective _)

Premises used: small_of_surjective, Submodule.Quotient.mk_surjective
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
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
M₂ : Type u_3
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
f g : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (M ⧸ p) M₂
h :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := M₂) ((f : (a : M ⧸ p) → M₂) (Quotient.mk x) : M₂) ((g : (a : M ⧸ p) → M₂) (Quotient.mk x) : M₂)
⊢ f = g

Tactic:
LinearMap.ext fun x => Submodule.Quotient.induction_on _ x h

Premises used: Submodule.Quotient.induction_on, LinearMap.ext
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
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
M₂ : Type u_3
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
⊢ ∀ (x y : M), Quotient.mk (x + y) = HAdd.hAdd (α := M ⧸ p) (Quotient.mk x) (Quotient.mk y)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
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
M₂ : Type u_3
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
⊢ ∀ (m : R) (x : M),
    Quotient.mk (m • x) = HSMul.hSMul (α := R) (β := M ⧸ p) ((RingHom.id R : (a : R) → R) m : R) (Quotient.mk x)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
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
⊢ Eq (α := M ⧸ p) ((p.mkQ : (a : M) → M ⧸ p) x : M ⧸ p) (Quotient.mk x : M ⧸ p)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
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
b : M ⧸ p
x : M
⊢ ∃ (a : M),
    Eq (α := M ⧸ p) ((p.mkQ : (a : M) → M ⧸ p) a : M ⧸ p)
      (Quot.mk (⇑p.quotientRel : M → M → Prop) x : Quot (α := M) (⇑p.quotientRel : M → M → Prop))

Tactic:
⟨x, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
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
b : M ⧸ p
x : M
⊢ ∃ (a : M),
    Eq (α := M ⧸ p) ((p.mkQ : (a : M) → M ⧸ p) a : M ⧸ p)
      (Quot.mk (⇑p.quotientRel : M → M → Prop) x : Quot (α := M) (⇑p.quotientRel : M → M → Prop))

Tactic:
exact ⟨x, rfl⟩
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
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 g : LinearMap.{u_1, u_3, u_2, u_4} τ₁₂ (M ⧸ p) M₂
h : f ∘ₛₗ p.mkQ = g ∘ₛₗ p.mkQ
⊢ f = g

Tactic:
LinearMap.ext fun x => Submodule.Quotient.induction_on _ x <| (LinearMap.congr_fun h :)

Premises used: Submodule.Quotient.induction_on, LinearMap.ext
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
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
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)
⊢ (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
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
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 : 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₂
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)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
Goal:
R : Type u_1
M : Type u_2
r : R
x_1 y_1 : 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'
x_2 : M ⧸ p
x : M
y_2 : M ⧸ p
y : M
⊢ Equiv.toFun (Quotient.congr (Equiv.refl M) ⋯)
      (HAdd.hAdd (α := M ⧸ p) (Quot.mk (⇑p.quotientRel : M → M → Prop) x) (Quot.mk (⇑p.quotientRel : M → M → Prop) y)) =
    HAdd.hAdd (α := M ⧸ p')
      (Equiv.toFun (α := Quotient p.quotientRel) (Quotient.congr (Equiv.refl M) ⋯)
        (Quot.mk (⇑p.quotientRel : M → M → Prop) x))
      (Equiv.toFun (α := Quotient p.quotientRel) (Quotient.congr (Equiv.refl M) ⋯)
        (Quot.mk (⇑p.quotientRel : M → M → Prop) y))

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
Goal:
R : Type u_1
M : Type u_2
r : R
x_1 y_1 : 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'
x : R
x_2 : M ⧸ p
y : M
⊢ Equiv.toFun (Quotient.congr (Equiv.refl M) ⋯)
      (HSMul.hSMul (β := M ⧸ p) x (Quot.mk (⇑p.quotientRel : M → M → Prop) y)) =
    HSMul.hSMul (α := R) (β := M ⧸ p') ((RingHom.id R : (a : R) → R) x : R)
      (Equiv.toFun (α := Quotient p.quotientRel) (Quotient.congr (Equiv.refl M) ⋯)
        (Quot.mk (⇑p.quotientRel : M → M → Prop) y))

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Defs
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
h : p = p'
x : M
⊢ Eq (α := M ⧸ p') ((p.quotEquivOfEq p' h : (a : M ⧸ p) → M ⧸ p') (Quotient.mk x) : M ⧸ p') (Quotient.mk x : M ⧸ p')

Tactic:
rfl

Premises used: Submodule.Quotient.mk, Quot.map, rfl
-- Module: Mathlib.LinearAlgebra.Quotient.Pi
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
rw :
  Eq.{u_4 + 1} (α := N ⧸ q)
    (∑ d : ι,
      ((p d).mapQ q (f d) ⋯ ∘ₗ 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))
⊢ 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)

Tactic:
rw [piQuotientLift, lsum_apply, sum_apply, ← mkQ_apply, lsum_apply, sum_apply, _root_.map_sum]

Premises used: LinearMap.lsum_apply, Submodule.mkQ_apply, map_sum, Submodule.piQuotientLift, LinearMap.sum_apply
-- Module: Mathlib.LinearAlgebra.Quotient.Pi
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)
    (∑ d : ι,
      ((p d).mapQ q (f d) ⋯ ∘ₗ 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:
simp only [coe_proj, mapQ_apply, mkQ_apply, comp_apply]

Premises used: Submodule.mapQ_apply, LinearMap.comp_apply, LinearMap.coe_proj, Submodule.mkQ_apply
-- Module: Mathlib.LinearAlgebra.Quotient.Pi
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
simp_rw :
  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)
⊢ 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)

Tactic:
simp_rw [piQuotientLift, lsum_apply, sum_apply, comp_apply, proj_apply]

Premises used: LinearMap.lsum_apply, LinearMap.proj_apply, LinearMap.comp_apply, Submodule.piQuotientLift, LinearMap.sum_apply
-- Module: Mathlib.LinearAlgebra.Quotient.Pi
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)
h₁ :
  i ∉ Finset.univ →
    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)
      (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)

Tactic:
rw [Finset.sum_eq_single i]

Premises used: Finset.sum_eq_single
-- Module: Mathlib.LinearAlgebra.Quotient.Pi
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 rw₁ :
  Eq.{u_4 + 1} (α := N ⧸ q) (((p i).mapQ q (f i) ⋯ : (a : Ms i ⧸ p i) → N ⧸ q) x : N ⧸ q)
    (((p i).mapQ q (f i) ⋯ : (a : Ms i ⧸ p i) → N ⧸ q) x : N ⧸ q)
⊢ 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)

Tactic:
rw [Pi.single_eq_same]

Premises used: Pi.single_eq_same
-- Module: Mathlib.LinearAlgebra.Quotient.Pi
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
h₁ h₂ : Eq.{u_4 + 1} (α := 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)

Tactic:
rw [Pi.single_eq_of_ne hj, map_zero]

Premises used: map_zero, Pi.single_eq_of_ne