mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.JacobsonSpace

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

Tactic:
discreteTopology_iff_forall_isOpen

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
h : (closedPoints X).Finite
this : closedPoints X = Set.univ
inst : Finite X
⊢ ∀ (s : Set X), IsOpen[inst✝¹] s
Module: Mathlib.RingTheory.RamificationInertia.Inertia

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
q : Ideal S
inst✝³ : Module.Finite R S
inst✝² : p.IsMaximal
inst✝¹ : q.IsMaximal
inst✝ : q.LiesOver p
⊢ Submodule.cardQuot p ^ q.inertiaDeg R = Submodule.cardQuot q

Tactic:
let _ : Field (R ⧸ p) := Quotient.field p

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal R
q : Ideal S
inst✝³ : Module.Finite R S
inst✝² : p.IsMaximal
inst✝¹ : q.IsMaximal
inst✝ : q.LiesOver p
x✝ : Field (R ⧸ p) := Quotient.field p
⊢ Submodule.cardQuot p ^ q.inertiaDeg R = Submodule.cardQuot q
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: case h₂
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDedekindDomain S
inst✝² : IsDedekindDomain R
inst✝¹ : FaithfulSMul R S
v : Ideal R
w : Ideal S
hv : Irreducible v
hw : Irreducible w
hw_bot : w ≠ ⊥
inst✝ : w.LiesOver v
hI : IsUnit ⊤
h : ⊤ ≠ ⊥
⊢ ↑(Multiset.count (normalize w) (normalizedFactors 1)) =
    ↑(v.ramificationIdx' w) * ↑(Multiset.count (normalize v) (normalizedFactors 1))

Tactic:
normalizedFactors_one

Goal state after:
case h₂
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDedekindDomain S
inst✝² : IsDedekindDomain R
inst✝¹ : FaithfulSMul R S
v : Ideal R
w : Ideal S
hv : Irreducible v
hw : Irreducible w
hw_bot : w ≠ ⊥
inst✝ : w.LiesOver v
hI : IsUnit ⊤
h : ⊤ ≠ ⊥
⊢ ↑(Multiset.count (normalize w) 0) = ↑(v.ramificationIdx' w) * ↑(Multiset.count (normalize v) 0)
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallyUnramified R A
I : Ideal B
hI : IsNilpotent I
⊢ ∀ (g₁ g₂ : A →ₐ[R] B), (Ideal.Quotient.mkₐ R I).comp g₁ = (Ideal.Quotient.mkₐ R I).comp g₂ → g₁ = g₂

Tactic:
change Function.Injective (Ideal.Quotient.mkₐ R I).comp

Goal state after:
R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallyUnramified R A
I : Ideal B
hI : IsNilpotent I
⊢ Function.Injective (Ideal.Quotient.mkₐ R I).comp
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
t e : S ⊗[R] S
ht₁ : ∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * (1 - e) = 0
ht₂ : e ∈ Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
s : S
⊢ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1 = e * (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Tactic:
linear_combination ht₁ s

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

Goal state before:
pp: case e_g
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
i : I
⊢ (fun a_1 b_1 ↦ ((a a_1) i • b.repr b_1).sum fun j z ↦ z • b j ⊗ₜ[R] b i) = fun i_1 y ↦
    (b.repr y).sum fun j z ↦ (a i_1) i • z • b j ⊗ₜ[R] b i

Tactic:
ext j s

Goal state after:
case e_g
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
i j : I
s : S
⊢ (((a j) i • b.repr s).sum fun j z ↦ z • b j ⊗ₜ[R] b i) = (b.repr s).sum fun j_1 z ↦ (a j) i • z • b j_1 ⊗ₜ[R] b i
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
r : S
m : M
⊢ (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip (r • m))) (elem R S) =
    (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (1 ⊗ₜ[R] r * elem R S)

Tactic:
induction elem R S using TensorProduct.induction_on
      · simp
      · simp [smul_comm r]
      · simp only [map_add, mul_add, *]

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.toExtension.Ring
hx : x ∈ Q.toExtension.ker
this : x ∈ Q.ker
⊢ ∃ a, (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) a = Extension.Cotangent.mk ⟨x, hx⟩

Tactic:
rw [← map_ofComp_ker Q P, Ideal.mem_map_iff_of_surjective
    _ (toAlgHom_ofComp_surjective Q P)] at this

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.toExtension.Ring
hx : x ∈ Q.toExtension.ker
this : ∃ x_1 ∈ (Q.comp P).ker, (Q.ofComp P).toAlgHom x_1 = x
⊢ ∃ a, (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) a = Extension.Cotangent.mk ⟨x, hx⟩
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 σ
⊢ LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom) ∘ₗ
      LinearMap.baseChange T P.toExtension.cotangentComplex =
    (Q.comp P).toExtension.cotangentComplex ∘ₗ
      LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom)

Tactic:
ext x; simp [Extension.CotangentSpace.map_cotangentComplex]

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

Goal state before:
pp: K : Type u_1
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FormallyUnramified K L
inst✝ : EssFiniteType K L
this✝¹ : Module.Finite K L
this✝ : FormallyUnramified (↥(separableClosure K L)) L
this : EssFiniteType (↥(separableClosure K L)) L
x✝ : L
⊢ x✝ ∈ separableClosure K L ↔ x✝ ∈ ⊤

Tactic:
change _ ↔ _ ∈ (⊤ : Subring _)

Goal state after:
K : Type u_1
L : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FormallyUnramified K L
inst✝ : EssFiniteType K L
this✝¹ : Module.Finite K L
this✝ : FormallyUnramified (↥(separableClosure K L)) L
this : EssFiniteType (↥(separableClosure K L)) L
x✝ : L
⊢ x✝ ∈ separableClosure K L ↔ x✝ ∈ ⊤
Module: Mathlib.RingTheory.Unramified.LocalRing

Goal state before:
pp: case e_6
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
hq : p.primesOver S = {q}
inst✝¹ : Module.Finite R S
inst✝ : q.LiesOver p
hRS : (RingHom.ker (algebraMap R S)).FG
H : Function.Bijective ⇑(localRingHom p q (algebraMap R S) ⋯)
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
a b : S → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S) (a x) = x * (algebraMap R S) (b x)
r : R
hrp : r ∉ p
hr : ∀ (r' : R), r ∣ r' → Function.Injective ⇑(awayMap (algebraMap R S) r')
r' : R
x : S
hxs : x ∈ ↑s
r'' : R
hr' : r' = (r * ∏ i ∈ s, b i) * r''
⊢ (algebraMap R S) r'' * (algebraMap R S) r * (algebraMap R S) (∏ i ∈ s.erase x, b i) * (x * (algebraMap R S) (b x)) =
    x * (algebraMap R S) r'

Tactic:
hr',

Goal state after:
case e_6
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
hq : p.primesOver S = {q}
inst✝¹ : Module.Finite R S
inst✝ : q.LiesOver p
hRS : (RingHom.ker (algebraMap R S)).FG
H : Function.Bijective ⇑(localRingHom p q (algebraMap R S) ⋯)
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
a b : S → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S) (a x) = x * (algebraMap R S) (b x)
r : R
hrp : r ∉ p
hr : ∀ (r' : R), r ∣ r' → Function.Injective ⇑(awayMap (algebraMap R S) r')
r' : R
x : S
hxs : x ∈ ↑s
r'' : R
hr' : r' = (r * ∏ i ∈ s, b i) * r''
⊢ (algebraMap R S) r'' * (algebraMap R S) r * (algebraMap R S) (∏ i ∈ s.erase x, b i) * (x * (algebraMap R S) (b x)) =
    x * (algebraMap R S) ((r * ∏ i ∈ s, b i) * r'')
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: s : Set ℝ
h₁ : s.Nonempty
h₂ : BddAbove s
⊢ IsLUB s (sSup s)

Tactic:
simp only [sSup_def, dif_pos (And.intro h₁ h₂)]
  apply Classical.choose_spec

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

Goal state before:
pp: r₁ r₂ : ℝ≥0
h : r₂ ≤ r₁
⊢ ↑r₂ ≤ ↑r₁ - 0

Tactic:
simp [show (r₂ : ℝ) ≤ r₁ from h]

Goal state after:
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
ε : ℝ
ε0 : ε > 0
i : ℕ
ih : ∀ j ≥ i, ε ≤ ↑(f - const abs (sSup s)) j
j : ℕ
ij : j ≥ i
⊢ ε / 2 ≤ ↑f j - (sSup s + ε / 2)

Tactic:
← sub_sub,

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
j : ℕ
ij : j ≥ i
⊢ ε / 2 ≤ ↑f j - sSup s - ε / 2
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:
by simp_rw [map_one_eq_zero p, map_one_eq_zero q, zero_add]

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

Goal state before:
pp: case h₁
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
s : Set (GroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
this : Nonempty ↑s
p : ↑s
⊢ ↑p x ≤ ⨆ p, ↑p x

pp: case h₂
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
s : Set (GroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
this : Nonempty ↑s
p : ↑s
⊢ ↑p y ≤ ⨆ p, ↑p y

Tactic:
all_goals
              apply le_ciSup (f := (DFunLike.coe · _) ∘ Subtype.val) ?_ p
              simpa [Set.range_comp] using Monotone.map_bddAbove (fun _ _ h' ↦ by exact h' _) h

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
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
hJ_ne_zero : J ≠ 0
hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J
ha_ne_zero : span {a} ≠ 0
ha :
  ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors) =
    ↑(span {a})
v : HeightOneSpectrum R
⊢ ↑v.asIdeal ^
      (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors)) =
    ↑v.asIdeal ^
      (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) +
        -↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors))

Tactic:
sub_eq_add_neg

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
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
hJ_ne_zero : J ≠ 0
hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J
ha_ne_zero : span {a} ≠ 0
ha :
  ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors) =
    ↑(span {a})
v : HeightOneSpectrum R
⊢ ↑v.asIdeal ^
      (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) +
        -↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors)) =
    ↑v.asIdeal ^
      (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) +
        -↑((Associates.mk v.asIdeal).count (Associates.mk (span {a})).factors))
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
h : a.toNNReal ≤ b.toNNReal
⊢ a ≤ b

Tactic:
by rwa [← coe_toNNReal ha, ← coe_toNNReal hb, coe_le_coe]

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

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

Tactic:
rw [ENNReal.ofReal, ENNReal.ofReal, coe_lt_coe, Real.toNNReal_lt_toNNReal_iff h]

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

Goal state before:
pp: case h₁
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p✝ q : NonarchAddGroupSeminorm E
s : Set (NonarchAddGroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
this : Nonempty ↑s
p : ↑s
⊢ ↑p x ≤ ⨆ p, ↑p x

pp: case h₂
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝ : AddGroup E
p✝ q : NonarchAddGroupSeminorm E
s : Set (NonarchAddGroupSeminorm E)
h : BddAbove s
x y : E
hs : s.Nonempty
this : Nonempty ↑s
p : ↑s
⊢ ↑p y ≤ ⨆ p, ↑p y

Tactic:
all_goals
              apply le_ciSup (f := (DFunLike.coe · _) ∘ Subtype.val) ?_ p
              simpa [Set.range_comp] using Monotone.map_bddAbove (fun _ _ h' ↦ by exact h' _) h

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

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : LinearOrder α✝
s✝ t✝ : Set α✝
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x a : α
has : a ∈ s
b : α
hbt : b ∈ t
hab : a ≤ b
ha : [[a, x]] ⊆ tᶜ
ha' : [[a, x]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
hb : [[b, x]] ⊆ sᶜ
hb' : [[x, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ
⊢ [[a, b]] ⊆ (s.ordSeparatingSet t).ordConnectedSectionᶜ

Tactic:
calc
      [[a, b]] ⊆ [[a, x]] ∪ [[x, b]] := uIcc_subset_uIcc_union_uIcc
      _ ⊆ (ordSeparatingSet s t).ordConnectedSectionᶜ := union_subset ha' hb'

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

Goal state before:
pp: c : ℝ≥0∞
a b : ℝ≥0
h : ↑b ≤ ↑a
⊢ ↑a - c - (↑a - ↑b) = ↑b - c

Tactic:
cases c

Goal state after:
case top
a b : ℝ≥0
h : ↑b ≤ ↑a
⊢ ↑a - ∞ - (↑a - ↑b) = ↑b - ∞

case coe
a b : ℝ≥0
h : ↑b ≤ ↑a
x✝ : ℝ≥0
⊢ ↑a - ↑x✝ - (↑a - ↑b) = ↑b - ↑x✝
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝¹ : Nonempty ι
inst✝ : Nonempty κ
g : κ → ℝ≥0∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
⊢ ⨆ i, f i + iSup g ≤ a

Tactic:
add_iSup

Goal state after:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝¹ : Nonempty ι
inst✝ : Nonempty κ
g : κ → ℝ≥0∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
⊢ ⨆ i, ⨆ i_1, f i + g i_1 ≤ a
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: 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

Tactic:
simp_rw [not_exists, not_lt] at h

Goal state after:
case inr
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ∞
h : ∀ (x : ι), f x ≤ a
⊢ a - ⨆ i, f i = ⨅ i, a - f i
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
ht : b ≠ ∞ ∨ c ≠ ∞
⊢ a ≤ c / b ↔ a * b ≤ c

Tactic:
cases b with
  | top =>
    lift c to ℝ≥0 using ht.neg_resolve_left rfl
    rw [div_top, nonpos_iff_eq_zero]
    rcases eq_or_ne a 0 with (rfl | ha) <;> simp [*]
  | coe b => ?_

Goal state after:
case coe
a c : ℝ≥0∞
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ∞ ∨ c ≠ ∞
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case refine_2
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ ↑x < ↑y ^ (n + 1)

Tactic:
rwa [← ENNReal.coe_zpow A, ENNReal.coe_lt_coe]

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

Goal state before:
pp: case refine_1
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ↑y ^ n < ↑x

Tactic:
rwa [← ENNReal.coe_zpow A, ENNReal.coe_lt_coe]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
⊢ (∀ (i : ℝ≥0∞), 0 < i → ∃ y ∈ s, y ∈ eball x i) ↔ ∀ ε > 0, ∃ y ∈ s, edist x y < ε

Tactic:
by simp only [mem_eball, edist_comm x]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
⊢ Tendsto f (𝓝 b) (𝓝 (f b)) ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, edist (f x) (f b) < ε

Tactic:
tendsto_nhds

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
⊢ (∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, edist (f x) (f b) < ε) ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, edist (f x) (f b) < ε
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
s : Set β
⊢ Tendsto f (𝓝[s] b) (𝓝 (f b)) ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, edist (f x) (f b) < ε

Tactic:
tendsto_nhds

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
s : Set β
⊢ (∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, edist (f x) (f b) < ε) ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, edist (f x) (f b) < ε
Module: Mathlib.Analysis.Normed.Group.Defs

Goal state before:
pp: 𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝ : Group E
f : GroupSeminorm E
x y z : E
⊢ f (x⁻¹ * z) ≤ f (x⁻¹ * y) + f (y⁻¹ * z)

Tactic:
convert! map_mul_le_add f (x⁻¹ * y) (y⁻¹ * z) using 2; group

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
⊢ Tendsto f (𝓝 b) (𝓝 (f b)) ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, dist (f x) (f b) < ε

Tactic:
tendsto_nhds

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
⊢ (∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, dist (f x) (f b) < ε) ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, dist (f x) (f b) < ε
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
s : Set β
⊢ Tendsto f (𝓝[s] b) (𝓝 (f b)) ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, dist (f x) (f b) < ε

Tactic:
tendsto_nhds

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
s : Set β
⊢ (∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, dist (f x) (f b) < ε) ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, dist (f x) (f b) < ε
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
⊢ sSup (a • ∅) = a • sInf ∅

Tactic:
rw [smul_set_empty, Real.sSup_empty, Real.sInf_empty, smul_zero]

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

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

Tactic:
add_sub_cancel_left,

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

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

Tactic:
add_sub_cancel_left,

Goal state after:
x y : ℝ
⊢ Icc x y = Icc ((x + x) / 2) ((y + x) / 2 + (y - x) / 2)
Module: Mathlib.Topology.Order.IsLUB

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

Tactic:
rcases (ha.1 ha').eq_or_lt with (rfl | ha'a)

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

case inr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[≤] a, ¬(fun x ↦ x ∈ s) x
ha'a : a' < a
⊢ False
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: case neg
γ : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : ClosedIicTopology α
f : γ → α
inst✝ : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst✝, inst✝³] f
h : ¬BddAbove (range fun x ↦ f ↑x)
⊢ ⨆ s, f ↑s = ⨆ i, f i

Tactic:
suffices ¬ BddAbove (range f) by simp [ciSup_of_not_bddAbove, this, h]

Goal state after:
case neg
γ : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : ClosedIicTopology α
f : γ → α
inst✝ : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst✝, inst✝³] f
h : ¬BddAbove (range fun x ↦ f ↑x)
⊢ ¬BddAbove (range f)
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝² : Fintype β
inst✝¹ : (b : β) → PseudoMetricSpace (X b)
inst✝ : Nonempty β
x : (b : β) → X b
r : ℝ
hr : r ≤ 0
⊢ ball x r = Set.univ.pi fun b ↦ ball (x b) r

Tactic:
simp [ball_eq_empty.2 hr]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : Preorder α
h : ∀ {a b : α}, a ≤ b → IsCompact (Icc a b)
a b : α
hab : ¬a ≤ b
⊢ IsCompact (Icc a b)

Tactic:
by rw [Icc_eq_empty hab]; exact isCompact_empty

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

Goal state before:
pp: case mpr
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u
⊢ ∀ᶠ (m : β × β) in atTop ×ˢ atTop, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u

Tactic:
rcases h ε hε with ⟨N, hN⟩

Goal state after:
case mpr
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hab : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u
N : β
hN : ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
⊢ ∀ᶠ (m : β × β) in atTop ×ˢ atTop, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case inr
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst✝³] (s ∩ Icc a b)
ha : a ∈ s
h✝ : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := ⋯
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := ⋯
t₁_mem : t₁ ∈ Icc a b
t : α
ht : t ∈ Icc a t₁
h : t < t₁
c : α
cA : c ∈ A
tc : t < c
⊢ t ∈ Icc a c

Tactic:
exact ⟨ht.1, tc.le⟩

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

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

Tactic:
coe_nnnorm',

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