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

Goal state before:
pp: case inl
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 S T
inst✝⁹ : Algebra R T
inst✝⁸ : IsScalarTower R S T
inst✝⁷ : IsDedekindDomain S
inst✝⁶ : IsDedekindDomain T
inst✝⁵ : IsDomain R
inst✝⁴ : IsTorsionFree R S
inst✝³ : IsTorsionFree S T
P : Ideal S
Q : Ideal T
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : P.LiesOver ⊥
⊢ ⊥.ramificationIdx' Q = ⊥.ramificationIdx' P * P.ramificationIdx' Q

pp: case inr
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 S T
inst✝⁹ : Algebra R T
inst✝⁸ : IsScalarTower R S T
inst✝⁷ : IsDedekindDomain S
inst✝⁶ : IsDedekindDomain T
inst✝⁵ : IsDomain R
inst✝⁴ : IsTorsionFree R S
inst✝³ : IsTorsionFree S T
p : Ideal R
P : Ideal S
Q : Ideal T
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : P.LiesOver p
hp : p ≠ ⊥
⊢ p.ramificationIdx' Q = p.ramificationIdx' P * P.ramificationIdx' Q

Tactic:
· simp

Goal state after:
case inr
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 S T
inst✝⁹ : Algebra R T
inst✝⁸ : IsScalarTower R S T
inst✝⁷ : IsDedekindDomain S
inst✝⁶ : IsDedekindDomain T
inst✝⁵ : IsDomain R
inst✝⁴ : IsTorsionFree R S
inst✝³ : IsTorsionFree S T
p : Ideal R
P : Ideal S
Q : Ideal T
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : P.LiesOver p
hp : p ≠ ⊥
⊢ p.ramificationIdx' Q = p.ramificationIdx' P * P.ramificationIdx' Q
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
inst✝⁶ : FiniteType R S
p : Ideal R
inst✝⁵ : p.IsPrime
q : Ideal S
inst✝⁴ : q.IsPrime
inst✝³ : q.LiesOver p
inst✝² : QuasiFiniteAt R q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
⊢ Function.Surjective
    ⇑(TensorProduct.lift (ofId p.ResidueField q.ResidueField) (IsScalarTower.toAlgHom R S q.ResidueField) ⋯)

Tactic:
let q' : Ideal (p.Fiber S) := (PrimeSpectrum.primesOverOrderIsoFiber R S p ⟨q, ‹_›, ‹_›⟩).asIdeal
  have hq' : q = q'.comap Algebra.TensorProduct.includeRight.toRingHom :=
    congr($((PrimeSpectrum.primesOverOrderIsoFiber R S p).symm_apply_apply ⟨q, ‹_›, ‹_›⟩).1).symm
  have : Algebra.QuasiFiniteAt p.ResidueField q' := .baseChange q _ hq'
  have : q'.IsMaximal := (PrimeSpectrum.isClosed_singleton_iff_isMaximal _).mp
    (QuasiFiniteAt.isClopen_singleton (R := p.ResidueField) _).isClosed
  refine .of_comp_left ?_
    (p.surjectiveOnStalks_residueField.baseChange'.residueFieldMap_bijective q q' hq').1
  rw [← AlgHom.coe_toRingHom, ← RingHom.coe_comp]
  convert! q'.algebraMap_residueField_surjective
  ext <;> simp [IsScalarTower.algebraMap_apply R S q.ResidueField]

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
H :
  ∀ ⦃B : Type (max u v)⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Bijective (Ideal.Quotient.mkₐ R I).comp
⊢ ∀ ⦃B : Type (max u v)⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp

Tactic:
by aesop (add safe Function.Bijective.injective)

Goal state after:
Module: Mathlib.RingTheory.Unramified.Locus

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
⊢ Module.support A Ω[A⁄R] ⊆ PrimeSpectrum.zeroLocus {f} ↔ FormallyUnramified R (Localization.Away f)

Tactic:
← LocalizedModule.subsingleton_iff_support_subset,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
⊢ Subsingleton (LocalizedModule.Away f Ω[A⁄R]) ↔ FormallyUnramified R (Localization.Away 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
x y : P
h : (algebraMap P S) x = (algebraMap P S) y
⊢ x - ↑(l (1 ⊗ₜ[P] (D R P) x)) = y - ↑(l (1 ⊗ₜ[P] (D R P) y))

Tactic:
sub_eq_iff_eq_add,

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) y)) + ↑(l (1 ⊗ₜ[P] (D R P) x))
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FormallyUnramified K L
inst✝ : EssFiniteType K L
⊢ Algebra.IsSeparable K L

Tactic:
have := finite_of_free (R := K) (S := L)
  rw [← separableClosure.eq_top_iff]
  have := of_restrictScalars K (separableClosure K L) L
  have := EssFiniteType.of_comp K (separableClosure K L) L
  ext
  change _ ↔ _ ∈ (⊤ : Subring _)
  rw [← range_eq_top_of_isPurelyInseparable (separableClosure K L) L]
  simp

Goal state after:
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: 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₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
inst✝ : Flat S T
f : W.Hom Q
g : P.Hom W
⊢ Function.Exact ⇑(LinearMap.liftBaseChange T (Extension.H1Cotangent.map g.toExtensionHom))
    ⇑(Extension.H1Cotangent.map f.toExtensionHom)

Tactic:
rw [← LinearEquiv.conj_exact_iff_exact _ _ (H1Cotangent.equiv W (Q.comp P))]

Goal state after:
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₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
inst✝ : Flat S T
f : W.Hom Q
g : P.Hom W
⊢ Function.Exact ⇑(↑(equiv W (Q.comp P)) ∘ₗ LinearMap.liftBaseChange T (Extension.H1Cotangent.map g.toExtensionHom))
    ⇑(Extension.H1Cotangent.map f.toExtensionHom ∘ₗ ↑(equiv W (Q.comp P)).symm)
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
⊢ (g • q).ramificationIdx R = q.ramificationIdx R

Tactic:
· let p := q.under R
    let f₀ := MulSemiringAction.toAlgAut G R S g
    have hg : g • q = q.map f₀ := q.pointwise_smul_def
    let Sq := Localization.AtPrime q
    let Sq' := Localization.AtPrime (q.map f₀)
    let f : Sq ≃ₐ[R] Sq' :=
      Localization.localAlgEquiv q (q.map f₀) f₀ (comap_map_of_bijective f₀ f₀.bijective).symm
    let : Algebra Sq Sq' := f.toRingHom.toAlgebra
    have : IsScalarTower R Sq Sq' := IsScalarTower.of_algHom f.toAlgHom
    let e : (Sq ⧸ p.map (algebraMap R Sq)) ≃ₐ[Sq] Sq' ⧸ p.map (algebraMap R Sq') :=
      Ideal.quotientEquivAlg _ _ (AlgEquiv.ofBijective (Algebra.ofId Sq Sq') f.bijective)
        (by rw [IsScalarTower.algebraMap_eq R Sq Sq', Ideal.map_map,
          ← AlgEquiv.toAlgHom_toRingHom, AlgEquiv.toAlgHom_ofBijective, Algebra.toRingHom_ofId])
    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 = ⊤
x : S
a b : R
hbp : b ∉ p
c : S
hcq : c ∉ q
hc : c * (algebraMap R S) a = c * (x * (algebraMap R S) b)
d : R
hd : d ∉ p
e : S
he : (algebraMap R S) d = c * e
⊢ (algebraMap R S) (d * a) = x * (algebraMap R S) (d * b)

Tactic:
by grind

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

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
t : Finset ι
hts : t ⊆ s
ht : t.Nonempty
⊢ (-1) ^ #t • 0 = 0

pp: case neg.h
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
t : Finset ι
hts : t ⊆ s
ht : t.Nonempty
⊢ a ∉ ⋂ i ∈ t, S i

Tactic:
· simp

Goal state after:
case neg.h
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
t : Finset ι
hts : t ⊆ s
ht : t.Nonempty
⊢ a ∉ ⋂ i ∈ t, S i
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case inl
⊢ ↑(sSup ∅) = sSup (toReal '' ∅)

pp: case inr
s : Set ℝ≥0
hs : s.Nonempty
⊢ ↑(sSup s) = sSup (toReal '' s)

Tactic:
· simp

Goal state after:
case inr
s : Set ℝ≥0
hs : s.Nonempty
⊢ ↑(sSup s) = sSup (toReal '' s)
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case inl
⊢ sSup (-∅) = -sInf ∅

pp: case inr
s : Set ℝ
hn : s.Nonempty
⊢ sSup (-s) = -sInf s

Tactic:
· simp

Goal state after:
case inr
s : Set ℝ
hn : s.Nonempty
⊢ sSup (-s) = -sInf s
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case neg
s : Set ℝ
hn : s.Nonempty
hb : ¬BddBelow s
⊢ sSup (-s) = -sInf ∅

Tactic:
Real.sInf_empty,

Goal state after:
case neg
s : Set ℝ
hn : s.Nonempty
hb : ¬BddBelow s
⊢ sSup (-s) = -0
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
⊢ False

Tactic:
have hw_prime : Prime w.asIdeal := Ideal.prime_of_isPrime w.ne_bot w.isPrime

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
⊢ False
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:
exact (Finset.mem_erase.mp hw).1 (HeightOneSpectrum.ext hvw.symm)

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

Goal state before:
pp: case inl
ι : Sort u_1
f : ι → ℝ≥0
hf : BddAbove (range f)
h✝ : IsEmpty ι
⊢ ⨆ i, f i = 0 ↔ ∀ (i : ι), f i = 0

pp: case inr
ι : Sort u_1
f : ι → ℝ≥0
hf : BddAbove (range f)
h✝ : Nonempty ι
⊢ ⨆ i, f i = 0 ↔ ∀ (i : ι), f i = 0

Tactic:
· simp

Goal state after:
case inr
ι : Sort u_1
f : ι → ℝ≥0
hf : BddAbove (range f)
h✝ : Nonempty ι
⊢ ⨆ i, f i = 0 ↔ ∀ (i : ι), f i = 0
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ 2 ^ (2 * k) = (1 / ↑k * ↑k + 1) ^ (2 * k)

Tactic:
simp [posk.ne']

Goal state after:
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ 2 = 1 + 1
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case inl
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q : GroupSeminorm E
f : F →* E
x y : E
h : BddAbove ∅
⊢ ⨆ p, ↑p (x * y) ≤ (⨆ p, ↑p x) + ⨆ p, ↑p y

pp: case inr
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
⊢ ⨆ p, ↑p (x * y) ≤ (⨆ p, ↑p x) + ⨆ p, ↑p y

Tactic:
· simp

Goal state after:
case inr
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
⊢ ⨆ p, ↑p (x * y) ≤ (⨆ p, ↑p x) + ⨆ p, ↑p y
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: a b : ℝ≥0∞
h : ∀ (ε : ℝ≥0), 0 < ε → b < ∞ → a ≤ b + ↑ε
⊢ a ≤ b

Tactic:
by
  contrapose! h
  rcases lt_iff_exists_add_pos_lt.1 h with ⟨r, hr0, hr⟩
  exact ⟨r, hr0, h.trans_le le_top, hr⟩

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

Goal state before:
pp: a : ℝ≥0∞
⊢ ⋃ n, Icc a ↑n = Ici a \ {∞}

Tactic:
simp only [← Ici_inter_Iic, ← inter_iUnion, iUnion_Iic_coe_nat, sdiff_eq]

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

Goal state before:
pp: r : ℝ
⊢ ENNReal.ofReal r ≠ 0 ↔ 0 < r

Tactic:
rw [← pos_iff_ne_zero, ENNReal.ofReal_pos]

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

Goal state before:
pp: case inl
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 : NonarchAddGroupSeminorm E
x y : E
h : BddAbove ∅
⊢ ⨆ p, ↑p (x + y) ≤ max (⨆ p, ↑p x) (⨆ p, ↑p y)

pp: case inr
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 : NonarchAddGroupSeminorm E
s : Set (NonarchAddGroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
⊢ ⨆ p, ↑p (x + y) ≤ max (⨆ p, ↑p x) (⨆ p, ↑p y)

Tactic:
· simp

Goal state after:
case inr
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 : NonarchAddGroupSeminorm E
s : Set (NonarchAddGroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
⊢ ⨆ p, ↑p (x + y) ≤ max (⨆ p, ↑p x) (⨆ p, ↑p y)
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf✝ : Surjective ⇑φ
b : M₁
hy : φ b ∈ primaryComponent M₂ P.asIdeal
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf : ((DFinsupp.lsum ℕ) fun i ↦ (primaryComponent M₁ i.asIdeal).subtype) f = b
hdiff : φ b - φ ↑(f P) = ∑ Q ∈ f.support \ {P}, φ ↑(f Q)
Q : HeightOneSpectrum A
hQ : Q ∈ f.support \ {P}
⊢ Q ≠ P

Tactic:
by grind

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

Goal state before:
pp: a : ℝ≥0∞
b : ℝ
ha : a ≠ ∞
⊢ a < ENNReal.ofReal b ↔ a.toReal < b

Tactic:
lift a to ℝ≥0 using ha
  simpa [ENNReal.ofReal, ENNReal.toReal] using Real.lt_toNNReal_iff_coe_lt

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : α
⊢ y ∈ s.ordConnectedComponent x ↔ x ∈ s.ordConnectedComponent y

Tactic:
rw [mem_ordConnectedComponent, mem_ordConnectedComponent, uIcc_comm]

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

Goal state before:
pp: case top.top
c : ℝ≥0
⊢ ∞ + ↑c - (∞ + ↑c) = ∞ - ∞

pp: case top.coe
c x✝ : ℝ≥0
⊢ ∞ + ↑c - (↑x✝ + ↑c) = ∞ - ↑x✝

pp: case coe.top
c x✝ : ℝ≥0
⊢ ↑x✝ + ↑c - (∞ + ↑c) = ↑x✝ - ∞

pp: case coe.coe
c x✝¹ x✝ : ℝ≥0
⊢ ↑x✝¹ + ↑c - (↑x✝ + ↑c) = ↑x✝¹ - ↑x✝

Tactic:
· simp

Goal state after:
case top.coe
c x✝ : ℝ≥0
⊢ ∞ + ↑c - (↑x✝ + ↑c) = ∞ - ↑x✝

case coe.top
c x✝ : ℝ≥0
⊢ ↑x✝ + ↑c - (∞ + ↑c) = ↑x✝ - ∞

case coe.coe
c x✝¹ x✝ : ℝ≥0
⊢ ↑x✝¹ + ↑c - (↑x✝ + ↑c) = ↑x✝¹ - ↑x✝
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case top.coe
c x✝ : ℝ≥0
⊢ ∞ + ↑c - (↑x✝ + ↑c) = ∞ - ↑x✝

pp: case coe.top
c x✝ : ℝ≥0
⊢ ↑x✝ + ↑c - (∞ + ↑c) = ↑x✝ - ∞

pp: case coe.coe
c x✝¹ x✝ : ℝ≥0
⊢ ↑x✝¹ + ↑c - (↑x✝ + ↑c) = ↑x✝¹ - ↑x✝

Tactic:
· simp

Goal state after:
case coe.top
c x✝ : ℝ≥0
⊢ ↑x✝ + ↑c - (∞ + ↑c) = ↑x✝ - ∞

case coe.coe
c x✝¹ x✝ : ℝ≥0
⊢ ↑x✝¹ + ↑c - (↑x✝ + ↑c) = ↑x✝¹ - ↑x✝
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case coe.top
c x✝ : ℝ≥0
⊢ ↑x✝ + ↑c - (∞ + ↑c) = ↑x✝ - ∞

pp: case coe.coe
c x✝¹ x✝ : ℝ≥0
⊢ ↑x✝¹ + ↑c - (↑x✝ + ↑c) = ↑x✝¹ - ↑x✝

Tactic:
· simp

Goal state after:
case coe.coe
c x✝¹ x✝ : ℝ≥0
⊢ ↑x✝¹ + ↑c - (↑x✝ + ↑c) = ↑x✝¹ - ↑x✝
Module: Mathlib.Data.ENNReal.Operations

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

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

Tactic:
· simp

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

Goal state before:
pp: case top
b : ℝ≥0
⊢ ∞.toReal - (↑b).toReal ≤ (∞ - ↑b).toReal

pp: case coe
b x✝ : ℝ≥0
⊢ (↑x✝).toReal - (↑b).toReal ≤ (↑x✝ - ↑b).toReal

Tactic:
· simp

Goal state after:
case coe
b x✝ : ℝ≥0
⊢ (↑x✝).toReal - (↑b).toReal ≤ (↑x✝ - ↑b).toReal
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case top
a b : ℝ≥0
h : ↑b ≤ ↑a
⊢ ↑a - ∞ - (↑a - ↑b) = ↑b - ∞

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

Tactic:
· simp

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

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
⊢ (iInf f).toNNReal = ⨅ i, (f i).toNNReal

Tactic:
by
  cases isEmpty_or_nonempty ι
  · rw [iInf_of_empty, toNNReal_top, NNReal.iInf_empty]
  · lift f to ι → ℝ≥0 using hf
    simp_rw [← coe_iInf, toNNReal_coe]

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

Goal state before:
pp: case inr.inl
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
⊢ ∞ ≤ ENNReal.ofReal (⨅ i, f i) ↔ ∞ ≤ ⨅ i, ENNReal.ofReal (f i)

pp: case inr.inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
⊢ a ≤ ENNReal.ofReal (⨅ i, f i) ↔ a ≤ ⨅ i, ENNReal.ofReal (f i)

Tactic:
· simp

Goal state after:
case inr.inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
⊢ a ≤ ENNReal.ofReal (⨅ i, f i) ↔ a ≤ ⨅ i, ENNReal.ofReal (f i)
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inl
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
⊢ ∞ + ⨆ i, f i = ⨆ i, ∞ + f i

pp: case inr
ι : Sort u_1
a : ℝ≥0∞
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
ha : a ≠ ∞
⊢ a + ⨆ i, f i = ⨆ i, a + f i

Tactic:
· simp

Goal state after:
case inr
ι : Sort u_1
a : ℝ≥0∞
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
ha : a ≠ ∞
⊢ a + ⨆ i, f i = ⨆ i, a + f i
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inl
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : IsEmpty ι
⊢ iSup f + iSup g = ⨆ i, f i + g i

pp: case inr
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
⊢ iSup f + iSup g = ⨆ i, f i + g i

Tactic:
· simp

Goal state after:
case inr
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
⊢ iSup f + iSup g = ⨆ i, f i + g i
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case coe
a✝ : ℝ
hx : ↑a✝ ≠ ⊤ ∧ ↑a✝ ≠ ⊥
⊢ ∃ y, ↑y = ↑a✝

pp: case top
hx : ⊤ ≠ ⊤ ∧ ⊤ ≠ ⊥
⊢ ∃ y, ↑y = ⊤

Tactic:
· simp

Goal state after:
case top
hx : ⊤ ≠ ⊤ ∧ ⊤ ≠ ⊥
⊢ ∃ y, ↑y = ⊤
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case bot
hx : 0 ≤ ⊥
⊢ 0 ≤ ⊥.toReal

pp: case coe
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ 0 ≤ (↑a✝).toReal

pp: case top
hx : 0 ≤ ⊤
⊢ 0 ≤ ⊤.toReal

Tactic:
· simp

Goal state after:
case coe
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ 0 ≤ (↑a✝).toReal

case top
hx : 0 ≤ ⊤
⊢ 0 ≤ ⊤.toReal
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case top
hx : 0 ≤ ⊤
⊢ 0 ≤ ⊤.toReal

Tactic:
· simp

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

Goal state before:
pp: case bot
hx : ⊥ ≤ 0
⊢ ⊥.toReal ≤ 0

pp: case coe
a✝ : ℝ
hx : ↑a✝ ≤ 0
⊢ (↑a✝).toReal ≤ 0

pp: case top
hx : ⊤ ≤ 0
⊢ ⊤.toReal ≤ 0

Tactic:
· simp

Goal state after:
case coe
a✝ : ℝ
hx : ↑a✝ ≤ 0
⊢ (↑a✝).toReal ≤ 0

case top
hx : ⊤ ≤ 0
⊢ ⊤.toReal ≤ 0
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case top
hx : ⊤ ≤ 0
⊢ ⊤.toReal ≤ 0

Tactic:
· simp

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
⊢ count K v 1 = 0

Tactic:
have h1 : (1 : FractionalIdeal R⁰ K) =
      spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑(1 : Ideal R) := by
    rw [(algebraMap R K).map_one, Ideal.one_eq_top, coeIdeal_top, mul_one, inv_one,
      spanSingleton_one]
  rw [count_well_defined K v one_ne_zero h1, Ideal.span_singleton_one, Ideal.one_eq_top, sub_self]

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

Goal state before:
pp: case inl
⊢ ↑(∞ * ↑0) = ⊤ * ↑↑0

pp: case inr
x : ℝ≥0
h0 : x ≠ 0
⊢ ↑(∞ * ↑x) = ⊤ * ↑↑x

Tactic:
· simp

Goal state after:
case inr
x : ℝ≥0
h0 : x ≠ 0
⊢ ↑(∞ * ↑x) = ⊤ * ↑↑x
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case neg
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
n : ℕ
h : count K v (I ^ n) = ↑n * count K v I
hI : ¬I = 0
⊢ ↑n * count K v I + count K v I = ↑(n + 1) * count K v I

Tactic:
Nat.cast_add,

Goal state after:
case neg
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
n : ℕ
h : count K v (I ^ n) = ↑n * count K v I
hI : ¬I = 0
⊢ ↑n * count K v I + count K v I = (↑n + ↑1) * count K v I
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case bot
y : EReal
h : ⊥ ≤ y
⊢ ⊥.toENNReal ≤ y.toENNReal

pp: case coe
y : EReal
a✝ : ℝ
h : ↑a✝ ≤ y
⊢ (↑a✝).toENNReal ≤ y.toENNReal

pp: case top
y : EReal
h : ⊤ ≤ y
⊢ ⊤.toENNReal ≤ y.toENNReal

Tactic:
· simp

Goal state after:
case coe
y : EReal
a✝ : ℝ
h : ↑a✝ ≤ y
⊢ (↑a✝).toENNReal ≤ y.toENNReal

case top
y : EReal
h : ⊤ ≤ y
⊢ ⊤.toENNReal ≤ y.toENNReal
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x✝ : ↑{⊥, ⊤}ᶜ
x : ℝ
hx : ↑x ∈ {⊥, ⊤}ᶜ
⊢ (fun x ↦ ⟨↑x, ⋯⟩) ((fun x ↦ (↑x).toReal) ⟨↑x, hx⟩) = ⟨↑x, hx⟩

Tactic:
· simp

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

Goal state before:
pp: x y z : ℝ≥0∞
h1 : y ≠ 0
h2 : y ≠ ∞
⊢ x / y ≤ z ↔ x ≤ z * y

Tactic:
ENNReal.div_le_iff h1 h2

Goal state after:
x y z : ℝ≥0∞
h1 : y ≠ 0
h2 : y ≠ ∞
⊢ x ≤ z * y ↔ x ≤ z * y
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case top
a : ℝ≥0
h : ↑a < ∞
⊢ ∞⁻¹ < (↑a)⁻¹

pp: case coe
a x✝ : ℝ≥0
h : ↑a < ↑x✝
⊢ (↑x✝)⁻¹ < (↑a)⁻¹

Tactic:
· simp

Goal state after:
case coe
a x✝ : ℝ≥0
h : ↑a < ↑x✝
⊢ (↑x✝)⁻¹ < (↑a)⁻¹
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 ≠ ∞
⊢ b / a * a = b

Tactic:
ENNReal.div_mul_cancel ha ha'

Goal state after:
case inr.inr
a b : ℝ≥0∞
h₀ : a = 0 → b = 0
h₁ : a = ∞ → b = 0
ha : a ≠ 0
ha' : a ≠ ∞
⊢ b = b