awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingHom.FiniteType
Goal:
R S : Type u_5
x : CommRing R
x_1 : CommRing S
e : R ≃+* S
algInst : Algebra R S := e.toRingHom.toAlgebra
⊢ e.toRingHom.FiniteType

Tactic:
apply Algebra.FiniteType.equiv (inferInstanceAs <| Algebra.FiniteType R R) <|
    .ofRingEquiv (congrFun rfl)

Premises used: Algebra.FiniteType.equiv
-- Module: Mathlib.RingTheory.RingHom.FiniteType
Goal:
h₁ : RespectsIso @FiniteType
h₂ :
  ∀ ⦃R S T : Type u_5⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], FiniteType (algebraMap R T) → FiniteType (B := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
⊢ IsStableUnderBaseChange @FiniteType

Tactic:
apply IsStableUnderBaseChange.mk

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

Tactic:
finiteType_respectsIso

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

Tactic:
exact finiteType_respectsIso

Premises used: RingHom.finiteType_respectsIso
-- Module: Mathlib.RingTheory.RingHom.FiniteType
Goal:
R S T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : FiniteType (algebraMap R T)
⊢ Algebra.FiniteType R T

Tactic:
rw [finiteType_algebraMap] at h

Premises used: RingHom.finiteType_algebraMap
-- Module: Mathlib.RingTheory.RingHom.FiniteType
Goal:
R S T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Algebra.FiniteType R T
h₂ : Algebra.FiniteType S (S ⊗[R] T)
⊢ FiniteType (B := S ⊗[R] T) (algebraMap S (S ⊗[R] T))

Tactic:
apply finiteType_algebraMap.mpr

Premises used: Iff.mpr, RingHom.finiteType_algebraMap
-- Module: Mathlib.RingTheory.RingHom.FiniteType
Goal:
R S T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Algebra.FiniteType R T
⊢ Algebra.FiniteType S (S ⊗[R] T)

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

Tactic:
finiteType_isStableUnderBaseChange.localizationPreserves

Premises used: RingHom.finiteType_isStableUnderBaseChange, RingHom.IsStableUnderBaseChange.localizationPreserves
-- Module: Mathlib.RingTheory.RingHom.FiniteType
Goal:
R S R' S' : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
f : R →+* S
inst_5 : Algebra S S'
r : R
inst_6 : IsLocalization.Away r R'
inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'
hf : f.FiniteType
⊢ FiniteType (IsLocalization.Away.map R' S' f r)

Tactic:
finiteType_localizationPreserves.away _ r _ _ hf

Premises used: RingHom.LocalizationPreserves.away, RingHom.finiteType_localizationPreserves
-- Module: Mathlib.RingTheory.RingHom.FiniteType
Goal:
⊢ OfLocalizationSpan @FiniteType

Tactic:
OfLocalizationSpan.mk _ finiteType_respectsIso (fun s hs h ↦ ?_)

Premises used: RingHom.OfLocalizationSpan.mk, RingHom.finiteType_respectsIso
-- Module: Mathlib.RingTheory.RingHom.FiniteType
Goal:
refine :
  ∀ {R S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (s : Set R)
    (hs : Eq (α := Ideal R) (Ideal.span s) ⊤)
    (h :
      ∀ r ∈ s,
        FiniteType.{u_5, u_5} (A := Localization.Away r) (B := Localization.Away r ⊗[R] S)
          (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))),
    FiniteType (algebraMap R S)
⊢ OfLocalizationSpan @FiniteType

Tactic:
refine OfLocalizationSpan.mk _ finiteType_respectsIso (fun s hs h ↦ ?_)

Premises used: RingHom.OfLocalizationSpan.mk, RingHom.finiteType_respectsIso
-- Module: Mathlib.RingTheory.RingHom.FiniteType
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
h :
  ∀ r ∈ s,
    FiniteType.{u_5, u_5} (A := Localization.Away r) (B := Localization.Away r ⊗[R] S)
      (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))
simp_rw :
  ∀ (h : ∀ r ∈ s, Algebra.FiniteType.{u_5, u_5} (Localization.Away r) (Localization.Away r ⊗[R] S)),
    Algebra.FiniteType R S
⊢ FiniteType (algebraMap R S)

Tactic:
simp_rw [finiteType_algebraMap] at h ⊢

Premises used: RingHom.finiteType_algebraMap
-- Module: Mathlib.RingTheory.RingHom.FiniteType
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
h : ∀ r ∈ s, Algebra.FiniteType.{u_5, u_5} (Localization.Away r) (Localization.Away r ⊗[R] S)
⊢ Algebra.FiniteType R S

Tactic:
Algebra.FiniteType.of_span_eq_top_source s hs h

Premises used: Algebra.FiniteType.of_span_eq_top_source
-- Module: Mathlib.RingTheory.RingHom.FiniteType
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
h : ∀ r ∈ s, Algebra.FiniteType.{u_5, u_5} (Localization.Away r) (Localization.Away r ⊗[R] S)
⊢ Algebra.FiniteType R S

Tactic:
exact Algebra.FiniteType.of_span_eq_top_source s hs h

Premises used: Algebra.FiniteType.of_span_eq_top_source
-- Module: Mathlib.RingTheory.RingHom.FiniteType
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
rw : Algebra.FiniteType R S
⊢ FiniteType (algebraMap R S)

Tactic:
rw [finiteType_algebraMap]

Premises used: RingHom.finiteType_algebraMap
-- Module: Mathlib.RingTheory.RingHom.FiniteType
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
⊢ Algebra.FiniteType R S

Tactic:
IsLocalization.finiteType_of_monoid_fg (Submonoid.powers r) S

Premises used: IsLocalization.finiteType_of_monoid_fg, Submonoid.powers
-- Module: Mathlib.RingTheory.RingHom.FiniteType
Goal:
R S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
⊢ Algebra.FiniteType R S

Tactic:
exact IsLocalization.finiteType_of_monoid_fg (Submonoid.powers r) S

Premises used: IsLocalization.finiteType_of_monoid_fg, Submonoid.powers
-- Module: Mathlib.RingTheory.RingHom.FiniteType
Goal:
R S : Type u_5
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_5)), Algebra.FiniteType R (Localization.Away (↑r : S))
algInst : Algebra R S := f.toAlgebra
r : S
hr : r ∈ s
⊢ Algebra.FiniteType 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.FiniteType
Goal:
R S : Type u_5
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_5)), Algebra.FiniteType R (Localization.Away (↑r : S))
algInst : Algebra R S := f.toAlgebra
r : S
hr : r ∈ s
h :
  Eq.{u_5 + 1} (α := Semiring (Localization.Away r)) OreLocalization.instSemiring CommSemiring.toSemiring →
    Eq.{u_5 + 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.FiniteType R (Localization.Away r)

Tactic:
convert! H ⟨r, hr⟩

Premises used: Subtype.mk
-- Module: Mathlib.RingTheory.RingHom.FiniteType
Goal:
R S : Type u_5
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_5)), Algebra.FiniteType R (Localization.Away (↑r : S))
algInst : Algebra R S := f.toAlgebra
r : S
hr : r ∈ s
e_4 : Eq.{u_5 + 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_5 + 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.FiniteType
Goal:
R S : Type u_5
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_5)), Algebra.FiniteType R (Localization.Away (↑r : S))
algInst : Algebra R S := f.toAlgebra
r : S
hr : r ∈ s
e_4 : Eq.{u_5 + 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.FiniteType
Goal:
R S : Type u_5
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_5)), Algebra.FiniteType R (Localization.Away (↑r : S))
algInst : Algebra R S := f.toAlgebra
r : S
hr : r ∈ s
e_4 : Eq.{u_5 + 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.FiniteType
Goal:
R S : Type u_5
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_5)),
    FiniteType (B := Localization.Away (↑r : S)) (comp (algebraMap S (Localization.Away (↑r : S))) f)
algInst : Algebra R S := f.toAlgebra
⊢ ∀ r ∈ s, Algebra.FiniteType R (Localization.Away r)

Tactic:
replace H : ∀ r ∈ s, Algebra.FiniteType R (Localization.Away (r : S)) := by
    intro r hr; simp_rw [RingHom.FiniteType] at H; convert! H ⟨r, hr⟩; ext
    simp_rw [Algebra.smul_def]; rfl
-- Module: Mathlib.RingTheory.RingHom.FiniteType
Goal:
R S : Type u_5
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.FiniteType R (Localization.Away r)
⊢ f.FiniteType

Tactic:
Algebra.FiniteType.of_span_eq_top_target s hs H

Premises used: RingHom.FiniteType, Algebra.FiniteType.of_span_eq_top_target
-- Module: Mathlib.RingTheory.RingHom.FiniteType
Goal:
R S : Type u_5
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.FiniteType R (Localization.Away r)
⊢ f.FiniteType

Tactic:
exact Algebra.FiniteType.of_span_eq_top_target s hs H

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

Tactic:
⟨finiteType_localizationPreserves.away,
    finiteType_ofLocalizationSpanTarget,
    finiteType_ofLocalizationSpanTarget.ofLocalizationSpan
      (finiteType_stableUnderComposition.stableUnderCompositionWithLocalizationAway
        finiteType_holdsForLocalizationAway).left,
    (finiteType_stableUnderComposition.stableUnderCompositionWithLocalizationAway
      finiteType_holdsForLocalizationAway).right⟩

Premises used: RingHom.finiteType_holdsForLocalizationAway, RingHom.finiteType_ofLocalizationSpanTarget, RingHom.finiteType_stableUnderComposition, RingHom.OfLocalizationSpanTarget.ofLocalizationSpan, And.right, And.left, RingHom.PropertyIsLocal.mk, RingHom.LocalizationPreserves.away, RingHom.finiteType_localizationPreserves, RingHom.StableUnderComposition.stableUnderCompositionWithLocalizationAway
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
rw : Module.Flat R S ↔ Module.Flat R S
rw₁ rw₂ : Module.Flat R S ↔ Module.Flat R S
⊢ Flat (algebraMap R S) ↔ Module.Flat R S

Tactic:
rw [RingHom.Flat, toAlgebra_algebraMap]

Premises used: RingHom.Flat, toAlgebra_algebraMap
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R : Type u_1
inst : CommRing R
⊢ Flat (RingHom.id R)

Tactic:
Module.Flat.self

Premises used: RingHom.Flat, Module.Flat.self
-- Module: Mathlib.RingTheory.RingHom.Flat
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.Flat
hg : g.Flat
⊢ Module.Flat R S

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

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.RingHom.Flat
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.Flat
hg : g.Flat
algebraizeInst : Module.Flat R S
⊢ Module.Flat S T

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

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.RingHom.Flat
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.Flat
hg : g.Flat
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.Flat R S
algebraizeInst_1 : Module.Flat S T
⊢ (g.comp f).Flat

Tactic:
Module.Flat.trans R S T

Premises used: RingHom.Flat, Module.Flat.trans
-- Module: Mathlib.RingTheory.RingHom.Flat
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.Flat
hg : g.Flat
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.Flat R S
algebraizeInst_1 : Module.Flat S T
⊢ (g.comp f).Flat

Tactic:
exact Module.Flat.trans R S T

Premises used: Module.Flat.trans
-- Module: Mathlib.RingTheory.RingHom.Flat
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)
algInst : Algebra R S := f.toAlgebra
⊢ f.Flat

Tactic:
Module.Flat.of_linearEquiv (LinearEquiv.ofBijective (Algebra.linearMap R S) hf).symm

Premises used: RingHom.Flat, LinearEquiv.symm, Algebra.linearMap, Module.Flat.of_linearEquiv, LinearEquiv.ofBijective
-- Module: Mathlib.RingTheory.RingHom.Flat
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)
algInst : Algebra R S := f.toAlgebra
⊢ f.Flat

Tactic:
exact Module.Flat.of_linearEquiv (LinearEquiv.ofBijective (Algebra.linearMap R S) hf).symm

Premises used: LinearEquiv.symm, Algebra.linearMap, Module.Flat.of_linearEquiv, LinearEquiv.ofBijective
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
⊢ ContainsIdentities.{u_4} fun {R S : Type u_4} [CommRing R] [CommRing S] ↦ Flat

Tactic:
id

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

Tactic:
hf.comp hg

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

Tactic:
exact hf.comp hg

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

Tactic:
apply stableUnderComposition.respectsIso

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

Tactic:
of_bijective e.bijective

Premises used: RingEquiv.bijective, RingHom.Flat.of_bijective
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S : Type u_4
inst : CommRing R
inst_1 : CommRing S
e : R ≃+* S
⊢ e.toRingHom.Flat

Tactic:
exact of_bijective e.bijective

Premises used: RingHom.Flat.of_bijective
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
apply :
  ∀ ⦃R S T : Type u_4⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], Flat (algebraMap R T) → Flat (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
⊢ IsStableUnderBaseChange.{u_4} fun {R S : Type u_4} [CommRing R] [CommRing S] ↦ Flat

Tactic:
apply IsStableUnderBaseChange.mk respectsIso

Premises used: RingHom.IsStableUnderBaseChange.mk, RingHom.Flat.respectsIso
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S T : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Flat (algebraMap R T)
rw : ∀ (h : Module.Flat R T), Module.Flat S (S ⊗[R] T)
⊢ Flat (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))

Tactic:
rw [flat_algebraMap_iff] at h ⊢

Premises used: RingHom.flat_algebraMap_iff
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S T : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Module.Flat R T
⊢ Module.Flat S (S ⊗[R] T)

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

Tactic:
flat_algebraMap_iff.mpr (IsLocalization.flat _ (Submonoid.powers r))

Premises used: Iff.mpr, Submonoid.powers, IsLocalization.flat, RingHom.flat_algebraMap_iff
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
h : IsLocalization.Away r S
⊢ Flat (algebraMap R S)

Tactic:
exact flat_algebraMap_iff.mpr (IsLocalization.flat _ (Submonoid.powers r))

Premises used: Iff.mpr, RingHom.flat_algebraMap_iff
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hsp : Eq (α := Ideal S) (Ideal.span s) ⊤
h :
  ∀ (r : (↑s : Type u_4)),
    (@fun {R S : Type u_4} [CommRing R] [CommRing S] ↦ (Flat : (f : R →+* S) → Prop)) _ (Localization.Away (↑r : S)) _ _
      (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)
algInst : Algebra R S := f.toAlgebra
⊢ f.Flat

Tactic:
Module.flat_of_isLocalized_span _ _ s hsp _
    (fun r ↦ Algebra.linearMap S <| Localization.Away r.1) ?_

Premises used: RingHom.Flat, Localization.Away, Module.flat_of_isLocalized_span, Algebra.linearMap, Subtype.val
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hsp : Eq (α := Ideal S) (Ideal.span s) ⊤
h :
  ∀ (r : (↑s : Type u_4)),
    (@fun {R S : Type u_4} [CommRing R] [CommRing S] ↦ (Flat : (f : R →+* S) → Prop)) _ (Localization.Away (↑r : S)) _ _
      (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)
algInst : Algebra R S := f.toAlgebra
refine : ∀ (r : (↑s : Type u_4)), Module.Flat R (Localization.Away (↑r : S))
⊢ f.Flat

Tactic:
refine Module.flat_of_isLocalized_span _ _ s hsp _
    (fun r ↦ Algebra.linearMap S <| Localization.Away r.1) ?_

Premises used: Localization.Away, Module.flat_of_isLocalized_span, Algebra.linearMap, Subtype.val
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hsp : Eq (α := Ideal S) (Ideal.span s) ⊤
h : ∀ (r : (↑s : Type u_4)), Module.Flat R (Localization.Away (↑r : S))
algInst : Algebra R S := f.toAlgebra
⊢ ∀ (r : (↑s : Type u_4)), Module.Flat R (Localization.Away (↑r : S))

Tactic:
h
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hsp : Eq (α := Ideal S) (Ideal.span s) ⊤
h : ∀ (r : (↑s : Type u_4)), Module.Flat R (Localization.Away (↑r : S))
algInst : Algebra R S := f.toAlgebra
h₁ :
  ∀ (a : (↑s : Type u_4)),
    Eq.{u_4 + 1} (α := Module R (Localization.Away (↑a : S)))
      (OreLocalization.instModuleOfIsScalarTower : Module R (OreLocalization (Submonoid.powers (↑a : S)) S))
      Algebra.toModule
⊢ ∀ (r : (↑s : Type u_4)), Module.Flat R (Localization.Away (↑r : S))

Tactic:
convert! h
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hsp : Eq (α := Ideal S) (Ideal.span s) ⊤
h : ∀ (r : (↑s : Type u_4)), Module.Flat R (Localization.Away (↑r : S))
algInst : Algebra R S := f.toAlgebra
a : (↑s : Type u_4)
h₁ : ∀ (x : R) (x_1 : OreLocalization (Submonoid.powers (↑a : S)) S), SMul.smul x x_1 = SMul.smul x x_1
⊢ Eq.{u_4 + 1} (α := Module R (Localization.Away (↑a : S)))
    (OreLocalization.instModuleOfIsScalarTower : Module R (OreLocalization (Submonoid.powers (↑a : S)) S))
    Algebra.toModule

Tactic:
ext
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hsp : Eq (α := Ideal S) (Ideal.span s) ⊤
h : ∀ (r : (↑s : Type u_4)), Module.Flat R (Localization.Away (↑r : S))
algInst : Algebra R S := f.toAlgebra
a : (↑s : Type u_4)
x : R
x_1 : OreLocalization (Submonoid.powers (↑a : S)) S
⊢ SMul.smul x x_1 = SMul.smul x x_1

Tactic:
apply Algebra.smul_def

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (@fun {R S : Type u_4} [CommRing R] [CommRing S] ↦ (Flat : (f : R →+* S) → Prop))
      (Localization.AtPrime (Ideal.comap f J)) (Localization.AtPrime J) _ _
      (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst : Algebra R S := f.toAlgebra
apply : ∀ (P : Ideal S) [inst_2 : P.IsMaximal], Module.Flat R (Localization.AtPrime P)
⊢ Module.Flat R S

Tactic:
apply Module.flat_of_isLocalized_maximal S S (fun P ↦ Localization.AtPrime P)
    (fun P ↦ Algebra.linearMap S _)

Premises used: Module.flat_of_isLocalized_maximal, Localization.AtPrime, Algebra.linearMap
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (@fun {R S : Type u_4} [CommRing R] [CommRing S] ↦ (Flat : (f : R →+* S) → Prop))
      (Localization.AtPrime (Ideal.comap f J)) (Localization.AtPrime J) _ _
      (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst : Algebra R S := f.toAlgebra
P : Ideal S
_ : ∀ [inst_2 : P.IsMaximal], Module.Flat R (Localization.AtPrime P)
⊢ ∀ [inst_2 : P.IsMaximal], Module.Flat R (Localization.AtPrime P)

Tactic:
_
-- Module: Mathlib.RingTheory.RingHom.Flat
Goal:
R S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
h :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (@fun {R S : Type u_4} [CommRing R] [CommRing S] ↦ (Flat : (f : R →+* S) → Prop))
      (Localization.AtPrime (Ideal.comap f J)) (Localization.AtPrime J) _ _
      (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst : Algebra R S := f.toAlgebra
P : Ideal S
inst_2 : P.IsMaximal
algInst_1 : Algebra (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
  toAlgebra (Localization.localRingHom (Ideal.comap f P) P f ⋯)
⊢ IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)

Tactic:
have : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
    .of_algebraMap_eq fun x ↦ (Localization.localRingHom_to_map _ _ _ rfl x).symm