mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
⊢ f (a * b) = f a * f b

Tactic:
let := Classical.decEq α
  by_cases ha0 : a = 0
  · rw [ha0, zero_mul, h0, zero_mul]
  by_cases hb0 : b = 0
  · rw [hb0, mul_zero, h0, mul_zero]
  by_cases hf1 : f 1 = 0
  · calc
      f (a * b) = f (a * b * 1) := by rw [mul_one]
      _ = 0 := by simp only [h1 isUnit_one, hf1, mul_zero]
      _ = f a * f (b * 1) := by simp only [h1 isUnit_one, hf1, mul_zero]
      _ = f a * f b := by rw [mul_one]
  have : Nontrivial α := ⟨⟨_, _, ha0⟩⟩
  let : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
  suffices
      f (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ ((normalizedFactors a).count p + (normalizedFactors b).count p)) =
      f (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (normalizedFactors a).count p) *
      f (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (normalizedFactors b).count p) by
    obtain ⟨ua, a_eq⟩ := prod_normalizedFactors ha0
    obtain ⟨ub, b_eq⟩ := prod_normalizedFactors hb0
    rw [← a_eq, ← b_eq, mul_right_comm (Multiset.prod (normalizedFactors a)) ua
        (Multiset.prod (normalizedFactors b) * ub), h1 ua.isUnit, h1 ub.isUnit, h1 ua.isUnit, ←
      mul_assoc, h1 ub.isUnit, mul_right_comm _ (f ua), ← mul_assoc]
    congr
    rw [← (normalizedFactors a).map_id, ← (normalizedFactors b).map_id,
      Finset.prod_multiset_map_count, Finset.prod_multiset_map_count,
      Finset.prod_subset (Finset.subset_union_left (s₂ := (normalizedFactors b).toFinset)),
      Finset.prod_subset (Finset.subset_union_right (s₂ := (normalizedFactors b).toFinset)), ←
      Finset.prod_mul_distrib]
    · simp_rw [id, ← pow_add, this]
    all_goals simp only [Multiset.mem_toFinset]
    · intro p _ hpb
      simp [hpb]
    · intro p _ hpa
      simp [hpa]
  refine multiplicative_prime_power _ _ _ ?_ ?_ @h1 @hpr @hcp
  all_goals simp only [Multiset.mem_toFinset, Finset.mem_union]
  · rintro p (hpa | hpb) <;> apply prime_of_normalized_factor <;> assumption
  · rintro p (hp | hp) q (hq | hq) hdvd <;>
      rw [← normalize_normalized_factor _ hp, ← normalize_normalized_factor _ hq] <;>
      exact
        normalize_eq_normalize hdvd
          ((prime_of_normalized_factor _ hp).irreducible.dvd_symm
            (prime_of_normalized_factor _ hq).irreducible hdvd)

Goal state after:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
h : (closedPoints X).Finite
⊢ closedPoints X = Set.univ

Tactic:
← Set.univ_subset_iff,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
h : (closedPoints X).Finite
⊢ Set.univ ⊆ closedPoints X
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
f : A →ₐ[R] B
H : Function.Surjective ⇑f
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] Q
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
x : A
⊢ (f₁.comp f) x = f₂ (f x)

Tactic:
← AlgHom.comp_apply

Goal state after:
R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : FormallyUnramified R A
f : A →ₐ[R] B
H : Function.Surjective ⇑f
Q : Type u_3
inst✝¹ : CommRing Q
inst✝ : Algebra R Q
I : Ideal Q
hI : I ^ 2 = ⊥
f₁ f₂ : B →ₐ[R] Q
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
x : A
⊢ (f₁.comp f) x = (f₂.comp f) x
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
inst✝ : FiniteType R S
⊢ QuasiFinite R S ↔ ∀ (x : PrimeSpectrum R), (PrimeSpectrum.comap (algebraMap R S) ⁻¹' {x}).Finite

Tactic:
by
  refine ⟨fun H _ ↦ finite_comap_preimage_singleton _, fun H ↦ ⟨fun P _ ↦ ?_⟩⟩
  rw [Module.finite_iff_isArtinianRing, isArtinianRing_iff_isNoetherianRing_krullDimLE_zero]
  have : IsJacobsonRing (P.Fiber S) := isJacobsonRing_of_finiteType (A := P.ResidueField)
  have : Finite (PrimeSpectrum (P.Fiber S)) :=
    (PrimeSpectrum.preimageEquivFiber R S ⟨P, ‹_›⟩).finite_iff.mp (H ⟨P, ‹_›⟩)
  exact ⟨Algebra.FiniteType.isNoetherianRing P.ResidueField _,
    (PrimeSpectrum.discreteTopology_iff_finite_and_krullDimLE_zero.mp inferInstance).right⟩

Goal state after:
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
inst✝ : FormallySmooth R A
I : Ideal B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B ⧸ I
P : Generators R A A := Generators.self R A
hP : Function.Injective ⇑P.toExtension.cotangentComplex
l : P.toExtension.CotangentSpace →ₗ[A] P.toExtension.Cotangent
hl : l ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
g : A →ₐ[R] P.Ring ⧸ RingHom.ker (IsScalarTower.toAlgHom R P.Ring A).toRingHom ^ 2
hg : (IsScalarTower.toAlgHom R P.Ring A).kerSquareLift.comp g = AlgHom.id R A
σ : B ⧸ I → B := Function.surjInv ⋯
x : P.Ring
⊢ (aeval (⇑(algebraMap B (B ⧸ I)) ∘ σ ∘ ⇑f)) x = (aeval fun i ↦ f (P.val i)) x

Tactic:
← Function.comp_assoc,

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
inst✝ : FormallySmooth R A
I : Ideal B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B ⧸ I
P : Generators R A A := Generators.self R A
hP : Function.Injective ⇑P.toExtension.cotangentComplex
l : P.toExtension.CotangentSpace →ₗ[A] P.toExtension.Cotangent
hl : l ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
g : A →ₐ[R] P.Ring ⧸ RingHom.ker (IsScalarTower.toAlgHom R P.Ring A).toRingHom ^ 2
hg : (IsScalarTower.toAlgHom R P.Ring A).kerSquareLift.comp g = AlgHom.id R A
σ : B ⧸ I → B := Function.surjInv ⋯
x : P.Ring
⊢ (aeval ((⇑(algebraMap B (B ⧸ I)) ∘ σ) ∘ ⇑f)) x = (aeval fun i ↦ f (P.val i)) x
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case add
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 ι
Q' : Generators S T ι'
f : Q.Hom Q'
this✝ : AddCommGroup (T ⊗[S] Ω[S⁄R]) := inferInstance
this : IsScalarTower Q.Ring Q.Ring T
x₁ x₂ : MvPolynomial ι S
hx₁ :
  (δAux R Q') (f.toAlgHom x₁) =
    (δAux R Q) x₁ +
      (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val)) (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₁))
hx₂ :
  (δAux R Q') (f.toAlgHom x₂) =
    (δAux R Q) x₂ +
      (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val)) (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₂))
⊢ (δAux R Q) x₁ +
        (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
          (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₁)) +
      ((δAux R Q) x₂ +
        (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
          (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₂))) =
    (δAux R Q) x₁ + (δAux R Q) x₂ +
      ((Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
          (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₁)) +
        (Finsupp.linearCombination T (⇑(δAux R Q') ∘ f.val))
          (Q.cotangentSpaceBasis.repr (1 ⊗ₜ[Q.Ring] (D S Q.Ring) x₂)))

Tactic:
rw [add_add_add_comm]

Goal state after:
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 σ
x : ↥Q.ker
hx : Extension.Cotangent.mk x ∈ Q.toExtension.cotangentComplex.ker
y : (Q.comp P).toExtension.Cotangent := Extension.Cotangent.mk (Q.kerCompPreimage P x)
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x
z : T ⊗[S] P.toExtension.CotangentSpace :=
  ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2
⊢ (δ Q P) ⟨Extension.Cotangent.mk x, hx⟩ = (δAux R Q) ↑x

Tactic:
rw [H1Cotangent.δ_eq (y := y) (z := z)]

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 σ
x : ↥Q.ker
hx : Extension.Cotangent.mk x ∈ Q.toExtension.cotangentComplex.ker
y : (Q.comp P).toExtension.Cotangent := Extension.Cotangent.mk (Q.kerCompPreimage P x)
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x
z : T ⊗[S] P.toExtension.CotangentSpace :=
  ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2
⊢ (LinearMap.baseChange T P.toExtension.toKaehler) z = (δAux R Q) ↑x

case hy
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 := Extension.Cotangent.mk (Q.kerCompPreimage P x)
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x
z : T ⊗[S] P.toExtension.CotangentSpace :=
  ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2
⊢ (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = ↑⟨Extension.Cotangent.mk x, hx⟩

case hz
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 := Extension.Cotangent.mk (Q.kerCompPreimage P x)
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x
z : T ⊗[S] P.toExtension.CotangentSpace :=
  ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2
⊢ (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)) z =
    (Q.comp P).toExtension.cotangentComplex y
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
⊢ Submodule.span T (Set.range (⇑(map R R S T) ∘ ⇑(D R S))) = ⊤

Tactic:
convert!
    span_eq_top_of_isLocalizedModule T M (map R R S T) (v := Set.range <| D R S)
      (span_range_derivation R S)
  rw [← Set.range_comp, Function.comp_def]

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✝ : Algebra.IsSeparable (ResidueField R) (ResidueField S)
H : Ideal.map (algebraMap R S) (maximalIdeal R) = maximalIdeal S
this✝ : FormallyUnramified (ResidueField R) (ResidueField S)
this : FormallyUnramified R (ResidueField S)
⊢ Subsingleton Ω[S⁄R]

Tactic:
rw [← subsingleton_tensorProduct (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✝ : Algebra.IsSeparable (ResidueField R) (ResidueField S)
H : Ideal.map (algebraMap R S) (maximalIdeal R) = maximalIdeal S
this✝ : FormallyUnramified (ResidueField R) (ResidueField S)
this : FormallyUnramified R (ResidueField S)
⊢ Subsingleton (TensorProduct S (ResidueField S) Ω[S⁄R])
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
t : Finset ι
hts : t ⊆ s
ht : t.Nonempty
⊢ (-1) ^ #t • (⋂ i ∈ t, S i).indicator f a = 0

Tactic:
Set.indicator_of_notMem

Goal state after:
case neg
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
t : Finset ι
hts : t ⊆ s
ht : t.Nonempty
⊢ (-1) ^ #t • 0 = 0

case neg.h
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
t : Finset ι
hts : t ⊆ s
ht : t.Nonempty
⊢ a ∉ ⋂ i ∈ t, S i
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0

Tactic:
by
  have h_supp : {v : HeightOneSpectrum R | ¬((Associates.mk v.asIdeal).count
      (Associates.mk I).factors : ℤ) = 0} = {v : HeightOneSpectrum R | v.asIdeal ∣ I} := by
    ext v
    simp_rw [Int.natCast_eq_zero]
    exact Associates.count_ne_zero_iff_dvd hI v.irreducible
  rw [Filter.eventually_cofinite, h_supp]
  exact Ideal.finite_factors hI

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

Goal state after:
case inl
hs : ∀ x ∈ ∅, 0 ≤ x
⊢ 0 ≤ sSup ∅

case inr
s : Set ℝ
hs : ∀ x ∈ s, 0 ≤ x
x : ℝ
hx : x ∈ s
⊢ 0 ≤ sSup s
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

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

Tactic:
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty

Goal state after:
case inl
hs : ∀ x ∈ ∅, x ≤ 0
⊢ sInf ∅ ≤ 0

case inr
s : Set ℝ
hs : ∀ x ∈ s, x ≤ 0
x : ℝ
hx : x ∈ s
⊢ sInf s ≤ 0
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
⊢ p 1 + q 1 = 0

Tactic:
map_one_eq_zero p,

Goal state after:
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
⊢ 0 + q 1 = 0
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
⊢ q 1 ≤ p 1

Tactic:
map_one_eq_zero p,

Goal state after:
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
⊢ q 1 ≤ 0
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
r : ℝ
hr : 0 < r
⊢ p 1 + q 1 < r

Tactic:
map_one_eq_zero p,

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
r : ℝ
hr : 0 < r
⊢ 0 + q 1 < r
Module: Mathlib.Data.ENNReal.Real

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

Tactic:
rw [mul_comm]
  exact toReal_mul_top _

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
k : K
hk : I = spanSingleton R⁰ k
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑(choose ⋯)})).factors)) =
    I

