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

Goal state before:
pp: case IJ
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Free ℤ S
I : Ideal S
hI : Nat.Prime (absNorm I)
this : (span {↑(absNorm I)}).IsPrime
⊢ ↑(absNorm I) ∈ comap (algebraMap ℤ S) I

Tactic:
mem_comap,

Goal state after:
case IJ
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Free ℤ S
I : Ideal S
hI : Nat.Prime (absNorm I)
this : (span {↑(absNorm I)}).IsPrime
⊢ (algebraMap ℤ S) ↑(absNorm I) ∈ I
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
⊢ Function.RightInverse (fun x ↦ ⟨↑(IsUnit.unit ⋯)⁻¹, ⋯⟩) (↑S.fromCommLeftInv).toFun

Tactic:
by
      rintro ⟨x, hx⟩
      ext
      simp [fromLeftInv_eq_iff]

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

Goal state before:
pp: S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
⊢ {I | absNorm I = n}.Finite

Tactic:
obtain hn | hn := Nat.eq_zero_or_pos n
  · simp only [hn, absNorm_eq_zero_iff, Set.ofPred_eq_eq_singleton, Set.finite_singleton]
  · let f := fun I : Ideal S => Ideal.map (Ideal.Quotient.mk (@Ideal.span S _ {↑n})) I
    refine Set.Finite.of_finite_image (f := f) ?_ ?_
    · suffices Finite (S ⧸ @Ideal.span S _ {↑n}) by
        let g := ((↑) : Ideal (S ⧸ @Ideal.span S _ {↑n}) → Set (S ⧸ @Ideal.span S _ {↑n}))
        refine Set.Finite.of_finite_image (f := g) ?_ SetLike.coe_injective.injOn
        exact Set.Finite.subset Set.finite_univ (Set.subset_univ _)
      rw [← absNorm_ne_zero_iff, absNorm_span_singleton]
      simpa only [Ne, Int.natAbs_eq_zero, Algebra.norm_eq_zero_iff, Nat.cast_eq_zero] using
        ne_of_gt hn
    · intro I hI J hJ h
      rw [← comap_map_mk (span_singleton_absNorm_le I), ← hI.symm, ←
        comap_map_mk (span_singleton_absNorm_le J), ← hJ.symm]
      congr

