awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingHom.LocallyStandardSmooth
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth) f
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Smooth) f

Tactic:
exact locally_of_locally (fun hf ↦ hf.smooth) hf

Premises used: RingHom.locally_of_locally
-- Module: Mathlib.RingTheory.RingHom.LocallyStandardSmooth
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
algInst : Algebra R S := f.toAlgebra
⊢ f.Etale ↔ IsStandardSmoothOfRelativeDimension 0 f

Tactic:
Algebra.Etale.iff_isStandardSmoothOfRelativeDimension_zero

Premises used: RingHom.Etale, Algebra.Etale.iff_isStandardSmoothOfRelativeDimension_zero, RingHom.IsStandardSmoothOfRelativeDimension
-- Module: Mathlib.RingTheory.RingHom.LocallyStandardSmooth
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
algInst : Algebra R S := f.toAlgebra
⊢ f.Etale ↔ IsStandardSmoothOfRelativeDimension 0 f

Tactic:
exact Algebra.Etale.iff_isStandardSmoothOfRelativeDimension_zero

Premises used: Algebra.Etale.iff_isStandardSmoothOfRelativeDimension_zero
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
inst_3 : Algebra R S
inst_4 : Algebra R T
r : R
⊢ IsStandardOpenImmersion R (Localization.Away r)

Tactic:
⟨r, inferInstance⟩

Premises used: inferInstance, Exists.intro, Algebra.IsStandardOpenImmersion.mk
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
inst_7 : IsStandardOpenImmersion R S
inst_8 : IsStandardOpenImmersion S T
⊢ IsStandardOpenImmersion R T

Tactic:
let ⟨r, _⟩ := exists_away R S
  let ⟨s, _⟩ := exists_away S T
  have : Away (algebraMap R S (sec r s).1) T :=
    .of_associated (associated_sec_fst r s).symm
  ⟨r * (sec r s).1, mul' S T r _⟩

Premises used: HMul.hMul, _private.0.Algebra.IsStandardOpenImmersion.trans.match_1, Algebra.IsStandardOpenImmersion.exists_away, IsLocalization.Away.sec, Prod.fst, IsLocalization.Away.mul', Associated.symm, Exists.intro, Algebra.IsStandardOpenImmersion, Algebra.IsStandardOpenImmersion.mk, IsLocalization.Away.associated_sec_fst, IsLocalization.Away.of_associated
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
inst_3 : Algebra R S
inst_4 : Algebra R T
inst_5 : IsStandardOpenImmersion R T
⊢ IsStandardOpenImmersion S (S ⊗[R] T)

Tactic:
let ⟨r, _⟩ := exists_away R T
  ⟨algebraMap R S r, inferInstance⟩

Premises used: Algebra.algebraMap, _private.0.Algebra.IsStandardOpenImmersion.trans.match_1, inferInstance, Algebra.IsStandardOpenImmersion.exists_away, Exists.intro, Algebra.IsStandardOpenImmersion, Algebra.IsStandardOpenImmersion.mk, TensorProduct, DFunLike.coe
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring T
inst_3 : Algebra R S
inst_4 : Algebra R T
⊢ IsStandardOpenImmersion R R

Tactic:
⟨1, IsLocalization.away_of_isUnit_of_bijective R isUnit_one Function.bijective_id⟩

Premises used: Function.bijective_id, IsLocalization.away_of_isUnit_of_bijective, isUnit_one, Exists.intro, Algebra.IsStandardOpenImmersion.mk, OfNat.ofNat
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
h : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
rw : ∃ (r : R), Away r S
⊢ IsStandardOpenImmersion R S

Tactic:
rw [Algebra.isStandardOpenImmersion_iff]

Premises used: Algebra.isStandardOpenImmersion_iff
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
h : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
h₁ : Away.{u_1, u_2} (R := R) 1 S
⊢ ∃ (r : R), Away r S

Tactic:
use 1
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
h : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Away.{u_1, u_2} (R := R) 1 S

Tactic:
apply IsLocalization.away_of_isUnit_of_bijective _ isUnit_one h

Premises used: IsLocalization.away_of_isUnit_of_bijective, isUnit_one
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_4
inst_3 : CommSemiring T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
h : IsStandardOpenImmersion R S
rw : ∀ (h : ∃ (r : R), Away r S), ∃ (r : R), Away r T
⊢ IsStandardOpenImmersion R T

Tactic:
rw [Algebra.isStandardOpenImmersion_iff] at *

Premises used: Algebra.isStandardOpenImmersion_iff
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_4
inst_3 : CommSemiring T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
h : ∃ (r : R), Away r S
obtain : ∀ (r : R) (hr : Away r S), ∃ (r : R), Away r T
⊢ ∃ (r : R), Away r T

Tactic:
obtain ⟨r, hr⟩ := h
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_4
inst_3 : CommSemiring T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
r : R
hr : Away r S
h : Away r T
⊢ ∃ (r : R), Away r T

Tactic:
use r
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_4
inst_3 : CommSemiring T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
r : R
hr : Away r S
⊢ Away r T

Tactic:
IsLocalization.isLocalization_of_algEquiv _ e

Premises used: IsLocalization.isLocalization_of_algEquiv
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_4
inst_3 : CommSemiring T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
r : R
hr : Away r S
⊢ Away r T

Tactic:
exact IsLocalization.isLocalization_of_algEquiv _ e

Premises used: IsLocalization.isLocalization_of_algEquiv
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_4
inst_3 : CommSemiring T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
⊢ IsStandardOpenImmersion R S ↔ IsStandardOpenImmersion R T

Tactic:
⟨fun _ ↦ .of_algEquiv e, fun _ ↦ .of_algEquiv e.symm⟩

Premises used: AlgEquiv.symm, Algebra.IsStandardOpenImmersion.of_algEquiv, Iff.intro
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
R' : Type u_4
S' : Type u_5
inst_3 : CommSemiring R'
inst_4 : CommSemiring S'
inst_5 : Algebra R R'
inst_6 : Algebra S S'
inst_7 : Algebra R' S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
inst_11 : IsPushout R S R' S'
inst_12 : IsStandardOpenImmersion R S
rwa rwa₁ rwa₂ rwa₃ : IsPushout R S R' S'
⊢ IsPushout R R' S S'

Tactic:
rwa [IsPushout.comm]

Premises used: Algebra.IsPushout.comm
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
rw : Algebra.IsStandardOpenImmersion R S ↔ Algebra.IsStandardOpenImmersion R S
rw₁ rw₂ : Algebra.IsStandardOpenImmersion R S ↔ Algebra.IsStandardOpenImmersion R S
⊢ IsStandardOpenImmersion (algebraMap R S) ↔ Algebra.IsStandardOpenImmersion R S

Tactic:
rw [IsStandardOpenImmersion, toAlgebra_algebraMap]

Premises used: RingHom.IsStandardOpenImmersion, toAlgebra_algebraMap
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
⊢ IsStandardOpenImmersion (algebraMap R S)

Tactic:
isStandardOpenImmersion_algebraMap.2 ⟨r, inferInstance⟩

Premises used: Iff.mpr, RingHom.isStandardOpenImmersion_algebraMap, inferInstance, Exists.intro, Algebra.IsStandardOpenImmersion.mk
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.IsStandardOpenImmersion
⊢ Algebra.IsStandardOpenImmersion R S

Tactic:
letI := f.toAlgebra; hf

Premises used: RingHom.IsStandardOpenImmersion
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ f.IsStandardOpenImmersion

Tactic:
letI := f.toAlgebra
  ⟨1, IsLocalization.away_of_isUnit_of_bijective _ isUnit_one hf⟩

Premises used: IsLocalization.away_of_isUnit_of_bijective, isUnit_one, Exists.intro, Algebra.IsStandardOpenImmersion.mk, OfNat.ofNat, RingHom.IsStandardOpenImmersion
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R : Type u_1
inst : CommRing R
⊢ IsStandardOpenImmersion (RingHom.id R)

Tactic:
of_bijective Function.bijective_id

Premises used: Function.bijective_id, RingHom.IsStandardOpenImmersion.of_bijective
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.IsStandardOpenImmersion
hg : g.IsStandardOpenImmersion
⊢ Algebra.IsStandardOpenImmersion R S

Tactic:
algebraize [f, g, g.comp f]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.IsStandardOpenImmersion
hg : g.IsStandardOpenImmersion
algebraizeInst : Algebra.IsStandardOpenImmersion R S
⊢ Algebra.IsStandardOpenImmersion S T

Tactic:
algebraize [f, g, g.comp f]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.IsStandardOpenImmersion
hg : g.IsStandardOpenImmersion
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra S T := g.toAlgebra
algInst_2 : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower R S T := ⋯
algebraizeInst : Algebra.IsStandardOpenImmersion R S
algebraizeInst_1 : Algebra.IsStandardOpenImmersion S T
obtain : ∀ (r : R) (hr : IsLocalization.Away r S), (g.comp f).IsStandardOpenImmersion
⊢ (g.comp f).IsStandardOpenImmersion

Tactic:
obtain ⟨r, hr⟩ := hf
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hg : g.IsStandardOpenImmersion
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra S T := g.toAlgebra
algInst_2 : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower R S T := ⋯
algebraizeInst : Algebra.IsStandardOpenImmersion R S
algebraizeInst_1 : Algebra.IsStandardOpenImmersion S T
r : R
hr : IsLocalization.Away r S
obtain : ∀ (s : S) (hs : IsLocalization.Away s T), (g.comp f).IsStandardOpenImmersion
⊢ (g.comp f).IsStandardOpenImmersion

Tactic:
obtain ⟨s, hs⟩ := hg
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra S T := g.toAlgebra
algInst_2 : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower R S T := ⋯
algebraizeInst : Algebra.IsStandardOpenImmersion R S
algebraizeInst_1 : Algebra.IsStandardOpenImmersion S T
r : R
hr : IsLocalization.Away r S
s : S
hs : IsLocalization.Away s T
⊢ (g.comp f).IsStandardOpenImmersion

Tactic:
.trans _ S _

Premises used: RingHom.IsStandardOpenImmersion, Algebra.IsStandardOpenImmersion.trans
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra S T := g.toAlgebra
algInst_2 : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower R S T := ⋯
algebraizeInst : Algebra.IsStandardOpenImmersion R S
algebraizeInst_1 : Algebra.IsStandardOpenImmersion S T
r : R
hr : IsLocalization.Away r S
s : S
hs : IsLocalization.Away s T
⊢ (g.comp f).IsStandardOpenImmersion

Tactic:
exact .trans _ S _
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
⊢ ContainsIdentities.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardOpenImmersion

Tactic:
id

Premises used: RingHom.IsStandardOpenImmersion.id, RingHom.ContainsIdentities
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
⊢ StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardOpenImmersion

Tactic:
@comp

Premises used: RingHom.IsStandardOpenImmersion.comp, RingHom.StableUnderComposition
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
⊢ RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardOpenImmersion

Tactic:
stableUnderComposition.respectsIso fun e ↦ of_bijective e.bijective

Premises used: RingHom.IsStandardOpenImmersion.stableUnderComposition, RingHom.StableUnderComposition.respectsIso, RingHom.IsStandardOpenImmersion.of_bijective, RingEquiv.bijective
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
⊢ IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardOpenImmersion

Tactic:
.mk respectsIso ?_

Premises used: RingHom.IsStableUnderBaseChange.mk, RingHom.IsStandardOpenImmersion.respectsIso
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
refine :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T],
    IsStandardOpenImmersion (algebraMap R T) →
      IsStandardOpenImmersion (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))
⊢ IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardOpenImmersion

Tactic:
refine .mk respectsIso ?_
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : IsStandardOpenImmersion (algebraMap R T)
rw : ∀ (h : Algebra.IsStandardOpenImmersion R T), Algebra.IsStandardOpenImmersion S (TensorProduct R S T)
⊢ IsStandardOpenImmersion (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))

Tactic:
rw [isStandardOpenImmersion_algebraMap] at h ⊢

Premises used: RingHom.isStandardOpenImmersion_algebraMap
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Algebra.IsStandardOpenImmersion R T
⊢ Algebra.IsStandardOpenImmersion S (TensorProduct R S T)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
h : IsLocalization.Away r S
⊢ IsStandardOpenImmersion (algebraMap R S)

Tactic:
.algebraMap r

Premises used: RingHom.IsStandardOpenImmersion.algebraMap
-- Module: Mathlib.RingTheory.RingHom.OpenImmersion
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
h : IsLocalization.Away r S
⊢ IsStandardOpenImmersion (algebraMap R S)

Tactic:
exact .algebraMap r
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.QuasiFinite
⊢ Algebra.QuasiFinite R S

Tactic:
hf

Premises used: RingHom.QuasiFinite
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R : Type u_4
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
rw : Algebra.QuasiFinite R S ↔ Algebra.QuasiFinite R S
rw₁ rw₂ : Algebra.QuasiFinite R S ↔ Algebra.QuasiFinite R S
⊢ QuasiFinite (algebraMap R S) ↔ Algebra.QuasiFinite R S

Tactic:
rw [RingHom.QuasiFinite, toAlgebra_algebraMap]

Premises used: RingHom.QuasiFinite, toAlgebra_algebraMap
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
T : Type u_3
inst : CommRing T
R : Type u_4
S : Type u_5
inst_1 : CommRing R
inst_2 : CommRing S
f : S →+* T
g : R →+* S
hf : f.QuasiFinite
hg : g.QuasiFinite
⊢ Algebra.QuasiFinite S T

Tactic:
algebraize [f, g, (f.comp g)]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
T : Type u_3
inst : CommRing T
R : Type u_4
S : Type u_5
inst_1 : CommRing R
inst_2 : CommRing S
f : S →+* T
g : R →+* S
hf : f.QuasiFinite
hg : g.QuasiFinite
algebraizeInst : Algebra.QuasiFinite S T
⊢ Algebra.QuasiFinite R S

Tactic:
algebraize [f, g, (f.comp g)]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
T : Type u_3
inst : CommRing T
R : Type u_4
S : Type u_5
inst_1 : CommRing R
inst_2 : CommRing S
f : S →+* T
g : R →+* S
hf : f.QuasiFinite
hg : g.QuasiFinite
algInst : Algebra S T := f.toAlgebra
algInst_1 : Algebra R S := g.toAlgebra
algInst_2 : Algebra R T := (f.comp g).toAlgebra
scalarTowerInst : IsScalarTower R S T := ⋯
algebraizeInst : Algebra.QuasiFinite S T
algebraizeInst_1 : Algebra.QuasiFinite R S
⊢ (f.comp g).QuasiFinite

Tactic:
.trans R S T

Premises used: RingHom.QuasiFinite, Algebra.QuasiFinite.trans
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
T : Type u_3
inst : CommRing T
R : Type u_4
S : Type u_5
inst_1 : CommRing R
inst_2 : CommRing S
f : S →+* T
g : R →+* S
hf : f.QuasiFinite
hg : g.QuasiFinite
algInst : Algebra S T := f.toAlgebra
algInst_1 : Algebra R S := g.toAlgebra
algInst_2 : Algebra R T := (f.comp g).toAlgebra
scalarTowerInst : IsScalarTower R S T := ⋯
algebraizeInst : Algebra.QuasiFinite S T
algebraizeInst_1 : Algebra.QuasiFinite R S
⊢ (f.comp g).QuasiFinite

Tactic:
exact .trans R S T
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
T : Type u_3
inst : CommRing T
R : Type u_4
S : Type u_5
inst_1 : CommRing R
inst_2 : CommRing S
f : S →+* T
g : R →+* S
h : (f.comp g).QuasiFinite
⊢ Algebra.QuasiFinite R T

Tactic:
algebraize [f, g, (f.comp g)]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
T : Type u_3
inst : CommRing T
R : Type u_4
S : Type u_5
inst_1 : CommRing R
inst_2 : CommRing S
f : S →+* T
g : R →+* S
h : (f.comp g).QuasiFinite
algInst : Algebra S T := f.toAlgebra
algInst_1 : Algebra R S := g.toAlgebra
algInst_2 : Algebra R T := (f.comp g).toAlgebra
scalarTowerInst : IsScalarTower R S T := ⋯
algebraizeInst : Algebra.QuasiFinite R T
⊢ f.QuasiFinite

Tactic:
.of_restrictScalars R S T

Premises used: Algebra.QuasiFinite.of_restrictScalars, RingHom.QuasiFinite
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
T : Type u_3
inst : CommRing T
R : Type u_4
S : Type u_5
inst_1 : CommRing R
inst_2 : CommRing S
f : S →+* T
g : R →+* S
h : (f.comp g).QuasiFinite
algInst : Algebra S T := f.toAlgebra
algInst_1 : Algebra R S := g.toAlgebra
algInst_2 : Algebra R T := (f.comp g).toAlgebra
scalarTowerInst : IsScalarTower R S T := ⋯
algebraizeInst : Algebra.QuasiFinite R T
⊢ f.QuasiFinite

Tactic:
exact .of_restrictScalars R S T
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
T : Type u_3
inst : CommRing T
R : Type u_4
S : Type u_5
inst_1 : CommRing R
inst_2 : CommRing S
f : S →+* T
g : R →+* S
hg : g.QuasiFinite
⊢ (f.comp g).QuasiFinite ↔ f.QuasiFinite

Tactic:
⟨.of_comp, (.comp · hg)⟩

Premises used: RingHom.QuasiFinite.of_comp, Iff.intro, RingHom.QuasiFinite.comp
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
T : Type u_3
inst : CommRing T
S : Type u_5
inst_1 : CommRing S
f : S →+* T
hf : f.Finite
⊢ Module.Finite S T

Tactic:
algebraize [f]
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
T : Type u_3
inst : CommRing T
S : Type u_5
inst_1 : CommRing S
f : S →+* T
hf : f.Finite
algInst : Algebra S T := f.toAlgebra
algebraizeInst : Module.Finite S T
⊢ f.QuasiFinite

Tactic:
inferInstanceAs (Algebra.QuasiFinite _ _)

Premises used: RingHom.QuasiFinite, Algebra.QuasiFinite.instOfFinite
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
T : Type u_3
inst : CommRing T
S : Type u_5
inst_1 : CommRing S
f : S →+* T
hf : f.Finite
algInst : Algebra S T := f.toAlgebra
algebraizeInst : Module.Finite S T
⊢ f.QuasiFinite

Tactic:
exact inferInstanceAs (Algebra.QuasiFinite _ _)
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
⊢ StableUnderComposition.{u_6} fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ QuasiFinite

Tactic:
fun _ _ _ _ _ _ _ _ hf hg ↦ comp hg hf

Premises used: RingHom.QuasiFinite.comp, RingHom.StableUnderComposition
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
⊢ RespectsIso.{u_6} fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ QuasiFinite

Tactic:
stableUnderComposition.respectsIso fun e ↦ .of_finite e.finite

Premises used: RingHom.StableUnderComposition.respectsIso, RingHom.QuasiFinite.stableUnderComposition, RingEquiv.finite, RingHom.QuasiFinite.of_finite
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
⊢ IsStableUnderBaseChange.{u_6} fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ QuasiFinite

Tactic:
.mk respectsIso ?_

Premises used: RingHom.IsStableUnderBaseChange.mk, RingHom.QuasiFinite.respectsIso
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
refine :
  ∀ ⦃R S T : Type u_6⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T],
    QuasiFinite (algebraMap R T) → QuasiFinite (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))
⊢ IsStableUnderBaseChange.{u_6} fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ QuasiFinite

Tactic:
refine .mk respectsIso ?_
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R S T : Type u_6
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
H : QuasiFinite (algebraMap R T)
rw : ∀ (H : Algebra.QuasiFinite R T), Algebra.QuasiFinite S (TensorProduct R S T)
⊢ QuasiFinite (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))

Tactic:
rw [quasiFinite_algebraMap] at H ⊢

Premises used: RingHom.quasiFinite_algebraMap
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R S T : Type u_6
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
H : Algebra.QuasiFinite R T
⊢ Algebra.QuasiFinite S (TensorProduct R S T)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R S : Type u_6
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
⊢ QuasiFinite (algebraMap R S)

Tactic:
quasiFinite_algebraMap.mpr (.of_isLocalization (.powers r))

Premises used: Iff.mpr, Algebra.QuasiFinite.of_isLocalization, RingHom.quasiFinite_algebraMap, Submonoid.powers
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R S : Type u_6
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
⊢ QuasiFinite (algebraMap R S)

Tactic:
exact quasiFinite_algebraMap.mpr (.of_isLocalization (.powers r))

Premises used: Iff.mpr, Algebra.QuasiFinite.of_isLocalization, RingHom.quasiFinite_algebraMap, Submonoid.powers
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
rw : OfLocalizationFiniteSpanTarget.{u_6} fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ QuasiFinite
⊢ OfLocalizationSpanTarget.{u_6} fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ QuasiFinite

Tactic:
rw [RingHom.ofLocalizationSpanTarget_iff_finite]

Premises used: RingHom.ofLocalizationSpanTarget_iff_finite