awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a_1 b_1 : R
inst_1 : I.IsTwoSided
a_2 : R ⧸ I
a : R
x : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
b : (i : ι) → R
y : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
c : (i : ι) → R
⊢ HSMul.hSMul (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a)
      (HAdd.hAdd (α :=
        HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
        (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) b)
        (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) c)) =
    HSMul.hSMul (α := R ⧸ I) (β :=
        HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
        (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a)
        (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) b) +
      HSMul.hSMul (α := R ⧸ I) (β :=
        HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
        (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a)
        (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) c)

Tactic:
congr_arg _ (smul_add _ _ _)

Premises used: Submodule.Quotient.mk, Quotient.map₂, congr_arg, smul_add, Quotient.liftOn₂'
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a_1 b_1 : R
inst_1 : I.IsTwoSided
a_2 : R ⧸ I
a : R
x : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
b : (i : ι) → R
y : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
c : (i : ι) → R
⊢ HSMul.hSMul (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a)
      (HAdd.hAdd (α :=
        HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
        (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) b)
        (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) c)) =
    HSMul.hSMul (α := R ⧸ I) (β :=
        HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
        (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a)
        (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) b) +
      HSMul.hSMul (α := R ⧸ I) (β :=
        HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
        (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a)
        (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) c)

Tactic:
exact congr_arg _ (smul_add _ _ _)

Premises used: congr_arg, smul_add
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a_1 b_1 : R
inst_1 : I.IsTwoSided
r : R ⧸ I
a : R
s : R ⧸ I
b : R
x : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
c : (i : ι) → R
⊢ HSMul.hSMul (β := HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
      (HAdd.hAdd (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a)
        (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) b))
      (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) c) =
    HSMul.hSMul (α := R ⧸ I) (β :=
        HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
        (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a)
        (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) c) +
      HSMul.hSMul (α := R ⧸ I) (β :=
        HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
        (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) b)
        (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) c)

Tactic:
congr_arg _ (add_smul _ _ _)

Premises used: Submodule.Quotient.mk, Quotient.map₂, congr_arg, add_smul, Quotient.liftOn₂'
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a_1 b_1 : R
inst_1 : I.IsTwoSided
r : R ⧸ I
a : R
s : R ⧸ I
b : R
x : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
c : (i : ι) → R
⊢ HSMul.hSMul (β := HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
      (HAdd.hAdd (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a)
        (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) b))
      (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) c) =
    HSMul.hSMul (α := R ⧸ I) (β :=
        HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
        (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a)
        (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) c) +
      HSMul.hSMul (α := R ⧸ I) (β :=
        HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
        (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) b)
        (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) c)

Tactic:
exact congr_arg _ (add_smul _ _ _)

Premises used: congr_arg, add_smul
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a_1 b : R
inst_1 : I.IsTwoSided
x : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
a : (i : ι) → R
⊢ HSMul.hSMul (α := R ⧸ I) (β :=
      HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)) 0
      (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) a) =
    0

Tactic:
congr_arg _ (zero_smul _ _)

Premises used: Submodule.Quotient.mk, congr_arg, zero_smul, Quotient.liftOn₂'
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a_1 b : R
inst_1 : I.IsTwoSided
x : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
a : (i : ι) → R
⊢ HSMul.hSMul (α := R ⧸ I) (β :=
      HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)) 0
      (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) a) =
    0

Tactic:
exact congr_arg _ (zero_smul _ _)

Premises used: congr_arg, zero_smul
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a b : R
inst_1 : I.IsTwoSided
x : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
a_1 : (i : ι) → R
y : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
a_2 : (i : ι) → R
⊢ Quotient.liftOn'
      (HAdd.hAdd (α :=
        HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
        (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) a_1)
        (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) a_2))
      (fun (f : (i : ι) → R) (i : ι) ↦ (Quotient.mk I : (a : R) → R ⧸ I) (f i)) ⋯ =
    HAdd.hAdd (α := ι → R ⧸ I)
      (Quotient.liftOn' (s₁ := Submodule.quotientRel (R := (i : ι) → R) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
        (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) a_1)
        (fun (f : (i : ι) → R) (i : ι) ↦ (Quotient.mk I : (a : R) → R ⧸ I) (f i)) ⋯)
      (Quotient.liftOn' (s₁ := Submodule.quotientRel (R := (i : ι) → R) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
        (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) a_2)
        (fun (f : (i : ι) → R) (i : ι) ↦ (Quotient.mk I : (a : R) → R ⧸ I) (f i)) ⋯)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a b : R
inst_1 : I.IsTwoSided
m : R ⧸ I
a_1 : R
x : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
a_2 : (i : ι) → R
⊢ Quotient.liftOn'
      (HSMul.hSMul (α := R ⧸ I) (β :=
        HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
        (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a_1)
        (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) a_2))
      (fun (f : (i : ι) → R) (i : ι) ↦ (Quotient.mk I : (a : R) → R ⧸ I) (f i)) ⋯ =
    HSMul.hSMul (α := R ⧸ I) (β := ι → R ⧸ I)
      ((RingHom.id (R ⧸ I) : (a : R ⧸ I) → R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a_1) : R ⧸ I)
      (Quotient.liftOn' (s₁ := Submodule.quotientRel (R := (i : ι) → R) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
        (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) a_2)
        (fun (f : (i : ι) → R) (i : ι) ↦ (Quotient.mk I : (a : R) → R ⧸ I) (f i)) ⋯)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a b : R
inst_1 : I.IsTwoSided
x_1 : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
x : (i : ι) → R
⊢ Eq (α := HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
    ((fun (x : ι → R ⧸ I) ↦
        ((Quotient.mk (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I) : (a : ι → R) → (ι → R) ⧸ pi fun (x : ι) ↦ I)
            fun (x_2 : ι) ↦ Quotient.out (x x_2) :
          HasQuotient.Quotient (ι → R) (B := Ideal (ι → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)))
      ((fun (x : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)) ↦
          (Quotient.liftOn' x (fun (f : (i : ι) → R) (i : ι) ↦ (Quotient.mk I : (a : R) → R ⧸ I) (f i)) ⋯ : ι → R ⧸ I))
        (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) x)))
    (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) x)

Tactic:
Ideal.Quotient.eq.2 fun i ↦ Ideal.Quotient.eq.1 (Quotient.out_eq' _)

Premises used: Iff.mpr, QuotientAddGroup.leftRel_apply, Quotient.out_eq', Quotient.liftOn', Ideal.Quotient.mk, Submodule.Quotient.mk, Ideal.Quotient.eq, funext, Iff.mp, DFunLike.coe, Submodule.Quotient.eq', Setoid.r, Quot.mk
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst : Ring R
I J : Ideal R
a b : R
inst_1 : I.IsTwoSided
x_1 : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
x : (i : ι) → R
⊢ Eq (α := HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
    ((fun (x : ι → R ⧸ I) ↦
        ((Quotient.mk (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I) : (a : ι → R) → (ι → R) ⧸ pi fun (x : ι) ↦ I)
            fun (x_2 : ι) ↦ Quotient.out (x x_2) :
          HasQuotient.Quotient (ι → R) (B := Ideal (ι → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)))
      ((fun (x : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)) ↦
          (Quotient.liftOn' x (fun (f : (i : ι) → R) (i : ι) ↦ (Quotient.mk I : (a : R) → R ⧸ I) (f i)) ⋯ : ι → R ⧸ I))
        (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) x)))
    (Quot.mk (⇑(Submodule.quotientRel (pi fun (x : ι) ↦ I)) : ((i : ι) → R) → ((i : ι) → R) → Prop) x)

Tactic:
exact Ideal.Quotient.eq.2 fun i ↦ Ideal.Quotient.eq.1 (Quotient.out_eq' _)
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
inst_2 : Finite ι
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
intro : ∀ (val : Fintype ι), Membership.mem (α := R) I ((f : (a : ι → R) → ι' → R) x i : R)
⊢ Membership.mem (α := R) I ((f : (a : ι → R) → ι' → R) x i : R)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
inst_2 : Finite ι
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
val : Fintype ι
intro :
  Membership.mem (α := R) I
    ((f : (a : ι → R) → ι' → R) (∑ i : ι, HSMul.hSMul (β := (j : ι) → R) (x i) fun (j : ι) ↦ if i = j then 1 else 0) i :
      R)
⊢ Membership.mem (α := R) I ((f : (a : ι → R) → ι' → R) x i : R)

Tactic:
rw [pi_eq_sum_univ x]

Premises used: pi_eq_sum_univ
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
inst_2 : Finite ι
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
val : Fintype ι
intro :
  ∑ x_1 : ι, HMul.hMul (β := R) (x x_1) ((f : (a : ι → R) → ι' → R) (fun (j : ι) ↦ if x_1 = j then 1 else 0) i : R) ∈ I
⊢ Membership.mem (α := R) I
    ((f : (a : ι → R) → ι' → R) (∑ i : ι, HSMul.hSMul (β := (j : ι) → R) (x i) fun (j : ι) ↦ if i = j then 1 else 0) i :
      R)

Tactic:
simp only [Finset.sum_apply, smul_eq_mul, map_sum, Pi.smul_apply, map_smul]

Premises used: Finset.sum_apply, map_sum, smul_eq_mul, map_smul, Pi.smul_apply
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
inst_2 : Finite ι
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
val : Fintype ι
⊢ ∑ x_1 : ι, HMul.hMul (β := R) (x x_1) ((f : (a : ι → R) → ι' → R) (fun (j : ι) ↦ if x_1 = j then 1 else 0) i : R) ∈ I

Tactic:
I.sum_mem fun j _ => I.mul_mem_right _ (hi j)

Premises used: Set.Mem, Submodule.sum_mem, Ideal.mul_mem_right, OfNat.ofNat, Eq, DFunLike.coe, ite
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
inst_2 : Finite ι
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
val : Fintype ι
⊢ ∑ x_1 : ι, HMul.hMul (β := R) (x x_1) ((f : (a : ι → R) → ι' → R) (fun (j : ι) ↦ if x_1 = j then 1 else 0) i : R) ∈ I

Tactic:
exact I.sum_mem fun j _ => I.mul_mem_right _ (hi j)

Premises used: Submodule.sum_mem, Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
inst_2 : Finite ι
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
intro : ∀ (val : Fintype ι), Membership.mem (α := R) I ((f : (a : ι → R) → ι' → R) x i : R)
intro₁ :
  ∀ (val : Fintype ι),
    Membership.mem (α := R) I
      ((f : (a : ι → R) → ι' → R) (∑ i : ι, HSMul.hSMul (β := (j : ι) → R) (x i) fun (j : ι) ↦ if i = j then 1 else 0)
          i :
        R)
intro₂ :
  ∀ (val : Fintype ι),
    ∑ x_1 : ι, HMul.hMul (β := R) (x x_1) ((f : (a : ι → R) → ι' → R) (fun (j : ι) ↦ if x_1 = j then 1 else 0) i : R) ∈
      I
⊢ Membership.mem (α := R) I ((f : (a : ι → R) → ι' → R) x i : R)

Tactic:
classical
    cases nonempty_fintype ι
    rw [pi_eq_sum_univ x]
    simp only [Finset.sum_apply, smul_eq_mul, map_sum, Pi.smul_apply, map_smul]
    exact I.sum_mem fun j _ => I.mul_mem_right _ (hi j)

Premises used: Finset.sum_apply, Submodule.sum_mem, map_sum, nonempty_fintype, Ideal.mul_mem_right, smul_eq_mul, map_smul, Pi.smul_apply
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
⊢ Eq.{u_3 + 1} (α := Set R) univ (⋃ (x : R ⧸ I), Quotient.out x +ᵥ (↑I : Set R))

Tactic:
QuotientAddGroup.univ_eq_iUnion_vadd I.toAddSubgroup

Premises used: QuotientAddGroup.univ_eq_iUnion_vadd, Submodule.toAddSubgroup, Submodule.quotientRel
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
⊢ Finite R ↔ Finite.{u_3 + 1} ↥I ∧ Finite.{u_3 + 1} (R ⧸ I)

Tactic:
finite_iff_addSubgroup_quotient I.toAddSubgroup

Premises used: Set.Mem, finite_iff_addSubgroup_quotient, Submodule.toAddSubgroup, Submodule.quotientRel
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : Finite.{u_3 + 1} ↥I
inst_2 : Finite.{u_3 + 1} (R ⧸ I)
rw : Finite.{u_3 + 1} ↥I ∧ Finite.{u_3 + 1} (R ⧸ I)
rw₁ : Ideal R
⊢ Finite R

Tactic:
rw [finite_iff_ideal_quotient]

Premises used: finite_iff_ideal_quotient
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : Finite.{u_3 + 1} ↥I
inst_2 : Finite.{u_3 + 1} (R ⧸ I)
left : Finite.{u_3 + 1} ↥I
right : Finite.{u_3 + 1} (R ⧸ I)
⊢ Finite.{u_3 + 1} ↥I ∧ Finite.{u_3 + 1} (R ⧸ I)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : Finite.{u_3 + 1} ↥I
inst_2 : Finite.{u_3 + 1} (R ⧸ I)
⊢ Finite.{u_3 + 1} ↥I

Tactic:
assumption
-- Module: Mathlib.RingTheory.Ideal.Quotient.Basic
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : Finite.{u_3 + 1} ↥I
inst_2 : Finite.{u_3 + 1} (R ⧸ I)
⊢ Finite.{u_3 + 1} (R ⧸ I)

Tactic:
assumption
-- Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
I : ι → Ideal R
inst_3 : Fintype ι
inst_4 : DecidableEq ι
a :
  ∀ (x : M),
    Eq (α := ((i : ι) → R ⧸ I i) ⊗[R] M)
      ((((AlgebraTensorModule.curry
                    (rTensor M (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) :
                  R →ₗ[R] M →ₗ[R] ((i : ι) → R ⧸ I i) ⊗[R] M) :
                (a : R) → M →ₗ[R] ((i : ι) → R ⧸ I i) ⊗[R] M)
              1 :
            (a : M) → ((i : ι) → R ⧸ I i) ⊗[R] M)
          x :
        ((i : ι) → R ⧸ I i) ⊗[R] M)
      ((((AlgebraTensorModule.curry
                    ((↑(LinearEquiv.symm (piLeft R M fun (i : ι) ↦ R ⧸ I i)) :
                        ((i : ι) → (R ⧸ I i) ⊗[R] M) →ₗ[R] ((i : ι) → R ⧸ I i) ⊗[R] M) ∘ₗ
                      (LinearMap.pi (φ := fun (i : ι) ↦ (R ⧸ I i) ⊗[R] M) fun (i : ι) ↦
                          (TensorProduct.mk R (R ⧸ I i) M : (a : R ⧸ I i) → M →ₗ[R] (R ⧸ I i) ⊗[R] M) 1) ∘ₗ
                        (↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M)) :
                  R →ₗ[R] M →ₗ[R] ((i : ι) → R ⧸ I i) ⊗[R] M) :
                (a : R) → M →ₗ[R] ((i : ι) → R ⧸ I i) ⊗[R] M)
              1 :
            (a : M) → ((i : ι) → R ⧸ I i) ⊗[R] M)
          x :
        ((i : ι) → R ⧸ I i) ⊗[R] M)
⊢ Eq (α := R ⊗[R] M →ₗ[R] ((i : ι) → R ⧸ I i) ⊗[R] M)
    (rTensor M (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i)))
    ((↑(LinearEquiv.symm (piLeft R M fun (i : ι) ↦ R ⧸ I i)) :
        ((i : ι) → (R ⧸ I i) ⊗[R] M) →ₗ[R] ((i : ι) → R ⧸ I i) ⊗[R] M) ∘ₗ
      (LinearMap.pi (φ := fun (i : ι) ↦ (R ⧸ I i) ⊗[R] M) fun (i : ι) ↦
          (TensorProduct.mk R (R ⧸ I i) M : (a : R ⧸ I i) → M →ₗ[R] (R ⧸ I i) ⊗[R] M) 1) ∘ₗ
        (↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M))

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
I : ι → Ideal R
inst_3 : Fintype ι
inst_4 : DecidableEq ι
x : M
⊢ Eq (α := ((i : ι) → R ⧸ I i) ⊗[R] M)
    ((((AlgebraTensorModule.curry
                  (rTensor M (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) :
                R →ₗ[R] M →ₗ[R] ((i : ι) → R ⧸ I i) ⊗[R] M) :
              (a : R) → M →ₗ[R] ((i : ι) → R ⧸ I i) ⊗[R] M)
            1 :
          (a : M) → ((i : ι) → R ⧸ I i) ⊗[R] M)
        x :
      ((i : ι) → R ⧸ I i) ⊗[R] M)
    ((((AlgebraTensorModule.curry
                  ((↑(LinearEquiv.symm (piLeft R M fun (i : ι) ↦ R ⧸ I i)) :
                      ((i : ι) → (R ⧸ I i) ⊗[R] M) →ₗ[R] ((i : ι) → R ⧸ I i) ⊗[R] M) ∘ₗ
                    (LinearMap.pi (φ := fun (i : ι) ↦ (R ⧸ I i) ⊗[R] M) fun (i : ι) ↦
                        (TensorProduct.mk R (R ⧸ I i) M : (a : R ⧸ I i) → M →ₗ[R] (R ⧸ I i) ⊗[R] M) 1) ∘ₗ
                      (↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M)) :
                R →ₗ[R] M →ₗ[R] ((i : ι) → R ⧸ I i) ⊗[R] M) :
              (a : R) → M →ₗ[R] ((i : ι) → R ⧸ I i) ⊗[R] M)
            1 :
          (a : M) → ((i : ι) → R ⧸ I i) ⊗[R] M)
        x :
      ((i : ι) → R ⧸ I i) ⊗[R] M)

Tactic:
simp [LinearMap.pi, LinearEquiv.piCongrRight]

Premises used: LinearMap.pi, LinearEquiv.piCongrRight
-- Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst_3 : Finite ι
⊢ Surjective (α := R ⊗[R] M) (β := ((i : ι) → R ⧸ I i) ⊗[R] M)
    (⇑(rTensor M (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) :
      (a : R ⊗[R] M) → ((i : ι) → R ⧸ I i) ⊗[R] M)

Tactic:
have := rTensor_surjective M (pi_mkQ_surjective hI)
-- Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst_3 : Finite ι
this :
  Surjective (α := R ⊗[R] M) (β := ((i : ι) → R ⧸ I i) ⊗[R] M)
    (⇑(rTensor M (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) :
      (a : R ⊗[R] M) → ((i : ι) → R ⧸ I i) ⊗[R] M)
⊢ Surjective (α := R ⊗[R] M) (β := ((i : ι) → R ⧸ I i) ⊗[R] M)
    (⇑((↑(LinearEquiv.symm (piLeft R M fun (i : ι) ↦ R ⧸ I i)) :
            ((i : ι) → (R ⧸ I i) ⊗[R] M) →ₗ[R] ((i : ι) → R ⧸ I i) ⊗[R] M) ∘ₗ
          (LinearMap.pi (φ := fun (i : ι) ↦ (R ⧸ I i) ⊗[R] M) fun (i : ι) ↦
              (TensorProduct.mk R (R ⧸ I i) M : (a : R ⧸ I i) → M →ₗ[R] (R ⧸ I i) ⊗[R] M) 1) ∘ₗ
            (↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M)) :
      (a : R ⊗[R] M) → ((i : ι) → R ⧸ I i) ⊗[R] M)

Tactic:
rw [pi_mkQ_rTensor] at this

Premises used: Ideal.pi_mkQ_rTensor
-- Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst_3 : Finite ι
this :
  Surjective (α := R ⊗[R] M) (β := ((i : ι) → R ⧸ I i) ⊗[R] M)
    (⇑(rTensor M (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) :
      (a : R ⊗[R] M) → ((i : ι) → R ⧸ I i) ⊗[R] M)
⊢ Surjective (α := R ⊗[R] M) (β := ((i : ι) → R ⧸ I i) ⊗[R] M)
    (⇑((↑(LinearEquiv.symm (piLeft R M fun (i : ι) ↦ R ⧸ I i)) :
            ((i : ι) → (R ⧸ I i) ⊗[R] M) →ₗ[R] ((i : ι) → R ⧸ I i) ⊗[R] M) ∘ₗ
          (LinearMap.pi (φ := fun (i : ι) ↦ (R ⧸ I i) ⊗[R] M) fun (i : ι) ↦
              (TensorProduct.mk R (R ⧸ I i) M : (a : R ⧸ I i) → M →ₗ[R] (R ⧸ I i) ⊗[R] M) 1) ∘ₗ
            (↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M)) :
      (a : R ⊗[R] M) → ((i : ι) → R ⧸ I i) ⊗[R] M)

Tactic:
classical rw [pi_mkQ_rTensor] at this

Premises used: Ideal.pi_mkQ_rTensor