awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_2 : Algebra R S
r : R
inst_3 : Away r S
u : Rˣ
a b : R
hab : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b : S)
n : ℕ
hn : r ^ n * a = r ^ n * b
h : r ^ n * (↑u : R) ^ n * a = r ^ n * (↑u : R) ^ n * b
h₁ : (↑u : R) ^ n * r ^ n * a = (↑u : R) ^ n * r ^ n * b
⊢ (r * (↑u : R)) ^ n * a = (r * (↑u : R)) ^ n * b
have h₂ : (↑u : R) ^ n * (r ^ n * a) = (↑u : R) ^ n * r ^ n * b
Tactic: rw [mul_pow, mul_comm (r ^ n), mul_assoc, mul_assoc, hn]
-- 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
inst_2 : Algebra R S
r : R
inst_3 : Away r S
u : Rˣ
a b : R
hab : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b : S)
n : ℕ
hn : r ^ n * a = r ^ n * b
h : r ^ n * (↑u : R) ^ n * a = r ^ n * (↑u : R) ^ n * b
h₁ : (↑u : R) ^ n * r ^ n * a = (↑u : R) ^ n * r ^ n * b
h₂ : (↑u : R) ^ n * (r ^ n * a) = (↑u : R) ^ n * r ^ n * b
⊢ (r * (↑u : R)) ^ n * a = (r * (↑u : R)) ^ n * b
have h₃ : (↑u : R) ^ n * (r ^ n * a) = (↑u : R) ^ n * (r ^ n * b)
Tactic: rw [mul_pow, mul_comm (r ^ n), mul_assoc, mul_assoc, hn]
-- 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
inst_2 : Algebra R S
r : R
inst_3 : Away r S
u : Rˣ
a b : R
hab : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) b : S)
n : ℕ
hn : r ^ n * a = r ^ n * b
h : r ^ n * (↑u : R) ^ n * a = r ^ n * (↑u : R) ^ n * b
h₁ : (↑u : R) ^ n * r ^ n * a = (↑u : R) ^ n * r ^ n * b
h₂ : (↑u : R) ^ n * (r ^ n * a) = (↑u : R) ^ n * r ^ n * b
h₃ : (↑u : R) ^ n * (r ^ n * a) = (↑u : R) ^ n * (r ^ n * b)
⊢ (r * (↑u : R)) ^ n * a = (r * (↑u : R)) ^ n * b
have h₄ : (↑u : R) ^ n * (r ^ n * b) = (↑u : R) ^ n * (r ^ n * b)
Tactic: rw [mul_pow, mul_comm (r ^ n), mul_assoc, mul_assoc, hn]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (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
P : Type u_3
inst_3 : CommSemiring P
x : R
inst_4 : Away x S
g : R →+* P
hg : IsUnit.{u_3} (M := P) ((g : (a : R) → P) x : P)
y : ↥(Submonoid.powers x)
⊢ IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
have obtain : ∀ (n : ℕ) (hn : (fun (x_1 : ℕ) ↦ x ^ x_1) n = (↑y : R)), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
Tactic: obtain ⟨n, hn⟩ := y.2
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (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
P : Type u_3
inst_3 : CommSemiring P
x : R
inst_4 : Away x S
g : R →+* P
hg : IsUnit.{u_3} (M := P) ((g : (a : R) → P) x : P)
y : ↥(Submonoid.powers x)
n : ℕ
hn : (fun (x_1 : ℕ) ↦ x ^ x_1) n = (↑y : R)
⊢ IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
have rw : IsUnit (HPow.hPow (α := P) ((g : (a : R) → P) x : P) n)
Tactic: rw [← hn, g.map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (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
P : Type u_3
inst_3 : CommSemiring P
x : R
inst_4 : Away x S
g : R →+* P
Q : Type u_4
inst_5 : CommSemiring Q
inst_6 : Algebra P Q
f : R →+* P
r : R
inst_7 : Away r S
inst_8 : Away.{u_3, u_4} (R := P) ((f : (a : R) → P) r : P) Q
n : ℕ
⊢ Membership.mem (γ := Submonoid R) (Submonoid.comap (N := P) f (Submonoid.powers ((f : (a : R) → P) r) : Submonoid P))
    ((fun (x : ℕ) ↦ r ^ x) n)
have h : Eq.{u_3 + 1} (α := P) ((fun (x : ℕ) ↦ HPow.hPow (α := P) ((f : (a : R) → P) r : P) x) n : P)
  ((f : (a : R) → P) ((fun (x : ℕ) ↦ r ^ x) n) : P)
Tactic: use n
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
P : Type u_3
inst_1 : CommSemiring P
Q : Type u_4
inst_2 : CommSemiring Q
inst_3 : Algebra P Q
S : Type u_5
inst_4 : CommRing S
inst_5 : Algebra R S
f : R →+* P
r : R
inst_6 : Away r S
inst_7 : Away.{u_3, u_4} (R := P) ((f : (a : R) → P) r : P) Q
⊢ Function.Injective.{u_5 + 1, u_4 + 1} (α := S) (β := Q) (⇑(map S Q f r) : (a : S) → Q) ↔
    ∀ (a : R), Eq.{u_3 + 1} (α := P) ((f : (a : R) → P) a : P) (0 : P) → ∃ (n : ℕ), r ^ n * a = 0
have rw : (∀ (a : S), Eq.{u_4 + 1} (α := Q) ((map S Q f r : (a : S) → Q) a : Q) (0 : Q) → a = 0) ↔
  ∀ (a : R), Eq.{u_3 + 1} (α := P) ((f : (a : R) → P) a : P) (0 : P) → ∃ (n : ℕ), r ^ n * a = 0
Tactic: rw [injective_iff_map_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
P : Type u_3
inst_1 : CommSemiring P
Q : Type u_4
inst_2 : CommSemiring Q
inst_3 : Algebra P Q
S : Type u_5
inst_4 : CommRing S
inst_5 : Algebra R S
f : R →+* P
r : R
inst_6 : Away r S
inst_7 : Away.{u_3, u_4} (R := P) ((f : (a : R) → P) r : P) Q
⊢ (∀ (a : S), Eq.{u_4 + 1} (α := Q) ((map S Q f r : (a : S) → Q) a : Q) (0 : Q) → a = 0) ↔
    ∀ (a : R), Eq.{u_3 + 1} (α := P) ((f : (a : R) → P) a : P) (0 : P) → ∃ (n : ℕ), r ^ n * a = 0
have trans : (∀ (a : S), Eq.{u_4 + 1} (α := Q) ((map S Q f r : (a : S) → Q) a : Q) (0 : Q) → a = 0) ↔
  ∀ (a : R) (n : ℕ),
    HMul.hMul (β := P) (HPow.hPow (α := P) ((f : (a : R) → P) r : P) n) ((f : (a : R) → P) a : P) = 0 →
      ∃ (m : ℕ), r ^ m * a = 0
Tactic: trans ∀ a n, f r ^ n * f a = 0 → ∃ m, r ^ m * a = 0
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
P : Type u_3
inst_1 : CommSemiring P
Q : Type u_4
inst_2 : CommSemiring Q
inst_3 : Algebra P Q
S : Type u_5
inst_4 : CommRing S
inst_5 : Algebra R S
f : R →+* P
r : R
inst_6 : Away r S
inst_7 : Away.{u_3, u_4} (R := P) ((f : (a : R) → P) r : P) Q
trans :
  (∀ (a : S), Eq.{u_4 + 1} (α := Q) ((map S Q f r : (a : S) → Q) a : Q) (0 : Q) → a = 0) ↔
    ∀ (a : R) (n : ℕ),
      HMul.hMul (β := P) (HPow.hPow (α := P) ((f : (a : R) → P) r : P) n) ((f : (a : R) → P) a : P) = 0 →
        ∃ (m : ℕ), r ^ m * a = 0
⊢ (∀ (a : S), Eq.{u_4 + 1} (α := Q) ((map S Q f r : (a : S) → Q) a : Q) (0 : Q) → a = 0) ↔
    ∀ (a : R), Eq.{u_3 + 1} (α := P) ((f : (a : R) → P) a : P) (0 : P) → ∃ (n : ℕ), r ^ n * a = 0
have trans₁ : (∀ (a : R) (n : ℕ),
    HMul.hMul (β := P) (HPow.hPow (α := P) ((f : (a : R) → P) r : P) n) ((f : (a : R) → P) a : P) = 0 →
      ∃ (m : ℕ), r ^ m * a = 0) ↔
  ∀ (a : R), Eq.{u_3 + 1} (α := P) ((f : (a : R) → P) a : P) (0 : P) → ∃ (n : ℕ), r ^ n * a = 0
Tactic: trans ∀ a n, f r ^ n * f a = 0 → ∃ m, r ^ m * a = 0
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
P : Type u_3
inst_1 : CommSemiring P
Q : Type u_4
inst_2 : CommSemiring Q
inst_3 : Algebra P Q
S : Type u_5
inst_4 : CommRing S
inst_5 : Algebra R S
f : R →+* P
r : R
inst_6 : Away r S
inst_7 : Away.{u_3, u_4} (R := P) ((f : (a : R) → P) r : P) Q
⊢ (∀ (a : R) (n : ℕ),
      HMul.hMul (β := P) (HPow.hPow (α := P) ((f : (a : R) → P) r : P) n) ((f : (a : R) → P) a : P) = 0 →
        ∃ (m : ℕ), r ^ m * a = 0) ↔
    ∀ (a : R), Eq.{u_3 + 1} (α := P) ((f : (a : R) → P) a : P) (0 : P) → ∃ (n : ℕ), r ^ n * a = 0
have refine : ∀ (H : ∀ (a : R), Eq.{u_3 + 1} (α := P) ((f : (a : R) → P) a : P) (0 : P) → ∃ (n : ℕ), r ^ n * a = 0) (a : R) (n : ℕ)
  (ha : HMul.hMul (β := P) (HPow.hPow (α := P) ((f : (a : R) → P) r : P) n) ((f : (a : R) → P) a : P) = 0),
  ∃ (m : ℕ), r ^ m * a = 0
Tactic: refine ⟨fun H x hx ↦ H x 0 (by simpa), fun H a n ha ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
P : Type u_3
inst_1 : CommSemiring P
Q : Type u_4
inst_2 : CommSemiring Q
inst_3 : Algebra P Q
S : Type u_5
inst_4 : CommRing S
inst_5 : Algebra R S
f : R →+* P
r : R
inst_6 : Away r S
inst_7 : Away.{u_3, u_4} (R := P) ((f : (a : R) → P) r : P) Q
H : ∀ (a : R), Eq.{u_3 + 1} (α := P) ((f : (a : R) → P) a : P) (0 : P) → ∃ (n : ℕ), r ^ n * a = 0
a : R
n : ℕ
ha : HMul.hMul (β := P) (HPow.hPow (α := P) ((f : (a : R) → P) r : P) n) ((f : (a : R) → P) a : P) = 0
⊢ ∃ (m : ℕ), r ^ m * a = 0
have obtain : ∀ (m : ℕ) (hm : r ^ m * (r ^ n * a) = 0), ∃ (m : ℕ), r ^ m * a = 0
Tactic: obtain ⟨m, hm⟩ := H (r ^ n * a) (by simpa)
-- 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
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
Q : Type u_4
inst_4 : CommSemiring Q
inst_5 : Algebra P Q
f : R →+* P
r : R
inst_6 : Away r S
inst_7 : Away.{u_3, u_4} (R := P) ((f : (a : R) → P) r : P) Q
⊢ Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := Q) (⇑(map S Q f r) : (a : S) → Q) ↔
    ∀ (a : P), ∃ (b : R) (m : ℕ), (f : (a : R) → P) b = HPow.hPow (α := P) ((f : (a : R) → P) r : P) m * a
have trans : Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := Q) (⇑(map S Q f r) : (a : S) → Q) ↔
  ∀ (a : P) (n : ℕ),
    ∃ (b : R) (m : ℕ) (k : ℕ),
      (f : (a : R) → P) (r ^ (k + n) * b) = HPow.hPow (α := P) ((f : (a : R) → P) r : P) (k + m) * a
Tactic: trans ∀ a n, ∃ b m k, f (r ^ (k + n) * b) = f r ^ (k + m) * a
-- 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
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
Q : Type u_4
inst_4 : CommSemiring Q
inst_5 : Algebra P Q
f : R →+* P
r : R
inst_6 : Away r S
inst_7 : Away.{u_3, u_4} (R := P) ((f : (a : R) → P) r : P) Q
trans :
  Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := Q) (⇑(map S Q f r) : (a : S) → Q) ↔
    ∀ (a : P) (n : ℕ),
      ∃ (b : R) (m : ℕ) (k : ℕ),
        (f : (a : R) → P) (r ^ (k + n) * b) = HPow.hPow (α := P) ((f : (a : R) → P) r : P) (k + m) * a
⊢ Function.Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := Q) (⇑(map S Q f r) : (a : S) → Q) ↔
    ∀ (a : P), ∃ (b : R) (m : ℕ), (f : (a : R) → P) b = HPow.hPow (α := P) ((f : (a : R) → P) r : P) m * a
have trans₁ : (∀ (a : P) (n : ℕ),
    ∃ (b : R) (m : ℕ) (k : ℕ),
      (f : (a : R) → P) (r ^ (k + n) * b) = HPow.hPow (α := P) ((f : (a : R) → P) r : P) (k + m) * a) ↔
  ∀ (a : P), ∃ (b : R) (m : ℕ), (f : (a : R) → P) b = HPow.hPow (α := P) ((f : (a : R) → P) r : P) m * a
Tactic: trans ∀ a n, ∃ b m k, f (r ^ (k + n) * b) = f r ^ (k + m) * a
-- 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
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
Q : Type u_4
inst_4 : CommSemiring Q
inst_5 : Algebra P Q
f : R →+* P
r : R
inst_6 : Away r S
inst_7 : Away.{u_3, u_4} (R := P) ((f : (a : R) → P) r : P) Q
⊢ (∀ (a : P) (n : ℕ),
      ∃ (b : R) (m : ℕ) (k : ℕ),
        (f : (a : R) → P) (r ^ (k + n) * b) = HPow.hPow (α := P) ((f : (a : R) → P) r : P) (k + m) * a) ↔
    ∀ (a : P), ∃ (b : R) (m : ℕ), (f : (a : R) → P) b = HPow.hPow (α := P) ((f : (a : R) → P) r : P) m * a
have refine : ∀ (H : ∀ (a : P), ∃ (b : R) (m : ℕ), (f : (a : R) → P) b = HPow.hPow (α := P) ((f : (a : R) → P) r : P) m * a) (a : P)
  (n : ℕ),
  ∃ (b : R) (m : ℕ) (k : ℕ),
    (f : (a : R) → P) (r ^ (k + n) * b) = HPow.hPow (α := P) ((f : (a : R) → P) r : P) (k + m) * a
Tactic: refine ⟨fun H x ↦ ⟨_, _, (H x 0).choose_spec.choose_spec.choose_spec⟩, fun H a n ↦ ?_⟩
-- 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
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
Q : Type u_4
inst_4 : CommSemiring Q
inst_5 : Algebra P Q
f : R →+* P
r : R
inst_6 : Away r S
inst_7 : Away.{u_3, u_4} (R := P) ((f : (a : R) → P) r : P) Q
H : ∀ (a : P), ∃ (b : R) (m : ℕ), (f : (a : R) → P) b = HPow.hPow (α := P) ((f : (a : R) → P) r : P) m * a
a : P
n : ℕ
⊢ ∃ (b : R) (m : ℕ) (k : ℕ),
    (f : (a : R) → P) (r ^ (k + n) * b) = HPow.hPow (α := P) ((f : (a : R) → P) r : P) (k + m) * a
have obtain : ∀ (b : R) (m : ℕ) (e : (f : (a : R) → P) b = HPow.hPow (α := P) ((f : (a : R) → P) r : P) m * a),
  ∃ (b : R) (m : ℕ) (k : ℕ),
    (f : (a : R) → P) (r ^ (k + n) * b) = HPow.hPow (α := P) ((f : (a : R) → P) r : P) (k + m) * a
Tactic: obtain ⟨b, m, e⟩ := H a
-- 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
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
Q : Type u_4
inst_4 : CommSemiring Q
inst_5 : Algebra P Q
f : R →+* P
r : R
inst_6 : Away r S
inst_7 : Away.{u_3, u_4} (R := P) ((f : (a : R) → P) r : P) Q
H : ∀ (a : P), ∃ (b : R) (m : ℕ), (f : (a : R) → P) b = HPow.hPow (α := P) ((f : (a : R) → P) r : P) m * a
a : P
n : ℕ
b : R
m : ℕ
e : (f : (a : R) → P) b = HPow.hPow (α := P) ((f : (a : R) → P) r : P) m * a
⊢ (f : (a : R) → P) (r ^ (0 + n) * b) = HPow.hPow (α := P) ((f : (a : R) → P) r : P) (0 + (n + m)) * a
have simp : HPow.hPow (α := P) ((f : (a : R) → P) r : P) n * (HPow.hPow (α := P) ((f : (a : R) → P) r : P) m * a) =
  HPow.hPow (α := P) ((f : (a : R) → P) r : P) n * HPow.hPow (α := P) ((f : (a : R) → P) r : P) m * a
Tactic: simp [e, pow_add]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (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
P : Type u_3
inst_3 : CommSemiring P
x : R
inst_4 : Away x S
g : R →+* P
Q : Type u_4
inst_5 : CommSemiring Q
inst_6 : Algebra P Q
A : Type u_5
inst_7 : CommSemiring A
inst_8 : Algebra R A
B : Type u_6
inst_9 : CommSemiring B
inst_10 : Algebra R B
Aₚ : Type u_7
inst_11 : CommSemiring Aₚ
inst_12 : Algebra A Aₚ
inst_13 : Algebra R Aₚ
inst_14 : IsScalarTower R A Aₚ
Bₚ : Type u_8
inst_15 : CommSemiring Bₚ
inst_16 : Algebra B Bₚ
inst_17 : Algebra R Bₚ
inst_18 : IsScalarTower R B Bₚ
f : A →ₐ[R] B
a : A
inst_19 : Away a Aₚ
inst_20 : Away.{u_6, u_8} (R := B) ((f : (a : A) → B) a : B) Bₚ
r : R
⊢ OneHom.toFun (↑(↑(map Aₚ Bₚ f.toRingHom a) : Aₚ →* Bₚ) : OneHom Aₚ Bₚ) ((algebraMap R Aₚ : (a : R) → Aₚ) r) =
    (algebraMap R Bₚ : (a : R) → Bₚ) r
have dsimp : Eq.{u_8 + 1} (α := Bₚ)
  (((↑(↑(IsLocalization.map (T := Submonoid.powers ((f : (a : A) → B) a)) Bₚ (↑f : A →+* B) sorry) : Aₚ →* Bₚ) :
          OneHom Aₚ Bₚ) :
        (a : Aₚ) → Bₚ)
      ((algebraMap R Aₚ : (a : R) → Aₚ) r : Aₚ) :
    Bₚ)
  ((algebraMap R Bₚ : (a : R) → Bₚ) r : Bₚ)
Tactic: dsimp only [AlgHom.toRingHom_eq_coe, map, RingHom.coe_coe, OneHom.toFun_eq_coe]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (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
P : Type u_3
inst_3 : CommSemiring P
x : R
inst_4 : Away x S
g : R →+* P
Q : Type u_4
inst_5 : CommSemiring Q
inst_6 : Algebra P Q
A : Type u_5
inst_7 : CommSemiring A
inst_8 : Algebra R A
B : Type u_6
inst_9 : CommSemiring B
inst_10 : Algebra R B
Aₚ : Type u_7
inst_11 : CommSemiring Aₚ
inst_12 : Algebra A Aₚ
inst_13 : Algebra R Aₚ
inst_14 : IsScalarTower R A Aₚ
Bₚ : Type u_8
inst_15 : CommSemiring Bₚ
inst_16 : Algebra B Bₚ
inst_17 : Algebra R Bₚ
inst_18 : IsScalarTower R B Bₚ
f : A →ₐ[R] B
a : A
inst_19 : Away a Aₚ
inst_20 : Away.{u_6, u_8} (R := B) ((f : (a : A) → B) a : B) Bₚ
r : R
⊢ Eq.{u_8 + 1} (α := Bₚ)
    (((↑(↑(IsLocalization.map (T := Submonoid.powers ((f : (a : A) → B) a)) Bₚ (↑f : A →+* B) ⋯) : Aₚ →* Bₚ) :
            OneHom Aₚ Bₚ) :
          (a : Aₚ) → Bₚ)
        ((algebraMap R Aₚ : (a : R) → Aₚ) r : Aₚ) :
      Bₚ)
    ((algebraMap R Bₚ : (a : R) → Bₚ) r : Bₚ)
have rw : Eq.{u_8 + 1} (α := Bₚ)
  (((↑(↑(IsLocalization.map (T := Submonoid.powers ((f : (a : A) → B) a)) Bₚ (↑f : A →+* B) sorry) : Aₚ →* Bₚ) :
          OneHom Aₚ Bₚ) :
        (a : Aₚ) → Bₚ)
      ((algebraMap A Aₚ : (a : A) → Aₚ) ((algebraMap R A : (a : R) → A) r : A) : Aₚ) :
    Bₚ)
  ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B Bₚ) (algebraMap R B) : (a : R) → Bₚ) r : Bₚ)
Tactic: rw [IsScalarTower.algebraMap_apply R A Aₚ, IsScalarTower.algebraMap_eq R B Bₚ]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Away.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_5
inst_1 : CommSemiring A
inst_2 : Algebra R A
B : Type u_6
inst_3 : CommSemiring B
inst_4 : Algebra R B
Aₚ : Type u_7
inst_5 : CommSemiring Aₚ
inst_6 : Algebra A Aₚ
inst_7 : Algebra R Aₚ
inst_8 : IsScalarTower R A Aₚ
Bₚ : Type u_8
inst_9 : CommSemiring Bₚ
inst_10 : Algebra B Bₚ
inst_11 : Algebra R Bₚ
inst_12 : IsScalarTower R B Bₚ
f : A →ₐ[R] B
a : A
inst_13 : Away a Aₚ
inst_14 : Away.{u_6, u_8} (R := B) ((f : (a : A) → B) a : B) Bₚ
hf : Function.Surjective.{u_5 + 1, u_6 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ IsLocalization (Submonoid.map f.toRingHom (Submonoid.powers a)) Bₚ
have simp : IsLocalization.{u_6, u_8} (R := B) (Submonoid.powers ((f : (a : A) → B) a) : Submonoid B) Bₚ
Tactic: simp only [AlgHom.toRingHom_eq_coe, Submonoid.map_powers, RingHom.coe_coe]
-- 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
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
x y : R
inst_7 : Away x S
inst_8 : Away.{u_2, u_5} (R := S) ((algebraMap R S : (a : R) → S) y : S) T
⊢ Away (y * x) T
have refine_1 : IsUnit.{u_5} (M := T) ((algebraMap R T : (a : R) → T) (y * x) : T)
Tactic: refine mk _ ?_ (fun z ↦ ?_) (fun a 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
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
x y : R
inst_7 : Away x S
inst_8 : Away.{u_2, u_5} (R := S) ((algebraMap R S : (a : R) → S) y : S) T
refine_1 : IsUnit.{u_5} (M := T) ((algebraMap R T : (a : R) → T) (y * x) : T)
⊢ Away (y * x) T
have refine_2 : ∀ (z : T),
  ∃ (n : ℕ) (a : R),
    z * HPow.hPow (α := T) ((algebraMap R T : (a : R) → T) (y * x) : T) n = (algebraMap R T : (a : R) → T) a
Tactic: refine mk _ ?_ (fun z ↦ ?_) (fun a 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
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
x y : R
inst_7 : Away x S
inst_8 : Away.{u_2, u_5} (R := S) ((algebraMap R S : (a : R) → S) y : S) T
refine_1 : IsUnit.{u_5} (M := T) ((algebraMap R T : (a : R) → T) (y * x) : T)
refine_2 :
  ∀ (z : T),
    ∃ (n : ℕ) (a : R),
      z * HPow.hPow (α := T) ((algebraMap R T : (a : R) → T) (y * x) : T) n = (algebraMap R T : (a : R) → T) a
⊢ Away (y * x) T
have refine_3 : ∀ (a b : R) (h : Eq.{u_5 + 1} (α := T) ((algebraMap R T : (a : R) → T) a : T) ((algebraMap R T : (a : R) → T) b : T)),
  ∃ (n : ℕ), (y * x) ^ n * a = (y * x) ^ n * b
Tactic: refine mk _ ?_ (fun z ↦ ?_) (fun a 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
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
x y : R
inst_7 : Away x S
inst_8 : Away.{u_2, u_5} (R := S) ((algebraMap R S : (a : R) → S) y : S) T
⊢ IsUnit.{u_5} (M := T) ((algebraMap R T : (a : R) → T) (y * x) : T)
have refine_1 : IsUnit.{u_5} (M := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T) ∧
  IsUnit.{u_5} (M := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T)
Tactic: simp only [map_mul, IsUnit.mul_iff, IsScalarTower.algebraMap_apply R S T]
-- 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
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
x y : R
inst_7 : Away x S
inst_8 : Away.{u_2, u_5} (R := S) ((algebraMap R S : (a : R) → S) y : S) T
z : T
⊢ ∃ (n : ℕ) (a : R),
    z * HPow.hPow (α := T) ((algebraMap R T : (a : R) → T) (y * x) : T) n = (algebraMap R T : (a : R) → T) a
have refine_2 : ∀ (m : ℕ) (p : S)
  (hpq :
    z * HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T) m =
      (algebraMap S T : (a : S) → T) p),
  ∃ (n : ℕ) (a : R),
    z * HPow.hPow (α := T) ((algebraMap R T : (a : R) → T) (y * x) : T) n = (algebraMap R T : (a : R) → T) a
Tactic: obtain ⟨m, p, hpq⟩ := surj (algebraMap R S y) z
-- 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
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
x y : R
inst_7 : Away x S
inst_8 : Away.{u_2, u_5} (R := S) ((algebraMap R S : (a : R) → S) y : S) T
z : T
m : ℕ
p : S
hpq :
  z * HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T) m =
    (algebraMap S T : (a : S) → T) p
⊢ ∃ (n : ℕ) (a : R),
    z * HPow.hPow (α := T) ((algebraMap R T : (a : R) → T) (y * x) : T) n = (algebraMap R T : (a : R) → T) a
have refine_2 : ∀ (n : ℕ) (a : R)
  (hab : p * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) x : S) n = (algebraMap R S : (a : R) → S) a),
  ∃ (n : ℕ) (a : R),
    z * HPow.hPow (α := T) ((algebraMap R T : (a : R) → T) (y * x) : T) n = (algebraMap R T : (a : R) → T) a
Tactic: obtain ⟨n, a, hab⟩ := surj x p
-- 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
inst_2 : Algebra R S
T : Type u_5
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
x y : R
inst_7 : Away x S
inst_8 : Away.{u_2, u_5} (R := S) ((algebraMap R S : (a : R) → S) y : S) T
z : T
m : ℕ
p : S
hpq :
  z * HPow.hPow (α := T) ((algebraMap S T : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T) m =
    (algebraMap S T : (a : S) → T) p
n : ℕ
a : R
hab : p * HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) x : S) n = (algebraMap R S : (a : R) → S) a
⊢ ∃ (n : ℕ) (a : R),
    z * HPow.hPow (α := T) ((algebraMap R T : (a : R) → T) (y * x) : T) n = (algebraMap R T : (a : R) → T) a
have h : z * HPow.hPow (α := T) ((algebraMap R T : (a : R) → T) (y * x) : T) (m + n) =
  (algebraMap R T : (a : R) → T) (a * x ^ m * y ^ n)
Tactic: use m + n, a * x ^ m * y ^ n