mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
⊢ (algebraMap R (Localization p.primeCompl)) r = 1

Tactic:
simpa [PrimeSpectrum.toPiLocalization,
      -FaithfulSMul.algebraMap_eq_one_iff] using funext_iff.mp hr ⟨p, inferInstance⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case pos
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : IsDedekindDomain S
inst✝³ : Free ℤ S
inst✝² : Module.Finite ℤ S
E : Type u_2
e : E
inst✝¹ : EquivLike E S ↥⊥
inst✝ : AddEquivClass E S ↥⊥
this✝ : 1 ≠ 0
this : 1 = 0
⊢ (LinearMap.det (↑ℤ (Submodule.subtype ⊥) ∘ₗ (↑e).toIntLinearMap)).natAbs = absNorm ⊥

Tactic:
contradiction

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case h₂
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 : Ideal S
hI' : IsUnit I
hI : p ∣ ↑(absNorm I)
⊢ ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ I

Tactic:
obtain rfl : I = ⊤ := by simpa using hI'

Goal state after:
case h₂
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
hI' : IsUnit ⊤
hI : p ∣ ↑(absNorm ⊤)
⊢ ∃ P, P.IsMaximal ∧ under ℤ P = span {p} ∧ P ∣ ⊤
Module: Mathlib.RingTheory.Localization.InvSubmonoid

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
⊢ x ∈ invSubmonoid M S ↔ ∃ m, mk' S 1 m = x

Tactic:
← toInvSubmonoid_eq_mk'

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : S
⊢ x ∈ invSubmonoid M S ↔ ∃ m, ↑((toInvSubmonoid M S) m) = x
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
x : X
hx : IsLocallyClosed {x}
⊢ IsClosed[inst✝¹] {x}

Tactic:
by
  obtain ⟨_, ⟨y, rfl : y = x, rfl⟩, hy'⟩ :=
    nonempty_inter_closedPoints (Set.singleton_nonempty x) hx
  exact hy'

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

Goal state before:
pp: case neg
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).inertiaDeg R = q.inertiaDeg R

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).inertiaDeg R = q.inertiaDeg R

Tactic:
· rw [inertiaDeg_of_not_isPrime, inertiaDeg_of_not_isPrime] <;> simpa

Goal state after:
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).inertiaDeg R = q.inertiaDeg R
Module: Mathlib.RingTheory.RamificationInertia.Inertia

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : q.IsPrime
p : Ideal R := under R q
f₀ : S ≃ₐ[R] S := (MulSemiringAction.toAlgAut G R S) g
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
this : Algebra (Localization.AtPrime p) (Localization.AtPrime (g • q)) :=
  Localization.AtPrime.algebraOfLiesOver p (g • q)
⊢ (g • q).inertiaDeg R = q.inertiaDeg R

Tactic:
inertiaDeg_eq p q,

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : q.IsPrime
p : Ideal R := under R q
f₀ : S ≃ₐ[R] S := (MulSemiringAction.toAlgAut G R S) g
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
this : Algebra (Localization.AtPrime p) (Localization.AtPrime (g • q)) :=
  Localization.AtPrime.algebraOfLiesOver p (g • q)
⊢ (g • q).inertiaDeg R = Module.finrank p.ResidueField q.ResidueField
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
this✝⁵ : IsLocalizedModule p.primeCompl LinearMap.id
this✝⁴ : Module.Finite R (Localization.AtPrime p)
this✝³ : Module.Finite S (Localization.AtPrime p)
this✝² : IsArtinianRing (Localization.AtPrime p)
this✝¹ : IsNoetherianRing S
this✝ : Module.FinitePresentation S (Localization.AtPrime p)
r : S
hrp : r ∈ p.primeCompl
H : IsLocalizedModule.Away r (Algebra.linearMap S (Localization.AtPrime p))
this : IsLocalization (Submonoid.powers r) (Localization.AtPrime p)
φ : Localization.Away r ≃ₐ[S] Localization.AtPrime p :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (Localization.AtPrime p)
hrq :
  PrimeSpectrum.comap (algebraMap S (Localization.Away r))
      ((PrimeSpectrum.comapEquiv φ.toRingEquiv).symm (IsLocalRing.closedPoint (Localization.AtPrime p))) ∈
    ↑(PrimeSpectrum.basicOpen r)
⊢ Ideal.comap ((↑φ).comp (algebraMap S (Localization.Away r)))
      (IsLocalRing.closedPoint (Localization.AtPrime p)).asIdeal =
    p

Tactic:
← AlgEquiv.toAlgHom_toRingHom,

Goal state after:
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
this✝⁵ : IsLocalizedModule p.primeCompl LinearMap.id
this✝⁴ : Module.Finite R (Localization.AtPrime p)
this✝³ : Module.Finite S (Localization.AtPrime p)
this✝² : IsArtinianRing (Localization.AtPrime p)
this✝¹ : IsNoetherianRing S
this✝ : Module.FinitePresentation S (Localization.AtPrime p)
r : S
hrp : r ∈ p.primeCompl
H : IsLocalizedModule.Away r (Algebra.linearMap S (Localization.AtPrime p))
this : IsLocalization (Submonoid.powers r) (Localization.AtPrime p)
φ : Localization.Away r ≃ₐ[S] Localization.AtPrime p :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (Localization.AtPrime p)
hrq :
  PrimeSpectrum.comap (algebraMap S (Localization.Away r))
      ((PrimeSpectrum.comapEquiv φ.toRingEquiv).symm (IsLocalRing.closedPoint (Localization.AtPrime p))) ∈
    ↑(PrimeSpectrum.basicOpen r)
⊢ Ideal.comap ((↑↑φ).comp (algebraMap S (Localization.Away r)))
      (IsLocalRing.closedPoint (Localization.AtPrime p)).asIdeal =
    p
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₂
Q : Generators S T ι
P : Generators R S σ
i : ι ⊕ σ
⊢ (LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ ↑(compEquiv Q P))
      ((Q.comp P).cotangentSpaceBasis i) =
    (Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom) ((Q.comp P).cotangentSpaceBasis i)

Tactic:
apply Q.cotangentSpaceBasis.repr.injective

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₂
Q : Generators S T ι
P : Generators R S σ
i : ι ⊕ σ
⊢ Q.cotangentSpaceBasis.repr
      ((LinearMap.fst T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) ∘ₗ ↑(compEquiv Q P))
        ((Q.comp P).cotangentSpaceBasis i)) =
    Q.cotangentSpaceBasis.repr
      ((Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom) ((Q.comp P).cotangentSpaceBasis i))
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: case refine_1
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
this : Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) ≤ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P)).ker →
  P ⧸ Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) →ₗ[R] S ⊗[P] Ω[P⁄R] :=
  (Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2)).liftQ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P))
⊢ Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) ≤ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P)).ker

Tactic:
rintro x hx
    simp only [Submodule.restrictScalars_mem, pow_two] at hx
    simp only [LinearMap.mem_ker, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
      Derivation.coeFn_coe, Function.comp_apply, mk_apply]
    refine Submodule.smul_induction_on hx ?_ ?_
    · intro x hx y hy
      simp only [smul_eq_mul, Derivation.leibniz, tmul_add, ← smul_tmul, Algebra.smul_def,
        mul_one, RingHom.mem_ker.mp hx, RingHom.mem_ker.mp hy, zero_tmul, zero_add]
    · intro x y hx hy; simp only [map_add, hx, hy, tmul_add, zero_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
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
f₁ : Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] →ₗ[P ⧸ RingHom.ker (algebraMap P S) ^ 2] S ⊗[P] Ω[P⁄R] :=
  (derivationQuotKerSq R P S).liftKaehlerDifferential
f₂ : S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] →ₗ[S] S ⊗[P] Ω[P⁄R] :=
  AlgebraTensorModule.lift
    ((LinearMap.ringLmapEquivSelf S S
          (Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] →ₗ[P ⧸ RingHom.ker (algebraMap P S) ^ 2] S ⊗[P] Ω[P⁄R])).symm
      f₁)
f₃ : Ω[P⁄R] →ₗ[P] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] :=
  KaehlerDifferential.map R R P (P ⧸ RingHom.ker (algebraMap P S) ^ 2)
f₄ : Ω[P⁄R] →ₗ[P] S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] :=
  ↑P ((mk (P ⧸ RingHom.ker (algebraMap P S) ^ 2) S Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R]) 1) ∘ₗ f₃
f₅ : S ⊗[P] Ω[P⁄R] →ₗ[S] S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] :=
  AlgebraTensorModule.lift
    ((LinearMap.ringLmapEquivSelf S S
          (Ω[P⁄R] →ₗ[P] S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R])).symm
      f₄)
a : P
⊢ (((AlgebraTensorModule.curry (f₅ ∘ₗ f₂)) 1).compDer (D R (P ⧸ RingHom.ker (algebraMap P S) ^ 2)))
      ((Ideal.Quotient.mk (RingHom.ker (algebraMap P S) ^ 2)) a) =
    (((AlgebraTensorModule.curry LinearMap.id) 1).compDer (D R (P ⧸ RingHom.ker (algebraMap P S) ^ 2)))
      ((Ideal.Quotient.mk (RingHom.ker (algebraMap P S) ^ 2)) a)

Tactic:
simp [f₁, f₂, f₃, f₄, f₅]

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
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
f₁ : Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] →ₗ[P ⧸ RingHom.ker (algebraMap P S) ^ 2] S ⊗[P] Ω[P⁄R] :=
  (derivationQuotKerSq R P S).liftKaehlerDifferential
f₂ : S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] →ₗ[S] S ⊗[P] Ω[P⁄R] :=
  AlgebraTensorModule.lift
    ((LinearMap.ringLmapEquivSelf S S
          (Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] →ₗ[P ⧸ RingHom.ker (algebraMap P S) ^ 2] S ⊗[P] Ω[P⁄R])).symm
      f₁)
f₃ : Ω[P⁄R] →ₗ[P] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] :=
  KaehlerDifferential.map R R P (P ⧸ RingHom.ker (algebraMap P S) ^ 2)
f₄ : Ω[P⁄R] →ₗ[P] S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] :=
  ↑P ((mk (P ⧸ RingHom.ker (algebraMap P S) ^ 2) S Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R]) 1) ∘ₗ f₃
f₅ : S ⊗[P] Ω[P⁄R] →ₗ[S] S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R] :=
  AlgebraTensorModule.lift
    ((LinearMap.ringLmapEquivSelf S S
          (Ω[P⁄R] →ₗ[P] S ⊗[P ⧸ RingHom.ker (algebraMap P S) ^ 2] Ω[P ⧸ RingHom.ker (algebraMap P S) ^ 2⁄R])).symm
      f₄)
a : P
⊢ (((AlgebraTensorModule.curry (f₂ ∘ₗ f₅)) 1).compDer (D R P)) a =
    (((AlgebraTensorModule.curry LinearMap.id) 1).compDer (D R P)) a

Tactic:
simp [f₁, f₂, f₃, f₄, f₅]

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

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

Tactic:
← AlgEquiv.toAlgHom_toRingHom,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : q.IsPrime
p : Ideal R := under R q
f₀ : S ≃ₐ[R] S := (MulSemiringAction.toAlgAut G R S) g
hg : g • q = map f₀ q
Sq : Type u_2 := Localization.AtPrime q
Sq' : Type u_2 := Localization.AtPrime (map f₀ q)
f : Sq ≃ₐ[R] Sq' := Localization.localAlgEquiv q (map f₀ q) f₀ ⋯
this✝ : Algebra Sq Sq' := f.toRingEquiv.toRingHom.toAlgebra
this : IsScalarTower R Sq Sq'
⊢ map ((algebraMap Sq Sq').comp (algebraMap R Sq)) p =
    map ((↑↑(AlgEquiv.ofBijective (Algebra.ofId Sq Sq') ⋯)).comp (algebraMap R Sq)) p
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r : ℝ
hr : 0 ≤ r
⊢ r.toNNReal = NNReal.mk r hr

Tactic:
by
  simp_rw [Real.toNNReal, max_eq_left hr]

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

Goal state before:
pp: ⊢ sInf Set.univ = 0

Tactic:
simp [sInf_def]

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

Goal state before:
pp: s : Set ℝ
h₁ : BddBelow s
h₂ : BddAbove s
⊢ sInf s ≤ sSup s

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hne)

Goal state after:
case inl
h₁ : BddBelow ∅
h₂ : BddAbove ∅
⊢ sInf ∅ ≤ sSup ∅

case inr
s : Set ℝ
h₁ : BddBelow s
h₂ : BddAbove s
hne : s.Nonempty
⊢ sInf s ≤ sSup s
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h✝ : HasFiniteMulSupport fun v ↦ v.maxPowDividing I
⊢ ∏ v ∈ Finite.toFinset h✝, v.maxPowDividing I ≠ 0

pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h✝ : ¬HasFiniteMulSupport fun v ↦ v.maxPowDividing I
⊢ 1 ≠ 0

Tactic:
· rw [Finset.prod_ne_zero_iff]
    intro v _
    apply pow_ne_zero _ v.ne_bot

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h✝ : ¬HasFiniteMulSupport fun v ↦ v.maxPowDividing I
⊢ 1 ≠ 0
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case pos
r p : ℝ≥0
h : 1 ≤ r * p
h✝ : r = 0
⊢ r⁻¹ ≤ p

Tactic:
simp [*, inv_le]

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

Goal state before:
pp: case neg
r p : ℝ≥0
h : 1 ≤ r * p
h✝ : ¬r = 0
⊢ r⁻¹ ≤ p

Tactic:
simp [*, inv_le]

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

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
r : ℚ
hrx : x < ↑r
⊢ Nonempty { r' // x < ↑r' }

Tactic:
exact ⟨⟨r, hrx⟩⟩

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✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝ : E
p q : GroupSeminorm E
x y u v : E
⊢ ⨅ y_1, p y_1 + q (x * y / y_1) ≤ p u + q (x / u) + (p v + q (y / v))

Tactic:
refine ciInf_le_of_le mul_bddBelow_range_add (u * v) ?_

Goal state after:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝ : E
p q : GroupSeminorm E
x y u v : E
⊢ p (u * v) + q (x * y / (u * v)) ≤ p u + q (x / u) + (p v + q (y / v))
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: t : Set ℝ≥0
h : t.OrdConnected
⊢ (ofNNReal '' t).OrdConnected

Tactic:
refine ⟨forall_mem_image.2 fun x hx => forall_mem_image.2 fun y hy z hz => ?_⟩
  rcases ENNReal.le_coe_iff.1 hz.2 with ⟨z, rfl, -⟩
  exact mem_image_of_mem _ (h.out hx hy ⟨ENNReal.coe_le_coe.1 hz.1, ENNReal.coe_le_coe.1 hz.2⟩)

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
⊢ spanSingleton R⁰ (mk' K n d) ≠ 0

Tactic:
spanSingleton_ne_zero_iff,

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
⊢ mk' K n d ≠ 0
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : α
⊢ [[x, x]] ⊆ s ↔ x ∈ s

Tactic:
uIcc_self,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : α
⊢ {x} ⊆ s ↔ x ∈ s
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: a b c : ℝ≥0∞
ha : a ≠ ∞
h : b ≤ a
⊢ a - c - (a - b) = b - c

Tactic:
have hb : b ≠ ∞ := ne_top_of_le_ne_top ha h
  lift a to ℝ≥0 using ha
  lift b to ℝ≥0 using hb
  cases c
  · simp
  · norm_cast
    rw [tsub_tsub_tsub_cancel_left]
    exact mod_cast h

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 : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
⊢ count K v I =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)

Tactic:
by
  set a₁ := choose (exists_eq_spanSingleton_mul I)
  set J₁ := choose (choose_spec (exists_eq_spanSingleton_mul I))
  have h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁ :=
    (choose_spec (choose_spec (exists_eq_spanSingleton_mul I))).2
  have h_a₁_ne_zero : a₁ ≠ 0 := (choose_spec (choose_spec (exists_eq_spanSingleton_mul I))).1
  have h_J₁_ne_zero : J₁ ≠ 0 := ideal_factor_ne_zero hI h_a₁J₁
  have h_a_ne_zero : Ideal.span {a} ≠ 0 := constant_factor_ne_zero hI h_aJ
  have h_J_ne_zero : J ≠ 0 := ideal_factor_ne_zero hI h_aJ
  have h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0 := by
    rw [ne_eq, spanSingleton_eq_zero_iff, ← (algebraMap R K).map_zero,
      Injective.eq_iff (IsLocalization.injective K (le_refl R⁰))]
    exact h_a₁_ne_zero
  have h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0 := by
    rw [ne_eq, spanSingleton_eq_zero_iff, ← (algebraMap R K).map_zero,
      Injective.eq_iff (IsLocalization.injective K (le_refl R⁰))]
    rw [ne_eq, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot] at h_a_ne_zero
    exact h_a_ne_zero
  have hv : Irreducible (Associates.mk v.asIdeal) := by
    exact Associates.irreducible_mk.mpr v.irreducible
  rw [h_a₁J₁, ← div_spanSingleton, ← div_spanSingleton, div_eq_div_iff h_a₁' h_a',
    ← coeIdeal_span_singleton, ← coeIdeal_span_singleton, ← coeIdeal_mul, ← coeIdeal_mul] at h_aJ
  rw [count, dif_neg hI, sub_eq_sub_iff_add_eq_add, ← natCast_add, ← natCast_add, natCast_inj,
    ← Associates.count_mul _ _ hv, ← Associates.count_mul _ _ hv, Associates.mk_mul_mk,
    Associates.mk_mul_mk, coeIdeal_injective h_aJ]
  · rw [ne_eq, Associates.mk_eq_zero]; exact h_J_ne_zero
  · rw [ne_eq, Associates.mk_eq_zero, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot]
    exact h_a₁_ne_zero
  · rw [ne_eq, Associates.mk_eq_zero]; exact h_J₁_ne_zero
  · rw [ne_eq, Associates.mk_eq_zero]; exact h_a_ne_zero

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

Goal state before:
pp: case inl
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ∞
i : ι
hi : a < f i
⊢ ∀ (b : ℝ≥0∞), ⊥ < b → ∃ i, a - f i < b

Tactic:
exact fun x hx ↦ ⟨i, by simpa [hi.le, tsub_eq_zero_of_le]⟩

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

Goal state before:
pp: case pos
x : EReal
hx : 0 ≤ x
h_top : x = ⊤
⊢ ↑(if x = ⊤ then ∞ else ENNReal.ofReal x.toReal) = x

Tactic:
rw [if_pos h_top, h_top]
    rfl

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

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

pp: case neg
x : ℝ≥0∞
h_top : ¬x = ∞
⊢ (↑x).toENNReal = x

Tactic:
· rw [h_top, coe_ennreal_top, toENNReal_top]

Goal state after:
case neg
x : ℝ≥0∞
h_top : ¬x = ∞
⊢ (↑x).toENNReal = x
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case coe.inr
a c : ℝ≥0∞
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ∞ ∨ c ≠ ∞
hb : b ≠ 0
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c

Tactic:
rw [← coe_ne_zero] at hb
    rw [← ENNReal.mul_le_mul_iff_left hb coe_ne_top, ENNReal.div_mul_cancel hb coe_ne_top]

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

Goal state before:
pp: a b c : ℝ≥0∞
hb0 : b ≠ 0 ∨ c ≠ ∞
hbt : b ≠ ∞ ∨ c ≠ 0
⊢ a / b ≤ c ↔ a ≤ c * b

Tactic:
suffices a * b⁻¹ ≤ c ↔ a ≤ c / b⁻¹ by simpa [div_eq_mul_inv]

Goal state after:
a b c : ℝ≥0∞
hb0 : b ≠ 0 ∨ c ≠ ∞
hbt : b ≠ ∞ ∨ c ≠ 0
⊢ a * b⁻¹ ≤ c ↔ a ≤ c / b⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c : ℝ≥0∞
h : a ≤ b * c
⊢ a / c ≤ b

Tactic:
by
  by_cases h0 : c = 0
  · have : a = 0 := by simpa [h0] using h
    simp [*]
  by_cases hinf : c = ∞; · simp [hinf]
  exact (ENNReal.div_le_iff_le_mul (Or.inl h0) (Or.inl hinf)).2 h

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

Goal state before:
pp: a b : ℝ≥0∞
h₁ : b = ∞ → a ≠ 0
h₂ : a = ∞ → b ≠ 0
⊢ a⁻¹ ≤ b ↔ 1 ≤ a * b

Tactic:
rw [← one_div, ENNReal.div_le_iff_le_mul, mul_comm]
  exacts [or_not_of_imp h₁, not_or_of_imp h₂]

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

Goal state before:
pp: r : ℝ≥0
hr : r ≠ 0
n : ℤ
⊢ ↑(r ^ n) = ↑r ^ n

Tactic:
rcases n with n | n

Goal state after:
case ofNat
r : ℝ≥0
hr : r ≠ 0
n : ℕ
⊢ ↑(r ^ Int.ofNat n) = ↑r ^ Int.ofNat n

case negSucc
r : ℝ≥0
hr : r ≠ 0
n : ℕ
⊢ ↑(r ^ Int.negSucc n) = ↑r ^ Int.negSucc n
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α✝ : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s : Set α
hs : s ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
t : Set α
ht : t ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
x : α
hx : x ∈ s
y : α
hy : y ∈ t
⊢ ∃ C, ∀ z ∈ s ∪ t, dist x z ≤ C

Tactic:
rcases hs with ⟨Cs, hs⟩

Goal state after:
α✝ : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s t : Set α
ht : t ∈ {s | ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C}
x : α
hx : x ∈ s
y : α
hy : y ∈ t
Cs : ℝ
hs : ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ Cs
⊢ ∃ C, ∀ z ∈ s ∪ t, dist x z ≤ C