awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingHom.Etale
Goal:
rw :
  PropertyIsLocal.{u_5} fun {R S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] ↦
    (fun (R S : Type u_5) (x : CommRing R) (x_1 : CommRing S) (f : R →+* S) ↦ f.FormallyUnramified ∧ f.Smooth) R S inst
      inst_1
⊢ PropertyIsLocal.{u_5} fun {R S : Type u_5} [CommRing R] [CommRing S] ↦ Etale

Tactic:
rw [eq_formallyUnramified_and_smooth]

Premises used: RingHom.Etale.eq_formallyUnramified_and_smooth
-- Module: Mathlib.RingTheory.RingHom.Etale
Goal:
⊢ PropertyIsLocal.{u_5} fun {R S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] ↦
    (fun (R S : Type u_5) (x : CommRing R) (x_1 : CommRing S) (f : R →+* S) ↦ f.FormallyUnramified ∧ f.Smooth) R S inst
      inst_1

Tactic:
FormallyUnramified.propertyIsLocal.and Smooth.propertyIsLocal

Premises used: RingHom.Smooth.propertyIsLocal, RingHom.PropertyIsLocal.and, RingHom.FormallyUnramified.propertyIsLocal
-- Module: Mathlib.RingTheory.RingHom.Etale
Goal:
⊢ PropertyIsLocal.{u_5} fun {R S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] ↦
    (fun (R S : Type u_5) (x : CommRing R) (x_1 : CommRing S) (f : R →+* S) ↦ f.FormallyUnramified ∧ f.Smooth) R S inst
      inst_1

Tactic:
exact FormallyUnramified.propertyIsLocal.and Smooth.propertyIsLocal

Premises used: RingHom.Smooth.propertyIsLocal, RingHom.PropertyIsLocal.and, RingHom.FormallyUnramified.propertyIsLocal
-- Module: Mathlib.RingTheory.RingHom.Etale
Goal:
⊢ RespectsIso.{u_5} fun {R S : Type u_5} [CommRing R] [CommRing S] ↦ Etale

Tactic:
propertyIsLocal.respectsIso

Premises used: RingHom.Etale.propertyIsLocal, RingHom.PropertyIsLocal.respectsIso
-- Module: Mathlib.RingTheory.RingHom.Etale
Goal:
⊢ OfLocalizationSpanTarget.{u_5} fun {R S : Type u_5} [CommRing R] [CommRing S] ↦ Etale

Tactic:
propertyIsLocal.ofLocalizationSpanTarget

Premises used: RingHom.Etale.propertyIsLocal, RingHom.PropertyIsLocal.ofLocalizationSpanTarget
-- Module: Mathlib.RingTheory.RingHom.Etale
Goal:
⊢ OfLocalizationSpan.{u_5} fun {R S : Type u_5} [CommRing R] [CommRing S] ↦ Etale

Tactic:
propertyIsLocal.ofLocalizationSpan

Premises used: RingHom.Etale.propertyIsLocal, RingHom.PropertyIsLocal.ofLocalizationSpan
-- Module: Mathlib.RingTheory.RingHom.Etale
Goal:
rw :
  StableUnderComposition.{u_5} fun {R S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] ↦
    (fun (R S : Type u_5) (x : CommRing R) (x_1 : CommRing S) (f : R →+* S) ↦ f.FormallyUnramified ∧ f.Smooth) R S inst
      inst_1
⊢ StableUnderComposition.{u_5} fun {R S : Type u_5} [CommRing R] [CommRing S] ↦ Etale

Tactic:
rw [eq_formallyUnramified_and_smooth]

Premises used: RingHom.Etale.eq_formallyUnramified_and_smooth
-- Module: Mathlib.RingTheory.RingHom.Etale
Goal:
⊢ StableUnderComposition.{u_5} fun {R S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] ↦
    (fun (R S : Type u_5) (x : CommRing R) (x_1 : CommRing S) (f : R →+* S) ↦ f.FormallyUnramified ∧ f.Smooth) R S inst
      inst_1

Tactic:
FormallyUnramified.stableUnderComposition.and Smooth.stableUnderComposition

Premises used: RingHom.Smooth.stableUnderComposition, RingHom.FormallyUnramified.stableUnderComposition, RingHom.StableUnderComposition.and
-- Module: Mathlib.RingTheory.RingHom.Etale
Goal:
⊢ StableUnderComposition.{u_5} fun {R S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] ↦
    (fun (R S : Type u_5) (x : CommRing R) (x_1 : CommRing S) (f : R →+* S) ↦ f.FormallyUnramified ∧ f.Smooth) R S inst
      inst_1

Tactic:
exact FormallyUnramified.stableUnderComposition.and Smooth.stableUnderComposition

Premises used: RingHom.Smooth.stableUnderComposition, RingHom.FormallyUnramified.stableUnderComposition, RingHom.StableUnderComposition.and
-- Module: Mathlib.RingTheory.RingHom.Etale
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
algInst : Algebra R S := f.toAlgebra
⊢ Algebra.Etale R S ↔ Module.Flat R S ∧ Algebra.FormallyUnramified R S ∧ Algebra.FinitePresentation R S

Tactic:
⟨fun h ↦ ⟨inferInstance, inferInstance, inferInstance⟩,
    fun ⟨_, _, _⟩ ↦ .of_formallyUnramified_of_flat⟩

Premises used: Algebra.Etale.of_formallyUnramified_of_flat, Algebra.Etale, inferInstance, And.intro, Iff.intro, _private.0.RingHom.Etale.iff_flat_and_formallyUnramified.match_4
-- Module: Mathlib.RingTheory.RingHom.Etale
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
algInst : Algebra R S := f.toAlgebra
⊢ Algebra.Etale R S ↔ Module.Flat R S ∧ Algebra.FormallyUnramified R S ∧ Algebra.FinitePresentation R S

Tactic:
refine ⟨fun h ↦ ⟨inferInstance, inferInstance, inferInstance⟩,
    fun ⟨_, _, _⟩ ↦ .of_formallyUnramified_of_flat⟩
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
a : toAlgebra (algebraMap R S) = inst_2
⊢ Module.FaithfullyFlat R S ↔ Module.FaithfullyFlat R S

Tactic:
congr!
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ toAlgebra (algebraMap R S) = inst_2

Tactic:
Algebra.algebra_ext _ _ fun _ ↦ rfl

Premises used: Algebra.algebra_ext, rfl
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ toAlgebra (algebraMap R S) = inst_2

Tactic:
exact Algebra.algebra_ext _ _ fun _ ↦ rfl

Premises used: Algebra.algebra_ext, rfl
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.FaithfullyFlat
⊢ Module.FaithfullyFlat R S

Tactic:
algebraize [f]
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.FaithfullyFlat
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Module.FaithfullyFlat R S
⊢ f.Flat

Tactic:
inferInstanceAs <| Module.Flat R S

Premises used: RingHom.Flat, Module.FaithfullyFlat.toFlat
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.FaithfullyFlat
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Module.FaithfullyFlat R S
⊢ f.Flat

Tactic:
exact inferInstanceAs <| Module.Flat R S
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
algInst : Algebra R S := f.toAlgebra
rw :
  Module.FaithfullyFlat R S ↔
    Module.Flat R S ∧
      Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))
⊢ f.FaithfullyFlat ↔ f.Flat ∧ Function.Surjective (PrimeSpectrum.comap f)

Tactic:
rw [← algebraMap_toAlgebra f, faithfullyFlat_algebraMap_iff, flat_algebraMap_iff]

Premises used: RingHom.faithfullyFlat_algebraMap_iff, RingHom.flat_algebraMap_iff, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
algInst : Algebra R S := f.toAlgebra
⊢ Module.FaithfullyFlat R S ↔
    Module.Flat R S ∧
      Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))

Tactic:
⟨fun h ↦ ⟨inferInstance, PrimeSpectrum.comap_surjective_of_faithfullyFlat⟩,
    fun ⟨h, hf⟩ ↦ .of_comap_surjective hf⟩

Premises used: PrimeSpectrum.comap_surjective_of_faithfullyFlat, Module.FaithfullyFlat.of_comap_surjective, inferInstance, _private.0.RingHom.FaithfullyFlat.iff_flat_and_comap_surjective.match_1, And.intro, Iff.intro, Module.FaithfullyFlat
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
algInst : Algebra R S := f.toAlgebra
⊢ Module.FaithfullyFlat R S ↔
    Module.Flat R S ∧
      Function.Surjective (α := PrimeSpectrum S) (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R S))

Tactic:
exact ⟨fun h ↦ ⟨inferInstance, PrimeSpectrum.comap_surjective_of_faithfullyFlat⟩,
    fun ⟨h, hf⟩ ↦ .of_comap_surjective hf⟩
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
h : ∀ (x : R →+* S), x.FaithfullyFlat ↔ x.Flat ∧ Function.Surjective (PrimeSpectrum.comap x)
⊢ Eq (α := (f : R →+* S) → Prop) FaithfullyFlat fun (f : R →+* S) ↦ f.Flat ∧ Function.Surjective (PrimeSpectrum.comap f)

Tactic:
ext
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
x : R →+* S
h h₁ : x.Flat ∧ Function.Surjective (PrimeSpectrum.comap x) ↔ x.Flat ∧ Function.Surjective (PrimeSpectrum.comap x)
⊢ x.FaithfullyFlat ↔ x.Flat ∧ Function.Surjective (PrimeSpectrum.comap x)

Tactic:
rw [iff_flat_and_comap_surjective]

Premises used: RingHom.FaithfullyFlat.iff_flat_and_comap_surjective
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
Goal:
R S T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.FaithfullyFlat
hg : g.FaithfullyFlat
⊢ Module.FaithfullyFlat R S

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

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

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

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
Goal:
R S T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.FaithfullyFlat
hg : g.FaithfullyFlat
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 : Module.FaithfullyFlat R S
algebraizeInst_1 : Module.FaithfullyFlat S T
⊢ Module.FaithfullyFlat R T

Tactic:
.trans R S T

Premises used: Module.FaithfullyFlat.trans
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
Goal:
R S T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.FaithfullyFlat
hg : g.FaithfullyFlat
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 : Module.FaithfullyFlat R S
algebraizeInst_1 : Module.FaithfullyFlat S T
⊢ Module.FaithfullyFlat R T

Tactic:
exact .trans R S T
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
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)
rw : f.Flat ∧ Function.Surjective (PrimeSpectrum.comap f)
⊢ f.FaithfullyFlat

Tactic:
rw [iff_flat_and_comap_surjective]

Premises used: RingHom.FaithfullyFlat.iff_flat_and_comap_surjective
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
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.Flat ∧ Function.Surjective (PrimeSpectrum.comap f)

Tactic:
⟨.of_bijective hf, fun p ↦ ?_⟩

Premises used: And.intro, RingHom.Flat.of_bijective
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
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)
refine : ∀ (p : PrimeSpectrum R), ∃ (a : PrimeSpectrum S), PrimeSpectrum.comap f a = p
⊢ f.Flat ∧ Function.Surjective (PrimeSpectrum.comap f)

Tactic:
refine ⟨.of_bijective hf, fun p ↦ ?_⟩
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
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)
p : PrimeSpectrum R
h : PrimeSpectrum.comap f (PrimeSpectrum.comap (↑(RingEquiv.symm (RingEquiv.ofBijective f hf)) : S →+* R) p) = p
⊢ ∃ (a : PrimeSpectrum S), PrimeSpectrum.comap f a = p

Tactic:
use p.comap ((RingEquiv.ofBijective f hf).symm : _ →+* _)

Premises used: PrimeSpectrum.comap
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
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)
p : PrimeSpectrum R
a :
  ∀ (x : R),
    Eq (α := R) ((comp (↑(RingEquiv.symm (RingEquiv.ofBijective f hf)) : S →+* R) f : (a : R) → R) x : R)
      ((id R : (a : R) → R) x : R)
⊢ comp (↑(RingEquiv.symm (RingEquiv.ofBijective f hf)) : S →+* R) f = id R

Tactic:
ext
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
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)
p : PrimeSpectrum R
x : R
⊢ Eq.{u_2 + 1} (α := S)
    ((RingEquiv.ofBijective f hf : (a : R) → S)
        ((comp (↑(RingEquiv.symm (RingEquiv.ofBijective f hf)) : S →+* R) f : (a : R) → R) x : R) :
      S)
    ((RingEquiv.ofBijective f hf : (a : R) → S) ((id R : (a : R) → R) x : R) : S)

Tactic:
simp
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
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)
p : PrimeSpectrum R
x : R
⊢ Eq (α := R) ((comp (↑(RingEquiv.symm (RingEquiv.ofBijective f hf)) : S →+* R) f : (a : R) → R) x : R)
    ((id R : (a : R) → R) x : R)

Tactic:
exact (RingEquiv.ofBijective f hf).injective (by simp)

Premises used: RingEquiv.ofBijective, RingEquiv.injective
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
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)
p : PrimeSpectrum R
⊢ comp (↑(RingEquiv.symm (RingEquiv.ofBijective f hf)) : S →+* R) f = id R

Tactic:
have : ((RingEquiv.ofBijective f hf).symm : _ →+* _).comp f = id R := by
    ext
    exact (RingEquiv.ofBijective f hf).injective (by simp)
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
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)
p : PrimeSpectrum R
this : comp (↑(RingEquiv.symm (RingEquiv.ofBijective f hf)) : S →+* R) f = id R
h : PrimeSpectrum.comap (comp (↑(RingEquiv.symm (RingEquiv.ofBijective f hf)) : S →+* R) f) p = p
h₁ : PrimeSpectrum.comap (id R) p = p
h₂ h₃ : (fun (x : PrimeSpectrum R) ↦ x) p = p
⊢ PrimeSpectrum.comap f (PrimeSpectrum.comap (↑(RingEquiv.symm (RingEquiv.ofBijective f hf)) : S →+* R) p) = p

Tactic:
rw [← PrimeSpectrum.comap_comp_apply, this, PrimeSpectrum.comap_id]

Premises used: PrimeSpectrum.comap_comp_apply, PrimeSpectrum.comap_id
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.FaithfullyFlat
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Module.FaithfullyFlat R S
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)

Tactic:
FaithfulSMul.algebraMap_injective R S

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.FaithfullyFlat
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Module.FaithfullyFlat R S
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)

Tactic:
exact FaithfulSMul.algebraMap_injective R S

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
Goal:
⊢ RespectsIso.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FaithfullyFlat

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

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

Tactic:
.mk respectsIso (fun R S T _ _ _ _ _ _ ↦ show (algebraMap _ _).FaithfullyFlat from ?_)

Premises used: RingHom.IsStableUnderBaseChange.mk, RingHom.FaithfullyFlat.respectsIso
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
Goal:
refine :
  ∀ (R S T : Type u_3) (x : CommRing R) (x_1 : CommRing S) (x_2 : CommRing T) (x_3 : Algebra R S) (x_4 : Algebra R T),
    FaithfullyFlat (algebraMap R T) → FaithfullyFlat (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))
⊢ IsStableUnderBaseChange.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FaithfullyFlat

Tactic:
refine .mk respectsIso (fun R S T _ _ _ _ _ _ ↦ show (algebraMap _ _).FaithfullyFlat from ?_)
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
Goal:
R S T : Type u_3
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : FaithfullyFlat (algebraMap R T)
rw : Module.FaithfullyFlat R T → Module.FaithfullyFlat S (TensorProduct R S T)
⊢ FaithfullyFlat (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))

Tactic:
rw [faithfullyFlat_algebraMap_iff] at *

Premises used: RingHom.faithfullyFlat_algebraMap_iff
-- Module: Mathlib.RingTheory.RingHom.FaithfullyFlat
Goal:
R S T : Type u_3
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
x_3 : Algebra R S
x_4 : Algebra R T
h : Module.FaithfullyFlat R T
⊢ Module.FaithfullyFlat S (TensorProduct R S T)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.RingHom.Finite
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.Finite
hg : g.Finite
⊢ (g.comp f).Finite

Tactic:
hg.comp hf

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

Tactic:
exact hg.comp hf

Premises used: RingHom.Finite.comp
-- Module: Mathlib.RingTheory.RingHom.Finite
Goal:
apply : ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.Finite
⊢ RespectsIso @Finite

Tactic:
apply finite_stableUnderComposition.respectsIso

Premises used: RingHom.StableUnderComposition.respectsIso, RingHom.finite_stableUnderComposition
-- Module: Mathlib.RingTheory.RingHom.Finite
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
e : R ≃+* S
⊢ e.toRingHom.Finite

Tactic:
Finite.of_surjective _ (RingEquiv.toEquiv _).surjective

Premises used: RingEquiv.toEquiv, RingHom.Finite.of_surjective, Equiv.surjective
-- Module: Mathlib.RingTheory.RingHom.Finite
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
e : R ≃+* S
⊢ e.toRingHom.Finite

Tactic:
exact Finite.of_surjective _ (RingEquiv.toEquiv _).surjective

Premises used: RingHom.Finite.of_surjective
-- Module: Mathlib.RingTheory.RingHom.Finite
Goal:
⊢ ContainsIdentities @Finite

Tactic:
Finite.id

Premises used: RingHom.Finite.id, RingHom.ContainsIdentities
-- Module: Mathlib.RingTheory.RingHom.Finite
Goal:
⊢ IsStableUnderBaseChange @Finite

Tactic:
IsStableUnderBaseChange.mk finite_respectsIso ?_

Premises used: RingHom.IsStableUnderBaseChange.mk, RingHom.finite_respectsIso
-- Module: Mathlib.RingTheory.RingHom.Finite
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], Finite (algebraMap R T) → Finite (B := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
⊢ IsStableUnderBaseChange @Finite

Tactic:
refine IsStableUnderBaseChange.mk finite_respectsIso ?_

Premises used: RingHom.IsStableUnderBaseChange.mk, RingHom.finite_respectsIso
-- Module: Mathlib.RingTheory.RingHom.Finite
Goal:
simp :
  ∀ ⦃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], Module.Finite R T → Module.Finite 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], Finite (algebraMap R T) → Finite (B := S ⊗[R] T) (algebraMap S (S ⊗[R] T))

Tactic:
simp only [finite_algebraMap]

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

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.RingHom.Finite
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_5
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this_1 : Algebra R S := f.toAlgebra
this_2 : Algebra R S' := toAlgebra (comp (algebraMap S S') f)
f' : R' →+* S' := IsLocalization.map S' f ⋯
this : Algebra R' S' := f'.toAlgebra
⊢ IsScalarTower R R' S'

Tactic:
have : IsScalarTower R R' S' := IsScalarTower.of_algebraMap_eq'
    (IsLocalization.map_comp M.le_comap_map).symm
-- Module: Mathlib.RingTheory.RingHom.Finite
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_5
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this_1 : Algebra R S := f.toAlgebra
this_2 : Algebra R S' := toAlgebra (comp (algebraMap S S') f)
f' : R' →+* S' := IsLocalization.map S' f ⋯
this_3 : Algebra R' S' := f'.toAlgebra
this : IsScalarTower R R' S'
⊢ IsScalarTower R S S'

Tactic:
have : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' rfl
-- Module: Mathlib.RingTheory.RingHom.Finite
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_5
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this_1 : Algebra R S := f.toAlgebra
this_2 : Algebra R S' := toAlgebra (comp (algebraMap S S') f)
f' : R' →+* S' := IsLocalization.map S' f ⋯
this_3 : Algebra R' S' := f'.toAlgebra
this_4 : IsScalarTower R R' S'
this : IsScalarTower R S S'
rwa : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) S'
rwa₁ rwa₂ rwa₃ rwa₄ : IsLocalization (Submonoid.map f M) S'
⊢ IsLocalization (Algebra.algebraMapSubmonoid S M) S'

Tactic:
rwa [Algebra.algebraMapSubmonoid, RingHom.algebraMap_toAlgebra]

Premises used: RingHom.algebraMap_toAlgebra, Algebra.algebraMapSubmonoid
-- Module: Mathlib.RingTheory.RingHom.Finite
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_5
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this_1 : Algebra R S := f.toAlgebra
this_2 : Algebra R S' := toAlgebra (comp (algebraMap S S') f)
f' : R' →+* S' := IsLocalization.map S' f ⋯
this_3 : Algebra R' S' := f'.toAlgebra
this_4 : IsScalarTower R R' S'
this : IsScalarTower R S S'
⊢ IsLocalization (Algebra.algebraMapSubmonoid S M) S'

Tactic:
have : IsLocalization (Algebra.algebraMapSubmonoid S M) S' := by
    rwa [Algebra.algebraMapSubmonoid, RingHom.algebraMap_toAlgebra]
-- Module: Mathlib.RingTheory.RingHom.Finite
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u_5
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
hf : f.Finite
this_1 : Algebra R S := f.toAlgebra
this_2 : Algebra R S' := toAlgebra (comp (algebraMap S S') f)
f' : R' →+* S' := IsLocalization.map S' f ⋯
this_3 : Algebra R' S' := f'.toAlgebra
this_4 : IsScalarTower R R' S'
this_5 : IsScalarTower R S S'
this : IsLocalization (Algebra.algebraMapSubmonoid S M) S'
⊢ Module.Finite R S

Tactic:
have : Module.Finite R S := hf