awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
Rₚ : Type u_3
Sₚ : Type u_4
inst_5 : CommRing Rₚ
inst_6 : IsDomain Rₚ
inst_7 : CommRing Sₚ
inst_8 : Algebra R Rₚ
inst_9 : Algebra R Sₚ
inst_10 : Algebra S Sₚ
inst_11 : Algebra Rₚ Sₚ
inst_12 : IsScalarTower R S Sₚ
inst_13 : IsScalarTower R Rₚ Sₚ
M : Submonoid R
hM : M ≤ R⁰
inst_14 : IsLocalization M Rₚ
inst_15 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
inst_16 : Module.IsTorsionFree R S
e : LE.le (α := Submonoid S) (Algebra.algebraMapSubmonoid S M) S⁰
this_1 : IsDomain Sₚ
this : Eq (α := Rₚ →+* Sₚ) (algebraMap Rₚ Sₚ) (map (T := Algebra.algebraMapSubmonoid S M) Sₚ (algebraMap R S) ⋯)
x : R
s : ↥M
a : R
ha : a ∈ (↑M : Set R)
H : HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) x : S) = 0
⊢ ∃ a ∈ M, a * x = 0
have H₁ : a * x = 0
Tactic: simp only [← map_mul,
    (injective_iff_map_eq_zero' _).mp (FaithfulSMul.algebraMap_injective R S)] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst_4 : CommRing R'
inst_5 : CommRing S'
inst_6 : Algebra R' S'
f : R →+* R'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
g : S →+* S'
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := S') (⇑g : (a : S) → S')
H : g.comp (algebraMap R S) = RingHom.comp (algebraMap R' S') f
H' : LE.le (α := Ideal S) (RingHom.ker g) (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker f))
z : S'
⊢ ∃ (x : R' × ↥(Submonoid.map f M)),
    HMul.hMul (β := S') z ((algebraMap R' S' : (a : R') → S') (↑x.2 : R') : S') = (algebraMap R' S' : (a : R') → S') x.1
have obtain : ∀ (z : S),
  ∃ (x : R' × ↥(Submonoid.map f M)),
    HMul.hMul (α := S') (β := S') ((g : (a : S) → S') z : S') ((algebraMap R' S' : (a : R') → S') (↑x.2 : R') : S') =
      (algebraMap R' S' : (a : R') → S') x.1
Tactic: obtain ⟨z, rfl⟩ := hg z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst_4 : CommRing R'
inst_5 : CommRing S'
inst_6 : Algebra R' S'
f : R →+* R'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
g : S →+* S'
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := S') (⇑g : (a : S) → S')
H : g.comp (algebraMap R S) = RingHom.comp (algebraMap R' S') f
H' : LE.le (α := Ideal S) (RingHom.ker g) (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker f))
z : S
⊢ ∃ (x : R' × ↥(Submonoid.map f M)),
    HMul.hMul (α := S') (β := S') ((g : (a : S) → S') z : S') ((algebraMap R' S' : (a : R') → S') (↑x.2 : R') : S') =
      (algebraMap R' S' : (a : R') → S') x.1
have obtain : ∀ (r : R) (s : ↥M)
  (e :
    HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑(r, s).2 : R) : S) =
      (algebraMap R S : (a : R) → S) (r, s).1),
  ∃ (x : R' × ↥(Submonoid.map f M)),
    HMul.hMul (α := S') (β := S') ((g : (a : S) → S') z : S') ((algebraMap R' S' : (a : R') → S') (↑x.2 : R') : S') =
      (algebraMap R' S' : (a : R') → S') x.1
Tactic: obtain ⟨⟨r, s⟩, e⟩ := IsLocalization.surj M z
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst_4 : CommRing R'
inst_5 : CommRing S'
inst_6 : Algebra R' S'
f : R →+* R'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
g : S →+* S'
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := S') (⇑g : (a : S) → S')
H : g.comp (algebraMap R S) = RingHom.comp (algebraMap R' S') f
H' : LE.le (α := Ideal S) (RingHom.ker g) (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker f))
z : S
r : R
s : ↥M
e : HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑(r, s).2 : R) : S) = (algebraMap R S : (a : R) → S) (r, s).1
⊢ ∃ (x : R' × ↥(Submonoid.map f M)),
    HMul.hMul (α := S') (β := S') ((g : (a : S) → S') z : S') ((algebraMap R' S' : (a : R') → S') (↑x.2 : R') : S') =
      (algebraMap R' S' : (a : R') → S') x.1
have refine : HMul.hMul (α := S') (β := S') ((g : (a : S) → S') z : S')
    ((algebraMap R' S' : (a : R') → S')
        ((↑((f : (a : R) → R') r,
                  Subtype.mk (p := fun (x : R') ↦ Membership.mem (γ := Submonoid R') (Submonoid.map f M) x)
                    ((f : (a : R) → R') (↑s : R)) sorry).2 :
            R') :
          R') :
      S') =
  (algebraMap R' S' : (a : R') → S')
    (((f : (a : R) → R') r,
          Subtype.mk (p := fun (x : R') ↦ Membership.mem (γ := Submonoid R') (Submonoid.map f M) x)
            ((f : (a : R) → R') (↑s : R)) sorry).1 :
      R')
Tactic: refine ⟨⟨f r, _, s.1, s.2, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst_4 : CommRing R'
inst_5 : CommRing S'
inst_6 : Algebra R' S'
f : R →+* R'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
g : S →+* S'
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := S') (⇑g : (a : S) → S')
H : g.comp (algebraMap R S) = RingHom.comp (algebraMap R' S') f
H' : LE.le (α := Ideal S) (RingHom.ker g) (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker f))
x y : R'
e : Eq.{u_4 + 1} (α := S') ((algebraMap R' S' : (a : R') → S') x : S') ((algebraMap R' S' : (a : R') → S') y : S')
⊢ ∃ (c : ↥(Submonoid.map f M)), (↑c : R') * x = (↑c : R') * y
have obtain : ∀ (x : R)
  (e :
    Eq.{u_4 + 1} (α := S') ((algebraMap R' S' : (a : R') → S') ((f : (a : R) → R') x : R') : S')
      ((algebraMap R' S' : (a : R') → S') y : S')),
  ∃ (c : ↥(Submonoid.map f M)), HMul.hMul (β := R') (↑c : R') ((f : (a : R) → R') x : R') = (↑c : R') * y
Tactic: obtain ⟨x, rfl⟩ := hf x
Cleared hypotheses: x, e
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst_4 : CommRing R'
inst_5 : CommRing S'
inst_6 : Algebra R' S'
f : R →+* R'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
g : S →+* S'
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := S') (⇑g : (a : S) → S')
H : g.comp (algebraMap R S) = RingHom.comp (algebraMap R' S') f
H' : LE.le (α := Ideal S) (RingHom.ker g) (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker f))
y : R'
x : R
e :
  Eq.{u_4 + 1} (α := S') ((algebraMap R' S' : (a : R') → S') ((f : (a : R) → R') x : R') : S')
    ((algebraMap R' S' : (a : R') → S') y : S')
⊢ ∃ (c : ↥(Submonoid.map f M)), HMul.hMul (β := R') (↑c : R') ((f : (a : R) → R') x : R') = (↑c : R') * y
have obtain : ∀ (y : R)
  (e :
    Eq.{u_4 + 1} (α := S') ((algebraMap R' S' : (a : R') → S') ((f : (a : R) → R') x : R') : S')
      ((algebraMap R' S' : (a : R') → S') ((f : (a : R) → R') y : R') : S')),
  ∃ (c : ↥(Submonoid.map f M)),
    HMul.hMul (β := R') (↑c : R') ((f : (a : R) → R') x : R') =
      HMul.hMul (β := R') (↑c : R') ((f : (a : R) → R') y : R')
Tactic: obtain ⟨y, rfl⟩ := hf y
Cleared hypotheses: y, e
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst_4 : CommRing R'
inst_5 : CommRing S'
inst_6 : Algebra R' S'
f : R →+* R'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
g : S →+* S'
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := S') (⇑g : (a : S) → S')
H : g.comp (algebraMap R S) = RingHom.comp (algebraMap R' S') f
H' : LE.le (α := Ideal S) (RingHom.ker g) (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker f))
x y : R
e :
  Eq.{u_4 + 1} (α := S') ((algebraMap R' S' : (a : R') → S') ((f : (a : R) → R') x : R') : S')
    ((algebraMap R' S' : (a : R') → S') ((f : (a : R) → R') y : R') : S')
⊢ ∃ (c : ↥(Submonoid.map f M)),
    HMul.hMul (β := R') (↑c : R') ((f : (a : R) → R') x : R') =
      HMul.hMul (β := R') (↑c : R') ((f : (a : R) → R') y : R')
have e₁ : Eq.{u_4 + 1} (α := S') ((g : (a : S) → S') (mk' (M := M) S (x - y) 1) : S') (0 : S')
Tactic: rw [← sub_eq_zero, ← map_sub, ← map_sub, ← RingHom.comp_apply, ← H, RingHom.comp_apply,
      ← IsLocalization.mk'_one (M := M)] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Ideal (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
R' : Type u_3
S' : Type u_4
inst_4 : CommRing R'
inst_5 : CommRing S'
inst_6 : Algebra R' S'
f : R →+* R'
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := R') (⇑f : (a : R) → R')
g : S →+* S'
hg : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := S') (⇑g : (a : S) → S')
H : g.comp (algebraMap R S) = RingHom.comp (algebraMap R' S') f
H' : LE.le (α := Ideal S) (RingHom.ker g) (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker f))
x y : R
e : Eq.{u_4 + 1} (α := S') ((g : (a : S) → S') (mk' (M := M) S (x - y) 1) : S') (0 : S')
⊢ ∃ (c : ↥(Submonoid.map f M)),
    HMul.hMul (β := R') (↑c : R') ((f : (a : R) → R') x : R') =
      HMul.hMul (β := R') (↑c : R') ((f : (a : R) → R') y : R')
have obtain : ∀ (r : R) (hr : r ∈ M) (hr' : Membership.mem (γ := Ideal R) (RingHom.ker f) (r * (x - y))),
  ∃ (c : ↥(Submonoid.map f M)),
    HMul.hMul (β := R') (↑c : R') ((f : (a : R) → R') x : R') =
      HMul.hMul (β := R') (↑c : R') ((f : (a : R) → R') y : R')
Tactic: obtain ⟨r, hr, hr'⟩ := (IsLocalization.mk'_mem_map_algebraMap_iff M _ _ _ _).mp (H' e)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
a : R
b : S
hb : IsInteger R b
⊢ IsInteger R (a • b)
have rcases : ∀ (b' : R) (hb : (algebraMap R S : (a : R) → S) b' = b), IsInteger R (a • b)
Tactic: rcases hb with ⟨b', hb⟩
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
a : R
b : S
b' : R
hb : (algebraMap R S : (a : R) → S) b' = b
⊢ IsInteger R (a • b)
have h : (algebraMap R S : (a : R) → S) (a * b') = a • b
Tactic: use a * b'
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
a : R
b : S
b' : R
hb : (algebraMap R S : (a : R) → S) b' = b
⊢ (algebraMap R S : (a : R) → S) (a * b') = a • b
have h : (algebraMap R S : (a : R) → S) (a * b') = HSMul.hSMul (β := S) a ((algebraMap R S : (a : R) → S) b' : S)
Tactic: rw [← hb, (algebraMap R S).map_mul, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
a : R
b : S
b' : R
hb : (algebraMap R S : (a : R) → S) b' = b
h : (algebraMap R S : (a : R) → S) (a * b') = HSMul.hSMul (β := S) a ((algebraMap R S : (a : R) → S) b' : S)
⊢ (algebraMap R S : (a : R) → S) (a * b') = a • b
have h₁ : HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b' : S) =
  HSMul.hSMul (β := S) a ((algebraMap R S : (a : R) → S) b' : S)
Tactic: rw [← hb, (algebraMap R S).map_mul, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
a : R
b : S
b' : R
hb : (algebraMap R S : (a : R) → S) b' = b
h : (algebraMap R S : (a : R) → S) (a * b') = HSMul.hSMul (β := S) a ((algebraMap R S : (a : R) → S) b' : S)
h₁ :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b' : S) =
    HSMul.hSMul (β := S) a ((algebraMap R S : (a : R) → S) b' : S)
⊢ (algebraMap R S : (a : R) → S) (a * b') = a • b
have h₂ : HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b' : S) =
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b' : S)
Tactic: rw [← hb, (algebraMap R S).map_mul, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
a : S
⊢ ∃ (b : ↥M), IsInteger R ((↑b : R) • a)
have simp_rw : ∃ (b : ↥M), IsInteger R (HMul.hMul (β := S) a ((algebraMap R S : (a : R) → S) (↑b : R) : S))
Tactic: simp_rw [Algebra.smul_def, mul_comm _ a]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
⊢ ∃ (b : ↥M), ∀ i ∈ s, IsInteger R ((↑b : R) • f i)
have haveI : ∀ (this : (a : Prop) → Decidable a), ∃ (b : ↥M), ∀ i ∈ s, IsInteger R ((↑b : R) • f i)
Tactic: haveI := Classical.propDecidable
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
⊢ ∃ (b : ↥M), ∀ i ∈ s, IsInteger R ((↑b : R) • f i)
have refine_1 : (i : ι) → (hi : i ∈ s) → R
Tactic: refine ⟨∏ i ∈ s, (sec M (f i)).2, fun i hi => ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
refine_1 : (i : ι) → (hi : i ∈ s) → R
⊢ ∃ (b : ↥M), ∀ i ∈ s, IsInteger R ((↑b : R) • f i)
have refine_2 : ∀ (i : ι) (hi : i ∈ s),
  (algebraMap R S : (a : R) → S) ((↑(∏ j ∈ s.erase i, (sec M (f j)).2) : R) * (sec M (f i)).1) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (↑(∏ i ∈ s, (sec M (f i)).2) : R) (f i)
Tactic: refine ⟨∏ i ∈ s, (sec M (f i)).2, fun i hi => ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ (algebraMap R S : (a : R) → S) ((↑(∏ j ∈ s.erase i, (sec M (f j)).2) : R) * (sec M (f i)).1) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (↑(∏ i ∈ s, (sec M (f i)).2) : R) (f i)
have refine_2 : ((↑(∏ j ∈ s.erase i, (sec M (f j)).2) : R) * (↑(sec M (f i)).2 : R)) • f i =
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (↑(∏ i ∈ s, (sec M (f i)).2) : R) (f i)
Tactic: rw [map_mul, sec_spec', ← mul_assoc, ← (algebraMap R S).map_mul, ← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ ((↑(∏ j ∈ s.erase i, (sec M (f j)).2) : R) * (↑(sec M (f i)).2 : R)) • f i =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (↑(∏ i ∈ s, (sec M (f i)).2) : R) (f i)
have refine_2 : (↑(∏ j ∈ s.erase i, (sec M (f j)).2) : R) * (↑(sec M (f i)).2 : R) = (↑(∏ i ∈ s, (sec M (f i)).2) : R)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ (↑(∏ j ∈ s.erase i, (sec M (f j)).2) : R) * (↑(sec M (f i)).2 : R) = (↑(∏ i ∈ s, (sec M (f i)).2) : R)
have refine_2 : (↑(∏ j ∈ s.erase i, (sec M (f j)).2) : R) * (↑(sec M (f i)).2 : R) = ∏ x ∈ s, (M.subtype : (a : ↥M) → R) (sec M (f x)).2
Tactic: refine _root_.trans ?_ (map_prod (Submonoid.subtype M) _ _).symm
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
ι : Type u_4
s : Finset ι
f : ι → S
this : (a : Prop) → Decidable a
i : ι
hi : i ∈ s
⊢ (↑(∏ j ∈ s.erase i, (sec M (f j)).2) : R) * (↑(sec M (f i)).2 : R) =
    ∏ x ∈ s, (M.subtype : (a : ↥M) → R) (sec M (f x)).2
have refine_2 : Eq.{u_1 + 1} (α := R) (∏ x ∈ s, (↑(sec M (f x)).2 : R)) (∏ x ∈ s, (M.subtype : (a : ↥M) → R) (sec M (f x)).2)
Tactic: rw [mul_comm, Submonoid.coe_finsetProd,
    -- Porting note: explicitly supplied `f`
    ← Finset.prod_insert (f := fun i => ((sec M (f i)).snd : R)) (s.notMem_erase i),
    Finset.insert_erase hi]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
ι : Type u_4
inst_4 : Finite ι
f : ι → S
⊢ ∃ (b : ↥M), ∀ (i : ι), IsInteger R ((↑b : R) • f i)
have intro : ∀ (val : Fintype ι), ∃ (b : ↥M), ∀ (i : ι), IsInteger R ((↑b : R) • f i)
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
ι : Type u_4
inst_4 : Finite ι
f : ι → S
val : Fintype ι
⊢ ∃ (b : ↥M), ∀ (i : ι), IsInteger R ((↑b : R) • f i)
have intro : ∀ (b : ↥M) (hb : ∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → IsInteger R ((↑b : R) • f i)),
  ∃ (b : ↥M), ∀ (i : ι), IsInteger R ((↑b : R) • f i)
Tactic: obtain ⟨b, hb⟩ := exist_integer_multiples M Finset.univ f
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
inst_4 : DecidableEq R
s : Finset S
⊢ (⇑(algebraMap R S) : (a : R) → S) '' (↑(Finset.image (fun (t : ↥s) ↦ integerMultiple M s id t) s.attach) : Set R) =
    commonDenomOfFinset M s • (↑s : Set S)
have rw : Set.image.{u_1, u_2} (α := R) (⇑(algebraMap R S) : (a : R) → S)
    ((fun (t : ↥s) ↦ integerMultiple M s id t) '' (↑s.attach : Set ↥s)) =
  commonDenomOfFinset M s • (↑s : Set S)
Tactic: rw [Finset.coe_image]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
inst_4 : DecidableEq R
s : Finset S
⊢ Set.image.{u_1, u_2} (α := R) (⇑(algebraMap R S) : (a : R) → S)
      ((fun (t : ↥s) ↦ integerMultiple M s id t) '' (↑s.attach : Set ↥s)) =
    commonDenomOfFinset M s • (↑s : Set S)
have h : ∀ (x : S),
  Membership.mem (γ := Set S)
      (Set.image.{u_1, u_2} (α := R) (⇑(algebraMap R S) : (a : R) → S)
        ((fun (t : ↥s) ↦ integerMultiple M s id t) '' (↑s.attach : Set ↥s)))
      x ↔
    x ∈ commonDenomOfFinset M s • (↑s : Set S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
inst_4 : DecidableEq R
s : Finset S
x : S
⊢ Membership.mem (γ := Set S)
      (Set.image.{u_1, u_2} (α := R) (⇑(algebraMap R S) : (a : R) → S)
        ((fun (t : ↥s) ↦ integerMultiple M s id t) '' (↑s.attach : Set ↥s)))
      x ↔
    x ∈ commonDenomOfFinset M s • (↑s : Set S)
have h : Membership.mem (γ := Set S)
    (Set.image.{u_1, u_2} (α := R) (⇑(algebraMap R S) : (a : R) → S)
      ((fun (t : ↥s) ↦ integerMultiple M s id t) '' (↑s.attach : Set ↥s)))
    x →
  x ∈ commonDenomOfFinset M s • (↑s : Set S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
inst_4 : DecidableEq R
s : Finset S
x : S
h :
  Membership.mem (γ := Set S)
      (Set.image.{u_1, u_2} (α := R) (⇑(algebraMap R S) : (a : R) → S)
        ((fun (t : ↥s) ↦ integerMultiple M s id t) '' (↑s.attach : Set ↥s)))
      x →
    x ∈ commonDenomOfFinset M s • (↑s : Set S)
⊢ Membership.mem (γ := Set S)
      (Set.image.{u_1, u_2} (α := R) (⇑(algebraMap R S) : (a : R) → S)
        ((fun (t : ↥s) ↦ integerMultiple M s id t) '' (↑s.attach : Set ↥s)))
      x ↔
    x ∈ commonDenomOfFinset M s • (↑s : Set S)
have h₁ : x ∈ commonDenomOfFinset M s • (↑s : Set S) →
  Membership.mem (γ := Set S)
    (Set.image.{u_1, u_2} (α := R) (⇑(algebraMap R S) : (a : R) → S)
      ((fun (t : ↥s) ↦ integerMultiple M s id t) '' (↑s.attach : Set ↥s)))
    x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integer (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
inst_4 : DecidableEq R
s : Finset S
x : ↥s
⊢ Membership.mem (α := S) (commonDenomOfFinset M s • (↑s : Set S))
    ((algebraMap R S : (a : R) → S) ((fun (t : ↥s) ↦ integerMultiple M s id t) x) : S)
have h : commonDenom M s id • id (↑x : S) ∈ commonDenomOfFinset M s • (↑s : Set S)
Tactic: rw [map_integerMultiple]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
p : S[X]
⊢ ∃ b ∈ M, ∃ (q : R[X]), Polynomial.map (algebraMap R S) q = b • p ∧ q.support ⊆ p.support
have obtain : ∀ (b : R) (hb : b ∈ (↑M : Set R))
  (h :
    IsInteger.{u_1, u_2} R[X]
      (HSMul.hSMul (α := R[X])
        ((↑(Subtype.mk (p := fun (x : R[X]) ↦
                Membership.mem (γ := Submonoid R[X]) (Submonoid.map (F := R →+* R[X]) C M) x) ((C : (a : R) → R[X]) b)
                sorry) :
            R[X]) :
          R[X])
        p)),
  ∃ b ∈ M, ∃ (q : R[X]), Polynomial.map (algebraMap R S) q = b • p ∧ q.support ⊆ p.support
Tactic: obtain ⟨⟨_, b, hb, rfl⟩, h⟩ := exists_integer_multiple (Submonoid.map C M) p
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
p : S[X]
b : R
hb : b ∈ (↑M : Set R)
h :
  IsInteger.{u_1, u_2} R[X]
    (HSMul.hSMul (α := R[X])
      ((↑(Subtype.mk (p := fun (x : R[X]) ↦
              Membership.mem (γ := Submonoid R[X]) (Submonoid.map (F := R →+* R[X]) C M) x) ((C : (a : R) → R[X]) b)
              ⋯) :
          R[X]) :
        R[X])
      p)
⊢ ∃ b ∈ M, ∃ (q : R[X]), Polynomial.map (algebraMap R S) q = b • p ∧ q.support ⊆ p.support
have h₁ : IsInteger.{u_1, u_2} R[X] (b • p)
Tactic: rw [Subtype.coe_mk, C_eq_algebraMap, algebraMap_smul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
p : S[X]
b : R
hb : b ∈ (↑M : Set R)
h : IsInteger.{u_1, u_2} R[X] (b • p)
⊢ ∃ b ∈ M, ∃ (q : R[X]), Polynomial.map (algebraMap R S) q = b • p ∧ q.support ⊆ p.support
have obtain : ∀ (q' : R[X]) (h₁ : Polynomial.map (algebraMap R S) q' = b • p) (h₂ : q'.support = (b • p).support),
  ∃ b ∈ M, ∃ (q : R[X]), Polynomial.map (algebraMap R S) q = b • p ∧ q.support ⊆ p.support
Tactic: obtain ⟨q', h₁, h₂⟩ := exists_support_eq_of_mem_lifts h