mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
inst✝ : QuasiFinite R T
P : Ideal S
hP : P.IsPrime
f : P.ResidueField ⊗[R] T →ₐ[P.ResidueField] P.Fiber T :=
  TensorProduct.lift (ofId P.ResidueField (P.Fiber T)) (AlgHom.restrictScalars R TensorProduct.includeRight) ⋯
⊢ Submodule.span S {t | ∃ m n, m ⊗ₜ[S] n = t} ≤ (AlgHom.restrictScalars S f).toLinearMap.range

Tactic:
Submodule.span_le

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
inst✝ : QuasiFinite R T
P : Ideal S
hP : P.IsPrime
f : P.ResidueField ⊗[R] T →ₐ[P.ResidueField] P.Fiber T :=
  TensorProduct.lift (ofId P.ResidueField (P.Fiber T)) (AlgHom.restrictScalars R TensorProduct.includeRight) ⋯
⊢ {t | ∃ m n, m ⊗ₜ[S] n = t} ⊆ ↑(AlgHom.restrictScalars S f).toLinearMap.range
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case monomial
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₁
Q : Generators S T ι
y : Q.Ring
n : ι →₀ ℕ
r : S
⊢ (δAux R Q) ((monomial n) r * y) = (monomial n) r • (δAux R Q) y + y • (δAux R Q) ((monomial n) r)

Tactic:
induction y using MvPolynomial.induction_on' with
    | monomial m s =>
      simp only [monomial_mul, δAux_monomial, Derivation.leibniz, tmul_add, tmul_smul,
        smul_tmul', Algebra.smul_def, algebraMap_apply, aeval_monomial, mul_assoc]
      rw [mul_comm (m.prod _) (n.prod _)]
      simp only [pow_zero, implies_true, pow_add, Finsupp.prod_add_index']
    | add y₁ y₂ hy₁ hy₂ => simp only [map_add, smul_add, hy₁, hy₂, mul_add, add_smul]; abel

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 σ
i : σ
| (Q.comp P).toExtension.toKaehler
    ((Extension.CotangentSpace.map (Q.toComp P).toExtensionHom) (1 ⊗ₜ[P.Ring] (D R P.Ring) (X i)))

Tactic:
enter [2]

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 σ
i : σ
| (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom) (1 ⊗ₜ[P.Ring] (D R P.Ring) (X i))
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: case pos
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
p : Ideal R := under R q
f₀ : S ≃ₐ[R] S := (MulSemiringAction.toAlgAut G R S) g
hg : g • q = map f₀ q
Sq : Type u_2 := Localization.AtPrime q
Sq' : Type u_2 := Localization.AtPrime (map f₀ q)
f : Sq ≃ₐ[R] Sq' := Localization.localAlgEquiv q (map f₀ q) f₀ ⋯
this✝ : Algebra Sq Sq' := f.toRingEquiv.toRingHom.toAlgebra
this : IsScalarTower R Sq Sq'
e : (Sq ⧸ map (algebraMap R Sq) p) ≃ₐ[Sq] Sq' ⧸ map (algebraMap R Sq') p :=
  (map (algebraMap R Sq) p).quotientEquivAlg (map (algebraMap R Sq') p) (AlgEquiv.ofBijective (Algebra.ofId Sq Sq') ⋯) ⋯
⊢ (Module.length (Localization.AtPrime (map f₀ q))
        (Localization.AtPrime (map f₀ q) ⧸ map (algebraMap R (Localization.AtPrime (map f₀ q))) p)).toNat =
    (Module.length (Localization.AtPrime q)
        (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) p)).toNat

Tactic:
e.toLinearEquiv.length_eq,

Goal state after:
case pos
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
p : Ideal R := under R q
f₀ : S ≃ₐ[R] S := (MulSemiringAction.toAlgAut G R S) g
hg : g • q = map f₀ q
Sq : Type u_2 := Localization.AtPrime q
Sq' : Type u_2 := Localization.AtPrime (map f₀ q)
f : Sq ≃ₐ[R] Sq' := Localization.localAlgEquiv q (map f₀ q) f₀ ⋯
this✝ : Algebra Sq Sq' := f.toRingEquiv.toRingHom.toAlgebra
this : IsScalarTower R Sq Sq'
e : (Sq ⧸ map (algebraMap R Sq) p) ≃ₐ[Sq] Sq' ⧸ map (algebraMap R Sq') p :=
  (map (algebraMap R Sq) p).quotientEquivAlg (map (algebraMap R Sq') p) (AlgEquiv.ofBijective (Algebra.ofId Sq Sq') ⋯) ⋯
⊢ (Module.length (Localization.AtPrime (map f₀ q))
        (Localization.AtPrime (map f₀ q) ⧸ map (algebraMap R (Localization.AtPrime (map f₀ q))) p)).toNat =
    (Module.length Sq (Sq' ⧸ map (algebraMap R Sq') p)).toNat
Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds

Goal state before:
pp: G : Type u_2
inst✝³ : Group G
inst✝² : Preorder G
inst✝¹ : MulLeftMono G
inst✝ : MulRightMono G
s t : Set G
a b : G
hs : IsLUB s a
ht : IsGLB t b
⊢ IsLUB (s * t⁻¹) (a / b)

Tactic:
div_eq_mul_inv

Goal state after:
G : Type u_2
inst✝³ : Group G
inst✝² : Preorder G
inst✝¹ : MulLeftMono G
inst✝ : MulRightMono G
s t : Set G
a b : G
hs : IsLUB s a
ht : IsGLB t b
⊢ IsLUB (s * t⁻¹) (a * b⁻¹)
Module: Mathlib.Algebra.Order.Group.Pointwise.Bounds

Goal state before:
pp: G : Type u_2
inst✝³ : Group G
inst✝² : Preorder G
inst✝¹ : MulLeftMono G
inst✝ : MulRightMono G
s t : Set G
a b : G
hs : IsLUB s a
ht : IsGLB t b
⊢ IsLUB (s / t) (a / b)

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv]
  exact hs.mul ht.inv

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice

Goal state before:
pp: M : Type u_1
inst✝³ : ConditionallyCompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s t : Set M
hs₀ : s.Nonempty
hs₁ : BddAbove s
ht₀ : t.Nonempty
ht₁ : BddBelow t
⊢ sSup s * (sInf t)⁻¹ = sSup s / sInf t

Tactic:
div_eq_mul_inv

Goal state after:
M : Type u_1
inst✝³ : ConditionallyCompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s t : Set M
hs₀ : s.Nonempty
hs₁ : BddAbove s
ht₀ : t.Nonempty
ht₁ : BddBelow t
⊢ sSup s * (sInf t)⁻¹ = sSup s * (sInf t)⁻¹
Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice

Goal state before:
pp: M : Type u_1
inst✝³ : ConditionallyCompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s t : Set M
hs₀ : s.Nonempty
hs₁ : BddBelow s
ht₀ : t.Nonempty
ht₁ : BddAbove t
⊢ sInf s * (sSup t)⁻¹ = sInf s / sSup t

Tactic:
div_eq_mul_inv

Goal state after:
M : Type u_1
inst✝³ : ConditionallyCompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s t : Set M
hs₀ : s.Nonempty
hs₁ : BddBelow s
ht₀ : t.Nonempty
ht₁ : BddAbove t
⊢ sInf s * (sSup t)⁻¹ = sInf s * (sSup t)⁻¹
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ sInf ∅ = 0

Tactic:
by
  rw [← coe_eq_zero, coe_sInf, Set.image_empty, Real.sInf_empty]

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_1
f : CauSeq ℝ abs
s : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ x, ∀ y ∈ s, y ≤ x
h : f < const abs (sSup s)
⊢ False

Tactic:
rcases h with ⟨ε, ε0, i, ih⟩

Goal state after:
case refine_1
f : CauSeq ℝ abs
s : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ x, ∀ y ∈ s, y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ j ≥ i, ε ≤ ↑(const abs (sSup s) - f) j
⊢ False
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_2
f : CauSeq ℝ abs
s : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ x, ∀ y ∈ s, y ≤ x
h : const abs (sSup s) < f
⊢ False

Tactic:
rcases h with ⟨ε, ε0, i, ih⟩

Goal state after:
case refine_2
f : CauSeq ℝ abs
s : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ x, ∀ y ∈ s, y ≤ x
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ j ≥ i, ε ≤ ↑(f - const abs (sSup s)) j
⊢ False
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
⊢ (Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)).factors =
    (Associates.mk v.asIdeal).count (Associates.mk I).factors

Tactic:
by
  have h_ne_zero := Associates.finprod_ne_zero I
  have hv : Irreducible (Associates.mk v.asIdeal) := v.associates_irreducible
  have h_dvd := finprod_mem_dvd v (hasFiniteMulSupport hI)
  have h_not_dvd := Ideal.finprod_not_dvd v I hI
  simp only [IsDedekindDomain.HeightOneSpectrum.maxPowDividing] at h_dvd h_ne_zero h_not_dvd
  rw [← Associates.mk_dvd_mk] at h_dvd h_not_dvd
  simp only [Associates.dvd_eq_le] at h_dvd h_not_dvd
  rw [Associates.mk_pow, Associates.prime_pow_dvd_iff_le h_ne_zero hv] at h_dvd h_not_dvd
  rw [not_le] at h_not_dvd
  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: r : ℝ
x : ℝ≥0
hx : r = ↑x ∨ r = -↑x
⊢ r = 0 ∨ ∃ x, 0 < x ∧ (r = ↑x ∨ r = -↑x)

Tactic:
or_iff_not_imp_left

Goal state after:
r : ℝ
x : ℝ≥0
hx : r = ↑x ∨ r = -↑x
⊢ ¬r = 0 → ∃ x, 0 < x ∧ (r = ↑x ∨ r = -↑x)
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: a : ℝ≥0∞
b : ℝ≥0
h : a ≤ ↑b
⊢ a.toReal ≤ ↑b

Tactic:
by
  lift a to ℝ≥0 using ne_top_of_le_ne_top coe_ne_top h
  simpa using h

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

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf : Surjective ⇑φ
y : M₂
hy : y ∈ primaryComponent M₂ P.asIdeal
⊢ ∃ a, (map P.asIdeal φ) a = ⟨y, hy⟩

Tactic:
obtain ⟨b, rfl⟩ : ∃ a, φ a = y := hf y

Goal state after:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf : Surjective ⇑φ
b : M₁
hy : φ b ∈ primaryComponent M₂ P.asIdeal
⊢ ∃ a, (map P.asIdeal φ) a = ⟨φ b, hy⟩
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: p q : ℝ
hp : 0 ≤ p
⊢ ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q

Tactic:
rw [ENNReal.ofReal, ENNReal.ofReal, coe_lt_coe, Real.toNNReal_lt_toNNReal_iff_of_nonneg hp]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
⊢ (⇑ofDual ⁻¹' s).ordConnectedSection = ⇑ofDual ⁻¹' s.ordConnectedSection

Tactic:
simp only [ordConnectedSection]
  simp +unfoldPartialApp only [ordConnectedProj]
  ext x
  simp only [mem_range, Subtype.exists, mem_preimage, OrderDual.exists, dual_ordConnectedComponent,
    ofDual_toDual]
  tauto

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

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ∞
⊢ a - ⨆ i, f i = ⨅ i, a - f i

Tactic:
obtain ⟨i, hi⟩ | h := em (∃ i, a < f i)

Goal state after:
case inl
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ∞
i : ι
hi : a < f i
⊢ a - ⨆ i, f i = ⨅ i, a - f i

case inr
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ∞
h : ¬∃ i, a < f i
⊢ a - ⨆ i, f i = ⨅ i, a - f i
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
ι : Type u_3
s : Finset ι
I : ι → FractionalIdeal R⁰ K
hS : ∀ i ∈ s, I i ≠ 0
⊢ count K v (∏ i ∈ s, I i) = ∑ i ∈ s, count K v (I i)

Tactic:
induction s using Finset.induction with

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

Goal state before:
pp: a b : ℝ≥0∞
ha₀ : a = 0 → b = 0
ha : a = ∞ → b = 0
⊢ a * (b / a) = b

Tactic:
by
  rw [mul_comm, ENNReal.div_mul_cancel' ha₀ ha]

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

Goal state before:
pp: m n : ℕ
⊢ ↑m = ↑n ↔ m = n

Tactic:
← coe_coe_eq_natCast n,

Goal state after:
m n : ℕ
⊢ ↑m = ↑↑n ↔ m = n
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: m n : ℕ
⊢ ↑m ≤ ↑n ↔ m ≤ n

Tactic:
← coe_coe_eq_natCast n,

Goal state after:
m n : ℕ
⊢ ↑m ≤ ↑↑n ↔ m ≤ n
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: m n : ℕ
⊢ ↑m < ↑n ↔ m < n

Tactic:
← coe_coe_eq_natCast n,

Goal state after:
m n : ℕ
⊢ ↑m < ↑↑n ↔ m < n
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ 0
⊢ (a - b) / c = a / c - b / c

Tactic:
div_eq_mul_inv

Goal state after:
a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ 0
⊢ (a - b) * c⁻¹ = a * c⁻¹ - b * c⁻¹
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
exps : HeightOneSpectrum R → ℤ
⊢ count K v (∏ᶠ (w : HeightOneSpectrum R) (_ : w ≠ v), ↑w.asIdeal ^ exps w) = 0

Tactic:
apply finprod_mem_induction fun I => count K v I = 0

Goal state after:
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 → ℤ
⊢ count K v 1 = 0

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 → ℤ
⊢ ∀ (x y : FractionalIdeal R⁰ K), count K v x = 0 → count K v y = 0 → count K v (x * y) = 0

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 → ℤ
⊢ ∀ x ∈ fun i ↦ i = v → False, count K v (↑x.asIdeal ^ exps x) = 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
⊢ a.toNNReal * b.toNNReal⁻¹ = a.toNNReal / b.toNNReal

Tactic:
div_eq_mul_inv

Goal state after:
a b : ℝ≥0∞
⊢ a.toNNReal * b.toNNReal⁻¹ = a.toNNReal * b.toNNReal⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
⊢ a.toReal * b.toReal⁻¹ = a.toReal / b.toReal

Tactic:
div_eq_mul_inv

Goal state after:
a b : ℝ≥0∞
⊢ a.toReal * b.toReal⁻¹ = a.toReal * b.toReal⁻¹
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: case bc
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : ε₁ + dist x y ≤ ε₂
z : α
hz : z ∈ ball x ε₁
⊢ dist z x < ε₁

Tactic:
exact hz

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

Goal state before:
pp: case h₁
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : ε₁ + dist x y ≤ ε₂
z : α
hz : z ∈ closedBall x ε₁
⊢ dist z x ≤ ε₁

Tactic:
exact hz

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

Goal state before:
pp: case h₁
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : ε₁ + dist x y < ε₂
z : α
hz : z ∈ closedBall x ε₁
⊢ dist z x ≤ ε₁

Tactic:
exact hz

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
p : α → Prop
x : α
H : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ ball x R, p y
y : α
⊢ p y

Tactic:
by
  obtain ⟨R, hR, h⟩ : ∃ R > dist y x, ∀ z : α, z ∈ ball x R → p z :=
    frequently_iff.1 H (Ioi_mem_atTop (dist y x))
  exact h _ hR

Goal state after:
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 : α
⊢ dist x z ≤ dist x y + dist y z

Tactic:
exact dist_triangle _ _ _

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

Goal state before:
pp: ι : Sort u_3
f : ι → ℝ≥0
a : ℝ≥0
⊢ iInf f * a = ⨅ i, f i * a

Tactic:
rw [← coe_inj, NNReal.coe_mul, coe_iInf, coe_iInf]

Goal state after:
ι : Sort u_3
f : ι → ℝ≥0
a : ℝ≥0
⊢ (⨅ i, ↑(f i)) * ↑a = ⨅ i, ↑(f i * a)
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: β : Type v
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetrizableSpace α
f : β → α
inst✝ : TopologicalSpace β
hf : IsInducing f
s : Set α
hs : IsSeparable s
⊢ IsSeparable (f ⁻¹' s)

Tactic:
let : UniformSpace α := TopologicalSpace.pseudoMetrizableSpaceUniformity α

Goal state after:
β : Type v
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetrizableSpace α
f : β → α
inst✝ : TopologicalSpace β
hf : IsInducing f
s : Set α
hs : IsSeparable s
this : UniformSpace α := pseudoMetrizableSpaceUniformity α
⊢ IsSeparable (f ⁻¹' s)
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
⊢ interior (Ici a) = Ioi a

Tactic:
rw [← compl_Iio, interior_compl, closure_Iio' ha, compl_Iic]

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝¹ : Lattice α
inst✝ : Nonempty α
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s

Tactic:
simp [IsBounded, IsCobounded, -isCobounded_compl_iff]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
x : α
Mf : MonotoneOn f (Iio x)
h_bdd : BddAbove (f '' Iio x)
⊢ Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))

Tactic:
rcases eq_empty_or_nonempty (Iio x) with (h | h)

Goal state after:
case inl
α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
x : α
Mf : MonotoneOn f (Iio x)
h_bdd : BddAbove (f '' Iio x)
h : Iio x = ∅
⊢ Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))

case inr
α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
x : α
Mf : MonotoneOn f (Iio x)
h_bdd : BddAbove (f '' Iio x)
h : (Iio x).Nonempty
⊢ Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
⊢ sInf (f '' Icc a b) ≤ f c

Tactic:
have := mem_image_of_mem f hc
  rw [h.image_Icc (hc.1.trans hc.2)] at this
  exact this.1

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
n : ℤ
⊢ ‖a ^ |n|‖ = ‖a ^ n‖

Tactic:
norm_zpow_abs

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
n : ℤ
⊢ ‖a ^ n‖ = ‖a ^ n‖
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) < ε

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

Tactic:
· intro h ε hε
    let u := { a : α × α | dist a.fst a.snd < ε }
    have hu : u ∈ 𝓤 α := Metric.mem_uniformity_dist.mpr ⟨ε, hε, by simp [u]⟩
    rw [← Filter.eventually_atTop_prod_self' (p := fun m =>
      ∀ x ∈ s, dist (F m.fst x) (F m.snd x) < ε)]
    specialize h u hu
    rw [prod_atTop_atTop_eq] at h
    exact h.mono fun n h x hx => h x hx

Goal state after:
case mpr
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
⊢ (∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε) → UniformCauchySeqOn F atTop s
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
r : ℝ
⊢ b ∈ ball a r ↔ ‖a⁻¹ * b‖ < r

Tactic:
by
  rw [mem_ball', dist_eq_norm_inv_mul]

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

Goal state before:
pp: 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 : X
ha : a ∈ s ∨ a ∈ t
b : X
hb : b ∈ s ∨ b ∈ t
⊢ edist a b ≤ ediam s + edist x y + ediam t

Tactic:
rcases ha with h'a | h'a <;> rcases hb with h'b | h'b

Goal state after:
case inl.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 ∈ s
h'b : b ∈ s
⊢ edist a b ≤ ediam s + edist x y + ediam t

case inl.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 ∈ s
h'b : b ∈ t
⊢ edist a b ≤ ediam s + edist x y + ediam t

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

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.Topology.EMetricSpace.Diam

Goal state before:
pp: ι : Type u_3
X : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (X i)
s : (i : ι) → Set (X i)
c : ℝ≥0∞
h : ∀ (b : ι), ediam (s b) ≤ c
x : (i : ι) → X i
hx : x ∈ univ.pi s
y : (i : ι) → X i
hy : y ∈ univ.pi s
⊢ ∀ (b : ι), edist (x b) (y b) ≤ c

Tactic:
mem_univ_pi

Goal state after:
ι : Type u_3
X : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (X i)
s : (i : ι) → Set (X i)
c : ℝ≥0∞
h : ∀ (b : ι), ediam (s b) ≤ c
x : (i : ι) → X i
hx : ∀ (i : ι), x i ∈ s i
y : (i : ι) → X i
hy : ∀ (i : ι), y i ∈ s i
⊢ ∀ (b : ι), edist (x b) (y b) ≤ c
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : NormedGroup E
a : E
⊢ ‖a‖ ≤ 0 ↔ a = 1

Tactic:
rw [← dist_one_right, dist_le_zero]

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

Goal state before:
pp: E : Type u_5
inst✝ : NormedGroup E
a b : E
⊢ 0 < ‖a / b‖ ↔ a ≠ b

Tactic:
(norm_nonneg' _).lt_iff_ne,

Goal state after:
E : Type u_5
inst✝ : NormedGroup E
a b : E
⊢ 0 ≠ ‖a / b‖ ↔ a ≠ b