mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case h₃.inl
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp✝ : Prime p
this✝¹ : IsAddTorsionFree S
this✝ : CharZero S
hpMax : (span {p}).IsMaximal
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH : p ∣ ↑(absNorm I) → ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I
this : P.IsMaximal
q n : ℕ
hn : 0 < n
hqP : ↑q ∈ P
hq : Nat.Prime q
H : absNorm P = q ^ n
m : ℕ
hmn : m ≤ n
hp : Associated p (↑q ^ m)
⊢ p ∈ under ℤ P

Tactic:
have : m ≠ 0 := fun h ↦ hpMax.ne_top (Ideal.span_singleton_eq_top.mpr (by simpa [h] using hp))

Goal state after:
case h₃.inl
S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
p : ℤ
hp✝ : Prime p
this✝² : IsAddTorsionFree S
this✝¹ : CharZero S
hpMax : (span {p}).IsMaximal
I P : Ideal S
hI' : I ≠ 0
hP : Prime P
IH : p ∣ ↑(absNorm I) → ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I
this✝ : P.IsMaximal
q n : ℕ
hn : 0 < n
hqP : ↑q ∈ P
hq : Nat.Prime q
H : absNorm P = q ^ n
m : ℕ
hmn : m ≤ n
hp : Associated p (↑q ^ m)
this : m ≠ 0
⊢ p ∈ under ℤ P
Module: Mathlib.RingTheory.Spectrum.Prime.Jacobson

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : IsOpen {x} → IsClopen {x}
tfae_2_to_3 : IsClopen {x} → IsClosed {x} ∧ StableUnderGeneralization {x}
h₁ : IsMax x
h₂ : StableUnderGeneralization {x}
this : {x} = (⋃ p ∈ {p | IsMin p ∧ p ≠ x}, closure {p})ᶜ
⊢ {p | IsMin p ∧ p ≠ x}.Finite

Tactic:
exact (finite_setOfPred_isMin R).subset fun x h ↦ h.1

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

Goal state before:
pp: case neg
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp : map f p ≠ ⊥
hP : P.IsPrime
hP₂ : ¬P = ⊥
⊢ emultiplicity P (map f p) = ↑(Multiset.count P (normalizedFactors (map f p)))

Tactic:
← normalize_eq P,

Goal state after:
case neg
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp : map f p ≠ ⊥
hP : P.IsPrime
hP₂ : ¬P = ⊥
⊢ emultiplicity (normalize P) (map f p) = ↑(Multiset.count (normalize P) (normalizedFactors (map f p)))
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R B
I : Ideal B
inst✝ : FormallyUnramified R A
hI : ⨅ i, I ^ i = ⊥
g₁ g₂ : A →ₐ[R] B
H : ∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)
this : ∀ (i : ℕ), (Ideal.Quotient.mkₐ R (I ^ i)).comp g₁ = (Ideal.Quotient.mkₐ R (I ^ i)).comp g₂
x : A
⊢ g₁ x = g₂ x

Tactic:
rw [← sub_eq_zero, ← Ideal.mem_bot, ← hI, Ideal.mem_iInf]

Goal state after:
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R B
I : Ideal B
inst✝ : FormallyUnramified R A
hI : ⨅ i, I ^ i = ⊥
g₁ g₂ : A →ₐ[R] B
H : ∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)
this : ∀ (i : ℕ), (Ideal.Quotient.mkₐ R (I ^ i)).comp g₁ = (Ideal.Quotient.mkₐ R (I ^ i)).comp g₂
x : A
⊢ ∀ (i : ℕ), g₁ x - g₂ x ∈ I ^ i
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 S
inst✝³ : p.IsPrime
inst✝² : IsArtinianRing R
inst✝¹ : EssFiniteType R S
inst✝ : QuasiFiniteAt R p
⊢ ∃ f ∉ p, ↑(PrimeSpectrum.basicOpen f) = {{ asIdeal := p, isPrime := inst✝³ }}

Tactic:
by
  have : IsLocalizedModule p.primeCompl (.id (R := S) (M := Localization.AtPrime p)) :=
    ⟨IsLocalizedModule.map_units (Algebra.linearMap S (Localization.AtPrime p)),
      fun y ↦ ⟨⟨y, 1⟩, by simp⟩, by simpa using ⟨1, p.primeCompl.one_mem⟩⟩
  have : Module.Finite R (Localization.AtPrime p) := .of_quasiFinite
  have : Module.Finite S (Localization.AtPrime p) := .of_restrictScalars_finite R _ _
  have : IsArtinianRing (Localization.AtPrime p) := .of_finite R _
  have : IsNoetherianRing S := Algebra.EssFiniteType.isNoetherianRing R S
  have : Module.FinitePresentation S (Localization.AtPrime p) :=
    Module.finitePresentation_of_finite _ _
  obtain ⟨r, hrp, H⟩ := IsLocalizedModule.exists_isLocalizedModule_powers_of_finitePresentation
    p.primeCompl (Algebra.linearMap S (Localization.AtPrime p))
  have : IsLocalization (.powers r) (Localization.AtPrime p) :=
    (isLocalizedModule_iff_isLocalization' _ _).mp H
  let φ : Localization.Away r ≃ₐ[S] Localization.AtPrime p :=
    IsLocalization.algEquiv (.powers r) _ _
  refine ⟨r, hrp, subset_antisymm (fun q hrq ↦ ?_) (Set.singleton_subset_iff.mpr hrp)⟩
  obtain ⟨q, rfl⟩ := (PrimeSpectrum.localization_away_comap_range (Localization.Away r) r).ge hrq
  obtain ⟨q, rfl⟩ := (PrimeSpectrum.comapEquiv φ.toRingEquiv).symm.surjective q
  -- As Sₚ is an artinian local ring, its prime spectrum is a singleton.
  obtain rfl : q = IsLocalRing.closedPoint _ := Subsingleton.elim _ _
  ext1
  dsimp [-RingEquiv.symm_mk]
  rw [Ideal.comap_comap, ← AlgEquiv.toAlgHom_toRingHom, AlgHom.comp_algebraMap]
  exact IsLocalization.AtPrime.under_maximalIdeal _ _

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

Goal state before:
pp: R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
I : Ideal B
hI : IsNilpotent I
g : A →ₐ[R] B ⧸ I
⊢ ∃ f, (Ideal.Quotient.mkₐ R I).comp f = g

Tactic:
by
  revert g
  change Function.Surjective (Ideal.Quotient.mkₐ R I).comp
  revert ‹Algebra R B›
  apply Ideal.IsNilpotent.induction_on (S := B) I hI
  · intro B _ I hI _; exact FormallySmooth.comp_surjective R A I hI
  · intro B _ I J hIJ h₁ h₂ _ g
    let : ((B ⧸ I) ⧸ J.map (Ideal.Quotient.mk I)) ≃ₐ[R] B ⧸ J :=
      { (DoubleQuot.quotQuotEquivQuotSup I J).trans
          (Ideal.quotEquivOfEq (sup_eq_right.mpr hIJ)) with
        commutes' := fun x => rfl }
    obtain ⟨g', e⟩ := h₂ (this.symm.toAlgHom.comp g)
    obtain ⟨g', rfl⟩ := h₁ g'
    replace e := congr_arg this.toAlgHom.comp e
    conv_rhs at e =>
      rw [← AlgHom.comp_assoc, AlgEquiv.comp_symm, AlgHom.id_comp]
    exact ⟨g', e⟩

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

Goal state before:
pp: case mp
R : Type u_4
inst✝² : CommRing R
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Function.Surjective ⇑(algebraMap R A)
g : A →ₐ[R] R ⧸ RingHom.ker (ofId R A).toRingHom ^ 2
hg : (ofId R A).kerSquareLift.comp g = AlgHom.id R A
e : A ≃ₐ[R] R ⧸ RingHom.ker (algebraMap R A) ^ 2 := AlgEquiv.ofAlgHom g (ofId R A).kerSquareLift ⋯ hg
⊢ RingHom.ker ((↑↑e).comp (algebraMap R A)) = RingHom.ker (algebraMap R A)

Tactic:
RingHom.ker_comp_of_injective _ (by exact e.injective)

Goal state after:
case mp
R : Type u_4
inst✝² : CommRing R
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Function.Surjective ⇑(algebraMap R A)
g : A →ₐ[R] R ⧸ RingHom.ker (ofId R A).toRingHom ^ 2
hg : (ofId R A).kerSquareLift.comp g = AlgHom.id R A
e : A ≃ₐ[R] R ⧸ RingHom.ker (algebraMap R A) ^ 2 := AlgEquiv.ofAlgHom g (ofId R A).kerSquareLift ⋯ hg
⊢ RingHom.ker (algebraMap R A) = RingHom.ker (algebraMap R A)
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case add
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 σ
this✝ : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower (Q.comp P).Ring (Q.comp P).Ring T
x₁ x₂ : MvPolynomial (ι ⊕ σ) R
hx₁ :
  (δAux R Q) ((Q.ofComp P).toAlgHom x₁) =
    (LinearMap.baseChange T P.toExtension.toKaehler)
      ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) x₁)).2
hx₂ :
  (δAux R Q) ((Q.ofComp P).toAlgHom x₂) =
    (LinearMap.baseChange T P.toExtension.toKaehler)
      ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) x₂)).2
⊢ (δAux R Q) ((Q.ofComp P).toAlgHom (x₁ + x₂)) =
    (LinearMap.baseChange T P.toExtension.toKaehler)
      ((CotangentSpace.compEquiv Q P) (1 ⊗ₜ[(Q.comp P).Ring] (D R (Q.comp P).Ring) (x₁ + x₂))).2

Tactic:
simp only [map_add, hx₁, hx₂, tmul_add, Prod.snd_add]

Goal state after:
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
x y : P
h : (algebraMap P S) x = (algebraMap P S) y
⊢ x - y = ↑(l (1 ⊗ₜ[P] (D R P) x)) - ↑(l (1 ⊗ₜ[P] (D R P) y))

Tactic:
← Submodule.coe_sub,

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
x y : P
h : (algebraMap P S) x = (algebraMap P S) y
⊢ x - y = ↑(l (1 ⊗ₜ[P] (D R P) x) - l (1 ⊗ₜ[P] (D R P) y))
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 = ⊥
⊢ σ 0 - ↑(l (1 ⊗ₜ[P] (D R P) (σ 0))) = 0

Tactic:
simp [sectionOfRetractionKerToTensorAux_prop l hl (σ 0) 0 (by simp [hσ])]

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
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : Algebra.IsSeparable (ResidueField R) (ResidueField S)
H : Ideal.map (algebraMap R S) (maximalIdeal R) = maximalIdeal S
⊢ FormallyUnramified R S

Tactic:
constructor
  have : FormallyUnramified (ResidueField R) (ResidueField S) := .of_isSeparable _ _
  have : FormallyUnramified R (ResidueField S) := .comp _ (ResidueField R) _
  rw [← subsingleton_tensorProduct (R := S)]
  refine subsingleton_of_forall_eq 0 fun x ↦ ?_
  obtain ⟨x, rfl⟩ := (KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange R S
    (ResidueField S) Ideal.Quotient.mk_surjective x).mp (Subsingleton.elim _ _)
  obtain ⟨⟨x, hx⟩, rfl⟩ := Ideal.toCotangent_surjective _ x
  simp only [KaehlerDifferential.kerCotangentToTensor_toCotangent]
  replace hx : x ∈ Ideal.map (algebraMap R S) (maximalIdeal R) := by simpa [H] using hx
  induction hx using Submodule.span_induction with
  | zero => simp
  | mem x h => obtain ⟨x, hx, rfl⟩ := h; simp
  | add x y hx hy _ _ => simp [*, TensorProduct.tmul_add]
  | smul a x hx _ =>
    have : residue S x = 0 := by rwa [residue_eq_zero_iff, ← H]
    simp [*, TensorProduct.tmul_add, TensorProduct.smul_tmul', ← Algebra.algebraMap_eq_smul_one]

Goal state after:
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
⊢ q.ramificationIdx R = 1 ↔ Algebra.IsUnramifiedAt R q

Tactic:
by
  refine ⟨fun h ↦ ?_, fun _ ↦ ramificationIdx_eq_one q R⟩
  rw [ramificationIdx_def, ENat.toNat_eq_iff_eq_natCast, Nat.cast_one, Module.length_eq_one_iff,
    isSimpleModule_iff_isCoatom, ← Ideal.isMaximal_def, IsLocalRing.isMaximal_iff] at h
  let p := q.under R
  let Rp := Localization.AtPrime p
  let Sq := Localization.AtPrime q
  let := Localization.AtPrime.algebraOfLiesOver p q
  have := Algebra.EssFiniteType.of_comp R Rp Sq
  suffices Algebra.FormallyUnramified Rp Sq from Algebra.FormallyUnramified.comp R Rp Sq
  rw [Algebra.FormallyUnramified.iff_map_maximalIdeal_eq,
    ← Localization.AtPrime.map_eq_maximalIdeal, map_map, ← IsScalarTower.algebraMap_eq]
  exact ⟨Algebra.IsAlgebraic.isSeparable_of_perfectField, h⟩

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ a ∈ s.biUnion S, f a = ∑ t, (-1) ^ (#↑t + 1) • ∑ a ∈ (↑t).inf' ⋯ S, f a

Tactic:
classical
  rw [← sub_eq_zero]
  calc
    ∑ a ∈ s.biUnion S, f a - ∑ t : s.powerset.filter (·.Nonempty),
      (-1) ^ (#t.1 + 1) • ∑ a ∈ t.1.inf' (mem_filter.1 t.2).2 S, f a
      = ∑ t : s.powerset.filter (·.Nonempty),
          (-1) ^ #t.1 • ∑ a ∈ t.1.inf' (mem_filter.1 t.2).2 S, f a +
          ∑ t ∈ s.powerset.filter (¬ ·.Nonempty), (-1) ^ #t • ∑ a ∈ s.biUnion S, f a := by
      simp [sub_eq_neg_add, ← sum_neg_distrib, filter_eq', pow_succ]
    _ = ∑ t ∈ s.powerset, (-1) ^ #t •
          if ht : t.Nonempty then ∑ a ∈ t.inf' ht S, f a else ∑ a ∈ s.biUnion S, f a := by
      rw [← sum_attach (filter ..)]; simp [sum_dite]
    _ = ∑ a ∈ s.biUnion S, (∏ i ∈ s, (1 - Set.indicator (S i) 1 a : ℤ)) • f a := by
      simp only [Int.reduceNeg, prod_sub, sum_comm (s := s.biUnion S), sum_smul, mul_assoc]
      congr! with t
      split_ifs with ht
      · obtain ⟨i, hi⟩ := ht
        simp only [prod_const_one, prod_indicator_apply]
        simp only [smul_sum, Set.indicator, Set.mem_iInter, mem_coe, Pi.one_apply, mul_ite, mul_one,
          mul_zero, ite_smul, zero_smul, sum_ite, not_forall, sum_const_zero, add_zero]
        congr
        aesop
      · obtain rfl := not_nonempty_iff_eq_empty.1 ht
        simp
    _ = ∑ a ∈ s.biUnion S, (∏ i ∈ s,
          (Set.indicator (s.biUnion S) 1 a - Set.indicator (S i) 1 a) : ℤ) • f a := by
      congr! with t; rw [Set.indicator_of_mem ‹_›, Pi.one_apply]
    _ = 0 := by
      obtain rfl | hs := s.eq_empty_or_nonempty <;>
        simp [-coe_biUnion, prod_indicator_biUnion_finset_sub_indicator, *]

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

Goal state before:
pp: x : ℚ≥0
y : ℝ≥0
⊢ 0 ≤ x • ↑y

Tactic:
by rw [NNRat.smul_def]; exact mul_nonneg x.cast_nonneg y.2

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
v : HeightOneSpectrum R
hv : v ∈ {v | v.maxPowDividing I ≠ 1}
⊢ v ∈ {v | ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) ≠ 0}

Tactic:
h_zero

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
v : HeightOneSpectrum R
hv : v ∈ {v | v.maxPowDividing I ≠ 1}
h_zero : ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0
⊢ False
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ≥0
⊢ 1 < ↑r ↔ 1 < r

Tactic:
← coe_lt_coe,

Goal state after:
r : ℝ≥0
⊢ 1 < ↑r ↔ ↑1 < ↑r
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ≥0
⊢ ↑r < 1 ↔ r < 1

Tactic:
← coe_lt_coe,

Goal state after:
r : ℝ≥0
⊢ ↑r < 1 ↔ ↑r < ↑1
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

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

Tactic:
rcases H ε ε_pos with ⟨x, x_in, hx⟩
    exact csInf_lt_of_lt h x_in hx

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

Goal state before:
pp: r : ℝ
n : ℕ
⊢ ↑n < r.toNNReal ↔ ↑n < r

Tactic:
simpa only [not_le] using toNNReal_le_natCast.not

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

Goal state before:
pp: E : Type u_3
F : Type u_4
inst✝² : AddGroup E
inst✝¹ : FunLike F E ℝ
inst✝ : NonarchAddGroupSeminormClass F E
f : F
x y : E
⊢ f (x - y) ≤ max (f x) (f y)

Tactic:
sub_eq_add_neg,

Goal state after:
E : Type u_3
F : Type u_4
inst✝² : AddGroup E
inst✝¹ : FunLike F E ℝ
inst✝ : NonarchAddGroupSeminormClass F E
f : F
x y : E
⊢ f (x + -y) ≤ max (f x) (f y)
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ↑(p + q).toNNReal = ↑(p.toNNReal + q.toNNReal)

Tactic:
coe_inj,

Goal state after:
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ (p + q).toNNReal = p.toNNReal + q.toNNReal
Module: Mathlib.Data.ENNReal.Real

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

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

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

Goal state before:
pp: p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ↑p.toNNReal = ↑q.toNNReal ↔ p = q

Tactic:
coe_inj,

Goal state after:
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ p.toNNReal = q.toNNReal ↔ p = q
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: a : ℝ
b : ℝ≥0
⊢ ENNReal.ofReal a ≤ ↑b ↔ a ≤ (↑b).toReal

Tactic:
simpa [ENNReal.ofReal, ENNReal.toReal] using Real.toNNReal_le_iff_le_coe

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

Goal state before:
pp: m n : ℕ
⊢ ↑m - ↑↑n = ↑m - ↑n

Tactic:
coe_natCast

Goal state after:
m n : ℕ
⊢ ↑m - ↑n = ↑m - ↑n
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:
by
  simp [add_iInf]

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

Goal state before:
pp: x : ℝ
hx : 0 < ↑x
h'x : ↑x ≠ ⊤
⊢ 0 < (↑x).toReal

Tactic:
simpa using hx

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

Goal state before:
pp: x : ℝ
hx : ↑x < 0
h'x : ↑x ≠ ⊥
⊢ (↑x).toReal < 0

Tactic:
simpa using hx

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

Goal state before:
pp: case h
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑x ∈ Ioo 0 ⊤ ∧ (↑x).toReal = x

Tactic:
simpa using hx

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

Goal state before:
pp: case h
x : ℝ
hx : x ∈ Iio 0
⊢ ↑x ∈ Ioo ⊥ 0 ∧ (↑x).toReal = x

Tactic:
simpa using hx

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

Goal state before:
pp: x : ℝ≥0∞
⊢ (↑x).toENNReal = x

Tactic:
by
  by_cases h_top : x = ⊤
  · rw [h_top, coe_ennreal_top, toENNReal_top]
  rwa [toENNReal, if_neg _, toReal_coe_ennreal, ENNReal.ofReal_toReal_eq_iff]
  simp [h_top]

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

Goal state before:
pp: m n : ℕ
⊢ ↑(↑m * ↑n) = ↑↑m * ↑↑n

Tactic:
EReal.coe_mul

Goal state after:
m n : ℕ
⊢ ↑↑m * ↑↑n = ↑↑m * ↑↑n
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
h : a * b = c
⊢ b = c / a

Tactic:
by
    rw [← h, mul_div_assoc, ENNReal.mul_div_cancel ha ha']

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

Goal state before:
pp: case hp₁
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
exps : HeightOneSpectrum R → ℤ
⊢ ∀ (x y : FractionalIdeal R⁰ K), count K v x = 0 → count K v y = 0 → count K v (x * y) = 0

Tactic:
intro I I' hI hI'
    classical
    by_cases h : I ≠ 0 ∧ I' ≠ 0
    · rw [count_mul' K v, if_pos h, hI, hI', add_zero]
    · rw [count_mul' K v, if_neg h]

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:
rw [edist_comm] at h
    rw [← zero_add (edist x z), ← h]
    apply edist_triangle

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
J : Ideal R
hJ : J ≠ 0
⊢ ↑((Associates.mk v.asIdeal).count (Associates.mk ⊤).factors) = 0

pp: case hI
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
J : Ideal R
hJ : J ≠ 0
⊢ ↑J ≠ 0

pp: case h_aJ
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
J : Ideal R
hJ : J ≠ 0
⊢ ↑J = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑J

Tactic:
Nat.cast_eq_zero,

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
J : Ideal R
hJ : J ≠ 0
⊢ (Associates.mk v.asIdeal).count (Associates.mk ⊤).factors = 0

case hI
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
J : Ideal R
hJ : J ≠ 0
⊢ ↑J ≠ 0

case h_aJ
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
J : Ideal R
hJ : J ≠ 0
⊢ ↑J = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑J
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
a : α
s : Set α
⊢ Tendsto f (𝓝[s] a) (𝓝 (f a)) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → edist (f x) (f a) < ε

Tactic:
tendsto_nhdsWithin_nhds

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
a : α
s : Set α
⊢ (∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) (f a) < ε) ↔
    ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → edist (f x) (f a) < ε
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
s : Set α
⊢ ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∃ δ > 0, ∀ a ∈ s, edist a b < δ → edist (f a) (f b) < ε

Tactic:
simp [ContinuousOn, continuousWithinAt_iff]

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

Goal state before:
pp: x : ℝ≥0∞
x_ne_zero : x ≠ 0
x_ne_top : x ≠ ∞
m n : ℤ
⊢ x ^ (m - n) = x ^ m * (x ^ n)⁻¹

Tactic:
sub_eq_add_neg,

Goal state after:
x : ℝ≥0∞
x_ne_zero : x ≠ 0
x_ne_top : x ≠ ∞
m n : ℤ
⊢ x ^ (m + -n) = x ^ m * (x ^ n)⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0∞
⊢ IsUnit a ↔ a ≠ 0 ∧ a ≠ ∞

Tactic:
refine ⟨fun ha ↦ ⟨ha.ne_zero, ?_⟩,
    fun ha ↦ ⟨⟨a, a⁻¹, ENNReal.mul_inv_cancel ha.1 ha.2, ENNReal.inv_mul_cancel ha.1 ha.2⟩, rfl⟩⟩
  obtain ⟨u, rfl⟩ := ha
  rintro hu
  have := congr($hu * u⁻¹)
  simp at this

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

Goal state before:
pp: s : Set ℝ≥0∞
⊢ (sInf s)⁻¹ = ⨆ a ∈ s, a⁻¹

Tactic:
simp [sInf_eq_iInf, inv_iInf]

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

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
⊢ 𝓤 PUnit.{u + 1} = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | 0 < ε}

Tactic:
simp +contextual [principal_univ, eq_top_of_neBot (𝓤 PUnit)]

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

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ ↑x⁻¹.toNNReal = ↑x.toNNReal⁻¹

Tactic:
coe_inj,

Goal state after:
x : ℝ
hx : 0 < x
⊢ x⁻¹.toNNReal = x.toNNReal⁻¹
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
a : α
s : Set α
⊢ Tendsto f (𝓝[s] a) (𝓝 (f a)) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) (f a) < ε

Tactic:
tendsto_nhdsWithin_nhds

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
a : α
s : Set α
⊢ (∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) (f a) < ε) ↔
    ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) (f a) < ε
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
s : Set α
⊢ ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∃ δ > 0, ∀ a ∈ s, dist a b < δ → dist (f a) (f b) < ε

Tactic:
simp [ContinuousOn, continuousWithinAt_iff]

Goal state after: