mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case h.tmul
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 σ
inst✝ : Flat S T
x : T
y : P.toExtension.H1Cotangent
x_in :
  (liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
      ((lTensor T Extension.h1Cotangentι) (x ⊗ₜ[S] y)) ∈
    (Q.comp P).toExtension.cotangentComplex.ker
⊢ (↑((liftBaseChange T (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)) (x ⊗ₜ[S] y))).val =
    (↑⟨(liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
            ((lTensor T Extension.h1Cotangentι) (x ⊗ₜ[S] y)),
          x_in⟩).val

Tactic:
simp

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

Goal state before:
pp: case left
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x✝ : T ⊗[S] P.H1Cotangent
hx : (LinearMap.liftBaseChange T (H1Cotangent.map f)) x✝ = 0
x : P.H1Cotangent
⊢ (((AlgebraTensorModule.curry (LinearMap.liftBaseChange T (Cotangent.map f) ∘ₗ LinearMap.baseChange T h1Cotangentι)) 1)
        x).val =
    (((AlgebraTensorModule.curry (h1Cotangentι ∘ₗ LinearMap.liftBaseChange T (H1Cotangent.map f))) 1) x).val

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
x s : P.Ring
hs : (algebraMap P.Ring S) s ∈ M
⊢ ↑((IsScalarTower.toAlgHom R S T).comp (IsScalarTower.toAlgHom R P.Ring S)) x =
    ↑((IsScalarTower.toAlgHom R S T).comp (IsScalarTower.toAlgHom R P.Ring S)) ↑⟨s, ⋯⟩ *
      IsLocalization.mk' T ((algebraMap P.Ring S) x) ⟨(algebraMap P.Ring S) s, hs⟩

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst✝¹ : r.LiesOver q
inst✝ : Module.Flat S T
⊢ q.ramificationIdx R ∣ r.ramificationIdx R

Tactic:
by
  use r.ramificationIdx S
  rw [← ramificationIdx_tower]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
x✝ : H1Cotangent R S
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
x s : P.Ring
hs : (algebraMap P.Ring S) s ∈ M
⊢ ↑((IsScalarTower.toAlgHom R S T).comp (IsScalarTower.toAlgHom R P.Ring S)) x =
    ↑((IsScalarTower.toAlgHom R S T).comp (IsScalarTower.toAlgHom R P.Ring S)) ↑⟨s, ⋯⟩ *
      IsLocalization.mk' T ((algebraMap P.Ring S) x) ⟨(algebraMap P.Ring S) s, hs⟩

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
x : H1Cotangent R S
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
i : T
⊢ ((IsScalarTower.toAlgHom R Q.Ring T).comp (MvPolynomial.aeval Q.σ)) (MvPolynomial.X i) =
    (algebraMap (Generators.self R T).Ring T) (MvPolynomial.X i)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: 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₂
y : M
hymem : y ∈ N₁
n₁ : ℕ
hy : ∀ a ∈ I ^ n₁, a • y = 0
z : M
hzmem : z ∈ N₂
n₂ : ℕ
hz : ∀ a ∈ I ^ n₂, a • z = 0
a : A
ha : a ∈ I ^ max n₁ n₂
⊢ n₁ ≤ max n₁ n₂

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: 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₂
y : M
hymem : y ∈ N₁
n₁ : ℕ
z : M
hzmem : z ∈ N₂
n₂ : ℕ
hz : ∀ a ∈ I ^ n₂, a • z = 0
a : A
hy : a • y = 0
ha : a ∈ I ^ max n₁ n₂
⊢ n₂ ≤ max n₁ n₂

Tactic:
simp

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

Tactic:
simp

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

Goal state before:
pp: case a
ι : Type u_1
α : Type u_2
s : Finset ι
inst✝ : DecidableEq α
hs : s.Nonempty
S : ι → Finset α
a : α
x✝ : ι
a✝ : x✝ ∈ s
⊢ ↑(s.biUnion S) = ⋃ i ∈ s, ↑(S i)

Tactic:
simp

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
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
a✝ : ∅ ∈ s.powerset
ht : ¬∅.Nonempty
⊢ (-1) ^ #∅ • ∑ a ∈ s.biUnion S, f a =
    ∑ x ∈ s.biUnion S, ((-1) ^ #∅ * ((∏ i ∈ s \ ∅, 1) * ∏ i ∈ ∅, (↑(S i)).indicator 1 x)) • f x

Tactic:
simp

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, (∏ i ∈ s, ((↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a)) • f a = 0

Tactic:
by
      obtain rfl | hs := s.eq_empty_or_nonempty <;>
        simp [-coe_biUnion, prod_indicator_biUnion_finset_sub_indicator, *]

Goal state after:
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 ≥ ⌈ε⁻¹⌉₊, ∀ k ≥ ⌈ε⁻¹⌉₊, ↑(f j) / ↑j - ↑(f k) / ↑k < ε

Tactic:
intro j

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 : ℕ
⊢ j ≥ ⌈ε⁻¹⌉₊ → ∀ k ≥ ⌈ε⁻¹⌉₊, ↑(f j) / ↑j - ↑(f k) / ↑k < ε
Module: Mathlib.Data.NNReal.Defs

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

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: ⊢ ¬(∅.Nonempty ∧ BddAbove ∅)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

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

Tactic:
simp

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ (x ^ n).toNNReal = x.toNNReal ^ n

Tactic:
rw [← coe_inj, NNReal.coe_pow, Real.coe_toNNReal _ (pow_nonneg hx _),
    Real.coe_toNNReal x hx]

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

Tactic:
simp

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

Goal state before:
pp: ⊢ ⟨|0|, ⋯⟩ = 0

Tactic:
simp

Goal state after:
⊢ ⟨0, ⋯⟩ = 0
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ ⟨|1|, ⋯⟩ = 1

Tactic:
simp

Goal state after:
⊢ ⟨1, ⋯⟩ = 1
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x : ℝ≥0
⊢ nnabs ↑x = x

Tactic:
simp

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

Goal state before:
pp: x : ℝ
⊢ ↑|x|.toNNReal = ↑(nnabs x)

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ nnabs ↑n = ↑n

Tactic:
simp

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

Goal state before:
pp: n : ℕ
inst✝ : n.AtLeastTwo
⊢ nnabs (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ 0 ≤ 1 / ↑k

Tactic:
simp

Goal state after:
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✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
⊢ ⨆ p, ↑p 1 = 0

Tactic:
simp

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

Goal state before:
pp: x : ℝ≥0∞
⊢ x = ↑1 ∨ x = ⊤ ∧ 1 = 0 ↔ x = 1

Tactic:
simp

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✝² : 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

Tactic:
simp

Goal state after:
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✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
x : E
⊢ ⨆ p, ↑p x⁻¹ = ⨆ p, ↑p x

Tactic:
simp

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

Goal state before:
pp: E : Type u_3
inst✝ : Group E
s : Set (GroupSeminorm E)
hs : BddAbove s
x : E
x✝ : ℝ
⊢ (x✝ ∈ range fun p ↦ ↑p x) ↔ x✝ ∈ (fun x_1 ↦ x_1 x) '' s

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
s : Finset (HeightOneSpectrum A)
p : HeightOneSpectrum A → M
hsum : ∑ i ∈ s, p i = 0
f : HeightOneSpectrum A → ℕ
hmem : ∀ i ∈ s, p i ∈ torsionBySet A M ↑(i.asIdeal ^ f i)
m : ℕ := s.sup f
⊢ ∀ (s : Finset (HeightOneSpectrum A)), s.SupIndep fun i ↦ torsionBySet A M ↑(i.asIdeal ^ m)

Tactic:
exact fun _ ↦ supIndep_torsionBySet_ideal
      fun _ _ _ _ hPQ ↦ (isCoprime_pow_of_ne _ _ hPQ _ _).sup_eq

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

Goal state before:
pp: E : Type u_3
inst✝ : Group E
ι : Type u_6
f : ι → GroupSeminorm E
h : BddAbove (range f)
x : E
⊢ ∀ (x_1 : ι), ↑(rangeFactorization f x_1) x = (f x_1) x

Tactic:
simp

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

Goal state before:
pp: case top
⊢ |∞.toReal| = ∞.toReal

Tactic:
simp

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

Goal state before:
pp: case coe
x✝ : ℝ≥0
⊢ |(↑x✝).toReal| = (↑x✝).toReal

Tactic:
simp

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

Goal state before:
pp: 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
⊢ (if x + y = 0 then 0 else 1) ≤ (if x = 0 then 0 else 1) + if y = 0 then 0 else 1

Tactic:
if_pos hx,

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
⊢ (if x + y = 0 then 0 else 1) ≤ 0 + if y = 0 then 0 else 1
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: case top
a : ℝ≥0∞
⊢ 0 < ∞.toNNReal ↔ 0 < ∞ ∧ ∞ < ∞

Tactic:
simp

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

Goal state before:
pp: case coe
a : ℝ≥0∞
x✝ : ℝ≥0
⊢ 0 < (↑x✝).toNNReal ↔ 0 < ↑x✝ ∧ ↑x✝ < ∞

Tactic:
simp

Goal state after:
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 : NonarchAddGroupSeminorm E
s : Set (NonarchAddGroupSeminorm E)
h : BddAbove s
⊢ ⨆ p, ↑p 0 = 0

Tactic:
simp

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)

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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : (algebraMap R K) ↑d ≠ 0
h0 : spanSingleton R⁰ (mk' K n d) ≠ 0
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {n})).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑d})).factors)) =
    spanSingleton R⁰ (mk' K n d)

Tactic:
have hI : spanSingleton R⁰ (mk' K n d) =
      spanSingleton R⁰ ((algebraMap R K) d)⁻¹ * ↑(Ideal.span {n} : Ideal R) := by
    rw [coeIdeal_span_singleton, spanSingleton_mul_spanSingleton]
    apply congr_arg
    rw [IsFractionRing.mk'_eq_div, div_eq_mul_inv, mul_comm]

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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : (algebraMap R K) ↑d ≠ 0
h0 : spanSingleton R⁰ (mk' K n d) ≠ 0
hI : spanSingleton R⁰ (mk' K n d) = spanSingleton R⁰ ((algebraMap R K) ↑d)⁻¹ * ↑(Ideal.span {n})
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {n})).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑d})).factors)) =
    spanSingleton R⁰ (mk' K n d)
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 : NonarchAddGroupSeminorm E
s : Set (NonarchAddGroupSeminorm E)
h : BddAbove s
⊢ ∀ (r : E), ⨆ p, ↑p (-r) = ⨆ p, ↑p r

Tactic:
simp

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

Goal state before:
pp: a : ℝ≥0∞
⊢ (a * ∞).toNNReal = 0

Tactic:
simp

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

Goal state before:
pp: a : ℝ≥0∞
⊢ (∞ * a).toNNReal = 0

Tactic:
simp

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

Goal state before:
pp: a : ℝ≥0∞
n : ℕ
⊢ (n • a).toReal = n • a.toReal

Tactic:
simp

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

Goal state before:
pp: E : Type u_3
inst✝ : AddGroup E
s : Set (NonarchAddGroupSeminorm E)
hs : BddAbove s
x : E
x✝ : ℝ
⊢ (x✝ ∈ range fun p ↦ ↑p x) ↔ x✝ ∈ (fun x_1 ↦ x_1 x) '' s

Tactic:
simp

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

Goal state before:
pp: E : Type u_3
inst✝ : AddGroup E
ι : Type u_6
f : ι → NonarchAddGroupSeminorm E
h : BddAbove (range f)
x : E
⊢ ∀ (x_1 : ι), ↑(rangeFactorization f x_1) x = (f x_1) x

Tactic:
simp

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

Goal state before:
pp: 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
⊢ (if x * y = 1 then 0 else 1) ≤ (if x = 1 then 0 else 1) + if y = 1 then 0 else 1

Tactic:
if_pos hx,

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
⊢ (if x * y = 1 then 0 else 1) ≤ 0 + if y = 1 then 0 else 1
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: 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
⊢ (if x + y = 0 then 0 else 1) ≤ max (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)

Tactic:
if_pos hx,

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
⊢ (if x + y = 0 then 0 else 1) ≤ max 0 (if y = 0 then 0 else 1)
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: 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
h✝ : y = 0
⊢ 0 ≤ max 1 0

Tactic:
simp

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
h✝¹ : x + y = 0
h✝ : ¬y = 0
⊢ 0 ≤ max 1 1

Tactic:
simp

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

Goal state before:
pp: 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
h✝ : y = 0
⊢ 1 ≤ max 1 0

Tactic:
simp

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
h✝¹ : ¬x + y = 0
h✝ : ¬y = 0
⊢ 1 ≤ max 1 1

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case mpr.inr.inl
b : ℝ≥0∞
⊢ 0 * b < ∞

Tactic:
simp

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

Goal state before:
pp: case mpr.inr.inr
a : ℝ≥0∞
⊢ a * 0 < ∞

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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)

Tactic:
simp

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

Goal state before:
pp: x y : ℝ
⊢ { toFun := Real.toEReal, inj' := coe_injective } x ≤ { toFun := Real.toEReal, inj' := coe_injective } y ↔ x ≤ y

Tactic:
simp

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

Goal state before:
pp: ι : Sort u_1
⊢ ⨆ x, 0 = 0

Tactic:
simp

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

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

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
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ count K v (I * I') = count K v I + count K v I'

Tactic:
obtain ⟨a, J, ha, haJ⟩ := exists_eq_spanSingleton_mul I

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
⊢ count K v (I * I') = count K v I + count K v 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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case bot
⊢ ⊥ ∈ range Real.toEReal ↔ ⊥ ∈ {⊥, ⊤}ᶜ

Tactic:
simp

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

Goal state before:
pp: case coe
a✝ : ℝ
⊢ ↑a✝ ∈ range Real.toEReal ↔ ↑a✝ ∈ {⊥, ⊤}ᶜ

Tactic:
simp

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

Goal state before:
pp: case top
⊢ ⊤ ∈ range Real.toEReal ↔ ⊤ ∈ {⊥, ⊤}ᶜ

Tactic:
simp

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

Goal state before:
pp: case bot
⊢ ⊥ ∈ range Real.toEReal ↔ ⊥ ∈ Ioo ⊥ ⊤

Tactic:
simp

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

Goal state before:
pp: case coe
a✝ : ℝ
⊢ ↑a✝ ∈ range Real.toEReal ↔ ↑a✝ ∈ Ioo ⊥ ⊤

Tactic:
simp

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

Goal state before:
pp: case top
⊢ ⊤ ∈ range Real.toEReal ↔ ⊤ ∈ Ioo ⊥ ⊤

Tactic:
simp

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

Goal state before:
pp: x : ℝ
hx_top : ↑x ≠ ⊤
hx_bot : ↑x ≠ ⊥
y : ℝ
hy_top : ↑y ≠ ⊤
hy_bot : ↑y ≠ ⊥
⊢ (↑x).toReal = (↑y).toReal ↔ ↑x = ↑y

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: x y : ℝ
⊢ Real.toEReal ⁻¹' (Ici ↑x ∩ Iic ↑y) = Ici x ∩ Iic y

Tactic:
simp

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

Goal state before:
pp: x y : ℝ
⊢ Real.toEReal ⁻¹' (Ici ↑x ∩ Iio ↑y) = Ici x ∩ Iio y

Tactic:
simp

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

Goal state before:
pp: x y : ℝ
⊢ Real.toEReal ⁻¹' (Ioi ↑x ∩ Iic ↑y) = Ioi x ∩ Iic y

Tactic:
simp

Goal state after: