awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s : Finset S
hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
a b : (x : S) → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S : (a : R) → S) (a x) = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S)
r : R
hrp : r ∉ p
hr :
  ∀ (r' : R),
    r ∣ r' →
      Function.Injective.{u_1 + 1, u_2 + 1} (α := Away r') (β := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
⊢ ∃ r ∉ p,
    ∀ (r' : R),
      r ∣ r' →
        Function.Bijective.{u_1 + 1, u_2 + 1} (α := Away r') (β :=
          Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
          (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))

Tactic:
⟨r * ∏ i ∈ s, b i, mul_mem (s := p.primeCompl) hrp (prod_mem fun _ _ ↦ hbp _), ?_⟩

Premises used: HMul.hMul, Finset.prod, And.intro, Exists.intro, prod_mem, MulMemClass.mul_mem
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s : Finset S
hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
a b : (x : S) → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S : (a : R) → S) (a x) = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S)
r : R
hrp : r ∉ p
hr :
  ∀ (r' : R),
    r ∣ r' →
      Function.Injective.{u_1 + 1, u_2 + 1} (α := Away r') (β := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
refine :
  ∀ (r' : R),
    r * ∏ i ∈ s, b i ∣ r' →
      Function.Bijective.{u_1 + 1, u_2 + 1} (α := Away r') (β := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
⊢ ∃ r ∉ p,
    ∀ (r' : R),
      r ∣ r' →
        Function.Bijective.{u_1 + 1, u_2 + 1} (α := Away r') (β :=
          Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
          (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))

Tactic:
refine ⟨r * ∏ i ∈ s, b i, mul_mem (s := p.primeCompl) hrp (prod_mem fun _ _ ↦ hbp _), ?_⟩
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s : Finset S
hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
a b : (x : S) → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S : (a : R) → S) (a x) = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S)
r : R
hrp : r ∉ p
hr :
  ∀ (r' : R),
    r ∣ r' →
      Function.Injective.{u_1 + 1, u_2 + 1} (α := Away r') (β := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
⊢ ∀ (r' : R),
    r * ∏ i ∈ s, b i ∣ r' →
      Function.Bijective.{u_1 + 1, u_2 + 1} (α := Away r') (β := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))

Tactic:
fun r' hr' ↦ ⟨hr _ (.trans ⟨_, rfl⟩ hr'), ?_⟩

Premises used: Finset.prod, And.intro, Exists.intro, Function.Bijective, rfl, Dvd.dvd.trans
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s : Finset S
hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
a b : (x : S) → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S : (a : R) → S) (a x) = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S)
r : R
hrp : r ∉ p
hr :
  ∀ (r' : R),
    r ∣ r' →
      Function.Injective.{u_1 + 1, u_2 + 1} (α := Away r') (β := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
refine :
  ∀ (r' : R) (hr' : r * ∏ i ∈ s, b i ∣ r'),
    Function.Surjective.{u_1 + 1, u_2 + 1} (α := Away r') (β := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
      (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
⊢ ∀ (r' : R),
    r * ∏ i ∈ s, b i ∣ r' →
      Function.Bijective.{u_1 + 1, u_2 + 1} (α := Away r') (β := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))

Tactic:
refine fun r' hr' ↦ ⟨hr _ (.trans ⟨_, rfl⟩ hr'), ?_⟩
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s : Finset S
hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
a b : (x : S) → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S : (a : R) → S) (a x) = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S)
r : R
hrp : r ∉ p
hr :
  ∀ (r' : R),
    r ∣ r' →
      Function.Injective.{u_1 + 1, u_2 + 1} (α := Away r') (β := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
r' : R
hr' : r * ∏ i ∈ s, b i ∣ r'
rw :
  (↑s : Set S) ⊆
    (↑(Subalgebra.comap (B := Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))
          (IsScalarTower.toAlgHom R S (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S)))
          (AlgHom.range (awayMapₐ (Algebra.ofId R S) r'))) :
      Set S)
⊢ LE.le (α := Subalgebra R (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S)))
    (AlgHom.range (IsScalarTower.toAlgHom R S (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))))
    (AlgHom.range (awayMapₐ (Algebra.ofId R S) r'))

Tactic:
rw [← Algebra.map_top, Subalgebra.map_le, ← hs, Algebra.adjoin_le_iff]

Premises used: Subalgebra.map_le, Algebra.adjoin_le_iff, Algebra.map_top
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s : Finset S
hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
a b : (x : S) → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S : (a : R) → S) (a x) = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S)
r : R
hrp : r ∉ p
hr :
  ∀ (r' : R),
    r ∣ r' →
      Function.Injective.{u_1 + 1, u_2 + 1} (α := Away r') (β := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
r' : R
hr' : r * ∏ i ∈ s, b i ∣ r'
x : S
hxs : x ∈ (↑s : Set S)
obtain :
  ∀ (r'' : R) (hr' : r' = (r * ∏ i ∈ s, b i) * r''),
    x ∈
      (↑(Subalgebra.comap (B := Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))
            (IsScalarTower.toAlgHom R S (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S)))
            (AlgHom.range (awayMapₐ (Algebra.ofId R S) r'))) :
        Set S)
⊢ x ∈
    (↑(Subalgebra.comap (B := Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))
          (IsScalarTower.toAlgHom R S (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S)))
          (AlgHom.range (awayMapₐ (Algebra.ofId R S) r'))) :
      Set S)

Tactic:
obtain ⟨r'', hr'⟩ := hr'
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s : Finset S
hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
a b : (x : S) → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S : (a : R) → S) (a x) = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S)
r : R
hrp : r ∉ p
hr :
  ∀ (r' : R),
    r ∣ r' →
      Function.Injective.{u_1 + 1, u_2 + 1} (α := Away r') (β := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
r' : R
x : S
hxs : x ∈ (↑s : Set S)
r'' : R
hr' : r' = (r * ∏ i ∈ s, b i) * r''
⊢ x ∈
    (↑(Subalgebra.comap (B := Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))
          (IsScalarTower.toAlgHom R S (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S)))
          (AlgHom.range (awayMapₐ (Algebra.ofId R S) r'))) :
      Set S)

Tactic:
⟨IsLocalization.mk' (M := .powers r') _
      (r'' * r * (∏ i ∈ s.erase x, b i) * a x) ⟨_, 1, rfl⟩, ?_⟩

Premises used: HMul.hMul, Set.Mem, setOf, Finset.prod, Subtype.mk, IsLocalization.mk', Set.preimage, Exists.intro, Set.range, OfNat.ofNat, Finset.erase, rfl
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s : Finset S
hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
a b : (x : S) → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S : (a : R) → S) (a x) = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S)
r : R
hrp : r ∉ p
hr :
  ∀ (r' : R),
    r ∣ r' →
      Function.Injective.{u_1 + 1, u_2 + 1} (α := Away r') (β := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
r' : R
x : S
hxs : x ∈ (↑s : Set S)
r'' : R
hr' : r' = (r * ∏ i ∈ s, b i) * r''
refine :
  Eq.{u_2 + 1} (α := Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))
    (((AlgHom.toRingHom (awayMapₐ (Algebra.ofId R S) r') :
            RingHom.{u_1, u_2} (Away r') (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))) :
          (a : Away r') → Away ((Algebra.ofId R S : (a : R) → S) r'))
        (IsLocalization.mk' (M := Submonoid.powers r') (Away r') ((r'' * r * ∏ i ∈ s.erase x, b i) * a x)
          (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r') x)
            ((fun (x : ℕ) ↦ r' ^ x) 1) ⋯)) :
      Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))
    (((↑(IsScalarTower.toAlgHom R S (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))) :
            S →+* Away ((Algebra.ofId R S : (a : R) → S) r')) :
          (a : S) → Away ((Algebra.ofId R S : (a : R) → S) r'))
        x :
      Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))
⊢ x ∈
    (↑(Subalgebra.comap (B := Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))
          (IsScalarTower.toAlgHom R S (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S)))
          (AlgHom.range (awayMapₐ (Algebra.ofId R S) r'))) :
      Set S)

Tactic:
refine ⟨IsLocalization.mk' (M := .powers r') _
      (r'' * r * (∏ i ∈ s.erase x, b i) * a x) ⟨_, 1, rfl⟩, ?_⟩
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s : Finset S
hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
a b : (x : S) → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S : (a : R) → S) (a x) = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S)
r : R
hrp : r ∉ p
hr :
  ∀ (r' : R),
    r ∣ r' →
      Function.Injective.{u_1 + 1, u_2 + 1} (α := Away r') (β := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
r' : R
x : S
hxs : x ∈ (↑s : Set S)
r'' : R
hr' : r' = (r * ∏ i ∈ s, b i) * r''
dsimp :
  Eq.{u_2 + 1} (α := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
    (((IsLocalization.map (T := Submonoid.powers ((algebraMap R S : (a : R) → S) r'))
              (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S)) (algebraMap R S) ⋯ :
            RingHom.{u_1, u_2} (Away r') (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))) :
          (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
        (IsLocalization.mk' (M := Submonoid.powers r') (Away r') ((r'' * r * ∏ i ∈ s.erase x, b i) * a x)
          (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r') x)
            (HPow.hPow (β := ℕ) r' 1) ⋯)) :
      Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
    ((algebraMap S (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S)) :
          (a : S) → Away ((algebraMap R S : (a : R) → S) r'))
        x :
      Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
⊢ Eq.{u_2 + 1} (α := Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))
    (((AlgHom.toRingHom (awayMapₐ (Algebra.ofId R S) r') :
            RingHom.{u_1, u_2} (Away r') (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))) :
          (a : Away r') → Away ((Algebra.ofId R S : (a : R) → S) r'))
        (IsLocalization.mk' (M := Submonoid.powers r') (Away r') ((r'' * r * ∏ i ∈ s.erase x, b i) * a x)
          (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers r') x)
            ((fun (x : ℕ) ↦ r' ^ x) 1) ⋯)) :
      Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))
    (((↑(IsScalarTower.toAlgHom R S (Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))) :
            S →+* Away ((Algebra.ofId R S : (a : R) → S) r')) :
          (a : S) → Away ((Algebra.ofId R S : (a : R) → S) r'))
        x :
      Away (M := S) ((Algebra.ofId R S : (a : R) → S) r' : S))

Tactic:
dsimp [awayMapₐ, IsLocalization.Away.map]

Premises used: IsLocalization.Away.map, Localization.awayMapₐ
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s : Finset S
hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
a b : (x : S) → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S : (a : R) → S) (a x) = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S)
r : R
hrp : r ∉ p
hr :
  ∀ (r' : R),
    r ∣ r' →
      Function.Injective.{u_1 + 1, u_2 + 1} (α := Away r') (β := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
r' : R
x : S
hxs : x ∈ (↑s : Set S)
r'' : R
hr' : r' = (r * ∏ i ∈ s, b i) * r''
h :
  HMul.hMul (β := S)
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) r'' : S) ((algebraMap R S : (a : R) → S) r : S))
        ((algebraMap R S : (a : R) → S) (∏ i ∈ s.erase x, b i) : S) *
      HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S) =
    HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) r' : S)
⊢ Eq (α := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
    ((algebraMap S (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S)) :
          (a : S) → Away ((algebraMap R S : (a : R) → S) r'))
        (HMul.hMul (β := S)
            (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) r'' : S)
              ((algebraMap R S : (a : R) → S) r : S))
            ((algebraMap R S : (a : R) → S) (∏ i ∈ s.erase x, b i) : S) *
          HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S)) :
      Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
    ((algebraMap S (Away (M := S) ((algebraMap R S : (a : R) → S) r' : S)) :
          (a : S) → Away ((algebraMap R S : (a : R) → S) r'))
        (HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) r' : S)) :
      Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))

Tactic:
congr 1
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s : Finset S
hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
a b : (x : S) → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S : (a : R) → S) (a x) = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S)
r : R
hrp : r ∉ p
hr :
  ∀ (r' : R),
    r ∣ r' →
      Function.Injective.{u_1 + 1, u_2 + 1} (α := Away r') (β := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
r' : R
x : S
hxs : x ∈ (↑s : Set S)
r'' : R
hr' : r' = (r * ∏ i ∈ s, b i) * r''
h :
  HMul.hMul (β := S)
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) r'' : S) ((algebraMap R S : (a : R) → S) r : S))
        ((algebraMap R S : (a : R) → S) (∏ i ∈ s.erase x, b i) : S) *
      HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S) =
    x *
      HMul.hMul (β := S)
        (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) r : S)
          (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (∏ x ∈ s.erase x, b x) : S)
            ((algebraMap R S : (a : R) → S) (b x) : S)))
        ((algebraMap R S : (a : R) → S) r'' : S)
⊢ HMul.hMul (β := S)
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) r'' : S) ((algebraMap R S : (a : R) → S) r : S))
        ((algebraMap R S : (a : R) → S) (∏ i ∈ s.erase x, b i) : S) *
      HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S) =
    HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) r' : S)

Tactic:
rw [hr', ← Finset.prod_erase_mul s b hxs, map_mul, map_mul, map_mul]

Premises used: Finset.prod_erase_mul, map_mul
-- Module: Mathlib.RingTheory.Unramified.LocalRing
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
inst_3 : p.IsPrime
q : Ideal S
inst_4 : q.IsPrime
hq : Eq (α := Set (Ideal S)) (p.primesOver S) {q}
inst_5 : Module.Finite R S
inst_6 : q.LiesOver p
hRS : Ideal.FG (RingHom.ker (F := R →+* S) (algebraMap R S))
H :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime p) (β := Localization.AtPrime q)
    (⇑(localRingHom p q (algebraMap R S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime q)
s : Finset S
hs : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
a b : (x : S) → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S : (a : R) → S) (a x) = HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S)
r : R
hrp : r ∉ p
hr :
  ∀ (r' : R),
    r ∣ r' →
      Function.Injective.{u_1 + 1, u_2 + 1} (α := Away r') (β := Away (M := S) ((algebraMap R S : (a : R) → S) r' : S))
        (⇑(awayMap (algebraMap R S) r') : (a : Away r') → Away ((algebraMap R S : (a : R) → S) r'))
r' : R
x : S
hxs : x ∈ (↑s : Set S)
r'' : R
hr' : r' = (r * ∏ i ∈ s, b i) * r''
⊢ HMul.hMul (β := S)
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) r'' : S) ((algebraMap R S : (a : R) → S) r : S))
        ((algebraMap R S : (a : R) → S) (∏ i ∈ s.erase x, b i) : S) *
      HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (b x) : S) =
    x *
      HMul.hMul (β := S)
        (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) r : S)
          (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (∏ x ∈ s.erase x, b x) : S)
            ((algebraMap R S : (a : R) → S) (b x) : S)))
        ((algebraMap R S : (a : R) → S) r'' : S)

Tactic:
ring_nf