awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
n : ℕ
hf : IsStandardSmoothOfRelativeDimension n f
algebraize :
  Algebra.IsStandardSmoothOfRelativeDimension n R S →
    ∃ (g : RingHom.{u, v} (MvPolynomial (Fin n) R) S), g.comp MvPolynomial.C = f ∧ g.Etale
algebraize₁ :
  let algInst := f.toAlgebra;
  Algebra.IsStandardSmoothOfRelativeDimension n R S →
    ∀ (g : MvPolynomial (Fin n) R →ₐ[R] S) (hg : g.Etale),
      ∃ (g : RingHom.{u, v} (MvPolynomial (Fin n) R) S), g.comp MvPolynomial.C = f ∧ g.Etale
⊢ ∃ (g : RingHom.{u, v} (MvPolynomial (Fin n) R) S), g.comp MvPolynomial.C = f ∧ g.Etale

Tactic:
classical
  algebraize [f]
  obtain ⟨g, hg⟩ := Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial n R S
  exact ⟨_, g.comp_algebraMap, hg⟩
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.IsStandardSmooth
obtain :
  ∀ (w w_1 : Type) (w_2 : _root_.Finite w_1),
    _root_.Finite w →
      ∀ (P : Algebra.SubmersivePresentation R S w w_1),
        ∃ (n : ℕ) (g : RingHom.{u, v} (MvPolynomial (Fin n) R) S), g.comp MvPolynomial.C = f ∧ g.Etale
⊢ ∃ (n : ℕ) (g : RingHom.{u, v} (MvPolynomial (Fin n) R) S), g.comp MvPolynomial.C = f ∧ g.Etale

Tactic:
obtain ⟨_, _, _, _, ⟨P⟩⟩ := hf
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
w w_1 : Type
w_2 : _root_.Finite w_1
left : _root_.Finite w
P : Algebra.SubmersivePresentation R S w w_1
this : Algebra R S := f.toAlgebra
⊢ ∃ (n : ℕ) (g : RingHom.{u, v} (MvPolynomial (Fin n) R) S), g.comp MvPolynomial.C = f ∧ g.Etale

Tactic:
⟨_, RingHom.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial
    ⟨_, _, _, ‹_›, P, rfl⟩⟩

Premises used: Exists.intro, Algebra.IsStandardSmoothOfRelativeDimension.mk, RingHom.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial, rfl
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
w w_1 : Type
w_2 : _root_.Finite w_1
left : _root_.Finite w
P : Algebra.SubmersivePresentation R S w w_1
this : Algebra R S := f.toAlgebra
⊢ ∃ (n : ℕ) (g : RingHom.{u, v} (MvPolynomial (Fin n) R) S), g.comp MvPolynomial.C = f ∧ g.Etale

Tactic:
exact ⟨_, RingHom.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial
    ⟨_, _, _, ‹_›, P, rfl⟩⟩
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : Function.Surjective (α := R) (β := S) (⇑f : (a : R) → S)
hg : Function.Surjective (α := S) (β := T) (⇑g : (a : S) → T)
⊢ Function.Surjective (α := R) (β := T) (⇑(g.comp f) : (a : R) → T)

Tactic:
hg.comp hf

Premises used: Function.Surjective.comp
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : Function.Surjective (α := R) (β := S) (⇑f : (a : R) → S)
hg : Function.Surjective (α := S) (β := T) (⇑g : (a : S) → T)
⊢ Function.Surjective (α := R) (β := T) (⇑(g.comp f) : (a : R) → T)

Tactic:
exact hg.comp hf

Premises used: Function.Surjective.comp
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
apply :
  ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S),
    Function.Surjective (α := R) (β := S) (⇑e.toRingHom : (a : R) → S)
⊢ RespectsIso.{u_1} fun {X Y : Type u_1} [CommRing X] [CommRing Y] (f : X →+* Y) ↦
    Function.Surjective (α := X) (β := Y) (⇑f : (a : X) → Y)

Tactic:
apply surjective_stableUnderComposition.respectsIso

Premises used: RingHom.StableUnderComposition.respectsIso, RingHom.surjective_stableUnderComposition
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
R : Type u_1
_ :
  ∀ {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S),
    Function.Surjective (α := R) (β := S) (⇑e.toRingHom : (a : R) → S)
⊢ ∀ {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S),
    Function.Surjective (α := R) (β := S) (⇑e.toRingHom : (a : R) → S)

Tactic:
_
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
R S : Type u_1
_ :
  ∀ [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S),
    Function.Surjective (α := R) (β := S) (⇑e.toRingHom : (a : R) → S)
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S),
    Function.Surjective (α := R) (β := S) (⇑e.toRingHom : (a : R) → S)

Tactic:
_
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
R S : Type u_1
inst : CommRing R
_ : ∀ [inst_1 : CommRing S] (e : R ≃+* S), Function.Surjective (α := R) (β := S) (⇑e.toRingHom : (a : R) → S)
⊢ ∀ [inst_1 : CommRing S] (e : R ≃+* S), Function.Surjective (α := R) (β := S) (⇑e.toRingHom : (a : R) → S)

Tactic:
_
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
e : R ≃+* S
⊢ Function.Surjective (α := R) (β := S) (⇑e.toRingHom : (a : R) → S)

Tactic:
e.surjective

Premises used: RingEquiv.surjective
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
e : R ≃+* S
⊢ Function.Surjective (α := R) (β := S) (⇑e.toRingHom : (a : R) → S)

Tactic:
exact e.surjective

Premises used: RingEquiv.surjective
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
⊢ IsStableUnderBaseChange.{u_1} fun {X Y : Type u_1} [CommRing X] [CommRing Y] (f : X →+* Y) ↦
    Function.Surjective (α := X) (β := Y) (⇑f : (a : X) → Y)

Tactic:
IsStableUnderBaseChange.mk surjective_respectsIso ?_

Premises used: RingHom.IsStableUnderBaseChange.mk, RingHom.surjective_respectsIso
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
refine :
  ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T],
    Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T) →
      Function.Surjective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)
⊢ IsStableUnderBaseChange.{u_1} fun {X Y : Type u_1} [CommRing X] [CommRing Y] (f : X →+* Y) ↦
    Function.Surjective (α := X) (β := Y) (⇑f : (a : X) → Y)

Tactic:
refine IsStableUnderBaseChange.mk surjective_respectsIso ?_

Premises used: RingHom.IsStableUnderBaseChange.mk, RingHom.surjective_respectsIso
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
⊢ ∃ (a : S), Eq (α := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a : S ⊗[R] T) (0 : S ⊗[R] T)

Tactic:
⟨0, map_zero _⟩

Premises used: map_zero, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
⊢ ∃ (a : S), Eq (α := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a : S ⊗[R] T) (0 : S ⊗[R] T)

Tactic:
exact ⟨0, map_zero _⟩
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
x : S
y : T
tmul :
  ∀ (y : R),
    ∃ (a : S),
      Eq (α := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a : S ⊗[R] T)
        (x ⊗ₜ[R] (algebraMap R T : (a : R) → T) y : S ⊗[R] T)
⊢ ∃ (a : S), Eq (α := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a : S ⊗[R] T) (x ⊗ₜ[R] y : S ⊗[R] T)

Tactic:
obtain ⟨y, rfl⟩ := h y

Premises used: rfl
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
x : S
y : R
h₁ :
  Eq (α := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) (y • x) : S ⊗[R] T)
    (x ⊗ₜ[R] (algebraMap R T : (a : R) → T) y : S ⊗[R] T)
⊢ ∃ (a : S),
    Eq (α := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a : S ⊗[R] T)
      (x ⊗ₜ[R] (algebraMap R T : (a : R) → T) y : S ⊗[R] T)

