awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.Pure
inst_2 : J.Pure
h : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R))
s : Set (PrimeSpectrum R)
hs : zeroLocus (↑I : Set R) = s
t : Set (PrimeSpectrum R)
ht : zeroLocus (↑J : Set R) = t
⊢ s = t
have rw : zeroLocus (↑I : Set R) = t
Tactic: rw [← hs, ← ht, h]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.Pure
inst_2 : J.Pure
h : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R))
s : Set (PrimeSpectrum R)
hs : zeroLocus (↑I : Set R) = s
t : Set (PrimeSpectrum R)
ht : zeroLocus (↑J : Set R) = t
rw : zeroLocus (↑I : Set R) = t
rw₁ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R))
⊢ s = t
have rw₂ : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑J : Set R)) (zeroLocus (↑J : Set R))
Tactic: rw [← hs, ← ht, h]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Pure (goal)
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
inst_1 : I.Pure
inst_2 : J.Pure
h : Eq (α := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) (zeroLocus (↑J : Set R))
s : Set (PrimeSpectrum R)
hs : zeroLocus (↑I : Set R) = s
t : Set (PrimeSpectrum R)
ht : zeroLocus (↑J : Set R) = t
⊢ Eq (α := Ideal R)
    (RingHom.ker (F := R →+* (i : (↑s : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
      (Pi.ringHom (f := fun (p : (↑s : Type u_1)) ↦ Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)
        fun (p : (↑s : Type u_1)) ↦ algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)))
    (RingHom.ker (F := R →+* (i : (↑t : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
      (Pi.ringHom (f := fun (p : (↑t : Type u_1)) ↦ Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)
        fun (p : (↑t : Type u_1)) ↦ algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)))
have obtain : ∀ (ht : zeroLocus (↑J : Set R) = s),
  Eq (α := Ideal R)
    (RingHom.ker (F := R →+* (i : (↑s : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
      (Pi.ringHom (f := fun (p : (↑s : Type u_1)) ↦ Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)
        fun (p : (↑s : Type u_1)) ↦ algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)))
    (RingHom.ker (F := R →+* (i : (↑s : Type u_1)) → Localization.AtPrime (↑i : PrimeSpectrum R).asIdeal)
      (Pi.ringHom (f := fun (p : (↑s : Type u_1)) ↦ Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)
        fun (p : (↑s : Type u_1)) ↦ algebraMap R (Localization.AtPrime (↑p : PrimeSpectrum R).asIdeal)))
Tactic: obtain rfl : s = t := by rw [← hs, ← ht, h]
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (goal)
Goal:
ι : Type u_1
R : Type u_3
inst : Ring R
f : ι → R
inst_1 : IsTwoSided (span (range f))
i : ι
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (span (range f)))
    ((mk (span (range f)) : (a : R) → R ⧸ span (range f)) (f i) :
      HasQuotient.Quotient R (B := Ideal R) (span (range f)))
    (0 : HasQuotient.Quotient R (B := Ideal R) (span (range f)))
have rw : Membership.mem (γ := Ideal R) (span (range f)) (f i)
Tactic: rw [Ideal.Quotient.eq_zero_iff_mem]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (goal)
Goal:
R : Type u_5
inst : CommRing R
x y : R
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {x}))
      ((mk (span {x}) : (a : R) → R ⧸ span {x}) y : HasQuotient.Quotient R (B := Ideal R) (span {x}))
      (0 : HasQuotient.Quotient R (B := Ideal R) (span {x})) ↔
    x ∣ y
have rw : Membership.mem (γ := Ideal R) (span {x}) y ↔ x ∣ y
Tactic: rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (goal)
Goal:
R : Type u_5
inst : CommRing R
x y : R
rw : Membership.mem (γ := Ideal R) (span {x}) y ↔ x ∣ y
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {x}))
      ((mk (span {x}) : (a : R) → R ⧸ span {x}) y : HasQuotient.Quotient R (B := Ideal R) (span {x}))
      (0 : HasQuotient.Quotient R (B := Ideal R) (span {x})) ↔
    x ∣ y
have rw₁ : x ∣ y ↔ x ∣ y
Tactic: rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (goal)
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
⊢ IsDomain.{u_3} (R ⧸ I) ↔ I.IsPrime
have refine_1 : ∀ (H : IsDomain.{u_3} (R ⧸ I)), Ne.{u_3 + 1} (α := R ⧸ I) 0 1
Tactic: refine ⟨fun H => ⟨zero_ne_one_iff.1 ?_, fun {x y} h => ?_⟩, fun h => inferInstance⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (goal)
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
refine_1 : ∀ (H : IsDomain.{u_3} (R ⧸ I)), Ne.{u_3 + 1} (α := R ⧸ I) 0 1
⊢ IsDomain.{u_3} (R ⧸ I) ↔ I.IsPrime
have refine_2 : ∀ (H : IsDomain.{u_3} (R ⧸ I)) {x y : R} (h : x * y ∈ I), x ∈ I ∨ y ∈ I
Tactic: refine ⟨fun H => ⟨zero_ne_one_iff.1 ?_, fun {x y} h => ?_⟩, fun h => inferInstance⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (hypothesis)
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
H : IsDomain.{u_3} (R ⧸ I)
⊢ Ne.{u_3 + 1} (α := R ⧸ I) 0 1
have this : Nontrivial.{u_3} (R ⧸ I)
Tactic: haveI : Nontrivial (R ⧸ I) := ⟨H.2.1⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (goal)
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
H : IsDomain.{u_3} (R ⧸ I)
x y : R
h : x * y ∈ I
⊢ x ∈ I ∨ y ∈ I
have refine_2 : ∀
  (h :
    HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I) = 0),
  Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) (0 : R ⧸ I) ∨
    Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I) (0 : R ⧸ I)
Tactic: simp only [← eq_zero_iff_mem, (mk I).map_mul] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (hypothesis)
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
H : IsDomain.{u_3} (R ⧸ I)
x y : R
h : HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I) = 0
⊢ Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I) (0 : R ⧸ I) ∨
    Eq (α := R ⧸ I) ((mk I : (a : R) → R ⧸ I) y : R ⧸ I) (0 : R ⧸ I)
have this : NoZeroDivisors.{u_3} (R ⧸ I)
Tactic: haveI := @IsDomain.to_noZeroDivisors (R ⧸ I) _ H
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (goal)
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
hI : I.IsMaximal
⊢ ∀ {a : R ⧸ I}, a ≠ 0 → ∃ (b : R ⧸ I), a * b = 1
have h : ∀ (a : R ⧸ I), a ≠ 0 → ∃ (b : R ⧸ I), b * a = 1
Tactic: apply exists_right_inv_of_exists_left_inv
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (goal)
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
hI : I.IsMaximal
a_1 : R ⧸ I
a : R
h : Ne (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a) 0
⊢ ∃ (b : R ⧸ I), b * Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a = 1
have h₁ : ∀ (b c : R) (hc : c ∈ I) (abc : b * a + c = 1),
  ∃ (b : R ⧸ I), b * Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a = 1
Tactic: rcases hI.exists_inv (mt eq_zero_iff_mem.2 h) with ⟨b, c, hc, abc⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (goal)
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
hI : I.IsMaximal
a_1 : R ⧸ I
a : R
h : Ne (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a) 0
b c : R
hc : c ∈ I
abc : b * a + c = 1
⊢ ∃ (b : R ⧸ I), b * Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a = 1
have h₁ : ((Quotient.ringCon I).toSetoid : R → R → Prop) ((fun (x1 x2 : R) ↦ x1 * x2) b a) 1
Tactic: refine ⟨mk _ b, Quot.sound ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (goal)
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
hI : I.IsMaximal
a_1 : R ⧸ I
a : R
h : Ne (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a) 0
b c : R
hc : c ∈ I
abc : b * a + c = 1
⊢ ((Quotient.ringCon I).toSetoid : R → R → Prop) ((fun (x1 x2 : R) ↦ x1 * x2) b a) 1
have h₁ : b * a - 1 ∈ I
Tactic: simp only [Submodule.quotientRel_def]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (hypothesis)
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
hI : I.IsMaximal
a_1 : R ⧸ I
a : R
h : Ne (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a) 0
b c : R
hc : c ∈ I
abc : b * a + c = 1
⊢ b * a - 1 ∈ I
have abc₁ : c = 1 - b * a
Tactic: rw [← eq_sub_iff_add_eq'] at abc
Cleared hypotheses: abc
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (goal)
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
hI : I.IsMaximal
a_1 : R ⧸ I
a : R
h : Ne (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a) 0
b c : R
hc : c ∈ I
abc : c = 1 - b * a
⊢ b * a - 1 ∈ I
have h₁ : ∀ (hc : 1 - b * a ∈ I) (abc : c = 1 - b * a), b * a - 1 ∈ I
Tactic: rwa [abc, ← neg_mem_iff (G := R) (H := I), neg_sub] at hc
Cleared hypotheses: hc, abc
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (goal)
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
hI : I.IsMaximal
a_1 : R ⧸ I
a : R
h : Ne (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a) 0
b c : R
hc : c ∈ I
abc : c = 1 - b * a
h₁ : ∀ (hc : 1 - b * a ∈ I) (abc : c = 1 - b * a), b * a - 1 ∈ I
⊢ b * a - 1 ∈ I
have h₂ : ∀ (hc : -(1 - b * a) ∈ I) (abc : c = 1 - b * a), b * a - 1 ∈ I
Tactic: rwa [abc, ← neg_mem_iff (G := R) (H := I), neg_sub] at hc
Cleared hypotheses: hc, abc
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (goal)
Goal:
R : Type u_3
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
hI : I.IsMaximal
a_1 : R ⧸ I
a : R
h : Ne (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) a) 0
b c : R
hc : c ∈ I
abc : c = 1 - b * a
h₁ : ∀ (hc : 1 - b * a ∈ I) (abc : c = 1 - b * a), b * a - 1 ∈ I
h₂ : ∀ (hc : -(1 - b * a) ∈ I) (abc : c = 1 - b * a), b * a - 1 ∈ I
⊢ b * a - 1 ∈ I
have h₃ : ∀ (hc : b * a - 1 ∈ I) (abc : c = 1 - b * a), b * a - 1 ∈ I
Tactic: rwa [abc, ← neg_mem_iff (G := R) (H := I), neg_sub] at hc
Cleared hypotheses: hc, abc
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (goal)
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 x y : R
inst_1 : I.IsTwoSided
hI : I.IsMaximal
a : R ⧸ I
ha : a ≠ 0
⊢ (a * if ha : a = 0 then 0 else choose (p := fun (x : R ⧸ I) ↦ a * x = 1) ⋯) = 1
have rw : a * choose (p := fun (x : R ⧸ I) ↦ a * x = 1) sorry = 1
Tactic: rw [dif_neg ha]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (goal)
Goal:
R : Type u_5
inst : CommRing R
I : Ideal R
hqf : IsField.{u_5} (R ⧸ I)
⊢ I.IsMaximal
have apply : 1 ∉ I ∧ ∀ (J : Ideal R) (x : R), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
Tactic: apply Ideal.isMaximal_iff.2
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (goal)
Goal:
R : Type u_5
inst : CommRing R
I : Ideal R
hqf : IsField.{u_5} (R ⧸ I)
⊢ 1 ∉ I ∧ ∀ (J : Ideal R) (x : R), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
have left : 1 ∉ I
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (goal)
Goal:
R : Type u_5
inst : CommRing R
I : Ideal R
hqf : IsField.{u_5} (R ⧸ I)
left : 1 ∉ I
⊢ 1 ∉ I ∧ ∀ (J : Ideal R) (x : R), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
have right : ∀ (J : Ideal R) (x : R), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (goal)
Goal:
R : Type u_5
inst : CommRing R
I : Ideal R
hqf : IsField.{u_5} (R ⧸ I)
h : 1 ∈ I
⊢ False
have left : ∀ (w : R ⧸ I) (x : R) (w : R ⧸ I) (y : R)
  (hxy :
    Ne (α := R ⧸ I) (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) x)
      (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) y)),
  False
Tactic: rcases hqf.exists_pair_ne with ⟨⟨x⟩, ⟨y⟩, hxy⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (goal)
Goal:
R : Type u_5
inst : CommRing R
I : Ideal R
hqf : IsField.{u_5} (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
hxnI : x ∉ I
hxJ : x ∈ J
⊢ 1 ∈ J
have right : ∀ (w : R ⧸ I) (y : R)
  (hy :
    HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I)
        (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) y) =
      1),
  1 ∈ J
Tactic: rcases hqf.mul_inv_cancel (mt Ideal.Quotient.eq_zero_iff_mem.1 hxnI) with ⟨⟨y⟩, hy⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (goal)
Goal:
R : Type u_5
inst : CommRing R
I : Ideal R
hqf : IsField.{u_5} (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
hxnI : x ∉ I
hxJ : x ∈ J
w : R ⧸ I
y : R
hy :
  HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((mk I : (a : R) → R ⧸ I) x : R ⧸ I)
      (Quot.mk (⇑(Submodule.quotientRel I) : R → R → Prop) y) =
    1
⊢ 1 ∈ J
have right : x * y - (x * y - 1) ∈ J
Tactic: rw [← zero_add (1 : R), ← sub_self (x * y), sub_add]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (goal)
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
c : R ⧸ I
m : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
c₁ : R
m₁ : (i : ι) → R
c₂ : R
m₂ : (i : ι) → R
hc : (Submodule.quotientRel I : R → R → Prop) c₁ c₂
hm : (Submodule.quotientRel (pi fun (x : ι) ↦ I) : ((i : ι) → R) → ((i : ι) → R) → Prop) m₁ m₂
⊢ Eq (α := HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I))
    ((fun (r : R) (m : (i : ι) → R) ↦
        (Submodule.Quotient.mk (r • m) :
          HasQuotient.Quotient (ι → R) (B := Submodule ((i : ι) → R) (ι → R))
            (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)))
      c₁ m₁)
    ((fun (r : R) (m : (i : ι) → R) ↦
        (Submodule.Quotient.mk (r • m) :
          HasQuotient.Quotient (ι → R) (B := Submodule ((i : ι) → R) (ι → R))
            (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)))
      c₂ m₂)
have apply : Membership.mem (γ := Ideal (ι → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I) (c₁ • m₁ - c₂ • m₂)
Tactic: apply Ideal.Quotient.eq.2
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (hypothesis)
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
c : R ⧸ I
m : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
c₁ : R
m₁ : (i : ι) → R
c₂ : R
m₂ : (i : ι) → R
hc : (Submodule.quotientRel I : R → R → Prop) c₁ c₂
hm : (Submodule.quotientRel (pi fun (x : ι) ↦ I) : ((i : ι) → R) → ((i : ι) → R) → Prop) m₁ m₂
⊢ Membership.mem (γ := Ideal (ι → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I) (c₁ • m₁ - c₂ • m₂)
have hc₁ : c₁ - c₂ ∈ I
Tactic: rw [Submodule.quotientRel_def] at hc hm
Cleared hypotheses: hc, hm
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (hypothesis)
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
c : R ⧸ I
m : HasQuotient.Quotient (ι → R) (B := Ideal ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I)
c₁ : R
m₁ : (i : ι) → R
c₂ : R
m₂ : (i : ι) → R
hc : (Submodule.quotientRel I : R → R → Prop) c₁ c₂
hm : (Submodule.quotientRel (pi fun (x : ι) ↦ I) : ((i : ι) → R) → ((i : ι) → R) → Prop) m₁ m₂
hc₁ : c₁ - c₂ ∈ I
⊢ Membership.mem (γ := Ideal (ι → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I) (c₁ • m₁ - c₂ • m₂)
have hm₁ : Membership.mem (γ := Submodule ((i : ι) → R) ((i : ι) → R)) (pi (R := fun (x : ι) ↦ R) fun (x : ι) ↦ I) (m₁ - m₂)
Tactic: rw [Submodule.quotientRel_def] at hc hm
Cleared hypotheses: hc, hm
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (goal)
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 : ι'
⊢ Membership.mem (α := R) I ((f : (a : ι → R) → ι' → R) x i : R)
have intro : ∀ (val : Fintype ι), Membership.mem (α := R) I ((f : (a : ι → R) → ι' → R) x i : R)
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (goal)
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 ι
⊢ Membership.mem (α := R) I ((f : (a : ι → R) → ι' → R) x i : R)
have 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)
Tactic: rw [pi_eq_sum_univ x]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (goal)
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 ι
⊢ 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)
have 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
Tactic: simp only [Finset.sum_apply, smul_eq_mul, map_sum, Pi.smul_apply, map_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (goal)
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 : ι'
⊢ Membership.mem (α := R) I ((f : (a : ι → R) → ι' → R) x i : R)
have intro : ∀ (val : Fintype ι), 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)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (goal)
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)
have 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)
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)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (goal)
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)
⊢ Membership.mem (α := R) I ((f : (a : ι → R) → ι' → R) x i : R)
have 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
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)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Basic (goal)
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 R
have rw : Finite.{u_3 + 1} ↥I ∧ Finite.{u_3 + 1} (R ⧸ I)
Tactic: rw [finite_iff_ideal_quotient]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder (goal)
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 ι
⊢ 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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder (hypothesis)
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 (α := M) (β := (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) :
      (a : M) → (i : ι) → (R ⧸ I i) ⊗[R] M)
have 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)
Tactic: have := rTensor_surjective M (pi_mkQ_surjective hI)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder (hypothesis)
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 (α := M) (β := (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) :
      (a : M) → (i : ι) → (R ⧸ I i) ⊗[R] M)
have this₁ : 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
Cleared hypotheses: this