mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
f₁ : Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] →ₗ[P ⧸ RingHom.ker (algebraMap P S) ^ 2] S ⊗[P] Ω[P⁄R] :=
  (derivationQuotKerSq R P S).liftKaehlerDifferential
f₂ : S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] →ₗ[S] S ⊗[P] Ω[P⁄R] :=
  AlgebraTensorModule.lift
    ((LinearMap.ringLmapEquivSelf S S
          (Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] →ₗ[P ⧸ RingHom.ker (algebraMap P S) ^ 2] S ⊗[P] Ω[P⁄R])).symm
      f₁)
f₃ : Ω[P⁄R] →ₗ[P] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] :=
  KaehlerDifferential.map R R P (P ⧸ RingHom.ker (algebraMap P S) ^ 2)
f₄ : Ω[P⁄R] →ₗ[P] S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] :=
  ↑P ((mk (P ⧸ RingHom.ker (algebraMap P S) ^ 2) S Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R]) 1) ∘ₗ f₃
f₅ : S ⊗[P] Ω[P⁄R] →ₗ[S] S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] :=
  AlgebraTensorModule.lift
    ((LinearMap.ringLmapEquivSelf S S
          (Ω[P⁄R] →ₗ[P] S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R])).symm
      f₄)
⊢ Function.LeftInverse (⇑f₅) f₂.toFun

Tactic:
suffices f₅.comp f₂ = LinearMap.id from LinearMap.congr_fun this

Goal state after:
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
f₁ : Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] →ₗ[P ⧸ RingHom.ker (algebraMap P S) ^ 2] S ⊗[P] Ω[P⁄R] :=
  (derivationQuotKerSq R P S).liftKaehlerDifferential
f₂ : S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] →ₗ[S] S ⊗[P] Ω[P⁄R] :=
  AlgebraTensorModule.lift
    ((LinearMap.ringLmapEquivSelf S S
          (Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] →ₗ[P ⧸ RingHom.ker (algebraMap P S) ^ 2] S ⊗[P] Ω[P⁄R])).symm
      f₁)
f₃ : Ω[P⁄R] →ₗ[P] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] :=
  KaehlerDifferential.map R R P (P ⧸ RingHom.ker (algebraMap P S) ^ 2)
f₄ : Ω[P⁄R] →ₗ[P] S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] :=
  ↑P ((mk (P ⧸ RingHom.ker (algebraMap P S) ^ 2) S Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R]) 1) ∘ₗ f₃
f₅ : S ⊗[P] Ω[P⁄R] →ₗ[S] S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] :=
  AlgebraTensorModule.lift
    ((LinearMap.ringLmapEquivSelf S S
          (Ω[P⁄R] →ₗ[P] S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R])).symm
      f₄)
⊢ f₅ ∘ₗ f₂ = LinearMap.id
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
x : A
⊢ x ∈ IsLocalRing.maximalIdeal A → x ∈ ⊥

Tactic:
hx

Goal state after:
K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
x : A
hx : x ∈ IsLocalRing.maximalIdeal A
⊢ x ∈ ⊥
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : FormallyUnramified K A
inst✝ : EssFiniteType K A
x : A
⊢ IsNilpotent x → x = 0

Tactic:
hx

Goal state after:
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : FormallyUnramified K A
inst✝ : EssFiniteType K A
x : A
hx : IsNilpotent x
⊢ x = 0
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : FormallyUnramified K A
inst✝ : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := ⋯
this : Function.Injective ⇑f
⊢ f x = f 0

Tactic:
map_zero

Goal state after:
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : FormallyUnramified K A
inst✝ : EssFiniteType K A
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this : Function.Injective ⇑f
⊢ f x = 0
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
inst✝¹ : IsScalarTower R S T
inst✝ : Algebra.FormallyEtale S T
x : T ⊗[S] Ω[S⁄R]
⊢ (mapBaseChange R S T) x = 0 → x = 0

Tactic:
hx

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
inst✝¹ : IsScalarTower R S T
inst✝ : Algebra.FormallyEtale S T
x : T ⊗[S] Ω[S⁄R]
hx : (mapBaseChange R S T) x = 0
⊢ x = 0
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
inst✝¹ : IsScalarTower R S T
inst✝ : Algebra.FormallyEtale S T
x : Algebra.H1Cotangent S T
hx : (mapBaseChange R S T) ((Algebra.H1Cotangent.δ R S T) x) = 0
⊢ (Algebra.H1Cotangent.δ R S T) 0 = 0

Tactic:
map_zero

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
inst✝¹ : IsScalarTower R S T
inst✝ : Algebra.FormallyEtale S T
x : Algebra.H1Cotangent S T
hx : (mapBaseChange R S T) ((Algebra.H1Cotangent.δ R S T) x) = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case hz.fst
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
z : T ⊗[S] P.toExtension.CotangentSpace :=
  ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2
⊢ 0 = Q.toExtension.cotangentComplex (Extension.Cotangent.mk x)

Tactic:
hx

Goal state after:
case hz.fst
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
z : T ⊗[S] P.toExtension.CotangentSpace :=
  ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2
⊢ 0 = 0
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
inst✝ : IsScalarTower R 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))
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
f' : ↥Q.ker →ₗ[Q.Ring] T ⊗[S] P.Cotangent :=
  LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk) ∘ₗ ↑e.symm
x : ↥Q.ker
⊢ x ∈ (Q.ker • ⊤).toAddSubgroup → x ∈ (↑f').ker

Tactic:
hx

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
inst✝ : IsScalarTower R 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))
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
f' : ↥Q.ker →ₗ[Q.Ring] T ⊗[S] P.Cotangent :=
  LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk) ∘ₗ ↑e.symm
x : ↥Q.ker
hx : x ∈ (Q.ker • ⊤).toAddSubgroup
⊢ x ∈ (↑f').ker
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
Q : Ideal A
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Ideal.span {p} = RingHom.ker (aeval x).toRingHom
hp₂ : Function.Surjective ⇑(aeval x)
this✝² : FiniteType K A
this✝¹ : Module.Finite K (Localization.AtPrime Q)
this✝ : IsField (Localization.AtPrime Q)
this : Field (Localization.AtPrime Q) := this✝.toField
q : K[X] := minpoly K ((algebraMap A Q.ResidueField) x)
⊢ 0 = (algebraMap (Localization.AtPrime Q) Q.ResidueField) 0

Tactic:
map_zero

Goal state after:
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
Q : Ideal A
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Ideal.span {p} = RingHom.ker (aeval x).toRingHom
hp₂ : Function.Surjective ⇑(aeval x)
this✝² : FiniteType K A
this✝¹ : Module.Finite K (Localization.AtPrime Q)
this✝ : IsField (Localization.AtPrime Q)
this : Field (Localization.AtPrime Q) := this✝.toField
q : K[X] := minpoly K ((algebraMap A Q.ResidueField) x)
⊢ 0 = 0
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: case left
R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.Cotangent
⊢ (map P.toInfinitesimal) x = 0 → x = 0

Tactic:
hx

Goal state after:
case left
R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.Cotangent
hx : (map P.toInfinitesimal) x = 0
⊢ x = 0
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✝¹ : Algebra.IsIntegral R S
inst✝ : FaithfulSMul R S
x : Localization.AtPrime p
⊢ (localRingHom p q (algebraMap R S) ⋯) x = 0 → x = 0

Tactic:
hx

Goal state after:
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✝¹ : Algebra.IsIntegral R S
inst✝ : FaithfulSMul R S
x : Localization.AtPrime p
hx : (localRingHom p q (algebraMap R S) ⋯) x = 0
⊢ x = 0
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case left
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
inst✝¹ : IsScalarTower R 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
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : T ⊗[S] P.H1Cotangent
⊢ (LinearMap.liftBaseChange T (H1Cotangent.map f)) x = 0 → x = 0

Tactic:
hx

Goal state after:
case left
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
inst✝¹ : IsScalarTower R 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
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : T ⊗[S] P.H1Cotangent
hx : (LinearMap.liftBaseChange T (H1Cotangent.map f)) x = 0
⊢ x = 0
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
p : Ideal R
q : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : q.LiesOver p
hq : q.IsPrime
hpS : map (algebraMap R S) p ≠ ⊥
hq' : q ≠ ⊥
this : q.IsMaximal
I : Ideal S
hqI : ¬I ≤ q
h :
  map (algebraMap R (Localization.AtPrime q)) p =
    IsLocalRing.maximalIdeal (Localization q.primeCompl) ^ p.ramificationIdx' q
hSq : IsDiscreteValuationRing (Localization.AtPrime q)
⊢ p.ramificationIdx' q = q.ramificationIdx R

Tactic:
rw [ramificationIdx_eq p q, h, hSq.length_quotient_pow_maximalIdeal, ENat.toNat_natCast]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsPrime
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.QuasiFinite R S
inst✝ : Fintype ↑(p.primesOver S)
this : Fintype (PrimeSpectrum (p.Fiber S)) := Fintype.ofFinite (PrimeSpectrum (p.Fiber S))
q : PrimeSpectrum (p.Fiber S)
a✝ : q ∈ Finset.univ
⊢ (↑((primesOverOrderIsoFiber R S p).symm.toEquiv q)).ramificationIdx R *
      (↑((primesOverOrderIsoFiber R S p).symm.toEquiv q)).inertiaDeg R =
    finrank p.ResidueField (Localization.AtPrime q.asIdeal)

Tactic:
toEquiv_symm,

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsPrime
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.QuasiFinite R S
inst✝ : Fintype ↑(p.primesOver S)
this : Fintype (PrimeSpectrum (p.Fiber S)) := Fintype.ofFinite (PrimeSpectrum (p.Fiber S))
q : PrimeSpectrum (p.Fiber S)
a✝ : q ∈ Finset.univ
⊢ (↑((primesOverOrderIsoFiber R S p).symm q)).ramificationIdx R *
      (↑((primesOverOrderIsoFiber R S p).symm q)).inertiaDeg R =
    finrank p.ResidueField (Localization.AtPrime q.asIdeal)
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
inst✝ : q.LiesOver p
H✝ : Function.Injective ⇑(localRingHom p q (algebraMap R S) ⋯)
s✝ : Finset R
hs : Ideal.span ↑s✝ = RingHom.ker (algebraMap R S)
this : ∀ (x : ↥s✝), (algebraMap R (Localization.AtPrime p)) ↑x = 0
m : ↥s✝ → ↥p.primeCompl
hm : ∀ (x : ↥s✝), ↑(m x) * ↑x = 0
H : RingHom.ker (algebraMap R S) ≤ RingHom.ker (algebraMap R (Away ↑(∏ i, m i)))
r' s : R
e : r' = ↑(∏ i, m i) * s
x : Away r'
⊢ (awayMap (algebraMap R S) r') x = 0 → x = 0

Tactic:
hx

Goal state after:
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
inst✝ : q.LiesOver p
H✝ : Function.Injective ⇑(localRingHom p q (algebraMap R S) ⋯)
s✝ : Finset R
hs : Ideal.span ↑s✝ = RingHom.ker (algebraMap R S)
this : ∀ (x : ↥s✝), (algebraMap R (Localization.AtPrime p)) ↑x = 0
m : ↥s✝ → ↥p.primeCompl
hm : ∀ (x : ↥s✝), ↑(m x) * ↑x = 0
H : RingHom.ker (algebraMap R S) ≤ RingHom.ker (algebraMap R (Away ↑(∏ i, m i)))
r' s : R
e : r' = ↑(∏ i, m i) * s
x : Away r'
hx : (awayMap (algebraMap R S) r') x = 0
⊢ x = 0
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) ⋯)
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
x : S
this : ∃ a, ∃ a_1 ∉ p, ∃ a_2 ∉ q, a_2 * (algebraMap R S) a = a_2 * (x * (algebraMap R S) a_1)
⊢ ∃ a, ∃ b ∉ p, (algebraMap R S) a = x * (algebraMap R S) b

Tactic:
obtain ⟨a, b, hbp, c, hcq, hc⟩ := this

Goal state after:
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) ⋯)
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
x : S
a b : R
hbp : b ∉ p
c : S
hcq : c ∉ q
hc : c * (algebraMap R S) a = c * (x * (algebraMap R S) b)
⊢ ∃ a, ∃ b ∉ p, (algebraMap R S) a = x * (algebraMap R S) b
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
x : HeightOneSpectrum R
⊢ x ∈ ↑(Finite.toFinset ⋯) →
    ∀ ⦃y : HeightOneSpectrum R⦄, y ∈ ↑(Finite.toFinset ⋯) → x ≠ y → (IsCoprime on fun i ↦ i.maxPowDividing I) x y

Tactic:
hx

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : HeightOneSpectrum R
hx : x ∈ ↑(Finite.toFinset ⋯)
⊢ ∀ ⦃y : HeightOneSpectrum R⦄, y ∈ ↑(Finite.toFinset ⋯) → x ≠ y → (IsCoprime on fun i ↦ i.maxPowDividing I) x y
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: x y : ℝ≥0∞
hx : x ≠ ∞
hy : y ≠ ∞
⊢ x.toNNReal = y.toNNReal ↔ x = y

Tactic:
by
  simp only [ENNReal.toNNReal_eq_toNNReal_iff x y, hx, hy, and_false, false_and, or_false]

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
hb : [[b, x]] ⊆ sᶜ
hb' : [[b, x]] ⊆ (t.ordSeparatingSet s).ordConnectedSectionᶜ
⊢ [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ

Tactic:
rw [ordSeparatingSet_comm, uIcc_comm] at hb'

Goal state after:
α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
hb : [[b, x]] ⊆ sᶜ
hb' : [[x, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
⊢ [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
Module: Mathlib.Topology.Order.T5

Goal state before:
pp: 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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
⊢ x ∈ Ico a c → x ∈ (s.ordSeparatingSet t).ordConnectedSectionᶜ

Tactic:
hx

Goal state after:
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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
⊢ x ∈ (s.ordSeparatingSet t).ordConnectedSectionᶜ
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case coe
a b : ℝ≥0
h : ↑b ≤ ↑a
x✝ : ℝ≥0
⊢ a - x✝ - (a - b) = b - x✝

Tactic:
rw [tsub_tsub_tsub_cancel_left]

Goal state after:
case coe
a b : ℝ≥0
h : ↑b ≤ ↑a
x✝ : ℝ≥0
⊢ b ≤ a
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
a : ℝ≥0∞
κ : ι → Sort u_2
f : (i : ι) → κ i → ℝ≥0∞
⊢ a + ⨅ i, ⨅ j, f i j = ⨅ i, ⨅ j, a + f i j

Tactic:
simp [add_iInf]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
⊢ Irreducible (Associates.mk v.asIdeal)

Tactic:
apply v.associates_irreducible

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : ↑v.asIdeal ≠ 0
h_self : ↑v.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑v.asIdeal
⊢ Irreducible (Associates.mk v.asIdeal)

Tactic:
apply v.associates_irreducible

Goal state after:
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0∞
h : a ≠ ∞
⊢ ∞ / a = ∞

Tactic:
simp [top_div, h]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v w : HeightOneSpectrum R
hw : w ≠ v
hw_fact : ↑w.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal
hw_ne_zero : ↑w.asIdeal ≠ 0
⊢ Irreducible (Associates.mk v.asIdeal)

Tactic:
apply v.associates_irreducible

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: case a
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist y z ≤ edist x z

Tactic:
edist_comm

Goal state after:
case a
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist y x = 0
⊢ edist y z ≤ edist x z
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
⊢ x ∈ eball y ε ↔ y ∈ eball x ε

Tactic:
by rw [mem_eball', mem_eball]

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
x✝ y✝ : α
h : edist x✝ y✝ < ∞
⊢ edist y✝ x✝ < ∞

Tactic:
edist_comm

Goal state after:
α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
x✝ y✝ : α
h : edist x✝ y✝ < ∞
⊢ edist x✝ y✝ < ∞
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
ha : IsUnit a
⊢ ∀ {a_1 b : ℝ≥0∞}, ha.unit.mulLeft a_1 ≤ ha.unit.mulLeft b ↔ a_1 ≤ b

Tactic:
simp [ENNReal.mul_le_mul_iff_right, ha.ne_zero, (isUnit_iff.1 ha).2]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: case refine_1
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ≥0∞
hε : ε > 0
⊢ {p | ↑(d p.1 p.2) < ε} ∈ ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | ↑(d p.1 p.2) < ε}

Tactic:
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 hε with ⟨ε', ε'0, ε'ε⟩
    refine mem_iInf_of_mem (ε' : ℝ) (mem_iInf_of_mem (ENNReal.coe_pos.1 ε'0) ?_)
    exact fun x hx => lt_trans (ENNReal.coe_lt_coe.2 hx) ε'ε

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

Goal state before:
pp: ι : Sort u_3
f : ι → ℕ
⊢ BddAbove (range fun x ↦ ↑(f x)) ↔ BddAbove (range f)

Tactic:
rw [← bddAbove_natCast_image_iff, ← Set.range_comp]

Goal state after:
ι : Sort u_3
f : ι → ℕ
⊢ BddAbove (range fun x ↦ ↑(f x)) ↔ BddAbove (range (Nat.cast ∘ f))