Tactic:
use y • x
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
x : S
y : R
h₁ : Eq (α := S ⊗[R] T) ((y • x) ⊗ₜ[R] 1 : S ⊗[R] T) (x ⊗ₜ[R] (algebraMap R T : (a : R) → T) y : S ⊗[R] T)
⊢ Eq (α := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) (y • x) : S ⊗[R] T)
    (x ⊗ₜ[R] (algebraMap R T : (a : R) → T) y : S ⊗[R] T)

Tactic:
dsimp
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
x : S
y : R
h₁ : Eq (α := S ⊗[R] T) (x ⊗ₜ[R] HSMul.hSMul (β := T) y 1) (x ⊗ₜ[R] (algebraMap R T : (a : R) → T) y)
h₂ h₃ : Eq (α := S ⊗[R] T) (x ⊗ₜ[R] HSMul.hSMul (β := T) y 1) (x ⊗ₜ[R] HSMul.hSMul (β := T) y 1)
⊢ Eq (α := S ⊗[R] T) ((y • x) ⊗ₜ[R] 1 : S ⊗[R] T) (x ⊗ₜ[R] (algebraMap R T : (a : R) → T) y : S ⊗[R] T)

Tactic:
rw [TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one]

Premises used: TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
x y : S ⊗[R] T
ex : ∃ (a : S), (algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a = x
ey : ∃ (a : S), (algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a = y
add :
  ∀ (x y : S),
    ∃ (a : S),
      (algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a =
        HAdd.hAdd (α := S ⊗[R] T) (β := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) x : S ⊗[R] T)
          ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) y : S ⊗[R] T)
⊢ ∃ (a : S), (algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a = x + y

Tactic:
obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := ex, ey

Premises used: rfl
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
x y : S
⊢ ∃ (a : S),
    (algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a =
      HAdd.hAdd (α := S ⊗[R] T) (β := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) x : S ⊗[R] T)
        ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) y : S ⊗[R] T)

Tactic:
⟨x + y, map_add _ x y⟩

Premises used: map_add, HAdd.hAdd, Exists.intro
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
x y : S
⊢ ∃ (a : S),
    (algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a =
      HAdd.hAdd (α := S ⊗[R] T) (β := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) x : S ⊗[R] T)
        ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) y : S ⊗[R] T)

Tactic:
exact ⟨x + y, map_add _ x y⟩
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
x : S ⊗[R] T
zero : ∃ (a : S), Eq (α := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a : S ⊗[R] T) (0 : S ⊗[R] T)
tmul :
  ∀ (x : S) (y : T),
    ∃ (a : S), Eq (α := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a : S ⊗[R] T) (x ⊗ₜ[R] y : S ⊗[R] T)
add :
  ∀ (x y : S ⊗[R] T) (ex : ∃ (a : S), (algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a = x)
    (ey : ∃ (a : S), (algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a = y),
    ∃ (a : S), (algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a = x + y
⊢ ∃ (a : S), (algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a = x

Tactic:
induction x with
  | zero => exact ⟨0, map_zero _⟩
  | tmul x y =>
    obtain ⟨y, rfl⟩ := h y; use y • x; dsimp
    rw [TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one]
  | add x y ex ey => obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := ex, ey; exact ⟨x + y, map_add _ x y⟩

Premises used: TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one, TensorProduct.tmul, rfl
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
introv introv₁ introv₂ introv₃ :
  ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T] (h : Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)),
    Function.Surjective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)
introv₄ :
  ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T] (h : Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)) (x : S ⊗[R] T),
    ∃ (a : S), (algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a = x
⊢ ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T],
    Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T) →
      Function.Surjective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)

Tactic:
classical
  introv h x
  induction x with
  | zero => exact ⟨0, map_zero _⟩
  | tmul x y =>
    obtain ⟨y, rfl⟩ := h y; use y • x; dsimp
    rw [TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one]
  | add x y ex ey => obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := ex, ey; exact ⟨x + y, map_add _ x y⟩

Premises used: TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one, TensorProduct.tmul, rfl
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
e : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {X Y : Type u_1} [CommRing X] [CommRing Y] (f : X →+* Y) ↦
        Function.Surjective (α := X) (β := Y) (⇑f : (a : X) → Y))
      (Localization.Away (↑r : R)) _ _ _ (Localization.awayMap f (↑r : R))
this : Algebra R S := f.toAlgebra
x : S
H₁ :
  ∀ (r : (↑s : Type u_1)),
    ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (LinearMap.range (Algebra.linearMap R S)) ((↑r : R) ^ n • x)
⊢ Membership.mem (γ := Set S) (Set.range (ι := R) (⇑f : (a : R) → S)) x

Tactic:
apply Submodule.mem_of_span_eq_top_of_smul_pow_mem
    (LinearMap.range (Algebra.linearMap R S)) s e

Premises used: Submodule.mem_of_span_eq_top_of_smul_pow_mem, LinearMap.range, Algebra.linearMap
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
e : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {X Y : Type u_1} [CommRing X] [CommRing Y] (f : X →+* Y) ↦
        Function.Surjective (α := X) (β := Y) (⇑f : (a : X) → Y))
      (Localization.Away (↑r : R)) _ _ _ (Localization.awayMap f (↑r : R))
this : Algebra R S := f.toAlgebra
x : S
r : (↑s : Type u_1)
H₁ :
  ∀ (a : Localization.Away (↑r : R))
    (e' :
      Eq (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
        ((Localization.awayMap f (↑r : R) :
              (a : Localization.Away (↑r : R)) → Localization.Away ((f : (a : R) → S) (↑r : R)))
            a :
          Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
        ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
              (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
            x :
          Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))),
    ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (LinearMap.range (Algebra.linearMap R S)) ((↑r : R) ^ n • x)
⊢ ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (LinearMap.range (Algebra.linearMap R S)) ((↑r : R) ^ n • x)

Tactic:
obtain ⟨a, e'⟩ := H r (algebraMap _ _ x)

Premises used: Algebra.algebraMap, DFunLike.coe
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
e : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {X Y : Type u_1} [CommRing X] [CommRing Y] (f : X →+* Y) ↦
        Function.Surjective (α := X) (β := Y) (⇑f : (a : X) → Y))
      (Localization.Away (↑r : R)) _ _ _ (Localization.awayMap f (↑r : R))
this : Algebra R S := f.toAlgebra
x : S
r : (↑s : Type u_1)
a : Localization.Away (↑r : R)
e' :
  Eq (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
    ((Localization.awayMap f (↑r : R) :
          (a : Localization.Away (↑r : R)) → Localization.Away ((f : (a : R) → S) (↑r : R)))
        a :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
        x :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
H₁ :
  ∀ (b : R) (n : ℕ)
    (e' :
      Eq (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
        ((Localization.awayMap f (↑r : R) :
              (a : Localization.Away (↑r : R)) → Localization.Away ((f : (a : R) → S) (↑r : R)))
            (IsLocalization.mk' (Localization.Away (↑r : R)) b
              (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                ((fun (x : ℕ) ↦ (↑r : R) ^ x) n) ⋯)) :
          Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
        ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
              (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
            x :
          Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))),
    ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (LinearMap.range (Algebra.linearMap R S)) ((↑r : R) ^ n • x)
⊢ ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (LinearMap.range (Algebra.linearMap R S)) ((↑r : R) ^ n • x)

Tactic:
obtain ⟨b, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.exists_mk'_eq (Submonoid.powers (r : R)) a

Premises used: Submonoid.powers, Subtype.val, rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
e : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {X Y : Type u_1} [CommRing X] [CommRing Y] (f : X →+* Y) ↦
        Function.Surjective (α := X) (β := Y) (⇑f : (a : X) → Y))
      (Localization.Away (↑r : R)) _ _ _ (Localization.awayMap f (↑r : R))
this : Algebra R S := f.toAlgebra
x : S
r : (↑s : Type u_1)
b : R
n : ℕ
e' :
  Eq (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
    ((Localization.awayMap f (↑r : R) :
          (a : Localization.Away (↑r : R)) → Localization.Away ((f : (a : R) → S) (↑r : R)))
        (IsLocalization.mk' (Localization.Away (↑r : R)) b
          (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
            ((fun (x : ℕ) ↦ (↑r : R) ^ x) n) ⋯)) :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
        x :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
⊢ Eq (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
        (HMul.hMul (β := S) x
          ((↑(Subtype.mk (p := fun (x : S) ↦
                  Membership.mem (γ := Submonoid S) (Submonoid.powers ((f : (a : R) → S) (↑r : R)) : Submonoid S) x)
                  ((f : (a : R) → S)
                    (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                          ((fun (x : ℕ) ↦ (↑r : R) ^ x) n) ⋯) :
                      R))
                  ⋯) :
              S) :
            S)) :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
        ((f : (a : R) → S) b) :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))

Tactic:
rw [Localization.awayMap, IsLocalization.Away.map, IsLocalization.map_mk', eq_comm,
    IsLocalization.eq_mk'_iff_mul_eq, Subtype.coe_mk, Subtype.coe_mk, ← map_mul] at e'

Premises used: Subtype.coe_mk, IsLocalization.map_mk', eq_comm, map_mul, IsLocalization.Away.map, Localization.awayMap, IsLocalization.eq_mk'_iff_mul_eq
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
e : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {X Y : Type u_1} [CommRing X] [CommRing Y] (f : X →+* Y) ↦
        Function.Surjective (α := X) (β := Y) (⇑f : (a : X) → Y))
      (Localization.Away (↑r : R)) _ _ _ (Localization.awayMap f (↑r : R))
this : Algebra R S := f.toAlgebra
x : S
r : (↑s : Type u_1)
b : R
n : ℕ
e' :
  Eq (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
        (HMul.hMul (β := S) x
          ((↑(Subtype.mk (p := fun (x : S) ↦
                  Membership.mem (γ := Submonoid S) (Submonoid.powers ((f : (a : R) → S) (↑r : R)) : Submonoid S) x)
                  ((f : (a : R) → S)
                    (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                          ((fun (x : ℕ) ↦ (↑r : R) ^ x) n) ⋯) :
                      R))
                  ⋯) :
              S) :
            S)) :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
        ((f : (a : R) → S) b) :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
H₁ :
  ∀ (n' : ℕ)
    (e'' :
      (↑(Subtype.mk (p := fun (x : S) ↦
                Membership.mem (γ := Submonoid S) (Submonoid.powers ((f : (a : R) → S) (↑r : R)) : Submonoid S) x)
                ((fun (x : ℕ) ↦ HPow.hPow (α := S) ((f : (a : R) → S) (↑r : R) : S) x) n') ⋯) :
            S) *
          HMul.hMul (β := S) x
            ((↑(Subtype.mk (p := fun (x : S) ↦
                    Membership.mem (γ := Submonoid S) (Submonoid.powers ((f : (a : R) → S) (↑r : R)) : Submonoid S) x)
                    ((f : (a : R) → S)
                      (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                            ((fun (x : ℕ) ↦ (↑r : R) ^ x) n) ⋯) :
                        R))
                    ⋯) :
                S) :
              S) =
        HMul.hMul (β := S)
          (↑(Subtype.mk (p := fun (x : S) ↦
                Membership.mem (γ := Submonoid S) (Submonoid.powers ((f : (a : R) → S) (↑r : R)) : Submonoid S) x)
                ((fun (x : ℕ) ↦ HPow.hPow (α := S) ((f : (a : R) → S) (↑r : R) : S) x) n') ⋯) :
            S)
          ((f : (a : R) → S) b : S)),
    ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (LinearMap.range (Algebra.linearMap R S)) ((↑r : R) ^ n • x)
⊢ ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (LinearMap.range (Algebra.linearMap R S)) ((↑r : R) ^ n • x)

Tactic:
obtain ⟨⟨_, n', rfl⟩, e''⟩ := (IsLocalization.eq_iff_exists (Submonoid.powers (f r)) _).mp e'

Premises used: Submonoid.powers, Iff.mp, Subtype.val, DFunLike.coe, rfl, IsLocalization.eq_iff_exists