Tactic:
by
  set n : R := choose (exists_mk'_eq R⁰ k)
  set d : ↥R⁰ := choose (choose_spec (exists_mk'_eq R⁰ k))
  have hnd : mk' K n d = k := choose_spec (choose_spec (exists_mk'_eq R⁰ k))
  have hn0 : n ≠ 0 := by
    by_contra h
    rw [← hnd, h, IsFractionRing.mk'_eq_div, map_zero, zero_div, spanSingleton_zero] at hk
    exact hI hk
  rw [finprod_heightOneSpectrum_factorization_principal_fraction hn0 d, hk, hnd]

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

Goal state before:
pp: case coe
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ 0 ≤ (↑a✝).toReal

Tactic:
exact toReal_coe _ ▸ EReal.coe_nonneg.mp hx

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

Goal state before:
pp: case mp
x : EReal
⊢ x = ⊤ → ∀ (y : ℝ), ↑y < x

Tactic:
rintro rfl
    exact EReal.coe_lt_top

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

Goal state before:
pp: a b : ℝ≥0∞
⊢ a ≤ b⁻¹ ↔ a * b ≤ 1

Tactic:
rw [← one_div, ENNReal.le_div_iff_mul_le] <;>
    · right
      simp

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
inst✝ : PseudoEMetricSpace α
x✝ y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
x : α
⊢ edist x x < ∞

Tactic:
by rw [edist_self]; exact ENNReal.coe_lt_top

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
⊢ closedBall x ε \ sphere x ε = ball x ε

Tactic:
rw [← ball_union_sphere, Set.union_sdiff_cancel_right sphere_disjoint_ball.symm.le_bot]

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

Goal state before:
pp: case refine_2
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
p : HeightOneSpectrum R
hps : p ∈ s
⊢ 0 < J * ∏ x ∈ s \ {p}, x.asIdeal

Tactic:
rw [Ideal.zero_eq_bot, bot_lt_iff_ne_bot, ← Ideal.zero_eq_bot,
        mul_ne_zero_iff, Finset.prod_ne_zero_iff]
      exact ⟨hJ, fun x _ ↦ x.3⟩

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

Goal state before:
pp: x y : ℝ
⊢ Ioo x y = Ioo x ((y + (x + (y - x))) / 2)

Tactic:
add_sub_cancel,

Goal state after:
x y : ℝ
⊢ Ioo x y = Ioo x ((y + y) / 2)
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: x y : ℝ
⊢ Icc x y = Icc x ((y + (x + (y - x))) / 2)

Tactic:
add_sub_cancel,

Goal state after:
x y : ℝ
⊢ Icc x y = Icc x ((y + y) / 2)
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

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

Tactic:
by
  simpa only [dist_comm x] using dist_dist_dist_le_left y z x

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

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : SigmaCompactSpace α
⊢ SecondCountableTopology α

Tactic:
by
  suffices SeparableSpace α by exact UniformSpace.secondCountable_of_separable α
  choose T _ hTc hsubT using fun n =>
    subset_countable_closure_of_compact (isCompact_compactCovering α n)
  refine ⟨⟨⋃ n, T n, countable_iUnion hTc, fun x => ?_⟩⟩
  rcases iUnion_eq_univ_iff.1 (iUnion_compactCovering α) x with ⟨n, hn⟩
  exact closure_mono (subset_iUnion _ n) (hsubT _ hn)

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
ha : (Iio a).Nonempty
⊢ frontier (Ici a) = {a}

Tactic:
by
  simp [frontier, ha]

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
ha : (Ioi a).Nonempty
⊢ frontier (Iic a) = {a}

Tactic:
by
  simp [frontier, ha]

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
β : Type u_3
inst✝² : LinearOrder β
inst✝¹ : DenselyOrdered α
inst✝ : FirstCountableTopology α
f : β → α
x y : α
hf : DenseRange f
hmono : Monotone f
hlt : y < x
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Ioo y x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)

Tactic:
rcases Dense.exists_seq_strictMono_tendsto_of_lt hf hlt with ⟨u, hu, huyxf, hlim⟩

Goal state after:
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
β : Type u_3
inst✝² : LinearOrder β
inst✝¹ : DenselyOrdered α
inst✝ : FirstCountableTopology α
f : β → α
x y : α
hf : DenseRange f
hmono : Monotone f
hlt : y < x
u : ℕ → α
hu : StrictMono u
huyxf : ∀ (n : ℕ), u n ∈ Ioo y x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Ioo y x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)
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 (iSup g)
Af : Antitone f
bdd : BddAbove (range g)
⊢ f (⨆ i, g i) = ⨅ i, f (g i)

Tactic:
by
  rw [iSup, Antitone.map_csSup_of_continuousAt Cf Af (range_nonempty g) bdd, ← range_comp, iInf,
    comp_def]

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

Goal state before:
pp: case inl
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
hf : Continuous[instTopologicalSpaceProd, inst✝³] ↿f
hK : IsCompact ∅
⊢ Continuous[inst✝, inst✝³] fun x ↦ sSup (f x '' ∅)

Tactic:
image_empty

Goal state after:
case inl
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
hf : Continuous[instTopologicalSpaceProd, inst✝³] ↿f
hK : IsCompact ∅
⊢ Continuous[inst✝, inst✝³] fun x ↦ sSup ∅
Module: Mathlib.Topology.MetricSpace.ProperSpace

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
ι : Type u_2
inst✝² : PseudoMetricSpace α
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
h : ∀ (b : β), ProperSpace (X b)
x : (b : β) → X b
r : ℝ
hr : 0 ≤ r
⊢ IsCompact (closedBall x r)

Tactic:
rw [closedBall_pi _ hr]

Goal state after:
α : Type u
β : Type v
X✝ : Type u_1
ι : Type u_2
inst✝² : PseudoMetricSpace α
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
h : ∀ (b : β), ProperSpace (X b)
x : (b : β) → X b
r : ℝ
hr : 0 ≤ r
⊢ IsCompact (univ.pi fun b ↦ closedBall (x b) r)
Module: Mathlib.Topology.MetricSpace.Cauchy

Goal state before:
pp: case mp
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
⊢ UniformCauchySeqOn F atTop s → ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε

Tactic:
intro h ε hε

Goal state after:
case mp
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : UniformCauchySeqOn F atTop s
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε