awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Nilpotent (goal)
Goal:
S : Type u_1
inst : CommRing S
I : Ideal S
inst_1 : I.IsMaximal
n : ℕ
x : S
hx : x ∉ I
hn : n = 0
⊢ IsUnit (M := S ⧸ I ^ n) ((mk (I ^ n) : (a : S) → S ⧸ I ^ n) x : S ⧸ I ^ n)
have pos : IsUnit (M := HasQuotient.Quotient S (B := Ideal S) ⊤)
  ((mk ⊤ : (a : S) → S ⧸ ⊤) x : HasQuotient.Quotient S (B := Ideal S) ⊤)
Tactic: rw [pow_eq_top_iff.mpr (Or.inr hn)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, Eq.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
hI : ker f ≤ I
⊢ Function.Injective.{u + 1, v + 1} (α := R ⧸ I) (β := S) (⇑(Ideal.Quotient.lift I f H) : (a : R ⧸ I) → S)
have rw : ∀ (x : R ⧸ I), Eq.{v + 1} (α := S) ((Ideal.Quotient.lift I f H : (a : R ⧸ I) → S) x : S) (0 : S) → x = 0
Tactic: rw [RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_bot_iff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, Eq.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
hI : ker f ≤ I
u : R ⧸ I
hu : Eq.{v + 1} (α := S) ((Ideal.Quotient.lift I f H : (a : R ⧸ I) → S) u : S) (0 : S)
⊢ u = 0
have obtain : ∀ (v : R)
  (hu :
    Eq.{v + 1} (α := S)
      ((Ideal.Quotient.lift I f H : (a : R ⧸ I) → S) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) v : R ⧸ I) : S) (0 : S)),
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) v : R ⧸ I) (0 : R ⧸ I)
Tactic: obtain ⟨v, rfl⟩ := Ideal.Quotient.mk_surjective u
Cleared hypotheses: u, hu
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (hypothesis)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, Eq.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
hI : ker f ≤ I
v : R
hu :
  Eq.{v + 1} (α := S)
    ((Ideal.Quotient.lift I f H : (a : R ⧸ I) → S) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) v : R ⧸ I) : S) (0 : S)
⊢ Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) v : R ⧸ I) (0 : R ⧸ I)
have hu₁ : Eq.{v + 1} (α := S) ((f : (a : R) → S) v : S) (0 : S)
Tactic: rw [Ideal.Quotient.lift_mk] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, Eq.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
hI : ker f ≤ I
v : R
hu : Eq.{v + 1} (α := S) ((f : (a : R) → S) v : S) (0 : S)
⊢ Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) v : R ⧸ I) (0 : R ⧸ I)
have rw : v ∈ I
Tactic: rw [Ideal.Quotient.eq_zero_iff_mem]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
f : R →+* S
g : S → R
hf : Function.RightInverse g (⇑f : (a : R) → S)
x_1 : HasQuotient.Quotient R (B := Ideal R) (ker f)
x : R
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (ker f))
    (((⇑(Ideal.Quotient.mk (ker f)) : (a : R) → R ⧸ ker f) ∘ g)
      ((f.kerLift : (a : R ⧸ ker f) → S) (Quot.mk (⇑(Submodule.quotientRel (ker f)) : R → R → Prop) x)))
    (Quot.mk (⇑(Submodule.quotientRel (ker f)) : R → R → Prop) x)
have mk : Eq.{v + 1} (α := S)
  ((f.kerLift : (a : R ⧸ ker f) → S)
      (((⇑(Ideal.Quotient.mk (ker f)) : (a : R) → R ⧸ ker f) ∘ g)
        ((f.kerLift : (a : R ⧸ ker f) → S) (Quot.mk (⇑(Submodule.quotientRel (ker f)) : R → R → Prop) x))) :
    S)
  ((f.kerLift : (a : R ⧸ ker f) → S) (Quot.mk (⇑(Submodule.quotientRel (ker f)) : R → R → Prop) x) : S)
Tactic: apply kerLift_injective
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x : R
⊢ Eq.{u + 1} (α := HasQuotient.Quotient R (B := Ideal R) (ker f))
    (((quotientKerEquivOfSurjective hf).symm : (a : S) → R ⧸ ker f) ((f : (a : R) → S) x) :
      HasQuotient.Quotient R (B := Ideal R) (ker f))
    ((Ideal.Quotient.mk (ker f) : (a : R) → R ⧸ ker f) x : HasQuotient.Quotient R (B := Ideal R) (ker f))
have a : Eq.{v + 1} (α := S)
  ((quotientKerEquivOfSurjective hf : (a : R ⧸ ker f) → S)
      (((quotientKerEquivOfSurjective hf).symm : (a : S) → R ⧸ ker f) ((f : (a : R) → S) x) :
        HasQuotient.Quotient R (B := Ideal R) (ker f)) :
    S)
  ((quotientKerEquivOfSurjective hf : (a : R ⧸ ker f) → S)
      ((Ideal.Quotient.mk (ker f) : (a : R) → R ⧸ ker f) x : HasQuotient.Quotient R (B := Ideal R) (ker f)) :
    S)
Tactic: apply (RingHom.quotientKerEquivOfSurjective hf).injective
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ (quotientKerEquivOfSurjective hf).symm.toRingHom.comp f = Ideal.Quotient.mk (ker f)
have a : ∀ (x : R),
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (ker f))
    (((quotientKerEquivOfSurjective hf).symm.toRingHom.comp f : (a : R) → R ⧸ ker f) x :
      HasQuotient.Quotient R (B := Ideal R) (ker f))
    ((Ideal.Quotient.mk (ker f) : (a : R) → R ⧸ ker f) x : HasQuotient.Quotient R (B := Ideal R) (ker f))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
⊢ ker (F := R →+* R ⧸ I) (Quotient.mk I) = I
have h : ∀ (x : R), Membership.mem (γ := Ideal R) (ker (F := R →+* R ⧸ I) (Quotient.mk I)) x ↔ x ∈ I
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
x : R
⊢ Membership.mem (γ := Ideal R) (ker (F := R →+* R ⧸ I) (Quotient.mk I)) x ↔ x ∈ I
have h : Membership.mem (γ := Ideal R) (comap (F := R →+* R ⧸ I) (Quotient.mk I) ⊥) x ↔ x ∈ I
Tactic: rw [ker, mem_comap, Submodule.mem_bot, Quotient.eq_zero_iff_mem]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
x : R
h : Membership.mem (γ := Ideal R) (comap (F := R →+* R ⧸ I) (Quotient.mk I) ⊥) x ↔ x ∈ I
⊢ Membership.mem (γ := Ideal R) (ker (F := R →+* R ⧸ I) (Quotient.mk I)) x ↔ x ∈ I
have h₁ : Membership.mem (α := R ⧸ I) (γ := Ideal (R ⧸ I)) ⊥ ((Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) ↔ x ∈ I
Tactic: rw [ker, mem_comap, Submodule.mem_bot, Quotient.eq_zero_iff_mem]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
x : R
h : Membership.mem (γ := Ideal R) (comap (F := R →+* R ⧸ I) (Quotient.mk I) ⊥) x ↔ x ∈ I
h₁ : Membership.mem (α := R ⧸ I) (γ := Ideal (R ⧸ I)) ⊥ ((Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) ↔ x ∈ I
⊢ Membership.mem (γ := Ideal R) (ker (F := R →+* R ⧸ I) (Quotient.mk I)) x ↔ x ∈ I
have h₂ : Eq (α := R ⧸ I) ((Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) (0 : R ⧸ I) ↔ x ∈ I
Tactic: rw [ker, mem_comap, Submodule.mem_bot, Quotient.eq_zero_iff_mem]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
x : R
h : Membership.mem (γ := Ideal R) (comap (F := R →+* R ⧸ I) (Quotient.mk I) ⊥) x ↔ x ∈ I
h₁ : Membership.mem (α := R ⧸ I) (γ := Ideal (R ⧸ I)) ⊥ ((Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) ↔ x ∈ I
h₂ : Eq (α := R ⧸ I) ((Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) (0 : R ⧸ I) ↔ x ∈ I
⊢ Membership.mem (γ := Ideal R) (ker (F := R →+* R ⧸ I) (Quotient.mk I)) x ↔ x ∈ I
have h₃ : x ∈ I ↔ x ∈ I
Tactic: rw [ker, mem_comap, Submodule.mem_bot, Quotient.eq_zero_iff_mem]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
⊢ Eq (α := Ideal (R ⧸ I)) (ker (F := RingHom.{u, v} (R ⧸ I) S) (Quotient.lift I f H))
    (map (F := R →+* R ⧸ I) (Quotient.mk I) (ker f))
have h : ∀ (x : R ⧸ I),
  Membership.mem (γ := Ideal (R ⧸ I)) (ker (F := RingHom.{u, v} (R ⧸ I) S) (Quotient.lift I f H)) x ↔
    Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) (ker f)) x
Tactic: apply Ideal.ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
⊢ Membership.mem (γ := Ideal (R ⧸ I)) (ker (F := RingHom.{u, v} (R ⧸ I) S) (Quotient.lift I f H)) x ↔
    Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) (ker f)) x
have h : Membership.mem (γ := Ideal (R ⧸ I)) (ker (F := RingHom.{u, v} (R ⧸ I) S) (Quotient.lift I f H)) x →
  Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) (ker f)) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
h :
  Membership.mem (γ := Ideal (R ⧸ I)) (ker (F := RingHom.{u, v} (R ⧸ I) S) (Quotient.lift I f H)) x →
    Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) (ker f)) x
⊢ Membership.mem (γ := Ideal (R ⧸ I)) (ker (F := RingHom.{u, v} (R ⧸ I) S) (Quotient.lift I f H)) x ↔
    Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) (ker f)) x
have h₁ : Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) (ker f)) x →
  Membership.mem (γ := Ideal (R ⧸ I)) (ker (F := RingHom.{u, v} (R ⧸ I) S) (Quotient.lift I f H)) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
hx : Membership.mem (γ := Ideal (R ⧸ I)) (ker (F := RingHom.{u, v} (R ⧸ I) S) (Quotient.lift I f H)) x
⊢ Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) (ker f)) x
have h : ∀ (y : R) (hy : (Quotient.mk I : (a : R) → R ⧸ I) y = x),
  Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) (ker f)) x
Tactic: obtain ⟨y, hy⟩ := Quotient.mk_surjective x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
hx : Membership.mem (γ := Ideal (R ⧸ I)) (ker (F := RingHom.{u, v} (R ⧸ I) S) (Quotient.lift I f H)) x
y : R
hy : (Quotient.mk I : (a : R) → R ⧸ I) y = x
⊢ Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) (ker f)) x
have h : ∀ (y : R) (hx : Membership.mem (γ := Ideal R) (ker f) y) (hy : (Quotient.mk I : (a : R) → R ⧸ I) y = x),
  Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) (ker f)) x
Tactic: rw [mem_ker, ← hy, Ideal.Quotient.lift_mk, ← mem_ker] at hx
Cleared hypotheses: hx, y, hy
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
y : R
hx : Membership.mem (γ := Ideal R) (ker f) y
hy : (Quotient.mk I : (a : R) → R ⧸ I) y = x
⊢ Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) (ker f)) x
have h : ∃ (x : R),
  Membership.mem (γ := Ideal R) (ker f) x ∧
    Eq (α := R ⧸ I) ((Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) ((Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
Tactic: rw [← hy, mem_map_iff_of_surjective (Quotient.mk I) Quotient.mk_surjective]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (hypothesis)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
hx : Membership.mem (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) (ker f)) x
⊢ Membership.mem (γ := Ideal (R ⧸ I)) (ker (F := RingHom.{u, v} (R ⧸ I) S) (Quotient.lift I f H)) x
have hx₁ : ∃ (x_1 : R), Membership.mem (γ := Ideal R) (ker f) x_1 ∧ (Quotient.mk I : (a : R) → R ⧸ I) x_1 = x
Tactic: rw [mem_map_iff_of_surjective (Quotient.mk I) Quotient.mk_surjective] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
hx : ∃ (x_1 : R), Membership.mem (γ := Ideal R) (ker f) x_1 ∧ (Quotient.mk I : (a : R) → R ⧸ I) x_1 = x
⊢ Membership.mem (γ := Ideal (R ⧸ I)) (ker (F := RingHom.{u, v} (R ⧸ I) S) (Quotient.lift I f H)) x
have h : ∀ (y : R) (hy : Membership.mem (γ := Ideal R) (ker f) y ∧ (Quotient.mk I : (a : R) → R ⧸ I) y = x),
  Membership.mem (γ := Ideal (R ⧸ I)) (ker (F := RingHom.{u, v} (R ⧸ I) S) (Quotient.lift I f H)) x
Tactic: obtain ⟨y, hy⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : I ≤ ker f
x : R ⧸ I
y : R
hy : Membership.mem (γ := Ideal R) (ker f) y ∧ (Quotient.mk I : (a : R) → R ⧸ I) y = x
⊢ Membership.mem (γ := Ideal (R ⧸ I)) (ker (F := RingHom.{u, v} (R ⧸ I) S) (Quotient.lift I f H)) x
have h : Eq.{v + 1} (α := S) ((f : (a : R) → S) y : S) (0 : S)
Tactic: rw [mem_ker, ← hy.right, Ideal.Quotient.lift_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, Eq.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
⊢ Injective.{u + 1, v + 1} (α := R ⧸ I) (β := S) (⇑(Quotient.lift I f H) : (a : R ⧸ I) → S) ↔ ker f = I
have rw : ker f ≤ I ↔ ker f = I
Tactic: rw [injective_iff_ker_eq_bot, ker_quotient_lift, map_eq_bot_iff_le_ker, mk_ker]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, Eq.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
⊢ ker f ≤ I ↔ ker f = I
have mp : ker f ≤ I → ker f = I
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Semiring S
I : Ideal R
inst_2 : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, Eq.{v + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S)
mp : ker f ≤ I → ker f = I
⊢ ker f ≤ I ↔ ker f = I
have mpr : ker f = I → ker f ≤ I
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : I.IsTwoSided
x : R
⊢ Membership.mem (α := R ⧸ I) (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J)
      ((Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) ↔
    x ∈ J ⊔ I
have rw : Membership.mem (γ := Ideal R) (comap (F := R →+* R ⧸ I) (Quotient.mk I) (map (F := R →+* R ⧸ I) (Quotient.mk I) J)) x ↔
  x ∈ J ⊔ I
Tactic: rw [← mem_comap, comap_map_of_surjective (Quotient.mk I) Quotient.mk_surjective, ←
    ker_eq_comap_bot, mk_ker]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : I.IsTwoSided
x : R
rw :
  Membership.mem (γ := Ideal R) (comap (F := R →+* R ⧸ I) (Quotient.mk I) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
      x ↔
    x ∈ J ⊔ I
⊢ Membership.mem (α := R ⧸ I) (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J)
      ((Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) ↔
    x ∈ J ⊔ I
have rw₁ : x ∈ J ⊔ comap (F := R →+* R ⧸ I) (Quotient.mk I) ⊥ ↔ x ∈ J ⊔ I
Tactic: rw [← mem_comap, comap_map_of_surjective (Quotient.mk I) Quotient.mk_surjective, ←
    ker_eq_comap_bot, mk_ker]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : I.IsTwoSided
x : R
rw :
  Membership.mem (γ := Ideal R) (comap (F := R →+* R ⧸ I) (Quotient.mk I) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
      x ↔
    x ∈ J ⊔ I
rw₁ : x ∈ J ⊔ comap (F := R →+* R ⧸ I) (Quotient.mk I) ⊥ ↔ x ∈ J ⊔ I
⊢ Membership.mem (α := R ⧸ I) (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J)
      ((Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) ↔
    x ∈ J ⊔ I
have rw₂ : x ∈ J ⊔ ker (F := R →+* R ⧸ I) (Quotient.mk I) ↔ x ∈ J ⊔ I
Tactic: rw [← mem_comap, comap_map_of_surjective (Quotient.mk I) Quotient.mk_surjective, ←
    ker_eq_comap_bot, mk_ker]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : I.IsTwoSided
x : R
rw :
  Membership.mem (γ := Ideal R) (comap (F := R →+* R ⧸ I) (Quotient.mk I) (map (F := R →+* R ⧸ I) (Quotient.mk I) J))
      x ↔
    x ∈ J ⊔ I
rw₁ : x ∈ J ⊔ comap (F := R →+* R ⧸ I) (Quotient.mk I) ⊥ ↔ x ∈ J ⊔ I
rw₂ : x ∈ J ⊔ ker (F := R →+* R ⧸ I) (Quotient.mk I) ↔ x ∈ J ⊔ I
⊢ Membership.mem (α := R ⧸ I) (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J)
      ((Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) ↔
    x ∈ J ⊔ I
have rw₃ : x ∈ J ⊔ I ↔ x ∈ J ⊔ I
Tactic: rw [← mem_comap, comap_map_of_surjective (Quotient.mk I) Quotient.mk_surjective, ←
    ker_eq_comap_bot, mk_ker]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : I.IsTwoSided
hIJ : I ≤ J
x : R
⊢ Membership.mem (α := R ⧸ I) (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J)
      ((Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) ↔
    x ∈ J
have rw : x ∈ J ⊔ I ↔ x ∈ J
Tactic: rw [mem_quotient_iff_mem_sup, sup_eq_left.mpr hIJ]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
inst : Ring R
I J : Ideal R
inst_1 : I.IsTwoSided
hIJ : I ≤ J
x : R
rw : x ∈ J ⊔ I ↔ x ∈ J
⊢ Membership.mem (α := R ⧸ I) (γ := Ideal (R ⧸ I)) (map (F := R →+* R ⧸ I) (Quotient.mk I) J)
      ((Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) ↔
    x ∈ J
have rw₁ : x ∈ J ↔ x ∈ J
Tactic: rw [mem_quotient_iff_mem_sup, sup_eq_left.mpr hIJ]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
inst : Ring R
ι : Type u_1
I : ι → Ideal R
inst_1 : ∀ (i : ι), (I i).IsTwoSided
⊢ Injective (α := HasQuotient.Quotient R (B := Ideal R) (⨅ (i : ι), I i)) (β := (i : ι) → R ⧸ I i)
    (⇑(quotientInfToPiQuotient I) : (a : R ⧸ ⨅ (i : ι), I i) → (i : ι) → R ⧸ I i)
have rw : Injective (α := HasQuotient.Quotient R (B := Ideal R) (⨅ (i : ι), I i)) (β := (i : ι) → R ⧸ I i)
  (⇑(lift (⨅ (i : ι), I i) (Pi.ringHom (f := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Quotient.mk (I i)) sorry :
        HasQuotient.Quotient R (B := Ideal R) (⨅ (i : ι), I i) →+* (i : ι) → R ⧸ I i) :
    (a : R ⧸ ⨅ (i : ι), I i) → (i : ι) → R ⧸ I i)
Tactic: rw [quotientInfToPiQuotient, injective_lift_iff, ker_Pi_Quotient_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
inst : Ring R
ι : Type u_1
I : ι → Ideal R
inst_1 : ∀ (i : ι), (I i).IsTwoSided
rw :
  Injective (α := HasQuotient.Quotient R (B := Ideal R) (⨅ (i : ι), I i)) (β := (i : ι) → R ⧸ I i)
    (⇑(lift (⨅ (i : ι), I i) (Pi.ringHom (f := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Quotient.mk (I i)) ⋯ :
          HasQuotient.Quotient R (B := Ideal R) (⨅ (i : ι), I i) →+* (i : ι) → R ⧸ I i) :
      (a : R ⧸ ⨅ (i : ι), I i) → (i : ι) → R ⧸ I i)
⊢ Injective (α := HasQuotient.Quotient R (B := Ideal R) (⨅ (i : ι), I i)) (β := (i : ι) → R ⧸ I i)
    (⇑(quotientInfToPiQuotient I) : (a : R ⧸ ⨅ (i : ι), I i) → (i : ι) → R ⧸ I i)
have rw₁ : Eq (α := Ideal R)
  (ker (F := R →+* (i : ι) → R ⧸ I i)
    (Pi.ringHom (f := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Quotient.mk (I i) : R →+* (i : ι) → R ⧸ I i))
  (⨅ (i : ι), I i)
Tactic: rw [quotientInfToPiQuotient, injective_lift_iff, ker_Pi_Quotient_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u
inst : Ring R
ι : Type u_1
I : ι → Ideal R
inst_1 : ∀ (i : ι), (I i).IsTwoSided
rw :
  Injective (α := HasQuotient.Quotient R (B := Ideal R) (⨅ (i : ι), I i)) (β := (i : ι) → R ⧸ I i)
    (⇑(lift (⨅ (i : ι), I i) (Pi.ringHom (f := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Quotient.mk (I i)) ⋯ :
          HasQuotient.Quotient R (B := Ideal R) (⨅ (i : ι), I i) →+* (i : ι) → R ⧸ I i) :
      (a : R ⧸ ⨅ (i : ι), I i) → (i : ι) → R ⧸ I i)
rw₁ :
  Eq (α := Ideal R)
    (ker (F := R →+* (i : ι) → R ⧸ I i)
      (Pi.ringHom (f := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Quotient.mk (I i) : R →+* (i : ι) → R ⧸ I i))
    (⨅ (i : ι), I i)
⊢ Injective (α := HasQuotient.Quotient R (B := Ideal R) (⨅ (i : ι), I i)) (β := (i : ι) → R ⧸ I i)
    (⇑(quotientInfToPiQuotient I) : (a : R ⧸ ⨅ (i : ι), I i) → (i : ι) → R ⧸ I i)
have rw₂ : Eq.{u + 1} (α := Ideal R) (⨅ (i : ι), I i) (⨅ (i : ι), I i)
Tactic: rw [quotientInfToPiQuotient, injective_lift_iff, ker_Pi_Quotient_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u_2
inst : CommRing R
ι : Type u_3
inst_1 : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
⊢ Surjective (α := HasQuotient.Quotient R (B := Ideal R) (⨅ (i : ι), I i)) (β := (i : ι) → R ⧸ I i)
    (⇑(quotientInfToPiQuotient I) : (a : R ⧸ ⨅ (i : ι), I i) → (i : ι) → R ⧸ I i)
have intro : ∀ (val : Fintype ι),
  Surjective (α := HasQuotient.Quotient R (B := Ideal R) (⨅ (i : ι), I i)) (β := (i : ι) → R ⧸ I i)
    (⇑(quotientInfToPiQuotient I) : (a : R ⧸ ⨅ (i : ι), I i) → (i : ι) → R ⧸ I i)
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u_2
inst : CommRing R
ι : Type u_3
inst_1 : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val : Fintype ι
g : (i : ι) → R ⧸ I i
⊢ ∃ (a : HasQuotient.Quotient R (B := Ideal R) (⨅ (i : ι), I i)),
    (quotientInfToPiQuotient I : (a : R ⧸ ⨅ (i : ι), I i) → (i : ι) → R ⧸ I i) a = g
have intro : ∀ (f : (i : ι) → R) (hf : ∀ (i : ι), (Quotient.mk (I i) : (a : R) → R ⧸ I i) (f i) = g i),
  ∃ (a : HasQuotient.Quotient R (B := Ideal R) (⨅ (i : ι), I i)),
    (quotientInfToPiQuotient I : (a : R ⧸ ⨅ (i : ι), I i) → (i : ι) → R ⧸ I i) a = g
Tactic: choose f hf using fun i ↦ mk_surjective (g i)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (hypothesis)
Goal:
R : Type u_2
inst : CommRing R
ι : Type u_3
inst_1 : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val : Fintype ι
g : (i : ι) → R ⧸ I i
f : (i : ι) → R
hf : ∀ (i : ι), (Quotient.mk (I i) : (a : R) → R ⧸ I i) (f i) = g i
i : ι
⊢ ∃ (e : R),
    Eq (α := R ⧸ I i) ((Quotient.mk (I i) : (a : R) → R ⧸ I i) e : R ⧸ I i) (1 : R ⧸ I i) ∧
      ∀ (j : ι), j ≠ i → Eq (α := R ⧸ I j) ((Quotient.mk (I j) : (a : R) → R ⧸ I j) e : R ⧸ I j) (0 : R ⧸ I j)
have hI' : ∀ (j : ι), Membership.mem (γ := Finset ι) {i}ᶜ j → IsCoprime (I i) (I j)
Tactic: have hI' : ∀ j ∈ ({i} : Finset ι)ᶜ, IsCoprime (I i) (I j) := by
      intro j hj
      exact hI (by simpa [ne_comm, isCoprime_iff_add] using hj)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.Operations (goal)
Goal:
R : Type u_2
inst : CommRing R
ι : Type u_3
inst_1 : Finite ι
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
val : Fintype ι
g : (i : ι) → R ⧸ I i
f : (i : ι) → R
hf : ∀ (i : ι), (Quotient.mk (I i) : (a : R) → R ⧸ I i) (f i) = g i
i : ι
hI' : ∀ (j : ι), Membership.mem (γ := Finset ι) {i}ᶜ j → IsCoprime (I i) (I j)
⊢ ∃ (e : R),
    Eq (α := R ⧸ I i) ((Quotient.mk (I i) : (a : R) → R ⧸ I i) e : R ⧸ I i) (1 : R ⧸ I i) ∧
      ∀ (j : ι), j ≠ i → Eq (α := R ⧸ I j) ((Quotient.mk (I j) : (a : R) → R ⧸ I j) e : R ⧸ I j) (0 : R ⧸ I j)
have rcases : ∀ (u : R) (hu : u ∈ I i) (e : R)
  (he : Membership.mem (γ := Ideal R) (⨅ (j : ι), ⨅ (_ : Membership.mem (γ := Finset ι) {i}ᶜ j), I j) e)
  (hue : u + e = 1),
  ∃ (e : R),
    Eq (α := R ⧸ I i) ((Quotient.mk (I i) : (a : R) → R ⧸ I i) e : R ⧸ I i) (1 : R ⧸ I i) ∧
      ∀ (j : ι), j ≠ i → Eq (α := R ⧸ I j) ((Quotient.mk (I j) : (a : R) → R ⧸ I j) e : R ⧸ I j) (0 : R ⧸ I j)
Tactic: rcases isCoprime_iff_exists.mp (isCoprime_biInf hI') with ⟨u, hu, e, he, hue⟩