awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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 * (↑u : R)) ^ n * a = (r * (↑u : R)) ^ n * b
⊢ ∃ (n : ℕ), (r * (↑u : R)) ^ n * a = (r * (↑u : R)) ^ n * b

Tactic:
use n
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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)
h₄ h₅ : (↑u : R) ^ n * (r ^ n * b) = (↑u : R) ^ n * (r ^ n * b)
⊢ (r * (↑u : R)) ^ n * a = (r * (↑u : R)) ^ n * b

Tactic:
rw [mul_pow, mul_comm (r ^ n), mul_assoc, mul_assoc, hn]

Premises used: mul_assoc, HPow.hPow, mul_comm, mul_pow
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
r r' : R
h : Associated r r'
⊢ Away r S ↔ Away r' S

Tactic:
⟨fun _ ↦ IsLocalization.Away.of_associated h, fun _ ↦ IsLocalization.Away.of_associated h.symm⟩

Premises used: Associated.symm, Iff.intro, IsLocalization.Away.of_associated
-- Module: Mathlib.RingTheory.Localization.Away.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
x : R
inst_3 : Away x S
r : R
h : r ∣ x
⊢ IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) r : S)

Tactic:
isUnit_of_dvd_unit (map_dvd _ h) (algebraMap_isUnit x)

Premises used: isUnit_of_dvd_unit, map_dvd, IsLocalization.Away.algebraMap_isUnit
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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)
obtain : ∀ (n : ℕ) (hn : (fun (x_1 : ℕ) ↦ x ^ x_1) n = (↑y : R)), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
⊢ IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)

Tactic:
obtain ⟨n, hn⟩ := y.2

Premises used: Subtype.property
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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)
rw : IsUnit (HPow.hPow (α := P) ((g : (a : R) → P) x : P) n)
⊢ IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)

Tactic:
rw [← hn, g.map_pow]

Premises used: RingHom.map_pow
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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 (HPow.hPow (α := P) ((g : (a : R) → P) x : P) n)

Tactic:
IsUnit.map (powMonoidHom n : P →* P) hg

Premises used: powMonoidHom, IsUnit.map
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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 (HPow.hPow (α := P) ((g : (a : R) → P) x : P) n)

Tactic:
exact IsUnit.map (powMonoidHom n : P →* P) hg

Premises used: powMonoidHom, IsUnit.map
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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
x : R
inst_4 : Away x S
g : R →+* P
hg : IsUnit.{u_3} (M := P) ((g : (a : R) → P) x : P)
a : R
⊢ Eq.{u_3 + 1} (α := P) ((lift x hg : (a : S) → P) ((algebraMap R S : (a : R) → S) a : S) : P) ((g : (a : R) → P) a : P)

Tactic:
IsLocalization.lift_eq _ _

Premises used: IsLocalization.lift_eq
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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
x : R
inst_4 : Away x S
g : R →+* P
hg : IsUnit.{u_3} (M := P) ((g : (a : R) → P) x : P)
⊢ @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (lift x hg) (algebraMap R S) = g

Tactic:
IsLocalization.lift_comp _

Premises used: IsLocalization.lift_comp, IsLocalization.Away.lift
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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
x : R
inst_4 : Away x S
y : R
inst_5 : Algebra R P
inst_6 : Away (y * x) P
a : R
⊢ Eq.{u_3 + 1} (α := P) ((awayToAwayLeft x y : (a : S) → P) ((algebraMap R S : (a : R) → S) a : S) : P)
    ((algebraMap R P : (a : R) → P) a : P)

Tactic:
lift_eq _ _ _

Premises used: IsLocalization.Away.lift_eq
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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
x : R
inst_4 : Away x S
y : R
inst_5 : Algebra R P
inst_6 : Away (x * y) P
a : R
⊢ Eq.{u_3 + 1} (α := P) ((awayToAwayRight x y : (a : S) → P) ((algebraMap R S : (a : R) → S) a : S) : P)
    ((algebraMap R P : (a : R) → P) a : P)

Tactic:
lift_eq _ _ _

Premises used: IsLocalization.Away.lift_eq
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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 : ℕ
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)
⊢ Membership.mem (γ := Submonoid R) (Submonoid.comap (N := P) f (Submonoid.powers ((f : (a : R) → P) r) : Submonoid P))
    ((fun (x : ℕ) ↦ r ^ x) n)

Tactic:
use n
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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 : ℕ
⊢ 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:
simp
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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
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
⊢ 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

Tactic:
rw [injective_iff_map_eq_zero]

Premises used: injective_iff_map_eq_zero
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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
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
⊢ (∀ (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:
trans ∀ a n, f r ^ n * f a = 0 → ∃ m, r ^ m * a = 0
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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) (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:
simp [(IsLocalization.mk'_surjective (.powers r)).forall, Submonoid.mem_powers_iff,
      IsLocalization.Away.map, IsLocalization.map_mk', IsLocalization.mk'_eq_zero_iff]

Premises used: IsLocalization.map_mk', IsLocalization.mk'_surjective, Function.Surjective.forall, IsLocalization.Away.map, Submonoid.powers, IsLocalization.mk'_eq_zero_iff, Submonoid.mem_powers_iff
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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) (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
x : R
hx : Eq.{u_3 + 1} (α := P) ((f : (a : R) → P) x : P) (0 : P)
⊢ HMul.hMul (β := P) (HPow.hPow (α := P) (β := ℕ) ((f : (a : R) → P) r : P) 0) ((f : (a : R) → P) x : P) = 0

Tactic:
simpa
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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
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
⊢ (∀ (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:
refine ⟨fun H x hx ↦ H x 0 (by simpa), fun H a n ha ↦ ?_⟩
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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
⊢ Eq.{u_3 + 1} (α := P) ((f : (a : R) → P) (r ^ n * a) : P) (0 : P)

Tactic:
simpa
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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
obtain : ∀ (m : ℕ) (hm : r ^ m * (r ^ n * a) = 0), ∃ (m : ℕ), r ^ m * a = 0
⊢ ∃ (m : ℕ), r ^ m * a = 0

Tactic:
obtain ⟨m, hm⟩ := H (r ^ n * a) (by simpa)

Premises used: HMul.hMul, HPow.hPow
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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 : ℕ
hm : r ^ m * (r ^ n * a) = 0
⊢ r ^ (m + n) * a = 0

Tactic:
simp [pow_add, mul_assoc, *]

Premises used: mul_assoc, pow_add
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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 : ℕ
hm : r ^ m * (r ^ n * a) = 0
⊢ ∃ (m : ℕ), r ^ m * a = 0

Tactic:
exact ⟨m + n, by simp [pow_add, mul_assoc, *]⟩
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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
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
⊢ 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

Tactic:
trans ∀ a n, ∃ b m k, f (r ^ (k + n) * b) = f r ^ (k + m) * a
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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) (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:
simp [Function.Surjective, (IsLocalization.mk'_surjective (.powers (f r))).forall, ← map_pow,
      (IsLocalization.mk'_surjective (.powers r)).exists, Submonoid.mem_powers_iff, pow_add,
      IsLocalization.Away.map, IsLocalization.map_mk', ← mul_assoc,
      IsLocalization.mk'_eq_iff_eq, ← map_mul, IsLocalization.eq_iff_exists (.powers (f r))]

Premises used: IsLocalization.map_mk', IsLocalization.mk'_surjective, Function.Surjective.forall, Function.Surjective.exists, mul_assoc, pow_add, map_pow, IsLocalization.mk'_eq_iff_eq, map_mul, IsLocalization.Away.map, Submonoid.powers, Submonoid.mem_powers_iff, DFunLike.coe, Function.Surjective, IsLocalization.eq_iff_exists
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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

Tactic:
⟨fun H x ↦ ⟨_, _, (H x 0).choose_spec.choose_spec.choose_spec⟩, fun H a n ↦ ?_⟩

Premises used: Exists.choose_spec, HMul.hMul, HPow.hPow, HAdd.hAdd, Iff.intro, Exists.intro, Exists.choose, OfNat.ofNat
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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
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
⊢ (∀ (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:
refine ⟨fun H x ↦ ⟨_, _, (H x 0).choose_spec.choose_spec.choose_spec⟩, fun H a n ↦ ?_⟩
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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 : ℕ
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
⊢ ∃ (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
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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
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
⊢ (f : (a : R) → P) (r ^ (0 + n) * b) = HPow.hPow (α := P) ((f : (a : R) → P) r : P) (0 + (n + m)) * a

Tactic:
simp [e, pow_add]

Premises used: pow_add
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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
⊢ 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:
ring_nf
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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
⊢ ∃ (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:
exact ⟨b, n + m, 0, by simp [e, pow_add]; ring_nf⟩
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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 →+* B
a : A
inst_19 : Away.{u_6, u_8} (R := B) ((f : (a : A) → B) a : B) Bₚ
⊢ IsLocalization (Submonoid.map f (Submonoid.powers a)) Bₚ

Tactic:
simpa
-- Module: Mathlib.RingTheory.Localization.Away.Basic
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_1 : R
inst_4 : Away x_1 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ₚ
x : R
inst_19 : Away.{u_5, u_7} (R := A) ((algebraMap R A : (a : R) → A) x : A) Aₚ
⊢ IsLocalization (Algebra.algebraMapSubmonoid A (Submonoid.powers x)) Aₚ

Tactic:
simpa