awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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)
⊢ Membership.mem (γ := Submodule R R) (RingHom.ker f) (x - x')
have a : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (x - x') : S) (0 : S)
Tactic: rw [RingHom.mem_ker, map_sub, hx, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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)
⊢ Membership.mem (γ := Submodule R R) (RingHom.ker f) (x - x')
have a₁ : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) x' : S) = 0
Tactic: rw [RingHom.mem_ker, map_sub, hx, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ Membership.mem (γ := Submodule R R) (RingHom.ker f) (x - x')
have a₂ : HSub.hSub (α := S) (β := S) ((f : (a : R) → S) x' : S) ((f : (a : R) → S) x' : S) = 0
Tactic: rw [RingHom.mem_ker, map_sub, hx, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ Membership.mem (γ := Submodule R R) (RingHom.ker f) (x - x')
have a₃ : Eq.{u_2 + 1} (α := S) 0 0
Tactic: rw [RingHom.mem_ker, map_sub, hx, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (hypothesis)
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 ∈ J
have this₁ : x - x' ∈ J
Tactic: have : x - x' ∈ J := by
      apply h J hJ
      rw [RingHom.mem_ker, map_sub, hx, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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)
have refine_1 : ∀ (h : Eq.{u_2 + 1} (α := Ideal S) (map f I) ⊤), ⊤ ≤ I
Tactic: refine ⟨fun h => H.ne_top (eq_top_iff.2 ?_), fun {x y} => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ IsPrime.{u_2} (α := S) (map f I)
have 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
Tactic: refine ⟨fun h => H.ne_top (eq_top_iff.2 ?_), fun {x y} => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (hypothesis)
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) ⊤
⊢ ⊤ ≤ I
have h₁ : Eq (α := Ideal R) (comap f (map f I)) (comap f ⊤)
Tactic: replace h := congr_arg (comap f) h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (hypothesis)
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
have h₁ : I ⊔ comap f ⊥ = ⊤
Tactic: rw [comap_map_of_surjective _ hf, comap_top] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
have 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
Tactic: refine fun hxy => (hf x).recOn fun a ha => (hf y).recOn fun b hb => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ Membership.mem (γ := Ideal S) (map f I) x ∨ Membership.mem (γ := Ideal S) (map f I) y
have 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
Tactic: rw [← ha, ← hb, ← map_mul f, mem_map_iff_of_surjective _ hf] at hxy
Cleared hypotheses: hxy, ha, b, hb
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ Membership.mem (γ := Ideal S) (map f I) x ∨ Membership.mem (γ := Ideal S) (map f I) y
have 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
Tactic: rcases hxy with ⟨c, hc, hc'⟩
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (hypothesis)
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)
⊢ Membership.mem (γ := Ideal S) (map f I) x ∨ Membership.mem (γ := Ideal S) (map f I) y
have hc'₁ : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) (c - a * b) : S) (0 : S)
Tactic: rw [← sub_eq_zero, ← map_sub] at hc'
Cleared hypotheses: hc'
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
have h : a * b = c - (c - a * b)
Tactic: convert! I.sub_mem hc (hk (hc' : c - a * b ∈ RingHom.ker f)) using 1
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (hypothesis)
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)
⊢ Membership.mem (γ := Ideal S) (map f I) x ∨ Membership.mem (γ := Ideal S) (map f I) y
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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)
have refine : ∀ (h : Eq.{u_2 + 1} (α := Ideal S) (map f m) ⊤), False
Tactic: refine m.map_eq_top_or_isMaximal_of_surjective f hf ‹_› |>.resolve_left fun h => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (hypothesis)
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) ⊤
⊢ False
have h₁ : Eq (α := Ideal R) (comap f (map f m)) (comap f ⊤)
Tactic: apply congr_arg (comap f) at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (hypothesis)
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 ⊤)
⊢ False
have h₁ : m = ⊤
Tactic: rw [comap_map_of_surjective _ hf, comap_top, ← RingHom.ker_eq_comap_bot, sup_of_le_left hk] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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)
⊢ Eq.{u_2 + 1} (α := Ideal S) (map f I) (map f J) ↔ I ⊔ RingHom.ker f = J ⊔ RingHom.ker f
have rw : Eq (α := Ideal R) (comap f (map f I)) (comap f (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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ Eq.{u_2 + 1} (α := Ideal S) (map f I) (map f J) ↔ I ⊔ RingHom.ker f = J ⊔ RingHom.ker f
have rw₁ : I ⊔ comap f ⊥ = comap f (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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ Eq.{u_2 + 1} (α := Ideal S) (map f I) (map f J) ↔ I ⊔ RingHom.ker f = J ⊔ RingHom.ker f
have rw₂ : I ⊔ comap f ⊥ = J ⊔ comap f ⊥ ↔ 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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ Eq.{u_2 + 1} (α := Ideal S) (map f I) (map f J) ↔ I ⊔ RingHom.ker f = J ⊔ RingHom.ker f
have rw₃ : I ⊔ comap f ⊥ = J ⊔ comap f ⊥ ↔ I ⊔ comap f ⊥ = J ⊔ comap 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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ Eq.{u_2 + 1} (α := Ideal S) (map f I.radical) (radical (map f I))
have 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})
Tactic: rw [radical_eq_sInf, radical_eq_sInf]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (hypothesis)
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
⊢ 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})
have this : ∀ (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
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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 {J : Ideal S | map f I ≤ J ∧ J.IsPrime})
have 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})
Tactic: convert! map_sInf hf this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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} (α := 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})
have 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
Tactic: ext j
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (hypothesis)
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
J : Ideal R
hJ : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsPrime} J
hJ' : map f J = j
⊢ Membership.mem (γ := Set (Ideal S)) {J : Ideal S | map f I ≤ J ∧ J.IsPrime} j
have this₁ : J.IsPrime
Tactic: haveI : J.IsPrime := hJ.right
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
g : A →+* C
hg : LE.le (α := Ideal A) (ker f) (ker g)
⊢ Eq.{u_3 + 1} (α := C) ((g : (a : A) → C) (f_inv 1) : C) (1 : C)
have rw : Membership.mem (γ := Ideal A) (ker g) (f_inv 1 - 1)
Tactic: rw [← map_one g, ← sub_eq_zero, ← map_sub g, ← mem_ker]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
g : A →+* C
hg : LE.le (α := Ideal A) (ker f) (ker g)
⊢ Membership.mem (γ := Ideal A) (ker g) (f_inv 1 - 1)
have a : Membership.mem (γ := Submodule A A) (ker f) (f_inv 1 - 1)
Tactic: apply hg
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
g : A →+* C
hg : LE.le (α := Ideal A) (ker f) (ker g)
⊢ Membership.mem (γ := Submodule A A) (ker f) (f_inv 1 - 1)
have a : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (f_inv 1) : B) (1 : B)
Tactic: rw [mem_ker, map_sub f, sub_eq_zero, map_one f]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
g : A →+* C
hg : LE.le (α := Ideal A) (ker f) (ker g)
x y : B
⊢ (g : (a : A) → C) (f_inv (x * y)) =
    HMul.hMul (α := C) (β := C) ((g : (a : A) → C) (f_inv x) : C) ((g : (a : A) → C) (f_inv y) : C)
have rw : Membership.mem (γ := Ideal A) (ker g) (f_inv (x * y) - f_inv x * f_inv y)
Tactic: rw [← map_mul g, ← sub_eq_zero, ← map_sub g, ← mem_ker]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
g : A →+* C
hg : LE.le (α := Ideal A) (ker f) (ker g)
x y : B
⊢ Membership.mem (γ := Ideal A) (ker g) (f_inv (x * y) - f_inv x * f_inv y)
have a : Membership.mem (γ := Submodule A A) (ker f) (f_inv (x * y) - f_inv x * f_inv y)
Tactic: apply hg
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
g : A →+* C
hg : LE.le (α := Ideal A) (ker f) (ker g)
x y : B
⊢ Membership.mem (γ := Submodule A A) (ker f) (f_inv (x * y) - f_inv x * f_inv y)
have a : (f : (a : A) → B) (f_inv (x * y)) =
  HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (f_inv x) : B) ((f : (a : A) → B) (f_inv y) : B)
Tactic: rw [mem_ker, map_sub f, sub_eq_zero, map_mul f]