mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: case pos
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp : map f p ≠ ⊥
hP : P.IsPrime
hP₂ : P = ⊥
⊢ p.ramificationIdx' 0 = multiplicity 0 (map f p)

Tactic:
multiplicity_zero_eq_zero_of_ne_zero _ hp

Goal state after:
case pos
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp : map f p ≠ ⊥
hP : P.IsPrime
hP₂ : P = ⊥
⊢ p.ramificationIdx' 0 = 0
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type v
inst✝⁶ : CommRing R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : Small.{w, u} A
H :
  ∀ ⦃B : Type w⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
B : Type u
inst✝² : CommRing B
inst✝¹ : Small.{w, u} B
inst✝ : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
f g : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = (Ideal.Quotient.mkₐ R I).comp g
⊢ Ideal.comap (Shrink.ringEquiv B) I ^ 2 = ⊥

Tactic:
rw [← Ideal.map_symm, ← Ideal.map_pow, hI]

Goal state after:
R : Type v
inst✝⁶ : CommRing R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : Small.{w, u} A
H :
  ∀ ⦃B : Type w⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
B : Type u
inst✝² : CommRing B
inst✝¹ : Small.{w, u} B
inst✝ : Algebra R B
I : Ideal B
hI : I ^ 2 = ⊥
f g : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = (Ideal.Quotient.mkₐ R I).comp g
⊢ Ideal.map (Shrink.ringEquiv B).symm ⊥ = ⊥
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: case mpr.refine_2
R : Type v
inst✝³ : CommRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Small.{w, u} A
H :
  ∀ ⦃B : Type u⦄ [inst : CommRing B] [Small.{w, u} B] [inst_2 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
h : Nontrivial Ω[A⁄R]
f₁ f₂ : { f // (TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R A }
e : f₁ ≠ f₂
f : Ideal (A ⊗[R] A ⧸ RingHom.ker (TensorProduct.lmul' R).toRingHom ^ 2) :=
  RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom
⊢ (Ideal.Quotient.mkₐ R (RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom)).comp ↑f₁ =
    (Ideal.Quotient.mkₐ R (RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom)).comp ↑f₂

Tactic:
ext x
      apply RingHom.kerLift_injective (TensorProduct.lmul' R (S := A)).kerSquareLift.toRingHom
      simpa using DFunLike.congr_fun (f₁.2.trans f₂.2.symm) x

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

Goal state before:
pp: case mp.refine_1
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
e : S ⊗[R] S
he₁ : IsIdempotentElem e
he₂ : Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Ideal.span {e}
s : S
x : S ⊗[R] S
hx : 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1 = e * x
⊢ (1 - e) * e * x = 0

Tactic:
sub_mul,

Goal state after:
case mp.refine_1
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
e : S ⊗[R] S
he₁ : IsIdempotentElem e
he₂ : Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Ideal.span {e}
s : S
x : S ⊗[R] S
hx : 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1 = e * x
⊢ (1 * e - e * e) * x = 0
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: case h.right
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
t e : S ⊗[R] S
ht₁ : ∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * (1 - e) = 0
ht₂ : e ∈ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
⊢ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = S ⊗[R] S ∙ e

Tactic:
apply le_antisymm <;> simp only [Ideal.submodule_span_eq, Ideal.mem_span_singleton, ht₂,
        Ideal.span_le, Set.singleton_subset_iff, SetLike.mem_coe, Set.range_subset_iff]

Goal state after:
case h.right.a
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
t e : S ⊗[R] S
ht₁ : ∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * (1 - e) = 0
ht₂ : e ∈ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
⊢ ∀ (y : S), e ∣ 1 ⊗ₜ[R] y - y ⊗ₜ[R] 1
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
⊢ ∑ i ∈ f.support, 1 ⊗ₜ[R] x * f i ⊗ₜ[R] b i =
    ∑ k ∈ f.support.biUnion fun i ↦ ((fun i ↦ b.repr (b i * x)) i).support,
      (b.repr (f.sum fun i y ↦ ((fun i ↦ b.repr (b i * x)) i) k • y)).sum fun j c ↦ c • b j ⊗ₜ[R] b k

Tactic:
let a i := b.repr (b i * x)

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
⊢ ∑ i ∈ f.support, 1 ⊗ₜ[R] x * f i ⊗ₜ[R] b i =
    ∑ k ∈ f.support.biUnion fun i ↦ ((fun i ↦ b.repr (b i * x)) i).support,
      (b.repr (f.sum fun i y ↦ ((fun i ↦ b.repr (b i * x)) i) k • y)).sum fun j c ↦ c • b j ⊗ₜ[R] b k
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
r : S
m : M
this : (1 ⊗ₜ[R] r - r ⊗ₜ[R] 1) * elem R S = 0
⊢ (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (1 ⊗ₜ[R] r * elem R S) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (elem R S)

Tactic:
sub_mul,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
r : S
m : M
this : 1 ⊗ₜ[R] r * elem R S - r ⊗ₜ[R] 1 * elem R S = 0
⊢ (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (1 ⊗ₜ[R] r * elem R S) =
    r • (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (elem R S)
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case h2
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
hx' : x ∈ (Q.comp P).toExtension.ker
hx :
  (Q.ofComp P).toAlgHom x ∈
    Ideal.map (Q.ofComp P).toAlgHom (Q.comp P).ker * Ideal.map (Q.ofComp P).toAlgHom (Q.comp P).ker
⊢ Extension.Cotangent.mk ⟨x, hx'⟩ ∈
    (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)).range

Tactic:
← Ideal.map_mul,

Goal state after:
case h2
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
hx' : x ∈ (Q.comp P).toExtension.ker
hx : (Q.ofComp P).toAlgHom x ∈ Ideal.map (Q.ofComp P).toAlgHom ((Q.comp P).ker * (Q.comp P).ker)
⊢ Extension.Cotangent.mk ⟨x, hx'⟩ ∈
    (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)).range
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case h2.refine_1
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
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
w : P.Ring
hw : w ∈ P.ker
⊢ (algebraMap S T) ((aeval P.val) w) = 0

Tactic:
rw [aeval_val_eq_zero hw, map_zero]

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✝² : Algebra.IsSeparable K L
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
hI : I ^ 2 = ⊥
f₁ f₂ : L →ₐ[K] B
e : (Ideal.Quotient.mkₐ K I).comp f₁ = (Ideal.Quotient.mkₐ K I).comp f₂
x : L
this✝ : f₁ x - f₂ x ∈ I
this : f₂ ((aeval x) (derivative (minpoly K x))) * (f₁ x - f₂ x) = 0
⊢ f₁ x = f₂ x

Tactic:
((isUnit_iff_ne_zero.mpr
    ((Algebra.IsSeparable.isSeparable K x).aeval_derivative_ne_zero
      (minpoly.aeval K x))).map f₂).mul_right_eq_zero,

Goal state after:
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra.IsSeparable K L
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
hI : I ^ 2 = ⊥
f₁ f₂ : L →ₐ[K] B
e : (Ideal.Quotient.mkₐ K I).comp f₁ = (Ideal.Quotient.mkₐ K I).comp f₂
x : L
this✝ : f₁ x - f₂ x ∈ I
this : f₁ x - f₂ x = 0
⊢ f₁ x = f₂ x
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₂
σ' : Type w₄
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
Q' : Generators S T ι'
P' : Generators R S σ'
W : Generators R T τ
⊢ Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom ∘ₗ (Q.comp P).toExtension.cotangentComplex =
    Q.toExtension.cotangentComplex ∘ₗ Extension.Cotangent.map (Q.ofComp P).toExtensionHom

Tactic:
by ext; exact Extension.CotangentSpace.map_cotangentComplex (ofComp Q P).toExtensionHom _

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.ker
hx : Extension.Cotangent.mk x ∈ Q.toExtension.cotangentComplex.ker
y : (Q.comp P).toExtension.Cotangent := Extension.Cotangent.mk (Q.kerCompPreimage P x)
⊢ (δ Q P) ⟨Extension.Cotangent.mk x, hx⟩ = (δAux R Q) ↑x

Tactic:
have hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x := by
    simp only [y, Extension.Cotangent.map_mk]
    congr
    exact ofComp_kerCompPreimage Q P x

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₂
Q : Generators S T ι
P : Generators R S σ
x : ↥Q.ker
hx : Extension.Cotangent.mk x ∈ Q.toExtension.cotangentComplex.ker
y : (Q.comp P).toExtension.Cotangent := Extension.Cotangent.mk (Q.kerCompPreimage P x)
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x
⊢ (δ Q P) ⟨Extension.Cotangent.mk x, hx⟩ = (δAux R Q) ↑x
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
this✝¹ : Module.Finite K L
this✝ : FormallyUnramified (↥(separableClosure K L)) L
this : EssFiniteType (↥(separableClosure K L)) L
x✝ : L
⊢ x✝ ∈ separableClosure K L ↔ x✝ ∈ ⊤

Tactic:
rw [← range_eq_top_of_isPurelyInseparable (separableClosure K L) L]

Goal state after:
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
this✝¹ : Module.Finite K L
this✝ : FormallyUnramified (↥(separableClosure K L)) L
this : EssFiniteType (↥(separableClosure K L)) L
x✝ : L
⊢ x✝ ∈ separableClosure K L ↔ x✝ ∈ (algebraMap (↥(separableClosure K L)) L).range
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : Q.Ring
y : ↥P.ker
this✝¹ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
⊢ (tensorCotangentInvFun f halg H) (x • Cotangent.mk ⟨f.toRingHom ↑y, ⋯⟩) = x • 1 ⊗ₜ[S] Cotangent.mk y

Tactic:
trans tensorCotangentInvFun f halg H (.mk ((f.mapKer halg).liftBaseChange Q.Ring (x ⊗ₜ y)))

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : Q.Ring
y : ↥P.ker
this✝¹ : Algebra P.Ring T := ⋯
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker := ⋯
⊢ (tensorCotangentInvFun f halg H) (x • Cotangent.mk ⟨f.toRingHom ↑y, ⋯⟩) =
    (tensorCotangentInvFun f halg H) (Cotangent.mk ((LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) (x ⊗ₜ[P.Ring] y)))

R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : Algebra S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : Q.Ring
y : ↥P.ker
this✝¹ : Algebra P.Ring T := ⋯
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker := ⋯
⊢ (tensorCotangentInvFun f halg H) (Cotangent.mk ((LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) (x ⊗ₜ[P.Ring] y))) =
    x • 1 ⊗ₜ[S] Cotangent.mk y
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
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
hq : p.primesOver S = {q}
inst✝¹ : Module.Finite R S
inst✝ : q.LiesOver p
hRS : (RingHom.ker (algebraMap R S)).FG
H : Function.Bijective ⇑(localRingHom p q (algebraMap R S) ⋯)
⊢ ∃ r ∉ p, ∀ (r' : R), r ∣ r' → Function.Bijective ⇑(awayMap (algebraMap R S) r')

Tactic:
obtain ⟨s, hs⟩ := Algebra.FiniteType.out (R := R) (A := S)
  have (x : S) : ∃ a, ∃ b ∉ p, algebraMap R S a = x * algebraMap R S b := by
    have := (IsLocalization.mk'_surjective p.primeCompl).exists.mp (H.2 (algebraMap _ _ x))
    simp only [localRingHom_mk', Prod.exists, Subtype.exists, Ideal.mem_primeCompl_iff,
      IsLocalization.mk'_eq_iff_eq_mul, exists_prop, ← map_mul,
      IsLocalization.eq_iff_exists q.primeCompl] at this
    obtain ⟨a, b, hbp, c, hcq, hc⟩ := this
    obtain ⟨d, hd, e, he⟩ := Ideal.exists_notMem_dvd_algebraMap_of_primesOver_eq_singleton hq _ hcq
    exact ⟨d * a, d * b, ‹p.IsPrime›.mul_notMem hd hbp, by grind⟩
  choose a b hbp e using this
  obtain ⟨r, hrp, hr⟩ := Localization.exists_awayMap_injective_of_localRingHom_injective hRS H.1
  refine ⟨r * ∏ i ∈ s, b i, mul_mem (s := p.primeCompl) hrp (prod_mem fun _ _ ↦ hbp _), ?_⟩
  refine fun r' hr' ↦ ⟨hr _ (.trans ⟨_, rfl⟩ hr'), ?_⟩
  have H : (IsScalarTower.toAlgHom R S _).range ≤ (awayMapₐ (Algebra.ofId R S) r').range := by
    rw [← Algebra.map_top, Subalgebra.map_le, ← hs, Algebra.adjoin_le_iff]
    intro x hxs
    obtain ⟨r'', hr'⟩ := hr'
    refine ⟨IsLocalization.mk' (M := .powers r') _
      (r'' * r * (∏ i ∈ s.erase x, b i) * a x) ⟨_, 1, rfl⟩, ?_⟩
    dsimp [awayMapₐ, IsLocalization.Away.map]
    simp only [pow_one, IsLocalization.map_mk', IsLocalization.mk'_eq_iff_eq_mul,
      ← map_mul (algebraMap S _), map_mul (algebraMap R _), e]
    congr 1
    rw [hr', ← Finset.prod_erase_mul s b hxs, map_mul, map_mul, map_mul]
    ring_nf
  intro x
  obtain ⟨x, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.exists_mk'_eq (.powers (algebraMap R S r')) x
  obtain ⟨y, hy : awayMap _ _ _ = _⟩ := H ⟨x, rfl⟩
  dsimp at hy
  refine ⟨y * Localization.Away.invSelf _ ^ n, ?_⟩
  simp only [map_mul, hy]
  simp [Away.invSelf, Localization.mk_eq_mk', awayMap, IsLocalization.Away.map,
    IsLocalization.map_mk', ← Algebra.smul_def, IsLocalization.smul_mk', ← IsLocalization.mk'_pow]

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
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
n : ℕ
n0 : n > 0
y : ℝ
yS : y ∈ s
this : y * ↑n - 1 < ↑(f n)
⊢ (y - (↑n)⁻¹) * ↑n < ↑(f n)

Tactic:
sub_mul,

Goal state after:
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
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
n : ℕ
n0 : n > 0
y : ℝ
yS : y ∈ s
this : y * ↑n - 1 < ↑(f n)
⊢ y * ↑n - (↑n)⁻¹ * ↑n < ↑(f n)
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
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
n : ℕ
n0 : n > 0
y : ℝ
yS : y ∈ s
this : y * ↑n - 1 < ↑(f n)
⊢ y * ↑n - (↑n)⁻¹ * ↑n < ↑(f n)

Tactic:
inv_mul_cancel₀

Goal state after:
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
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
n : ℕ
n0 : n > 0
y : ℝ
yS : y ∈ s
this : y * ↑n - 1 < ↑(f n)
⊢ y * ↑n - 1 < ↑(f n)

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
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
n : ℕ
n0 : n > 0
y : ℝ
yS : y ∈ s
this : y * ↑n - 1 < ↑(f n)
⊢ ↑n ≠ 0
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
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
⊢ IsCauSeq abs fun n ↦ ↑(f n) / ↑n

Tactic:
intro ε ε0

Goal state after:
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
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
⊢ ∃ i, ∀ j ≥ i, |(fun n ↦ ↑(f n) / ↑n) j - (fun n ↦ ↑(f n) / ↑n) i| < ε
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case mp
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → sInf s < a + ε
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ x ∈ s, x < a + ε

Tactic:
exact exists_lt_of_csInf_lt h' (H ε ε_pos)

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

Goal state before:
pp: case neg
s : Set ℝ
hn : s.Nonempty
hb : ¬BddBelow s
⊢ 0 = -0

Tactic:
neg_zero

Goal state after:
case neg
s : Set ℝ
hn : s.Nonempty
hb : ¬BddBelow s
⊢ 0 = 0
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: ⊢ ⋂ r, Iic ↑r = ∅

Tactic:
exact iInter_Iic_eq_empty_iff.mpr not_bddBelow_coe

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

Goal state before:
pp: a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : 1 < ↑q
⊢ 1 ≤ (↑q - 1) * ↑q.den

Tactic:
sub_mul,

Goal state after:
a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : 1 < ↑q
⊢ 1 ≤ ↑q * ↑q.den - 1 * ↑q.den
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s t : Set α
⊢ Disjoint (s.ordT5Nhd t) (t.ordT5Nhd s)

Tactic:
rw [disjoint_iff_inf_le]

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
⊢ s.ordT5Nhd t ⊓ t.ordT5Nhd s ⊆ ⊥
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x : α
hx₂ : x ∈ t.ordT5Nhd s
a : α
has : a ∈ s
ha : x ∈ (tᶜ ∩ (s.ordSeparatingSet t).ordConnectedSectionᶜ).ordConnectedComponent a
b : α
hbt : b ∈ t
hb : x ∈ (sᶜ ∩ (t.ordSeparatingSet s).ordConnectedSectionᶜ).ordConnectedComponent b
⊢ x ∈ ⊥

Tactic:
clear hx₂

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
ha : x ∈ (tᶜ ∩ (s.ordSeparatingSet t).ordConnectedSectionᶜ).ordConnectedComponent a
b : α
hbt : b ∈ t
hb : x ∈ (sᶜ ∩ (t.ordSeparatingSet s).ordConnectedSectionᶜ).ordConnectedComponent b
⊢ x ∈ ⊥
Module: Mathlib.Topology.Order.T5

Goal state before:
pp: case neg
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
H : ¬Disjoint (Icc a b) (s.ordSeparatingSet t).ordConnectedSection
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a

Tactic:
simp only [Set.disjoint_left, not_forall, Classical.not_not] at H
    rcases H with ⟨c, ⟨hac, hcb⟩, hc⟩
    have hsub' : Icc a b ⊆ ordConnectedComponent tᶜ a :=
      subset_ordConnectedComponent (left_mem_Icc.2 hab) hsub
    have hd : Disjoint s (ordConnectedSection (ordSeparatingSet s t)) :=
      disjoint_left_ordSeparatingSet.mono_right ordConnectedSection_subset
    replace hac : a < c := hac.lt_of_ne <| Ne.symm <| ne_of_mem_of_not_mem hc <|
      disjoint_left.1 hd ha
    filter_upwards [Ico_mem_nhdsGE hac] with x hx hx'
    refine hx.2.ne (eq_of_mem_ordConnectedSection_of_uIcc_subset hx' hc ?_)
    refine subset_inter (subset_iUnion₂_of_subset a ha ?_) ?_
    · exact OrdConnected.uIcc_subset inferInstance (hsub' ⟨hx.1, hx.2.le.trans hcb⟩)
        (hsub' ⟨hac.le, hcb⟩)
    · rcases mem_iUnion₂.1 (ordConnectedSection_subset hx').2 with ⟨y, hyt, hxy⟩
      refine subset_iUnion₂_of_subset y hyt (OrdConnected.uIcc_subset inferInstance hxy ?_)
      refine subset_ordConnectedComponent left_mem_uIcc hxy ?_
      suffices c < y by
        rw [uIcc_of_ge (hx.2.trans this).le]
        exact ⟨hx.2.le, this.le⟩
      refine lt_of_not_ge fun hyc => ?_
      have hya : y < a := not_le.1 fun hay => hsub ⟨hay, hyc.trans hcb⟩ hyt
      exact hxy (Icc_subset_uIcc ⟨hya.le, hx.1⟩) ha

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : EReal
hx : 0 < x
h'x : x ≠ ⊤
⊢ 0 < x.toReal

Tactic:
by
  lift x to ℝ using by aesop
  simpa using hx

Goal state after: