awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hK : K.IsRadical
rw : IsRadical (Ideal.radical (Ideal.comap f K))
⊢ IsRadical (Ideal.comap f K)

Tactic:
rw [← hK.radical, comap_radical]

Premises used: Ideal.IsRadical.radical, Ideal.comap_radical
-- 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
hK : K.IsRadical
⊢ IsRadical (Ideal.radical (Ideal.comap f K))

Tactic:
apply radical_isRadical

Premises used: Ideal.radical_isRadical
-- 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
⊢ LE.le.{v} (α := Ideal S) (map f I.radical) (radical (map f I))

Tactic:
map_le_iff_le_comap.2 fun r ⟨n, hrni⟩ => ⟨n, map_pow f r n ▸ mem_map_of_mem f hrni⟩

Premises used: Iff.mpr, Ideal.mem_map_of_mem, Membership.mem, Eq.rec, Ideal.map, map_pow, Ideal.map_le_iff_le_comap, Ideal.comap, Exists.intro, _private.0.Ideal.map_radical_le.match_1, Ideal.radical
-- 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 L : Ideal S
⊢ HMul.hMul (α := Ideal R) (comap f K) (comap f L) ≤ comap f (K * L)

Tactic:
map_le_iff_le_comap.1 <|
    (Ideal.map_mul f (comap f K) (comap f L)).symm ▸
      mul_mono (map_le_iff_le_comap.2 <| le_rfl) (map_le_iff_le_comap.2 <| le_rfl)

Premises used: Iff.mpr, le_rfl, Ideal.map_mul, Eq.rec, Ideal.mul_mono, Ideal.map_le_iff_le_comap, Ideal.comap, Iff.mp, Eq.symm
-- 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
zero : LE.le (α := Ideal R) ⊤ (comap f ⊤)
⊢ HPow.hPow (α := Ideal R) (β := ℕ) (comap f K) 0 ≤ comap f (HPow.hPow (β := ℕ) K 0)

Tactic:
rw [pow_zero, pow_zero, Ideal.one_eq_top, Ideal.one_eq_top]

Premises used: Ideal.one_eq_top, pow_zero
-- 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
⊢ LE.le (α := Ideal R) ⊤ (comap f ⊤)

Tactic:
rfl.le

Premises used: Set.Mem, Set.univ, setOf, Eq.le, Set.preimage, rfl
-- 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
⊢ LE.le (α := Ideal R) ⊤ (comap f ⊤)

Tactic:
exact rfl.le

Premises used: Eq.le, rfl
-- 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
n : ℕ
n_ih : HPow.hPow (α := Ideal R) (comap f K) n ≤ comap f (K ^ n)
succ : HPow.hPow (α := Ideal R) (comap f K) n * comap f K ≤ comap f (K ^ n * K)
⊢ HPow.hPow (α := Ideal R) (comap f K) (n + 1) ≤ comap f (K ^ (n + 1))

Tactic:
rw [pow_succ, pow_succ]

Premises used: pow_succ
-- 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
n : ℕ
n_ih : HPow.hPow (α := Ideal R) (comap f K) n ≤ comap f (K ^ n)
⊢ HPow.hPow (α := Ideal R) (comap f K) n * comap f K ≤ comap f (K ^ n * K)

Tactic:
(Ideal.mul_mono_left n_ih).trans (Ideal.le_comap_mul f)

Premises used: Set.Mem, Ideal.mul_mono_left, LE.le.trans, Ideal.le_comap_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
K : Ideal S
n : ℕ
n_ih : HPow.hPow (α := Ideal R) (comap f K) n ≤ comap f (K ^ n)
⊢ HPow.hPow (α := Ideal R) (comap f K) n * comap f K ≤ comap f (K ^ n * K)

Tactic:
exact (Ideal.mul_mono_left n_ih).trans (Ideal.le_comap_mul f)

Premises used: Ideal.mul_mono_left, LE.le.trans, Ideal.le_comap_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
K : Ideal S
n : ℕ
zero : HPow.hPow (α := Ideal R) (β := ℕ) (comap f K) 0 ≤ comap f (HPow.hPow (β := ℕ) K 0)
succ :
  ∀ (n : ℕ) (n_ih : HPow.hPow (α := Ideal R) (comap f K) n ≤ comap f (K ^ n)),
    HPow.hPow (α := Ideal R) (comap f K) (n + 1) ≤ comap f (K ^ (n + 1))
⊢ HPow.hPow (α := Ideal R) (comap f K) n ≤ comap f (K ^ n)

Tactic:
induction n with
  | zero =>
    rw [pow_zero, pow_zero, Ideal.one_eq_top, Ideal.one_eq_top]
    exact rfl.le
  | succ n n_ih =>
    rw [pow_succ, pow_succ]
    exact (Ideal.mul_mono_left n_ih).trans (Ideal.le_comap_mul f)

Premises used: Ideal.one_eq_top, pow_succ, Eq.le, pow_zero, rfl
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
inst : CommSemiring R
S : Type u_2
inst_1 : Semiring S
f : R →+* S
p : Ideal R
I : Ideal S
inst_2 : p.IsPrime
⊢ Disjoint (↑I : Set S) (↑(Submonoid.map f p.primeCompl) : Set S) ↔ comap f I ≤ p

Tactic:
(@Set.disjoint_image_right _ _ f p.primeCompl I).trans disjoint_compl_right_iff

Premises used: disjoint_compl_right_iff, setOf, Set.disjoint_image_right, Iff.trans, Set.image
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
p : Ideal R
inst_2 : p.IsPrime
⊢ comap f (map f p) = p ↔ ∃ (q : Ideal S), q.IsPrime ∧ comap f q = p

Tactic:
⟨fun hp ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
p : Ideal R
inst_2 : p.IsPrime
refine_1 : ∀ (hp : comap f (map f p) = p), ∃ (q : Ideal S), q.IsPrime ∧ comap f q = p
refine_2 : (∃ (q : Ideal S), q.IsPrime ∧ comap f q = p) → comap f (map f p) = p
⊢ comap f (map f p) = p ↔ ∃ (q : Ideal S), q.IsPrime ∧ comap f q = p

Tactic:
refine ⟨fun hp ↦ ?_, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
p : Ideal R
inst_2 : p.IsPrime
hp : comap f (map f p) = p
refine_1 :
  ∀ (q : Ideal S) (hq₁ : q.IsPrime) (hq₂ : map f p ≤ q)
    (hq₃ : Disjoint (↑q : Set S) (↑(Submonoid.map f p.primeCompl) : Set S)), ∃ (q : Ideal S), q.IsPrime ∧ comap f q = p
⊢ ∃ (q : Ideal S), q.IsPrime ∧ comap f q = p

Tactic:
obtain ⟨q, hq₁, hq₂, hq₃⟩ := Ideal.exists_le_prime_disjoint _ _
      (disjoint_map_primeCompl_iff_comap_le.mpr hp.le)

Premises used: Iff.mpr, Ideal.exists_le_prime_disjoint, Ideal.disjoint_map_primeCompl_iff_comap_le, Eq.le
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
p : Ideal R
inst_2 : p.IsPrime
hp : comap f (map f p) = p
q : Ideal S
hq₁ : q.IsPrime
hq₂ : map f p ≤ q
hq₃ : Disjoint (↑q : Set S) (↑(Submonoid.map f p.primeCompl) : Set S)
⊢ ∃ (q : Ideal S), q.IsPrime ∧ comap f q = p

Tactic:
⟨q, hq₁, le_antisymm (disjoint_map_primeCompl_iff_comap_le.mp hq₃)
      (map_le_iff_le_comap.mp hq₂)⟩

Premises used: Ideal.disjoint_map_primeCompl_iff_comap_le, Ideal.map_le_iff_le_comap, le_antisymm, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
p : Ideal R
inst_2 : p.IsPrime
hp : comap f (map f p) = p
q : Ideal S
hq₁ : q.IsPrime
hq₂ : map f p ≤ q
hq₃ : Disjoint (↑q : Set S) (↑(Submonoid.map f p.primeCompl) : Set S)
⊢ ∃ (q : Ideal S), q.IsPrime ∧ comap f q = p

Tactic:
exact ⟨q, hq₁, le_antisymm (disjoint_map_primeCompl_iff_comap_le.mp hq₃)
      (map_le_iff_le_comap.mp hq₂)⟩
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
q : Ideal S
hq : q.IsPrime
inst_2 : IsPrime (comap f q)
⊢ Eq (α := Ideal R) (comap f (map f (comap f q))) (comap f q)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
p : Ideal R
hP' : p.IsMaximal
hP : Ne.{v + 1} (α := Ideal S) (map f p) ⊤
⊢ comap f (map f p) = p

Tactic:
(IsCoatom.le_iff_eq hP'.out (comap_ne_top _ hP)).mp <| le_comap_map

Premises used: Ideal.comap_ne_top, Ideal.IsMaximal.out, Ideal.le_comap_map, Iff.mp, IsCoatom.le_iff_eq
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
T : Type w
F : Type u_1
G : Type u_2
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
inst_3 : FunLike F R S
rcf : RingHomClass F R S
inst_4 : FunLike G T S
rcg : RingHomClass G T S
f : F
g : G
⊢ Ideal.IsTwoSided (ker f)

Tactic:
inferInstanceAs (Ideal.comap f ⊥).IsTwoSided

Premises used: _private.0.RingHom.instIsTwoSidedKer._proof_1
-- 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
rcf : RingHomClass F R S
f : F
r : R
rw : Membership.mem (γ := Ideal R) (Ideal.comap f ⊥) r ↔ Eq.{v + 1} (α := S) ((f : (a : R) → S) r : S) (0 : S)
rw₁ :
  Membership.mem.{v, v} (α := S) (γ := Ideal S) ⊥ ((f : (a : R) → S) r : S) ↔
    Eq.{v + 1} (α := S) ((f : (a : R) → S) r : S) (0 : S)
rw₂ rw₃ : Eq.{v + 1} (α := S) ((f : (a : R) → S) r : S) (0 : S) ↔ Eq.{v + 1} (α := S) ((f : (a : R) → S) r : S) (0 : S)
⊢ Membership.mem (γ := Ideal R) (ker f) r ↔ Eq.{v + 1} (α := S) ((f : (a : R) → S) r : S) (0 : S)

Tactic:
rw [ker, Ideal.mem_comap, Submodule.mem_bot]

Premises used: Submodule.mem_bot, Ideal.mem_comap, RingHom.ker
-- 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
rcf : RingHomClass F R S
f : F
⊢ (↑(ker f) : Set R) = Set.preimage (β := S) (⇑f : (a : R) → S) {0}

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton, 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
rcf : RingHomClass F R S
f : F
⊢ Eq (α := Ideal R) (ker f) (Ideal.comap f ⊥)

Tactic:
rfl

Premises used: rfl, RingHom.ker
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
T : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : S →+* R
g : T →+* S
rw : Eq (α := Ideal T) (Ideal.comap g (Ideal.comap f ⊥)) (ker (f.comp g))
rw₁ : Eq (α := Ideal T) (Ideal.comap (f.comp g) ⊥) (ker (f.comp g))
rw₂ rw₃ : Eq (α := Ideal T) (Ideal.comap (f.comp g) ⊥) (Ideal.comap (f.comp g) ⊥)
⊢ Eq (α := Ideal T) (Ideal.comap g (ker f)) (ker (f.comp g))

Tactic:
rw [RingHom.ker_eq_comap_bot, Ideal.comap_comap, RingHom.ker_eq_comap_bot]

Premises used: RingHom.ker_eq_comap_bot, Ideal.comap_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
rcf : RingHomClass F R S
inst_3 : Nontrivial S
f : F
rw : ¬Eq.{v + 1} (α := S) 1 0
⊢ 1 ∉ ker f

Tactic:
rw [mem_ker, map_one]

Premises used: RingHom.mem_ker, map_one
-- 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
rcf : RingHomClass F R S
inst_3 : Nontrivial S
f : F
⊢ ¬Eq.{v + 1} (α := S) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- 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
rcf : RingHomClass F R S
inst_3 : Nontrivial S
f : F
⊢ ¬Eq.{v + 1} (α := S) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- 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
rcf : RingHomClass F R S
inst_3 : Nontrivial S
f : F
⊢ Ne (α := Ideal R) (ker f) ⊤

Tactic:
(Ideal.ne_top_iff_one _).mpr <| one_notMem_ker f

Premises used: Iff.mpr, Ideal.ne_top_iff_one, RingHom.one_notMem_ker
-- 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
rcf : RingHomClass F R S
inst_3 : Subsingleton S
f : F
⊢ Eq (α := Ideal R) (ker f) ⊤

Tactic:
eq_top_iff.mpr fun _ _ ↦ Subsingleton.elim _ _

Premises used: Iff.mpr, eq_top_iff, Subsingleton.elim, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
S : Type v
inst : Semiring S
ι : Type u_3
R : ι → Type u_4
inst_1 : (i : ι) → Semiring (R i)
φ : (i : ι) → RingHom.{v, u_4} S (R i)
h :
  ∀ (x : S),
    Membership.mem (γ := Ideal S) (ker (Pi.ringHom (f := R) φ)) x ↔
      Membership.mem (γ := Ideal S) (⨅ (i : ι), ker (φ i)) x
⊢ Eq (α := Ideal S) (ker (Pi.ringHom (f := R) φ)) (⨅ (i : ι), ker (φ i))

Tactic:
ext x
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
S : Type v
inst : Semiring S
ι : Type u_3
R : ι → Type u_4
inst_1 : (i : ι) → Semiring (R i)
φ : (i : ι) → RingHom.{v, u_4} S (R i)
x : S
⊢ Membership.mem (γ := Ideal S) (ker (Pi.ringHom (f := R) φ)) x ↔ Membership.mem (γ := Ideal S) (⨅ (i : ι), ker (φ i)) x

Tactic:
simp [mem_ker, funext_iff]

Premises used: funext_iff, RingHom.mem_ker
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
⊢ Eq (α := Ideal R) (ker f.rangeSRestrict) (ker f)

Tactic:
Ideal.ext fun _ ↦ Subtype.ext_iff

Premises used: Ideal.ext, Subtype.ext_iff
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R ≃+* S
h : ∀ (x : R), Membership.mem (γ := Ideal R) (ker (F := R →+* S) (↑f : R →+* S)) x ↔ Membership.mem (γ := Ideal R) ⊥ x
⊢ Eq (α := Ideal R) (ker (F := R →+* S) (↑f : R →+* S)) ⊥

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R ≃+* S
x : R
⊢ Membership.mem (γ := Ideal R) (ker (F := R →+* S) (↑f : R →+* S)) x ↔ Membership.mem (γ := Ideal R) ⊥ x

Tactic:
simp
-- 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
rcf : RingHomClass F R S
f : F
⊢ Eq (α := Ideal R) (ker (F := R →+* S) (↑f : R →+* S)) (ker f)

Tactic:
rfl

Premises used: RingHomClass.toRingHom, Ideal.comap, rfl, RingHom.ker
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
F' : Type u_3
inst_2 : EquivLike F' R S
inst_3 : RingEquivClass F' R S
f : F'
h : ∀ (x : R), Membership.mem (γ := Ideal R) (ker f) x ↔ Membership.mem (γ := Ideal R) ⊥ x
⊢ Eq (α := Ideal R) (ker f) ⊥

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
F' : Type u_3
inst_2 : EquivLike F' R S
inst_3 : RingEquivClass F' R S
f : F'
x : R
⊢ Membership.mem (γ := Ideal R) (ker f) x ↔ Membership.mem (γ := Ideal R) ⊥ x

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
T : Type w
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
e : S ≃+* T
rw : Eq (α := Ideal R) (Ideal.comap f (ker e.toRingHom)) (ker f)
rw₁ : Eq (α := Ideal R) (Ideal.comap f (ker (F := S →+* T) (↑e : S →+* T))) (ker f)
rw₂ : Eq (α := Ideal R) (Ideal.comap f ⊥) (ker f)
rw₃ rw₄ : Eq (α := Ideal R) (Ideal.comap f ⊥) (Ideal.comap f ⊥)
⊢ Eq (α := Ideal R) (ker (e.toRingHom.comp f)) (ker f)

Tactic:
rw [← RingHom.comap_ker, RingEquiv.toRingHom_eq_coe, RingHom.ker_coe_equiv, RingHom.ker]

Premises used: RingHom.comap_ker, RingHom.ker_coe_equiv, RingEquiv.toRingHom_eq_coe, RingHom.ker
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Ring R
inst_1 : Semiring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
rw :
  Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S) ↔
    ∀ (x : R), Membership.mem (γ := Set R) (Set.preimage (β := S) (⇑f : (a : R) → S) {0}) x ↔ x ∈ (↑⊥ : Set R)
⊢ Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S) ↔ Eq (α := Ideal R) (ker f) ⊥

Tactic:
rw [SetLike.ext'_iff, ker_eq, Set.ext_iff]

Premises used: SetLike.ext'_iff, Set.ext_iff, RingHom.ker_eq
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Ring R
inst_1 : Semiring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
⊢ Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S) ↔
    ∀ (x : R), Membership.mem (γ := Set R) (Set.preimage (β := S) (⇑f : (a : R) → S) {0}) x ↔ x ∈ (↑⊥ : Set R)

Tactic:
injective_iff_map_eq_zero' f

Premises used: Set.Mem, setOf, injective_iff_map_eq_zero', Set.preimage, Set.singleton
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Ring R
inst_1 : Semiring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
⊢ Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S) ↔
    ∀ (x : R), Membership.mem (γ := Set R) (Set.preimage (β := S) (⇑f : (a : R) → S) {0}) x ↔ x ∈ (↑⊥ : Set R)

Tactic:
exact injective_iff_map_eq_zero' f

Premises used: injective_iff_map_eq_zero'
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Ring R
inst_1 : Semiring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
f : F
rw : Eq (α := Ideal R) (ker f) ⊥ ↔ Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
rw₁ rw₂ : Eq (α := Ideal R) (ker f) ⊥ ↔ Eq (α := Ideal R) (ker f) ⊥
⊢ Eq (α := Ideal R) (ker f) ⊥ ↔ ∀ (x : R), Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S) → x = 0

Tactic:
rw [← injective_iff_map_eq_zero f, injective_iff_ker_eq_bot]

Premises used: RingHom.injective_iff_ker_eq_bot, injective_iff_map_eq_zero
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
T : Type w
inst : Ring R
inst_1 : Semiring S
inst_2 : Semiring T
g : T →+* R
f : R →+* S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
rw : Eq (α := Ideal T) (Ideal.comap g (ker f)) (ker g)
rw₁ : Eq (α := Ideal T) (Ideal.comap g ⊥) (ker g)
rw₂ rw₃ : Eq (α := Ideal T) (Ideal.comap g ⊥) (Ideal.comap g ⊥)
⊢ Eq (α := Ideal T) (ker (f.comp g)) (ker g)

Tactic:
rw [← RingHom.comap_ker, (injective_iff_ker_eq_bot f).mp hf, RingHom.ker]

Premises used: RingHom.comap_ker, RingHom.injective_iff_ker_eq_bot, Iff.mp, RingHom.ker
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
e : A ≃ₐ[R] B
⊢ Eq (α := Ideal A) (ker (F := A →+* B) (↑e : A →+* B)) ⊥

Tactic:
RingHom.ker_coe_equiv (e.toRingEquiv)

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, AlgEquiv.toRingEquiv, RingHom.ker_coe_equiv
-- 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
rc : RingHomClass F R S
f : F
x y : R
rw :
  Eq.{v + 1} (α := S) ((f : (a : R) → S) (x - y) : S) (0 : S) ↔
    Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)
rw₁ :
  HSub.hSub (α := S) (β := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S) = 0 ↔
    Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)
rw₂ rw₃ :
  Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S) ↔
    Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)
⊢ Membership.mem (γ := Ideal R) (ker f) (x - y) ↔
    Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)

Tactic:
rw [mem_ker, map_sub, sub_eq_zero]

Premises used: map_sub, sub_eq_zero, RingHom.mem_ker
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
inst : Ring R
inst_1 : Ring S
f : R →+* S
⊢ Eq (α := Ideal R) (ker (F := RingHom.{u, v} R ↥(range.{u, v} (R := R) f)) f.rangeRestrict) (ker f)

Tactic:
Ideal.ext fun _ ↦ Subtype.ext_iff

Premises used: Ideal.ext, Subtype.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 : IsDomain S
inst_3 : FunLike F R S
inst_4 : RingHomClass F R S
f : F
⊢ Ideal.IsPrime (ker f)

Tactic:
inferInstanceAs (Ideal.comap f ⊥).IsPrime

Premises used: _private.0.RingHom.ker_isPrime._proof_1
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
K : Type u_2
F : Type u_3
inst : Ring R
inst_1 : DivisionRing K
inst_2 : FunLike F R K
inst_3 : RingHomClass F R K
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := K) (⇑f : (a : R) → K)
⊢ Ideal.IsMaximal (ker f)

Tactic:
have := Ideal.bot_isMaximal (K := K)
  Ideal.comap_isMaximal_of_surjective _ hf

Premises used: Ideal.comap_isMaximal_of_surjective, Ideal.bot_isMaximal, RingHom.ker
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
r : R
⊢ Membership.mem (γ := Ideal R) (annihilator R M) r ↔ ∀ (m : M), r • m = 0

Tactic:
⟨fun h ↦ (congr($h ·)), (AddMonoidHom.ext ·)⟩

Premises used: congrArg, id, AddMonoidHom.ext, Iff.intro, DFunLike.coe
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
M : Type u_2
inst : AddCommMonoid M
R : Type u_4
inst_1 : CommSemiring R
inst_2 : Module R M
r : R
⊢ Membership.mem (γ := Ideal R) (annihilator R M) r ↔
    Eq.{u_2 + 1} (α := M →ₗ[R] M) ((LinearMap.lsmul R M : (a : R) → M →ₗ[R] M) r : M →ₗ[R] M) (0 : M →ₗ[R] M)

Tactic:
simp [Module.mem_annihilator, LinearMap.ext_iff]

Premises used: Module.mem_annihilator, LinearMap.ext_iff
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
⊢ Ideal.IsTwoSided (Module.annihilator R M)

Tactic:
inferInstanceAs (RingHom.ker _).IsTwoSided

Premises used: _private.0.instIsTwoSidedAnnihilator._proof_1
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
x : R
h : Membership.mem (γ := Submodule R R) (Module.annihilator R M') x
rw : ∀ (h : ∀ (m : M'), x • m = 0) (m : M), x • m = 0
⊢ Membership.mem (γ := Submodule R R) (Module.annihilator R M) x

Tactic:
rw [Module.mem_annihilator] at h ⊢

Premises used: Module.mem_annihilator
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
x : R
h : ∀ (m : M'), x • m = 0
m : M
rw : HSMul.hSMul (β := M') x ((f : (a : M) → M') m : M') = (f : (a : M) → M') 0
rw₁ : Eq.{u_3 + 1} (α := M') (0 : M') ((f : (a : M) → M') 0 : M')
rw₂ rw₃ : Eq.{u_3 + 1} (α := M') 0 0
⊢ Eq.{u_3 + 1} (α := M') ((f : (a : M) → M') (x • m) : M') ((f : (a : M) → M') 0 : M')

Tactic:
rw [map_smul, h, f.map_zero]

Premises used: LinearMap.map_zero, map_smul
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
x : R
h : ∀ (m : M'), x • m = 0
⊢ ∀ (m : M), x • m = 0

Tactic:
exact fun m ↦ hf (by rw [map_smul, h, f.map_zero])
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := M') (⇑f : (a : M) → M')
x : R
h : Membership.mem (γ := Submodule R R) (Module.annihilator R M) x
rw : ∀ (h : ∀ (m : M), x • m = 0) (m : M'), x • m = 0
⊢ Membership.mem (γ := Submodule R R) (Module.annihilator R M') x

Tactic:
rw [Module.mem_annihilator] at h ⊢

Premises used: Module.mem_annihilator