awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : ∀ J ∈ A, RingHom.ker f ≤ J
y : S
hy : Membership.mem (γ := Submodule S S) (sInf (map f '' A)) y
x : R
hx : (f : (a : R) → S) x = y
this : ∀ I ∈ A, Membership.mem (γ := Ideal S) (map f I) y
refine_2 : ∀ p ∈ A, x ∈ p
⊢ x ∈ sInf A

Tactic:
rw [Submodule.mem_sInf]

Premises used: Submodule.mem_sInf
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : ∀ J ∈ A, RingHom.ker f ≤ J
y : S
hy : Membership.mem (γ := Submodule S S) (sInf (map f '' A)) y
x : R
hx : (f : (a : R) → S) x = y
this : ∀ I ∈ A, Membership.mem (γ := Ideal S) (map f I) y
J : Submodule R R
hJ : J ∈ A
refine_2 :
  ∀ (x' : R) (hx' : x' ∈ J)
    (hy : Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (sInf (map f '' A)) ((f : (a : R) → S) x' : S))
    (hx : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) x' : S))
    (this : ∀ I ∈ A, Membership.mem.{u_2, u_2} (α := S) (γ := Ideal S) (map f I) ((f : (a : R) → S) x' : S)), x ∈ J
⊢ x ∈ J

Tactic:
rcases (mem_map_iff_of_surjective f hf).1 (this J hJ) with ⟨x', hx', rfl⟩

Premises used: Iff.mp, Ideal.mem_map_iff_of_surjective, rfl
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : ∀ J ∈ A, RingHom.ker f ≤ J
x : R
J : Submodule R R
hJ : J ∈ A
x' : R
hx' : x' ∈ J
hy : Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (sInf (map f '' A)) ((f : (a : R) → S) x' : S)
hx : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) x' : S)
this : ∀ I ∈ A, Membership.mem.{u_2, u_2} (α := S) (γ := Ideal S) (map f I) ((f : (a : R) → S) x' : S)
a : Membership.mem (γ := Submodule R R) (RingHom.ker f) (x - x')
⊢ x - x' ∈ J

Tactic:
apply h J hJ
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : ∀ J ∈ A, RingHom.ker f ≤ J
x : R
J : Submodule R R
hJ : J ∈ A
x' : R
hx' : x' ∈ J
hy : Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (sInf (map f '' A)) ((f : (a : R) → S) x' : S)
hx : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) x' : S)
this : ∀ I ∈ A, Membership.mem.{u_2, u_2} (α := S) (γ := Ideal S) (map f I) ((f : (a : R) → S) x' : S)
a : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (x - x') : S) (0 : S)
a₁ : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) x' : S) = 0
a₂ : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) x' : S) ((f : (a : R) → S) x' : S) = 0
a₃ a₄ : Eq.{u_2 + 1} (α := S) 0 0
⊢ Membership.mem (γ := Submodule R R) (RingHom.ker f) (x - x')

Tactic:
rw [RingHom.mem_ker, map_sub, hx, sub_self]

Premises used: map_sub, sub_self, RingHom.mem_ker
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : ∀ J ∈ A, RingHom.ker f ≤ J
x : R
J : Submodule R R
hJ : J ∈ A
x' : R
hx' : x' ∈ J
hy : Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (sInf (map f '' A)) ((f : (a : R) → S) x' : S)
hx : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) x' : S)
this : ∀ I ∈ A, Membership.mem.{u_2, u_2} (α := S) (γ := Ideal S) (map f I) ((f : (a : R) → S) x' : S)
⊢ x - x' ∈ J

Tactic:
have : x - x' ∈ J := by
      apply h J hJ
      rw [RingHom.mem_ker, map_sub, hx, sub_self]
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
A : Set (Ideal R)
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : ∀ J ∈ A, RingHom.ker f ≤ J
x : R
J : Submodule R R
hJ : J ∈ A
x' : R
hx' : x' ∈ J
hy : Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (sInf (map f '' A)) ((f : (a : R) → S) x' : S)
hx : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) x' : S)
this_1 : ∀ I ∈ A, Membership.mem.{u_2, u_2} (α := S) (γ := Ideal S) (map f I) ((f : (a : R) → S) x' : S)
this : x - x' ∈ J
⊢ x ∈ J

Tactic:
simpa only [sub_add_cancel] using J.add_mem this hx'

Premises used: sub_add_cancel, Submodule.add_mem
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
⊢ IsPrime.{u_2} (α := S) (map f I)

Tactic:
⟨fun h => H.ne_top (eq_top_iff.2 ?_), fun {x y} => ?_⟩

Premises used: Iff.mpr, eq_top_iff, Ideal.IsPrime.mk, Ideal.IsPrime.ne_top
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
refine_1 : ∀ (h : Eq.{u_2 + 1} (α := Ideal S) (map f I) ⊤), ⊤ ≤ I
refine_2 :
  ∀ {x y : S},
    Membership.mem (γ := Ideal S) (map f I) (x * y) →
      Membership.mem (γ := Ideal S) (map f I) x ∨ Membership.mem (γ := Ideal S) (map f I) y
⊢ IsPrime.{u_2} (α := S) (map f I)

Tactic:
refine ⟨fun h => H.ne_top (eq_top_iff.2 ?_), fun {x y} => ?_⟩
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
h : Eq.{u_2 + 1} (α := Ideal S) (map f I) ⊤
⊢ Eq (α := Ideal R) (comap f (map f I)) (comap f ⊤)

Tactic:
replace h := congr_arg (comap f) h
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
h : Eq (α := Ideal R) (comap f (map f I)) (comap f ⊤)
⊢ I ⊔ comap f ⊥ = ⊤

Tactic:
rw [comap_map_of_surjective _ hf, comap_top] at h

Premises used: Ideal.comap_map_of_surjective, Ideal.comap_top
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
h : I ⊔ comap f ⊥ = ⊤
⊢ ⊤ ≤ I

Tactic:
h ▸ sup_le (le_of_eq rfl) hk

Premises used: Set.Mem, Eq.rec, sup_le, le_of_eq, rfl
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
h : I ⊔ comap f ⊥ = ⊤
⊢ ⊤ ≤ I

Tactic:
exact h ▸ sup_le (le_of_eq rfl) hk
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
⊢ Membership.mem (γ := Ideal S) (map f I) (x * y) →
    Membership.mem (γ := Ideal S) (map f I) x ∨ Membership.mem (γ := Ideal S) (map f I) y

Tactic:
fun hxy => (hf x).recOn fun a ha => (hf y).recOn fun b hb => ?_

Premises used: Exists.recOn
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
refine_2 :
  ∀ (hxy : Membership.mem (γ := Ideal S) (map f I) (x * y)) (a : R) (ha : (f : (a : R) → S) a = x) (b : R)
    (hb : (f : (a : R) → S) b = y),
    Membership.mem (γ := Ideal S) (map f I) x ∨ Membership.mem (γ := Ideal S) (map f I) y
⊢ Membership.mem (γ := Ideal S) (map f I) (x * y) →
    Membership.mem (γ := Ideal S) (map f I) x ∨ Membership.mem (γ := Ideal S) (map f I) y

Tactic:
refine fun hxy => (hf x).recOn fun a ha => (hf y).recOn fun b hb => ?_
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
hxy : Membership.mem (γ := Ideal S) (map f I) (x * y)
a : R
ha : (f : (a : R) → S) a = x
b : R
hb : (f : (a : R) → S) b = y
refine_2 :
  ∀ (ha : (f : (a : R) → S) a = x) (b : R)
    (hxy : ∃ x ∈ I, Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) (a * b) : S))
    (hb : (f : (a : R) → S) b = y),
    Membership.mem (γ := Ideal S) (map f I) x ∨ Membership.mem (γ := Ideal S) (map f I) y
⊢ Membership.mem (γ := Ideal S) (map f I) x ∨ Membership.mem (γ := Ideal S) (map f I) y

Tactic:
rw [← ha, ← hb, ← map_mul f, mem_map_iff_of_surjective _ hf] at hxy

Premises used: map_mul, Ideal.mem_map_iff_of_surjective
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : (f : (a : R) → S) a = x
b : R
hxy : ∃ x ∈ I, Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) (a * b) : S)
hb : (f : (a : R) → S) b = y
refine_2 :
  ∀ (c : R) (hc : c ∈ I) (hc' : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) c : S) ((f : (a : R) → S) (a * b) : S)),
    Membership.mem (γ := Ideal S) (map f I) x ∨ Membership.mem (γ := Ideal S) (map f I) y
⊢ Membership.mem (γ := Ideal S) (map f I) x ∨ Membership.mem (γ := Ideal S) (map f I) y

Tactic:
rcases hxy with ⟨c, hc, hc'⟩
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : (f : (a : R) → S) a = x
b : R
hb : (f : (a : R) → S) b = y
c : R
hc : c ∈ I
hc' : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) c : S) ((f : (a : R) → S) (a * b) : S)
⊢ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (c - a * b) : S) (0 : S)

Tactic:
rw [← sub_eq_zero, ← map_sub] at hc'

Premises used: map_sub, sub_eq_zero
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : (f : (a : R) → S) a = x
b : R
hb : (f : (a : R) → S) b = y
c : R
hc : c ∈ I
hc' : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (c - a * b) : S) (0 : S)
⊢ c - (c - a * b) ∈ I

Tactic:
I.sub_mem hc (hk (hc' : c - a * b ∈ RingHom.ker f))

Premises used: Ideal.sub_mem
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : (f : (a : R) → S) a = x
b : R
hb : (f : (a : R) → S) b = y
c : R
hc : c ∈ I
hc' : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (c - a * b) : S) (0 : S)
h : a * b = c - (c - a * b)
⊢ a * b ∈ I

Tactic:
convert! I.sub_mem hc (hk (hc' : c - a * b ∈ RingHom.ker f)) using 1

Premises used: Ideal.sub_mem
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : (f : (a : R) → S) a = x
b : R
hb : (f : (a : R) → S) b = y
c : R
hc : c ∈ I
hc' : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (c - a * b) : S) (0 : S)
⊢ a * b = c - (c - a * b)

Tactic:
abel
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : (f : (a : R) → S) a = x
b : R
hb : (f : (a : R) → S) b = y
c : R
hc : c ∈ I
hc' : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (c - a * b) : S) (0 : S)
⊢ a * b ∈ I

Tactic:
have : a * b ∈ I := by
      convert! I.sub_mem hc (hk (hc' : c - a * b ∈ RingHom.ker f)) using 1
      abel
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : (f : (a : R) → S) a = x
b : R
hb : (f : (a : R) → S) b = y
c : R
hc : c ∈ I
hc' : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (c - a * b) : S) (0 : S)
this : a * b ∈ I
⊢ Membership.mem (γ := Ideal S) (map f I) x ∨ Membership.mem (γ := Ideal S) (map f I) y

Tactic:
(H.mem_or_mem this).imp (fun h => ha ▸ mem_map_of_mem f h) fun h => hb ▸ mem_map_of_mem f h

Premises used: Ideal.mem_map_of_mem, Eq.rec, Ideal.IsPrime.mem_or_mem, Or.imp
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : (f : (a : R) → S) a = x
b : R
hb : (f : (a : R) → S) b = y
c : R
hc : c ∈ I
hc' : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (c - a * b) : S) (0 : S)
this : a * b ∈ I
⊢ Membership.mem (γ := Ideal S) (map f I) x ∨ Membership.mem (γ := Ideal S) (map f I) y

Tactic:
exact
      (H.mem_or_mem this).imp (fun h => ha ▸ mem_map_of_mem f h) fun h => hb ▸ mem_map_of_mem f h

Premises used: Ideal.IsPrime.mem_or_mem, Or.imp
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
m : Ideal R
inst_3 : m.IsMaximal
hk : RingHom.ker f ≤ m
⊢ IsMaximal.{u_2} (α := S) (map f m)

Tactic:
m.map_eq_top_or_isMaximal_of_surjective f hf ‹_› |>.resolve_left fun h => ?_

Premises used: Ideal.map_eq_top_or_isMaximal_of_surjective, Or.resolve_left
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
m : Ideal R
inst_3 : m.IsMaximal
hk : RingHom.ker f ≤ m
refine : ∀ (h : Eq.{u_2 + 1} (α := Ideal S) (map f m) ⊤), False
⊢ IsMaximal.{u_2} (α := S) (map f m)

Tactic:
refine m.map_eq_top_or_isMaximal_of_surjective f hf ‹_› |>.resolve_left fun h => ?_

Premises used: Ideal.map_eq_top_or_isMaximal_of_surjective, Or.resolve_left
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
m : Ideal R
inst_3 : m.IsMaximal
hk : RingHom.ker f ≤ m
h : Eq.{u_2 + 1} (α := Ideal S) (map f m) ⊤
⊢ Eq (α := Ideal R) (comap f (map f m)) (comap f ⊤)

Tactic:
apply congr_arg (comap f) at h

Premises used: congr_arg, Ideal.comap
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
m : Ideal R
inst_3 : m.IsMaximal
hk : RingHom.ker f ≤ m
h : Eq (α := Ideal R) (comap f (map f m)) (comap f ⊤)
⊢ m = ⊤

Tactic:
rw [comap_map_of_surjective _ hf, comap_top, ← RingHom.ker_eq_comap_bot, sup_of_le_left hk] at h

Premises used: Ideal.comap_map_of_surjective, RingHom.ker_eq_comap_bot, Ideal.comap_top, sup_of_le_left
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
m : Ideal R
inst_3 : m.IsMaximal
hk : RingHom.ker f ≤ m
h : m = ⊤
⊢ False

Tactic:
IsMaximal.ne_top ‹_› h

Premises used: Ideal.IsMaximal.ne_top
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Ring R
inst_1 : Ring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
m : Ideal R
inst_3 : m.IsMaximal
hk : RingHom.ker f ≤ m
h : m = ⊤
⊢ False

Tactic:
exact IsMaximal.ne_top ‹_› h

Premises used: Ideal.IsMaximal.ne_top
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_4
inst_2 : Ring S
inst_3 : Nontrivial S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
I : Ideal R
h : I ≠ ⊥
⊢ Ne.{u_4 + 1} (α := Ideal S) (map (F := R →+* S) (algebraMap R S) I) ⊥

Tactic:
(map_eq_bot_iff_of_injective (FaithfulSMul.algebraMap_injective R S)).mp.mt h

Premises used: Function.mt, Ideal.map_eq_bot_iff_of_injective, FaithfulSMul.algebraMap_injective, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
I J : Ideal R
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
rw : Eq (α := Ideal R) (comap f (map f I)) (comap f (map f J)) ↔ I ⊔ RingHom.ker f = J ⊔ RingHom.ker f
rw₁ : I ⊔ comap f ⊥ = comap f (map f J) ↔ I ⊔ RingHom.ker f = J ⊔ RingHom.ker f
rw₂ : I ⊔ comap f ⊥ = J ⊔ comap f ⊥ ↔ I ⊔ RingHom.ker f = J ⊔ RingHom.ker f
rw₃ rw₄ : I ⊔ comap f ⊥ = J ⊔ comap f ⊥ ↔ I ⊔ comap f ⊥ = J ⊔ comap f ⊥
⊢ Eq.{u_2 + 1} (α := Ideal S) (map f I) (map f J) ↔ I ⊔ RingHom.ker f = J ⊔ RingHom.ker f

Tactic:
rw [← (comap_injective_of_surjective f hf).eq_iff, comap_map_of_surjective f hf,
    comap_map_of_surjective f hf, RingHom.ker_eq_comap_bot]

Premises used: Function.Injective.eq_iff, Ideal.comap_map_of_surjective, RingHom.ker_eq_comap_bot, Ideal.comap_injective_of_surjective
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
h : RingHom.ker f ≤ I
rw :
  Eq.{u_2 + 1} (α := Ideal S) (map (R := R) f (sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}))
    (sInf {J : Ideal S | map f I ≤ J ∧ J.IsPrime})
⊢ Eq.{u_2 + 1} (α := Ideal S) (map f I.radical) (radical (map f I))

Tactic:
rw [radical_eq_sInf, radical_eq_sInf]

Premises used: Ideal.radical_eq_sInf
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
h : RingHom.ker f ≤ I
⊢ ∀ (J : Ideal R), Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsPrime} J → RingHom.ker f ≤ J

Tactic:
have : ∀ J ∈ {J : Ideal R | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J := fun J hJ => h.trans hJ.left
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsPrime} J → RingHom.ker f ≤ J
⊢ Eq.{u_2 + 1} (α := Ideal S) (map (R := R) f (sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}))
    (sInf (Set.image.{u_1, u_2} (α := Ideal R) (map f) {J : Ideal R | I ≤ J ∧ J.IsPrime}))

Tactic:
map_sInf hf this

Premises used: Ideal.map_sInf
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsPrime} J → RingHom.ker f ≤ J
h₁ :
  Eq.{u_2 + 1} (α := Set (Ideal S)) {J : Ideal S | map f I ≤ J ∧ J.IsPrime}
    (Set.image.{u_1, u_2} (α := Ideal R) (map f) {J : Ideal R | I ≤ J ∧ J.IsPrime})
⊢ Eq.{u_2 + 1} (α := Ideal S) (map (R := R) f (sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}))
    (sInf {J : Ideal S | map f I ≤ J ∧ J.IsPrime})

Tactic:
convert! map_sInf hf this

Premises used: Ideal.map_sInf
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsPrime} J → RingHom.ker f ≤ J
h₁ :
  ∀ (j : Ideal S),
    Membership.mem (γ := Set (Ideal S)) {J : Ideal S | map f I ≤ J ∧ J.IsPrime} j ↔
      Membership.mem (γ := Set (Ideal S))
        (Set.image.{u_1, u_2} (α := Ideal R) (map f) {J : Ideal R | I ≤ J ∧ J.IsPrime}) j
⊢ Eq.{u_2 + 1} (α := Set (Ideal S)) {J : Ideal S | map f I ≤ J ∧ J.IsPrime}
    (Set.image.{u_1, u_2} (α := Ideal R) (map f) {J : Ideal R | I ≤ J ∧ J.IsPrime})

Tactic:
ext j
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsPrime} J → RingHom.ker f ≤ J
j : Ideal S
h₁ :
  Membership.mem (γ := Set (Ideal S)) {J : Ideal S | map f I ≤ J ∧ J.IsPrime} j →
    Membership.mem (γ := Set (Ideal S)) (Set.image.{u_1, u_2} (α := Ideal R) (map f) {J : Ideal R | I ≤ J ∧ J.IsPrime})
      j
h₂ :
  Membership.mem (γ := Set (Ideal S)) (Set.image.{u_1, u_2} (α := Ideal R) (map f) {J : Ideal R | I ≤ J ∧ J.IsPrime})
      j →
    Membership.mem (γ := Set (Ideal S)) {J : Ideal S | map f I ≤ J ∧ J.IsPrime} j
⊢ Membership.mem (γ := Set (Ideal S)) {J : Ideal S | map f I ≤ J ∧ J.IsPrime} j ↔
    Membership.mem (γ := Set (Ideal S)) (Set.image.{u_1, u_2} (α := Ideal R) (map f) {J : Ideal R | I ≤ J ∧ J.IsPrime})
      j

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsPrime} J → RingHom.ker f ≤ J
j : Ideal S
hj : map f I ≤ j
hj' : j.IsPrime
⊢ j.IsPrime

Tactic:
haveI : j.IsPrime := hj'