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

Goal state before:
pp: 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✝² : Algebra.EssFiniteType R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : PerfectField (under R q).ResidueField
h : map (algebraMap R (Localization.AtPrime q)) (under R q) = IsLocalRing.maximalIdeal (Localization.AtPrime q)
p : Ideal R := under R q
Rp : Type u_2 := Localization.AtPrime p
Sq : Type u_1 := Localization.AtPrime q
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
this : Algebra.EssFiniteType Rp Sq
⊢ Algebra.IsSeparable (IsLocalRing.ResidueField Rp) (IsLocalRing.ResidueField Sq) ∧
    map (algebraMap Rp Sq) (map (algebraMap R (Localization.AtPrime p)) p) = IsLocalRing.maximalIdeal Sq

Tactic:
map_map,

Goal state after:
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✝² : Algebra.EssFiniteType R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : PerfectField (under R q).ResidueField
h : map (algebraMap R (Localization.AtPrime q)) (under R q) = IsLocalRing.maximalIdeal (Localization.AtPrime q)
p : Ideal R := under R q
Rp : Type u_2 := Localization.AtPrime p
Sq : Type u_1 := Localization.AtPrime q
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
this : Algebra.EssFiniteType Rp Sq
⊢ Algebra.IsSeparable (IsLocalRing.ResidueField Rp) (IsLocalRing.ResidueField Sq) ∧
    map ((algebraMap Rp Sq).comp (algebraMap R (Localization.AtPrime p))) p = IsLocalRing.maximalIdeal Sq
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
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : Q.H1Cotangent
this : Function.Exact ⇑(LinearMap.baseChange T h1Cotangentι) ⇑(LinearMap.baseChange T P.cotangentComplex)
⊢ (LinearMap.baseChange T P.cotangentComplex) ((tensorCotangent f halg H₂).symm ↑x) = 0

Tactic:
apply (Extension.tensorCotangentSpaceOfFormallyEtale f H₁).injective
      rw [LinearEquiv.map_zero, ← x.2]
      have : (CotangentSpace.map f).liftBaseChange T ∘ₗ P.cotangentComplex.baseChange T =
          Q.cotangentComplex ∘ₗ (Cotangent.map f).liftBaseChange T := by
        ext x; obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x; dsimp
        simp only [CotangentSpace.map_tmul,
          map_one, Hom.toAlgHom_apply, one_smul, cotangentComplex_mk]
      exact (DFunLike.congr_fun this _).trans (DFunLike.congr_arg Q.cotangentComplex
        ((tensorCotangent f halg H₂).apply_symm_apply x.1))

Goal state after:
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
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : Q.H1Cotangent
this : Function.Exact ⇑(LinearMap.baseChange T h1Cotangentι) ⇑(LinearMap.baseChange T P.cotangentComplex)
⊢ (LinearMap.baseChange T P.cotangentComplex) ((tensorCotangent f halg H₂).symm ↑x) = 0

Tactic:
by
      apply (Extension.tensorCotangentSpaceOfFormallyEtale f H₁).injective
      rw [LinearEquiv.map_zero, ← x.2]
      have : (CotangentSpace.map f).liftBaseChange T ∘ₗ P.cotangentComplex.baseChange T =
          Q.cotangentComplex ∘ₗ (Cotangent.map f).liftBaseChange T := by
        ext x; obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x; dsimp
        simp only [CotangentSpace.map_tmul,
          map_one, Hom.toAlgHom_apply, one_smul, cotangentComplex_mk]
      exact (DFunLike.congr_fun this _).trans (DFunLike.congr_arg Q.cotangentComplex
        ((tensorCotangent f halg H₂).apply_symm_apply x.1))

Goal state after:
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 S (Localization.AtPrime q)) (map (algebraMap R S) p) =
    map (algebraMap S (Localization.AtPrime q)) (q ^ p.ramificationIdx' q * I)
⊢ p.ramificationIdx' q = q.ramificationIdx R

Tactic:
map_map,

Goal state after:
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 S (Localization.AtPrime q)).comp (algebraMap R S)) p =
    map (algebraMap S (Localization.AtPrime q)) (q ^ p.ramificationIdx' q * I)
⊢ p.ramificationIdx' q = q.ramificationIdx R
Module: Mathlib.RingTheory.RamificationInertia.Ramification

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
q : Ideal S
r : Ideal T
inst✝⁵ : q.IsPrime
inst✝⁴ : r.IsPrime
inst✝³ : r.LiesOver q
inst✝² : Algebra (Localization.AtPrime q) (Localization.AtPrime r)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra q r
inst✝ : Module.Flat (Localization.AtPrime q) (Localization.AtPrime r)
this : q.LiesOver (under R r)
⊢ ?m.101 =
    map (algebraMap (Localization.AtPrime q) (Localization.AtPrime r))
      (map (algebraMap R (Localization.AtPrime q)) (under R r))

Tactic:
map_map,

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
q : Ideal S
r : Ideal T
inst✝⁵ : q.IsPrime
inst✝⁴ : r.IsPrime
inst✝³ : r.LiesOver q
inst✝² : Algebra (Localization.AtPrime q) (Localization.AtPrime r)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra q r
inst✝ : Module.Flat (Localization.AtPrime q) (Localization.AtPrime r)
this : q.LiesOver (under R r)
⊢ ?m.101 =
    map ((algebraMap (Localization.AtPrime q) (Localization.AtPrime r)).comp (algebraMap R (Localization.AtPrime q)))
      (under R r)
Module: Mathlib.RingTheory.RamificationInertia.Ramification

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
q : Ideal S
r : Ideal T
inst✝¹ : r.LiesOver q
inst✝ : Module.Flat S T
⊢ r.ramificationIdx S ∣ r.ramificationIdx R

Tactic:
use q.ramificationIdx R

Goal state after:
case h
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
q : Ideal S
r : Ideal T
inst✝¹ : r.LiesOver q
inst✝ : Module.Flat S T
⊢ r.ramificationIdx R = r.ramificationIdx S * q.ramificationIdx R
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
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
f : P.Hom Q :=
  { toRingHom := algebraMap P.Ring (Localization M'), toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
this✝⁸ : FormallySmooth R P.Ring
this✝⁷ : FormallySmooth P.Ring (Localization M')
this✝⁶ : FormallySmooth R Q.Ring
this✝⁵ : Module.Flat S T
this✝⁴ : Algebra P.Ring Q.Ring := inferInstance
this✝³ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝² : Algebra (Localization M') T := fQ.toAlgebra
this✝¹ : IsScalarTower P.Ring S T
this✝ : IsScalarTower P.Ring (Localization M') T
this : IsLocalizedModule M' (IsScalarTower.toAlgHom P.Ring S T).toLinearMap
F : ↥P.ker →ₗ[P.Ring] ↥(RingHom.ker fQ) := f.mapKer ⋯
x s : P.Ring
hs : s ∈ M'
⊢ (algebraMap P.Ring (Localization M')) x =
    ⟨s, hs⟩ • IsLocalizedModule.mk' (Algebra.linearMap P.Ring (Localization M')) x ⟨s, hs⟩

Tactic:
IsLocalizedModule.mk'_cancel'

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
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
f : P.Hom Q :=
  { toRingHom := algebraMap P.Ring (Localization M'), toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
this✝⁸ : FormallySmooth R P.Ring
this✝⁷ : FormallySmooth P.Ring (Localization M')
this✝⁶ : FormallySmooth R Q.Ring
this✝⁵ : Module.Flat S T
this✝⁴ : Algebra P.Ring Q.Ring := inferInstance
this✝³ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝² : Algebra (Localization M') T := fQ.toAlgebra
this✝¹ : IsScalarTower P.Ring S T
this✝ : IsScalarTower P.Ring (Localization M') T
this : IsLocalizedModule M' (IsScalarTower.toAlgHom P.Ring S T).toLinearMap
F : ↥P.ker →ₗ[P.Ring] ↥(RingHom.ker fQ) := f.mapKer ⋯
x s : P.Ring
hs : s ∈ M'
⊢ (algebraMap P.Ring (Localization M')) x = (Algebra.linearMap P.Ring (Localization M')) x
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: case inr.inr
α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
x : { x // x ∈ s.ordSeparatingSet t }
ha : [[a, ↑x]] ⊆ tᶜ
hb : [[b, ↑x]] ⊆ sᶜ
hax : a ≤ ↑x
hxb : ↑x ≤ b
y : α
hy : y ∈ (s.ordSeparatingSet t).ordConnectedComponent ↑x
sol1 : y < a → False
⊢ ¬y < a ∧ ¬b < y

Tactic:
have sol2 := fun (hby : b < y) =>
      (disjoint_left (t := ordSeparatingSet s t)).1 disjoint_right_ordSeparatingSet hbt
        (hy <| Icc_subset_uIcc ⟨hxb, hby.le⟩)

Goal state after:
case inr.inr
α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
x : { x // x ∈ s.ordSeparatingSet t }
ha : [[a, ↑x]] ⊆ tᶜ
hb : [[b, ↑x]] ⊆ sᶜ
hax : a ≤ ↑x
hxb : ↑x ≤ b
y : α
hy : y ∈ (s.ordSeparatingSet t).ordConnectedComponent ↑x
sol1 : y < a → False
sol2 : b < y → False
⊢ ¬y < a ∧ ¬b < y
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 : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ Associates.mk (Ideal.span {a}) ≠ 0

Tactic:
rw [ne_eq, Associates.mk_eq_zero]; exact h_a_ne_zero

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

Goal state before:
pp: case mp
x : ℝ
⊢ x ∈ toReal '' Ioo ⊥ 0 → x ∈ Iio 0

Tactic:
rintro ⟨y, ⟨_, hy0⟩, rfl⟩

Goal state after:
case mp
y : EReal
left✝ : ⊥ < y
hy0 : y < 0
⊢ y.toReal ∈ Iio 0
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case empty
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
ι : Type u_3
I : ι → FractionalIdeal R⁰ K
hS : ∀ i ∈ ∅, I i ≠ 0
⊢ count K v 1 = ∑ i ∈ ∅, count K v (I i)

Tactic:
Finset.sum_empty,

Goal state after:
case empty
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
ι : Type u_3
I : ι → FractionalIdeal R⁰ K
hS : ∀ i ∈ ∅, I i ≠ 0
⊢ count K v 1 = 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
htop : b⁻¹ ≠ 0 ∨ a ≠ ∞
hzero : b⁻¹ ≠ ∞ ∨ a ≠ 0
⊢ (a / b)⁻¹ = b / a

Tactic:
ENNReal.div_eq_inv_mul,

Goal state after:
a b : ℝ≥0∞
htop : b⁻¹ ≠ 0 ∨ a ≠ ∞
hzero : b⁻¹ ≠ ∞ ∨ a ≠ 0
⊢ (b⁻¹ * a)⁻¹ = b / a
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
htop : b⁻¹ ≠ 0 ∨ a ≠ ∞
hzero : b⁻¹ ≠ ∞ ∨ a ≠ 0
⊢ (b⁻¹ * a)⁻¹ = b / a

Tactic:
ENNReal.div_eq_inv_mul,

Goal state after:
a b : ℝ≥0∞
htop : b⁻¹ ≠ 0 ∨ a ≠ ∞
hzero : b⁻¹ ≠ ∞ ∨ a ≠ 0
⊢ (b⁻¹ * a)⁻¹ = a⁻¹ * b
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inr.inr
a b : ℝ≥0∞
h₀ : a = 0 → b = 0
h₁ : a = ∞ → b = 0
ha : a ≠ 0
ha' : a ≠ ∞
⊢ a / (a / b) = b

Tactic:
ENNReal.div_eq_inv_mul,

Goal state after:
case inr.inr
a b : ℝ≥0∞
h₀ : a = 0 → b = 0
h₁ : a = ∞ → b = 0
ha : a ≠ 0
ha' : a ≠ ∞
⊢ (a / b)⁻¹ * a = b
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case coe.inr
a c : ℝ≥0∞
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ∞ ∨ c ≠ ∞
hb : b ≠ 0
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c

Tactic:
← coe_ne_zero

Goal state after:
case coe.inr
a c : ℝ≥0∞
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ∞ ∨ c ≠ ∞
hb : ↑b ≠ 0
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case refine_2
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ ↑x < ↑y ^ (n + 1)

Tactic:
· rwa [← ENNReal.coe_zpow A, ENNReal.coe_lt_coe]

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

Goal state before:
pp: case refine_1
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ↑y ^ n < ↑x

pp: case refine_2
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ↑x ≤ ↑y ^ (n + 1)

Tactic:
· rwa [← ENNReal.coe_zpow A, ENNReal.coe_lt_coe]

Goal state after:
case refine_2
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ↑x ≤ ↑y ^ (n + 1)
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
h : y ∈ eball x ε
⊢ ∃ ε' > 0, eball y ε' ⊆ eball x ε

Tactic:
have : 0 < ε - edist y x := by simpa using h
  refine ⟨ε - edist y x, this, eball_subset ?_ (ne_top_of_lt h)⟩
  exact (add_tsub_cancel_of_le (mem_eball.mp h).le).le

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

Goal state before:
pp: y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ y ^ (n + 1) < ∞

Tactic:
exact ENNReal.zpow_lt_top (zero_lt_one.trans hy).ne' h'y _

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

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
i : ι
hi : f i = 0
x✝¹ : ℝ≥0∞
x✝ : ⊥ < x✝¹
⊢ ∞ * f i < x✝¹

Tactic:
simpa [hi]

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

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
i : ι
hi : f i = 0
x✝¹ : ℝ≥0∞
x✝ : ⊥ < x✝¹
⊢ f i < x✝¹

Tactic:
simpa [hi]

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

Goal state before:
pp: α✝ : Type u
β✝ : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α✝
γ : Type w
inst✝ : EMetricSpace γ
α : Type u_2
β : Type u_3
e : TopologicalSpace α
n : TopologicalSpace β
f : α → β
hf : Topology.IsInducing f
m : WeakPseudoEMetricSpace β
x : α
r : ℝ≥0∞
u : Set β
hu : IsOpen[n] u
uy : Subtype.val ⁻¹' u = Metric.eball (f x) ∞ ↓∩ Metric.eball (f x) r
⊢ Subtype.val ⁻¹' f ⁻¹' u = Metric.eball x ∞ ↓∩ Metric.eball x r

Tactic:
by aesop (add simp [Set.ext_iff])

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
r : ℝ
hr : 0 ≤ r
⊢ edist x y ≤ ENNReal.ofReal r ↔ dist x y ≤ r

Tactic:
by
  rw [edist_dist, ENNReal.ofReal_le_ofReal_iff hr]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
⊢ ball x 0 = ∅

Tactic:
by rw [ball_eq_empty]

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

Goal state before:
pp: case base
α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n : ℕ
⊢ dist (f m) (f m) ≤ ∑ i ∈ ∅, dist (f i) (f (i + 1))

Tactic:
Finset.sum_empty,

Goal state after:
case base
α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n : ℕ
⊢ dist (f m) (f m) ≤ 0
Module: Mathlib.Topology.EMetricSpace.Basic

Goal state before:
pp: case base
α : Type u
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n : ℕ
⊢ edist (f m) (f m) ≤ ∑ i ∈ ∅, edist (f i) (f (i + 1))

Tactic:
Finset.sum_empty,

Goal state after:
case base
α : Type u
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n : ℕ
⊢ edist (f m) (f m) ≤ 0
Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
⊢ ⋂ r', ⋂ (_ : r' > r), closedBall x r' = closedBall x r

Tactic:
ext
  simp [forall_gt_imp_ge_iff_le_of_dense]

Goal state after:
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
x✝ : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ ↑f
hf : ∀ x ∈ Icc a b, ¬↑f ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this✝² : ∀ i < c, Ioi i ∈ f
x : α
hx : c < x
hxf : Iio x ∉ f
this✝¹ : Icc a c ∉ f
this✝ : x ∈ Icc a b
this : Icc a x ∈ f
⊢ {x} ∈ f

Tactic:
filter_upwards [f.compl_mem_iff_notMem.mpr hxf, this]; grind

Goal state after:
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: case inl
α : Type u_1
γ : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
l : Filter γ
inst✝ : CountableInterFilter l
f : γ → α
d : α
h : ∀ (b : α), d < b → ∀ᶠ (x : γ) in l, f x < b
hd : IsGLB (Ioi d) d
⊢ ∀ᶠ (x : γ) in l, f x ≤ d

Tactic:
obtain h | _ := isTop_or_exists_gt d
      · exact .of_forall (fun _ ↦ h _)
      obtain ⟨u, -, -, hu_tt, hu_gt⟩ := hd.exists_seq_antitone_tendsto (by simpa)
      replace h := fun n ↦ h (u n) (by grind)
      rw [← eventually_countable_forall] at h
      filter_upwards [h] with x hx
      exact ge_of_tendsto hu_tt <| .of_forall <| fun n ↦ le_of_lt <| hx n

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 J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this :
  (J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I) * (J' ⊔ spanSingleton R⁰ (I'.divMod I J') * I) =
    J' * (spanSingleton R⁰ (I'.divMod I J') * I)
⊢ J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J

Tactic:
FractionalIdeal.sup_eq_add,

Goal state after:
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 J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this :
  (J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I) * (J' + spanSingleton R⁰ (I'.divMod I J') * I) =
    J' * (spanSingleton R⁰ (I'.divMod I J') * I)
⊢ J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ (fun x ↦ b * x) ⁻¹' ball a r = ball (a / b) r

Tactic:
ext c

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
c : E
⊢ c ∈ (fun x ↦ b * x) ⁻¹' ball a r ↔ c ∈ ball (a / b) r
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ (fun x ↦ b * x) ⁻¹' closedBall a r = closedBall (a / b) r

Tactic:
ext c

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
c : E
⊢ c ∈ (fun x ↦ b * x) ⁻¹' closedBall a r ↔ c ∈ closedBall (a / b) r
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ (fun x ↦ b * x) ⁻¹' sphere a r = sphere (a / b) r

Tactic:
ext c

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
c : E
⊢ c ∈ (fun x ↦ b * x) ⁻¹' sphere a r ↔ c ∈ sphere (a / b) r
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: R : Type u_2
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℚ) in atTop, p ↑n

Tactic:
by
  rw [← Rat.comap_cast_atTop (R := R)]; exact h.comap _

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

Goal state before:
pp: x : EReal
h : x ≠ ⊥
⊢ x + ⊤ = ⊤

Tactic:
rw [add_comm, top_add_of_ne_bot h]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
s : Set α
⊢ (𝓟 s).limsSup = sSup s

Tactic:
simpa only [limsSup, eventually_principal] using! sInf_upperBounds_eq_sSup s

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

Goal state before:
pp: case bot
h_top : ⊥ ≠ ⊤
h_bot : ⊥ ≠ ⊥
⊢ ⊥ - ⊥ = 0

Tactic:
simp_all [← coe_sub]

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

Goal state before:
pp: case coe
a✝ : ℝ
h_top : ↑a✝ ≠ ⊤
h_bot : ↑a✝ ≠ ⊥
⊢ ↑a✝ - ↑a✝ = 0

Tactic:
simp_all [← coe_sub]

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

Goal state before:
pp: case top
h_top : ⊤ ≠ ⊤
h_bot : ⊤ ≠ ⊥
⊢ ⊤ - ⊤ = 0

Tactic:
simp_all [← coe_sub]

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

Goal state before:
pp: x y : ℝ≥0∞
hy_top : y ≠ ∞
h_le : y ≤ x
⊢ ↑(x - y) = ↑x - ↑y

Tactic:
lift y to ℝ≥0 using hy_top

Goal state after:
x : ℝ≥0∞
y : ℝ≥0
h_le : ↑y ≤ x
⊢ ↑(x - ↑y) = ↑x - ↑↑y
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case pos_bot
x✝ : ℝ
hx : 0 < x✝
⊢ 0 < ↑x✝ * ⊥ ↔ 0 < ↑x✝ ∧ 0 < ⊥ ∨ ↑x✝ < 0 ∧ ⊥ < 0

Tactic:
simp [hx, EReal.coe_mul_bot_of_pos hx, le_of_lt]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
inst✝ : Infinite α
⊢ ⨅ a, 𝓟 (Finset.card '' {a' | a ⊆ a'}) = ⨅ a, 𝓟 (Ici a)

Tactic:
refine Function.Surjective.iInf_congr Finset.card Finset.exists_card_eq fun s ↦ congr(𝓟 $(?_))

Goal state after:
α : Type u_3
inst✝ : Infinite α
s : Finset α
⊢ Ici s.card = Finset.card '' {a' | s ⊆ a'}
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.NeBot
f : β ↪ γ
⊢ (L.map f).support = ⇑f '' L.support

Tactic:
ext c

Goal state after:
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.NeBot
f : β ↪ γ
c : γ
⊢ c ∈ (L.map f).support ↔ c ∈ ⇑f '' L.support