awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingHom.Finite
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
this_1 : Algebra R S := f.toAlgebra
this_2 : (r : ↥s) →
  Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
  fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R))
this_3 :
  ∀ (r : ↥s),
    IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
      (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
this :
  ∀ (r : ↥s), IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₂ :
  ∀ (r : ↥s),
    Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (Submodule.span (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R))))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
x : S
r : (↑(↑s : Set R) : Type u_5)
n₁ : ℕ
hn₁ :
  Membership.mem (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) (γ :=
    Submodule R (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
    (Submodule.span R (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
    ((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)
          ((algebraMap R S : (a : R) → S)
              (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                    ((↑r : R) ^ n₁) ⋯) :
                R) :
            S)
          x) :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
n₂ : ℕ
hn₂ :
  Membership.mem (γ := Submodule R S)
    (Submodule.span R
      (↑(IsLocalization.finsetIntegerMultiple
            (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R))) (s₁ r)) :
        Set S))
    (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
        ((fun (x : ℕ) ↦ (↑r : R) ^ x) n₂) ⋯ •
      HMul.hMul (α := S)
        ((algebraMap R S : (a : R) → S)
            (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                  ((↑r : R) ^ n₁) ⋯) :
              R) :
          S)
        x)
⊢ Membership.mem (γ := Submodule R S)
    (Submodule.span R
      (↑(IsLocalization.finsetIntegerMultiple
            (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R))) (s₁ r)) :
        Set S))
    ((↑r : R) ^ (n₂ + n₁) • x)

Tactic:
rw [Submonoid.smul_def, ← Algebra.smul_def, smul_smul, ← pow_add] at hn₂

Premises used: pow_add, smul_smul, Submonoid.smul_def, Algebra.smul_def
-- Module: Mathlib.RingTheory.RingHom.Finite
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
this_1 : Algebra R S := f.toAlgebra
this_2 : (r : ↥s) →
  Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
  fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R))
this_3 :
  ∀ (r : ↥s),
    IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
      (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
this :
  ∀ (r : ↥s), IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₂ :
  ∀ (r : ↥s),
    Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (Submodule.span (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R))))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
x : S
r : (↑(↑s : Set R) : Type u_5)
n₁ : ℕ
hn₁ :
  Membership.mem (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) (γ :=
    Submodule R (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
    (Submodule.span R (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
    ((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)
          ((algebraMap R S : (a : R) → S)
              (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                    ((↑r : R) ^ n₁) ⋯) :
                R) :
            S)
          x) :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
n₂ : ℕ
hn₂ :
  Membership.mem (γ := Submodule R S)
    (Submodule.span R
      (↑(IsLocalization.finsetIntegerMultiple
            (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R))) (s₁ r)) :
        Set S))
    ((↑r : R) ^ (n₂ + n₁) • x)
⊢ Membership.mem (γ := Submodule R S)
    (Submodule.span R
      (↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ((algebraMap R S : (a : R) → S) (↑r : R))) (s₁ r) :
            Finset S) :
        Set S))
    ((↑r : R) ^ (n₂ + n₁) • x)

Tactic:
simp_rw [Submonoid.map_powers] at hn₂

Premises used: Submonoid.map_powers
-- Module: Mathlib.RingTheory.RingHom.Finite
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
this_1 : Algebra R S := f.toAlgebra
this_2 : (r : ↥s) →
  Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
  fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R))
this_3 :
  ∀ (r : ↥s),
    IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
      (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
this :
  ∀ (r : ↥s), IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₂ :
  ∀ (r : ↥s),
    Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (Submodule.span (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R))))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
x : S
r : (↑(↑s : Set R) : Type u_5)
n₁ : ℕ
hn₁ :
  Membership.mem (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) (γ :=
    Submodule R (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
    (Submodule.span R (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
    ((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)
          ((algebraMap R S : (a : R) → S)
              (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                    ((↑r : R) ^ n₁) ⋯) :
                R) :
            S)
          x) :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
n₂ : ℕ
hn₂ :
  Membership.mem (γ := Submodule R S)
    (Submodule.span R
      (↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ((algebraMap R S : (a : R) → S) (↑r : R))) (s₁ r) :
            Finset S) :
        Set S))
    ((↑r : R) ^ (n₂ + n₁) • x)
h : Membership.mem (γ := Submodule R S) (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S)) ((↑r : R) ^ (n₂ + n₁) • x)
⊢ ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S)) ((↑r : R) ^ n • x)

Tactic:
use n₂ + n₁
-- Module: Mathlib.RingTheory.RingHom.Finite
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
this_1 : Algebra R S := f.toAlgebra
this_2 : (r : ↥s) →
  Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
  fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R))
this_3 :
  ∀ (r : ↥s),
    IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
      (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
this :
  ∀ (r : ↥s), IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₂ :
  ∀ (r : ↥s),
    Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (Submodule.span (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R))))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
x : S
r : (↑(↑s : Set R) : Type u_5)
n₁ : ℕ
hn₁ :
  Membership.mem (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) (γ :=
    Submodule R (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
    (Submodule.span R (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
    ((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)
          ((algebraMap R S : (a : R) → S)
              (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                    ((↑r : R) ^ n₁) ⋯) :
                R) :
            S)
          x) :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
n₂ : ℕ
hn₂ :
  Membership.mem (γ := Submodule R S)
    (Submodule.span R
      (↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ((algebraMap R S : (a : R) → S) (↑r : R))) (s₁ r) :
            Finset S) :
        Set S))
    ((↑r : R) ^ (n₂ + n₁) • x)
⊢ Membership.mem (γ := Submodule R S) (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S)) ((↑r : R) ^ (n₂ + n₁) • x)

Tactic:
le_iSup (fun x : s => Submodule.span R (sf x : Set S)) r hn₂

Premises used: Set.Mem, setOf, le_iSup, SetLike.coe, Submodule.span
-- Module: Mathlib.RingTheory.RingHom.Finite
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Finset R
hs : Eq (α := Ideal R) (Ideal.span (↑s : Set R)) ⊤
this_1 : Algebra R S := f.toAlgebra
this_2 : (r : ↥s) →
  Algebra (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :=
  fun (r : ↥s) ↦ toAlgebra (Localization.awayMap f (↑r : R))
this_3 :
  ∀ (r : ↥s),
    IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) (Submonoid.powers (↑r : R)))
      (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
this :
  ∀ (r : ↥s), IsScalarTower R (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₁ : (r : ↥s) → Finset (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
s₂ :
  ∀ (r : ↥s),
    Eq (α := Submodule (Localization.Away (↑r : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
      (Submodule.span (Localization.Away (↑r : R)) (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R))))) ⊤
sf : (x : ↥s) → Finset S :=
  fun (x : ↥s) ↦ IsLocalization.finsetIntegerMultiple (Submonoid.powers ((f : (a : R) → S) (↑x : R))) (s₁ x)
x : S
r : (↑(↑s : Set R) : Type u_5)
n₁ : ℕ
hn₁ :
  Membership.mem (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) (γ :=
    Submodule R (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)))
    (Submodule.span R (↑(s₁ r) : Set (Localization.Away ((f : (a : R) → S) (↑r : R)))))
    ((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)
          ((algebraMap R S : (a : R) → S)
              (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                    ((↑r : R) ^ n₁) ⋯) :
                R) :
            S)
          x) :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
n₂ : ℕ
hn₂ :
  Membership.mem (γ := Submodule R S)
    (Submodule.span R
      (↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ((algebraMap R S : (a : R) → S) (↑r : R))) (s₁ r) :
            Finset S) :
        Set S))
    ((↑r : R) ^ (n₂ + n₁) • x)
⊢ Membership.mem (γ := Submodule R S) (⨆ (x : ↥s), Submodule.span R (↑(sf x) : Set S)) ((↑r : R) ^ (n₂ + n₁) • x)

Tactic:
exact le_iSup (fun x : s => Submodule.span R (sf x : Set S)) r hn₂

Premises used: le_iSup, SetLike.coe, Submodule.span
-- Module: Mathlib.RingTheory.RingHom.FinitePresentation
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 : f.FinitePresentation
hg : g.FinitePresentation
⊢ (g.comp f).FinitePresentation

Tactic:
hg.comp hf

Premises used: RingHom.FinitePresentation.comp
-- Module: Mathlib.RingTheory.RingHom.FinitePresentation
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 : f.FinitePresentation
hg : g.FinitePresentation
⊢ (g.comp f).FinitePresentation

Tactic:
exact hg.comp hf

Premises used: RingHom.FinitePresentation.comp
-- Module: Mathlib.RingTheory.RingHom.FinitePresentation
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
e : R ≃+* S
⊢ Ideal.FG (ker e.toRingHom)

Tactic:
simpa using Submodule.fg_bot

Premises used: Submodule.fg_bot
-- Module: Mathlib.RingTheory.RingHom.FinitePresentation
Goal:
h₁ : RespectsIso @FinitePresentation
h₂ :
  ∀ ⦃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],
    FinitePresentation (algebraMap R T) → FinitePresentation (B := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
⊢ IsStableUnderBaseChange @FinitePresentation

Tactic:
apply IsStableUnderBaseChange.mk

Premises used: RingHom.IsStableUnderBaseChange.mk
-- Module: Mathlib.RingTheory.RingHom.FinitePresentation
Goal:
⊢ RespectsIso @FinitePresentation

Tactic:
finitePresentation_respectsIso

Premises used: RingHom.finitePresentation_respectsIso
-- Module: Mathlib.RingTheory.RingHom.FinitePresentation
Goal:
⊢ RespectsIso @FinitePresentation

Tactic:
exact finitePresentation_respectsIso

Premises used: RingHom.finitePresentation_respectsIso
-- Module: Mathlib.RingTheory.RingHom.FinitePresentation
Goal:
h₂ :
  ∀ ⦃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], Algebra.FinitePresentation R T → Algebra.FinitePresentation S (S ⊗[R] T)
⊢ ∀ ⦃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],
    FinitePresentation (algebraMap R T) → FinitePresentation (B := S ⊗[R] T) (algebraMap S (S ⊗[R] T))

Tactic:
simp only [finitePresentation_algebraMap]

Premises used: RingHom.finitePresentation_algebraMap
-- Module: Mathlib.RingTheory.RingHom.FinitePresentation
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 : Algebra.FinitePresentation R T
⊢ Algebra.FinitePresentation S (S ⊗[R] T)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.RingHom.FinitePresentation
Goal:
⊢ LocalizationPreserves @FinitePresentation

Tactic:
finitePresentation_isStableUnderBaseChange.localizationPreserves

Premises used: RingHom.IsStableUnderBaseChange.localizationPreserves, RingHom.finitePresentation_isStableUnderBaseChange
-- Module: Mathlib.RingTheory.RingHom.FinitePresentation
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
rw : Algebra.FinitePresentation R S
⊢ FinitePresentation (algebraMap R S)

Tactic:
rw [finitePresentation_algebraMap]

Premises used: RingHom.finitePresentation_algebraMap
-- Module: Mathlib.RingTheory.RingHom.FinitePresentation
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
⊢ Algebra.FinitePresentation R S

Tactic:
IsLocalization.Away.finitePresentation r

Premises used: IsLocalization.Away.finitePresentation
-- Module: Mathlib.RingTheory.RingHom.FinitePresentation
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
⊢ Algebra.FinitePresentation R S

Tactic:
exact IsLocalization.Away.finitePresentation r

Premises used: IsLocalization.Away.finitePresentation
-- Module: Mathlib.RingTheory.RingHom.FinitePresentation
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H : ∀ (r : (↑s : Type u_1)), Algebra.FinitePresentation R (Localization.Away (↑r : S))
algInst : Algebra R S := f.toAlgebra
r : S
hr : r ∈ s
⊢ Algebra.FinitePresentation R (Localization.Away (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ s) r hr) : S))

