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

Goal state before:
pp: case succ.refine_1
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k : (c' : S ⧸ P ^ i.succ) → c' ∈ map (mkQ (P ^ i.succ)) (P ^ i) → S
hk_mem : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), k c' hc' ∈ P ^ i
hk_eq : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), (mkQ (P ^ i.succ)) (k c' hc') = c'
c₁' : S ⧸ P ^ i.succ
hc₁' : c₁' ∈ map (mkQ (P ^ i.succ)) (P ^ i)
c₂' : S ⧸ P ^ i.succ
hc₂' : c₂' ∈ map (mkQ (P ^ i.succ)) (P ^ i)
h : (fun c' ↦ Quotient.mk'' (f (k ↑c' ⋯) ⋯)) ⟨c₁', hc₁'⟩ = (fun c' ↦ Quotient.mk'' (f (k ↑c' ⋯) ⋯)) ⟨c₂', hc₂'⟩
⊢ ⟨c₁', hc₁'⟩ = ⟨c₂', hc₂'⟩

Tactic:
rw [Subtype.mk_eq_mk, ← hk_eq _ hc₁', ← hk_eq _ hc₂', mkQ_apply, mkQ_apply,
      Submodule.Quotient.eq, ← hf _ (hk_mem _ hc₁'), ← hf _ (hk_mem _ hc₂')]

Goal state after:
case succ.refine_1
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k : (c' : S ⧸ P ^ i.succ) → c' ∈ map (mkQ (P ^ i.succ)) (P ^ i) → S
hk_mem : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), k c' hc' ∈ P ^ i
hk_eq : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), (mkQ (P ^ i.succ)) (k c' hc') = c'
c₁' : S ⧸ P ^ i.succ
hc₁' : c₁' ∈ map (mkQ (P ^ i.succ)) (P ^ i)
c₂' : S ⧸ P ^ i.succ
hc₂' : c₂' ∈ map (mkQ (P ^ i.succ)) (P ^ i)
h : (fun c' ↦ Quotient.mk'' (f (k ↑c' ⋯) ⋯)) ⟨c₁', hc₁'⟩ = (fun c' ↦ Quotient.mk'' (f (k ↑c' ⋯) ⋯)) ⟨c₂', hc₂'⟩
⊢ a * f (k c₁' hc₁') ⋯ + g (k c₁' hc₁') ⋯ - (a * f (k c₂' hc₂') ⋯ + g (k c₂' hc₂') ⋯) ∈ P ^ i.succ
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
S : Submonoid M
x y : M
z : ↥S
h₁ : y * ↑z = 1
h₂ : x * y = 1
⊢ x = ↑z

Tactic:
rw [← mul_one x, ← h₁, ← mul_assoc, h₂, one_mul]

Goal state after:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace X
S : Set X
hS : IsLocallyClosed S
hS' : IsPreirreducible S
hf₁ : Continuous[inst✝², inst✝¹] f
hf₂ : IsClosedMap f
hfS : (f '' S).Finite
⊢ (f '' closure[inst✝²] S).Subsingleton

Tactic:
obtain rfl | hS'' := S.eq_empty_or_nonempty
  · simp
  replace hS' : IsIrreducible S := ⟨hS'', hS'⟩
  have H₁ : IsIrreducible (S ∩ closedPoints X) := by
    rwa [← isIrreducible_iff_closure, ← JacobsonSpace.closure_inter_closedPoints_eq_closure hS,
      isIrreducible_iff_closure] at hS'
  have H₂ : f '' (S ∩ closedPoints X) ⊆ closedPoints Y := by
    rintro _ ⟨x, hx, rfl⟩; simpa using hf₂ _ hx.2
  have H₃ := ((hfS.subset (Set.image_mono Set.inter_subset_left)).isDiscrete_of_subset_closedPoints
    H₂).subsingleton_of_isPreirreducible (H₁.image _ hf₁.continuousOn).isPreirreducible
  have H₄ : IsClosed (f '' (S ∩ closedPoints X)) := by
    obtain (h | ⟨x, hx⟩) := Set.eq_empty_or_nonempty (f '' (S ∩ closedPoints X))
    · simp [h]
    · rw [H₃.eq_singleton_of_mem hx]; exact H₂ hx
  have := image_closure_subset_closure_image (s := S ∩ closedPoints X) hf₁
  rw [JacobsonSpace.closure_inter_closedPoints_eq_closure hS, H₄.closure_eq] at this
  exact H₃.anti this

Goal state after:
Module: Mathlib.RingTheory.HopkinsLevitzki

Goal state before:
pp: M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : Finite ↑s
span : ⨆ i, R ∙ ↑i = ⊤
i : M
e : (I : Ideal R) → R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := fun I ↦ { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ IsArtinianRing (R ⧸ (LinearMap.toSpanSingleton R M i).ker)

Tactic:
rw [IsArtinianRing, ← (e _).isArtinian_iff_of_bijective Function.bijective_id,
      (LinearMap.quotKerEquivRange _).isArtinian_iff]

Goal state after:
M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : Finite ↑s
span : ⨆ i, R ∙ ↑i = ⊤
i : M
e : (I : Ideal R) → R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := fun I ↦ { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ IsArtinian R ↥(LinearMap.toSpanSingleton R M i).range
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 Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
h₂ : Ideal.under R P = Ideal.under R Q
inst✝ : QuasiFiniteAt R Q
this : (Ideal.map (algebraMap S (Localization.AtPrime Q)) P).IsPrime
H : Ideal.map (algebraMap S (Localization.AtPrime Q)) P = IsLocalRing.maximalIdeal (Localization.AtPrime Q)
⊢ P = Q

Tactic:
rw [← Localization.AtPrime.under_maximalIdeal (I := Q), ← H,
    Q.under_map_of_isLocalizationAtPrime h₁]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
P : Ideal R
inst✝⁴ : P.IsPrime
Q : Ideal A
inst✝³ : Q.IsPrime
inst✝² : Q.LiesOver P
inst✝¹ : IsUnramifiedAt R Q
Q' : Ideal (P.Fiber A)
inst✝ : Q'.IsPrime
hQ' : Q = Ideal.comap TensorProduct.includeRight.toRingHom Q'
f₀ : Localization.AtPrime Q →ₐ[R] Localization.AtPrime Q' :=
  Localization.localAlgHom Q Q' TensorProduct.includeRight hQ'
hf₀ : Function.Surjective ⇑f₀
f : P.Fiber (Localization.AtPrime Q) →ₐ[P.ResidueField] Localization.AtPrime Q' :=
  TensorProduct.lift (ofId P.ResidueField (Localization.AtPrime Q')) f₀ ⋯
hf : Function.Surjective ⇑f
⊢ IsUnramifiedAt P.ResidueField Q'

Tactic:
exact .of_surjective _ hf

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
⊢ Module.support A Ω[A⁄R] ⊆ (PrimeSpectrum.zeroLocus {f})ᶜᶜ ↔ FormallyUnramified R (Localization.Away f)

Tactic:
compl_compl,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
⊢ Module.support A Ω[A⁄R] ⊆ PrimeSpectrum.zeroLocus {f} ↔ FormallyUnramified R (Localization.Away f)
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: case e_a
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
g : S →ₐ[R] P
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S
this : Algebra S P := g.toAlgebra
p : P
s : S
m : ↥(RingHom.ker (algebraMap P S))
⊢ g ((algebraMap P S) p) * ↑m - p * ↑m ∈ RingHom.ker (algebraMap P S) * RingHom.ker (algebraMap P S)

Tactic:
← sub_mul

Goal state after:
case e_a
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
g : S →ₐ[R] P
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S
this : Algebra S P := g.toAlgebra
p : P
s : S
m : ↥(RingHom.ker (algebraMap P S))
⊢ (g ((algebraMap P S) p) - p) * ↑m ∈ RingHom.ker (algebraMap P S) * RingHom.ker (algebraMap P S)
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: case e_f
K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
this✝ : Module.Finite K A
this : IsArtinianRing A
hA : IsNilpotent (IsLocalRing.maximalIdeal A)
e : K ≃ₐ[K] A ⧸ IsLocalRing.maximalIdeal A :=
  let __spread.0 := ofId K (A ⧸ IsLocalRing.maximalIdeal A);
  let __spread.1 := Equiv.ofBijective ⇑(algebraMap K (A ⧸ IsLocalRing.maximalIdeal A)) ⋯;
  { toFun := (↑↑__spread.0.toRingHom).toFun, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
e' : A ⊗[K] (A ⧸ IsLocalRing.maximalIdeal A) ≃ₐ[A] A :=
  (TensorProduct.congr AlgEquiv.refl e.symm).trans (TensorProduct.rid K A A)
f : A ⧸ IsLocalRing.maximalIdeal A →ₗ[A] A := e'.toLinearMap ∘ₗ sec K A (A ⧸ IsLocalRing.maximalIdeal A)
⊢ (ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ e'.toLinearMap =
    TensorProduct.AlgebraTensorModule.lift (↑K (lsmul A A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap.flip).flip

Tactic:
apply LinearMap.restrictScalars_injective K

Goal state after:
case e_f
K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
this✝ : Module.Finite K A
this : IsArtinianRing A
hA : IsNilpotent (IsLocalRing.maximalIdeal A)
e : K ≃ₐ[K] A ⧸ IsLocalRing.maximalIdeal A := ⋯
e' : A ⊗[K] (A ⧸ IsLocalRing.maximalIdeal A) ≃ₐ[A] A := ⋯
f : A ⧸ IsLocalRing.maximalIdeal A →ₗ[A] A := ⋯
⊢ ↑K ((ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ e'.toLinearMap) =
    ↑K (TensorProduct.AlgebraTensorModule.lift (↑K (lsmul A A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap.flip).flip)
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
this✝ : Module.Finite K A
this : IsArtinianRing A
hA : IsNilpotent (IsLocalRing.maximalIdeal A)
e : K ≃ₐ[K] A ⧸ IsLocalRing.maximalIdeal A :=
  let __spread.0 := ofId K (A ⧸ IsLocalRing.maximalIdeal A);
  let __spread.1 := Equiv.ofBijective ⇑(algebraMap K (A ⧸ IsLocalRing.maximalIdeal A)) ⋯;
  { toFun := (↑↑__spread.0.toRingHom).toFun, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
e' : A ⊗[K] (A ⧸ IsLocalRing.maximalIdeal A) ≃ₐ[A] A :=
  (TensorProduct.congr AlgEquiv.refl e.symm).trans (TensorProduct.rid K A A)
f : A ⧸ IsLocalRing.maximalIdeal A →ₗ[A] A := e'.toLinearMap ∘ₗ sec K A (A ⧸ IsLocalRing.maximalIdeal A)
hf : (ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ f = LinearMap.id
hf₁ : f 1 • 1 = 1
hf₂ : 1 - f 1 ∈ IsLocalRing.maximalIdeal A
hf₃ : IsIdempotentElem (1 - f 1)
hf₄ : f 1 = 1
x : A
k : K
| f (k • e 1)

Tactic:
LinearMap.map_smul_of_tower,

Goal state after:
K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
this✝ : Module.Finite K A
this : IsArtinianRing A
hA : IsNilpotent (IsLocalRing.maximalIdeal A)
e : K ≃ₐ[K] A ⧸ IsLocalRing.maximalIdeal A :=
  let __spread.0 := ofId K (A ⧸ IsLocalRing.maximalIdeal A);
  let __spread.1 := Equiv.ofBijective ⇑(algebraMap K (A ⧸ IsLocalRing.maximalIdeal A)) ⋯;
  { toFun := (↑↑__spread.0.toRingHom).toFun, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
e' : A ⊗[K] (A ⧸ IsLocalRing.maximalIdeal A) ≃ₐ[A] A :=
  (TensorProduct.congr AlgEquiv.refl e.symm).trans (TensorProduct.rid K A A)
f : A ⧸ IsLocalRing.maximalIdeal A →ₗ[A] A := e'.toLinearMap ∘ₗ sec K A (A ⧸ IsLocalRing.maximalIdeal A)
hf : (ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ f = LinearMap.id
hf₁ : f 1 • 1 = 1
hf₂ : 1 - f 1 ∈ IsLocalRing.maximalIdeal A
hf₃ : IsIdempotentElem (1 - f 1)
hf₄ : f 1 = 1
x : A
k : K
| k • f (e 1)
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
inst✝ : q.LiesOver p
H : Function.Injective ⇑(localRingHom p q (algebraMap R S) ⋯)
s : Finset R
hs : Ideal.span ↑s = RingHom.ker (algebraMap R S)
this : ∀ (x : ↥s), (algebraMap R (Localization.AtPrime p)) ↑x = 0
m : ↥s → ↥p.primeCompl
hm : ∀ (x : ↥s), ↑(m x) * ↑x = 0
x : R
hxs : x ∈ ↑s
⊢ x ∈ ↑(RingHom.ker (algebraMap R (Away ↑(∏ i, m i))))

Tactic:
refine (IsLocalization.map_eq_zero_iff (.powers (∏ i, m i).1) _ _).mpr ⟨⟨_, 1, rfl⟩, ?_⟩

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
inst✝ : q.LiesOver p
H : Function.Injective ⇑(localRingHom p q (algebraMap R S) ⋯)
s : Finset R
hs : Ideal.span ↑s = RingHom.ker (algebraMap R S)
this : ∀ (x : ↥s), (algebraMap R (Localization.AtPrime p)) ↑x = 0
m : ↥s → ↥p.primeCompl
hm : ∀ (x : ↥s), ↑(m x) * ↑x = 0
x : R
hxs : x ∈ ↑s
⊢ ↑⟨(fun x ↦ ↑(∏ i, m i) ^ x) 1, ⋯⟩ * x = 0
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
w : ℕ
y : M
hy : y ∈ N₁
z : M
hz : z ∈ N₂
h : ∀ a ∈ I ^ w, a • (y + z) = 0
⊢ z ∈ N₂

Tactic:
simp [hz]

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

Goal state before:
pp: s : Set ℝ≥0
⊢ ↑(sSup s) = sSup (toReal '' s)

Tactic:
rcases Set.eq_empty_or_nonempty s with rfl | hs

Goal state after:
case inl
⊢ ↑(sSup ∅) = sSup (toReal '' ∅)

case inr
s : Set ℝ≥0
hs : s.Nonempty
⊢ ↑(sSup s) = sSup (toReal '' s)
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: ι : Sort u_1
⊢ ⨅ x, 0 = 0

Tactic:
cases isEmpty_or_nonempty ι
  · exact Real.iInf_of_isEmpty _
  · exact ciInf_const

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

Goal state before:
pp: s : Set ℝ≥0
⊢ ↑(sInf s) = sInf (toReal '' s)

Tactic:
rcases Set.eq_empty_or_nonempty s with rfl | hs

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

case inr
s : Set ℝ≥0
hs : s.Nonempty
⊢ ↑(sInf s) = sInf (toReal '' s)
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

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

Tactic:
by
  rcases s.eq_empty_or_nonempty with (rfl | hne)
  · rw [sInf_empty, sSup_empty]
  · exact csInf_le_csSup hne h₁ h₂

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

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

Tactic:
by
  by_cases r = 0 <;> simp [*, inv_le]

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

Goal state before:
pp: x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
⊢ a ≤ y

Tactic:
have hx : x ≠ 0 := ha.ne_zero
    have hx' : x⁻¹ ≠ 0 := by rwa [Ne, inv_eq_zero]
    have : a * x⁻¹ < 1 := by rwa [← lt_inv_iff_mul_lt hx', inv_inv]
    have : a * x⁻¹ * x ≤ y := h _ this
    rwa [mul_assoc, inv_mul_cancel₀ hx, mul_one] at this

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

Goal state before:
pp: ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℝ≥0
⊢ ⨅ i, f i = 0

Tactic:
_root_.iInf_of_isEmpty,

Goal state after:
ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℝ≥0
⊢ sInf ∅ = 0
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: a : ℝ
h : (ENNReal.ofReal a).toReal = a
⊢ 0 ≤ a

Tactic:
rw [← h]
    exact toReal_nonneg

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
n : R := choose ⋯
d : ↥R⁰ := choose ⋯
hk : I = spanSingleton R⁰ (0 / (algebraMap R K) ↑d)
hnd : mk' K n d = k
h : n = 0
⊢ False

Tactic:
zero_div,

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
k : K
n : R := choose ⋯
d : ↥R⁰ := choose ⋯
hk : I = spanSingleton R⁰ 0
hnd : mk' K n d = k
h : n = 0
⊢ False
Module: Mathlib.Topology.Order.T5

Goal state before:
pp: case refine_1
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd✝ : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
⊢ [[x, c]] ⊆ tᶜ.ordConnectedComponent a

Tactic:
exact OrdConnected.uIcc_subset inferInstance (hsub' ⟨hx.1, hx.2.le.trans hcb⟩)
        (hsub' ⟨hac.le, hcb⟩)

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

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≤] a

Tactic:
have hd' : Disjoint (ofDual ⁻¹' s) (closure <| ofDual ⁻¹' t) := hd
  have ha' : toDual a ∈ ofDual ⁻¹' s := ha
  simpa only [dual_ordSeparatingSet, dual_ordConnectedSection] using!
    compl_ordConnectedSection_ordSeparatingSet_mem_nhdsGE hd' ha'

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

Goal state before:
pp: a : ℝ≥0∞
h : 0 < a
⊢ a ∈ {b | 1 ≤ ∞ * b}

Tactic:
by
    simp [*, h.ne', top_mul]

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

Goal state before:
pp: x : EReal
⊢ 0 < x.toENNReal ↔ 0 < x

Tactic:
pos_iff_ne_zero,

Goal state after:
x : EReal
⊢ x.toENNReal ≠ 0 ↔ 0 < x
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: m n : ℕ
⊢ ↑(m * n) = ↑m * ↑n

Tactic:
rw [← coe_coe_eq_natCast, ← coe_coe_eq_natCast, ← coe_coe_eq_natCast, Nat.cast_mul, EReal.coe_mul]

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

Goal state before:
pp: a : ℝ≥0∞
⊢ ∞ / a = if a = ∞ then 0 else ∞

Tactic:
by simp [div_eq_mul_inv, top_mul']

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

Goal state before:
pp: α : Type u_3
m m' : PseudoMetricSpace α
h : m.toDist = m'.toDist
d : Dist α := m.toDist
⊢ m = m'

Tactic:
obtain ⟨_, _, _, _, hed, _, hU, _, hB⟩ := m

Goal state after:
α : Type u_3
m' : PseudoMetricSpace α
toDist✝ : Dist α
dist_self✝ : ∀ (x : α), dist x x = 0
dist_comm✝ : ∀ (x y : α), dist x y = dist y x
dist_triangle✝ : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
edist✝ : α → α → ℝ≥0∞
hed : ∀ (x y : α), edist✝ x y = ENNReal.ofReal (dist x y)
toUniformSpace✝ : UniformSpace α
hU : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | dist p.1 p.2 < ε}
toBornology✝ : Bornology α
hB : (cobounded α).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
h :
  { toDist := toDist✝, dist_self := dist_self✝, dist_comm := dist_comm✝, dist_triangle := dist_triangle✝,
        edist := edist✝, edist_dist := hed, toUniformSpace := toUniformSpace✝, uniformity_dist := hU,
        toBornology := toBornology✝, cobounded_sets := hB }.toDist =
    m'.toDist
d : Dist α :=
  { toDist := toDist✝, dist_self := dist_self✝, dist_comm := dist_comm✝, dist_triangle := dist_triangle✝,
      edist := edist✝, edist_dist := hed, toUniformSpace := toUniformSpace✝, uniformity_dist := hU,
      toBornology := toBornology✝, cobounded_sets := hB }.toDist
⊢ { toDist := toDist✝, dist_self := dist_self✝, dist_comm := dist_comm✝, dist_triangle := dist_triangle✝,
      edist := edist✝, edist_dist := hed, toUniformSpace := toUniformSpace✝, uniformity_dist := hU,
      toBornology := toBornology✝, cobounded_sets := hB } =
    m'
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝¹ : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
l : Filter β
inst✝ : l.NeBot
hf₀ : ∀ (i : β), p i → 0 < f i
hf₁ : ∀ᶠ (i : β) in l, p i
hf : ∀ (i : ℝ), 0 < i → ∀ᶠ (x : β) in l, f x ∈ closedBall 0 i
ε : ℝ
hε : 0 < ε
i : β
hp : p i
hi : f i ∈ closedBall 0 ε
⊢ f i ≤ ε

Tactic:
by
    simpa [Metric.mem_closedBall, Real.dist_eq, abs_of_nonneg (hf₀ i hp).le] using hi

Goal state after:
Module: Mathlib.Topology.Bornology.Constructions

Goal state before:
pp: α : Type u_1
inst✝ : Bornology α
s : Set α
⊢ IsBounded (s ×ˢ s) ↔ IsBounded s

Tactic:
by
  rcases s.eq_empty_or_nonempty with (rfl | hs); · simp
  exact (isBounded_prod_of_nonempty (hs.prod hs)).trans and_self_iff

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

Goal state before:
pp: case inl
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
s : Set α
a' : α
ha' : a' ∈ s
ha : IsLUB s a'
h : ∀ᶠ (x : α) in 𝓝[≤] a', ¬(fun x ↦ x ∈ s) x
⊢ False

Tactic:
exact h.self_of_nhdsWithin le_rfl 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 b : α
h : a < b
⊢ Icc a b \ interior (Ioo a b) = {a, b}

Tactic:
interior_Ioo,

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : a < b
⊢ Icc a b \ Ioo a b = {a, b}
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
hr : 0 < ↑r
⊢ nndist f g = r ↔ (∃ i, nndist (f i) (g i) = r) ∧ ∀ (b : β), ↑(nndist (f b) (g b)) ≤ ↑r

Tactic:
nndist_pi_eq_iff hr,

Goal state after:
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
hr : 0 < ↑r
⊢ ((∃ i, nndist (f i) (g i) = r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r) ↔
    (∃ i, nndist (f i) (g i) = r) ∧ ∀ (b : β), ↑(nndist (f b) (g b)) ≤ ↑r
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: case inr
α : Type u_1
γ : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
l : Filter γ
inst✝ : CountableInterFilter l
f : γ → α
a : α
h : ∀ (b : α), a < b → ∀ᶠ (x : γ) in l, f x < b
d : α
hd : IsGLB (Ioi a) d
H0 : Ioi a = Ici d
⊢ ∀ᶠ (x : γ) in l, f x ≤ a

Tactic:
specialize h d <| by simp [← Set.mem_Ioi, H0]
      filter_upwards [h] with x hx
      rw [← Set.compl_Iic, ← Set.compl_Iio, compl_inj_iff] at H0
      simpa [← Set.mem_Iic, ← Set.mem_Iio, H0] using hx

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

Goal state before:
pp: X : Type u_2
x y z : X
inst✝ : PseudoEMetricSpace X
⊢ ediam {x, y, z} = max (max (edist x y) (edist x z)) (edist y z)

Tactic:
simp only [ediam_insert, iSup_insert, iSup_singleton, ediam_singleton, max_zero]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a : E
r : ℝ
⊢ {x | x / a ∈ sphere 1 r} = sphere a r

Tactic:
ext x
  rw [mem_sphere_iff_norm']
  simp

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty
h' : Tendsto (fun n ↦ diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N ↦ ⋯.some
n : ℕ
⊢ ∀ (N : ℕ), n ≤ N → u N ∈ s n

Tactic:
N

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty
h' : Tendsto (fun n ↦ diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N ↦ ⋯.some
n N : ℕ
⊢ n ≤ N → u N ∈ s n