awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Maps
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) (comap (F := S ≃+* R) (RingEquiv.symm (↑e : R ≃+* S)) I) y
⊢ ∃ x ∈ I, (e : (a : R) → S) x = y

Tactic:
exact ⟨(EquivLike.toEquiv e).symm y, h, (EquivLike.toEquiv e).apply_symm_apply y⟩
-- Module: Mathlib.RingTheory.Ideal.Maps
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
x : R
hx : x ∈ I
⊢ Membership.mem.{v, v} (α := S) (γ := Ideal S) (map e I) ((e : (a : R) → S) x : S)

Tactic:
mem_map_of_mem e hx

Premises used: Ideal.mem_map_of_mem
-- Module: Mathlib.RingTheory.Ideal.Maps
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
x : R
hx : x ∈ I
⊢ Membership.mem.{v, v} (α := S) (γ := Ideal S) (map e I) ((e : (a : R) → S) x : S)

Tactic:
exact mem_map_of_mem e hx

Premises used: Ideal.mem_map_of_mem
-- Module: Mathlib.RingTheory.Ideal.Maps
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
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)
⊢ Submonoid.map f (primeCompl (comap f p)) = p.primeCompl

Tactic:
rw [SetLike.ext_iff, hf.forall]

Premises used: Function.Surjective.forall, SetLike.ext_iff
-- Module: Mathlib.RingTheory.Ideal.Maps
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
⊢ ∀ (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:
grind [Submonoid.mem_map, mem_primeCompl_iff, mem_comap]

Premises used: Submonoid.mem_map, Ideal.mem_primeCompl_iff, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
e : R ≃+* S
p : Ideal S
inst_2 : p.IsPrime
⊢ Submonoid.map e (primeCompl (comap e p)) = p.primeCompl

Tactic:
p.map_primeCompl_comap_of_surjective e e.surjective

Premises used: Ideal.map_primeCompl_comap_of_surjective, RingEquiv.surjective
-- Module: Mathlib.RingTheory.Ideal.Maps
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

Tactic:
⟨fun h ↦ ?_, comap_mono⟩

Premises used: Ideal.comap_mono, Iff.intro
-- Module: Mathlib.RingTheory.Ideal.Maps
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
refine :
  ∀
    (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
⊢ 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

Tactic:
refine ⟨fun h ↦ ?_, comap_mono⟩
-- Module: Mathlib.RingTheory.Ideal.Maps
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)
⊢ LE.le.{v} (α := Ideal S)
    (map.{u, v, u_1} (R := R) f
      ((({ 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))
    (map.{u, v, u_1} (R := R) f
      ((({ 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))

Tactic:
have := map_mono (f := f) h
-- Module: Mathlib.RingTheory.Ideal.Maps
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)
this :
  LE.le.{v} (α := Ideal S)
    (map.{u, v, u_1} (R := R) f
      ((({ 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))
    (map.{u, v, u_1} (R := R) f
      ((({ 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))
⊢ x ≤ x_1

Tactic:
simpa only [Equiv.coe_fn_mk, map_comap_of_surjective f hf.2] using this

Premises used: And.right, Equiv.coe_fn_mk, Ideal.map_comap_of_surjective
-- Module: Mathlib.RingTheory.Ideal.Maps
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
K : Ideal S
⊢ comap f K ≤ I ↔ K ≤ map f I

Tactic:
⟨fun h => le_map_of_comap_le_of_surjective f hf.right h, fun h =>
    (relIsoOfBijective f hf).right_inv I ▸ comap_mono h⟩

Premises used: Equiv.right_inv, Eq.rec, Ideal.le_map_of_comap_le_of_surjective, Ideal.comap_mono, And.right, Iff.intro, RelIso.toEquiv, Ideal.relIsoOfBijective
-- Module: Mathlib.RingTheory.Ideal.Maps
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 = ⊤
rw₃ rw₄ : I = ⊤ ↔ I = ⊤
⊢ Eq.{v + 1} (α := Ideal S) (map f I) ⊤ ↔ I = ⊤

Tactic:
rw [eq_top_iff, ← comap_le_iff_le_map f hf, comap_top, top_le_iff]

Premises used: eq_top_iff, top_le_iff, Ideal.comap_top, Ideal.comap_le_iff_le_map
-- Module: Mathlib.RingTheory.Ideal.Maps
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
⊢ comap f (map f I) = I

Tactic:
le_antisymm ((comap_le_iff_le_map f hf).mpr fun _ ↦ id) le_comap_map

Premises used: Iff.mpr, id, le_antisymm, Ideal.le_comap_map, Ideal.comap_le_iff_le_map
-- Module: Mathlib.RingTheory.Ideal.Maps
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
⊢ IsMaximal.{v} (α := S) (map f I) ↔ I.IsMaximal

Tactic:
simpa only [isMaximal_def] using (relIsoOfBijective _ hf).symm.isCoatom_iff _

Premises used: OrderIso.isCoatom_iff, OrderIso.symm, Ideal.relIsoOfBijective, Ideal.isMaximal_def
-- Module: Mathlib.RingTheory.Ideal.Maps
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)
K : Ideal S
⊢ IsMaximal (comap f K) ↔ K.IsMaximal

Tactic:
simpa only [isMaximal_def] using (relIsoOfBijective _ hf).isCoatom_iff _

Premises used: OrderIso.isCoatom_iff, Ideal.relIsoOfBijective, Ideal.isMaximal_def
-- Module: Mathlib.RingTheory.Ideal.Maps
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 : Ideal S
E : Type u_4
inst_5 : EquivLike E R S
inst_6 : RingEquivClass E R S
e : E
p : Ideal R
hp : p.IsMaximal
⊢ IsMaximal.{v} (α := S) (map e p)

Tactic:
hp.map_bijective e (EquivLike.bijective e)

Premises used: Ideal.IsMaximal.map_bijective, EquivLike.bijective
-- Module: Mathlib.RingTheory.Ideal.Maps
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 : Ideal S
E : Type u_4
inst_5 : EquivLike E R S
inst_6 : RingEquivClass E R S
e : E
p : Ideal S
hp : p.IsMaximal
⊢ IsMaximal (comap e p)

Tactic:
hp.comap_bijective e (EquivLike.bijective e)

Premises used: Ideal.IsMaximal.comap_bijective, EquivLike.bijective
-- Module: Mathlib.RingTheory.Ideal.Maps
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)
⊢ IsMaximal.{u} (α := R) ⊥ ↔ IsMaximal.{v} (α := S) ⊥

Tactic:
⟨fun h ↦ map_bot (f := f) ▸ h.map_bijective f hf, fun h ↦ have e := RingEquiv.ofBijective f hf
    map_bot (f := e.symm) ▸ h.map_bijective _ e.symm.bijective⟩

Premises used: Ideal.IsMaximal.map_bijective, RingEquiv.ofBijective, Eq.rec, Ideal.map_bot, Iff.intro, RingEquiv.bijective, RingEquiv.symm
-- Module: Mathlib.RingTheory.Ideal.Maps
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
rw₂ rw₃ : Eq.{v + 1} (α := S) 0 0
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (r - s) : S) (0 : S)

Tactic:
rw [map_sub, hfsr, sub_self]

Premises used: map_sub, sub_self
-- Module: Mathlib.RingTheory.Ideal.Maps
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)

Tactic:
⟨⟨comap_ne_top _ H.1.1, fun J hJ => ?_⟩⟩

Premises used: Ideal.comap_ne_top, Ideal.IsMaximal.mk, Ideal.IsMaximal.out, And.left, And.intro
-- Module: Mathlib.RingTheory.Ideal.Maps
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
refine : ∀ (J : Ideal R) (hJ : comap f K < J), J = ⊤
⊢ IsMaximal (comap f K)

Tactic:
refine ⟨⟨comap_ne_top _ H.1.1, fun J hJ => ?_⟩⟩
-- Module: Mathlib.RingTheory.Ideal.Maps
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) ⊤
⊢ Eq (α := Ideal R) (comap f (map f J)) (comap f ⊤)

Tactic:
have := congr_arg (comap f) this
-- Module: Mathlib.RingTheory.Ideal.Maps
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 ⊔ comap f ⊥

Tactic:
rw [comap_top, comap_map_of_surjective _ hf, eq_top_iff] at this

Premises used: eq_top_iff, Ideal.comap_map_of_surjective, Ideal.comap_top
-- Module: Mathlib.RingTheory.Ideal.Maps
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 ⊥
rw : ⊤ ≤ J
⊢ J = ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.RingTheory.Ideal.Maps
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

Tactic:
le_trans this (sup_le (le_of_eq rfl) (le_trans (comap_mono bot_le) (le_of_lt hJ)))

Premises used: le_of_lt, Ideal.comap_mono, sup_le, le_of_eq, bot_le, rfl, le_trans
-- Module: Mathlib.RingTheory.Ideal.Maps
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

Tactic:
exact le_trans this (sup_le (le_of_eq rfl) (le_trans (comap_mono bot_le) (le_of_lt hJ)))

Premises used: le_of_lt, Ideal.comap_mono, sup_le, le_of_eq, bot_le, rfl, le_trans
-- Module: Mathlib.RingTheory.Ideal.Maps
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
suffices : Eq.{v + 1} (α := Ideal S) (map f J) ⊤
⊢ 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)))
-- Module: Mathlib.RingTheory.Ideal.Maps
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) ⊤

Tactic:
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) ?_))

Premises used: trans, le_of_lt, Ideal.map, Ideal.le_map_of_comap_le_of_surjective, congr_arg, And.right, Ideal.IsMaximal.out, Ideal.comap, ne_of_lt, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.Ideal.Maps
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
f₁ : ∀ (h : K = map f J), comap f (map f J) = J
⊢ Eq.{v + 1} (α := Ideal S) (map f 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) ?_))

Premises used: trans, le_of_lt, Ideal.map, Ideal.le_map_of_comap_le_of_surjective, congr_arg, And.right, Ideal.IsMaximal.out, Ideal.comap, ne_of_lt, lt_of_le_of_ne
-- Module: Mathlib.RingTheory.Ideal.Maps
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
rw : comap f ⊥ ≤ J
⊢ comap f (map f J) = J

Tactic:
rw [comap_map_of_surjective _ hf, sup_eq_left]

Premises used: sup_eq_left, Ideal.comap_map_of_surjective
-- Module: Mathlib.RingTheory.Ideal.Maps
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 ⊥ ≤ J

Tactic:
le_trans (comap_mono bot_le) (le_of_lt hJ)

Premises used: le_of_lt, Ideal.comap_mono, bot_le, le_trans
-- Module: Mathlib.RingTheory.Ideal.Maps
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 ⊥ ≤ J

Tactic:
exact le_trans (comap_mono bot_le) (le_of_lt hJ)

Premises used: le_of_lt, Ideal.comap_mono, bot_le, le_trans
-- Module: Mathlib.RingTheory.Ideal.Maps
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
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)
⊢ Membership.mem (α := S) (HMul.hMul (α := Ideal S) (map f I) (map f J)) ((f : (a : R) → S) (r * s) : S)

Tactic:
rw [map_mul]

Premises used: map_mul
-- Module: Mathlib.RingTheory.Ideal.Maps
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
⊢ 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:
mul_mem_mul (mem_map_of_mem f hri) (mem_map_of_mem f hsj)

Premises used: Ideal.mem_map_of_mem, Set.Mem, Ideal.mul_mem_mul
-- Module: Mathlib.RingTheory.Ideal.Maps
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
⊢ 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:
exact mul_mem_mul (mem_map_of_mem f hri) (mem_map_of_mem f hsj)

Premises used: Ideal.mem_map_of_mem, Ideal.mul_mem_mul
-- Module: Mathlib.RingTheory.Ideal.Maps
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)
simp_rw : Membership.mem (α := S) (↑(map f (I * J)) : Set S) ((f : (a : R) → S) (r * s) : S)
⊢ (fun (x1 x2 : S) ↦ x1 * x2) ((f : (a : R) → S) r) ((f : (a : R) → S) s) ∈ (↑(map f (I * J)) : Set S)

Tactic:
simp_rw [← map_mul]

Premises used: map_mul
-- Module: Mathlib.RingTheory.Ideal.Maps
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)
⊢ Membership.mem (α := S) (↑(map f (I * J)) : Set S) ((f : (a : R) → S) (r * s) : S)

Tactic:
mem_map_of_mem f (mul_mem_mul hri hsj)

Premises used: Ideal.mem_map_of_mem, Ideal.mul_mem_mul
-- Module: Mathlib.RingTheory.Ideal.Maps
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)
⊢ Membership.mem (α := S) (↑(map f (I * J)) : Set S) ((f : (a : R) → S) (r * s) : S)

Tactic:
exact mem_map_of_mem f (mul_mem_mul hri hsj)

Premises used: Ideal.mem_map_of_mem, Ideal.mul_mem_mul
-- Module: Mathlib.RingTheory.Ideal.Maps
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
I J : Ideal R
K L : Ideal S
⊢ Eq.{v + 1} (α := Ideal S) (map.{u, v, u_1} (R := R) f 1) 1

Tactic:
simp only [one_eq_top, Ideal.map_top f]

Premises used: Ideal.one_eq_top, Ideal.map_top
-- Module: Mathlib.RingTheory.Ideal.Maps
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
I : Ideal R
n : ℕ
⊢ map f (I ^ n) = HPow.hPow (α := Ideal S) (map f I) n

Tactic:
map_pow (mapHom f) I n

Premises used: Set.Mem, setOf, Ideal.map, map_pow, Submodule.span, Ideal.mapHom
-- Module: Mathlib.RingTheory.Ideal.Maps
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
h :
  ∀ (x : R), Membership.mem (γ := Ideal R) (comap f K.radical) x ↔ Membership.mem (γ := Ideal R) (radical (comap f K)) x
⊢ Eq (α := Ideal R) (comap f K.radical) (radical (comap f K))

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Maps
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
x : R
⊢ Membership.mem (γ := Ideal R) (comap f K.radical) x ↔ Membership.mem (γ := Ideal R) (radical (comap f K)) x

Tactic:
simp [radical]

Premises used: Ideal.radical