Tactic:
H ⟨r, hr⟩

Premises used: Subtype.mk
-- Module: Mathlib.RingTheory.RingHom.FinitePresentation
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H : ∀ (r : (↑s : Type u_1)), Algebra.FinitePresentation R (Localization.Away (↑r : S))
algInst : Algebra R S := f.toAlgebra
r : S
hr : r ∈ s
h :
  Eq.{u_1 + 1} (α := Semiring (Localization.Away r)) OreLocalization.instSemiring CommSemiring.toSemiring →
    Eq.{u_1 + 1} (α := Algebra R (Localization.Away r)) OreLocalization.instAlgebra
      (toAlgebra (comp (algebraMap S (Localization.Away (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ s) r hr) : S))) f))
⊢ Algebra.FinitePresentation R (Localization.Away r)

Tactic:
convert! H ⟨r, hr⟩

Premises used: Subtype.mk
-- Module: Mathlib.RingTheory.RingHom.FinitePresentation
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H : ∀ (r : (↑s : Type u_1)), Algebra.FinitePresentation R (Localization.Away (↑r : S))
algInst : Algebra R S := f.toAlgebra
r : S
hr : r ∈ s
e_4 : Eq.{u_1 + 1} (α := Semiring (Localization.Away r)) OreLocalization.instSemiring CommSemiring.toSemiring
h :
  ∀ (r_1 : R) (x : OreLocalization (Submonoid.powers r) S),
    (have I : Algebra R (OreLocalization (Submonoid.powers r) S) := OreLocalization.instAlgebra;
      r_1 • x) =
      r_1 • x
⊢ Eq.{u_1 + 1} (α := Algebra R (Localization.Away r)) OreLocalization.instAlgebra
    (toAlgebra (comp (algebraMap S (Localization.Away (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ s) r hr) : S))) f))

Tactic:
ext
-- Module: Mathlib.RingTheory.RingHom.FinitePresentation
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H : ∀ (r : (↑s : Type u_1)), Algebra.FinitePresentation R (Localization.Away (↑r : S))
algInst : Algebra R S := f.toAlgebra
r : S
hr : r ∈ s
e_4 : Eq.{u_1 + 1} (α := Semiring (Localization.Away r)) OreLocalization.instSemiring CommSemiring.toSemiring
r_1 : R
x : OreLocalization (Submonoid.powers r) S
h :
  HMul.hMul (α := OreLocalization (Submonoid.powers r) S)
      ((algebraMap R (OreLocalization (Submonoid.powers r) S) : (a : R) → OreLocalization (Submonoid.powers r) S) r_1 :
        OreLocalization (Submonoid.powers r) S)
      x =
    r_1 • x
⊢ (have I : Algebra R (OreLocalization (Submonoid.powers r) S) := OreLocalization.instAlgebra;
    r_1 • x) =
    r_1 • x

Tactic:
simp_rw [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.RingHom.FinitePresentation
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H : ∀ (r : (↑s : Type u_1)), Algebra.FinitePresentation R (Localization.Away (↑r : S))
algInst : Algebra R S := f.toAlgebra
r : S
hr : r ∈ s
e_4 : Eq.{u_1 + 1} (α := Semiring (Localization.Away r)) OreLocalization.instSemiring CommSemiring.toSemiring
r_1 : R
x : OreLocalization (Submonoid.powers r) S
⊢ HMul.hMul (α := OreLocalization (Submonoid.powers r) S)
      ((algebraMap R (OreLocalization (Submonoid.powers r) S) : (a : R) → OreLocalization (Submonoid.powers r) S) r_1 :
        OreLocalization (Submonoid.powers r) S)
      x =
    r_1 • x

Tactic:
rfl
-- Module: Mathlib.RingTheory.RingHom.FinitePresentation
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    FinitePresentation (B := Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
algInst : Algebra R S := f.toAlgebra
⊢ ∀ r ∈ s, Algebra.FinitePresentation R (Localization.Away r)

Tactic:
replace H : ∀ r ∈ s, Algebra.FinitePresentation R (Localization.Away (r : S)) := by
    intro r hr; simp_rw [RingHom.FinitePresentation] at H; convert! H ⟨r, hr⟩; ext
    simp_rw [Algebra.smul_def]; rfl
-- Module: Mathlib.RingTheory.RingHom.FinitePresentation
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
algInst : Algebra R S := f.toAlgebra
H : ∀ r ∈ s, Algebra.FinitePresentation R (Localization.Away r)
⊢ f.FinitePresentation

Tactic:
Algebra.FinitePresentation.of_span_eq_top_target s hs H

Premises used: RingHom.FinitePresentation, Algebra.FinitePresentation.of_span_eq_top_target
-- Module: Mathlib.RingTheory.RingHom.FinitePresentation
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
algInst : Algebra R S := f.toAlgebra
H : ∀ r ∈ s, Algebra.FinitePresentation R (Localization.Away r)
⊢ f.FinitePresentation

Tactic:
exact Algebra.FinitePresentation.of_span_eq_top_target s hs H

Premises used: Algebra.FinitePresentation.of_span_eq_top_target
-- Module: Mathlib.RingTheory.RingHom.FinitePresentation
Goal:
⊢ PropertyIsLocal @FinitePresentation

Tactic:
⟨finitePresentation_localizationPreserves.away,
    finitePresentation_ofLocalizationSpanTarget,
    finitePresentation_ofLocalizationSpanTarget.ofLocalizationSpan
      (finitePresentation_stableUnderComposition.stableUnderCompositionWithLocalizationAway
        finitePresentation_holdsForLocalizationAway).left,
    (finitePresentation_stableUnderComposition.stableUnderCompositionWithLocalizationAway
      finitePresentation_holdsForLocalizationAway).right⟩

Premises used: RingHom.finitePresentation_stableUnderComposition, RingHom.OfLocalizationSpanTarget.ofLocalizationSpan, And.right, And.left, RingHom.finitePresentation_localizationPreserves, RingHom.PropertyIsLocal.mk, RingHom.LocalizationPreserves.away, RingHom.finitePresentation_ofLocalizationSpanTarget, RingHom.finitePresentation_holdsForLocalizationAway, RingHom.StableUnderComposition.stableUnderCompositionWithLocalizationAway
-- Module: Mathlib.RingTheory.RingHom.FiniteType
Goal:
R S T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.FiniteType
hg : g.FiniteType
⊢ (g.comp f).FiniteType

Tactic:
hg.comp hf

Premises used: RingHom.FiniteType.comp
-- Module: Mathlib.RingTheory.RingHom.FiniteType
Goal:
R S T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.FiniteType
hg : g.FiniteType
⊢ (g.comp f).FiniteType

Tactic:
exact hg.comp hf

Premises used: RingHom.FiniteType.comp
-- Module: Mathlib.RingTheory.RingHom.FiniteType
Goal:
⊢ RespectsIso @FiniteType

Tactic:
finiteType_stableUnderComposition.respectsIso (fun {R S} _ _ e ↦ ?_)

Premises used: RingHom.StableUnderComposition.respectsIso, RingHom.finiteType_stableUnderComposition
-- Module: Mathlib.RingTheory.RingHom.FiniteType
Goal:
refine : ∀ {R S : Type u_5} (x : CommRing R) (x_1 : CommRing S) (e : R ≃+* S), e.toRingHom.FiniteType
⊢ RespectsIso @FiniteType

Tactic:
refine finiteType_stableUnderComposition.respectsIso (fun {R S} _ _ e ↦ ?_)

Premises used: RingHom.StableUnderComposition.respectsIso, RingHom.finiteType_stableUnderComposition