mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ LinearMap.liftBaseChange T (Cotangent.map f) ∘ₗ LinearMap.baseChange T h1Cotangentι =
    h1Cotangentι ∘ₗ LinearMap.liftBaseChange T (H1Cotangent.map f)

Tactic:
ext x

Goal state after:
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
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
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 : Q.H1Cotangent
this : Function.Exact ⇑(LinearMap.baseChange T h1Cotangentι) ⇑(LinearMap.baseChange T P.cotangentComplex)
⊢ LinearMap.liftBaseChange T (CotangentSpace.map f) ∘ₗ LinearMap.baseChange T P.cotangentComplex =
    Q.cotangentComplex ∘ₗ LinearMap.liftBaseChange T (Cotangent.map f)

Tactic:
ext x

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
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✝ : Q.H1Cotangent
this : Function.Exact ⇑(LinearMap.baseChange T h1Cotangentι) ⇑(LinearMap.baseChange T P.cotangentComplex)
x : P.Cotangent
⊢ ((AlgebraTensorModule.curry
          (LinearMap.liftBaseChange T (CotangentSpace.map f) ∘ₗ LinearMap.baseChange T P.cotangentComplex))
        1)
      x =
    ((AlgebraTensorModule.curry (Q.cotangentComplex ∘ₗ LinearMap.liftBaseChange T (Cotangent.map f))) 1) x
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case right
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 : Q.H1Cotangent
this : Function.Exact ⇑(LinearMap.baseChange T h1Cotangentι) ⇑(LinearMap.baseChange T P.cotangentComplex)
⊢ ∃ a, (LinearMap.liftBaseChange T (H1Cotangent.map f)) a = x

Tactic:
obtain ⟨a, ha⟩ := (this ((Extension.tensorCotangent f halg H₂).symm x.1)).mp (by
      apply (Extension.tensorCotangentSpaceOfFormallyEtale f H₁).injective
      rw [LinearEquiv.map_zero, ← x.2]
      have : (CotangentSpace.map f).liftBaseChange T ∘ₗ P.cotangentComplex.baseChange T =
          Q.cotangentComplex ∘ₗ (Cotangent.map f).liftBaseChange T := by
        ext x; obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x; dsimp
        simp only [CotangentSpace.map_tmul,
          map_one, Hom.toAlgHom_apply, one_smul, cotangentComplex_mk]
      exact (DFunLike.congr_fun this _).trans (DFunLike.congr_arg Q.cotangentComplex
        ((tensorCotangent f halg H₂).apply_symm_apply x.1)))

