awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
f : R ≃+* S
rw : map (R := S) f.symm.toRingHom (map (F := R →+* S) (↑f : R →+* S) I) = I
rw₁ : map (R := S) f.symm.toRingHom (map f.toRingHom I) = I
rw₂ : map (f.symm.toRingHom.comp f.toRingHom) I = I
rw₃ : map (F := R →+* R) (RingHom.comp (↑f.symm : S →+* R) f.toRingHom) I = I
rw₄ : map (F := R →+* R) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f.symm : S →+* R) (↑f : R →+* S)) I = I
rw₅ : map (F := R →+* R) (RingHom.id R) I = I
⊢ map (R := S) (F := S →+* R) (↑f.symm : S →+* R) (map (F := R →+* S) (↑f : R →+* S) I) = I
have rw₆ : I = I
Tactic: rw [← RingEquiv.toRingHom_eq_coe, ← RingEquiv.toRingHom_eq_coe, map_map,
    RingEquiv.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp, map_id]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
f : R ≃+* S
⊢ comap (F := R →+* S) (↑f : R →+* S) (comap (F := S →+* R) (↑f.symm : S →+* R) I) = I
have rw : comap f.toRingHom (comap (F := S →+* R) (↑f.symm : S →+* R) I) = I
Tactic: rw [← RingEquiv.toRingHom_eq_coe, ← RingEquiv.toRingHom_eq_coe, comap_comap,
    RingEquiv.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp, comap_id]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
f : R ≃+* S
rw : comap f.toRingHom (comap (F := S →+* R) (↑f.symm : S →+* R) I) = I
⊢ comap (F := R →+* S) (↑f : R →+* S) (comap (F := S →+* R) (↑f.symm : S →+* R) I) = I
have rw₁ : comap f.toRingHom (comap f.symm.toRingHom I) = I
Tactic: rw [← RingEquiv.toRingHom_eq_coe, ← RingEquiv.toRingHom_eq_coe, comap_comap,
    RingEquiv.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp, comap_id]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
f : R ≃+* S
rw : comap f.toRingHom (comap (F := S →+* R) (↑f.symm : S →+* R) I) = I
rw₁ : comap f.toRingHom (comap f.symm.toRingHom I) = I
⊢ comap (F := R →+* S) (↑f : R →+* S) (comap (F := S →+* R) (↑f.symm : S →+* R) I) = I
have rw₂ : comap (f.symm.toRingHom.comp f.toRingHom) I = I
Tactic: rw [← RingEquiv.toRingHom_eq_coe, ← RingEquiv.toRingHom_eq_coe, comap_comap,
    RingEquiv.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp, comap_id]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
f : R ≃+* S
rw : comap f.toRingHom (comap (F := S →+* R) (↑f.symm : S →+* R) I) = I
rw₁ : comap f.toRingHom (comap f.symm.toRingHom I) = I
rw₂ : comap (f.symm.toRingHom.comp f.toRingHom) I = I
⊢ comap (F := R →+* S) (↑f : R →+* S) (comap (F := S →+* R) (↑f.symm : S →+* R) I) = I
have rw₃ : comap (F := R →+* R) (RingHom.comp (↑f.symm : S →+* R) f.toRingHom) I = I
Tactic: rw [← RingEquiv.toRingHom_eq_coe, ← RingEquiv.toRingHom_eq_coe, comap_comap,
    RingEquiv.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp, comap_id]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
f : R ≃+* S
rw : comap f.toRingHom (comap (F := S →+* R) (↑f.symm : S →+* R) I) = I
rw₁ : comap f.toRingHom (comap f.symm.toRingHom I) = I
rw₂ : comap (f.symm.toRingHom.comp f.toRingHom) I = I
rw₃ : comap (F := R →+* R) (RingHom.comp (↑f.symm : S →+* R) f.toRingHom) I = I
⊢ comap (F := R →+* S) (↑f : R →+* S) (comap (F := S →+* R) (↑f.symm : S →+* R) I) = I
have rw₄ : comap (F := R →+* R) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f.symm : S →+* R) (↑f : R →+* S)) I = I
Tactic: rw [← RingEquiv.toRingHom_eq_coe, ← RingEquiv.toRingHom_eq_coe, comap_comap,
    RingEquiv.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp, comap_id]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
f : R ≃+* S
rw : comap f.toRingHom (comap (F := S →+* R) (↑f.symm : S →+* R) I) = I
rw₁ : comap f.toRingHom (comap f.symm.toRingHom I) = I
rw₂ : comap (f.symm.toRingHom.comp f.toRingHom) I = I
rw₃ : comap (F := R →+* R) (RingHom.comp (↑f.symm : S →+* R) f.toRingHom) I = I
rw₄ :
  comap (F := R →+* R) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f.symm : S →+* R) (↑f : R →+* S)) I = I
⊢ comap (F := R →+* S) (↑f : R →+* S) (comap (F := S →+* R) (↑f.symm : S →+* R) I) = I
have rw₅ : comap (F := R →+* R) (RingHom.id R) I = I
Tactic: rw [← RingEquiv.toRingHom_eq_coe, ← RingEquiv.toRingHom_eq_coe, comap_comap,
    RingEquiv.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp, comap_id]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
f : R ≃+* S
rw : comap f.toRingHom (comap (F := S →+* R) (↑f.symm : S →+* R) I) = I
rw₁ : comap f.toRingHom (comap f.symm.toRingHom I) = I
rw₂ : comap (f.symm.toRingHom.comp f.toRingHom) I = I
rw₃ : comap (F := R →+* R) (RingHom.comp (↑f.symm : S →+* R) f.toRingHom) I = I
rw₄ :
  comap (F := R →+* R) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f.symm : S →+* R) (↑f : R →+* S)) I = I
rw₅ : comap (F := R →+* R) (RingHom.id R) I = I
⊢ comap (F := R →+* S) (↑f : R →+* S) (comap (F := S →+* R) (↑f.symm : S →+* R) I) = I
have rw₆ : I = I
Tactic: rw [← RingEquiv.toRingHom_eq_coe, ← RingEquiv.toRingHom_eq_coe, comap_comap,
    RingEquiv.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp, comap_id]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
f : R ≃+* S
y : S
⊢ Membership.mem (α := R) I ((f.symm : (a : S) → R) y : R) ↔ Membership.mem (γ := Ideal S) (map f I) y
have rw : Membership.mem (α := R) I ((f.symm : (a : S) → R) y : R) ↔ Membership.mem (γ := Ideal S) (comap f.symm I) y
Tactic: rw [← comap_symm, mem_comap]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
f : R ≃+* S
y : S
rw : Membership.mem (α := R) I ((f.symm : (a : S) → R) y : R) ↔ Membership.mem (γ := Ideal S) (comap f.symm I) y
⊢ Membership.mem (α := R) I ((f.symm : (a : S) → R) y : R) ↔ Membership.mem (γ := Ideal S) (map f I) y
have rw₁ : Membership.mem (α := R) I ((f.symm : (a : S) → R) y : R) ↔ Membership.mem (α := R) I ((f.symm : (a : S) → R) y : R)
Tactic: rw [← comap_symm, mem_comap]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
f : R ≃+* S
x : R
⊢ Membership.mem.{v, v} (α := S) (γ := Ideal S) (map f I) ((f : (a : R) → S) x : S) ↔ x ∈ I
have rw : Membership.mem (α := S) (γ := Ideal S) (comap f.symm I) ((f : (a : R) → S) x : S) ↔ x ∈ I
Tactic: rw [← comap_symm, Ideal.mem_comap, f.symm_apply_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
f : R ≃+* S
x : R
rw : Membership.mem (α := S) (γ := Ideal S) (comap f.symm I) ((f : (a : R) → S) x : S) ↔ x ∈ I
⊢ Membership.mem.{v, v} (α := S) (γ := Ideal S) (map f I) ((f : (a : R) → S) x : S) ↔ x ∈ I
have rw₁ : Membership.mem (α := R) I ((f.symm : (a : S) → R) ((f : (a : R) → S) x : S) : R) ↔ x ∈ I
Tactic: rw [← comap_symm, Ideal.mem_comap, f.symm_apply_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
f : R ≃+* S
x : R
rw : Membership.mem (α := S) (γ := Ideal S) (comap f.symm I) ((f : (a : R) → S) x : S) ↔ x ∈ I
rw₁ : Membership.mem (α := R) I ((f.symm : (a : S) → R) ((f : (a : R) → S) x : S) : R) ↔ x ∈ I
⊢ Membership.mem.{v, v} (α := S) (γ := Ideal S) (map f I) ((f : (a : R) → S) x : S) ↔ x ∈ I
have rw₂ : x ∈ I ↔ x ∈ I
Tactic: rw [← comap_symm, Ideal.mem_comap, f.symm_apply_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
E : Type u_4
inst_2 : EquivLike E R S
inst_3 : RingEquivClass E R S
e : E
I : Ideal R
y : S
⊢ Membership.mem (γ := Ideal S) (map e I) y ↔ ∃ x ∈ I, (e : (a : R) → S) x = y
have mp : Membership.mem (γ := Ideal S) (map e I) y → ∃ x ∈ I, (e : (a : R) → S) x = y
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
E : Type u_4
inst_2 : EquivLike E R S
inst_3 : RingEquivClass E R S
e : E
I : Ideal R
y : S
mp : Membership.mem (γ := Ideal S) (map e I) y → ∃ x ∈ I, (e : (a : R) → S) x = y
⊢ Membership.mem (γ := Ideal S) (map e I) y ↔ ∃ x ∈ I, (e : (a : R) → S) x = y
have mpr : (∃ x ∈ I, (e : (a : R) → S) x = y) → Membership.mem (γ := Ideal S) (map e I) y
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (hypothesis)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
E : Type u_4
inst_2 : EquivLike E R S
inst_3 : RingEquivClass E R S
e : E
I : Ideal R
y : S
h : Membership.mem (γ := Ideal S) (map e I) y
⊢ ∃ x ∈ I, (e : (a : R) → S) x = y
have h₁ : Membership.mem (γ := Ideal S) (comap (F := S ≃+* R) (RingEquiv.symm (↑e : R ≃+* S)) I) y
Tactic: simp_rw [show map e I = _ from map_comap_of_equiv (RingEquivClass.toRingEquiv e : R ≃+* S)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p : Ideal S
inst_4 : p.IsPrime
⊢ Submonoid.map f (primeCompl (comap f p)) = p.primeCompl
have rw : ∀ (x : R),
  Membership.mem (α := S) (γ := Submonoid S) (Submonoid.map f (primeCompl (comap f p))) ((f : (a : R) → S) x : S) ↔
    Membership.mem (α := S) p.primeCompl ((f : (a : R) → S) x : S)
Tactic: rw [SetLike.ext_iff, hf.forall]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I_1 J : Ideal R
K_1 L : Ideal S
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass F R S
ι : Sort u_3
hf : Function.Bijective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
K x x_1 : Ideal S
⊢ LE.le.{u} (α := Ideal R)
      ((({ toFun := comap f, invFun := map f, left_inv := ⋯, right_inv := ⋯ } :
              Equiv.{v + 1, u + 1} (Ideal S) (Ideal R)) :
            (a : Ideal S) → Ideal R)
          x :
        Ideal R)
      ((({ toFun := comap f, invFun := map f, left_inv := ⋯, right_inv := ⋯ } :
              Equiv.{v + 1, u + 1} (Ideal S) (Ideal R)) :
            (a : Ideal S) → Ideal R)
          x_1 :
        Ideal R) ↔
    x ≤ x_1
have refine : ∀
  (h :
    LE.le.{u} (α := Ideal R)
      ((({ toFun := comap f, invFun := map f, left_inv := sorry, right_inv := sorry } :
              Equiv.{v + 1, u + 1} (Ideal S) (Ideal R)) :
            (a : Ideal S) → Ideal R)
          x :
        Ideal R)
      ((({ toFun := comap f, invFun := map f, left_inv := sorry, right_inv := sorry } :
              Equiv.{v + 1, u + 1} (Ideal S) (Ideal R)) :
            (a : Ideal S) → Ideal R)
          x_1 :
        Ideal R)),
  x ≤ x_1
Tactic: refine ⟨fun h ↦ ?_, comap_mono⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (hypothesis)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I_1 J : Ideal R
K_1 L : Ideal S
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass F R S
ι : Sort u_3
hf : Function.Bijective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
K x x_1 : Ideal S
h :
  LE.le.{u} (α := Ideal R)
    ((({ toFun := comap f, invFun := map f, left_inv := ⋯, right_inv := ⋯ } :
            Equiv.{v + 1, u + 1} (Ideal S) (Ideal R)) :
          (a : Ideal S) → Ideal R)
        x :
      Ideal R)
    ((({ toFun := comap f, invFun := map f, left_inv := ⋯, right_inv := ⋯ } :
            Equiv.{v + 1, u + 1} (Ideal S) (Ideal R)) :
          (a : Ideal S) → Ideal R)
        x_1 :
      Ideal R)
⊢ x ≤ x_1
have this : LE.le.{v} (α := Ideal S)
  (map.{u, v, u_1} (R := R) f
    ((({ toFun := comap f, invFun := map f, left_inv := sorry, right_inv := sorry } :
          Equiv.{v + 1, u + 1} (Ideal S) (Ideal R)) :
        (a : Ideal S) → Ideal R)
      x))
  (map.{u, v, u_1} (R := R) f
    ((({ toFun := comap f, invFun := map f, left_inv := sorry, right_inv := sorry } :
          Equiv.{v + 1, u + 1} (Ideal S) (Ideal R)) :
        (a : Ideal S) → Ideal R)
      x_1))
Tactic: have := map_mono (f := f) h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
hf : Function.Bijective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
⊢ Eq.{v + 1} (α := Ideal S) (map f I) ⊤ ↔ I = ⊤
have rw : LE.le.{v} (α := Ideal S) ⊤ (map f I) ↔ I = ⊤
Tactic: rw [eq_top_iff, ← comap_le_iff_le_map f hf, comap_top, top_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
hf : Function.Bijective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
rw : LE.le.{v} (α := Ideal S) ⊤ (map f I) ↔ I = ⊤
⊢ Eq.{v + 1} (α := Ideal S) (map f I) ⊤ ↔ I = ⊤
have rw₁ : comap f ⊤ ≤ I ↔ I = ⊤
Tactic: rw [eq_top_iff, ← comap_le_iff_le_map f hf, comap_top, top_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
hf : Function.Bijective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
rw : LE.le.{v} (α := Ideal S) ⊤ (map f I) ↔ I = ⊤
rw₁ : comap f ⊤ ≤ I ↔ I = ⊤
⊢ Eq.{v + 1} (α := Ideal S) (map f I) ⊤ ↔ I = ⊤
have rw₂ : ⊤ ≤ I ↔ I = ⊤
Tactic: rw [eq_top_iff, ← comap_le_iff_le_map f hf, comap_top, top_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
hf : Function.Bijective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
rw : LE.le.{v} (α := Ideal S) ⊤ (map f I) ↔ I = ⊤
rw₁ : comap f ⊤ ≤ I ↔ I = ⊤
rw₂ : ⊤ ≤ I ↔ I = ⊤
⊢ Eq.{v + 1} (α := Ideal S) (map f I) ⊤ ↔ I = ⊤
have rw₃ : I = ⊤ ↔ I = ⊤
Tactic: rw [eq_top_iff, ← comap_le_iff_le_map f hf, comap_top, top_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
inst_3 : RingHomClass F R S
f : F
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
r : R
h : Membership.mem.{v, v} (α := S) (γ := Ideal S) (map f I) ((f : (a : R) → S) r : S)
s : R
hsi : s ∈ (↑I : Set R)
hfsr : Eq.{v + 1} (α := S) ((f : (a : R) → S) s : S) ((f : (a : R) → S) r : S)
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (r - s) : S) (0 : S)
have rw : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) r : S) ((f : (a : R) → S) s : S) = 0
Tactic: rw [map_sub, hfsr, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
inst_3 : RingHomClass F R S
f : F
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
r : R
h : Membership.mem.{v, v} (α := S) (γ := Ideal S) (map f I) ((f : (a : R) → S) r : S)
s : R
hsi : s ∈ (↑I : Set R)
hfsr : Eq.{v + 1} (α := S) ((f : (a : R) → S) s : S) ((f : (a : R) → S) r : S)
rw : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) r : S) ((f : (a : R) → S) s : S) = 0
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (r - s) : S) (0 : S)
have rw₁ : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) r : S) ((f : (a : R) → S) r : S) = 0
Tactic: rw [map_sub, hfsr, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
inst_3 : RingHomClass F R S
f : F
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
r : R
h : Membership.mem.{v, v} (α := S) (γ := Ideal S) (map f I) ((f : (a : R) → S) r : S)
s : R
hsi : s ∈ (↑I : Set R)
hfsr : Eq.{v + 1} (α := S) ((f : (a : R) → S) s : S) ((f : (a : R) → S) r : S)
rw : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) r : S) ((f : (a : R) → S) s : S) = 0
rw₁ : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) r : S) ((f : (a : R) → S) r : S) = 0
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (r - s) : S) (0 : S)
have rw₂ : Eq.{v + 1} (α := S) 0 0
Tactic: rw [map_sub, hfsr, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
inst_3 : RingHomClass F R S
f : F
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
K : Ideal S
H : K.IsMaximal
⊢ IsMaximal (comap f K)
have refine : ∀ (J : Ideal R) (hJ : comap f K < J), J = ⊤
Tactic: refine ⟨⟨comap_ne_top _ H.1.1, fun J hJ => ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (hypothesis)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
inst_3 : RingHomClass F R S
f : F
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
this : Eq.{v + 1} (α := Ideal S) (map f J) ⊤
⊢ J = ⊤
have this₁ : Eq (α := Ideal R) (comap f (map f J)) (comap f ⊤)
Tactic: have := congr_arg (comap f) this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (hypothesis)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
inst_3 : RingHomClass F R S
f : F
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
this_1 : Eq.{v + 1} (α := Ideal S) (map f J) ⊤
this : Eq (α := Ideal R) (comap f (map f J)) (comap f ⊤)
⊢ J = ⊤
have this₁ : ⊤ ≤ J ⊔ comap f ⊥
Tactic: rw [comap_top, comap_map_of_surjective _ hf, eq_top_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
inst_3 : RingHomClass F R S
f : F
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
this_1 : Eq.{v + 1} (α := Ideal S) (map f J) ⊤
this : ⊤ ≤ J ⊔ comap f ⊥
⊢ J = ⊤
have rw : ⊤ ≤ J
Tactic: rw [eq_top_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
inst_3 : RingHomClass F R S
f : F
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
⊢ J = ⊤
have suffices : Eq.{v + 1} (α := Ideal S) (map f J) ⊤
Tactic: suffices map f J = ⊤ by
    have := congr_arg (comap f) this
    rw [comap_top, comap_map_of_surjective _ hf, eq_top_iff] at this
    rw [eq_top_iff]
    exact le_trans this (sup_le (le_of_eq rfl) (le_trans (comap_mono bot_le) (le_of_lt hJ)))
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
inst_3 : RingHomClass F R S
f : F
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
⊢ Eq.{v + 1} (α := Ideal S) (map f J) ⊤
have f₁ : ∀ (h : K = map f J), comap f (map f J) = J
Tactic: refine
    H.1.2 (map f J)
      (lt_of_le_of_ne (le_map_of_comap_le_of_surjective _ hf (le_of_lt hJ)) fun h =>
        ne_of_lt hJ (_root_.trans (congr_arg (comap f) h) ?_))
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
inst_3 : RingHomClass F R S
f : F
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
h : K = map f J
⊢ comap f (map f J) = J
have rw : comap f ⊥ ≤ J
Tactic: rw [comap_map_of_surjective _ hf, sup_eq_left]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
S : Type v
F : Type u_1
inst : CommSemiring S
R : Type u_2
inst_1 : Semiring R
inst_2 : FunLike F R S
inst_3 : RingHomClass F R S
f : F
I J : Ideal R
r : R
hri : r ∈ I
s : R
hsj : s ∈ J
⊢ Membership.mem (α := S) (HMul.hMul (α := Ideal S) (map f I) (map f J)) ((f : (a : R) → S) (r * s) : S)
have rw : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) r : S) ((f : (a : R) → S) s : S) ∈
  HMul.hMul (α := Ideal S) (map f I) (map f J)
Tactic: rw [map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
S : Type v
F : Type u_1
inst : CommSemiring S
R : Type u_2
inst_1 : Semiring R
inst_2 : FunLike F R S
inst_3 : RingHomClass F R S
f : F
I J : Ideal R
r : R
hri : r ∈ (↑I : Set R)
s : R
hsj : s ∈ (↑J : Set R)
⊢ (fun (x1 x2 : S) ↦ x1 * x2) ((f : (a : R) → S) r) ((f : (a : R) → S) s) ∈ (↑(map f (I * J)) : Set S)
have simp_rw : Membership.mem (α := S) (↑(map f (I * J)) : Set S) ((f : (a : R) → S) (r * s) : S)
Tactic: simp_rw [← map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
⊢ Eq (α := Ideal R) (comap f K.radical) (radical (comap f K))
have h : ∀ (x : R), Membership.mem (γ := Ideal R) (comap f K.radical) x ↔ Membership.mem (γ := Ideal R) (radical (comap f K)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
hK : K.IsRadical
⊢ IsRadical (Ideal.comap f K)
have rw : IsRadical (Ideal.radical (Ideal.comap f K))
Tactic: rw [← hK.radical, comap_radical]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
⊢ HPow.hPow (α := Ideal R) (β := ℕ) (comap f K) 0 ≤ comap f (HPow.hPow (β := ℕ) K 0)
have zero : LE.le (α := Ideal R) ⊤ (comap f ⊤)
Tactic: rw [pow_zero, pow_zero, Ideal.one_eq_top, Ideal.one_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
n : ℕ
n_ih : HPow.hPow (α := Ideal R) (comap f K) n ≤ comap f (K ^ n)
⊢ HPow.hPow (α := Ideal R) (comap f K) (n + 1) ≤ comap f (K ^ (n + 1))
have succ : HPow.hPow (α := Ideal R) (comap f K) n * comap f K ≤ comap f (K ^ n * K)
Tactic: rw [pow_succ, pow_succ]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
F : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
K : Ideal S
n : ℕ
⊢ HPow.hPow (α := Ideal R) (comap f K) n ≤ comap f (K ^ n)
have zero : HPow.hPow (α := Ideal R) (β := ℕ) (comap f K) 0 ≤ comap f (HPow.hPow (β := ℕ) K 0)
Tactic: induction n with
  | zero =>
    rw [pow_zero, pow_zero, Ideal.one_eq_top, Ideal.one_eq_top]
    exact rfl.le
  | succ n n_ih =>
    rw [pow_succ, pow_succ]
    exact (Ideal.mul_mono_left n_ih).trans (Ideal.le_comap_mul f)
Cleared hypotheses: n