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

Goal state before:
pp: R : Type u_4
Rₘ : Type u_6
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
Q : Type (max u_4 u_6)
x✝¹ : CommRing Q
x✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
⊢ ∃ a, (Ideal.Quotient.mkₐ R I).comp a = f

Tactic:
have : ∀ x : M, IsUnit (algebraMap R Q x) := by
    intro x
    apply (IsNilpotent.isUnit_quotient_mk_iff ⟨2, e⟩).mp
    convert! (IsLocalization.map_units Rₘ x).map f
    simp only [Ideal.Quotient.mk_algebraMap, AlgHom.commutes]

Goal state after:
R : Type u_4
Rₘ : Type u_6
inst✝³ : CommRing R
inst✝² : CommRing Rₘ
M : Submonoid R
inst✝¹ : Algebra R Rₘ
inst✝ : IsLocalization M Rₘ
Q : Type (max u_4 u_6)
x✝¹ : CommRing Q
x✝ : Algebra R Q
I : Ideal Q
e : I ^ 2 = ⊥
f : Rₘ →ₐ[R] Q ⧸ I
this : ∀ (x : ↥M), IsUnit ((algebraMap R Q) ↑x)
⊢ ∃ a, (Ideal.Quotient.mkₐ R I).comp a = f
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
g✝ : S →ₐ[R] P
f : P →ₐ[R] S
hf' : RingHom.ker f ^ 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
a b : P
⊢ (a - g (f a)) * (b - g (f b)) = 0

Tactic:
rw [← Ideal.mem_bot, ← hf', pow_two]

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
g✝ : S →ₐ[R] P
f : P →ₐ[R] S
hf' : RingHom.ker f ^ 2 = ⊥
g : S →ₐ[R] P
hg : f.comp g = AlgHom.id R S
a b : P
⊢ (a - g (f a)) * (b - g (f b)) ∈ RingHom.ker f * RingHom.ker f
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
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S) (σ x) = x
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
a b : S
x y : S ⊗[P] Ω[P⁄R]
⊢ ↑(l x) * ↑(l y) = 0

Tactic:
rw [← Ideal.mem_bot, ← hf', pow_two]

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
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S) (σ x) = x
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
a b : S
x y : S ⊗[P] Ω[P⁄R]
⊢ ↑(l x) * ↑(l y) ∈ RingHom.ker (algebraMap P S) * RingHom.ker (algebraMap P S)
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)
l : { l // l ∘ₗ kerToTensor R P S = LinearMap.id }
p s : P
x y : S ⊗[P] Ω[P⁄R]
⊢ ↑(↑l x) * ↑(↑l y) = 0

Tactic:
rw [← Ideal.mem_bot, ← hf', pow_two]

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)
l : { l // l ∘ₗ kerToTensor R P S = LinearMap.id }
p s : P
x y : S ⊗[P] Ω[P⁄R]
⊢ ↑(↑l x) * ↑(↑l y) ∈ RingHom.ker (algebraMap P S) * RingHom.ker (algebraMap P S)
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: A : Type u_2
inst✝⁵ : CommRing A
B : Type u_4
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : EssFiniteType A B
inst✝¹ : FormallyUnramified A B
p : Ideal A
inst✝ : p.IsMaximal
⊢ (Ideal.map (algebraMap A B) p).IsRadical

Tactic:
let : Field (A ⧸ p) := Ideal.Quotient.field p
  rw [Ideal.isRadical_iff_quotient_reduced]
  exact Algebra.FormallyUnramified.isReduced_of_field (A ⧸ p) (B ⧸ p.map (algebraMap A B))

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

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

Tactic:
Module.length_eq_of_surjective (R := Sq ⧸ p.map (algebraMap R Sq)) Quotient.mk_surjective,

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

Goal state before:
pp: case pos
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
hp0 : map (algebraMap R S) p ≠ ⊥
hq : q.IsPrime
hq0 : q ≠ ⊥
⊢ q.ramificationIdx R = Multiset.count q (factors (map (algebraMap R S) p))

Tactic:
rw [← ramificationIdx'_eq_ramificationIdx' p q hp0, ramificationIdx'_eq_factors_count hp0 ‹_› hq0]

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
r : Ideal S := comap Algebra.TensorProduct.includeRight q.asIdeal
this : Algebra (Localization.AtPrime p) (Localization.AtPrime r) := Localization.AtPrime.algebraOfLiesOver p r
Rp : Type u_1 := Localization.AtPrime p
Sq : Type (max u_1 u_2) := Localization.AtPrime q.asIdeal
Sr : Type u_2 := Localization.AtPrime r
κp : Type u_1 := p.ResidueField
κr : Type u_2 := r.ResidueField
A : Type u_2 := Sr ⧸ map (algebraMap R Sr) p
⊢ length Sr A * ↑(finrank κp κr) = length Sr A * length κp κr

Tactic:
length_eq_finrank

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
r : Ideal S := comap Algebra.TensorProduct.includeRight q.asIdeal
this : Algebra (Localization.AtPrime p) (Localization.AtPrime r) := Localization.AtPrime.algebraOfLiesOver p r
Rp : Type u_1 := Localization.AtPrime p
Sq : Type (max u_1 u_2) := Localization.AtPrime q.asIdeal
Sr : Type u_2 := Localization.AtPrime r
κp : Type u_1 := p.ResidueField
κr : Type u_2 := r.ResidueField
A : Type u_2 := Sr ⧸ map (algebraMap R Sr) p
⊢ length Sr A * ↑(finrank κp κr) = length Sr A * ↑(finrank κp κr)
Module: Mathlib.RingTheory.RamificationInertia.Ramification

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

Tactic:
rw [hg, ramificationIdx_eq p q, ramificationIdx_eq p (q.map f₀),
      e.toLinearEquiv.length_eq, Module.length_eq_of_surjective f.surjective]

Goal state after:
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 = ⊤
a b : S → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S) (a x) = x * (algebraMap R S) (b x)
r : R
hrp : r ∉ p
hr : ∀ (r' : R), r ∣ r' → Function.Injective ⇑(awayMap (algebraMap R S) r')
r' : R
hr' : r * ∏ i ∈ s, b i ∣ r'
⊢ (IsScalarTower.toAlgHom R S (Away ((Algebra.ofId R S) r'))).range ≤ (awayMapₐ (Algebra.ofId R S) r').range

Tactic:
← Algebra.map_top,

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 = ⊤
a b : S → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S) (a x) = x * (algebraMap R S) (b x)
r : R
hrp : r ∉ p
hr : ∀ (r' : R), r ∣ r' → Function.Injective ⇑(awayMap (algebraMap R S) r')
r' : R
hr' : r * ∏ i ∈ s, b i ∣ r'
⊢ Subalgebra.map (IsScalarTower.toAlgHom R S (Away ((Algebra.ofId R S) r'))) ⊤ ≤ (awayMapₐ (Algebra.ofId R S) r').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
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
x : H1Cotangent R S
⊢ (Extension.H1Cotangent.equivOfFormallySmooth (Extension.ofSurjective (IsLocalization.liftAlgHom ⋯) ⋯)
        (Generators.self R T).toExtension)
      ((Extension.H1Cotangent.map
          {
            toRingHom :=
              algebraMap (Generators.self R S).toExtension.Ring
                (Localization (Submonoid.comap (algebraMap (Generators.self R S).toExtension.Ring S) M)),
            toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ })
        x) =
    (H1Cotangent.map R R S T) x

Tactic:
let P : Extension R S := (Generators.self R S).toExtension

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
x : H1Cotangent R S
P : Extension R S := (Generators.self R S).toExtension
⊢ (Extension.H1Cotangent.equivOfFormallySmooth (Extension.ofSurjective (IsLocalization.liftAlgHom ⋯) ⋯)
        (Generators.self R T).toExtension)
      ((Extension.H1Cotangent.map
          {
            toRingHom :=
              algebraMap (Generators.self R S).toExtension.Ring
                (Localization (Submonoid.comap (algebraMap (Generators.self R S).toExtension.Ring S) M)),
            toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ })
        x) =
    (H1Cotangent.map R R S T) x
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case mp
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
w : ℕ
y : M
hy : y ∈ N₁
z : M
hz : z ∈ N₂
h : ∀ a ∈ I ^ w, a • (y + z) = 0
⊢ ∃ y_1,
    ((∃ n, ∀ a ∈ I ^ n, a • y_1 = 0) ∧ y_1 ∈ N₁) ∧
      ∃ z_1, ((∃ n, ∀ a ∈ I ^ n, a • z_1 = 0) ∧ z_1 ∈ N₂) ∧ y_1 + z_1 = y + z

Tactic:
refine ⟨y, ⟨⟨w, fun a ha ↦ ?_⟩, by simp [hy]⟩, z, ⟨⟨w, fun a ha ↦ ?_⟩, by simp [hz]⟩, rfl⟩

Goal state after:
case mp.refine_1
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
w : ℕ
y : M
hy : y ∈ N₁
z : M
hz : z ∈ N₂
h : ∀ a ∈ I ^ w, a • (y + z) = 0
a : A
ha : a ∈ I ^ w
⊢ a • y = 0

case mp.refine_2
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
w : ℕ
y : M
hy : y ∈ N₁
z : M
hz : z ∈ N₂
h : ∀ a ∈ I ^ w, a • (y + z) = 0
a : A
ha : a ∈ I ^ w
⊢ a • z = 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)
ε : ℚ
ε0 : ε > 0
j : ℕ
ij : j ≥ ⌈ε⁻¹⌉₊
k : ℕ
ik : k ≥ ⌈ε⁻¹⌉₊
⊢ ↑(f j) / ↑j - ↑(f k) / ↑k < ε

Tactic:
replace ij := le_trans (Nat.le_ceil _) (Nat.cast_le.2 ij)

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
j k : ℕ
ik : k ≥ ⌈ε⁻¹⌉₊
ij : ε⁻¹ ≤ ↑j
⊢ ↑(f j) / ↑j - ↑(f k) / ↑k < ε
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:
by
    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.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: s : Set ℝ
hs : ∃ x ∈ s, x ≤ 0
⊢ sInf s ≤ 0

Tactic:
by
  classical
  obtain ⟨x, hxs, hx⟩ := hs
  exact dite _ (fun h ↦ csInf_le_of_le h hxs hx) fun h ↦ (sInf_of_not_bddBelow h).le

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

Goal state before:
pp: n : ℕ
r : ℝ
⊢ ↑n ≤ r.toNNReal ↔ ↑n ≤ r ∨ n = 0

Tactic:
by
  simpa [n.cast_nonneg.ge_iff_eq'] using toNNReal_le_toNNReal_iff' (r := n)

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

Goal state before:
pp: case inl
r : ℝ
hr : 0 ≤ r
⊢ ∃ x, r = ↑x ∨ r = -↑x

Tactic:
rw [← neg_neg r]

Goal state after:
case inl
r : ℝ
hr : 0 ≤ r
⊢ ∃ x, - -r = ↑x ∨ - -r = -↑x
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case inr
r : ℝ
hr : 0 ≤ -r
⊢ ∃ x, r = ↑x ∨ r = -↑x

Tactic:
rw [← neg_neg r]

Goal state after:
case inr
r : ℝ
hr : 0 ≤ -r
⊢ ∃ x, - -r = ↑x ∨ - -r = -↑x
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: a b : ℝ≥0∞
ha : a = ∞
⊢ (a + b).toReal ≤ a.toReal + b.toReal

Tactic:
by simp only [ha, top_add, toReal_top, zero_add, toReal_nonneg]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ 1 + if y = 0 then 0 else 1

Tactic:
refine le_add_of_le_of_nonneg ?_ ?_ <;> split_ifs

Goal state after:
case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝ : x + y = 0
⊢ 0 ≤ 1

case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝ : ¬x + y = 0
⊢ 1 ≤ 1

case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝ : y = 0
⊢ 0 ≤ 0

case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 0
h✝ : ¬y = 0
⊢ 0 ≤ 1
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p q f g : NonarchAddGroupSeminorm E
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by obtain ⟨⟨_, _⟩, _, _⟩ := f; cases g; congr

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
⊢ (if x * y = 1 then 0 else 1) ≤ 1 + if y = 1 then 0 else 1

Tactic:
refine le_add_of_le_of_nonneg ?_ ?_ <;> split_ifs

Goal state after:
case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
h✝ : x * y = 1
⊢ 0 ≤ 1

case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
h✝ : ¬x * y = 1
⊢ 1 ≤ 1

case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
h✝ : y = 1
⊢ 0 ≤ 0

case neg
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : ¬x = 1
h✝ : ¬y = 1
⊢ 0 ≤ 1
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 α
x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
hax : a ≤ x
hxb : x ≤ b
⊢ x ∈ ⊥

Tactic:
have h' : x ∈ ordSeparatingSet s t := ⟨mem_iUnion₂.2 ⟨a, has, ha⟩, mem_iUnion₂.2 ⟨b, hbt, hb⟩⟩

Goal state after:
case inr.inr
α✝ : 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ᶜ
hb : [[b, x]] ⊆ sᶜ
hsub : [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
hax : a ≤ x
hxb : x ≤ b
h' : x ∈ s.ordSeparatingSet t
⊢ x ∈ ⊥
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: a : ℝ≥0∞
⊢ a * a < ∞ ↔ a < ∞

Tactic:
by
  rw [ENNReal.mul_lt_top_iff, and_self, or_self, or_iff_left_iff_imp]
  rintro rfl
  exact zero_lt_top

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

Goal state before:
pp: case inl
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ∞
hab : a ≤ b
⊢ (a - b) * c = a * c - b * c

pp: case inr
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ∞
hab : b < a
⊢ (a - b) * c = a * c - b * c

Tactic:
· simp [hab, mul_left_mono hab, tsub_eq_zero_of_le]

Goal state after:
case inr
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ ∞
hab : b < a
⊢ (a - b) * c = a * c - b * c
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ ↑x
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P ↑x ↑y
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P ↑x ⊤
neg_bot : ∀ x < 0, P ↑x ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ ↑x
bot_bot : P ⊥ ⊥
x : ℝ
⊢ P ↑x ⊥

Tactic:
by
    rcases lt_trichotomy x 0 with (hx | rfl | hx)
    exacts [neg_bot x hx, zero_bot, pos_bot x hx]

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

Goal state before:
pp: x : EReal
hx : 0 ≤ x
⊢ ↑x.toENNReal = x

Tactic:
by
  rw [toENNReal]
  by_cases h_top : x = ⊤
  · rw [if_pos h_top, h_top]
    rfl
  rw [if_neg h_top]
  simp only [coe_ennreal_ofReal, hx, toReal_nonneg, max_eq_left]
  exact coe_toReal h_top fun _ ↦ by simp_all only [le_bot_iff, zero_ne_bot]

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

Goal state before:
pp: m n : ℕ
⊢ ↑m < ↑n ↔ m < n

Tactic:
by
  rw [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, EReal.coe_lt_coe_iff, Nat.cast_lt]

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

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

pp: case mpr.right
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ x < ∞

Tactic:
· apply lt_of_lt_of_le _ hn
      exact ENNReal.zpow_pos (zero_lt_one.trans hy).ne' h'y _

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
⊢ ContinuousAt f b ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, edist (f x) (f b) < ε

Tactic:
by
  rw [ContinuousAt, tendsto_nhds]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
⊢ ContinuousAt f b ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, dist (f x) (f b) < ε

Tactic:
by
  rw [ContinuousAt, tendsto_nhds]

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

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

Tactic:
rw [Finset.Ico_self, Finset.sum_empty, edist_self]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t

Tactic:
apply UniformSpace.subset_countable_closure_of_almost_dense_set
  intro U hU
  obtain ⟨ε, hε, hεU⟩ := uniformity_basis_edist_le.mem_iff.1 hU
  obtain ⟨t, tC, ht⟩ := hs ε hε
  refine ⟨t, tC, ht.trans (iUnion₂_mono fun x hx y hy => UniformSpace.ball_mono hεU x ?_)⟩
  rwa [mem_closedEBall, edist_comm] at hy

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

Goal state before:
pp: case inr.inr.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α × β
r : ℝ
hr : 0 < r
x' : α
y' : β
⊢ dist x' x.1 = r → (dist y' x.2 ≤ dist x' x.1 ↔ dist y' x.2 ≤ r)

Tactic:
rintro rfl; rfl

Goal state after: