awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
g : { g : A →+* C // LE.le (α := Ideal A) (ker f) (ker g) }
⊢ (fun (φ : B →+* C) ↦
        (Subtype.mk (p := fun (g : A →+* C) ↦ LE.le (α := Ideal A) (ker f) (ker g)) (φ.comp f) ⋯ :
          { g : A →+* C // LE.le (α := Ideal A) (ker f) (ker g) }))
      ((fun (g : { g : A →+* C // LE.le (α := Ideal A) (ker f) (ker g) }) ↦
          f.liftOfRightInverseAux f_inv hf (↑g : A →+* C) ⋯)
        g) =
    g
have a : ∀ (x : A),
  Eq.{u_3 + 1} (α := C)
    (((↑((fun (φ : B →+* C) ↦
                  (Subtype.mk (p := fun (g : A →+* C) ↦ LE.le (α := Ideal A) (ker f) (ker g)) (φ.comp f) sorry :
                    { g : A →+* C // LE.le (α := Ideal A) (ker f) (ker g) }))
                ((fun (g : { g : A →+* C // LE.le (α := Ideal A) (ker f) (ker g) }) ↦
                    f.liftOfRightInverseAux f_inv hf (↑g : A →+* C) sorry)
                  g)) :
            A →+* C) :
          (a : A) → C)
        x :
      C)
    (((↑g : A →+* C) : (a : A) → C) x : C)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
φ : B →+* C
⊢ (fun (g : { g : A →+* C // LE.le (α := Ideal A) (ker f) (ker g) }) ↦
        f.liftOfRightInverseAux f_inv hf (↑g : A →+* C) ⋯)
      ((fun (φ : B →+* C) ↦
          (Subtype.mk (p := fun (g : A →+* C) ↦ LE.le (α := Ideal A) (ker f) (ker g)) (φ.comp f) ⋯ :
            { g : A →+* C // LE.le (α := Ideal A) (ker f) (ker g) }))
        φ) =
    φ
have a : ∀ (b : B),
  Eq.{u_3 + 1} (α := C)
    (((fun (g : { g : A →+* C // LE.le (α := Ideal A) (ker f) (ker g) }) ↦
              f.liftOfRightInverseAux f_inv hf (↑g : A →+* C) sorry)
            ((fun (φ : B →+* C) ↦
                (Subtype.mk (p := fun (g : A →+* C) ↦ LE.le (α := Ideal A) (ker f) (ker g)) (φ.comp f) sorry :
                  { g : A →+* C // LE.le (α := Ideal A) (ker f) (ker g) }))
              φ) :
          (a : B) → C)
        b :
      C)
    ((φ : (a : B) → C) b : C)
Tactic: ext b
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
g : A →+* C
hg : LE.le (α := Ideal A) (ker f) (ker g)
h : B →+* C
hh : h.comp f = g
⊢ h =
    (f.liftOfRightInverse f_inv hf : (a : { g : A →+* C // ker f ≤ ker g }) → B →+* C)
      (Subtype.mk (p := fun (g : A →+* C) ↦ LE.le (α := Ideal A) (ker f) (ker g)) g hg)
have simp_rw : h =
  (f.liftOfRightInverse f_inv hf : (a : { g : A →+* C // ker f ≤ ker g }) → B →+* C)
    (Subtype.mk (p := fun (g : A →+* C) ↦ LE.le (α := Ideal A) (ker f) (ker g)) (h.comp f) sorry)
Tactic: simp_rw [← hh]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Semiring S
inst_2 : Algebra R S
I : Ideal R
x y : ↥I
⊢ ((idealMap S I : LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id R) ↥I ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)) :
        (a : ↥I) → ↥(Ideal.map (algebraMap R S) I))
      (x * y) =
    HMul.hMul (α := ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)) (β :=
      ↥(Ideal.map (F := R →+* S) (algebraMap R S) I))
      (((idealMap S I :
              LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id R) ↥I ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)) :
            (a : ↥I) → ↥(Ideal.map (algebraMap R S) I))
          x :
        ↥(Ideal.map (F := R →+* S) (algebraMap R S) I))
      (((idealMap S I :
              LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id R) ↥I ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)) :
            (a : ↥I) → ↥(Ideal.map (algebraMap R S) I))
          y :
        ↥(Ideal.map (F := R →+* S) (algebraMap R S) I))
have a : (↑(((idealMap S I : LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id R) ↥I ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)) :
          (a : ↥I) → ↥(Ideal.map (algebraMap R S) I))
        (x * y)) :
    S) =
  (↑(HMul.hMul (α := ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)) (β :=
        ↥(Ideal.map (F := R →+* S) (algebraMap R S) I))
        (((idealMap S I :
                LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id R) ↥I ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)) :
              (a : ↥I) → ↥(Ideal.map (algebraMap R S) I))
            x :
          ↥(Ideal.map (F := R →+* S) (algebraMap R S) I))
        (((idealMap S I :
                LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id R) ↥I ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)) :
              (a : ↥I) → ↥(Ideal.map (algebraMap R S) I))
            y :
          ↥(Ideal.map (F := R →+* S) (algebraMap R S) I))) :
    S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
⊢ Eq (α := Ideal R) (RingHom.ker (F := R →+* A) (algebraMap R A)) ⊥
have h : ∀ (x : R),
  Membership.mem (γ := Ideal R) (RingHom.ker (F := R →+* A) (algebraMap R A)) x ↔ Membership.mem (γ := Ideal R) ⊥ x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
I : Ideal R
inst_2 : Submodule.IsPrincipal I
⊢ Submodule.IsPrincipal.{u_2, u_2} (R := S) (Ideal.map f I)
have obtain : ∀ (x : R) [Submodule.IsPrincipal (M := R) (R ∙ x)], Submodule.IsPrincipal.{u_2, u_2} (R := S) (Ideal.map f (R ∙ x))
Tactic: obtain ⟨x, rfl⟩ := Submodule.IsPrincipal.principal I
Cleared hypotheses: I, inst_2
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : R
inst_2 : Submodule.IsPrincipal (M := R) (R ∙ x)
⊢ Eq (α := Submodule S S) (Ideal.map f (R ∙ x)) (Submodule.span S (singleton (α := S) ((f : (a : R) → S) x : S)))
have rw : Eq (α := Submodule S S) (Ideal.map (R := R) f (Ideal.span {x}))
  (Submodule.span S (singleton (α := S) ((f : (a : R) → S) x : S)))
Tactic: rw [← Ideal.span, ← Set.image_singleton, Ideal.map_span, Set.image_singleton,
      Ideal.submodule_span_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : R
inst_2 : Submodule.IsPrincipal (M := R) (R ∙ x)
rw :
  Eq (α := Submodule S S) (Ideal.map (R := R) f (Ideal.span {x}))
    (Submodule.span S (singleton (α := S) ((f : (a : R) → S) x : S)))
⊢ Eq (α := Submodule S S) (Ideal.map f (R ∙ x)) (Submodule.span S (singleton (α := S) ((f : (a : R) → S) x : S)))
have rw₁ : Eq (α := Submodule S S) (Ideal.map (R := R) f (Ideal.span {x}))
  (Submodule.span S (Set.image (α := R) (⇑f : (a : R) → S) {x}))
Tactic: rw [← Ideal.span, ← Set.image_singleton, Ideal.map_span, Set.image_singleton,
      Ideal.submodule_span_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : R
inst_2 : Submodule.IsPrincipal (M := R) (R ∙ x)
rw :
  Eq (α := Submodule S S) (Ideal.map (R := R) f (Ideal.span {x}))
    (Submodule.span S (singleton (α := S) ((f : (a : R) → S) x : S)))
rw₁ :
  Eq (α := Submodule S S) (Ideal.map (R := R) f (Ideal.span {x}))
    (Submodule.span S (Set.image (α := R) (⇑f : (a : R) → S) {x}))
⊢ Eq (α := Submodule S S) (Ideal.map f (R ∙ x)) (Submodule.span S (singleton (α := S) ((f : (a : R) → S) x : S)))
have rw₂ : Eq (α := Submodule S S) (Ideal.span (Set.image (α := R) (⇑f : (a : R) → S) {x}))
  (Submodule.span S (Set.image (α := R) (⇑f : (a : R) → S) {x}))
Tactic: rw [← Ideal.span, ← Set.image_singleton, Ideal.map_span, Set.image_singleton,
      Ideal.submodule_span_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : R
inst_2 : Submodule.IsPrincipal (M := R) (R ∙ x)
rw :
  Eq (α := Submodule S S) (Ideal.map (R := R) f (Ideal.span {x}))
    (Submodule.span S (singleton (α := S) ((f : (a : R) → S) x : S)))
rw₁ :
  Eq (α := Submodule S S) (Ideal.map (R := R) f (Ideal.span {x}))
    (Submodule.span S (Set.image (α := R) (⇑f : (a : R) → S) {x}))
rw₂ :
  Eq (α := Submodule S S) (Ideal.span (Set.image (α := R) (⇑f : (a : R) → S) {x}))
    (Submodule.span S (Set.image (α := R) (⇑f : (a : R) → S) {x}))
⊢ Eq (α := Submodule S S) (Ideal.map f (R ∙ x)) (Submodule.span S (singleton (α := S) ((f : (a : R) → S) x : S)))
have rw₃ : Eq (α := Submodule S S) (Ideal.span (singleton (α := S) ((f : (a : R) → S) x : S)))
  (Submodule.span S (singleton (α := S) ((f : (a : R) → S) x : S)))
Tactic: rw [← Ideal.span, ← Set.image_singleton, Ideal.map_span, Set.image_singleton,
      Ideal.submodule_span_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
x : R
inst_2 : Submodule.IsPrincipal (M := R) (R ∙ x)
rw :
  Eq (α := Submodule S S) (Ideal.map (R := R) f (Ideal.span {x}))
    (Submodule.span S (singleton (α := S) ((f : (a : R) → S) x : S)))
rw₁ :
  Eq (α := Submodule S S) (Ideal.map (R := R) f (Ideal.span {x}))
    (Submodule.span S (Set.image (α := R) (⇑f : (a : R) → S) {x}))
rw₂ :
  Eq (α := Submodule S S) (Ideal.span (Set.image (α := R) (⇑f : (a : R) → S) {x}))
    (Submodule.span S (Set.image (α := R) (⇑f : (a : R) → S) {x}))
rw₃ :
  Eq (α := Submodule S S) (Ideal.span (singleton (α := S) ((f : (a : R) → S) x : S)))
    (Submodule.span S (singleton (α := S) ((f : (a : R) → S) x : S)))
⊢ Eq (α := Submodule S S) (Ideal.map f (R ∙ x)) (Submodule.span S (singleton (α := S) ((f : (a : R) → S) x : S)))
have rw₄ : Eq (α := Submodule S S) (Ideal.span (singleton (α := S) ((f : (a : R) → S) x : S)))
  (Ideal.span (singleton (α := S) ((f : (a : R) → S) x : S)))
Tactic: rw [← Ideal.span, ← Set.image_singleton, Ideal.map_span, Set.image_singleton,
      Ideal.submodule_span_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
R : ι → Type u_2
inst_1 : (i : ι) → CommRing (R i)
i : ι
⊢ Eq (α := Ideal ((i : ι) → R i)) (ker (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i))
    (Ideal.span {HSub.hSub (α := (j : ι) → R j) 1 (Pi.single (M := R) i 1)})
have refine : ∀ (x : (i : ι) → R i)
  (hx :
    Membership.mem (γ := Submodule ((i : ι) → R i) ((i : ι) → R i))
      (ker (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i)) x),
  Membership.mem (γ := Submodule ((i : ι) → R i) ((i : ι) → R i))
    (Ideal.span {HSub.hSub (α := (j : ι) → R j) 1 (Pi.single (M := R) i 1)}) x
Tactic: refine le_antisymm (fun x hx ↦ ?_) (by simp [Ideal.span_le])
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (hypothesis)
Goal:
ι : Type u_1
inst : DecidableEq ι
R : ι → Type u_2
inst_1 : (i : ι) → CommRing (R i)
i : ι
x : (i : ι) → R i
hx :
  Membership.mem (γ := Submodule ((i : ι) → R i) ((i : ι) → R i))
    (ker (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i)) x
⊢ Membership.mem (γ := Submodule ((i : ι) → R i) ((i : ι) → R i))
    (Ideal.span {HSub.hSub (α := (j : ι) → R j) 1 (Pi.single (M := R) i 1)}) x
have hx₁ : x i = 0
Tactic: simp only [RingHom.mem_ker, Pi.evalRingHom_apply] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
R : ι → Type u_2
inst_1 : (i : ι) → CommRing (R i)
i : ι
x : (i : ι) → R i
hx : x i = 0
⊢ Membership.mem (γ := Submodule ((i : ι) → R i) ((i : ι) → R i))
    (Ideal.span {HSub.hSub (α := (j : ι) → R j) 1 (Pi.single (M := R) i 1)}) x
have rw : HSub.hSub (α := (j : ι) → R j) 1 (Pi.single (M := R) i 1) ∣ x
Tactic: rw [Ideal.mem_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
R : ι → Type u_2
inst_1 : (i : ι) → CommRing (R i)
i : ι
x : (i : ι) → R i
hx : x i = 0
⊢ HSub.hSub (α := (j : ι) → R j) 1 (Pi.single (M := R) i 1) ∣ x
have h : x = HSub.hSub (α := (j : ι) → R j) 1 (Pi.single (M := R) i 1) * (x + Pi.single (M := R) i 1)
Tactic: use x + Pi.single i 1
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
A : Type u_1
B : Type u_2
inst : Ring A
inst_1 : Ring B
f : A →+* B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
x : B
hx : x ∈ I
⊢ ∃ y ∈ J, (f : (a : A) → B) y = x
have rcases : ∀ (x' : A) (hx' : (f : (a : A) → B) x' = x), ∃ y ∈ J, (f : (a : A) → B) y = x
Tactic: rcases surj x with ⟨x', hx'⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : Ring A
inst_1 : Ring B
f : A →+* B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
x : B
hx : x ∈ I
x' : A
hx' : (f : (a : A) → B) x' = x
⊢ ∃ y ∈ J, (f : (a : A) → B) y = x
have hx₁ : x' ∈ RingHom.ker f ⊔ J
Tactic: rw [← hx', ← Ideal.mem_comap, eq] at hx
Cleared hypotheses: hx, hx'
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
A : Type u_1
B : Type u_2
inst : Ring A
inst_1 : Ring B
f : A →+* B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
x : B
x' : A
hx : x' ∈ RingHom.ker f ⊔ J
hx' : (f : (a : A) → B) x' = x
⊢ ∃ y ∈ J, (f : (a : A) → B) y = x
have rcases : ∀ (y : A) (hy : Membership.mem (γ := Submodule A A) (RingHom.ker f) y) (z : A) (hz : z ∈ J) (hyz : y + z = x'),
  ∃ y ∈ J, (f : (a : A) → B) y = x
Tactic: rcases Submodule.mem_sup.mp hx with ⟨y, hy, z, hz, hyz⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
A : Type u_1
B : Type u_2
inst : Ring A
inst_1 : Ring B
f : A →+* B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
x : B
x' : A
hx : x' ∈ RingHom.ker f ⊔ J
hx' : (f : (a : A) → B) x' = x
y : A
hy : Membership.mem (γ := Submodule A A) (RingHom.ker f) y
z : A
hz : z ∈ J
hyz : y + z = x'
⊢ ∃ y ∈ J, (f : (a : A) → B) y = x
have right : (f : (a : A) → B) z = x
Tactic: use z, hz
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
⊢ I = map f J
have refine : ∀ (x : B) (hx : x ∈ I), Membership.mem (γ := Submodule B B) (map f J) x
Tactic: refine le_antisymm (fun x hx ↦ ?_)
    (Ideal.map_le_iff_le_comap.mpr (le_of_le_of_eq le_sup_right eq.symm))
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
surj : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
x : B
hx : x ∈ I
⊢ Membership.mem (γ := Submodule B B) (map f J) x
have rcases : ∀ (y : A) (mem : y ∈ J) (hy : (f : (a : A) → B) y = x), Membership.mem (γ := Submodule B B) (map f J) x
Tactic: rcases Ideal.exists_of_comap_eq_ker_sup _ surj eq hx with ⟨y, mem, hy⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : Semiring α
I : Ideal α
⊢ I.IsMaximal ↔ 1 ∉ I ∧ ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
have simp_rw : IsCoatom I ↔ 1 ∉ I ∧ ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
Tactic: simp_rw [isMaximal_def, SetLike.isCoatom_iff, Ideal.ne_top_iff_one, ← Ideal.eq_top_iff_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : Semiring α
I : Ideal α
simp_rw : IsCoatom I ↔ 1 ∉ I ∧ ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
⊢ I.IsMaximal ↔ 1 ∉ I ∧ ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
have simp_rw₁ : (I ≠ ⊤ ∧ ∀ (H : Ideal α) (g : α), I ≤ H → g ∉ I → g ∈ H → H = ⊤) ↔
  1 ∉ I ∧ ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
Tactic: simp_rw [isMaximal_def, SetLike.isCoatom_iff, Ideal.ne_top_iff_one, ← Ideal.eq_top_iff_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : Semiring α
I : Ideal α
simp_rw : IsCoatom I ↔ 1 ∉ I ∧ ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
simp_rw₁ :
  (I ≠ ⊤ ∧ ∀ (H : Ideal α) (g : α), I ≤ H → g ∉ I → g ∈ H → H = ⊤) ↔
    1 ∉ I ∧ ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
⊢ I.IsMaximal ↔ 1 ∉ I ∧ ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
have simp_rw₂ : (1 ∉ I ∧ ∀ (H : Ideal α) (g : α), I ≤ H → g ∉ I → g ∈ H → H = ⊤) ↔
  1 ∉ I ∧ ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
Tactic: simp_rw [isMaximal_def, SetLike.isCoatom_iff, Ideal.ne_top_iff_one, ← Ideal.eq_top_iff_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : Semiring α
M M' : Ideal α
hM : M.IsMaximal
hM' : M'.IsMaximal
hne : M ≠ M'
⊢ M ⊔ M' = ⊤
have contrapose! : ∀ (h : M ⊔ M' ≠ ⊤), M = M'
Tactic: contrapose! hne with h
Cleared hypotheses: hne
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : Semiring α
I : Ideal α
⊢ I ≠ ⊤ ↔ ∃ (M : Ideal α), M.IsMaximal ∧ I ≤ M
have refine : (∃ (M : Ideal α), M.IsMaximal ∧ I ≤ M) → I ≠ ⊤
Tactic: refine ⟨exists_le_maximal I, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : Semiring α
I : Ideal α
⊢ (∃ (M : Ideal α), M.IsMaximal ∧ I ≤ M) → I ≠ ⊤
have contrapose! : I = ⊤ → ∀ (M : Ideal α) (_ : M.IsMaximal), ¬I ≤ M
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : Semiring α
M : Ideal α
hMmax : M.IsMaximal
⊢ ¬⊤ ≤ M
have rw : ¬M = ⊤
Tactic: rw [top_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
β : Type v
F : Type w
inst : Semiring α
I : Ideal α
a b : α
inst_1 : Nontrivial α
⊢ Nontrivial.{u} (Ideal α)
have rcases : ∀ (M : Ideal α) (hM : M ≠ ⊤), (∀ (b : Ideal α), M < b → b = ⊤) → Nontrivial.{u} (Ideal α)
Tactic: rcases @exists_maximal α _ _ with ⟨M, hM, _⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : Semiring α
P : Ideal α
hmax : ∀ (m : Ideal α), P < m → ¬m.IsMaximal
J : Ideal α
hPJ : P < J
⊢ J = ⊤
have by_contra : ∀ (hnonmax : ¬J = ⊤), False
Tactic: by_contra hnonmax
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : Semiring α
P : Ideal α
hmax : ∀ (m : Ideal α), P < m → ¬m.IsMaximal
J : Ideal α
hPJ : P < J
hnonmax : ¬J = ⊤
⊢ False
have rcases : ∀ (M : Ideal α) (hM1 : M.IsMaximal) (hM2 : J ≤ M), False
Tactic: rcases exists_le_maximal J hnonmax with ⟨M, hM1, hM2⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (hypothesis)
Goal:
α : Type u
inst : Semiring α
I : Ideal α
hI : I.IsMaximal
x : α
hx : x ∉ I
⊢ ∃ (y : α), ∃ i ∈ I, y * x + i = 1
have H₁ : 1 ∉ I
Tactic: obtain ⟨H₁, H₂⟩ := isMaximal_iff.1 hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (hypothesis)
Goal:
α : Type u
inst : Semiring α
I : Ideal α
hI : I.IsMaximal
x : α
hx : x ∉ I
H₁ : 1 ∉ I
⊢ ∃ (y : α), ∃ i ∈ I, y * x + i = 1
have H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
Tactic: obtain ⟨H₁, H₂⟩ := isMaximal_iff.1 hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : Semiring α
I : Ideal α
hI : I.IsMaximal
x : α
hx : x ∉ I
H₁ : 1 ∉ I
H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
⊢ ∃ (y : α), ∃ i ∈ I, y * x + i = 1
have rcases : ∀ (y z : α) (hz : Membership.mem (γ := Ideal α) (span (↑I : Set α)) z) (hy : 1 = y * x + z),
  ∃ (y : α), ∃ i ∈ I, y * x + i = 1
Tactic: rcases mem_span_insert.1
      (H₂ (span (insert x I)) x (Set.Subset.trans (subset_insert _ _) subset_span) hx
        (subset_span (mem_insert _ _))) with
    ⟨y, z, hz, hy⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : Semiring α
I : Ideal α
hI : I.IsMaximal
x : α
hx : x ∉ I
H₁ : 1 ∉ I
H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
y z : α
hz : Membership.mem (γ := Ideal α) (span (↑I : Set α)) z
hy : 1 = y * x + z
⊢ ∃ (y : α), ∃ i ∈ I, y * x + i = 1
have refine : z ∈ I
Tactic: refine ⟨y, z, ?_, hy.symm⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun (x1 x2 : Ideal α) ↦ x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x y : α
e : x * y ∈ sInf s
hx : x ∉ sInf s
⊢ y ∈ sInf s
have rw : ∀ (e : ∀ ⦃I : Ideal α⦄, I ∈ s → x * y ∈ I) (hx : ¬∀ ⦃I : Ideal α⦄, I ∈ s → x ∈ I) ⦃I : Ideal α⦄, I ∈ s → y ∈ I
Tactic: rw [Ideal.mem_sInf] at hx e ⊢
Cleared hypotheses: e, hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (hypothesis)
Goal:
α : Type u
inst : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun (x1 x2 : Ideal α) ↦ x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x y : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x * y ∈ I
hx : ¬∀ ⦃I : Ideal α⦄, I ∈ s → x ∈ I
⊢ ∀ ⦃I : Ideal α⦄, I ∈ s → y ∈ I
have hx₁ : ∃ I ∈ s, x ∉ I
Tactic: push Not at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun (x1 x2 : Ideal α) ↦ x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x y : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x * y ∈ I
hx : ∃ I ∈ s, x ∉ I
⊢ ∀ ⦃I : Ideal α⦄, I ∈ s → y ∈ I
have obtain : ∀ (I : Ideal α) (hI : I ∈ s) (hI' : x ∉ I) ⦃I : Ideal α⦄, I ∈ s → y ∈ I
Tactic: obtain ⟨I, hI, hI'⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun (x1 x2 : Ideal α) ↦ x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x y : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x * y ∈ I
I : Ideal α
hI : I ∈ s
hI' : x ∉ I
J : Ideal α
hJ : J ∈ s
⊢ y ∈ J
have inl : ∀ (h : I ≤ J), y ∈ J
Tactic: rcases hs'.total hI hJ with h | h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (goal)
Goal:
α : Type u
inst : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun (x1 x2 : Ideal α) ↦ x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x y : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x * y ∈ I
I : Ideal α
hI : I ∈ s
hI' : x ∉ I
J : Ideal α
hJ : J ∈ s
inl : ∀ (h : I ≤ J), y ∈ J
⊢ y ∈ J
have inr : ∀ (h : J ≤ I), y ∈ J
Tactic: rcases hs'.total hI hJ with h | h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (hypothesis)
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x (↑I : Set α))
⊢ y ∈ I
have IJ : I ≤ J
Tactic: have IJ : I ≤ J := Set.Subset.trans (subset_insert _ _) subset_span
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (hypothesis)
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x (↑I : Set α))
IJ : I ≤ J
⊢ y ∈ I
have xJ : x ∈ J
Tactic: have xJ : x ∈ J := Ideal.subset_span (Set.mem_insert x I)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (hypothesis)
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x (↑I : Set α))
IJ : I ≤ J
xJ : x ∈ J
⊢ y ∈ I
have left : 1 ∉ I
Tactic: obtain ⟨_, oJ⟩ := isMaximal_iff.1 H
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (hypothesis)
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x (↑I : Set α))
IJ : I ≤ J
xJ : x ∈ J
left : 1 ∉ I
⊢ y ∈ I
have oJ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
Tactic: obtain ⟨_, oJ⟩ := isMaximal_iff.1 H
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maximal (hypothesis)
Goal:
α : Type u
inst : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x (↑I : Set α))
IJ : I ≤ J
xJ : x ∈ J
left : 1 ∉ I
oJ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
⊢ y ∈ I
have oJ₁ : 1 ∈ J
Tactic: specialize oJ J x IJ hx xJ
Cleared hypotheses: oJ