Goal state after:
case right
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 : Q.H1Cotangent
this : Function.Exact ⇑(LinearMap.baseChange T h1Cotangentι) ⇑(LinearMap.baseChange T P.cotangentComplex)
a : T ⊗[S] P.H1Cotangent
ha : (LinearMap.baseChange T h1Cotangentι) a = (tensorCotangent f halg H₂).symm ↑x
⊢ ∃ a, (LinearMap.liftBaseChange T (H1Cotangent.map f)) a = x
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 ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
f : P.Hom Q :=
  { toRingHom := algebraMap P.Ring (Localization M'), toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
this✝⁸ : FormallySmooth R P.Ring
this✝⁷ : FormallySmooth P.Ring (Localization M')
this✝⁶ : FormallySmooth R Q.Ring
this✝⁵ : Module.Flat S T
this✝⁴ : Algebra P.Ring Q.Ring := inferInstance
this✝³ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝² : Algebra (Localization M') T := fQ.toAlgebra
this✝¹ : IsScalarTower P.Ring S T
this✝ : IsScalarTower P.Ring (Localization M') T
this : IsLocalizedModule M' (IsScalarTower.toAlgHom P.Ring S T).toLinearMap
F : ↥P.ker →ₗ[P.Ring] ↥(RingHom.ker fQ) := f.mapKer ⋯
⊢ (LinearMap.extendScalarsOfIsLocalization M' (Localization M')
        ((IsLocalizedModule.map M' (Algebra.linearMap P.Ring (Localization M'))
            (IsScalarTower.toAlgHom P.Ring S T).toLinearMap)
          (Algebra.linearMap P.Ring S))).ker =
    RingHom.ker fQ

Tactic:
ext x

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
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 ⋯
f : P.Hom Q :=
  { toRingHom := algebraMap P.Ring (Localization M'), toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
this✝⁸ : FormallySmooth R P.Ring
this✝⁷ : FormallySmooth P.Ring (Localization M')
this✝⁶ : FormallySmooth R Q.Ring
this✝⁵ : Module.Flat S T
this✝⁴ : Algebra P.Ring Q.Ring := inferInstance
this✝³ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝² : Algebra (Localization M') T := fQ.toAlgebra
this✝¹ : IsScalarTower P.Ring S T
this✝ : IsScalarTower P.Ring (Localization M') T
this : IsLocalizedModule M' (IsScalarTower.toAlgHom P.Ring S T).toLinearMap
F : ↥P.ker →ₗ[P.Ring] ↥(RingHom.ker fQ) := f.mapKer ⋯
x : Localization M'
⊢ x ∈
      (LinearMap.extendScalarsOfIsLocalization M' (Localization M')
          ((IsLocalizedModule.map M' (Algebra.linearMap P.Ring (Localization M'))
              (IsScalarTower.toAlgHom P.Ring S T).toLinearMap)
            (Algebra.linearMap P.Ring S))).ker ↔
    x ∈ RingHom.ker fQ
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝² : CommRing A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
I : Ideal A
⊢ Submodule.map (torsionBySet A M ↑I).subtype (primaryComponent (↥(torsionBySet A M ↑I)) I) =
    primaryComponent M I ⊓ torsionBySet A M ↑I

Tactic:
ext x

Goal state after:
A : Type u_1
M : Type u_2
inst✝² : CommRing A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
I : Ideal A
x : M
⊢ x ∈ Submodule.map (torsionBySet A M ↑I).subtype (primaryComponent (↥(torsionBySet A M ↑I)) I) ↔
    x ∈ primaryComponent M I ⊓ torsionBySet A M ↑I
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✝¹ : AddCommMonoid M
inst✝ : Module A M
J : Ideal A
hD : IsCoprime I J
this : ∀ (n : ℕ), Disjoint (torsionBySet A M ↑(I ^ n)) (torsionBySet A M ↑J)
⊢ Submodule.map (torsionBySet A M ↑J).subtype (primaryComponent (↥(torsionBySet A M ↑J)) I) =
    Submodule.map (torsionBySet A M ↑J).subtype ⊥

Tactic:
ext x

Goal state after:
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
J : Ideal A
hD : IsCoprime I J
this : ∀ (n : ℕ), Disjoint (torsionBySet A M ↑(I ^ n)) (torsionBySet A M ↑J)
x : M
⊢ x ∈ Submodule.map (torsionBySet A M ↑J).subtype (primaryComponent (↥(torsionBySet A M ↑J)) I) ↔
    x ∈ Submodule.map (torsionBySet A M ↑J).subtype ⊥
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₂
⊢ Submodule.map (N₁ ⊔ N₂).subtype (primaryComponent (↥(N₁ ⊔ N₂)) I) =
    Submodule.map N₁.subtype (primaryComponent (↥N₁) I) ⊔ Submodule.map N₂.subtype (primaryComponent (↥N₂) I)

Tactic:
ext x

Goal state after:
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₂
x : M
⊢ x ∈ Submodule.map (N₁ ⊔ N₂).subtype (primaryComponent (↥(N₁ ⊔ N₂)) I) ↔
    x ∈ Submodule.map N₁.subtype (primaryComponent (↥N₁) I) ⊔ Submodule.map N₂.subtype (primaryComponent (↥N₂) I)
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
s : Finset ι
hs : s.Nonempty
S : ι → Set α
a : α
ha ha' : a ∈ ⋃ i ∈ s, S i
⊢ ∏ i ∈ s, ((⋃ i ∈ s, S i).indicator 1 a - (S i).indicator 1 a) = 0

Tactic:
simp only [Set.mem_iUnion, exists_prop] at ha

Goal state after:
case pos
ι : Type u_1
α : Type u_2
s : Finset ι
hs : s.Nonempty
S : ι → Set α
a : α
ha' : a ∈ ⋃ i ∈ s, S i
ha : ∃ i ∈ s, a ∈ S i
⊢ ∏ i ∈ s, ((⋃ i ∈ s, S i).indicator 1 a - (S i).indicator 1 a) = 0
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
s : Finset ι
hs : s.Nonempty
S : ι → Set α
a : α
ha : a ∈ ⋃ i ∈ s, S i
⊢ ∏ i ∈ s, ((⋃ i ∈ s, S i).indicator 1 a - (S i).indicator 1 a) = 0

pp: case neg
ι : Type u_1
α : Type u_2
s : Finset ι
hs : s.Nonempty
S : ι → Set α
a : α
ha : a ∉ ⋃ i ∈ s, S i
⊢ ∏ i ∈ s, ((⋃ i ∈ s, S i).indicator 1 a - (S i).indicator 1 a) = 0

Tactic:
· have ha' := ha
    simp only [Set.mem_iUnion, exists_prop] at ha
    obtain ⟨i, hi, ha⟩ := ha
    apply prod_eq_zero hi (by simp [ha, ha'])

Goal state after:
case neg
ι : Type u_1
α : Type u_2
s : Finset ι
hs : s.Nonempty
S : ι → Set α
a : α
ha : a ∉ ⋃ i ∈ s, S i
⊢ ∏ i ∈ s, ((⋃ i ∈ s, S i).indicator 1 a - (S i).indicator 1 a) = 0
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
h : IsTorsion A M
x : M
a : A
ha : a ∈ A⁰
hmem : x ∈ torsionBySet A M ↑(⨅ i, i.maxPowDividing (span {a}))
ha0 : span {a} ≠ ⊥
this : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := Finite.fintype ⋯
S : Finset (HeightOneSpectrum A) := (mulSupport fun v ↦ v.maxPowDividing (span {a})).toFinset
⊢ ⨅ i, i.maxPowDividing (span {a}) = ⨅ i ∈ S, i.maxPowDividing (span {a})

Tactic:
ext x

Goal state after:
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h : IsTorsion A M
x✝ : M
a : A
ha : a ∈ A⁰
hmem : x✝ ∈ torsionBySet A M ↑(⨅ i, i.maxPowDividing (span {a}))
ha0 : span {a} ≠ ⊥
this : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := Finite.fintype ⋯
S : Finset (HeightOneSpectrum A) := (mulSupport fun v ↦ v.maxPowDividing (span {a})).toFinset
x : A
⊢ x ∈ ⨅ i, i.maxPowDividing (span {a}) ↔ x ∈ ⨅ i ∈ S, i.maxPowDividing (span {a})
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: case hs
ι : 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
this : (⋃ i ∈ s, S i).indicator 1 a = 1
⊢ s.Nonempty

Tactic:
simp only [Set.mem_iUnion, exists_prop] at ha

Goal state after:
case hs
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
this : (⋃ i ∈ s, S i).indicator 1 a = 1
ha : ∃ i ∈ s, a ∈ S i
⊢ s.Nonempty
Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice

Goal state before:
pp: M : Type u_1
inst✝³ : ConditionallyCompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s t : Set M
hs₀ : s.Nonempty
hs₁ : BddBelow s
ht₀ : t.Nonempty
ht₁ : BddAbove t
⊢ sInf (s / t) = sInf s / sSup t

Tactic:
rw [div_eq_mul_inv, csInf_mul hs₀ hs₁ ht₀.inv ht₁.inv, csInf_inv ht₀ ht₁, div_eq_mul_inv]

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

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

Tactic:
simp only [Set.image_empty, Real.sInf_empty, coe_eq_zero]

Goal state after:
case inl
⊢ sInf ∅ = 0
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: s : Set ℝ
hs : ∀ x ∈ s, 0 ≤ x
⊢ 0 ≤ sSup s

Tactic:
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
  · exact sSup_empty.ge
  · exact sSup_nonneg' ⟨x, hx, hs _ hx⟩

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

Goal state before:
pp: r : ℝ
⊢ r.toNNReal < 1 ↔ r < 1

Tactic:
simp only [← not_le, one_le_toNNReal]

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
h0 : I ≠ 0
⊢ ⨅ i, i.maxPowDividing I = ⨅ i ∈ Finite.toFinset ⋯, i.maxPowDividing I

Tactic:
ext x

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : R
⊢ x ∈ ⨅ i, i.maxPowDividing I ↔ x ∈ ⨅ i ∈ Finite.toFinset ⋯, i.maxPowDividing I
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: ι : Type u_2
f : ι → ℝ≥0∞
hf : ∀ (x : ι), f x ≠ ∞
⊢ (fun x ↦ ↑x) ∘ ENNReal.toNNReal ∘ f = f

Tactic:
ext x

Goal state after:
ι : Type u_2
f : ι → ℝ≥0∞
hf : ∀ (x : ι), f x ≠ ∞
x : ι
⊢ ((fun x ↦ ↑x) ∘ ENNReal.toNNReal ∘ f) x = f x
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: x : ℝ≥0∞
⊢ x.toReal = 1 ↔ x = 1

Tactic:
by
  rw [ENNReal.toReal, NNReal.coe_eq_one, ENNReal.toNNReal_eq_one_iff]

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

Goal state before:
pp: ⊢ ⋃ n, Iio ↑n = {∞}ᶜ

Tactic:
ext x

Goal state after:
x : ℝ≥0∞
⊢ x ∈ ⋃ n, Iio ↑n ↔ x ∈ {∞}ᶜ
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
⊢ ∏ᶠ (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 h0 : spanSingleton R⁰ (mk' K n d) ≠ 0 := by
    rw [spanSingleton_ne_zero_iff, IsFractionRing.mk'_eq_div, ne_eq, div_eq_zero_iff, not_or]
    exact ⟨(map_ne_zero_iff (algebraMap R K) (IsFractionRing.injective R K)).mpr hn, hd_ne_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
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)
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
⊢ (range fun x ↦ ⋯.some) = ⇑ofDual ⁻¹' range fun x ↦ ⋯.some

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : αᵒᵈ
⊢ (x ∈ range fun x ↦ ⋯.some) ↔ x ∈ ⇑ofDual ⁻¹' range fun x ↦ ⋯.some
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: x y : ℝ≥0
⊢ ofNNReal '' uIcc x y = uIcc ↑x ↑y

Tactic:
simp [uIcc]

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

Goal state before:
pp: ⊢ range Real.toEReal = {⊥, ⊤}ᶜ

Tactic:
ext x

Goal state after:
x : EReal
⊢ x ∈ range Real.toEReal ↔ x ∈ {⊥, ⊤}ᶜ
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: ⊢ range Real.toEReal = Ioo ⊥ ⊤

Tactic:
ext x

Goal state after:
x : EReal
⊢ x ∈ range Real.toEReal ↔ x ∈ Ioo ⊥ ⊤
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : EReal
⊢ x.toReal ≠ 0 ↔ x ≠ 0 ∧ x ≠ ⊤ ∧ x ≠ ⊥

Tactic:
simp only [ne_eq, toReal_eq_zero_iff, not_or]

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

Goal state before:
pp: ⊢ toReal '' Ioo 0 ⊤ = Ioi 0

Tactic:
ext x

Goal state after:
x : ℝ
⊢ x ∈ toReal '' Ioo 0 ⊤ ↔ x ∈ Ioi 0
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: ⊢ toReal '' Ioo ⊥ 0 = Iio 0

Tactic:
ext x

Goal state after:
x : ℝ
⊢ x ∈ toReal '' Ioo ⊥ 0 ↔ x ∈ Iio 0
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
n : ℤ
I : FractionalIdeal R⁰ K
hI : ¬I = 0
⊢ count K v (I ^ (-n)) = -count K v (I ^ n)

Tactic:
rw [eq_neg_iff_add_eq_zero, ← count_mul K v (zpow_ne_zero _ hI) (zpow_ne_zero _ hI),
      ← zpow_add₀ hI, neg_add_cancel, zpow_zero]
    exact count_one K v

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

Goal state before:
pp: x y : ℝ≥0∞
hx : x ≠ 0
h'x : x ≠ ∞
hy : 1 < y
h'y : y ≠ ∞
⊢ ∃ n, x ∈ Ico (y ^ n) (y ^ (n + 1))

Tactic:
lift x to ℝ≥0 using h'x

Goal state after:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0
hx : ↑x ≠ 0
⊢ ∃ n, ↑x ∈ Ico (y ^ n) (y ^ (n + 1))
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x y : ℝ≥0∞
hx : x ≠ 0
h'x : x ≠ ∞
hy : 1 < y
h'y : y ≠ ∞
⊢ ∃ n, x ∈ Ioc (y ^ n) (y ^ (n + 1))

Tactic:
lift x to ℝ≥0 using h'x

Goal state after:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0
hx : ↑x ≠ 0
⊢ ∃ n, ↑x ∈ Ioc (y ^ n) (y ^ (n + 1))
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
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:
simp only [map_one, inv_one, spanSingleton_one, one_mul]

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

Goal state before:
pp: y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
⊢ Ioo 0 ∞ = ⋃ n, Ico (y ^ n) (y ^ (n + 1))

Tactic:
ext x

Goal state after:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
⊢ x ∈ Ioo 0 ∞ ↔ x ∈ ⋃ n, Ico (y ^ n) (y ^ (n + 1))
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x : ℝ≥0∞
hx : 1 ≤ x
a b : ℤ
h : a ≤ b
⊢ x ^ a ≤ x ^ b

Tactic:
obtain a | a := a <;> obtain b | b := b

Goal state after:
case ofNat.ofNat
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.ofNat a ≤ Int.ofNat b
⊢ x ^ Int.ofNat a ≤ x ^ Int.ofNat b

case ofNat.negSucc
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.ofNat a ≤ Int.negSucc b
⊢ x ^ Int.ofNat a ≤ x ^ Int.negSucc b

case negSucc.ofNat
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.ofNat b
⊢ x ^ Int.negSucc a ≤ x ^ Int.ofNat b

case negSucc.negSucc
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.negSucc a ≤ Int.negSucc b
⊢ x ^ Int.negSucc a ≤ x ^ Int.negSucc b
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x : ℝ≥0∞
hx : x ≠ 0
h'x : x ≠ ∞
m n : ℤ
⊢ x ^ (m + n) = x ^ m * x ^ n

Tactic:
lift x to ℝ≥0 using h'x

Goal state after:
m n : ℤ
x : ℝ≥0
hx : ↑x ≠ 0
⊢ ↑x ^ (m + n) = ↑x ^ m * ↑x ^ n
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: γ : Type w
inst✝ : EMetricSpace γ
x y : γ
⊢ 0 < edist x y ↔ x ≠ y

Tactic:
by simp [← not_le]

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

Goal state before:
pp: case neg.inr.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
ha₀ : ∞ ≠ 0
⊢ ∞ * ⨆ i, f i = ⨆ i, ∞ * f i

Tactic:
obtain ⟨i, hi⟩ := not_forall.1 hf

Goal state after:
case neg.inr.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
ha₀ : ∞ ≠ 0
i : ι
hi : ¬f i = 0
⊢ ∞ * ⨆ i, f i = ⨆ i, ∞ * f i
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
⊢ J ∣ Ideal.span {∑ p ∈ s, a p}

Tactic:
by
    rw [Ideal.dvd_iff_le, Ideal.span_singleton_le_iff_mem]
    exact sum_mem fun p hp ↦ Ideal.mul_le_left (ha p hp)

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
H : ∀ ε > 0, ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
ε' : ℝ≥0
ε'0 : 0 < ↑ε'
ε'ε : ↑ε' < ε
s : Set α
hsc : s.Countable
y : α → α
hys : ∀ (x : α), y x ∈ s
hyx : ∀ (x : α), dist x (y x) ≤ ↑ε'
⊢ ∃ t, t.Countable ∧ ⋃ x ∈ t, closedEBall x ε = univ

Tactic:
refine ⟨s, hsc, iUnion₂_eq_univ_iff.2 fun x => ⟨y x, hys _, le_trans ?_ ε'ε.le⟩⟩

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
H : ∀ ε > 0, ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
ε' : ℝ≥0
ε'0 : 0 < ↑ε'
ε'ε : ↑ε' < ε
s : Set α
hsc : s.Countable
y : α → α
hys : ∀ (x : α), y x ∈ s
hyx : ∀ (x : α), dist x (y x) ≤ ↑ε'
x : α
⊢ edist x (y x) ≤ ↑ε'
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: c : ℝ≥0
⊢ ball 0 ↑c = Ico 0 c

Tactic:
ext x

Goal state after:
c x : ℝ≥0
⊢ x ∈ ball 0 ↑c ↔ x ∈ Ico 0 c
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: c : ℝ≥0
⊢ closedBall 0 ↑c = Icc 0 c

Tactic:
ext x

Goal state after:
c x : ℝ≥0
⊢ x ∈ closedBall 0 ↑c ↔ x ∈ Icc 0 c
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: case refine_1
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : Nontrivial α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
⊢ t \ ({x | IsBot x} ∪ {x | IsTop x}) ⊆ s

Tactic:
exact sdiff_subset.trans hts

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

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝² : Fintype β
inst✝¹ : (b : β) → PseudoMetricSpace (X b)
inst✝ : Nonempty β
x : (b : β) → X b
r : ℝ
hr : r ≤ 0
⊢ ball x r = Set.univ.pi fun b ↦ ball (x b) r

Tactic:
by simp [ball_eq_empty.2 hr]

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

Goal state before:
pp: γ : Type w
inst✝ : MetricSpace γ
s : Set γ
ε : ℝ
hε : 0 < ε
hs : s.Pairwise fun x y ↦ ε ≤ dist x y
⊢ s.Pairwise fun x y ↦ (x, y) ∉ {p | dist p.1 p.2 < ε}

Tactic:
simpa using hs

Goal state after: