awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
r : R
mp :
  (∀ (n : M), Membership.mem (γ := Submodule R M) (span R s) n → r • n = 0) → ∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0
mpr :
  (∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0) → ∀ (n : M), Membership.mem (γ := Submodule R M) (span R s) n → r • n = 0
⊢ (∀ (n : M), Membership.mem (γ := Submodule R M) (span R s) n → r • n = 0) ↔ ∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
r : R
h : ∀ (n : M), Membership.mem (γ := Submodule R M) (span R s) n → r • n = 0
n : (↑s : Type u_2)
⊢ r • (↑n : M) = 0

Tactic:
h _ (Submodule.subset_span n.prop)

Premises used: Subtype.prop, Submodule.subset_span
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
r : R
h : ∀ (n : M), Membership.mem (γ := Submodule R M) (span R s) n → r • n = 0
n : (↑s : Type u_2)
⊢ r • (↑n : M) = 0

Tactic:
exact h _ (Submodule.subset_span n.prop)

Premises used: Subtype.prop, Submodule.subset_span
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
r : R
h : ∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0
n : M
hn : Membership.mem (γ := Submodule R M) (span R s) n
⊢ r • n = 0

Tactic:
Submodule.span_induction ?_ ?_ ?_ ?_ hn

Premises used: Submodule.span_induction
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
r : R
h : ∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0
n : M
hn : Membership.mem (γ := Submodule R M) (span R s) n
mpr : ∀ (x : M) (h : x ∈ s), r • x = 0
mpr₁ : HSMul.hSMul (β := M) r 0 = 0
mpr₂ :
  ∀ (x y : M) (hx : Membership.mem (γ := Submodule R M) (span R s) x)
    (hy : Membership.mem (γ := Submodule R M) (span R s) y), r • x = 0 → r • y = 0 → r • (x + y) = 0
mpr₃ : ∀ (a : R) (x : M) (hx : Membership.mem (γ := Submodule R M) (span R s) x), r • x = 0 → r • a • x = 0
⊢ r • n = 0

Tactic:
refine Submodule.span_induction ?_ ?_ ?_ ?_ hn
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
r : R
h : ∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0
n : M
hn : Membership.mem (γ := Submodule R M) (span R s) n
x : M
hx : x ∈ s
⊢ r • x = 0

Tactic:
h ⟨x, hx⟩

Premises used: Subtype.mk
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
r : R
h : ∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0
n : M
hn : Membership.mem (γ := Submodule R M) (span R s) n
x : M
hx : x ∈ s
⊢ r • x = 0

Tactic:
exact h ⟨x, hx⟩

Premises used: Subtype.mk
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
r : R
h : ∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0
n : M
hn : Membership.mem (γ := Submodule R M) (span R s) n
⊢ HSMul.hSMul (β := M) r 0 = 0

Tactic:
smul_zero _

Premises used: smul_zero
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
r : R
h : ∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0
n : M
hn : Membership.mem (γ := Submodule R M) (span R s) n
⊢ HSMul.hSMul (β := M) r 0 = 0

Tactic:
exact smul_zero _

Premises used: smul_zero
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
r : R
h : ∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0
n : M
hn : Membership.mem (γ := Submodule R M) (span R s) n
x y : M
mpr :
  Membership.mem (γ := Submodule R M) (span R s) x →
    ∀ (hy : Membership.mem (γ := Submodule R M) (span R s) y), r • x = 0 → r • y = 0 → r • (x + y) = 0
⊢ ∀ (hx : Membership.mem (γ := Submodule R M) (span R s) x) (hy : Membership.mem (γ := Submodule R M) (span R s) y),
    r • x = 0 → r • y = 0 → r • (x + y) = 0

Tactic:
_
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
r : R
h : ∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0
n : M
hn : Membership.mem (γ := Submodule R M) (span R s) n
x y : M
hx : Membership.mem (γ := Submodule R M) (span R s) x
mpr : Membership.mem (γ := Submodule R M) (span R s) y → r • x = 0 → r • y = 0 → r • (x + y) = 0
⊢ ∀ (hy : Membership.mem (γ := Submodule R M) (span R s) y), r • x = 0 → r • y = 0 → r • (x + y) = 0

Tactic:
_
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
r : R
h : ∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0
n : M
hn : Membership.mem (γ := Submodule R M) (span R s) n
x y : M
hx_1 : Membership.mem (γ := Submodule R M) (span R s) x
hy_1 : Membership.mem (γ := Submodule R M) (span R s) y
hx : r • x = 0
hy : r • y = 0
mpr : r • x + r • y = 0
mpr₁ : 0 + r • y = 0
mpr₂ : HAdd.hAdd (α := M) 0 0 = 0
mpr₃ mpr₄ : Eq.{u_2 + 1} (α := M) 0 0
⊢ r • (x + y) = 0

Tactic:
rw [smul_add, hx, hy, zero_add]

Premises used: zero_add, smul_add
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
r : R
h : ∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0
n : M
hn : Membership.mem (γ := Submodule R M) (span R s) n
a : R
x : M
mpr : Membership.mem (γ := Submodule R M) (span R s) x → r • x = 0 → r • a • x = 0
⊢ ∀ (hx : Membership.mem (γ := Submodule R M) (span R s) x), r • x = 0 → r • a • x = 0

Tactic:
_
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
r : R
h : ∀ (n : (↑s : Type u_2)), r • (↑n : M) = 0
n : M
hn : Membership.mem (γ := Submodule R M) (span R s) n
a : R
x : M
hx_1 : Membership.mem (γ := Submodule R M) (span R s) x
hx : r • x = 0
mpr : a • r • x = 0
mpr₁ : HSMul.hSMul (β := M) a 0 = 0
mpr₂ mpr₃ : Eq.{u_2 + 1} (α := M) 0 0
⊢ r • a • x = 0

Tactic:
rw [smul_comm, hx, smul_zero]

Premises used: smul_zero, SMulCommClass.smul_comm
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
g : M
r : R
⊢ Membership.mem (γ := Ideal R) (annihilator (M := M) (R ∙ g)) r ↔ r • g = 0

Tactic:
simp [mem_annihilator_span]

Premises used: Submodule.mem_annihilator_span
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
h :
  ∀ (x : R),
    Membership.mem (γ := Ideal R) (annihilator (span R s)) x ↔
      Membership.mem (γ := Ideal R) (⨅ (g : (↑s : Type u_2)), ker (toSpanSingleton R M (↑g : M))) x
⊢ Eq (α := Ideal R) (annihilator (span R s)) (⨅ (g : (↑s : Type u_2)), ker (toSpanSingleton R M (↑g : M)))

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
x : R
⊢ Membership.mem (γ := Ideal R) (annihilator (span R s)) x ↔
    Membership.mem (γ := Ideal R) (⨅ (g : (↑s : Type u_2)), ker (toSpanSingleton R M (↑g : M))) x

Tactic:
simp [mem_annihilator_span]

Premises used: Submodule.mem_annihilator_span
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
g : M
⊢ Eq (α := Ideal R) (annihilator (M := M) (R ∙ g)) (ker (toSpanSingleton R M g))

Tactic:
simp [annihilator_span]

Premises used: Submodule.annihilator_span
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
rw : annihilator I * I = ⊥
rw₁ rw₂ : Eq.{u_1 + 1} (α := Ideal R) ⊥ ⊥
⊢ I * annihilator I = ⊥

Tactic:
rw [mul_comm, annihilator_mul]

Premises used: Submodule.annihilator_mul, mul_comm
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_3
M : Type u_4
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower S R M
I : Ideal S
N : Submodule R M
⊢ restrictScalars S (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' (↑I : Set S)) N) =
    HSMul.hSMul (β := Submodule S M) (↑I : Set S) (restrictScalars S N)

Tactic:
have := N.restrictScalars_image_smul_eq (I : Set S)
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_3
M : Type u_4
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower S R M
I : Ideal S
N : Submodule R M
this :
  restrictScalars S (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' (↑I : Set S)) N) =
    HSMul.hSMul (β := Submodule S M) (↑I : Set S) (restrictScalars S N)
⊢ restrictScalars S (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' (↑I : Set S)) N) =
    HSMul.hSMul (β := Submodule S M) I (restrictScalars S N)

Tactic:
rw [coe_set_smul] at this

Premises used: Submodule.coe_set_smul
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_3
M : Type u_4
inst_1 : CommSemiring S
inst_2 : Algebra S R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower S R M
I : Ideal S
N : Submodule R M
this :
  restrictScalars S (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' (↑I : Set S)) N) =
    HSMul.hSMul (β := Submodule S M) I (restrictScalars S N)
rw :
  restrictScalars S
      (HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (Ideal.span ((⇑(algebraMap S R) : (a : S) → R) '' (↑I : Set S))) N) =
    HSMul.hSMul (β := Submodule S M) I (restrictScalars S N)
rw₁ :
  restrictScalars S (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' (↑I : Set S)) N) =
    HSMul.hSMul (β := Submodule S M) I (restrictScalars S N)
rw₂ rw₃ :
  Eq (α := Submodule S M)
    (restrictScalars S (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' (↑I : Set S)) N))
    (restrictScalars S (HSMul.hSMul.{u_1, u_4, u_4} (α := Set R) ((⇑(algebraMap S R) : (a : S) → R) '' (↑I : Set S)) N))
⊢ restrictScalars S (HSMul.hSMul.{u_1, u_4, u_4} (α := Ideal R) (Ideal.map (F := S →+* R) (algebraMap S R) I) N) =
    HSMul.hSMul (β := Submodule S M) I (restrictScalars S N)

Tactic:
rw [Ideal.map, span_smul_eq, ← this]

Premises used: Ideal.map, Submodule.span_smul_eq
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
I : Ideal R
f : F
rw : Eq.{u_2 + 1} (α := Ideal S) (map f I) ⊥ ↔ I ≤ comap f ⊥
rw₁ : LE.le.{u_2} (α := Ideal S) (map f I) ⊥ ↔ I ≤ comap f ⊥
rw₂ rw₃ : I ≤ comap f ⊥ ↔ I ≤ comap f ⊥
⊢ Eq.{u_2 + 1} (α := Ideal S) (map f I) ⊥ ↔ I ≤ RingHom.ker f

Tactic:
rw [RingHom.ker, eq_bot_iff, map_le_iff_le_comap]

Premises used: Ideal.map_le_iff_le_comap, eq_bot_iff, RingHom.ker
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
K : Ideal S
f : F
⊢ LE.le (α := Ideal R) (RingHom.ker f) (comap f K)

Tactic:
fun _ hx =>
  mem_comap.2 (RingHom.mem_ker.1 hx ▸ K.zero_mem)

Premises used: Iff.mpr, Set.Mem, RingHom.mem_ker, Eq.rec, Ideal.zero_mem, Iff.mp, Eq.symm, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
F' : Type u_4
inst_3 : EquivLike F' R S
inst_4 : RingEquivClass F' R S
f : F'
I : Ideal R
inst_5 : I.IsPrime
⊢ Eq.{u_2 + 1} (α := Ideal S) (map f I) (map (F := R →+* S) (↑(↑f : R ≃+* S) : R →+* S) I)

Tactic:
have h : I.map f = I.map ((RingEquivClass.toRingEquiv f : R ≃+* S) : R →+* S) := rfl
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
F' : Type u_4
inst_3 : EquivLike F' R S
inst_4 : RingEquivClass F' R S
f : F'
I : Ideal R
inst_5 : I.IsPrime
h : Eq.{u_2 + 1} (α := Ideal S) (map f I) (map (F := R →+* S) (↑(↑f : R ≃+* S) : R →+* S) I)
rw : IsPrime (comap (F := S ≃+* R) (RingEquiv.symm (↑f : R ≃+* S)) I)
⊢ IsPrime.{u_2} (α := S) (map f I)

Tactic:
rw [h, map_comap_of_equiv (RingEquivClass.toRingEquiv f : R ≃+* S)]

Premises used: RingEquivClass.toRingEquiv, Ideal.map_comap_of_equiv
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
F' : Type u_4
inst_3 : EquivLike F' R S
inst_4 : RingEquivClass F' R S
f : F'
I : Ideal R
inst_5 : I.IsPrime
h : Eq.{u_2 + 1} (α := Ideal S) (map f I) (map (F := R →+* S) (↑(↑f : R ≃+* S) : R →+* S) I)
⊢ IsPrime (comap (F := S ≃+* R) (RingEquiv.symm (↑f : R ≃+* S)) I)

Tactic:
Ideal.IsPrime.comap (RingEquivClass.toRingEquiv f : R ≃+* S).symm

Premises used: Ideal.IsPrime.comap, RingEquivClass.toRingEquiv, RingEquiv.symm
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
F' : Type u_4
inst_3 : EquivLike F' R S
inst_4 : RingEquivClass F' R S
f : F'
I : Ideal R
inst_5 : I.IsPrime
h : Eq.{u_2 + 1} (α := Ideal S) (map f I) (map (F := R →+* S) (↑(↑f : R ≃+* S) : R →+* S) I)
⊢ IsPrime (comap (F := S ≃+* R) (RingEquiv.symm (↑f : R ≃+* S)) I)

Tactic:
exact Ideal.IsPrime.comap (RingEquivClass.toRingEquiv f : R ≃+* S).symm

Premises used: Ideal.IsPrime.comap, RingEquivClass.toRingEquiv, RingEquiv.symm
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
rc : RingHomClass F R S
I : Ideal R
f : F
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ Eq.{u_2 + 1} (α := Ideal S) (map f I) ⊥ ↔ I = ⊥

Tactic:
simp [map, ← map_zero f, -map_zero, hf.eq_iff, I.eq_bot_iff]

Premises used: Function.Injective.eq_iff, map_zero, Ideal.map, Submodule.eq_bot_iff
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
r : R
I : Ideal R
f : R →+* S
rw :
  map f (HSMul.hSMul (α := Ideal R) (span {r}) I) =
    HSMul.hSMul (α := S) (β := Ideal S) ((f : (a : R) → S) r : S) (map f I)
rw₁ : map f (span {r} * I) = HSMul.hSMul (α := S) (β := Ideal S) ((f : (a : R) → S) r : S) (map f I)
rw₂ :
  HMul.hMul (α := Ideal S) (map (R := R) f (span {r})) (map f I) =
    HSMul.hSMul (α := S) (β := Ideal S) ((f : (a : R) → S) r : S) (map f I)
rw₃ :
  HMul.hMul (α := Ideal S) (span (Set.image (α := R) (⇑f : (a : R) → S) {r})) (map f I) =
    HSMul.hSMul (α := S) (β := Ideal S) ((f : (a : R) → S) r : S) (map f I)
rw₄ :
  HMul.hMul (α := Ideal S) (span (singleton (α := S) ((f : (a : R) → S) r : S))) (map f I) =
    HSMul.hSMul (α := S) (β := Ideal S) ((f : (a : R) → S) r : S) (map f I)
rw₅ :
  HSMul.hSMul (α := Ideal S) (β := Ideal S) (span (singleton (α := S) ((f : (a : R) → S) r : S))) (map f I) =
    HSMul.hSMul (α := S) (β := Ideal S) ((f : (a : R) → S) r : S) (map f I)
rw₆ rw₇ :
  HSMul.hSMul (α := S) (β := Submodule S S) ((f : (a : R) → S) r : S) (map f I) =
    HSMul.hSMul (α := S) (β := Ideal S) ((f : (a : R) → S) r : S) (map f I)
⊢ map f (r • I) = HSMul.hSMul (α := S) (β := Ideal S) ((f : (a : R) → S) r : S) (map f I)

Tactic:
rw [← Submodule.ideal_span_singleton_smul, smul_eq_mul, Ideal.map_mul, Ideal.map_span,
    Set.image_singleton, ← smul_eq_mul, Submodule.ideal_span_singleton_smul]

Premises used: Submodule.ideal_span_singleton_smul, Set.image_singleton, Ideal.map_mul, Ideal.map_span, smul_eq_mul
-- 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
⊢ comap f (map f I) = I ⊔ RingHom.ker f

Tactic:
comap_map_of_surjective f hf I

Premises used: Set.Mem, setOf, Ideal.comap_map_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
A : Set (Ideal R)
f : F
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ (∀ J ∈ A, RingHom.ker f ≤ J) → Eq.{u_2 + 1} (α := Ideal S) (map f (sInf A)) (sInf (map f '' A))

Tactic:
fun h => le_antisymm (le_sInf ?_) ?_

Premises used: le_antisymm, le_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)
refine_1 :
  ∀ (h : ∀ J ∈ A, RingHom.ker f ≤ J) (b : Ideal S),
    Membership.mem (γ := Set (Ideal S)) (map f '' A) b → map f (sInf A) ≤ b
refine_2 : ∀ (h : ∀ J ∈ A, RingHom.ker f ≤ J), LE.le.{u_2} (α := Ideal S) (sInf (map f '' A)) (map f (sInf A))
⊢ (∀ J ∈ A, RingHom.ker f ≤ J) → Eq.{u_2 + 1} (α := Ideal S) (map f (sInf A)) (sInf (map f '' A))

Tactic:
refine fun h => le_antisymm (le_sInf ?_) ?_

Premises used: le_antisymm, le_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
j : Ideal S
hj : Membership.mem (γ := Set (Ideal S)) (map f '' A) j
y : S
hy : Membership.mem (γ := Submodule S S) (map f (sInf A)) y
refine_1 : ∀ (x : R) (hx : x ∈ sInf A ∧ (f : (a : R) → S) x = y), y ∈ j
⊢ y ∈ j

Tactic:
obtain ⟨x, hx⟩ := (mem_map_iff_of_surjective f hf).1 hy

Premises used: Iff.mp, 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
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
j : Ideal S
hj : Membership.mem (γ := Set (Ideal S)) (map f '' A) j
y : S
hy : Membership.mem (γ := Submodule S S) (map f (sInf A)) y
x : R
hx : x ∈ sInf A ∧ (f : (a : R) → S) x = y
refine_1 : ∀ (J : Ideal R) (hJ : J ∈ A ∧ map f J = j), y ∈ j
⊢ y ∈ j

Tactic:
obtain ⟨J, hJ⟩ := (Set.mem_image _ _ _).mp hj

Premises used: Set.mem_image, Iff.mp
-- 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
j : Ideal S
hj : Membership.mem (γ := Set (Ideal S)) (map f '' A) j
y : S
hy : Membership.mem (γ := Submodule S S) (map f (sInf A)) y
x : R
hx : x ∈ sInf A ∧ (f : (a : R) → S) x = y
J : Ideal R
hJ : J ∈ A ∧ map f J = j
refine_1 : Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (map f J) ((f : (a : R) → S) x : S)
⊢ y ∈ j

Tactic:
rw [← hJ.right, ← hx.right]

Premises used: And.right
-- 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
j : Ideal S
hj : Membership.mem (γ := Set (Ideal S)) (map f '' A) j
y : S
hy : Membership.mem (γ := Submodule S S) (map f (sInf A)) y
x : R
hx : x ∈ sInf A ∧ (f : (a : R) → S) x = y
J : Ideal R
hJ : J ∈ A ∧ map f J = j
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (map f J) ((f : (a : R) → S) x : S)

Tactic:
mem_map_of_mem f (sInf_le_of_le hJ.left (le_of_eq rfl) hx.left)

Premises used: Ideal.mem_map_of_mem, Set.Mem, And.left, le_of_eq, sInf_le_of_le, 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
j : Ideal S
hj : Membership.mem (γ := Set (Ideal S)) (map f '' A) j
y : S
hy : Membership.mem (γ := Submodule S S) (map f (sInf A)) y
x : R
hx : x ∈ sInf A ∧ (f : (a : R) → S) x = y
J : Ideal R
hJ : J ∈ A ∧ map f J = j
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (map f J) ((f : (a : R) → S) x : S)

Tactic:
exact mem_map_of_mem f (sInf_le_of_le hJ.left (le_of_eq rfl) hx.left)

Premises used: Ideal.mem_map_of_mem, And.left, le_of_eq, sInf_le_of_le, 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
y : S
hy : Membership.mem (γ := Submodule S S) (sInf (map f '' A)) y
refine_2 : ∀ (x : R) (hx : (f : (a : R) → S) x = y), Membership.mem (γ := Submodule S S) (map f (sInf A)) y
⊢ Membership.mem (γ := Submodule S S) (map f (sInf A)) y

Tactic:
obtain ⟨x, hx⟩ := hf 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
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
⊢ Membership.mem (γ := Submodule S S) (map f (sInf A)) y

Tactic:
hx ▸ mem_map_of_mem f ?_

Premises used: Ideal.mem_map_of_mem, Eq.rec
-- 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
refine_2 : x ∈ sInf A
⊢ Membership.mem (γ := Submodule S S) (map f (sInf A)) y

Tactic:
refine hx ▸ mem_map_of_mem f ?_
-- 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
⊢ ∀ I ∈ A, Membership.mem (γ := Ideal S) (map f I) y

Tactic:
simpa using hy
-- 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
⊢ ∀ I ∈ A, Membership.mem (γ := Ideal S) (map f I) y

Tactic:
have : ∀ I ∈ A, y ∈ map f I := by simpa using hy