mathlib-initiative/mathlib-tactics huggingface dataset:
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
P : Type u_2
C✝ : Type u_3
inst✝¹¹ : CommRing B✝
inst✝¹⁰ : Algebra R✝ B✝
inst✝⁹ : CommRing C✝
inst✝⁸ : Algebra R✝ C✝
inst✝⁷ : CommRing P
inst✝⁶ : Algebra R✝ P
R : Type u_4
inst✝⁵ : CommRing R
A : Type u_5
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type u_6
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
C : Type (max u_5 u_6)
x✝¹ : CommRing C
x✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this : Algebra R C := ((algebraMap B C).comp (algebraMap R B)).toAlgebra
⊢ ∃ a, (Ideal.Quotient.mkₐ B I).comp a = f

Tactic:
have : IsScalarTower R B C := IsScalarTower.of_algebraMap_eq' rfl

Goal state after:
R✝ : Type u
A✝ : Type v
inst✝¹⁴ : CommRing R✝
inst✝¹³ : CommRing A✝
inst✝¹² : Algebra R✝ A✝
B✝ : Type u_1
P : Type u_2
C✝ : Type u_3
inst✝¹¹ : CommRing B✝
inst✝¹⁰ : Algebra R✝ B✝
inst✝⁹ : CommRing C✝
inst✝⁸ : Algebra R✝ C✝
inst✝⁷ : CommRing P
inst✝⁶ : Algebra R✝ P
R : Type u_4
inst✝⁵ : CommRing R
A : Type u_5
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type u_6
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
C : Type (max u_5 u_6)
x✝¹ : CommRing C
x✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
this✝ : Algebra R C := ((algebraMap B C).comp (algebraMap R B)).toAlgebra
this : IsScalarTower R B C
⊢ ∃ a, (Ideal.Quotient.mkₐ B I).comp a = f
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: R : Type u_4
A : Type u_5
Rₘ : Type u_6
Sₘ : Type u_7
inst✝¹³ : CommRing R
inst✝¹² : CommRing A
inst✝¹¹ : CommRing Rₘ
inst✝¹⁰ : CommRing Sₘ
M : Submonoid R
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R Sₘ
inst✝⁷ : Algebra A Sₘ
inst✝⁶ : Algebra R Rₘ
inst✝⁵ : Algebra Rₘ Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R A Sₘ
inst✝² : IsLocalization M Rₘ
inst✝¹ : IsLocalization (Submonoid.map (algebraMap R A) M) Sₘ
inst✝ : FormallySmooth R A
this✝ : FormallySmooth A Sₘ
this : FormallySmooth R Sₘ
⊢ FormallySmooth Rₘ Sₘ

Tactic:
exact FormallySmooth.localization_base M

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
⊢ ↑(PrimeSpectrum.basicOpen f) ⊆ unramifiedLocus R A ↔ FormallyUnramified R (Localization.Away f)

Tactic:
unramifiedLocus_eq_compl_support,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
⊢ ↑(PrimeSpectrum.basicOpen f) ⊆ (Module.support A Ω[A⁄R])ᶜ ↔ FormallyUnramified R (Localization.Away f)
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
⊢ unramifiedLocus R A = Set.univ ↔ FormallyUnramified R A

Tactic:
unramifiedLocus_eq_compl_support,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (Module.support A Ω[A⁄R])ᶜ = Set.univ ↔ FormallyUnramified R A
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
inst✝ : EssFiniteType R A
⊢ IsOpen (unramifiedLocus R A)

Tactic:
unramifiedLocus_eq_compl_support,

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
⊢ IsOpen (Module.support A Ω[A⁄R])ᶜ
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
⊢ 1 - f 1 ∈ IsLocalRing.maximalIdeal A

Tactic:
← Ideal.Quotient.eq_zero_iff_mem,

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
⊢ (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) (1 - f 1) = 0
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
inst✝ : Algebra.FormallyEtale S T
⊢ IsBaseChange T (map R R S T)

Tactic:
change Function.Bijective _
  convert! (tensorKaehlerEquivOfFormallyEtale R S T).bijective using 1
  change _ = ((tensorKaehlerEquivOfFormallyEtale
    R S T).toLinearMap.restrictScalars S : T ⊗[S] Ω[S⁄R] → _)
  congr!
  ext
  simp

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case mp.H
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
x : M
a : x ∈ ⨆ i, torsionBySet A M ↑(I ^ i)
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun i ↦ torsionBySet A M ↑(I ^ i)

Tactic:
intro x y

Goal state after:
case mp.H
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
x✝ : M
a : x✝ ∈ ⨆ i, torsionBySet A M ↑(I ^ i)
x y : ℕ
⊢ ∃ z,
    (fun x1 x2 ↦ x1 ≤ x2) ((fun i ↦ torsionBySet A M ↑(I ^ i)) x) ((fun i ↦ torsionBySet A M ↑(I ^ i)) z) ∧
      (fun x1 x2 ↦ x1 ≤ x2) ((fun i ↦ torsionBySet A M ↑(I ^ i)) y) ((fun i ↦ torsionBySet A M ↑(I ^ i)) z)
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: ⊢ ⋃ r, Iic ↑r = univ

Tactic:
by
  exact iUnion_Iic_of_not_bddAbove_range not_bddAbove_coe

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : ↑s
h : [[s.ordConnectedProj x, s.ordConnectedProj y]] ⊆ s
⊢ s.ordConnectedProj x = s.ordConnectedProj y

Tactic:
exact
    ordConnectedProj_eq.2
      (mem_ordConnectedComponent_trans
        (mem_ordConnectedComponent_trans (ordConnectedProj_mem_ordConnectedComponent _ _) h)
        (mem_ordConnectedComponent_ordConnectedProj _ _))

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

Goal state before:
pp: a b c : ℝ≥0∞
hab : b ≤ a
b_ne_top : b ≠ ∞
⊢ a - b + c = a + c - b

Tactic:
by_cases c_top : c = ∞

Goal state after:
case pos
a b c : ℝ≥0∞
hab : b ≤ a
b_ne_top : b ≠ ∞
c_top : c = ∞
⊢ a - b + c = a + c - b

case neg
a b c : ℝ≥0∞
hab : b ≤ a
b_ne_top : b ≠ ∞
c_top : ¬c = ∞
⊢ a - b + c = a + c - b
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
κ : Sort u_2
g : κ → ℝ≥0∞
h : ∀ (i : ι) (j : κ), a ≤ f i + g j
⊢ a ≤ ⨅ i, ⨅ b, f i + g b

Tactic:
exact le_iInf₂ h

Goal state after:
Module: Mathlib.Algebra.Order.Module.Field

Goal state before:
pp: 𝕜 : Type u_1
G : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup G
inst✝³ : PartialOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : Module 𝕜 G
a : 𝕜
b₁ b₂ : G
inst✝ : PosSMulStrictMono 𝕜 G
h : a < 0
⊢ a⁻¹ • b₁ < b₂ ↔ a • b₂ < b₁

Tactic:
rw [← smul_lt_smul_iff_of_neg_left h, smul_inv_smul₀ h.ne]

Goal state after:
Module: Mathlib.Algebra.Order.Module.Field

Goal state before:
pp: 𝕜 : Type u_1
G : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup G
inst✝³ : PartialOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : Module 𝕜 G
a : 𝕜
b₁ b₂ : G
inst✝ : PosSMulStrictMono 𝕜 G
h : a < 0
⊢ b₁ < a⁻¹ • b₂ ↔ b₂ < a • b₁

Tactic:
rw [← smul_lt_smul_iff_of_neg_left h, smul_inv_smul₀ h.ne]

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
I I' : FractionalIdeal R⁰ K
inst✝ : Decidable (I ≠ 0 ∧ I' ≠ 0)
h : ¬(I ≠ 0 ∧ I' ≠ 0)
⊢ count K v (I * I') = 0

Tactic:
· rw [← mul_ne_zero_iff, not_ne_iff] at h
    rw [h, count_zero]

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

Goal state before:
pp: x : ℝ
⊢ Real.toEReal ⁻¹' Ici ↑x = Ici x

Tactic:
by
  change (WithBot.some ∘ WithTop.some) ⁻¹' (Ici (WithBot.some (WithTop.some x))) = _
  refine preimage_comp.trans ?_
  simp only [WithBot.preimage_coe_Ici, WithTop.preimage_coe_Ici]

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

Goal state before:
pp: ⊢ Real.toEReal ⁻¹' Ioi ⊥ = univ

Tactic:
change ((WithBot.some ∘ WithTop.some) ⁻¹' (Ioi (⊥ : WithBot (WithTop ℝ))) : Set ℝ) = _

Goal state after:
⊢ WithBot.some ∘ WithTop.some ⁻¹' Ioi ⊥ = univ
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case coe.top
x✝ : ℝ≥0
ha : ∞ ≠ 0 ∨ ↑x✝ ≠ ∞
hb : ∞ ≠ ∞ ∨ ↑x✝ ≠ 0
⊢ (∞ * ↑x✝)⁻¹ = ∞⁻¹ * (↑x✝)⁻¹

pp: case coe.coe
x✝¹ x✝ : ℝ≥0
ha : ↑x✝ ≠ 0 ∨ ↑x✝¹ ≠ ∞
hb : ↑x✝ ≠ ∞ ∨ ↑x✝¹ ≠ 0
⊢ (↑x✝ * ↑x✝¹)⁻¹ = (↑x✝)⁻¹ * (↑x✝¹)⁻¹

Tactic:
case top =>
    simp_all only [Ne, top_ne_zero, not_false_eq_true, coe_ne_top, or_self, not_true_eq_false,
      coe_eq_zero, false_or, top_mul, inv_top, zero_mul]

Goal state after:
case coe.coe
x✝¹ x✝ : ℝ≥0
ha : ↑x✝ ≠ 0 ∨ ↑x✝¹ ≠ ∞
hb : ↑x✝ ≠ ∞ ∨ ↑x✝¹ ≠ 0
⊢ (↑x✝ * ↑x✝¹)⁻¹ = (↑x✝)⁻¹ * (↑x✝¹)⁻¹
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 → ℤ
w : HeightOneSpectrum R
hw : w ∈ fun i ↦ i = v → False
⊢ count K v (↑w.asIdeal ^ exps w) = 0

Tactic:
rw [count_zpow, count_maximal_coprime K v hw, mul_zero]

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

Goal state before:
pp: α : Type u_2
m' : PseudoEMetricSpace α
toEDist✝ : EDist α
edist_self✝ : ∀ (x : α), edist x x = 0
edist_comm✝ : ∀ (x y : α), edist x y = edist y x
edist_triangle✝ : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
U : UniformSpace α
hU : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}
h :
  { toEDist := toEDist✝, edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
        toUniformSpace := U, uniformity_edist := hU }.toEDist =
    m'.toEDist
⊢ { toEDist := toEDist✝, edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
      toUniformSpace := U, uniformity_edist := hU } =
    m'

Tactic:
rename EDist α => ed

Goal state after:
α : Type u_2
m' : PseudoEMetricSpace α
ed : EDist α
edist_self✝ : ∀ (x : α), edist x x = 0
edist_comm✝ : ∀ (x y : α), edist x y = edist y x
edist_triangle✝ : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
U : UniformSpace α
hU : 𝓤 α = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}
h :
  { toEDist := ed, edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
        toUniformSpace := U, uniformity_edist := hU }.toEDist =
    m'.toEDist
⊢ { toEDist := ed, edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
      toUniformSpace := U, uniformity_edist := hU } =
    m'
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
⊢ edist x y ≤ edist z x + edist z y

Tactic:
rw [edist_comm z]; apply edist_triangle

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
ε : ℝ≥0∞
h : 0 < ε
⊢ x ∈ eball x ε

Tactic:
rwa [mem_eball, edist_self]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
s : Set α
inst✝ : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
x✝¹ : 0 < ε
δ : ℝ≥0∞
x✝ : 0 < δ
x : α
⊢ x ∈ eball a δ ∩ s → f x ∈ eball b ε ∩ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε

Tactic:
simp; tauto

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

Goal state before:
pp: x : ℝ≥0∞
x_ne_zero : x ≠ 0
x_ne_top : x ≠ ∞
m n : ℤ
⊢ x ^ (m + -n) = x ^ m * (x ^ n)⁻¹

Tactic:
ENNReal.zpow_add x_ne_zero x_ne_top,

Goal state after:
x : ℝ≥0∞
x_ne_zero : x ≠ 0
x_ne_top : x ≠ ∞
m n : ℤ
⊢ x ^ m * x ^ (-n) = x ^ m * (x ^ n)⁻¹
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

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

Tactic:
← add_assoc

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x₁ y₁ x₂ y₂ : α
⊢ dist x₂ y₂ ≤ dist x₂ x₁ + dist x₁ y₁ + dist y₁ y₂
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
⊢ closedBall x ε = ∅ ↔ ε < 0

Tactic:
rw [← not_nonempty_iff_eq_empty, nonempty_closedBall, not_le]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
a : R
K : Ideal R
e : J * K = Ideal.span {a}
e' : I + K = ⊤
⊢ J * I ⊔ Ideal.span {a} = J

Tactic:
rw [← e, ← Ideal.add_eq_sup, ← mul_add, e', Ideal.mul_top]

Goal state after:
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case neg
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
ha' : 0 < a
h : ¬BddAbove s
⊢ sSup (a • s) = a • sSup s

Tactic:
Real.sSup_of_not_bddAbove (mt (bddAbove_smul_iff_of_pos ha').1 h),

Goal state after:
case neg
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
ha' : 0 < a
h : ¬BddAbove s
⊢ 0 = a • sSup s
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
x y z : α
⊢ edist x z ≤ edist x y + edist y z

Tactic:
by
      simp only [edist_dist, ← ENNReal.ofReal_add, dist_nonneg]
      rw [ENNReal.ofReal_le_ofReal_iff _]
      · exact dist_triangle _ _ _
      · simpa using add_le_add (dist_nonneg : 0 ≤ dist x y) dist_nonneg

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
⊢ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1)) + dist (f n) (f (n + 1)) =
    ∑ i ∈ Finset.Ico m (n + 1), dist (f i) (f (i + 1))

Tactic:
by
        rw [← Finset.insert_Ico_right_eq_Ico_add_one hle, Finset.sum_insert, add_comm]; simp

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

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝ : Bornology β
f : α → β
⊢ Bornology.IsBounded univ ↔ Bornology.IsBounded (range f)

Tactic:
isBounded_induced,

Goal state after:
α : Type u_5
β : Type u_6
inst✝ : Bornology β
f : α → β
⊢ Bornology.IsBounded (f '' univ) ↔ Bornology.IsBounded (range f)
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 ι
⊢ TendstoLocallyUniformly F f p ↔ ∀ ε > 0, ∀ (x : β), ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε

Tactic:
by
  simp only [← tendstoLocallyUniformlyOn_univ, tendstoLocallyUniformlyOn_iff, nhdsWithin_univ,
    mem_univ, forall_const]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ Inseparable x y ↔ dist x y = 0

Tactic:
Metric.inseparable_iff_nndist,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ nndist x y = 0 ↔ dist x y = 0
Module: Mathlib.Topology.EMetricSpace.Basic

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))
⊢ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1)) + edist (f n) (f (n + 1)) =
    ∑ i ∈ Finset.Ico m (n + 1), edist (f i) (f (i + 1))

Tactic:
by
        rw [← Finset.insert_Ico_right_eq_Ico_add_one hle, Finset.sum_insert, add_comm]; simp

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

Goal state before:
pp: case inr.inl
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
h : 0 < 0 ∨ Nonempty β
this : Nonempty β := Or.resolve_left h (lt_irrefl 0)
inhabited_h : Inhabited β
⊢ sphere x 0 ⊆ ⋃ i, Function.eval i ⁻¹' sphere (x i) 0

Tactic:
refine subset_iUnion_of_subset default ?_

Goal state after:
case inr.inl
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
h : 0 < 0 ∨ Nonempty β
this : Nonempty β := Or.resolve_left h (lt_irrefl 0)
inhabited_h : Inhabited β
⊢ sphere x 0 ⊆ Function.eval default ⁻¹' sphere (x default) 0
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case neg
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
ha : ¬BddAbove s
⊢ s ∈ {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}

Tactic:
rcases mem_Ici_Ioi_of_subset_of_subset (hs.Ioi_csInf_subset hb ha) fun x hx ↦
      csInf_le hb hx with hs | hs

Goal state after:
case neg.inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs✝ : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
ha : ¬BddAbove s
hs : s = Ici (sInf s)
⊢ s ∈ {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}

case neg.inr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs✝ : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
ha : ¬BddAbove s
hs : s ∈ {Ioi (sInf s)}
⊢ s ∈ {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
Module: Mathlib.Topology.MetricSpace.ProperSpace

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
f : Filter α
hf : Cauchy f
t : Set α
t_fset : t ∈ f
ht : ∀ x ∈ t, ∀ y ∈ t, dist x y < 1
⊢ ∃ x, f ≤ nhds x

Tactic:
rcases hf.1.nonempty_of_mem t_fset with ⟨x, xt⟩

Goal state after:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
f : Filter α
hf : Cauchy f
t : Set α
t_fset : t ∈ f
ht : ∀ x ∈ t, ∀ y ∈ t, dist x y < 1
x : α
xt : x ∈ t
⊢ ∃ x, f ≤ nhds x
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
⊢ (∃ x y, ¬Inseparable x y) ↔ ∃ x, ‖x‖₊ ≠ 0

Tactic:
Metric.inseparable_iff_nndist,

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
⊢ (∃ x y, ¬nndist x y = 0) ↔ ∃ x, ‖x‖₊ ≠ 0
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: case inr.inl
X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
h'a : a ∈ t
h'b : b ∈ s
⊢ edist a b ≤ ediam s + edist x y + ediam t

pp: case inr.inr
X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
h'a : a ∈ t
h'b : b ∈ t
⊢ edist a b ≤ ediam s + edist x y + ediam t

Tactic:
· have Z := A b h'b a h'a
    rwa [edist_comm] at Z

Goal state after:
case inr.inr
X : Type u_2
s t : Set X
x y : X
inst✝ : PseudoEMetricSpace X
xs : x ∈ s
yt : y ∈ t
A : ∀ a ∈ s, ∀ b ∈ t, edist a b ≤ ediam s + edist x y + ediam t
a b : X
h'a : a ∈ t
h'b : b ∈ t
⊢ edist a b ≤ ediam s + edist x y + ediam t
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: ι : Type u_3
E : Type u_5
inst✝ : SeminormedCommGroup E
s : Finset ι
f a : ι → E
d : ι → ℝ
h : ∀ b ∈ s, ‖(f b)⁻¹ * a b‖ ≤ d b
⊢ dist (∏ b ∈ s, f b) (∏ b ∈ s, a b) ≤ ∑ b ∈ s, d b

Tactic:
rw [dist_eq_norm_inv_mul, ← Finset.prod_inv_distrib, ← Finset.prod_mul_distrib]

Goal state after:
ι : Type u_3
E : Type u_5
inst✝ : SeminormedCommGroup E
s : Finset ι
f a : ι → E
d : ι → ℝ
h : ∀ b ∈ s, ‖(f b)⁻¹ * a b‖ ≤ d b
⊢ ‖∏ x ∈ s, (f x)⁻¹ * a x‖ ≤ ∑ b ∈ s, d b
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ a • ball b r = ball (a • b) r

Tactic:
ext
  simp [mem_ball, Set.mem_smul_set, dist_eq_norm_inv_mul, ← eq_inv_mul_iff_mul_eq, mul_assoc]

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

Goal state before:
pp: E : Type u_5
inst✝ : NormedGroup E
a b : E
h : ‖a / b‖ ≤ 0
⊢ a = b

Tactic:
← div_eq_one,

Goal state after:
E : Type u_5
inst✝ : NormedGroup E
a b : E
h : ‖a / b‖ ≤ 0
⊢ a / b = 1
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u_3
inst✝⁴ : AddCommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompactIccSpace α
C : α
⊢ Bornology.IsBounded {x | |x| < C}

Tactic:
convert! Metric.isBounded_Ioo (-C) C

Goal state after:
α : Type u_3
inst✝⁴ : AddCommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompactIccSpace α
C : α
⊢ {x | |x| < C} = Ioo (-C) C
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
s : Set α
x y : α
inst✝ : PseudoMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ diam (s ∪ t) ≤ diam s + dist x y + diam t

Tactic:
simp only [diam, dist_edist]
  grw [ENNReal.toReal_le_add' (ediam_union_le_add_edist xs yt), ENNReal.toReal_add_le]
  · simp only [ENNReal.add_eq_top, edist_ne_top, or_false]
    exact fun h ↦ top_unique <| h ▸ ediam_mono subset_union_left
  · exact fun h ↦ top_unique <| h ▸ ediam_mono subset_union_right

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

Goal state before:
pp: α : Type u
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
⊢ cobounded α = cocompact α

Tactic:
nontriviality α; inhabit α
  exact cobounded_le_cocompact.antisymm <| (hasBasis_cobounded_compl_closedBall default).ge_iff.2
    fun _ _ ↦ (isCompact_closedBall _ _).compl_mem_cocompact

Goal state after: