awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_4
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
e : R
he : IsIdempotentElem e
H : Eq (α := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S)) (Ideal.span {1 - e})
H' : Function.Surjective.{u_4 + 1, u_5 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
x y : R
⊢ Eq.{u_5 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) ↔ e * x = e * y
have rw : x • e = y • e ↔ e * x = e * y
Tactic: rw [← sub_eq_zero, ← map_sub, ← RingHom.mem_ker, H, ← he.ker_toSpanSingleton_eq_span,
      LinearMap.mem_ker, LinearMap.toSpanSingleton_apply, sub_smul, sub_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_4
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
e : R
he : IsIdempotentElem e
H : Eq (α := Ideal R) (RingHom.ker (F := R →+* S) (algebraMap R S)) (Ideal.span {1 - e})
H' : Function.Surjective.{u_4 + 1, u_5 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
x y : R
⊢ x • e = y • e ↔ e * x = e * y
have simp_rw : x • e = y • e ↔ x * e = y * e
Tactic: simp_rw [mul_comm e, smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S_1
R : Type u_4
S : Type u_5
inst_5 : CommSemiring R
inst_6 : CommSemiring S
this : Algebra (R × S) R := RingHom.toAlgebra (RingHom.fst R S)
⊢ IsIdempotentElem (M := R × S) (1, 0)
have fst : (HMul.hMul (α := R × S) (1, 0) (1, 0)).1 = (1, 0).1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S_1
R : Type u_4
S : Type u_5
inst_5 : CommSemiring R
inst_6 : CommSemiring S
this : Algebra (R × S) R := RingHom.toAlgebra (RingHom.fst R S)
fst : (HMul.hMul (α := R × S) (1, 0) (1, 0)).1 = (1, 0).1
⊢ IsIdempotentElem (M := R × S) (1, 0)
have snd : (HMul.hMul (α := R × S) (1, 0) (1, 0)).2 = (1, 0).2
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S_1
R : Type u_4
S : Type u_5
inst_5 : CommSemiring R
inst_6 : CommSemiring S
this : Algebra (R × S) S := RingHom.toAlgebra (RingHom.snd R S)
⊢ IsIdempotentElem (M := R × S) (0, 1)
have fst : (HMul.hMul (α := R × S) (0, 1) (0, 1)).1 = (0, 1).1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S_1
R : Type u_4
S : Type u_5
inst_5 : CommSemiring R
inst_6 : CommSemiring S
this : Algebra (R × S) S := RingHom.toAlgebra (RingHom.snd R S)
fst : (HMul.hMul (α := R × S) (0, 1) (0, 1)).1 = (0, 1).1
⊢ IsIdempotentElem (M := R × S) (0, 1)
have snd : (HMul.hMul (α := R × S) (0, 1) (0, 1)).2 = (0, 1).2
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
S : Type u_4
T : Type u_5
inst : CommRing S
inst_1 : CommRing T
inst_2 : Algebra S T
h₁ : Function.Surjective.{u_4 + 1, u_5 + 1} (α := S) (β := T) (⇑(algebraMap S T) : (a : S) → T)
r : S
hr : IsUnit.{u_5} (M := T) ((algebraMap S T : (a : S) → T) r : T)
n : ℕ
hn : HSMul.hSMul (β := Ideal S) (r ^ n) (RingHom.ker (F := S →+* T) (algebraMap S T)) ≤ ⊥
⊢ Away r T
have refine_1 : ∀ (t : T),
  ∃ (n : ℕ) (a : S), t * HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) r : T) n = (algebraMap S T : (a : S) → T) a
Tactic: refine .mk _ hr (fun t ↦ ?_) fun x y h ↦ ⟨n, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
S : Type u_4
T : Type u_5
inst : CommRing S
inst_1 : CommRing T
inst_2 : Algebra S T
h₁ : Function.Surjective.{u_4 + 1, u_5 + 1} (α := S) (β := T) (⇑(algebraMap S T) : (a : S) → T)
r : S
hr : IsUnit.{u_5} (M := T) ((algebraMap S T : (a : S) → T) r : T)
n : ℕ
hn : HSMul.hSMul (β := Ideal S) (r ^ n) (RingHom.ker (F := S →+* T) (algebraMap S T)) ≤ ⊥
refine_1 :
  ∀ (t : T),
    ∃ (n : ℕ) (a : S),
      t * HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) r : T) n = (algebraMap S T : (a : S) → T) a
⊢ Away r T
have refine_2 : ∀ (x y : S) (h : Eq.{u_5 + 1} (α := T) ((algebraMap S T : (a : S) → T) x : T) ((algebraMap S T : (a : S) → T) y : T)),
  r ^ n * x = r ^ n * y
Tactic: refine .mk _ hr (fun t ↦ ?_) fun x y h ↦ ⟨n, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
S : Type u_4
T : Type u_5
inst : CommRing S
inst_1 : CommRing T
inst_2 : Algebra S T
h₁ : Function.Surjective.{u_4 + 1, u_5 + 1} (α := S) (β := T) (⇑(algebraMap S T) : (a : S) → T)
r : S
hr : IsUnit.{u_5} (M := T) ((algebraMap S T : (a : S) → T) r : T)
n : ℕ
hn : HSMul.hSMul (β := Ideal S) (r ^ n) (RingHom.ker (F := S →+* T) (algebraMap S T)) ≤ ⊥
t : T
⊢ ∃ (n : ℕ) (a : S), t * HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) r : T) n = (algebraMap S T : (a : S) → T) a
have refine_1 : ∀ (s : S),
  ∃ (n : ℕ) (a : S),
    HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) s : T)
        (HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) r : T) n) =
      (algebraMap S T : (a : S) → T) a
Tactic: obtain ⟨s, rfl⟩ := h₁ t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
S : Type u_4
T : Type u_5
inst : CommRing S
inst_1 : CommRing T
inst_2 : Algebra S T
h₁ : Function.Surjective.{u_4 + 1, u_5 + 1} (α := S) (β := T) (⇑(algebraMap S T) : (a : S) → T)
r : S
hr : IsUnit.{u_5} (M := T) ((algebraMap S T : (a : S) → T) r : T)
n : ℕ
hn : HSMul.hSMul (β := Ideal S) (r ^ n) (RingHom.ker (F := S →+* T) (algebraMap S T)) ≤ ⊥
x y : S
h : Eq.{u_5 + 1} (α := T) ((algebraMap S T : (a : S) → T) x : T) ((algebraMap S T : (a : S) → T) y : T)
⊢ r ^ n * x = r ^ n * y
have refine_2 : r ^ n * (x - y) = 0
Tactic: rw [← sub_eq_zero, ← mul_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
S : Type u_4
T : Type u_5
inst : CommRing S
inst_1 : CommRing T
inst_2 : Algebra S T
R : Type u_6
inst_3 : CommRing R
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
h₁ : Function.Surjective.{u_4 + 1, u_5 + 1} (α := S) (β := T) (⇑(algebraMap S T) : (a : S) → T)
h₂ : Function.Surjective.{u_6 + 1, u_4 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
r : R
hr : IsUnit.{u_5} (M := T) ((algebraMap R T : (a : R) → T) r : T)
n : ℕ
hn :
  HSMul.hSMul (β := Ideal R) (r ^ n) (RingHom.ker (F := R →+* T) (algebraMap R T)) ≤
    RingHom.ker (F := R →+* S) (algebraMap R S)
⊢ Away.{u_4, u_5} (R := S) ((algebraMap R S : (a : R) → S) r : S) T
have refine_1 : IsUnit.{u_5} (M := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) r : S) : T)
Tactic: refine Away.of_surjective h₁ ?_ n ?_
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
S : Type u_4
T : Type u_5
inst : CommRing S
inst_1 : CommRing T
inst_2 : Algebra S T
R : Type u_6
inst_3 : CommRing R
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
h₁ : Function.Surjective.{u_4 + 1, u_5 + 1} (α := S) (β := T) (⇑(algebraMap S T) : (a : S) → T)
h₂ : Function.Surjective.{u_6 + 1, u_4 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
r : R
hr : IsUnit.{u_5} (M := T) ((algebraMap R T : (a : R) → T) r : T)
n : ℕ
hn :
  HSMul.hSMul (β := Ideal R) (r ^ n) (RingHom.ker (F := R →+* T) (algebraMap R T)) ≤
    RingHom.ker (F := R →+* S) (algebraMap R S)
refine_1 : IsUnit.{u_5} (M := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) r : S) : T)
⊢ Away.{u_4, u_5} (R := S) ((algebraMap R S : (a : R) → S) r : S) T
have refine_2 : HSMul.hSMul (β := Ideal S) (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n)
    (RingHom.ker (F := S →+* T) (algebraMap S T)) ≤
  ⊥
Tactic: refine Away.of_surjective h₁ ?_ n ?_
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
S : Type u_4
T : Type u_5
inst : CommRing S
inst_1 : CommRing T
inst_2 : Algebra S T
R : Type u_6
inst_3 : CommRing R
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
h₁ : Function.Surjective.{u_4 + 1, u_5 + 1} (α := S) (β := T) (⇑(algebraMap S T) : (a : S) → T)
h₂ : Function.Surjective.{u_6 + 1, u_4 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
r : R
hr : IsUnit.{u_5} (M := T) ((algebraMap R T : (a : R) → T) r : T)
n : ℕ
hn :
  HSMul.hSMul (β := Ideal R) (r ^ n) (RingHom.ker (F := R →+* T) (algebraMap R T)) ≤
    RingHom.ker (F := R →+* S) (algebraMap R S)
⊢ HSMul.hSMul (β := Ideal S) (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n)
      (RingHom.ker (F := S →+* T) (algebraMap S T)) ≤
    ⊥
have refine_2 : LE.le.{u_4} (α := Ideal S)
  (Ideal.map (F := R →+* S) (algebraMap R S)
    (HSMul.hSMul (β := Ideal R) (r ^ n) (RingHom.ker (F := R →+* T) (algebraMap R T))))
  ⊥
Tactic: rw [← (RingHom.ker (algebraMap S T)).map_comap_of_surjective _ h₂, ← map_pow,
      ← Ideal.map_pointwise_smul, RingHom.comap_ker, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
S : Type u_4
T : Type u_5
inst : CommRing S
inst_1 : CommRing T
inst_2 : Algebra S T
R : Type u_6
inst_3 : CommRing R
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
h₁ : Function.Surjective.{u_4 + 1, u_5 + 1} (α := S) (β := T) (⇑(algebraMap S T) : (a : S) → T)
h₂ : Function.Surjective.{u_6 + 1, u_4 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
r : R
hr : IsUnit.{u_5} (M := T) ((algebraMap R T : (a : R) → T) r : T)
n : ℕ
hn :
  HSMul.hSMul (β := Ideal R) (r ^ n) (RingHom.ker (F := R →+* T) (algebraMap R T)) ≤
    RingHom.ker (F := R →+* S) (algebraMap R S)
⊢ LE.le.{u_4} (α := Ideal S)
    (Ideal.map (F := R →+* S) (algebraMap R S)
      (HSMul.hSMul (β := Ideal R) (r ^ n) (RingHom.ker (F := R →+* T) (algebraMap R T))))
    ⊥
have refine_2 : ∀
  (hn :
    HSMul.hSMul (β := Ideal R) (r ^ n) (RingHom.ker (F := R →+* T) (algebraMap R T)) ≤
      Ideal.comap (F := R →+* S) (algebraMap R S) ⊥),
  LE.le.{u_4} (α := Ideal S)
    (Ideal.map (F := R →+* S) (algebraMap R S)
      (HSMul.hSMul (β := Ideal R) (r ^ n) (RingHom.ker (F := R →+* T) (algebraMap R T))))
    ⊥
Tactic: rwa [RingHom.ker_eq_comap_bot (algebraMap R S), ← Ideal.map_le_iff_le_comap] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
S : Type u_4
T : Type u_5
inst : CommRing S
inst_1 : CommRing T
inst_2 : Algebra S T
R : Type u_6
inst_3 : CommRing R
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
h₁ : Function.Surjective.{u_4 + 1, u_5 + 1} (α := S) (β := T) (⇑(algebraMap S T) : (a : S) → T)
h₂ : Function.Surjective.{u_6 + 1, u_4 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
r : R
hr : IsUnit.{u_5} (M := T) ((algebraMap R T : (a : R) → T) r : T)
n : ℕ
hn :
  HSMul.hSMul (β := Ideal R) (r ^ n) (RingHom.ker (F := R →+* T) (algebraMap R T)) ≤
    RingHom.ker (F := R →+* S) (algebraMap R S)
refine_2 :
  ∀
    (hn :
      HSMul.hSMul (β := Ideal R) (r ^ n) (RingHom.ker (F := R →+* T) (algebraMap R T)) ≤
        Ideal.comap (F := R →+* S) (algebraMap R S) ⊥),
    LE.le.{u_4} (α := Ideal S)
      (Ideal.map (F := R →+* S) (algebraMap R S)
        (HSMul.hSMul (β := Ideal R) (r ^ n) (RingHom.ker (F := R →+* T) (algebraMap R T))))
      ⊥
⊢ LE.le.{u_4} (α := Ideal S)
    (Ideal.map (F := R →+* S) (algebraMap R S)
      (HSMul.hSMul (β := Ideal R) (r ^ n) (RingHom.ker (F := R →+* T) (algebraMap R T))))
    ⊥
have refine_2₁ : ∀
  (hn :
    LE.le.{u_4} (α := Ideal S)
      (Ideal.map (F := R →+* S) (algebraMap R S)
        (HSMul.hSMul (β := Ideal R) (r ^ n) (RingHom.ker (F := R →+* T) (algebraMap R T))))
      ⊥),
  LE.le.{u_4} (α := Ideal S)
    (Ideal.map (F := R →+* S) (algebraMap R S)
      (HSMul.hSMul (β := Ideal R) (r ^ n) (RingHom.ker (F := R →+* T) (algebraMap R T))))
    ⊥
Tactic: rwa [RingHom.ker_eq_comap_bot (algebraMap R S), ← Ideal.map_le_iff_le_comap] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
S : Type u_2
inst : CommSemiring S
R : Type u_4
inst_1 : CommRing R
f : R →+* S
a b : R
h : a ∣ b
H :
  Function.Injective.{u_4 + 1, u_2 + 1} (α := Away a) (β := Away (M := S) ((f : (a : R) → S) a : S))
    (⇑(awayMap f a) : (a_1 : Away a) → Away ((f : (a : R) → S) a))
⊢ Function.Injective.{u_4 + 1, u_2 + 1} (α := Away b) (β := Away (M := S) ((f : (a : R) → S) b : S))
    (⇑(awayMap f b) : (a : Away b) → Away ((f : (a : R) → S) b))
have simp : ∀ (H : ∀ (a_1 : R), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a_1 : S) (0 : S) → ∃ (n : ℕ), a ^ n * a_1 = 0) (a : R),
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S) → ∃ (n : ℕ), b ^ n * a = 0
Tactic: simp only [awayMap_injective_iff] at H ⊢
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
S : Type u_2
inst : CommSemiring S
R : Type u_4
inst_1 : CommRing R
f : R →+* S
a b : R
h : a ∣ b
H : ∀ (a_1 : R), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a_1 : S) (0 : S) → ∃ (n : ℕ), a ^ n * a_1 = 0
⊢ ∀ (a : R), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a : S) (0 : S) → ∃ (n : ℕ), b ^ n * a = 0
have obtain : ∀ (b a_1 : R), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a_1 : S) (0 : S) → ∃ (n : ℕ), (a * b) ^ n * a_1 = 0
Tactic: obtain ⟨b, rfl⟩ := h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
S : Type u_2
inst : CommSemiring S
R : Type u_4
inst_1 : CommRing R
f : R →+* S
a : R
H : ∀ (a_1 : R), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) a_1 : S) (0 : S) → ∃ (n : ℕ), a ^ n * a_1 = 0
b x : R
hx : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S)
⊢ ∃ (n : ℕ), (a * b) ^ n * x = 0
have obtain : ∀ (n : ℕ) (hn : a ^ n * x = 0), ∃ (n : ℕ), (a * b) ^ n * x = 0
Tactic: obtain ⟨n, hn⟩ := H x hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
a b : R
h : a ∣ b
H :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := Away a) (β := Away (M := S) ((f : (a : R) → S) a : S))
    (⇑(awayMap f a) : (a_1 : Away a) → Away ((f : (a : R) → S) a))
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := Away b) (β := Away (M := S) ((f : (a : R) → S) b : S))
    (⇑(awayMap f b) : (a : Away b) → Away ((f : (a : R) → S) b))
have simp : ∀ (H : ∀ (a_1 : S), ∃ (b : R) (m : ℕ), (f : (a : R) → S) b = HPow.hPow (α := S) ((f : (a : R) → S) a : S) m * a_1)
  (a : S), ∃ (b_1 : R) (m : ℕ), (f : (a : R) → S) b_1 = HPow.hPow (α := S) ((f : (a : R) → S) b : S) m * a
Tactic: simp only [awayMap_surjective_iff] at H ⊢
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
a b : R
h : a ∣ b
H : ∀ (a_1 : S), ∃ (b : R) (m : ℕ), (f : (a : R) → S) b = HPow.hPow (α := S) ((f : (a : R) → S) a : S) m * a_1
⊢ ∀ (a : S), ∃ (b_1 : R) (m : ℕ), (f : (a : R) → S) b_1 = HPow.hPow (α := S) ((f : (a : R) → S) b : S) m * a
have obtain : ∀ (b : R) (a_1 : S),
  ∃ (b_1 : R) (m : ℕ), (f : (a : R) → S) b_1 = HPow.hPow (α := S) ((f : (a : R) → S) (a * b) : S) m * a_1
Tactic: obtain ⟨b, rfl⟩ := h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
a : R
H : ∀ (a_1 : S), ∃ (b : R) (m : ℕ), (f : (a : R) → S) b = HPow.hPow (α := S) ((f : (a : R) → S) a : S) m * a_1
b : R
x : S
⊢ ∃ (b_1 : R) (m : ℕ), (f : (a : R) → S) b_1 = HPow.hPow (α := S) ((f : (a : R) → S) (a * b) : S) m * x
have obtain : ∀ (c : R) (m : ℕ) (e : (f : (a : R) → S) c = HPow.hPow (α := S) ((f : (a : R) → S) a : S) m * x),
  ∃ (b_1 : R) (m : ℕ), (f : (a : R) → S) b_1 = HPow.hPow (α := S) ((f : (a : R) → S) (a * b) : S) m * x
Tactic: obtain ⟨c, m, e⟩ := H x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
a b : R
H :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := Away (a * b)) (β := Away (M := S) ((f : (a : R) → S) (a * b) : S))
    (⇑(awayMap f (a * b)) : (a_1 : Away (a * b)) → Away ((f : (a : R) → S) (a * b)))
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α :=
    Away (M := Away a) ((algebraMap R (Away a) : (a_1 : R) → Away a) b : Away a)) (β :=
    Away (M := Away (M := S) ((f : (a : R) → S) a : S))
      ((awayMap f a : (a_1 : Away a) → Away ((f : (a : R) → S) a)) ((algebraMap R (Away a) : (a_1 : R) → Away a) b) :
        Away (M := S) ((f : (a : R) → S) a : S)))
    (⇑(awayMap (awayMap f a) ((algebraMap R (Away a) : (a_1 : R) → Away a) b)) :
      (a_1 : Away ((algebraMap R (Away a) : (a_1 : R) → Away a) b)) →
        Away
          ((awayMap f a : (a_2 : Away a) → Away ((f : (a : R) → S) a))
            ((algebraMap R (Away a) : (a_2 : R) → Away a) b)))
have rw : ∀
  (H :
    ∀ (a_1 : S),
      ∃ (b_1 : R) (m : ℕ), (f : (a : R) → S) b_1 = HPow.hPow (α := S) ((f : (a : R) → S) (a * b) : S) m * a_1)
  (a_1 : Away (M := S) ((f : (a : R) → S) a : S)),
  ∃ (b_1 : Away a) (m : ℕ),
    (awayMap f a : (a_2 : Away a) → Away ((f : (a : R) → S) a)) b_1 =
      HPow.hPow (α := Away (M := S) ((f : (a : R) → S) a : S))
          ((awayMap f a : (a_2 : Away a) → Away ((f : (a : R) → S) a))
              ((algebraMap R (Away a) : (a_2 : R) → Away a) b) :
            Away (M := S) ((f : (a : R) → S) a : S))
          m *
        a_1
Tactic: rw [awayMap_surjective_iff] at H ⊢
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
a b : R
H : ∀ (a_1 : S), ∃ (b_1 : R) (m : ℕ), (f : (a : R) → S) b_1 = HPow.hPow (α := S) ((f : (a : R) → S) (a * b) : S) m * a_1
⊢ ∀ (a_1 : Away (M := S) ((f : (a : R) → S) a : S)),
    ∃ (b_1 : Away a) (m : ℕ),
      (awayMap f a : (a_2 : Away a) → Away ((f : (a : R) → S) a)) b_1 =
        HPow.hPow (α := Away (M := S) ((f : (a : R) → S) a : S))
            ((awayMap f a : (a_2 : Away a) → Away ((f : (a : R) → S) a))
                ((algebraMap R (Away a) : (a_2 : R) → Away a) b) :
              Away (M := S) ((f : (a : R) → S) a : S))
            m *
          a_1
have suffices : ∀ (s : S) (n : ℕ),
  ∃ (c : R) (l : ℕ) (m : ℕ) (k : ℕ),
    (f : (a : R) → S) (a ^ (k + n) * c) = HMul.hMul (α := S) ((f : (a : R) → S) (a ^ (k + l) * b ^ m) : S) s
Tactic: suffices ∀ (s : S) (n : ℕ), ∃ c l m k, f (a ^ (k + n) * c) =
      f (a ^ (k + l) * b ^ m) * s by
    simpa [Function.Surjective, (IsLocalization.mk'_surjective (.powers (f a))).forall, ← map_pow,
      (IsLocalization.mk'_surjective (.powers a)).exists, Submonoid.mem_powers_iff, pow_add,
      Localization.awayMap, IsLocalization.Away.map, IsLocalization.map_mk', ← mul_assoc,
      IsLocalization.mk'_eq_iff_eq, ← map_mul, IsLocalization.eq_iff_exists (.powers (f a)),
      IsLocalization.mul_mk'_eq_mk'_of_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
a b : R
H : ∀ (a_1 : S), ∃ (b_1 : R) (m : ℕ), (f : (a : R) → S) b_1 = HPow.hPow (α := S) ((f : (a : R) → S) (a * b) : S) m * a_1
s : S
n : ℕ
⊢ ∃ (c : R) (l : ℕ) (m : ℕ) (k : ℕ),
    (f : (a : R) → S) (a ^ (k + n) * c) = HMul.hMul (α := S) ((f : (a : R) → S) (a ^ (k + l) * b ^ m) : S) s
have obtain : ∀ (c : R) (m : ℕ) (e : (f : (a : R) → S) c = HPow.hPow (α := S) ((f : (a : R) → S) (a * b) : S) m * s),
  ∃ (c : R) (l : ℕ) (m : ℕ) (k : ℕ),
    (f : (a : R) → S) (a ^ (k + n) * c) = HMul.hMul (α := S) ((f : (a : R) → S) (a ^ (k + l) * b ^ m) : S) s
Tactic: obtain ⟨c, m, e⟩ := H s
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
f : R →+* S
a b : R
H : ∀ (a_1 : S), ∃ (b_1 : R) (m : ℕ), (f : (a : R) → S) b_1 = HPow.hPow (α := S) ((f : (a : R) → S) (a * b) : S) m * a_1
s : S
n : ℕ
c : R
m : ℕ
e : (f : (a : R) → S) c = HPow.hPow (α := S) ((f : (a : R) → S) (a * b) : S) m * s
⊢ (f : (a : R) → S) (a ^ (0 + n) * c) = HMul.hMul (α := S) ((f : (a : R) → S) (a ^ (0 + (n + m)) * b ^ m) : S) s
have simp : HPow.hPow (α := S) ((f : (a : R) → S) a : S) n *
    (HMul.hMul (α := S) (β := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) b : S) ^ m * s) =
  HPow.hPow (α := S) ((f : (a : R) → S) a : S) n * HPow.hPow (α := S) ((f : (a : R) → S) a : S) m *
      HPow.hPow (α := S) ((f : (a : R) → S) b : S) m *
    s
Tactic: simp [e, pow_add]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
span_eq : Eq (α := Ideal R) (Ideal.span s) ⊤
x y : R
eq :
  Eq (α := (a : (↑s : Type u_1)) → Away (↑a : R))
    ((algebraMap R ((a : (↑s : Type u_1)) → Away (↑a : R)) : (a : R) → (a : (↑s : Type u_1)) → Away (↑a : R)) x :
      (a : (↑s : Type u_1)) → Away (↑a : R))
    ((algebraMap R ((a : (↑s : Type u_1)) → Away (↑a : R)) : (a : R) → (a : (↑s : Type u_1)) → Away (↑a : R)) y :
      (a : (↑s : Type u_1)) → Away (↑a : R))
⊢ x = y
have suffices : Eq (α := Ideal R) (Module.eqIdeal R x y) ⊤
Tactic: suffices Module.eqIdeal R x y = ⊤ by simpa [Module.eqIdeal] using (Ideal.eq_top_iff_one _).mp this
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
span_eq : Eq (α := Ideal R) (Ideal.span s) ⊤
x y : R
eq :
  Eq (α := (a : (↑s : Type u_1)) → Away (↑a : R))
    ((algebraMap R ((a : (↑s : Type u_1)) → Away (↑a : R)) : (a : R) → (a : (↑s : Type u_1)) → Away (↑a : R)) x :
      (a : (↑s : Type u_1)) → Away (↑a : R))
    ((algebraMap R ((a : (↑s : Type u_1)) → Away (↑a : R)) : (a : R) → (a : (↑s : Type u_1)) → Away (↑a : R)) y :
      (a : (↑s : Type u_1)) → Away (↑a : R))
⊢ Eq (α := Ideal R) (Module.eqIdeal R x y) ⊤
have by_contra : ∀ (ne : ¬Eq (α := Ideal R) (Module.eqIdeal R x y) ⊤), False
Tactic: by_contra ne
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
s : Set R
span_eq : Eq (α := Ideal R) (Ideal.span s) ⊤
x y : R
eq :
  Eq (α := (a : (↑s : Type u_1)) → Away (↑a : R))
    ((algebraMap R ((a : (↑s : Type u_1)) → Away (↑a : R)) : (a : R) → (a : (↑s : Type u_1)) → Away (↑a : R)) x :
      (a : (↑s : Type u_1)) → Away (↑a : R))
    ((algebraMap R ((a : (↑s : Type u_1)) → Away (↑a : R)) : (a : R) → (a : (↑s : Type u_1)) → Away (↑a : R)) y :
      (a : (↑s : Type u_1)) → Away (↑a : R))
ne : ¬Eq (α := Ideal R) (Module.eqIdeal R x y) ⊤
⊢ False
have have : ∀ (r : R) (hrs : r ∈ s) (disj : Disjoint (↑(Module.eqIdeal R x y) : Set R) (↑(Submonoid.powers r) : Set R)), False
Tactic: have ⟨r, hrs, disj⟩ := Ideal.exists_disjoint_powers_of_span_eq_top s span_eq _ ne