Goal state after:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed[inst✝] Z → closure[inst✝] (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed[inst✝] (closure[inst✝] Z \ Z)
e : Z ∩ closedPoints X = ∅
this : Z ⊆ closure[inst✝] Z ∧ Z = ∅
⊢ False

Tactic:
exact hZ this.2

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

Goal state before:
pp: S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
e : { I // absNorm I ≤ n } ≃ { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n } ⊕ { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n } :=
  (Equiv.subtypeEquivRight ⋯).trans
    (subtypeOrEquiv (fun I ↦ I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n) (fun I ↦ I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n) ⋯)
⊢ Nat.card { I // absNorm I ≤ n } = Nat.card { x // x ∈ (Ideal S)⁰ ∧ absNorm x ≤ n } + 1

Tactic:
simp_rw [Nat.card_congr e, Nat.card_sum, add_right_inj]

Goal state after:
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
n : ℕ
inst✝ : CharZero S
this✝ : Finite { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n }
this : Finite { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n }
e : { I // absNorm I ≤ n } ≃ { I // I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n } ⊕ { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n } :=
  (Equiv.subtypeEquivRight ⋯).trans
    (subtypeOrEquiv (fun I ↦ I ∈ (Ideal S)⁰ ∧ absNorm I ≤ n) (fun I ↦ I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n) ⋯)
⊢ Nat.card { I // I ∉ (Ideal S)⁰ ∧ absNorm I ≤ n } = 1
Module: Mathlib.RingTheory.QuasiFinite.Basic

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
inst✝² : Algebra.IsIntegral R S
inst✝¹ : FiniteType R T
s : S
inst✝ : IsLocalization.Away s T
A : Subalgebra R S := R[s]
⊢ QuasiFinite R T

Tactic:
let sA : A := ⟨s, Algebra.subset_adjoin (by simp)⟩

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
inst✝² : Algebra.IsIntegral R S
inst✝¹ : FiniteType R T
s : S
inst✝ : IsLocalization.Away s T
A : Subalgebra R S := R[s]
sA : ↥A := ⟨s, ⋯⟩
⊢ QuasiFinite R T
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✝³ : QuasiFiniteAt R p
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra R A
q : Ideal (A ⊗[R] S)
inst✝ : q.IsPrime
hq : p = Ideal.comap TensorProduct.includeRight.toRingHom q
⊢ ∀ (r : R),
    (↑↑(Localization.localRingHom p q TensorProduct.includeRight.toRingHom hq)).toFun
        ((algebraMap R (Localization.AtPrime p)) r) =
      (algebraMap R (Localization.AtPrime q)) r

Tactic:
simp [IsScalarTower.algebraMap_apply R S (Localization.AtPrime p),
        IsScalarTower.algebraMap_apply R (A ⊗[R] S) (Localization.AtPrime q)]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal S
inst✝³ : p.IsPrime
inst✝² : IsArtinianRing R
inst✝¹ : EssFiniteType R S
inst✝ : QuasiFiniteAt R p
⊢ ∃ f ∉ p, ↑(PrimeSpectrum.basicOpen f) = {{ asIdeal := p, isPrime := inst✝³ }}

Tactic:
have : IsLocalizedModule p.primeCompl (.id (R := S) (M := Localization.AtPrime p)) :=
    ⟨IsLocalizedModule.map_units (Algebra.linearMap S (Localization.AtPrime p)),
      fun y ↦ ⟨⟨y, 1⟩, by simp⟩, by simpa using ⟨1, p.primeCompl.one_mem⟩⟩

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
⊢ ∃ f ∉ p, ↑(PrimeSpectrum.basicOpen f) = {{ asIdeal := p, isPrime := inst✝³ }}
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case h2
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 σ
x : (Q.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
⊢ Extension.Cotangent.mk ⟨x, hx'⟩ ∈ Submodule.span T ↑(Extension.Cotangent.map (Q.toComp P).toExtensionHom).range

Tactic:
have : Extension.Cotangent.mk (P := (Q.comp P).toExtension) ⟨x, hx'⟩ =
      Extension.Cotangent.mk z := by
      ext; simpa only [val_mk, Ideal.toCotangent_eq, sub_sub_cancel, pow_two, z]

Goal state after:
case h2
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 σ
x : (Q.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
⊢ Extension.Cotangent.mk ⟨x, hx'⟩ ∈ Submodule.span T ↑(Extension.Cotangent.map (Q.toComp P).toExtensionHom).range
Module: Mathlib.RingTheory.Smooth.Basic

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

Tactic:
let P := Generators.self R A
  let f := IsScalarTower.toAlgHom R P.Ring A
  rw [iff_split_surjection f P.algebraMap_surjective]
  have surj : Function.Surjective f.kerSquareLift :=
    Ideal.Quotient.lift_surjective_of_surjective _ _ P.algebraMap_surjective
  have sqz : RingHom.ker f.kerSquareLift.toRingHom ^ 2 = ⊥ := by
    rw [AlgHom.ker_kerSquareLift, Ideal.cotangentIdeal_square]
  dsimp only [AlgHom.toRingHom_eq_coe, RingHom.ker_coe_toRingHom] at sqz
  obtain ⟨g, hg⟩ := H _ sqz (Ideal.quotientKerAlgEquivOfSurjective surj).symm.toAlgHom
  refine ⟨g, AlgHom.ext fun x ↦ congr(f.kerSquareLift.kerLift ($hg x)).trans ?_⟩
  obtain ⟨x, rfl⟩ := (Ideal.quotientKerAlgEquivOfSurjective surj).surjective x
  obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
  simp only [AlgHom.toRingHom_eq_coe, AlgEquiv.coe_toAlgHom, AlgEquiv.symm_apply_apply,
    AlgHom.coe_id, id_eq]
  simp only [Ideal.quotientKerAlgEquivOfSurjective_apply]

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

Goal state before:
pp: case hz.snd
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 σ
x : ↥Q.ker
hx : Extension.Cotangent.mk x ∈ Q.toExtension.cotangentComplex.ker
y : (Q.comp P).toExtension.Cotangent := ⋯
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x
z : T ⊗[S] P.toExtension.CotangentSpace := ⋯
⊢ (0, ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2).2 =
    ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2

pp: case hz.fst
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 σ
x : ↥Q.ker
hx : Extension.Cotangent.mk x ∈ Q.toExtension.cotangentComplex.ker
y : (Q.comp P).toExtension.Cotangent := ⋯
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x
z : T ⊗[S] P.toExtension.CotangentSpace := ⋯
⊢ (0, ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2).1 =
    ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).1

Tactic:
· rfl

Goal state after:
case hz.fst
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 σ
x : ↥Q.ker
hx : Extension.Cotangent.mk x ∈ Q.toExtension.cotangentComplex.ker
y : (Q.comp P).toExtension.Cotangent := ⋯
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x
z : T ⊗[S] P.toExtension.CotangentSpace := ⋯
⊢ (0, ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2).1 =
    ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).1
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
inst✝ : IsPurelyInseparable K L
this : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
⊢ ExpChar (L ⊗[K] L) (ringExpChar K)

Tactic:
refine expChar_of_injective_ringHom (algebraMap K _).injective (ringExpChar K)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
⊢ IsField (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))

Tactic:
let mR := (maximalIdeal R).map (algebraMap R S)

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
mR : Ideal S := Ideal.map (algebraMap R S) (maximalIdeal R)
⊢ IsField (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))
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
inst✝² : Algebra.IsUnramifiedAt R q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : AtPrime.IsLiesOverAlgebra p q
H : Function.Surjective ⇑(algebraMap p.ResidueField q.ResidueField)
this : Module.Finite (Localization.AtPrime p) (Localization.AtPrime q)
x : Localization.AtPrime q
a : p.ResidueField
ha : (algebraMap p.ResidueField q.ResidueField) a = (algebraMap (Localization.AtPrime q) q.ResidueField) x
⊢ x ∈
    (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)).range ⊔
      Submodule.restrictScalars (Localization.AtPrime p) (maximalIdeal (Localization.AtPrime q))

Tactic:
obtain ⟨a, rfl⟩ := residue_surjective a

Goal state after:
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
inst✝² : Algebra.IsUnramifiedAt R q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : AtPrime.IsLiesOverAlgebra p q
H : Function.Surjective ⇑(algebraMap p.ResidueField q.ResidueField)
this : Module.Finite (Localization.AtPrime p) (Localization.AtPrime q)
x : Localization.AtPrime q
a : Localization.AtPrime p
ha :
  (algebraMap p.ResidueField q.ResidueField) ((residue (Localization.AtPrime p)) a) =
    (algebraMap (Localization.AtPrime q) q.ResidueField) x
⊢ x ∈
    (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)).range ⊔
      Submodule.restrictScalars (Localization.AtPrime p) (maximalIdeal (Localization.AtPrime q))
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
x : M
x✝ : (∃ n, ∀ a ∈ I ^ n, a • x = 0) ∧ ∀ a ∈ J, a • x = 0
n : ℕ
this : Disjoint (torsionBySet A M ↑(I ^ n)) (torsionBySet A M ↑J)
h✝ : ∀ a ∈ I ^ n, a • x = 0
right✝ : ∀ a ∈ J, a • x = 0
⊢ x = 0

Tactic:
simp_all [disjoint_def]

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

Goal state before:
pp: r p : ℝ
⊢ r.toNNReal ≤ p.toNNReal ↔ r ≤ p ∨ r ≤ 0

Tactic:
by
  simp_rw [← not_lt, toNNReal_lt_toNNReal_iff', not_and_or]

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

Goal state before:
pp: n : ℕ
r : ℝ
⊢ ↑n ≤ r.toNNReal ↔ ↑n ≤ r ∨ n = 0

Tactic:
simpa [n.cast_nonneg.ge_iff_eq'] using toNNReal_le_toNNReal_iff' (r := n)

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
p q : GroupSeminorm E
x : E
⊢ p x⁻¹ + q x⁻¹ = p x + q x

Tactic:
simp_rw [map_inv_eq_map p, map_inv_eq_map q]

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
⊢ iSupIndep fun i ↦ torsionBySet A M ↑(i.asIdeal ^ m)

Tactic:
rw [iSupIndep_iff_supIndep]

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

Tactic:
simp_rw [if_neg hx]

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

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
⊢ a + b - a = b

Tactic:
by
  simp [ha]

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

Goal state before:
pp: x : ℝ≥0∞
hx : x ≠ ∞
⊢ ↑x.toReal = ↑x

Tactic:
by
  lift x to ℝ≥0 using hx
  rfl

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

Goal state before:
pp: a : ℝ≥0
n : ℕ
⊢ (↑a ^ (n + 1))⁻¹ = (↑a)⁻¹ ^ (n + 1)

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)
    · simp [top_pow]
    · have := pow_ne_zero (n + 1) ha
      norm_cast
      rw [inv_pow]

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

Goal state before:
pp: case inr
x : EReal
hx : x ≤ 0
⊢ ↑x.toENNReal = max 0 x

Tactic:
· rw [toENNReal_of_nonpos hx, max_eq_left hx, coe_ennreal_zero]

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

Goal state before:
pp: a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ a⁻¹⁻¹ = a

Tactic:
by_cases a = 0 <;> cases a

Goal state after:
case pos.top
a b c d : ℝ≥0∞
r p q : ℝ≥0
h✝ : ∞ = 0
⊢ ∞⁻¹⁻¹ = ∞

case pos.coe
a b c d : ℝ≥0∞
r p q x✝ : ℝ≥0
h✝ : ↑x✝ = 0
⊢ (↑x✝)⁻¹⁻¹ = ↑x✝

case neg.top
a b c d : ℝ≥0∞
r p q : ℝ≥0
h✝ : ¬∞ = 0
⊢ ∞⁻¹⁻¹ = ∞

case neg.coe
a b c d : ℝ≥0∞
r p q x✝ : ℝ≥0
h✝ : ¬↑x✝ = 0
⊢ (↑x✝)⁻¹⁻¹ = ↑x✝
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ⊢ StrictAnti Inv.inv

Tactic:
intro a b h
  lift a to ℝ≥0 using h.ne_top
  cases b; · simp
  rw [coe_lt_coe] at h
  rcases eq_or_ne a 0 with (rfl | ha); · simp [h]
  rw [← coe_inv h.ne_bot, ← coe_inv ha, coe_lt_coe]
  exact NNReal.inv_lt_inv ha h

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

Goal state before:
pp: case e'_2
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
⊢ ∏ i ∈ Finite.toFinset h_exps, ↑i.asIdeal ^ exps i =
    ∏ a ∈ { support := Finite.toFinset h_exps, toFun := exps, mem_support_toFun := ⋯ }.support,
      ↑a.asIdeal ^ { support := Finite.toFinset h_exps, toFun := exps, mem_support_toFun := ⋯ } a

pp: case e'_2.h
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
⊢ (mulSupport fun v ↦ ↑v.asIdeal ^ exps v) ⊆ ↑(Finite.toFinset h_exps)

Tactic:
· rfl

Goal state after:
case e'_2.h
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
⊢ (mulSupport fun v ↦ ↑v.asIdeal ^ exps v) ⊆ ↑(Finite.toFinset h_exps)
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case negSucc
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ∞
a✝ : ℕ
⊢ 0 < a ^ Int.negSucc a✝

Tactic:
simp only [h'a, pow_eq_top_iff, zpow_negSucc, Ne, ENNReal.inv_pos, false_and,
      not_false_eq_true]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
J : Ideal R
hJ : J ≠ 0
⊢ count K v ↑J = ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors)

Tactic:
by
  rw [count_well_defined K (J := J) (a := 1), Ideal.span_singleton_one, sub_eq_self,
    Nat.cast_eq_zero, ← Ideal.one_eq_top, Associates.mk_one, Associates.factors_one,
    Associates.count_zero v.associates_irreducible]
  · simpa only [ne_eq, coeIdeal_eq_zero]
  · simp only [map_one, inv_one, spanSingleton_one, one_mul]

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
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Ideal.span {a} ≠ 0
hJ_ne_zero : J ≠ 0
v : HeightOneSpectrum R
hv :
  v ∈
    {v |
      ¬↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
            ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
          0}
hv_irred : Irreducible v.asIdeal
h_notMem :
  (Associates.mk v.asIdeal).count (Associates.mk J).factors = 0 ∧
    (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors = 0
⊢ False

Tactic:
rw [mem_ofPred_eq, h_notMem.1, h_notMem.2, sub_self] at hv

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
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Ideal.span {a} ≠ 0
hJ_ne_zero : J ≠ 0
v : HeightOneSpectrum R
hv : ¬0 = 0
hv_irred : Irreducible v.asIdeal
h_notMem :
  (Associates.mk v.asIdeal).count (Associates.mk J).factors = 0 ∧
    (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors = 0
⊢ False
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y z w : α
⊢ dist x z + dist z w ≤ dist x y + dist y z + dist z w

Tactic:
by gcongr; apply dist_triangle x y z

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
⊢ Bornology.IsBounded s ↔ ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → nndist x y ≤ C

Tactic:
by
  simp only [isBounded_iff_exists_ge 0, NNReal.exists, ← NNReal.coe_le_coe, ← dist_nndist,
    NNReal.coe_mk, exists_prop]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : PseudoMetricSpace β
t : Set β
f : α → β
a : α
b : β
⊢ (∀ (ib : ℝ), 0 < ib → ∃ ia, 0 < ia ∧ ∀ x ∈ ball a ia ∩ s, f x ∈ ball b ib ∩ t) ↔
    ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → f x ∈ t ∧ dist (f x) b < ε

Tactic:
simp only [inter_comm _ s, inter_comm _ t, mem_inter_iff, and_imp, gt_iff_lt, mem_ball]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ≥0
⊢ eball x ↑ε = ball x ↑ε

Tactic:
rw [← eball_ofReal]
  simp

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

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
⊢ TendstoLocallyUniformlyOn F f p s ↔ ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε

Tactic:
by
  refine ⟨fun H ε hε => H _ (dist_mem_uniformity hε), fun H u hu x hx => ?_⟩
  rcases mem_uniformity_dist.1 hu with ⟨ε, εpos, hε⟩
  rcases H ε εpos x hx with ⟨t, ht, Ht⟩
  exact ⟨t, ht, Ht.mono fun n hs x hx => hε (hs x hx)⟩

Goal state after: