awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
s : Set (Ideal R)
⊢ Eq.{v + 1} (α := Ideal S) (map f (sSup s)) (⨆ I ∈ s, map f I)

Tactic:
(gc_map_comap f : GaloisConnection (map f) (comap f)).l_sSup

Premises used: GaloisConnection.l_sSup, Ideal.gc_map_comap
-- 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
s : Set (Ideal S)
⊢ Eq (α := Ideal R) (comap f (sInf s)) (⨅ I ∈ s, comap f I)

Tactic:
(gc_map_comap f : GaloisConnection (map f) (comap f)).u_sInf

Premises used: GaloisConnection.u_sInf, Ideal.gc_map_comap
-- 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
s : Set (Ideal S)
rw rw₁ : Eq.{u + 1} (α := Ideal R) (⨅ I ∈ s, comap f I) (⨅ b ∈ s, comap f b)
⊢ Eq.{u + 1} (α := Ideal R) (⨅ I ∈ s, comap f I)
    (⨅ (I : Ideal R), ⨅ (_ : Membership.mem (γ := Set (Ideal R)) (comap f '' s) I), I)

Tactic:
rw [iInf_image]

Premises used: iInf_image
-- 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
K : Ideal S
inst_3 : RingHomClass F R S
H : K.IsPrime
⊢ IsPrime (comap f K)

Tactic:
H.comap f

Premises used: Ideal.IsPrime.comap
-- 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 J : Ideal R
inst_3 : RingHomClass F R S
⊢ LE.le.{v} (α := Ideal S) (map f (I ⊓ J)) (map f I ⊓ map f J)

Tactic:
(gc_map_comap f : GaloisConnection (map f) (comap f)).monotone_l.map_inf_le _ _

Premises used: Set.Mem, setOf, Monotone.map_inf_le, GaloisConnection.monotone_l, Ideal.gc_map_comap
-- 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
K L : Ideal S
inst_3 : RingHomClass F R S
⊢ LE.le (α := Ideal R) (comap f K ⊔ comap f L) (comap f (K ⊔ L))

Tactic:
(gc_map_comap f : GaloisConnection (map f) (comap f)).monotone_u.le_map_sup _ _

Premises used: GaloisConnection.monotone_u, Monotone.le_map_sup, Ideal.gc_map_comap
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_4
S : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
r : R
N : Submodule S M
⊢ Submodule.restrictScalars R (HSMul.hSMul.{u_5, u_6, u_6} (α := S) ((algebraMap R S : (a : R) → S) r : S) N) =
    HSMul.hSMul (β := Submodule R M) r (Submodule.restrictScalars R N)

Tactic:
SetLike.coe_injective (congrArg (· '' _) (funext (algebraMap_smul S r)))

Premises used: congrArg, algebraMap_smul, SetLike.coe_injective, funext, Set.image
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_4
S : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
I : Ideal R
N : Submodule S M
simp_rw :
  Eq.{u_6 + 1} (α := Submodule R M)
    (Submodule.restrictScalars.{u_4, u_5, u_6} R (R := S)
      (⨆ b ∈ (↑I : Set R), HSMul.hSMul.{u_5, u_6, u_6} (α := S) ((algebraMap R S : (a : R) → S) b : S) N))
    (⨆ a ∈ (↑I : Set R),
      Submodule.restrictScalars R (HSMul.hSMul.{u_5, u_6, u_6} (α := S) ((algebraMap R S : (a : R) → S) a : S) N))
⊢ Submodule.restrictScalars R (HSMul.hSMul.{u_5, u_6, u_6} (α := Ideal S) (map (F := R →+* S) (algebraMap R S) I) N) =
    HSMul.hSMul (β := Submodule R M) I (Submodule.restrictScalars R N)

Tactic:
simp_rw [map, Submodule.span_smul_eq, ← Submodule.coe_set_smul,
    Submodule.set_smul_eq_iSup, ← element_smul_restrictScalars, iSup_image]

Premises used: iSup_image, element_smul_restrictScalars, Ideal.map, Submodule.set_smul_eq_iSup, Submodule.span_smul_eq, Submodule.coe_set_smul
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_4
S : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
I : Ideal R
N : Submodule S M
⊢ Eq.{u_6 + 1} (α := Submodule R M)
    (Submodule.restrictScalars.{u_4, u_5, u_6} R (R := S)
      (⨆ b ∈ (↑I : Set R), HSMul.hSMul.{u_5, u_6, u_6} (α := S) ((algebraMap R S : (a : R) → S) b : S) N))
    (⨆ a ∈ (↑I : Set R),
      Submodule.restrictScalars R (HSMul.hSMul.{u_5, u_6, u_6} (α := S) ((algebraMap R S : (a : R) → S) a : S) N))

Tactic:
map_iSup₂ (Submodule.restrictScalarsLatticeHom R S M) _

Premises used: Set.Mem, Submodule.restrictScalars, setOf, Submodule.restrictScalarsLatticeHom, map_iSup₂
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_4
S : Type u_5
M : Type u_6
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
I : Ideal R
N : Submodule S M
⊢ Eq.{u_6 + 1} (α := Submodule R M)
    (Submodule.restrictScalars.{u_4, u_5, u_6} R (R := S)
      (⨆ b ∈ (↑I : Set R), HSMul.hSMul.{u_5, u_6, u_6} (α := S) ((algebraMap R S : (a : R) → S) b : S) N))
    (⨆ a ∈ (↑I : Set R),
      Submodule.restrictScalars R (HSMul.hSMul.{u_5, u_6, u_6} (α := S) ((algebraMap R S : (a : R) → S) a : S) N))

Tactic:
exact map_iSup₂ (Submodule.restrictScalarsLatticeHom R S M) _

Premises used: Submodule.restrictScalarsLatticeHom, map_iSup₂
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
I : Ideal R
⊢ HSMul.hSMul (β := Submodule R S) I ⊤ = Submodule.restrictScalars R (map (F := R →+* S) (algebraMap R S) I)

Tactic:
Eq.trans (smul_restrictScalars I (⊤ : Ideal S)).symm <|
    congrArg _ <| Eq.trans (Ideal.smul_eq_mul _ _) (Ideal.mul_top _)

Premises used: congrArg, Ideal.smul_eq_mul, Ideal.smul_restrictScalars, Ideal.mul_top, Top.top, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_4
S : Type u_5
inst : Semiring R
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
I : Ideal S
⊢ (↑(Submodule.restrictScalars R I) : Set S) = (↑I : Set S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_4
S : Type u_5
inst : Semiring R
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
I J : Ideal S
⊢ Submodule.restrictScalars R (I * J) =
    HMul.hMul (α := Submodule R S) (Submodule.restrictScalars R I) (Submodule.restrictScalars R J)

Tactic:
rfl

Premises used: iInf, Set.Mem, iSup, Set.iInter, Submodule.restrictScalars, setOf, rfl
-- 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 : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal S
⊢ map f (comap f I) = I

Tactic:
le_antisymm (map_le_iff_le_comap.2 le_rfl) fun s hsi =>
    let ⟨r, hfrs⟩ := hf s
    hfrs ▸ (mem_map_of_mem f <| show f r ∈ I from hfrs.symm ▸ hsi)

Premises used: Iff.mpr, le_rfl, _private.0.Ideal.map_comap_of_surjective.match_1, Ideal.mem_map_of_mem, Membership.mem, Eq.rec, Ideal.map, Ideal.map_le_iff_le_comap, le_antisymm, Ideal.comap, Eq.symm
-- 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 : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ Surjective.{u + 1, v + 1} (α := Ideal R) (β := Ideal S) (map f)

Tactic:
(giMapComap f hf).l_surjective

Premises used: Ideal.giMapComap, GaloisInsertion.l_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 : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ Injective (α := Ideal S) (β := Ideal R) (comap f)

Tactic:
(giMapComap f hf).u_injective

Premises used: Ideal.giMapComap, GaloisInsertion.u_injective
-- 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 : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I J : Ideal S
⊢ map f (comap f I ⊔ comap f J) = I ⊔ J

Tactic:
(giMapComap f hf).l_sup_u _ _

Premises used: GaloisInsertion.l_sup_u, Ideal.giMapComap
-- 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
ι : Sort u_3
hf : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
K : ι → Ideal S
⊢ map.{u, v, u_1} (R := R) f (⨆ (i : ι), comap f (K i)) = iSup K

Tactic:
(giMapComap f hf).l_iSup_u _

Premises used: Ideal.giMapComap, GaloisInsertion.l_iSup_u
-- 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 : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I J : Ideal S
⊢ map f (comap f I ⊓ comap f J) = I ⊓ J

Tactic:
(giMapComap f hf).l_inf_u _ _

Premises used: Ideal.giMapComap, GaloisInsertion.l_inf_u
-- 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
ι : Sort u_3
hf : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
K : ι → Ideal S
⊢ map.{u, v, u_1} (R := R) f (⨅ (i : ι), comap f (K i)) = iInf K

Tactic:
(giMapComap f hf).l_iInf_u _

Premises used: Ideal.giMapComap, GaloisInsertion.l_iInf_u
-- 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 : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
y : S
H : Membership.mem (γ := Ideal S) (map f I) y
⊢ Membership.mem (γ := Set S) ((⇑f : (a : R) → S) '' (↑I : Set R)) y

Tactic:
Submodule.span_induction (hx := H) (fun _ => id) ⟨0, I.zero_mem, map_zero f⟩
    (fun _ _ _ _ ⟨x1, hx1i, hxy1⟩ ⟨x2, hx2i, hxy2⟩ =>
      ⟨x1 + x2, I.add_mem hx1i hx2i, hxy1 ▸ hxy2 ▸ map_add f _ _⟩)
    fun c _ _ ⟨x, hxi, hxy⟩ =>
    let ⟨d, hdc⟩ := hf c
    ⟨d * x, I.mul_mem_left _ hxi, hdc ▸ hxy ▸ map_mul f _ _⟩

Premises used: Submodule.span_induction
-- 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 : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
y : S
⊢ Membership.mem (γ := Ideal S) (map f I) y ↔ ∃ x ∈ I, (f : (a : R) → S) x = y

Tactic:
⟨fun h => (Set.mem_image _ _ _).2 (mem_image_of_mem_map_of_surjective f hf h), fun ⟨_, hx⟩ =>
    hx.right ▸ mem_map_of_mem f hx.left⟩

Premises used: Ideal.mem_image_of_mem_map_of_surjective, Iff.mpr, Ideal.mem_map_of_mem, Set.mem_image, Membership.mem, Eq.rec, Ideal.map, SetLike.coe, And.right, _private.0.Ideal.mem_map_iff_of_surjective.match_1, And.left, Iff.intro, DFunLike.coe
-- 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 : Ideal R
K : Ideal S
inst_3 : RingHomClass F R S
hf : Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ comap f K ≤ I → K ≤ map f I

Tactic:
fun h =>
  map_comap_of_surjective f hf K ▸ map_mono h

Premises used: Eq.rec, Ideal.map_mono, Ideal.map_comap_of_surjective
-- 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 S
⊢ map e (comap e I) = I

Tactic:
I.map_comap_of_surjective e (EquivLike.surjective e)

Premises used: EquivLike.surjective, Ideal.map_comap_of_surjective
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
h : RingHomSurjective f
I : Ideal R
⊢ map f I = Submodule.map f.toSemilinearMap I

Tactic:
Submodule.ext fun _ => mem_map_iff_of_surjective f h.1

Premises used: Ideal.mem_map_iff_of_surjective, Submodule.ext, RingHomSurjective.is_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_1 : F
I_1 J : Ideal R
K L : Ideal S
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass F R S
ι : Sort u_3
f : R →+* S
inst_5 : RingHomSurjective f
I : Ideal R
inst_6 : I.IsTwoSided
a b : S
ha : Membership.mem (γ := Ideal S) (map f I) a
rw : ∀ (ha : a ∈ Submodule.map f.toSemilinearMap I), a * b ∈ Submodule.map f.toSemilinearMap I
⊢ Membership.mem (γ := Ideal S) (map f I) (a * b)

Tactic:
rw [map_eq_submodule_map] at ha ⊢

Premises used: Ideal.map_eq_submodule_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_1 : F
I_1 J : Ideal R
K L : Ideal S
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass F R S
ι : Sort u_3
f : R →+* S
inst_5 : RingHomSurjective f
I : Ideal R
inst_6 : I.IsTwoSided
a b : S
ha : a ∈ Submodule.map f.toSemilinearMap I
obtain :
  ∀ (a : R) (ha : a ∈ (↑I : Set R)),
    HMul.hMul (α := S) ((f.toSemilinearMap : (a : R) → S) a : S) b ∈ Submodule.map f.toSemilinearMap I
⊢ a * b ∈ Submodule.map f.toSemilinearMap I

Tactic:
obtain ⟨a, ha, rfl⟩ := ha

Premises used: rfl
-- 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_1 : F
I_1 J : Ideal R
K L : Ideal S
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass F R S
ι : Sort u_3
f : R →+* S
inst_5 : RingHomSurjective f
I : Ideal R
inst_6 : I.IsTwoSided
b : S
a : R
ha : a ∈ (↑I : Set R)
obtain :
  ∀ (b : R),
    HMul.hMul (α := S) (β := S) ((f.toSemilinearMap : (a : R) → S) a : S) ((f : (a : R) → S) b : S) ∈
      Submodule.map f.toSemilinearMap I
⊢ HMul.hMul (α := S) ((f.toSemilinearMap : (a : R) → S) a : S) b ∈ Submodule.map f.toSemilinearMap I

Tactic:
obtain ⟨b, rfl⟩ := f.surjective b

Premises used: RingHom.surjective, rfl
-- 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_1 : F
I_1 J : Ideal R
K L : Ideal S
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass F R S
ι : Sort u_3
f : R →+* S
inst_5 : RingHomSurjective f
I : Ideal R
inst_6 : I.IsTwoSided
a : R
ha : a ∈ (↑I : Set R)
b : R
rw : Membership.mem (α := S) (Submodule.map f.toSemilinearMap I) ((f : (a : R) → S) (a * b) : S)
⊢ HMul.hMul (α := S) (β := S) ((f.toSemilinearMap : (a : R) → S) a : S) ((f : (a : R) → S) b : S) ∈
    Submodule.map f.toSemilinearMap I

Tactic:
rw [RingHom.coe_toSemilinearMap, ← map_mul]

Premises used: map_mul, RingHom.coe_toSemilinearMap
-- 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_1 : F
I_1 J : Ideal R
K L : Ideal S
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass F R S
ι : Sort u_3
f : R →+* S
inst_5 : RingHomSurjective f
I : Ideal R
inst_6 : I.IsTwoSided
a : R
ha : a ∈ (↑I : Set R)
b : R
⊢ Membership.mem (α := S) (Submodule.map f.toSemilinearMap I) ((f : (a : R) → S) (a * b) : S)

Tactic:
⟨_, I.mul_mem_right _ ha, rfl⟩

Premises used: Set.Mem, setOf, Ideal.mul_mem_right, And.intro, Exists.intro, Set.image, rfl
-- 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_1 : F
I_1 J : Ideal R
K L : Ideal S
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass F R S
ι : Sort u_3
f : R →+* S
inst_5 : RingHomSurjective f
I : Ideal R
inst_6 : I.IsTwoSided
a : R
ha : a ∈ (↑I : Set R)
b : R
⊢ Membership.mem (α := S) (Submodule.map f.toSemilinearMap I) ((f : (a : R) → S) (a * b) : S)

Tactic:
exact ⟨_, I.mul_mem_right _ ha, rfl⟩
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
⊢ IsMaximal (comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I)

Tactic:
isMaximal_iff.mpr ⟨I.ne_top_iff_one.mp h.ne_top, fun J x le hxI hxJ ↦ ?_⟩

Premises used: Iff.mpr, Ideal.ne_top_iff_one, Ideal.isMaximal_iff, And.intro, Iff.mp, Ideal.IsMaximal.ne_top
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
refine :
  ∀ (J : Ideal ((i : ι) → R i)) (x : (i : ι) → R i)
    (le : comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I ≤ J)
    (hxI : x ∉ comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I) (hxJ : x ∈ J), 1 ∈ J
⊢ IsMaximal (comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I)

Tactic:
refine isMaximal_iff.mpr ⟨I.ne_top_iff_one.mp h.ne_top, fun J x le hxI hxJ ↦ ?_⟩

Premises used: Iff.mpr, Ideal.ne_top_iff_one, Ideal.isMaximal_iff, And.intro, Iff.mp, Ideal.IsMaximal.ne_top
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
le : comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I ≤ J
hxI : x ∉ comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I
hxJ : x ∈ J
have :
  ∀ (r y : R i) (hy : y ∈ I)
    (eq : HMul.hMul (β := R i) r ((Pi.evalRingHom R i : (a : (i : ι) → R i) → R i) x : R i) + y = 1), 1 ∈ J
⊢ 1 ∈ J

Tactic:
have ⟨r, y, hy, eq⟩ := h.exists_inv hxI
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
le : comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I ≤ J
hxI : x ∉ comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I
hxJ : x ∈ J
r y : R i
hy : y ∈ I
eq : HMul.hMul (β := R i) r ((Pi.evalRingHom R i : (a : (i : ι) → R i) → R i) x : R i) + y = 1
⊢ Membership.mem (γ := Submodule ((i : ι) → R i) ((i : ι) → R i))
    (comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I) (update (β := R) 1 i y)

Tactic:
apply update_self i y 1 ▸ hy
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
le : comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I ≤ J
hxI : x ∉ comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I
hxJ : x ∈ J
r y : R i
hy : y ∈ I
eq : HMul.hMul (β := R i) r ((Pi.evalRingHom R i : (a : (i : ι) → R i) → R i) x : R i) + y = 1
h₁ : 1 = update (β := R) 0 i r * x + update (β := R) 1 i y
⊢ 1 ∈ J

Tactic:
convert!
    J.add_mem (J.mul_mem_left (update 0 i r) hxJ) (b := update 1 i y)
      (le <| by apply update_self i y 1 ▸ hy)

Premises used: Function.update, Ideal.add_mem, Ideal.mul_mem_left, OfNat.ofNat
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
le : comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I ≤ J
hxI : x ∉ comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I
hxJ : x ∈ J
r y : R i
hy : y ∈ I
eq : HMul.hMul (β := R i) r ((Pi.evalRingHom R i : (a : (i : ι) → R i) → R i) x : R i) + y = 1
h₁ : ∀ (j : ι), 1 j = (update (β := R) 0 i r * x + update (β := R) 1 i y) j
⊢ 1 = update (β := R) 0 i r * x + update (β := R) 1 i y

Tactic:
ext j
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
le : comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I ≤ J
hxI : x ∉ comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I
hxJ : x ∈ J
r y : R i
hy : y ∈ I
eq : HMul.hMul (β := R i) r ((Pi.evalRingHom R i : (a : (i : ι) → R i) → R i) x : R i) + y = 1
j : ι
h₁ :
  ∀ {I : Ideal (R j)} (h : I.IsMaximal) (le : comap (F := ((i : ι) → R i) →+* R j) (Pi.evalRingHom R j) I ≤ J)
    (hxI : x ∉ comap (F := ((i : ι) → R i) →+* R j) (Pi.evalRingHom R j) I) (r y : R j) (hy : y ∈ I)
    (eq : HMul.hMul (β := R j) r ((Pi.evalRingHom R j : (a : (i : ι) → R i) → R j) x : R j) + y = 1),
    1 j = (update (β := R) 0 j r * x + update (β := R) 1 j y) j
h₂ : ∀ (ne : j ≠ i), 1 j = (update (β := R) 0 i r * x + update (β := R) 1 i y) j
⊢ 1 j = (update (β := R) 0 i r * x + update (β := R) 1 i y) j

Tactic:
obtain rfl | ne := eq_or_ne j i

Premises used: eq_or_ne, rfl
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
hxJ : x ∈ J
j : ι
I : Ideal (R j)
h : I.IsMaximal
le : comap (F := ((i : ι) → R i) →+* R j) (Pi.evalRingHom R j) I ≤ J
hxI : x ∉ comap (F := ((i : ι) → R i) →+* R j) (Pi.evalRingHom R j) I
r y : R j
hy : y ∈ I
eq : HMul.hMul (β := R j) r ((Pi.evalRingHom R j : (a : (i : ι) → R i) → R j) x : R j) + y = 1
⊢ 1 j = (update (β := R) 0 j r * x + update (β := R) 1 j y) j

Tactic:
simpa [eq_comm] using eq

Premises used: eq_comm
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
le : comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I ≤ J
hxI : x ∉ comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I
hxJ : x ∈ J
r y : R i
hy : y ∈ I
eq : HMul.hMul (β := R i) r ((Pi.evalRingHom R i : (a : (i : ι) → R i) → R i) x : R i) + y = 1
j : ι
ne : j ≠ i
⊢ 1 j = (update (β := R) 0 i r * x + update (β := R) 1 i y) j

Tactic:
simp [update_of_ne ne]

Premises used: Function.update_of_ne
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
le : comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I ≤ J
hxI : x ∉ comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I
hxJ : x ∈ J
r y : R i
hy : y ∈ I
eq : HMul.hMul (β := R i) r ((Pi.evalRingHom R i : (a : (i : ι) → R i) → R i) x : R i) + y = 1
h₁ : 1 = update (β := R) 0 i r * x + update (β := R) 1 i y
h₂ : ∀ (j : ι), 1 j = (update (β := R) 0 i r * x + update (β := R) 1 i y) j
h₃ :
  ∀ (j : ι) {I : Ideal (R j)} (h : I.IsMaximal) (le : comap (F := ((i : ι) → R i) →+* R j) (Pi.evalRingHom R j) I ≤ J)
    (hxI : x ∉ comap (F := ((i : ι) → R i) →+* R j) (Pi.evalRingHom R j) I) (r y : R j) (hy : y ∈ I)
    (eq : HMul.hMul (β := R j) r ((Pi.evalRingHom R j : (a : (i : ι) → R i) → R j) x : R j) + y = 1),
    1 j = (update (β := R) 0 j r * x + update (β := R) 1 j y) j
h₄ h₅ : ∀ (j : ι) (ne : j ≠ i), 1 j = (update (β := R) 0 i r * x + update (β := R) 1 i y) j
⊢ 1 ∈ J

Tactic:
classical
  convert!
    J.add_mem (J.mul_mem_left (update 0 i r) hxJ) (b := update 1 i y)
      (le <| by apply update_self i y 1 ▸ hy)
  ext j
  obtain rfl | ne := eq_or_ne j i
  · simpa [eq_comm] using eq
  · simp [update_of_ne ne]

Premises used: eq_comm, rfl
-- 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)
I J : Ideal S
⊢ LE.le (α := Ideal R) (comap f I) (comap f J) ↔ I ≤ J

Tactic:
⟨fun h => (map_comap_of_surjective f hf I).symm.le.trans (map_le_of_le_comap h), fun h =>
    le_comap_of_map_le ((map_comap_of_surjective f hf I).le.trans h)⟩

Premises used: Ideal.le_comap_of_map_le, Eq.le, Iff.intro, Ideal.map_le_of_le_comap, LE.le.trans, Eq.symm, Ideal.map_comap_of_surjective