awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
inst_11 : Free ℤ R
inst_12 : Free ℤ S
inst_13 : Module.Finite ℤ S
I : Ideal R
inst_14 : Module.Finite ℤ R
rw :
  (absNorm : (a : Ideal ℤ) → ℕ)
      (((relNorm ℤ : Ideal S →*₀ Ideal ℤ) : (a : Ideal S) → Ideal ℤ) (map (F := R →+* S) (algebraMap R S) I) :
        Ideal ℤ) =
    HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) I : ℕ) (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))
⊢ (absNorm : (a : Ideal S) → ℕ) (map (F := R →+* S) (algebraMap R S) I) =
    HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) I : ℕ) (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))
have rw₁ : (absNorm : (a : Ideal ℤ) → ℕ)
    (((relNorm ℤ : Ideal R →*₀ Ideal ℤ) : (a : Ideal R) → Ideal ℤ)
        ((relNorm R : (a : Ideal S) → Ideal R) (map (F := R →+* S) (algebraMap R S) I)) :
      Ideal ℤ) =
  HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) I : ℕ) (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))
Tactic: rw [← absNorm_relNorm ℤ, ← relNorm_relNorm ℤ R, relNorm_algebraMap, absNorm_relNorm, map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
inst_11 : Free ℤ R
inst_12 : Free ℤ S
inst_13 : Module.Finite ℤ S
I : Ideal R
inst_14 : Module.Finite ℤ R
rw :
  (absNorm : (a : Ideal ℤ) → ℕ)
      (((relNorm ℤ : Ideal S →*₀ Ideal ℤ) : (a : Ideal S) → Ideal ℤ) (map (F := R →+* S) (algebraMap R S) I) :
        Ideal ℤ) =
    HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) I : ℕ) (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))
rw₁ :
  (absNorm : (a : Ideal ℤ) → ℕ)
      (((relNorm ℤ : Ideal R →*₀ Ideal ℤ) : (a : Ideal R) → Ideal ℤ)
          ((relNorm R : (a : Ideal S) → Ideal R) (map (F := R →+* S) (algebraMap R S) I)) :
        Ideal ℤ) =
    HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) I : ℕ) (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))
⊢ (absNorm : (a : Ideal S) → ℕ) (map (F := R →+* S) (algebraMap R S) I) =
    HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) I : ℕ) (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))
have rw₂ : (absNorm : (a : Ideal ℤ) → ℕ)
    (((relNorm ℤ : Ideal R →*₀ Ideal ℤ) : (a : Ideal R) → Ideal ℤ)
        (I ^ finrank.{u_1, u_3} (FractionRing R) (FractionRing S)) :
      Ideal ℤ) =
  HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) I : ℕ) (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))
Tactic: rw [← absNorm_relNorm ℤ, ← relNorm_relNorm ℤ R, relNorm_algebraMap, absNorm_relNorm, map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
inst_11 : Free ℤ R
inst_12 : Free ℤ S
inst_13 : Module.Finite ℤ S
I : Ideal R
inst_14 : Module.Finite ℤ R
rw :
  (absNorm : (a : Ideal ℤ) → ℕ)
      (((relNorm ℤ : Ideal S →*₀ Ideal ℤ) : (a : Ideal S) → Ideal ℤ) (map (F := R →+* S) (algebraMap R S) I) :
        Ideal ℤ) =
    HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) I : ℕ) (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))
rw₁ :
  (absNorm : (a : Ideal ℤ) → ℕ)
      (((relNorm ℤ : Ideal R →*₀ Ideal ℤ) : (a : Ideal R) → Ideal ℤ)
          ((relNorm R : (a : Ideal S) → Ideal R) (map (F := R →+* S) (algebraMap R S) I)) :
        Ideal ℤ) =
    HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) I : ℕ) (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))
rw₂ :
  (absNorm : (a : Ideal ℤ) → ℕ)
      (((relNorm ℤ : Ideal R →*₀ Ideal ℤ) : (a : Ideal R) → Ideal ℤ)
          (I ^ finrank.{u_1, u_3} (FractionRing R) (FractionRing S)) :
        Ideal ℤ) =
    HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) I : ℕ) (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))
⊢ (absNorm : (a : Ideal S) → ℕ) (map (F := R →+* S) (algebraMap R S) I) =
    HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) I : ℕ) (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))
have rw₃ : (absNorm : (a : Ideal R) → ℕ) (I ^ finrank.{u_1, u_3} (FractionRing R) (FractionRing S)) =
  HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) I : ℕ) (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))
Tactic: rw [← absNorm_relNorm ℤ, ← relNorm_relNorm ℤ R, relNorm_algebraMap, absNorm_relNorm, map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Norm.RelNorm (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Type u_3
inst_2 : CommRing S
inst_3 : IsDomain S
inst_4 : IsIntegrallyClosed R
inst_5 : IsIntegrallyClosed S
inst_6 : Algebra R S
inst_7 : Module.Finite R S
inst_8 : IsTorsionFree R S
inst_9 : IsDedekindDomain R
inst_10 : IsDedekindDomain S
inst_11 : Free ℤ R
inst_12 : Free ℤ S
inst_13 : Module.Finite ℤ S
I : Ideal R
inst_14 : Module.Finite ℤ R
rw :
  (absNorm : (a : Ideal ℤ) → ℕ)
      (((relNorm ℤ : Ideal S →*₀ Ideal ℤ) : (a : Ideal S) → Ideal ℤ) (map (F := R →+* S) (algebraMap R S) I) :
        Ideal ℤ) =
    HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) I : ℕ) (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))
rw₁ :
  (absNorm : (a : Ideal ℤ) → ℕ)
      (((relNorm ℤ : Ideal R →*₀ Ideal ℤ) : (a : Ideal R) → Ideal ℤ)
          ((relNorm R : (a : Ideal S) → Ideal R) (map (F := R →+* S) (algebraMap R S) I)) :
        Ideal ℤ) =
    HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) I : ℕ) (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))
rw₂ :
  (absNorm : (a : Ideal ℤ) → ℕ)
      (((relNorm ℤ : Ideal R →*₀ Ideal ℤ) : (a : Ideal R) → Ideal ℤ)
          (I ^ finrank.{u_1, u_3} (FractionRing R) (FractionRing S)) :
        Ideal ℤ) =
    HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) I : ℕ) (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))
rw₃ :
  (absNorm : (a : Ideal R) → ℕ) (I ^ finrank.{u_1, u_3} (FractionRing R) (FractionRing S)) =
    HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) I : ℕ) (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))
⊢ (absNorm : (a : Ideal S) → ℕ) (map (F := R →+* S) (algebraMap R S) I) =
    HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) I : ℕ) (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))
have rw₄ : HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) I : ℕ) (finrank.{u_1, u_3} (FractionRing R) (FractionRing S)) =
  HPow.hPow (α := ℕ) ((absNorm : (a : Ideal R) → ℕ) I : ℕ) (finrank.{u_1, u_3} (FractionRing R) (FractionRing S))
Tactic: rw [← absNorm_relNorm ℤ, ← relNorm_relNorm ℤ R, relNorm_algebraMap, absNorm_relNorm, map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Oka (goal)
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
I : Ideal R
hI : Maximal (fun (x : Ideal R) ↦ ¬P x) I
⊢ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
have by_contra! : ∀ (a b : R) (hab : a * b ∈ I) (ha : a ∉ I) (hb : b ∉ I), False
Tactic: by_contra! ⟨a, b, hab, ha, hb⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Oka (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
I : Ideal R
hI : Maximal (fun (x : Ideal R) ↦ ¬P x) I
a b : R
hab : a * b ∈ I
ha : a ∉ I
hb : b ∉ I
⊢ False
have h₁ : P (I ⊔ span {a})
Tactic: have h₁ : P (I ⊔ span {a}) := of_not_not <| hI.not_prop_of_gt (Submodule.lt_sup_iff_notMem.2 ha)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Oka (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
I : Ideal R
hI : Maximal (fun (x : Ideal R) ↦ ¬P x) I
a b : R
hab : a * b ∈ I
ha : a ∉ I
hb : b ∉ I
h₁ : P (I ⊔ span {a})
⊢ False
have h₂ : P (Submodule.colon I (↑(span {a}) : Set R))
Tactic: have h₂ : P (I.colon (span {a})) := of_not_not <| hI.not_prop_of_gt <| lt_of_le_of_ne le_colon
      (fun H ↦ hb <| H ▸ mem_colon_span_singleton.2 (mul_comm a b ▸ hab))
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Oka (goal)
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
hmax : ∀ (I : Ideal R), ¬P I → ∃ (I : Ideal R), Maximal (fun (x : Ideal R) ↦ ¬P x) I
hprime : ∀ (I : Ideal R), I.IsPrime → P I
I : Ideal R
⊢ P I
have by_contra : ∀ (hI : ¬P I), False
Tactic: by_contra hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Oka (goal)
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
hmax : ∀ (I : Ideal R), ¬P I → ∃ (I : Ideal R), Maximal (fun (x : Ideal R) ↦ ¬P x) I
hprime : ∀ (I : Ideal R), I.IsPrime → P I
I : Ideal R
hI : ¬P I
⊢ False
have obtain : ∀ (I : Ideal R) (hI : Maximal (fun (x : Ideal R) ↦ ¬P x) I), False
Tactic: obtain ⟨I, hI⟩ := hmax I hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Oka (goal)
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
hchain : ∀ C ⊆ {I : Ideal R | ¬P I}, IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C → ∀ x ∈ C, P (sSup C) → ∃ I ∈ C, P I
hprime : ∀ (I : Ideal R), I.IsPrime → P I
⊢ ∀ (I : Ideal R), P I
have refine : ∀ (I : Ideal R) (hI : ¬P I), ∃ (I : Ideal R), Maximal (fun (x : Ideal R) ↦ ¬P x) I
Tactic: refine forall_of_forall_prime hP (fun I hI ↦ ?_) hprime
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Oka (goal)
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
hchain : ∀ C ⊆ {I : Ideal R | ¬P I}, IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C → ∀ x ∈ C, P (sSup C) → ∃ I ∈ C, P I
hprime : ∀ (I : Ideal R), I.IsPrime → P I
I : Ideal R
hI : ¬P I
⊢ ∃ (M : Ideal R), I ≤ M ∧ Maximal (fun (x : Ideal R) ↦ ¬P x) M
have refine : ∀ (C : Set (Ideal R)) (hC₁ : C ⊆ {I : Ideal R | ¬P I}) (hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C) (J : Ideal R)
  (hJ : J ∈ C), Membership.mem (γ := Set (Ideal R)) {I : Ideal R | ¬P I} (sSup C)
Tactic: refine zorn_le_nonempty₀ {I | ¬P I} (fun C hC₁ hC₂ J hJ ↦ ⟨sSup C, ?_, fun _ ↦ le_sSup⟩) I hI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Oka (goal)
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
hchain : ∀ C ⊆ {I : Ideal R | ¬P I}, IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C → ∀ x ∈ C, P (sSup C) → ∃ I ∈ C, P I
hprime : ∀ (I : Ideal R), I.IsPrime → P I
I : Ideal R
hI : ¬P I
C : Set (Ideal R)
hC₁ : C ⊆ {I : Ideal R | ¬P I}
hC₂ : IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C
J : Ideal R
hJ : J ∈ C
H : P (sSup C)
⊢ False
have obtain : ∀ (w : Ideal R) (h₁ : w ∈ C) (h₂ : P w), False
Tactic: obtain ⟨_, h₁, h₂⟩ := hchain C hC₁ hC₂ J hJ H
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Oka (goal)
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R → Prop
hP : IsOka P
hchain : ∀ C ⊆ {I : Ideal R | ¬P I}, IsChain (fun (x1 x2 : Ideal R) ↦ x1 ≤ x2) C → ∀ x ∈ C, P (sSup C) → ∃ I ∈ C, P I
hprime : ∀ (I : Ideal R), I.IsPrime → P I
I : Ideal R
hI : ¬P I
⊢ ∃ (I : Ideal R), Maximal (fun (x : Ideal R) ↦ ¬P x) I
have obtain : ∀ (M : Ideal R),
  I ≤ M → ∀ (hM : Maximal (fun (x : Ideal R) ↦ ¬P x) M), ∃ (I : Ideal R), Maximal (fun (x : Ideal R) ↦ ¬P x) I
Tactic: obtain ⟨M, _, hM⟩ : ∃ M, I ≤ M ∧ Maximal (¬P ·) M := by
    refine zorn_le_nonempty₀ {I | ¬P I} (fun C hC₁ hC₂ J hJ ↦ ⟨sSup C, ?_, fun _ ↦ le_sSup⟩) I hI
    intro H
    obtain ⟨_, h₁, h₂⟩ := hchain C hC₁ hC₂ J hJ H
    exact hC₁ h₁ h₂
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R') 0 n ∈ s • N
have zero : 0 ∈ s • N
Tactic: rw [zero_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
x y : R'
hx : Membership.mem (γ := Submodule R' R') (span R' s) x
hy : Membership.mem (γ := Submodule R' R') (span R' s) y
ihr : x • n ∈ s • N
ihs : y • n ∈ s • N
⊢ (x + y) • n ∈ s • N
have add : x • n + y • n ∈ s • N
Tactic: rw [add_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a x : R'
hr : Membership.mem (γ := Submodule R' R') (span R' s) x
h : x • n ∈ s • N
⊢ (a • x) • n ∈ s • N
have hr₁ : ∃ (c : R' →₀ R'), (↑c.support : Set R') ⊆ s ∧ (c.sum fun (mi r : R') ↦ r • mi) = x
Tactic: rw [mem_span_set] at hr
Cleared hypotheses: hr, h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a x : R'
hr : ∃ (c : R' →₀ R'), (↑c.support : Set R') ⊆ s ∧ (c.sum fun (mi r : R') ↦ r • mi) = x
h : x • n ∈ s • N
⊢ (a • x) • n ∈ s • N
have smul : ∀ (c : R' →₀ R') (hc : (↑c.support : Set R') ⊆ s),
  HSMul.hSMul (α := R') (c.sum fun (mi r : R') ↦ r • mi) n ∈ s • N →
    HSMul.hSMul (β := R') a (c.sum fun (mi r : R') ↦ r • mi) • n ∈ s • N
Tactic: obtain ⟨c, hc, rfl⟩ := hr
Cleared hypotheses: x, hr, h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a : R'
c : R' →₀ R'
hc : (↑c.support : Set R') ⊆ s
h : HSMul.hSMul (α := R') (c.sum fun (mi r : R') ↦ r • mi) n ∈ s • N
⊢ HSMul.hSMul (β := R') a (c.sum fun (mi r : R') ↦ r • mi) • n ∈ s • N
have smul : ∑ i ∈ c.support, (a • HSMul.hSMul (α := R') ((c : (a : R') → R') i : R') i) • n ∈ s • N
Tactic: rw [Finsupp.sum, Finset.smul_sum, Finset.sum_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a : R'
c : R' →₀ R'
hc : (↑c.support : Set R') ⊆ s
h : HSMul.hSMul (α := R') (c.sum fun (mi r : R') ↦ r • mi) n ∈ s • N
⊢ ∑ i ∈ c.support, (a • HSMul.hSMul (α := R') ((c : (a : R') → R') i : R') i) • n ∈ s • N
have smul : ∀ (i : R') (hi : i ∈ c.support), (a • HSMul.hSMul (α := R') ((c : (a : R') → R') i : R') i) • n ∈ s • N
Tactic: refine Submodule.sum_mem _ fun i hi => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hn : n ∈ N
a : R'
c : R' →₀ R'
hc : (↑c.support : Set R') ⊆ s
h : HSMul.hSMul (α := R') (c.sum fun (mi r : R') ↦ r • mi) n ∈ s • N
i : R'
hi : i ∈ c.support
⊢ (a • HSMul.hSMul (α := R') ((c : (a : R') → R') i : R') i) • n ∈ s • N
have smul : i • HMul.hMul (β := R') a ((c : (a : R') → R') i : R') • n ∈ s • N
Tactic: rw [← mul_smul, smul_eq_mul, mul_comm, mul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hr : r ∈ (↑(Ideal.span s) : Set R')
hn : n ∈ N
⊢ r • n ∈ s • N
have mem : ∀ (x : R') (h : x ∈ s), x • n ∈ s • N
Tactic: induction hr using Submodule.span_induction with
        | mem _ h => exact mem_set_smul_of_mem_mem h hn
        | zero => rw [zero_smul]; exact Submodule.zero_mem _
        | add _ _ _ _ ihr ihs => rw [add_smul]; exact Submodule.add_mem _ ihr ihs
        | smul _ _ hr =>
          rw [mem_span_set] at hr
          obtain ⟨c, hc, rfl⟩ := hr
          rw [Finsupp.sum, Finset.smul_sum, Finset.sum_smul]
          refine Submodule.sum_mem _ fun i hi => ?_
          rw [← mul_smul, smul_eq_mul, mul_comm, mul_smul]
          exact mem_set_smul_of_mem_mem (hc hi) <| Submodule.smul_mem _ _ hn
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hr : r ∈ (↑(Ideal.span s) : Set R')
hn : n ∈ N
mem : ∀ (x : R') (h : x ∈ s), x • n ∈ s • N
⊢ r • n ∈ s • N
have zero : HSMul.hSMul.{u_1, u_2, u_2} (α := R') 0 n ∈ s • N
Tactic: induction hr using Submodule.span_induction with
        | mem _ h => exact mem_set_smul_of_mem_mem h hn
        | zero => rw [zero_smul]; exact Submodule.zero_mem _
        | add _ _ _ _ ihr ihs => rw [add_smul]; exact Submodule.add_mem _ ihr ihs
        | smul _ _ hr =>
          rw [mem_span_set] at hr
          obtain ⟨c, hc, rfl⟩ := hr
          rw [Finsupp.sum, Finset.smul_sum, Finset.sum_smul]
          refine Submodule.sum_mem _ fun i hi => ?_
          rw [← mul_smul, smul_eq_mul, mul_comm, mul_smul]
          exact mem_set_smul_of_mem_mem (hc hi) <| Submodule.smul_mem _ _ hn
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hr : r ∈ (↑(Ideal.span s) : Set R')
hn : n ∈ N
mem : ∀ (x : R') (h : x ∈ s), x • n ∈ s • N
zero : HSMul.hSMul.{u_1, u_2, u_2} (α := R') 0 n ∈ s • N
⊢ r • n ∈ s • N
have add : ∀ (x y : R'),
  Membership.mem (γ := Submodule R' R') (span R' s) x →
    Membership.mem (γ := Submodule R' R') (span R' s) y →
      ∀ (ihr : x • n ∈ s • N) (ihs : y • n ∈ s • N), (x + y) • n ∈ s • N
Tactic: induction hr using Submodule.span_induction with
        | mem _ h => exact mem_set_smul_of_mem_mem h hn
        | zero => rw [zero_smul]; exact Submodule.zero_mem _
        | add _ _ _ _ ihr ihs => rw [add_smul]; exact Submodule.add_mem _ ihr ihs
        | smul _ _ hr =>
          rw [mem_span_set] at hr
          obtain ⟨c, hc, rfl⟩ := hr
          rw [Finsupp.sum, Finset.smul_sum, Finset.sum_smul]
          refine Submodule.sum_mem _ fun i hi => ?_
          rw [← mul_smul, smul_eq_mul, mul_comm, mul_smul]
          exact mem_set_smul_of_mem_mem (hc hi) <| Submodule.smul_mem _ _ hn
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R' : Type u_1
M' : Type u_2
inst : CommSemiring R'
inst_1 : AddCommMonoid M'
inst_2 : Module R' M'
s : Set R'
N : Submodule R' M'
r : R'
n : M'
hr : r ∈ (↑(Ideal.span s) : Set R')
hn : n ∈ N
mem : ∀ (x : R') (h : x ∈ s), x • n ∈ s • N
zero : HSMul.hSMul.{u_1, u_2, u_2} (α := R') 0 n ∈ s • N
add :
  ∀ (x y : R'),
    Membership.mem (γ := Submodule R' R') (span R' s) x →
      Membership.mem (γ := Submodule R' R') (span R' s) y →
        ∀ (ihr : x • n ∈ s • N) (ihs : y • n ∈ s • N), (x + y) • n ∈ s • N
⊢ r • n ∈ s • N
have smul : ∀ (a x : R') (hr : Membership.mem (γ := Submodule R' R') (span R' s) x), x • n ∈ s • N → (a • x) • n ∈ s • N
Tactic: induction hr using Submodule.span_induction with
        | mem _ h => exact mem_set_smul_of_mem_mem h hn
        | zero => rw [zero_smul]; exact Submodule.zero_mem _
        | add _ _ _ _ ihr ihs => rw [add_smul]; exact Submodule.add_mem _ ihr ihs
        | smul _ _ hr =>
          rw [mem_span_set] at hr
          obtain ⟨c, hc, rfl⟩ := hr
          rw [Finsupp.sum, Finset.smul_sum, Finset.sum_smul]
          refine Submodule.sum_mem _ fun i hi => ?_
          rw [← mul_smul, smul_eq_mul, mul_comm, mul_smul]
          exact mem_set_smul_of_mem_mem (hc hi) <| Submodule.smul_mem _ _ hn
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
a : M
⊢ Eq (α := AddSubgroup M) (toAddSubgroup (module_M := AddCommGroup.toIntModule M) (ℤ ∙ a)) (AddSubgroup.zmultiples a)
have h : ∀ (i : M),
  Membership.mem (γ := AddSubgroup M) (toAddSubgroup (module_M := AddCommGroup.toIntModule M) (ℤ ∙ a)) i ↔
    Membership.mem (γ := AddSubgroup M) (AddSubgroup.zmultiples a) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
f : R →ₗ[R] M
y : R
hy : y ∈ (↑I : Set R)
⊢ Membership.mem (α := M) (HSMul.hSMul (β := Submodule R M) I ⊤) ((f : (a : R) → M) y : M)
have rw : HSMul.hSMul (β := M) y ((f : (a : R) → M) 1 : M) ∈ HSMul.hSMul (β := Submodule R M) I ⊤
Tactic: rw [← mul_one y, ← smul_eq_mul, f.map_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Submodule R M
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
x : M
H : ∀ (r : (↑s : Type u)), (↑r : R) • x ∈ M'
this : LinearMap.range (LinearMap.toSpanSingleton R M x) ≤ M'
⊢ x ∈ M'
have rw : Membership.mem (α := M) M' ((LinearMap.toSpanSingleton R M x : (a : R) → M) 1 : M)
Tactic: rw [← LinearMap.toSpanSingleton_apply_one R M x]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Submodule R M
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
x : M
H : ∀ (r : (↑s : Type u)), (↑r : R) • x ∈ M'
⊢ x ∈ M'
have suffices : LinearMap.range (LinearMap.toSpanSingleton R M x) ≤ M'
Tactic: suffices LinearMap.range (LinearMap.toSpanSingleton R M x) ≤ M' by
    rw [← LinearMap.toSpanSingleton_apply_one R M x]
    exact this (LinearMap.mem_range_self _ 1)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Submodule R M
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
x : M
H : ∀ (r : (↑s : Type u)), (↑r : R) • x ∈ M'
⊢ LinearMap.range (LinearMap.toSpanSingleton R M x) ≤ M'
have rw : s ⊆ (↑(comap (LinearMap.toSpanSingleton R M x) M') : Set R)
Tactic: rw [LinearMap.range_eq_map, ← hs, map_le_iff_le_comap, Ideal.span, span_le]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
x : ↥N
⊢ map N.subtype (HSMul.hSMul (β := Submodule R ↥N) I ⊤) = I • N
have rw : I • map N.subtype ⊤ = I • N
Tactic: rw [Submodule.map_smul'', Submodule.map_top, Submodule.range_subtype]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
x : ↥N
rw : I • map N.subtype ⊤ = I • N
⊢ map N.subtype (HSMul.hSMul (β := Submodule R ↥N) I ⊤) = I • N
have rw₁ : I • N.subtype.range = I • N
Tactic: rw [Submodule.map_smul'', Submodule.map_top, Submodule.range_subtype]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
x : ↥N
rw : I • map N.subtype ⊤ = I • N
rw₁ : I • N.subtype.range = I • N
⊢ map N.subtype (HSMul.hSMul (β := Submodule R ↥N) I ⊤) = I • N
have rw₂ : I • N = I • N
Tactic: rw [Submodule.map_smul'', Submodule.map_top, Submodule.range_subtype]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Ideal R
N : Submodule R M
x : ↥N
⊢ x ∈ HSMul.hSMul (β := Submodule R ↥N) I ⊤ ↔ (↑x : M) ∈ I • N
have this : map N.subtype (HSMul.hSMul (β := Submodule R ↥N) I ⊤) = I • N
Tactic: have : Submodule.map N.subtype (I • ⊤) = I • N := by
    rw [Submodule.map_smul'', Submodule.map_top, Submodule.range_subtype]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type w
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
S : Submodule R M'
I : Ideal R
⊢ I • comap f S ≤ comap f (I • S)
have refine : ∀ (r : R) (hr : r ∈ I) (x : M) (hx : x ∈ comap f S), r • x ∈ comap f (I • S)
Tactic: refine Submodule.smul_le.mpr fun r hr x hx => ?_