mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: case pos
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : IsLocalRing A
inst✝⁶ : IsLocalRing B
inst✝⁵ : Algebra A B
inst✝⁴ : IsLocalHom (algebraMap A B)
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : IsScalarTower A B M
h : IsFiniteLength B M
⊢ length A M = length B M * length (ResidueField A) (ResidueField B)

Tactic:
obtain ⟨s, hs_bot, hs_top⟩ := isFiniteLength_iff_exists_compositionSeries.mp h
    rw [← length_compositionSeries s hs_bot hs_top]
    suffices ∀ k, length A (s k) = k * Module.length (ResidueField A) (ResidueField B) by
      rw [← Fin.val_last s.length, ← this, ← RelSeries.last, hs_top]
      exact length_top.symm
    intro k
    induction k using Fin.induction with
    | zero => rw [← RelSeries.head, hs_bot]; simp
    | succ i hi => simpa [hi, add_one_mul] using (s.step i).length_restrictScalars A

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

Goal state before:
pp: case pos
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
hr : r.IsPrime
⊢ r.inertiaDeg R = q.inertiaDeg R * r.inertiaDeg S

Tactic:
have : q.IsPrime := isPrime_of_liesOver r q
    have : q.LiesOver (r.under R) := LiesOver.tower_bot r q (r.under R)
    let := Localization.AtPrime.algebraOfLiesOver (r.under R) r
    let := Localization.AtPrime.algebraOfLiesOver (r.under R) q
    let := Localization.AtPrime.algebraOfLiesOver q r
    rw [inertiaDeg_def, inertiaDeg_eq (r.under R), inertiaDeg_eq q, eq_comm]
    apply Module.finrank_mul_finrank

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✝³ : 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
f : A ⊗[R] Localization.AtPrime p →ₐ[A] Localization.AtPrime q :=
  TensorProduct.lift (ofId A (Localization.AtPrime q))
    { toRingHom := Localization.localRingHom p q TensorProduct.includeRight.toRingHom hq, commutes' := ⋯ } ⋯
⊢ QuasiFiniteAt A q

Tactic:
let g : A ⊗[R] S →ₐ[A] A ⊗[R] Localization.AtPrime p :=
    Algebra.TensorProduct.map (.id _ _) (IsScalarTower.toAlgHom _ _ _)

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✝³ : 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
f : A ⊗[R] Localization.AtPrime p →ₐ[A] Localization.AtPrime q :=
  TensorProduct.lift (ofId A (Localization.AtPrime q))
    { toRingHom := Localization.localRingHom p q TensorProduct.includeRight.toRingHom hq, commutes' := ⋯ } ⋯
g : A ⊗[R] S →ₐ[A] A ⊗[R] Localization.AtPrime p :=
  TensorProduct.map (AlgHom.id A A) (IsScalarTower.toAlgHom R S (Localization.AtPrime p))
⊢ QuasiFiniteAt A q
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
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
⊢ ∃ f ∉ p, ↑(PrimeSpectrum.basicOpen f) = {{ asIdeal := p, isPrime := inst✝³ }}

Tactic:
have : Module.FinitePresentation S (Localization.AtPrime p) :=
    Module.finitePresentation_of_finite _ _

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)
⊢ ∃ f ∉ p, ↑(PrimeSpectrum.basicOpen f) = {{ asIdeal := p, isPrime := inst✝³ }}
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
B : Type u_1
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
C : Type u_4
inst✝² : CommRing C
inst✝¹ : Algebra R C
inst✝ : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective ⇑g
hg' : IsNilpotent (RingHom.ker g)
x : A
⊢ (Ideal.quotientKerAlgEquivOfSurjective hg).symm (g ((liftOfSurjective f g hg hg') x)) =
    (Ideal.Quotient.mk (RingHom.ker g))
      ((lift (RingHom.ker g) hg' ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm).comp f)) x)

Tactic:
apply (Ideal.quotientKerAlgEquivOfSurjective hg).injective

Goal state after:
R : Type u
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
B : Type u_1
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
C : Type u_4
inst✝² : CommRing C
inst✝¹ : Algebra R C
inst✝ : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective ⇑g
hg' : IsNilpotent (RingHom.ker g)
x : A
⊢ (Ideal.quotientKerAlgEquivOfSurjective hg)
      ((Ideal.quotientKerAlgEquivOfSurjective hg).symm (g ((liftOfSurjective f g hg hg') x))) =
    (Ideal.quotientKerAlgEquivOfSurjective hg)
      ((Ideal.Quotient.mk (RingHom.ker g))
        ((lift (RingHom.ker g) hg' ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm).comp f)) x))
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
x : M
⊢ (TensorProduct.AlgebraTensorModule.lift (↑R (lsmul S S M).toLinearMap.flip).flip ∘ₗ sec R S M) x = LinearMap.id x

Tactic:
simp only [sec, LinearMap.coe_comp, LinearMap.coe_mk, LinearMap.coe_toAddHom,
    Function.comp_apply, LinearMap.flip_apply, TensorProduct.AlgebraTensorModule.mapBilinear_apply,
    TensorProduct.AlgebraTensorModule.lift_apply, LinearMap.id_coe, id_eq]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
x : M
⊢ (_root_.TensorProduct.lift (↑R (↑R (lsmul S S M).toLinearMap.flip).flip))
      ((TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip x)) (elem R S)) =
    x
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing P
inst✝² : CommRing S
inst✝¹ : Algebra R P
inst✝ : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
x y : P
h : (algebraMap P S) x = (algebraMap P S) y
⊢ x = y - ↑(l (1 ⊗ₜ[P] (D R P) y)) + ↑(l (1 ⊗ₜ[P] (D R P) x))

Tactic:
sub_add_comm,

Goal state after:
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing P
inst✝² : CommRing S
inst✝¹ : Algebra R P
inst✝ : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
x y : P
h : (algebraMap P S) x = (algebraMap P S) y
⊢ x = ↑(l (1 ⊗ₜ[P] (D R P) x)) - ↑(l (1 ⊗ₜ[P] (D R P) y)) + y
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: case right
R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.infinitesimal.Cotangent
hx : x ∈ P.infinitesimal.cotangentComplex.ker
⊢ ∃ a, (map P.toInfinitesimal) a = ⟨x, hx⟩

Tactic:
obtain ⟨x, rfl⟩ := (Cotangent.map_toInfinitesimal_bijective P).2 x

Goal state after:
case right
R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
x : P.Cotangent
hx : (Cotangent.map P.toInfinitesimal) x ∈ P.infinitesimal.cotangentComplex.ker
⊢ ∃ a, (map P.toInfinitesimal) a = ⟨(Cotangent.map P.toInfinitesimal) x, hx⟩
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
⊢ (IsLocalization.lift ⋯) (IsLocalization.mk' (Localization M') x ⟨s, ⋯⟩) =
    IsLocalization.mk' T ((algebraMap P.Ring S) x) ⟨(algebraMap P.Ring S) s, hs⟩

Tactic:
rw [IsLocalization.lift_mk'_spec]

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 ⋯
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⟩
Module: Mathlib.RingTheory.RamificationInertia.Ramification

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

Tactic:
ramificationIdx_of_not_isPrime,

Goal state after:
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
⊢ 0 = q.ramificationIdx R

case neg.hq
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).IsPrime
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
⊢ (IsLocalization.lift ⋯) (IsLocalization.mk' (Localization M') x ⟨s, ⋯⟩) =
    IsLocalization.mk' T ((algebraMap P.Ring S) x) ⟨(algebraMap P.Ring S) s, hs⟩

Tactic:
rw [IsLocalization.lift_mk'_spec]

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
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⟩
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
⊢ ↑(#(s.biUnion S)) = ∑ t, (-1) ^ (#↑t + 1) * ↑(#((↑t).inf' ⋯ S))

Tactic:
by
  simpa using inclusion_exclusion_sum_biUnion (G := ℤ) s S (f := 1)

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
⊢ ∃ i, ∀ j ≥ i, |(fun n ↦ ↑(f n) / ↑n) j - (fun n ↦ ↑(f n) / ↑n) i| < ε

Tactic:
suffices ∀ j ≥ ⌈ε⁻¹⌉₊, ∀ k ≥ ⌈ε⁻¹⌉₊, (f j / j - f k / k : ℚ) < ε by
      refine ⟨_, fun j ij => abs_lt.2 ⟨?_, this _ ij _ le_rfl⟩⟩
      rw [neg_lt, neg_sub]
      exact this _ le_rfl _ ij

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 ≥ ⌈ε⁻¹⌉₊, ∀ k ≥ ⌈ε⁻¹⌉₊, ↑(f j) / ↑j - ↑(f k) / ↑k < ε
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
h_ne_zero :
  Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors) ≠
    0
hv : Irreducible (Associates.mk v.asIdeal)
h_dvd :
  (Associates.mk v.asIdeal).count (Associates.mk I).factors ≤
    (Associates.mk v.asIdeal).count
      (Associates.mk
          (∏ᶠ (v : HeightOneSpectrum R), v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors)).factors
h_not_dvd :
  (Associates.mk v.asIdeal).count
      (Associates.mk
          (∏ᶠ (v : HeightOneSpectrum R),
            v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors)).factors <
    (Associates.mk v.asIdeal).count (Associates.mk I).factors + 1
⊢ (Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors =
    (Associates.mk v.asIdeal).count (Associates.mk I).factors

Tactic:
apply Nat.eq_of_le_of_lt_succ h_dvd h_not_dvd

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

Goal state before:
pp: case inr
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
z y : ℝ≥0
hy : ↑y ∈ s
hz : z ∈ Icc x.toNNReal y
⊢ z ∈ toNNReal '' s

Tactic:
exact ⟨z, h.out hx hy ⟨toNNReal_le_iff_le_coe.1 hz.1, hz.2⟩, toNNReal_coe⟩

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

Goal state before:
pp: x : ℝ≥0∞
⊢ x ∈ ⋃ n, Iio ↑n ↔ x ∈ {∞}ᶜ

Tactic:
mem_iUnion

Goal state after:
x : ℝ≥0∞
⊢ (∃ i, x ∈ Iio ↑i) ↔ x ∈ {∞}ᶜ
Module: Mathlib.Data.ENNReal.Basic

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

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

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

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

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

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

Goal state before:
pp: case neg
ι : Sort u_1
f : ι → ℝ≥0
h : ¬BddAbove (range f)
⊢ (⨆ i, ↑(f i)).toNNReal = 0

Tactic:
iSup_coe_eq_top.2 h,

Goal state after:
case neg
ι : Sort u_1
f : ι → ℝ≥0
h : ¬BddAbove (range f)
⊢ ∞.toNNReal = 0
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : EReal
⊢ x * 1 = x

Tactic:
by rw [EReal.mul_comm, EReal.one_mul]

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

Goal state before:
pp: x : EReal
h : x ≠ ⊤
⊢ x ≤ ↑x.toReal

Tactic:
by_cases h' : x = ⊥
  · simp only [h', bot_le]
  · simp only [le_refl, coe_toReal h h']

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

Goal state before:
pp: x : EReal
hx : x ≤ 0
⊢ ENNReal.ofReal x.toReal = 0

pp: x : EReal
hx : x ≤ 0
h : x = ⊤
⊢ False

Tactic:
· exact ENNReal.ofReal_of_nonpos (toReal_nonpos hx)

Goal state after:
x : EReal
hx : x ≤ 0
h : x = ⊤
⊢ False
Module: Mathlib.Data.EReal.Basic

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

Tactic:
by_cases h_top : x = ⊤
  · rw [h_top, coe_ennreal_top, toENNReal_top]
  rwa [toENNReal, if_neg _, toReal_coe_ennreal, ENNReal.ofReal_toReal_eq_iff]
  simp [h_top]

Goal state after:
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 + n)) = 0

Tactic:
neg_add_cancel,

Goal state after:
case neg
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
n : ℤ
I : FractionalIdeal R⁰ K
hI : ¬I = 0
⊢ count K v (I ^ 0) = 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 ^ 0) = 0

Tactic:
zpow_zero

Goal state after:
case neg
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
n : ℤ
I : FractionalIdeal R⁰ K
hI : ¬I = 0
⊢ count K v 1 = 0
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case hp₁
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 → ℤ
I I' : FractionalIdeal R⁰ K
hI : count K v I = 0
hI' : count K v I' = 0
⊢ count K v (I * I') = 0

Tactic:
classical
    by_cases h : I ≠ 0 ∧ I' ≠ 0
    · rw [count_mul' K v, if_pos h, hI, hI', add_zero]
    · rw [count_mul' K v, if_neg h]

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

Goal state before:
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
v : HeightOneSpectrum R
hv : ↑v.asIdeal ^ 0 ≠ 1
h : v ∈ {x | (fun v ↦ exps v = 0) x}
⊢ False

Tactic:
zpow_zero

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
v : HeightOneSpectrum R
hv : 1 ≠ 1
h : v ∈ {x | (fun v ↦ exps v = 0) x}
⊢ False
Module: Mathlib.Topology.MetricSpace.Defs

Goal state before:
pp: γ : Type w
inst✝ : MetricSpace γ
x y : γ
⊢ 0 = dist x y ↔ x = y

Tactic:
by rw [eq_comm, dist_eq_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PseudoMetricSpace α
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
i : PseudoMetricSpace ((b : β) → X b) :=
  PseudoEMetricSpace.toPseudoMetricSpaceOfDist (fun f g ↦ ↑(Finset.univ.sup fun b ↦ nndist (f b) (g b))) ⋯ ⋯
s : Set ((b : β) → X b)
C : ℝ≥0
H : ∀ ⦃x : (b : β) → X b⦄, x ∈ s → ∀ ⦃y : (b : β) → X b⦄, y ∈ s → dist x y ≤ ↑C
b : β
x : (x : β) → X x
hx : x ∈ s
y : (x : β) → X x
hy : y ∈ s
⊢ nndist (Function.eval b x) (Function.eval b y) ≤ C

Tactic:
exact Finset.sup_le_iff.1 (NNReal.coe_le_coe.1 <| H hx hy) b (Finset.mem_univ b)

Goal state after:
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
x✝ : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ ↑f
⊢ ∃ x ∈ Icc a b, ↑f ≤ 𝓝 x

Tactic:
by_contra! hf

Goal state after:
α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
x✝ : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ ↑f
hf : ∀ x ∈ Icc a b, ¬↑f ≤ 𝓝 x
⊢ False
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 β
f g : (b : β) → X b
r : ℝ
⊢ dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r

Tactic:
by
  by_cases hr : 0 ≤ r
  · exact dist_pi_le_iff hr
  · exact iff_of_false (fun h => hr <| dist_nonneg.trans h) fun h =>
      hr <| dist_nonneg.trans <| h <| Classical.arbitrary _

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : PseudoEMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ ∀ (x : X), d x x = 0

Tactic:
simp [hd]

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ ∀ (x : X), d x x = 0

Tactic:
simp [hd]

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : EMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ ∀ (x : X), d x x = 0

Tactic:
simp [hd]

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : EMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ ∀ {x y : X}, d x y = 0 → x = y

Tactic:
simp [hd]

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ ∀ (x : X), d x x = 0

Tactic:
simp [hd]

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ ∀ {x y : X}, d x y = 0 → x = y

Tactic:
simp [hd]

Goal state after:
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
ι : Sort u_3
inst✝ : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iInf g)
Af : Antitone f
bdd : BddBelow (range g)
⊢ f (sInf (range fun i ↦ g i)) = ⨆ i, f (g i)

Tactic:
Antitone.map_csInf_of_continuousAt Cf Af (range_nonempty g) bdd,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
ι : Sort u_3
inst✝ : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iInf g)
Af : Antitone f
bdd : BddBelow (range g)
⊢ sSup (f '' range g) = ⨆ i, f (g i)