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

Goal state before:
pp: case e'_3
S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
hq : q.IsPrime
inst✝¹ : Algebra (Localization.AtPrime (under R q)) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (under R q) q
⊢ inst✝¹ = Localization.AtPrime.algebraOfLiesOver (under R q) q

Tactic:
simp [Algebra.algebra_ext_iff, Localization.AtPrime.IsLiesOverAlgebra.algebraMap_eq]

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: case neg.mp
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
hp : map f p ≤ P
H : ∃ n, ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n
he : Nat.find H ≠ 1
this : 1 ≤ Nat.find H
k : ℕ
hk : map f p ≤ P ^ k
h1k : 1 < k
⊢ map f p ≤ P ^ 2

Tactic:
exact hk.trans (Ideal.pow_le_pow_right (Nat.succ_le_iff.mpr h1k))

Goal state after:
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 Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
inst✝ : QuasiFiniteAt R Q
⊢ ∀ (y : ↥Q.primeCompl), IsUnit ((IsScalarTower.toAlgHom R S (Localization.AtPrime P)) ↑y)

Tactic:
simp only [IsScalarTower.coe_toAlgHom', Subtype.forall, Ideal.mem_primeCompl_iff]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
inst✝ : QuasiFiniteAt R Q
⊢ ∀ a ∉ Q, IsUnit ((algebraMap S (Localization.AtPrime P)) a)
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 R
inst✝⁴ : p.IsPrime
q : Ideal S
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : EssFiniteType R S
inst✝ : QuasiFiniteAt R q
e : ↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := p, isPrime := ⋯ }}) ≃ₜ
  PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S { asIdeal := p, isPrime := ⋯ }
qF : PrimeSpectrum (p.Fiber S) := e ⟨{ asIdeal := q, isPrime := inst✝³ }, ⋯⟩
this✝ : QuasiFiniteAt p.ResidueField qF.asIdeal
r : p.Fiber S
hr : r ∉ qF.asIdeal
hrq : ↑(PrimeSpectrum.basicOpen r) = {{ asIdeal := qF.asIdeal, isPrime := ⋯ }}
s : R
hs : s ∉ p
x : S
hsx : s • r = 1 ⊗ₜ[R] x
this : x ∉ q
q' : Ideal S
x✝¹ : q'.IsPrime
hq' : q' ≠ q
x✝ : q'.LiesOver p
hxq' : x ∉ q'
⊢ (algebraMap R (p.Fiber S)) s ∉
    RingHom.ker
      (TensorProduct.lift
          (Ideal.ResidueField.mapₐ { asIdeal := p, isPrime := ⋯ }.asIdeal
            (↑⟨{ asIdeal := q', isPrime := x✝¹ }, ⋯⟩).asIdeal (ofId R S) ⋯)
          (IsScalarTower.toAlgHom R S (↑⟨{ asIdeal := q', isPrime := x✝¹ }, ⋯⟩).asIdeal.ResidueField) ⋯).toRingHom

Tactic:
· simpa [IsScalarTower.algebraMap_apply R S q'.ResidueField, ← Ideal.mem_comap, ← q'.over_def p]

Goal state after:
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 ∈ Q.ker ^ 2
⊢ Extension.Cotangent.mk ⟨x, hx'⟩ ∈
    (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)).range

Tactic:
rw [pow_two, ← map_ofComp_ker (P := P), ← Ideal.map_mul, Ideal.mem_map_iff_of_surjective
      _ (toAlgHom_ofComp_surjective Q P)] at hx

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 : ∃ x_1 ∈ (Q.comp P).ker * (Q.comp P).ker, (Q.ofComp P).toAlgHom x_1 = (Q.ofComp P).toAlgHom x
⊢ Extension.Cotangent.mk ⟨x, hx'⟩ ∈
    (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)).range
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: case refine_1
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)
this : Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) ≤ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P)).ker →
  P ⧸ Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) →ₗ[R] S ⊗[P] Ω[P⁄R] :=
  (Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2)).liftQ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P))
⊢ Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) ≤ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P)).ker

Tactic:
rintro x hx

Goal state after:
case refine_1
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)
this : Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) ≤ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P)).ker →
  P ⧸ Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) →ₗ[R] S ⊗[P] Ω[P⁄R] :=
  (Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2)).liftQ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P))
x : P
hx : x ∈ Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2)
⊢ x ∈ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P)).ker
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
H : f.toRingHom.FormallyEtale
this✝⁴ : Algebra P.Ring Q.Ring := f.toRingHom.toAlgebra
this✝³ : IsScalarTower R P.Ring Q.Ring
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
this : FormallyEtale P.Ring Q.Ring
x : Q.CotangentSpace
a : Q.Ring
⊢ (LinearMap.liftBaseChange T (CotangentSpace.map f))
      (1 •
        (LinearMap.liftBaseChange Q.Ring
            (↑P.Ring ((TensorProduct.mk S T P.CotangentSpace) 1) ∘ₗ (TensorProduct.mk P.Ring S Ω[P.Ring⁄R]) 1))
          ((tensorKaehlerEquivOfFormallyEtale R P.Ring Q.Ring).symm ((D R Q.Ring) a))) =
    1 ⊗ₜ[Q.Ring] (D R Q.Ring) a

Tactic:
obtain ⟨x, hx⟩ := (tensorKaehlerEquivOfFormallyEtale R P.Ring _).surjective (D R Q.Ring a)

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
H : f.toRingHom.FormallyEtale
this✝⁴ : Algebra P.Ring Q.Ring := f.toRingHom.toAlgebra
this✝³ : IsScalarTower R P.Ring Q.Ring
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
this : FormallyEtale P.Ring Q.Ring
x✝ : Q.CotangentSpace
a : Q.Ring
x : Q.Ring ⊗[P.Ring] Ω[P.Ring⁄R]
hx : (tensorKaehlerEquivOfFormallyEtale R P.Ring Q.Ring) x = (D R Q.Ring) a
⊢ (LinearMap.liftBaseChange T (CotangentSpace.map f))
      (1 •
        (LinearMap.liftBaseChange Q.Ring
            (↑P.Ring ((TensorProduct.mk S T P.CotangentSpace) 1) ∘ₗ (TensorProduct.mk P.Ring S Ω[P.Ring⁄R]) 1))
          ((tensorKaehlerEquivOfFormallyEtale R P.Ring Q.Ring).symm ((D R Q.Ring) a))) =
    1 ⊗ₜ[Q.Ring] (D R Q.Ring) a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : factorization a = factorization b
⊢ a ~ᵤ b

Tactic:
by
  simp_rw [factorization, AddEquiv.apply_eq_iff_eq] at h
  rwa [associated_iff_normalizedFactors_eq_normalizedFactors ha hb]

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
hI : I ≠ 0
h_supp : {v | ¬↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0} = {v | v.asIdeal ∣ I}
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0

Tactic:
rw [Filter.eventually_cofinite, h_supp]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_supp : {v | ¬↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0} = {v | v.asIdeal ∣ I}
⊢ {v | v.asIdeal ∣ I}.Finite
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ {v | v.maxPowDividing I ≠ 1} ⊆ {v | ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) ≠ 0}

Tactic:
intro v hv h_zero
    have hv' : v.maxPowDividing I = 1 := by
      rw [IsDedekindDomain.HeightOneSpectrum.maxPowDividing, Int.natCast_eq_zero.mp h_zero,
        pow_zero _]
    exact hv hv'

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

Goal state before:
pp: r : ℝ
⊢ r.toNNReal = 0 ↔ r ≤ 0

Tactic:
by
  simpa [-toNNReal_pos] using not_iff_not.2 (@toNNReal_pos r)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : HasFiniteMulSupport fun v ↦ v.maxPowDividing I
h_ne_zero : v.maxPowDividing I ≠ 0
h_contr :
  v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣
    v.maxPowDividing I * ∏ i ∈ (Finite.toFinset hf).erase v, i.maxPowDividing I
hv_prime : Prime v.asIdeal
w : HeightOneSpectrum R
hw : w ∈ (Finite.toFinset hf).erase v
hvw' : v.asIdeal ∣ w.maxPowDividing I
hw_prime : Prime w.asIdeal
hvw : v.asIdeal ∣ w.asIdeal
⊢ False

Tactic:
rw [Prime.dvd_prime_iff_associated hv_prime hw_prime, associated_iff_eq] at hvw

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : HasFiniteMulSupport fun v ↦ v.maxPowDividing I
h_ne_zero : v.maxPowDividing I ≠ 0
h_contr :
  v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣
    v.maxPowDividing I * ∏ i ∈ (Finite.toFinset hf).erase v, i.maxPowDividing I
hv_prime : Prime v.asIdeal
w : HeightOneSpectrum R
hw : w ∈ (Finite.toFinset hf).erase v
hvw' : v.asIdeal ∣ w.maxPowDividing I
hw_prime : Prime w.asIdeal
hvw : v.asIdeal = w.asIdeal
⊢ False
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: a : ℝ≥0∞
b : ℝ≥0
h : a ≤ ↑b
⊢ a.toReal ≤ ↑b

Tactic:
lift a to ℝ≥0 using ne_top_of_le_ne_top coe_ne_top h
  simpa using h

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

Goal state before:
pp: b a : ℝ≥0
h : ↑a = ∞ → ↑b = ∞
h_nnreal : ↑a ≠ ∞ → ↑b ≠ ∞ → (↑a).toNNReal ≤ (↑b).toNNReal
hlt : ↑b < ↑a
⊢ ↑a ≤ ↑b

Tactic:
simpa using h_nnreal

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

Goal state before:
pp: a b : ℝ≥0∞
hr : a ≠ ∞
hp : b ≠ ∞
h : a ≤ b
⊢ (max a b).toReal = max a.toReal b.toReal

Tactic:
simp only [h, ENNReal.toReal_mono hp h, max_eq_right]

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

Goal state before:
pp: a b : ℝ≥0∞
hr : a ≠ ∞
hp : b ≠ ∞
h : b ≤ a
⊢ (max a b).toReal = max a.toReal b.toReal

Tactic:
by
    simp only [h, ENNReal.toReal_mono hr h, max_eq_left]

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
inst : PseudoEMetricSpace α
⊢ (uniformSpaceOfEDist edist ⋯ ⋯ ⋯).toTopologicalSpace ≤ toUniformSpace.toTopologicalSpace

Tactic:
uniformSpace_edist

Goal state after:
α✝ : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α✝
γ : Type w
inst✝ : EMetricSpace γ
α : Type u
inst : PseudoEMetricSpace α
⊢ (uniformSpaceOfEDist edist ⋯ ⋯ ⋯).toTopologicalSpace ≤ (uniformSpaceOfEDist edist ⋯ ⋯ ⋯).toTopologicalSpace
Module: Mathlib.Topology.MetricSpace.Defs

Goal state before:
pp: γ : Type w
inst✝ : MetricSpace γ
x y : γ
⊢ dist x y = 0 ↔ x = y

Tactic:
dist_eq_zero

Goal state after:
γ : Type w
inst✝ : MetricSpace γ
x y : γ
⊢ x = y ↔ x = y
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
⊢ BoundedSpace α ↔ ∃ C, ∀ (a b : α), dist a b ≤ C

Tactic:
rw [← isBounded_univ, Metric.isBounded_iff]
  simp

Goal state after:
Module: Mathlib.Topology.Bornology.Constructions

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝ : Bornology β
f : α → β
⊢ BoundedSpace α ↔ Bornology.IsBounded (range f)

Tactic:
by
  rw [← @isBounded_univ, isBounded_induced, image_univ]

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

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α × β
r : ℝ
hr : 0 < r
x' : α
y' : β
⊢ (x', y') ∈ sphere x r ↔ x' ∈ sphere x.1 r ∧ y' ∈ closedBall x.2 r ∨ x' ∈ closedBall x.1 r ∧ y' ∈ sphere x.2 r

Tactic:
Metric.mem_closedBall,

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α × β
r : ℝ
hr : 0 < r
x' : α
y' : β
⊢ (x', y') ∈ sphere x r ↔ x' ∈ sphere x.1 r ∧ dist y' x.2 ≤ r ∨ dist x' x.1 ≤ r ∧ y' ∈ sphere x.2 r
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
b : β
⊢ edist (f b) (g b) ≤ edist f g

Tactic:
exact edist_le_pi_edist f g b

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

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
ht : t.Nonempty
h : x ∈ t
⊢ ∃ u, Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t

Tactic:
exact ⟨fun _ => x, monotone_const, fun n => le_rfl, tendsto_const_nhds, fun _ => h⟩

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

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

Tactic:
· specialize h d <| by simp [← Set.mem_Ioi, H0]
      filter_upwards [h] with x hx
      rw [← Set.compl_Iic, ← Set.compl_Iio, compl_inj_iff] at H0
      simpa [← Set.mem_Iic, ← Set.mem_Iio, H0] using hx

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

Goal state before:
pp: α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
⊢ ∃ x, IsLeast s x

Tactic:
have : Nonempty s := ne_s.to_subtype

Goal state after:
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty ↑s
⊢ ∃ x, IsLeast s x
Module: Mathlib.Topology.MetricSpace.Cauchy

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
⊢ ∃ R > 0, ∀ (m n : ℕ), dist (u m) (u n) < R

Tactic:
rcases Metric.cauchySeq_iff'.1 hu 1 zero_lt_one with ⟨N, hN⟩

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
N : ℕ
hN : ∀ n ≥ N, dist (u n) (u N) < 1
⊢ ∃ R > 0, ∀ (m n : ℕ), dist (u m) (u n) < R
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: α : Type u_1
X : Type u_2
inst✝ : PseudoEMetricSpace X
d : ℝ≥0∞
f : α → X
s : Set α
⊢ ediam (f '' s) ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) ≤ d

Tactic:
by
  simp only [ediam_le_iff, forall_mem_image]

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

Goal state before:
pp: X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
⊢ ediam (s ∪ t) ≤ ediam s + edist x y + ediam t

Tactic:
refine ediam_le fun a ha b hb => ?_

Goal state after:
X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a : X
ha : a ∈ s ∪ t
b : X
hb : b ∈ s ∪ t
⊢ edist a b ≤ ediam s + edist x y + ediam t
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case refine_4
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 = spanSingleton R⁰ (I'.divMod I J') * J
H : Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
⊢ ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I ≤ ↑I'

Tactic:
exact le_trans (by simp) (divMod_spec h' hJ' hI).le

Goal state after:
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ diam {x, y, z} = max (max (dist x y) (dist x z)) (dist y z)

Tactic:
by
  simp only [diam, ediam_triple, dist_edist]
  rw [ENNReal.toReal_max, ENNReal.toReal_max] <;> apply_rules [ne_of_lt, edist_lt_top, max_lt]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
⊢ blimsup u f p = limsup (u ∘ Subtype.val) (comap Subtype.val f)

Tactic:
by
  rw [blimsup_eq_limsup, limsup, limsup, ← map_map, map_comap_setCoe_val]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
b : β
x y : α
⊢ edist ((fun x ↦ b) x) ((fun x ↦ b) y) ≤ ↑0 * edist x y

Tactic:
by
  simp only [edist_self, zero_le]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
b : β
K : ℝ≥0
x y : α
⊢ edist ((fun x ↦ b) x) ((fun x ↦ b) y) ≤ ↑K * edist x y

Tactic:
by
  simp only [edist_self, zero_le]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
⊢ liminf u f \ a = liminf (fun b ↦ u b \ a) f

Tactic:
simp only [_root_.sdiff_eq, inf_comm _ aᶜ, inf_liminf]

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

Goal state before:
pp: α : Type u_3
inst✝ : Infinite α
⊢ Tendsto Finset.card atTop atTop

Tactic:
by
  rw [Tendsto, map_card_atTop]

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

Goal state before:
pp: case neg_coe
a b c : ℝ≥0∞
hc : 0 < c
⊢ -(↑(a * c) + ↑(b * c)) = -↑(a * c) + -↑(b * c)

Tactic:
EReal.neg_add (.inl (coe_ennreal_ne_bot _)) (.inr (coe_ennreal_ne_bot _)),

Goal state after:
case neg_coe
a b c : ℝ≥0∞
hc : 0 < c
⊢ -↑(a * c) - ↑(b * c) = -↑(a * c) + -↑(b * c)
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: case e'_6
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite
⊢ finprod (L.support.mulIndicator fun b ↦ f b) = ∏ b ∈ (↑⋯.toFinset).toFinset, f b

Tactic:
simp only [Set.Finite.coe_toFinset, Finset.toFinset_coe]

Goal state after:
case e'_6
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite
⊢ finprod (L.support.mulIndicator fun b ↦ f b) = ∏ b ∈ ⋯.toFinset, f b
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f : β → α
hf : Multipliable (fun b ↦ (f b)⁻¹) L
⊢ Multipliable f L

Tactic:
by
  simpa only [inv_inv] using hf.inv

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f : β → α
a₁ a₂ : α
s : Set β
hf : HasProd (f ∘ Subtype.val) a₁
⊢ HasProd (f ∘ Subtype.val) a₂ ↔ HasProd f (a₁ * a₂)

Tactic:
by
  refine ⟨fun h ↦ hf.mul_compl h, fun h ↦ ?_⟩
  rw [hasProd_subtype_iff_mulIndicator] at hf ⊢
  rw [Set.mulIndicator_compl]
  simpa only [div_eq_mul_inv, mul_inv_cancel_comm] using! h.div hf

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
s : Finset β
L : SummationFilter β
inst✝ : L.LeAtTop
⊢ ∏ x ∈ s, f x = ∏'[L] (x : β), (↑s).mulIndicator f x

Tactic:
tprod_eq_prod' (Set.mulSupport_mulIndicator_subset),

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
s : Finset β
L : SummationFilter β
inst✝ : L.LeAtTop
⊢ ∏ x ∈ s, f x = ∏ b ∈ s, (↑s).mulIndicator f b
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
K : Type u_4
inst✝² : CommGroupWithZero K
inst✝¹ : TopologicalSpace K
f g : α → K
inst✝ : SeparatelyContinuousMul K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
t : Finset α
ht : s ⊆ t
⊢ ∏ x ∈ s ∪ t \ s, g x = ∏ i ∈ t, g i

Tactic:
union_sdiff_of_subset ht

Goal state after:
α : Type u_1
K : Type u_4
inst✝² : CommGroupWithZero K
inst✝¹ : TopologicalSpace K
f g : α → K
inst✝ : SeparatelyContinuousMul K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
t : Finset α
ht : s ⊆ t
⊢ ∏ x ∈ t, g x = ∏ i ∈ t, g i
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: ι : Sort u_1
n✝ n : ℕ
hn : n ≠ 0
⊢ (fun x ↦ x ^ n) = ⇑(NNReal.powOrderIso n hn).withTopCongr

Tactic:
cases n; (· cases hn rfl); · ext (_ | _) <;> rfl

Goal state after:
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
hf : Isometry f
s : Set α
⊢ (Metric.ediam (f '' s)).toReal = (Metric.ediam s).toReal

Tactic:
hf.ediam_image

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
hf : Isometry f
s : Set α
⊢ (Metric.ediam s).toReal = (Metric.ediam s).toReal
Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝³ : AddCommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : StarAddMonoid α
inst✝ : ContinuousStar α
f : β → α
a : α
h : HasSum f a L
⊢ HasSum (fun b ↦ Star.star (f b)) (Star.star a) L

Tactic:
simpa only using! h.map (starAddEquiv : α ≃+ α) continuous_star

Goal state after: