mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal S
inst✝³ : p.IsPrime
inst✝² : IsArtinianRing R
inst✝¹ : EssFiniteType R S
inst✝ : QuasiFiniteAt R p
this✝⁵ : IsLocalizedModule p.primeCompl LinearMap.id
this✝⁴ : Module.Finite R (Localization.AtPrime p)
this✝³ : Module.Finite S (Localization.AtPrime p)
this✝² : IsArtinianRing (Localization.AtPrime p)
this✝¹ : IsNoetherianRing S
this✝ : Module.FinitePresentation S (Localization.AtPrime p)
r : S
hrp : r ∈ p.primeCompl
H : IsLocalizedModule.Away r (Algebra.linearMap S (Localization.AtPrime p))
this : IsLocalization (Submonoid.powers r) (Localization.AtPrime p)
φ : Localization.Away r ≃ₐ[S] Localization.AtPrime p := ⋯
hrq :
  PrimeSpectrum.comap (algebraMap S (Localization.Away r))
      ((PrimeSpectrum.comapEquiv φ.toRingEquiv).symm (IsLocalRing.closedPoint (Localization.AtPrime p))) ∈
    ↑(PrimeSpectrum.basicOpen r)
⊢ (PrimeSpectrum.comap (algebraMap S (Localization.Away r))
        ((PrimeSpectrum.comapEquiv φ.toRingEquiv).symm (IsLocalRing.closedPoint (Localization.AtPrime p)))).asIdeal =
    { asIdeal := p, isPrime := inst✝³ }.asIdeal

Tactic:
dsimp [-RingEquiv.symm_mk]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal S
inst✝³ : p.IsPrime
inst✝² : IsArtinianRing R
inst✝¹ : EssFiniteType R S
inst✝ : QuasiFiniteAt R p
this✝⁵ : IsLocalizedModule p.primeCompl LinearMap.id
this✝⁴ : Module.Finite R (Localization.AtPrime p)
this✝³ : Module.Finite S (Localization.AtPrime p)
this✝² : IsArtinianRing (Localization.AtPrime p)
this✝¹ : IsNoetherianRing S
this✝ : Module.FinitePresentation S (Localization.AtPrime p)
r : S
hrp : r ∈ p.primeCompl
H : IsLocalizedModule.Away r (Algebra.linearMap S (Localization.AtPrime p))
this : IsLocalization (Submonoid.powers r) (Localization.AtPrime p)
φ : Localization.Away r ≃ₐ[S] Localization.AtPrime p :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (Localization.AtPrime p)
hrq :
  PrimeSpectrum.comap (algebraMap S (Localization.Away r))
      ((PrimeSpectrum.comapEquiv φ.toRingEquiv).symm (IsLocalRing.closedPoint (Localization.AtPrime p))) ∈
    ↑(PrimeSpectrum.basicOpen r)
⊢ Ideal.comap (algebraMap S (Localization.Away r))
      (Ideal.comap (↑φ) (IsLocalRing.closedPoint (Localization.AtPrime p)).asIdeal) =
    p
Module: Mathlib.RingTheory.Etale.Basic

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
⊢ FormallyEtale R S ↔ IsIdempotentElem (RingHom.ker (algebraMap R S))

Tactic:
FormallyEtale.iff_formallyUnramified_and_formallySmooth,

Goal state after:
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
⊢ FormallyUnramified R S ∧ FormallySmooth R S ↔ IsIdempotentElem (RingHom.ker (algebraMap R S))
Module: Mathlib.RingTheory.Etale.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ autoParam (FormallyEtale R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam ↔
    FormallyUnramified R A ∧ Smooth R A

Tactic:
FormallyEtale.iff_formallyUnramified_and_formallySmooth,

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ autoParam (FormallyUnramified R A ∧ FormallySmooth R A) formallyEtale._autoParam ∧
      autoParam (FinitePresentation R A) finitePresentation._autoParam ↔
    FormallyUnramified R A ∧ Smooth R A
Module: Mathlib.RingTheory.Etale.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.FormallyEtale
hg : g.FormallyEtale
⊢ (g.comp f).FormallyEtale

Tactic:
algebraize [f, g, g.comp f]
  exact Algebra.FormallyEtale.comp R S T

Goal state after:
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
P₁ : Extension R A
P₂ : Extension R A
f : P₁.Hom P₂
inst✝¹ : FormallySmooth R P₁.Ring
inst✝ : FormallySmooth R P₂.Ring
⊢ ↑(equivOfFormallySmooth P₁ P₂) = map f

Tactic:
ext1 x
  refine (LinearEquiv.symm_apply_eq _).mpr ?_
  change ((map (P₁.homInfinitesimal P₂)).restrictScalars A ∘ₗ map P₁.toInfinitesimal) x =
    ((map P₂.toInfinitesimal).restrictScalars A ∘ₗ map f) x
  rw [← map_comp, ← map_comp, map_eq]

Goal state after:
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: case mpr
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
P : Extension R A
inst✝ : FormallySmooth R P.Ring
e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent := ⋯
⊢ (∃ l, l ∘ₗ P.cotangentComplex = LinearMap.id) → ∃ l, l ∘ₗ kerCotangentToTensor R P.Ring A = LinearMap.id

Tactic:
· intro ⟨l, hl⟩
    exact ⟨e.symm.toLinearMap ∘ₗ l.restrictScalars P.Ring,
      LinearMap.ext (DFunLike.congr_fun hl : _)⟩

Goal state after:
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
⊢ Function.Surjective ⇑(Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom)

Tactic:
by
  rw [← fst_compEquiv]
  exact (Prod.fst_surjective).comp (compEquiv Q P).surjective

Goal state after:
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: case refine_2
R✝ : Type u
A✝ : Type v
inst✝¹⁴ : CommRing R✝
inst✝¹³ : CommRing A✝
inst✝¹² : Algebra R✝ A✝
B✝ : Type u_1
P : Type u_2
C✝ : Type u_3
inst✝¹¹ : CommRing B✝
inst✝¹⁰ : Algebra R✝ B✝
inst✝⁹ : CommRing C✝
inst✝⁸ : Algebra R✝ C✝
inst✝⁷ : CommRing P
inst✝⁶ : Algebra R✝ P
R : Type u_4
inst✝⁵ : CommRing R
A : Type u_5
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type u_6
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
C : Type (max u_5 u_6)
x✝¹ : CommRing C
x✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this✝ : Algebra R C := ((algebraMap B C).comp (algebraMap R B)).toAlgebra
this : IsScalarTower R B C
b : B
a : A
⊢ (AlgHom.restrictScalars R
        ((Ideal.Quotient.mkₐ B I).comp
          (TensorProduct.productLeftAlgHom (ofId B C)
            (lift I ⋯ ((AlgHom.restrictScalars R f).comp TensorProduct.includeRight)))))
      (b ⊗ₜ[R] a) =
    (AlgHom.restrictScalars R f) (b ⊗ₜ[R] a)

Tactic:
suffices algebraMap B _ b * f (1 ⊗ₜ[R] a) = f (b ⊗ₜ[R] a) by simpa [Algebra.ofId_apply]

Goal state after:
case refine_2
R✝ : Type u
A✝ : Type v
inst✝¹⁴ : CommRing R✝
inst✝¹³ : CommRing A✝
inst✝¹² : Algebra R✝ A✝
B✝ : Type u_1
P : Type u_2
C✝ : Type u_3
inst✝¹¹ : CommRing B✝
inst✝¹⁰ : Algebra R✝ B✝
inst✝⁹ : CommRing C✝
inst✝⁸ : Algebra R✝ C✝
inst✝⁷ : CommRing P
inst✝⁶ : Algebra R✝ P
R : Type u_4
inst✝⁵ : CommRing R
A : Type u_5
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type u_6
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
C : Type (max u_5 u_6)
x✝¹ : CommRing C
x✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this✝ : Algebra R C := ((algebraMap B C).comp (algebraMap R B)).toAlgebra
this : IsScalarTower R B C
b : B
a : A
⊢ (algebraMap B (C ⧸ I)) b * f (1 ⊗ₜ[R] a) = f (b ⊗ₜ[R] a)
Module: Mathlib.RingTheory.Unramified.Locus

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : FiniteType R A
p : Ideal A
inst✝¹ : p.IsPrime
inst✝ : IsUnramifiedAt R p
⊢ ∃ f ∉ p, Unramified R (Localization.Away f)

Tactic:
obtain ⟨f, hfp, H⟩ := exists_formallyUnramified_of_isUnramifiedAt (R := R) p
  exact ⟨f, hfp, ⟨H, .trans ‹_› (IsLocalization.finiteType_of_monoid_fg (.powers f) _)⟩⟩

Goal state after:
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : (Q.comp P).Ring
⊢ (δAux R Q) ((Q.ofComp P).toAlgHom x) =
    (LinearMap.baseChange T P.toExtension.toKaehler)
      ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) x)).2

Tactic:
let : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
  have : IsScalarTower (Q.comp P).Ring (Q.comp P).Ring T := IsScalarTower.left _
  induction x using MvPolynomial.induction_on with
  | C s =>
    simp only [algHom_C, δAux_C, derivation_C, Derivation.map_algebraMap,
      tmul_zero, map_zero, MvPolynomial.algebraMap_apply, Prod.snd_zero]
  | add x₁ x₂ hx₁ hx₂ =>
    simp only [map_add, hx₁, hx₂, tmul_add, Prod.snd_add]
  | mul_X p n IH =>
    simp only [map_mul, Hom.toAlgHom_X, ofComp_val, δAux_mul,
      ← @IsScalarTower.algebraMap_smul Q.Ring T, algebraMap_apply, Hom.algebraMap_toAlgHom,
      algebraMap_self, map_aeval, RingHomCompTriple.comp_eq, comp_val, RingHom.id_apply,
      IH, Derivation.leibniz, tmul_add, tmul_smul, ← cotangentSpaceBasis_apply, coe_eval₂Hom,
      ← @IsScalarTower.algebraMap_smul (Q.comp P).Ring T, aeval_X, map_smul, Prod.snd_add,
      Prod.smul_snd, map_add]
    obtain (n | n) := n
    · simp only [Sum.elim_inl, δAux_X, smul_zero, aeval_X,
        CotangentSpace.compEquiv, LinearEquiv.trans_apply, Basis.repr_symm_apply, zero_add,
        Basis.repr_self, Finsupp.linearCombination_single, Basis.prod_apply, LinearMap.coe_inl,
        LinearMap.coe_inr, Function.comp_apply, one_smul, map_zero]
    · simp only [Sum.elim_inr, Function.comp_apply, algHom_C, δAux_C,
        CotangentSpace.compEquiv, LinearEquiv.trans_apply, Basis.repr_symm_apply,
        algebraMap_smul, Basis.repr_self, Finsupp.linearCombination_single, Basis.prod_apply,
        LinearMap.coe_inr, Basis.baseChange_apply, one_smul, LinearMap.baseChange_tmul,
        toKaehler_cotangentSpaceBasis, add_left_inj, LinearMap.coe_inl]
      rfl

Goal state after:
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
⊢ Nontrivial L

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
f : W.Hom Q
⊢ Function.Exact ⇑(Extension.H1Cotangent.map f.toExtensionHom ∘ₗ ↑(equiv (Q.comp P) W)) ⇑(δ Q P)

Tactic:
change Function.Exact ((Extension.H1Cotangent.map f.toExtensionHom).restrictScalars T ∘ₗ
    (Extension.H1Cotangent.map _)) (δ Q P)

Goal state after:
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
f : W.Hom Q
⊢ Function.Exact
    ⇑(↑T (Extension.H1Cotangent.map f.toExtensionHom) ∘ₗ
        Extension.H1Cotangent.map ((Q.comp P).defaultHom W).toExtensionHom)
    ⇑(δ Q P)
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : EssFiniteType R S
p : Ideal R
inst✝⁴ : p.IsPrime
q : Ideal S
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
this : EssFiniteType (Localization.AtPrime p) (Localization.AtPrime q)
⊢ Ideal.map (Localization.localRingHom p q (algebraMap R S) ⋯) (Ideal.map (algebraMap R (Localization.AtPrime p)) p) =
    Ideal.map (algebraMap R (Localization.AtPrime q)) p

Tactic:
Ideal.map_map,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : EssFiniteType R S
p : Ideal R
inst✝⁴ : p.IsPrime
q : Ideal S
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
this : EssFiniteType (Localization.AtPrime p) (Localization.AtPrime q)
⊢ Ideal.map ((Localization.localRingHom p q (algebraMap R S) ⋯).comp (algebraMap R (Localization.AtPrime p))) p =
    Ideal.map (algebraMap R (Localization.AtPrime q)) p
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: case hxt
S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : q.IsPrime
inst✝ : Module.Finite R S
p : Ideal R := under R q
Sq : Type u_1 := Localization.AtPrime q
r : PrimeSpectrum (p.Fiber S) := (PrimeSpectrum.primesOverOrderIsoFiber R S p) (primesOver.mk p q)
this✝¹ : q = comap Algebra.TensorProduct.includeRight r.asIdeal
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime (comap Algebra.TensorProduct.includeRight r.asIdeal)) :=
  Localization.AtPrime.algebraOfLiesOver p (comap Algebra.TensorProduct.includeRight r.asIdeal)
this : IsArtinianRing (Sq ⧸ map (algebraMap R Sq) p)
⊢ Module.length (Sq ⧸ map (algebraMap R Sq) p)
      (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R q)) ≠
    ⊤

Tactic:
Module.length_ne_top_iff,

Goal state after:
case hxt
S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : q.IsPrime
inst✝ : Module.Finite R S
p : Ideal R := under R q
Sq : Type u_1 := Localization.AtPrime q
r : PrimeSpectrum (p.Fiber S) := (PrimeSpectrum.primesOverOrderIsoFiber R S p) (primesOver.mk p q)
this✝¹ : q = comap Algebra.TensorProduct.includeRight r.asIdeal
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime (comap Algebra.TensorProduct.includeRight r.asIdeal)) :=
  Localization.AtPrime.algebraOfLiesOver p (comap Algebra.TensorProduct.includeRight r.asIdeal)
this : IsArtinianRing (Sq ⧸ map (algebraMap R Sq) p)
⊢ IsFiniteLength (Sq ⧸ map (algebraMap R Sq) p)
    (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R q))
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : q.IsPrime
p : Ideal R := under R q
f₀ : S ≃ₐ[R] S := (MulSemiringAction.toAlgAut G R S) g
hg : g • q = map f₀ q
Sq : Type u_2 := Localization.AtPrime q
Sq' : Type u_2 := Localization.AtPrime (map f₀ q)
f : Sq ≃ₐ[R] Sq' := Localization.localAlgEquiv q (map f₀ q) f₀ ⋯
this✝ : Algebra Sq Sq' := f.toRingEquiv.toRingHom.toAlgebra
this : IsScalarTower R Sq Sq'
⊢ map ((algebraMap Sq Sq').comp (algebraMap R Sq)) p =
    map (↑(AlgEquiv.ofBijective (Algebra.ofId Sq Sq') ⋯)) (map (algebraMap R Sq) p)

Tactic:
Ideal.map_map,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : q.IsPrime
p : Ideal R := under R q
f₀ : S ≃ₐ[R] S := (MulSemiringAction.toAlgAut G R S) g
hg : g • q = map f₀ q
Sq : Type u_2 := Localization.AtPrime q
Sq' : Type u_2 := Localization.AtPrime (map f₀ q)
f : Sq ≃ₐ[R] Sq' := Localization.localAlgEquiv q (map f₀ q) f₀ ⋯
this✝ : Algebra Sq Sq' := f.toRingEquiv.toRingHom.toAlgebra
this : IsScalarTower R Sq Sq'
⊢ map ((algebraMap Sq Sq').comp (algebraMap R Sq)) p =
    map ((↑(AlgEquiv.ofBijective (Algebra.ofId Sq Sq') ⋯)).comp (algebraMap R Sq)) p
Module: Mathlib.Data.DFinsupp.Encodable

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : Countable ι
inst✝ : ∀ (i : ι), Countable (α i)
x✝¹ : Encodable ι := Encodable.ofCountable ι
x✝ : (i : ι) → Encodable (α i) := fun i ↦ Encodable.ofCountable (α i)
⊢ Countable (Π₀ (i : ι), α i)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
n : ℕ
n0 : n > 0
y : ℝ
yS : y ∈ s
hy : ↑(f n) ≤ y * ↑n
⊢ ↑(↑(f n) / ↑n) ≤ y

Tactic:
by simpa using (div_le_iff₀ (Nat.cast_pos.2 n0 : (_ : ℝ) < _)).2 hy

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ Zero ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ One ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ Add ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ Sub ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ Mul ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ Inv ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ Div ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ LE ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ Bot ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ Inhabited ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ Nontrivial ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
⊢ CommSemiring ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
⊢ Algebra ℝ≥0 ℝ

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
⊢ DistribMulAction ℝ≥0ˣ ℝ

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
⊢ MonoidWithZero ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
⊢ CommMonoidWithZero ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
⊢ CommGroupWithZero ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ LinearOrder ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ OrderBot ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ PartialOrder ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ AddCommMonoid ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ IsOrderedAddMonoid ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ DistribLattice ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ SemilatticeInf ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ SemilatticeSup ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ Semiring ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ CommMonoid ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ LinearOrderedCommMonoidWithZero ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ DenselyOrdered ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r r₁ r₂ : ℝ≥0
x y : ℝ
ι : Type u_1
f : ι → ℝ
⊢ NoMaxOrder ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℝ
⊢ IsEmpty ι

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case neg
s : Set ℝ
hn : s.Nonempty
hb : ¬BddBelow s
⊢ sSup (-s) = -sInf s

Tactic:
csInf_of_not_bddBelow hb,

Goal state after:
case neg
s : Set ℝ
hn : s.Nonempty
hb : ¬BddBelow s
⊢ sSup (-s) = -sInf ∅
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ OrderedSub ℝ≥0

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r p : ℝ≥0
h : p ≠ 0
⊢ p * r ≤ 1 ↔ r * p ≤ 1

Tactic:
mul_comm

Goal state after:
r p : ℝ≥0
h : p ≠ 0
⊢ r * p ≤ 1 ↔ r * p ≤ 1
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r p : ℝ≥0
h : p ≠ 0
⊢ p * r < 1 ↔ r * p < 1

Tactic:
mul_comm

Goal state after:
r p : ℝ≥0
h : p ≠ 0
⊢ r * p < 1 ↔ r * p < 1
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r p : ℝ≥0
h : p ≠ 0
⊢ r < p⁻¹ ↔ r * p < 1

Tactic:
by
  rw [← mul_lt_mul_iff_right₀ (pos_iff_ne_zero.2 h), mul_inv_cancel₀ h, mul_comm]

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_2
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
⊢ ⨅ q, f ↑↑q ≤ f ↑q

Tactic:
have hq := q.prop

Goal state after:
case refine_2
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : ↑q ∈ Ioi x
⊢ ⨅ q, f ↑↑q ≤ f ↑q
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : R
h : ∀ (i : HeightOneSpectrum R), ¬i.maxPowDividing I = ⊤ → x ∈ i.maxPowDividing I
i : HeightOneSpectrum R
⊢ x ∈ i.maxPowDividing I

Tactic:
by_cases i.maxPowDividing I = ⊤ <;> simp_all

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
⊢ ⨅ i, i.maxPowDividing I = I

Tactic:
nth_rw 2 [← Ideal.finprod_heightOneSpectrum_factorization h0]
  classical
  rw [finprod_def, dif_pos (Ideal.hasFiniteMulSupport h0), Ideal.prod_eq_iInf_of_pairwise_isCoprime]
  · ext x
    constructor
    · aesop
    · simp only [Finite.mem_toFinset, mem_mulSupport, one_eq_top, ne_eq, Submodule.mem_iInf]
      intro h i
      by_cases i.maxPowDividing I = ⊤ <;> simp_all
  · intro x hx y hy hxy
    apply IsDedekindDomain.HeightOneSpectrum.isCoprime_pow_of_ne _ _ hxy

Goal state after: