awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ r • (x + y) = 0
have mpr₃ : Eq.{u_2 + 1} (α := M) 0 0
Tactic: rw [smul_add, hx, hy, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ r • a • x = 0
have mpr : a • r • x = 0
Tactic: rw [smul_comm, hx, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ r • a • x = 0
have mpr₁ : HSMul.hSMul (β := M) a 0 = 0
Tactic: rw [smul_comm, hx, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ r • a • x = 0
have mpr₂ : Eq.{u_2 + 1} (α := M) 0 0
Tactic: rw [smul_comm, hx, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
⊢ Eq (α := Ideal R) (annihilator (span R s)) (⨅ (g : (↑s : Type u_2)), ker (toSpanSingleton R M (↑g : M)))
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
⊢ I * annihilator I = ⊥
have rw : annihilator I * I = ⊥
Tactic: rw [mul_comm, annihilator_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
rw : annihilator I * I = ⊥
⊢ I * annihilator I = ⊥
have rw₁ : Eq.{u_1 + 1} (α := Ideal R) ⊥ ⊥
Tactic: rw [mul_comm, annihilator_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (hypothesis)
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} (α := Ideal R) (Ideal.map (F := S →+* R) (algebraMap S R) I) N) =
    HSMul.hSMul (β := Submodule S M) I (restrictScalars S N)
have 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)
Tactic: have := N.restrictScalars_image_smul_eq (I : Set S)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (hypothesis)
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} (α := Ideal R) (Ideal.map (F := S →+* R) (algebraMap S R) I) N) =
    HSMul.hSMul (β := Submodule S M) I (restrictScalars S N)
have 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)
Tactic: rw [coe_set_smul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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)
⊢ 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)
have 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)
Tactic: rw [Ideal.map, span_smul_eq, ← this]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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)
⊢ 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)
have 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))
Tactic: rw [Ideal.map, span_smul_eq, ← this]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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
⊢ Eq.{u_2 + 1} (α := Ideal S) (map f I) ⊥ ↔ I ≤ RingHom.ker f
have rw : Eq.{u_2 + 1} (α := Ideal S) (map f I) ⊥ ↔ I ≤ comap f ⊥
Tactic: rw [RingHom.ker, eq_bot_iff, map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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 ⊥
⊢ Eq.{u_2 + 1} (α := Ideal S) (map f I) ⊥ ↔ I ≤ RingHom.ker f
have rw₁ : LE.le.{u_2} (α := Ideal S) (map f I) ⊥ ↔ I ≤ comap f ⊥
Tactic: rw [RingHom.ker, eq_bot_iff, map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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 ⊥
⊢ Eq.{u_2 + 1} (α := Ideal S) (map f I) ⊥ ↔ I ≤ RingHom.ker f
have rw₂ : I ≤ comap f ⊥ ↔ I ≤ comap f ⊥
Tactic: rw [RingHom.ker, eq_bot_iff, map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (hypothesis)
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
⊢ IsPrime.{u_2} (α := S) (map f I)
have h : 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
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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.{u_2} (α := S) (map f I)
have rw : IsPrime (comap (F := S ≃+* R) (RingEquiv.symm (↑f : R ≃+* S)) I)
Tactic: rw [h, map_comap_of_equiv (RingEquivClass.toRingEquiv f : R ≃+* S)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
r : R
I : Ideal R
f : R →+* S
⊢ map f (r • I) = HSMul.hSMul (α := S) (β := Ideal S) ((f : (a : R) → S) r : S) (map f I)
have rw : map f (HSMul.hSMul (α := Ideal R) (span {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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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)
⊢ map f (r • I) = HSMul.hSMul (α := S) (β := Ideal S) ((f : (a : R) → S) r : S) (map f I)
have rw₁ : map f (span {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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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)
⊢ map f (r • I) = HSMul.hSMul (α := S) (β := Ideal S) ((f : (a : R) → S) r : S) (map f I)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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)
⊢ map f (r • I) = HSMul.hSMul (α := S) (β := Ideal S) ((f : (a : R) → S) r : S) (map f I)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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)
⊢ map f (r • I) = HSMul.hSMul (α := S) (β := Ideal S) ((f : (a : R) → S) r : S) (map f I)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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)
⊢ map f (r • I) = HSMul.hSMul (α := S) (β := Ideal S) ((f : (a : R) → S) r : S) (map f I)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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)
⊢ map f (r • I) = HSMul.hSMul (α := S) (β := Ideal S) ((f : (a : R) → S) r : S) (map f I)
have 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)
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]
-- 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)
⊢ (∀ J ∈ A, RingHom.ker f ≤ J) → Eq.{u_2 + 1} (α := Ideal S) (map f (sInf A)) (sInf (map f '' A))
have 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
Tactic: refine fun h => le_antisymm (le_sInf ?_) ?_
-- 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)
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
⊢ (∀ J ∈ A, RingHom.ker f ≤ J) → Eq.{u_2 + 1} (α := Ideal S) (map f (sInf A)) (sInf (map f '' A))
have refine_2 : ∀ (h : ∀ J ∈ A, RingHom.ker f ≤ J), LE.le.{u_2} (α := Ideal S) (sInf (map f '' A)) (map f (sInf A))
Tactic: refine fun h => le_antisymm (le_sInf ?_) ?_
-- 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
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
⊢ y ∈ j
have refine_1 : ∀ (x : R) (hx : x ∈ sInf A ∧ (f : (a : R) → S) x = y), y ∈ j
Tactic: obtain ⟨x, hx⟩ := (mem_map_iff_of_surjective f hf).1 hy
-- 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
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
⊢ y ∈ j
have refine_1 : ∀ (J : Ideal R) (hJ : J ∈ A ∧ map f J = j), y ∈ j
Tactic: obtain ⟨J, hJ⟩ := (Set.mem_image _ _ _).mp hj
-- 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
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
⊢ y ∈ j
have refine_1 : Membership.mem.{u_2, u_2} (α := S) (γ := Submodule S S) (map f J) ((f : (a : R) → S) x : S)
Tactic: rw [← hJ.right, ← hx.right]
-- 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
y : S
hy : Membership.mem (γ := Submodule S S) (sInf (map f '' A)) y
⊢ Membership.mem (γ := Submodule S S) (map f (sInf A)) y
have refine_2 : ∀ (x : R) (hx : (f : (a : R) → S) x = y), Membership.mem (γ := Submodule S S) (map f (sInf A)) y
Tactic: obtain ⟨x, hx⟩ := hf 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
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
have refine_2 : x ∈ sInf A
Tactic: refine hx ▸ mem_map_of_mem f ?_
-- 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
y : S
hy : Membership.mem (γ := Submodule S S) (sInf (map f '' A)) y
x : R
hx : (f : (a : R) → S) x = y
⊢ x ∈ sInf A
have this : ∀ I ∈ A, Membership.mem (γ := Ideal S) (map f I) y
Tactic: have : ∀ I ∈ A, y ∈ map f I := by simpa using hy
-- 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
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
⊢ x ∈ sInf A
have refine_2 : ∀ p ∈ A, x ∈ p
Tactic: rw [Submodule.mem_sInf]
-- 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
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
⊢ x ∈ J
have 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
Tactic: rcases (mem_map_iff_of_surjective f hf).1 (this J hJ) with ⟨x', hx', rfl⟩
Cleared hypotheses: y, hy, hx, this
-- 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)
⊢ x - x' ∈ J
have a : Membership.mem (γ := Submodule R R) (RingHom.ker f) (x - x')
Tactic: apply h J hJ