mathlib-initiative/mathlib-tactics huggingface dataset:
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
| k • 1

Tactic:
← algebraMap_eq_smul_one

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
| (algebraMap K A) k
Module: Mathlib.RingTheory.RamificationInertia.Ramification

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
q : Ideal S
r : Ideal T
inst✝⁵ : q.IsPrime
inst✝⁴ : r.IsPrime
inst✝³ : r.LiesOver q
inst✝² : Algebra (Localization.AtPrime q) (Localization.AtPrime r)
inst✝¹ : Localization.AtPrime.IsLiesOverAlgebra q r
inst✝ : Module.Flat (Localization.AtPrime q) (Localization.AtPrime r)
⊢ r.ramificationIdx R = q.ramificationIdx R * r.ramificationIdx S

Tactic:
by
  have : q.LiesOver (r.under R) := LiesOver.tower_bot r q (r.under R)
  let f := (Ideal.quotientEquivAlgOfEq (Localization.AtPrime r)
    (by rw [map_map, ← IsScalarTower.algebraMap_eq])).trans
      (Algebra.TensorProduct.quotIdealMapEquivTensorQuot (Localization.AtPrime r)
        ((r.under R).map (algebraMap R (Localization.AtPrime q))))
  rw [ramificationIdx_def, ramificationIdx_eq (r.under R), ramificationIdx_eq q,
    f.toLinearEquiv.length_eq, IsLocalRing.length_baseChange, ENat.toNat_mul,
    ← Localization.AtPrime.map_eq_maximalIdeal, map_map, ← IsScalarTower.algebraMap_eq]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
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
hr' : r * ∏ i ∈ s, b i ∣ r'
H : (IsScalarTower.toAlgHom R S (Away ((Algebra.ofId R S) r'))).range ≤ (awayMapₐ (Algebra.ofId R S) r').range
x : S
n : ℕ
y : Away r'
hy :
  (awayMap (Algebra.ofId R S).toRingHom r') y = (IsScalarTower.toAlgHom R S (Away ((Algebra.ofId R S) r'))).toRingHom x
⊢ ∃ a,
    (awayMap (algebraMap R S) r') a =
      IsLocalization.mk' (Away ((algebraMap R S) r')) x ⟨(fun x ↦ (algebraMap R S) r' ^ x) n, ⋯⟩

Tactic:
dsimp at hy

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
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
hr' : r * ∏ i ∈ s, b i ∣ r'
H : (IsScalarTower.toAlgHom R S (Away ((Algebra.ofId R S) r'))).range ≤ (awayMapₐ (Algebra.ofId R S) r').range
x : S
n : ℕ
y : Away r'
hy : (awayMap (algebraMap R S) r') y = (algebraMap S (Away ((algebraMap R S) r'))) x
⊢ ∃ a,
    (awayMap (algebraMap R S) r') a =
      IsLocalization.mk' (Away ((algebraMap R S) r')) x ⟨(fun x ↦ (algebraMap R S) r' ^ x) n, ⋯⟩
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_supp : {v | ¬↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0} = {v | v.asIdeal ∣ I}
⊢ {x | ¬↑((Associates.mk x.asIdeal).count (Associates.mk I).factors) = 0}.Finite

Tactic:
h_supp

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
h_supp : {v | ¬↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0} = {v | v.asIdeal ∣ I}
⊢ {v | v.asIdeal ∣ I}.Finite
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: a b r : ℝ≥0
h : a < b / r
hr : r = 0
⊢ False

Tactic:
simp [hr] at h

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

Goal state before:
pp: case refine_1
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
⊢ ⨅ r, f ↑r ≤ ⨅ q, f ↑↑q

pp: case refine_2
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
⊢ ⨅ q, f ↑↑q ≤ ⨅ r, f ↑r

Tactic:
· have : Nonempty { r' : ℚ // x < ↑r' } := by
      obtain ⟨r, hrx⟩ := exists_rat_gt x
      exact ⟨⟨r, hrx⟩⟩
    refine le_ciInf fun r => ?_
    obtain ⟨y, hxy, hyr⟩ := exists_rat_btwn r.prop
    refine ciInf_set_le hf (hxy.trans ?_)
    exact_mod_cast hyr

Goal state after:
case refine_2
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
⊢ ⨅ q, f ↑↑q ≤ ⨅ r, f ↑r
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
⊢ 0 + 0 = 0

Tactic:
zero_add

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

Goal state before:
pp: n : ℕ
⊢ (↑n).toReal = ↑n

Tactic:
← ENNReal.ofReal_natCast n,

Goal state after:
n : ℕ
⊢ (ENNReal.ofReal ↑n).toReal = ↑n
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝ : E
p q : GroupSeminorm E
x : E
⊢ ⨅ x_1, p x_1⁻¹ + q (x⁻¹ / x_1⁻¹) = ⨅ y, p y + q (x / y)

Tactic:
simp_rw [map_inv_eq_map p, ← inv_div', map_inv_eq_map q]

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

Goal state before:
pp: case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 0
⊢ (if y = 0 then 0 else 1) ≤ 0 + if y = 0 then 0 else 1

Tactic:
zero_add

Goal state after:
case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 0
⊢ (if y = 0 then 0 else 1) ≤ if y = 0 then 0 else 1
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 1
⊢ (if y = 1 then 0 else 1) ≤ 0 + if y = 1 then 0 else 1

Tactic:
zero_add

Goal state after:
case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 1
⊢ (if y = 1 then 0 else 1) ≤ if y = 1 then 0 else 1
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 0
⊢ (if 0 + y = 0 then 0 else 1) ≤ max 0 (if y = 0 then 0 else 1)

Tactic:
zero_add

Goal state after:
case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 0
⊢ (if y = 0 then 0 else 1) ≤ max 0 (if y = 0 then 0 else 1)
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

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

Tactic:
rw [← mem_ordConnectedComponent, ← ordConnectedComponent_ordConnectedProj, h,
      ordConnectedComponent_ordConnectedProj, self_mem_ordConnectedComponent]
    exact y.2

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

Goal state before:
pp: case inl
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ ↑x
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P ↑x ↑y
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P ↑x ⊤
neg_bot : ∀ x < 0, P ↑x ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ ↑x
bot_bot : P ⊥ ⊥
y : ℝ
hy : y < 0
⊢ P ⊥ ↑y

pp: case inr.inl
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ ↑x
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P ↑x ↑y
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P ↑x ⊤
neg_bot : ∀ x < 0, P ↑x ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ ↑x
bot_bot : P ⊥ ⊥
⊢ P ⊥ ↑0

pp: case inr.inr
P : EReal → EReal → Prop
top_top : P ⊤ ⊤
top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x
top_zero : P ⊤ 0
top_neg : ∀ x < 0, P ⊤ ↑x
top_bot : P ⊤ ⊥
pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤
pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥
zero_top : P 0 ⊤
coe_coe : ∀ (x y : ℝ), P ↑x ↑y
zero_bot : P 0 ⊥
neg_top : ∀ x < 0, P ↑x ⊤
neg_bot : ∀ x < 0, P ↑x ⊥
bot_top : P ⊥ ⊤
bot_pos : ∀ (x : ℝ), 0 < x → P ⊥ ↑x
bot_zero : P ⊥ 0
bot_neg : ∀ x < 0, P ⊥ ↑x
bot_bot : P ⊥ ⊥
y : ℝ
hy : 0 < y
⊢ P ⊥ ↑y

Tactic:
exacts [bot_neg y hy, bot_zero, bot_pos y hy]

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

Goal state before:
pp: a : ℝ≥0∞
h : a ≠ 0
⊢ a / 0 = ∞

Tactic:
by simp [div_eq_mul_inv, h]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ t ∈ c, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
hc₂ : s ⊆ ⋃₀ c
⊢ ∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, eball x δ ⊆ t

Tactic:
by
  rw [sUnion_eq_iUnion] at hc₂; simpa using lebesgue_number_lemma_of_emetric hs (by simpa) hc₂

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

Goal state before:
pp: case right
ι : Type u_1
E : Type u_2
inst✝² : Fintype ι
inst✝¹ : SeminormedGroup E
inst✝ : Nonempty ι
f : ι → E
⊢ ‖f‖ ∈ upperBounds (Set.range fun x ↦ ‖f x‖)

Tactic:
rintro - ⟨x, rfl⟩
    exact norm_le_pi_norm' f x

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed[inst✝¹] s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
⊢ ∃ x ∈ s, IsMinOn f s x

Tactic:
rcases (hasBasis_cocompact.inf_principal _).eventually_iff.1 hc with ⟨K, hK, hKf⟩

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed[inst✝¹] s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
K : Set β
hK : IsCompact K
hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x
⊢ ∃ x ∈ s, IsMinOn f s x
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 α := {t | t ∈ Icc a b ∧ Icc a t ⊆ s}
⊢ Icc a b ⊆ s

Tactic:
have a_mem : a ∈ A := ⟨left_mem_Icc.mpr hab, by simp [ha]⟩

Goal state after:
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 α := {t | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
⊢ Icc a b ⊆ s
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedCancelAddMonoid R
inst✝ : Archimedean R
f : α → ℕ
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto (fun x ↦ f x • r) l atTop

Tactic:
refine tendsto_atTop.mpr fun s => ?_
  obtain ⟨n : ℕ, hn : s ≤ n • r⟩ := Archimedean.arch s hr
  exact (tendsto_atTop.mp hf n).mono fun a ha => hn.trans (nsmul_le_nsmul_left hr.le ha)

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ (max (max (edist x y) (edist x z)) (edist y z)).toReal =
    max (max (edist x y).toReal (edist x z).toReal) (edist y z).toReal

Tactic:
ENNReal.toReal_max,

Goal state after:
α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ max (max (edist x y) (edist x z)).toReal (edist y z).toReal =
    max (max (edist x y).toReal (edist x z).toReal) (edist y z).toReal

case hr
α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ max (edist x y) (edist x z) ≠ ∞

case hp
α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ edist y z ≠ ∞
Module: Mathlib.Topology.Algebra.Order.Archimedean

Goal state before:
pp: case inr
G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
S : Subgroup G
hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε
h✝ : Nontrivial G
a b : G
hlt : a < b
g : G
hgS : g ∈ S
hg0 : 1 < g
hg : g < b / a
m : ℤ
hm : g ^ m ∈ Ioc a (a * g)
⊢ a * g < b

Tactic:
rwa [lt_div_iff_mul_lt'] at hg

Goal state after:
Module: Mathlib.Topology.Instances.Nat

Goal state before:
pp: case inl
x : ℕ
r : ℝ
hr : 0 ≤ r
⊢ closedBall x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊

pp: case inr
x : ℕ
r : ℝ
hr : r < 0
⊢ closedBall x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊

Tactic:
· rw [← preimage_closedBall, Real.closedBall_eq_Icc, preimage_Icc]
    positivity

Goal state after:
case inr
x : ℕ
r : ℝ
hr : r < 0
⊢ closedBall x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case inr
α : Type u_1
f : Filter α
inst✝ : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
l' : α
hl' : l' < l
u : α
hu : ∀ᶠ (x : α) in f, (fun x1 x2 ↦ x1 ≤ x2) x u
⊢ (fun x1 x2 ↦ x1 ≤ x2) l' u

Tactic:
obtain ⟨w, l_le_w, w_le_u⟩ := (freq_ge.and_eventually hu).exists

Goal state after:
case inr
α : Type u_1
f : Filter α
inst✝ : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
l' : α
hl' : l' < l
u : α
hu : ∀ᶠ (x : α) in f, (fun x1 x2 ↦ x1 ≤ x2) x u
w : α
l_le_w : l ≤ w
w_le_u : w ≤ u
⊢ l' ≤ u
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_5
R : Type u_6
inst✝⁴ : LinearOrder R
inst✝³ : Add R
f : Filter α
inst✝² : f.NeBot
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
u v : α → R
hu : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) f u
hv : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
⊢ IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f (u + v)

Tactic:
obtain ⟨U, hU⟩ := hu.eventually_ge
  obtain ⟨V, hV⟩ := hv.frequently_ge
  apply IsCoboundedUnder.of_frequently_ge (a := U + V)
  exact (hV.and_eventually hU).mono fun x hx ↦ add_le_add hx.2 hx.1

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

Goal state before:
pp: case inl
x y z : EReal
h : x < y
h' : z ≤ z
hbot : z ≠ ⊥
htop : z = ⊤ → z = ⊤ → x = ⊥
⊢ x + z < y + z

Tactic:
rcases eq_or_ne z ⊤ with (rfl | hz)

Goal state after:
case inl.inl
x y : EReal
h : x < y
h' : ⊤ ≤ ⊤
hbot : ⊤ ≠ ⊥
htop : ⊤ = ⊤ → ⊤ = ⊤ → x = ⊥
⊢ x + ⊤ < y + ⊤

case inl.inr
x y z : EReal
h : x < y
h' : z ≤ z
hbot : z ≠ ⊥
htop : z = ⊤ → z = ⊤ → x = ⊥
hz : z ≠ ⊤
⊢ x + z < y + z
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : CompleteLattice α
p : ι → Prop
s : ι → Set β
f : Filter β
u : β → α
hf : f.HasBasis p s
q : β → Prop
⊢ blimsup u f q = ⨅ i, ⨅ (_ : p i), ⨆ a ∈ s i, ⨆ (_ : q a), u a

Tactic:
by
  simp only [blimsup_eq_limsup, (hf.inf_principal _).limsup_eq_iInf_iSup, mem_inter_iff, iSup_and,
    mem_ofPred_eq]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
⊢ (limsup u f)ᶜ = liminf (compl ∘ u) f

Tactic:
simp only [limsup_eq_iInf_iSup, compl_iInf, compl_iSup, liminf_eq_iSup_iInf, Function.comp_apply]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
⊢ (liminf u f)ᶜ = limsup (compl ∘ u) f

Tactic:
simp only [limsup_eq_iInf_iSup, compl_iInf, compl_iSup, liminf_eq_iSup_iInf, Function.comp_apply]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
⊢ a \ limsup u f = liminf (fun b ↦ a \ u b) f

Tactic:
← compl_inj_iff

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
inst✝ : f.NeBot
a : α
⊢ (a \ limsup u f)ᶜ = (liminf (fun b ↦ a \ u b) f)ᶜ
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ a \ liminf u f = limsup (fun b ↦ a \ u b) f

Tactic:
← compl_inj_iff

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ (a \ liminf u f)ᶜ = (limsup (fun b ↦ a \ u b) f)ᶜ
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ bliminf s cofinite p = {x | {n | p n ∧ x ∉ s n}.Finite}

Tactic:
← compl_inj_iff

Goal state after:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ (bliminf s cofinite p)ᶜ = {x | {n | p n ∧ x ∉ s n}.Finite}ᶜ
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x : EReal
h : 0 < x
⊢ ⊥ * x = ⊥

Tactic:
rw [EReal.mul_comm]
  exact mul_bot_of_pos h

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

Goal state before:
pp: ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ b'
r✝ : α
hr✝ : ∀ s ≥ r✝, limsup (fun x ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r✝ ≤ b''
n : ι
r : α
hr : ∀ (b : α), r ≤ b → u n b ≤ b'
⊢ ∃ r, ∀ s ≥ r, u n s ≤ b''

Tactic:
exact ⟨r, fun s hs ↦ (hr s hs).trans hb''b.1⟩

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: case refine_1
β : Type u_2
L : SummationFilter β
h : ∀ (x : β), ∀ᶠ (s : Finset β) in L.filter, x ∈ s
s : Set (Finset β)
hs : s ∈ atTop
⊢ s ∈ L.filter

pp: case refine_2
β : Type u_2
L : SummationFilter β
h : L.filter ≤ atTop
b : β
⊢ ∀ᶠ (x : Finset β) in atTop, b ∈ x

Tactic:
· obtain ⟨t, ht⟩ := mem_atTop_sets.mp hs
    have := (Filter.biInter_finset_mem t).mpr fun b hb ↦ h b
    exact Filter.mem_of_superset this fun r hr ↦ ht r (by simpa using! hr)

Goal state after:
case refine_2
β : Type u_2
L : SummationFilter β
h : L.filter ≤ atTop
b : β
⊢ ∀ᶠ (x : Finset β) in atTop, b ∈ x
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
H : ∃ j, BddBelow (range fun i ↦ f ↑i)
⊢ liminf f v = ⨆ j, ⨅ i, f ↑i

Tactic:
rcases H with ⟨j0, hj0⟩

Goal state after:
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
⊢ liminf f v = ⨆ j, ⨅ i, f ↑i
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.coe.inl
hx : 0 ≤ ⊤
a : ℝ
ha : a < 0
⊢ (⊤ * ↑a).toENNReal = ⊤.toENNReal * (↑a).toENNReal

Tactic:
simp_all [le_of_lt, top_mul_of_neg (EReal.coe_neg'.mpr ha)]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
b : β
inst✝¹ : DecidablePred fun x ↦ x = b
a : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
b' : β
hb' : b' ≠ b
⊢ (if b' = b then a b' else 1) = 1

Tactic:
simp [hb']

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: G : Type u_2
inst✝⁴ : CommGroup G
inst✝³ : UniformSpace G
inst✝² : IsUniformGroup G
inst✝¹ : CompleteSpace G
inst✝ : T2Space G
f : ℤ → G
hf2 : Multipliable f
h1 : Multipliable fun n ↦ f ↑n
h2 : Multipliable fun n ↦ f (-↑n)
h3 : Multipliable fun n ↦ f ↑↑n
h4 : Multipliable fun n ↦ f (-↑↑n)
this : ∏' (n : ℕ), f ↑n * f (-↑n) = (∏' (n : ℤ), f n) * f 0
⊢ Multipliable ?m.133

Tactic:
simpa using h1.mul h2

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
⊢ ∀ (ib : Set Y), b ∉ ib ∧ IsClosed[inst✝¹] ib → ∃ ia, (a ∉ ia ∧ IsClosed[inst✝²] ia) ∧ ∀ x ∈ iaᶜ, f x ∈ ibᶜ

Tactic:
rintro s ⟨hbs, hsc⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : FrechetUrysohnSpace X
f : X → Y
a : X
b : Y
h : ∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 b)
s : Set Y
hbs : b ∉ s
hsc : IsClosed[inst✝¹] s
⊢ ∃ ia, (a ∉ ia ∧ IsClosed[inst✝²] ia) ∧ ∀ x ∈ iaᶜ, f x ∈ sᶜ