mathlib-initiative/mathlib-tactics huggingface dataset:
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 : GroupSeminorm E
f : F →* E
x : F
⊢ p (f x⁻¹) = p (f x)

Tactic:
by simp_rw [map_inv, map_inv_eq_map p]

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

Goal state before:
pp: a : ℝ≥0∞
⊢ 0 < a.toNNReal ↔ 0 < a ∧ a < ∞

Tactic:
induction a

Goal state after:
case top
a : ℝ≥0∞
⊢ 0 < ∞.toNNReal ↔ 0 < ∞ ∧ ∞ < ∞

case coe
a : ℝ≥0∞
x✝ : ℝ≥0
⊢ 0 < (↑x✝).toNNReal ↔ 0 < ↑x✝ ∧ ↑x✝ < ∞
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: a : ℝ≥0∞
⊢ a.toReal * 0 = 0

Tactic:
mul_zero

Goal state after:
a : ℝ≥0∞
⊢ 0 = 0
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
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
⊢ count K v I =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)

Tactic:
have hv : Irreducible (Associates.mk v.asIdeal) := by
    exact Associates.irreducible_mk.mpr v.irreducible

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
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ count K v I =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)
Module: Mathlib.Data.ENNReal.Operations

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

Tactic:
induction a

Goal state after:
case top
b : ℝ≥0
⊢ ∞.toReal - (↑b).toReal ≤ (∞ - ↑b).toReal

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

Goal state before:
pp: a : ℝ≥0∞
b : ℝ≥0
⊢ (a - ↑b).toNNReal = a.toNNReal - (↑b).toNNReal

Tactic:
induction a

Goal state after:
case top
b : ℝ≥0
⊢ (∞ - ↑b).toNNReal = ∞.toNNReal - (↑b).toNNReal

case coe
b x✝ : ℝ≥0
⊢ (↑x✝ - ↑b).toNNReal = (↑x✝).toNNReal - (↑b).toNNReal
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case pos
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 : FractionalIdeal R⁰ K
n : ℕ
h : count K v (I ^ n) = ↑n * count K v I
hI : I = 0
h_neg : ¬(I ^ n ≠ 0 ∧ I ≠ 0)
⊢ 0 = ↑(n + 1) * 0

Tactic:
mul_zero

Goal state after:
case pos
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 : FractionalIdeal R⁰ K
n : ℕ
h : count K v (I ^ n) = ↑n * count K v I
hI : I = 0
h_neg : ¬(I ^ n ≠ 0 ∧ I ≠ 0)
⊢ 0 = 0
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case inr
x : EReal
hx : x ≤ 0
⊢ ↑x.toENNReal = max 0 x

Tactic:
toENNReal_of_nonpos hx,

Goal state after:
case inr
x : EReal
hx : x ≤ 0
⊢ ↑0 = max 0 x
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0∞
⊢ a * 0 = 0

Tactic:
mul_zero

Goal state after:
a : ℝ≥0∞
⊢ 0 = 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c : ℝ≥0∞
hb0 : b ≠ 0 ∨ c ≠ ∞
hbt : b ≠ ∞ ∨ c ≠ 0
this : a * b⁻¹ ≤ c ↔ a ≤ c / b⁻¹
⊢ a / b ≤ c ↔ a ≤ c * b

Tactic:
by simpa [div_eq_mul_inv]

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

Goal state before:
pp: a : ℝ≥0∞
⊢ a⁻¹ * a ≤ 1

Tactic:
by simp [mul_comm]

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

Goal state before:
pp: a : ℝ≥0∞
⊢ a⁻¹ * a ≠ ∞

Tactic:
by simp [mul_comm]

Goal state after:
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
⊢ exps w * 0 = 0

Tactic:
mul_zero

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 → ℤ
w : HeightOneSpectrum R
hw : w ∈ fun i ↦ i = v → False
⊢ 0 = 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case ofNat.zero
⊢ 0 ^ Int.ofNat 0 = if Int.ofNat 0 = 0 then 1 else if 0 < Int.ofNat 0 then 0 else ∞

Tactic:
simp [-Nat.cast_add, -Int.natCast_add]

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

Goal state before:
pp: case ofNat.succ
n : ℕ
⊢ 0 ^ Int.ofNat (n + 1) = if Int.ofNat (n + 1) = 0 then 1 else if 0 < Int.ofNat (n + 1) then 0 else ∞

Tactic:
simp [-Nat.cast_add, -Int.natCast_add]

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

Goal state before:
pp: case negSucc
n : ℕ
⊢ 0 ^ Int.negSucc n = if Int.negSucc n = 0 then 1 else if 0 < Int.negSucc n then 0 else ∞

Tactic:
simp [-Nat.cast_add, -Int.natCast_add]

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

Goal state before:
pp: case ofNat.zero
⊢ ∞ ^ Int.ofNat 0 = if Int.ofNat 0 = 0 then 1 else if 0 < Int.ofNat 0 then ∞ else 0

Tactic:
simp [-Nat.cast_add, -Int.natCast_add]

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

Goal state before:
pp: case ofNat.succ
n : ℕ
⊢ ∞ ^ Int.ofNat (n + 1) = if Int.ofNat (n + 1) = 0 then 1 else if 0 < Int.ofNat (n + 1) then ∞ else 0

Tactic:
simp [-Nat.cast_add, -Int.natCast_add]

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

Goal state before:
pp: case negSucc
n : ℕ
⊢ ∞ ^ Int.negSucc n = if Int.negSucc n = 0 then 1 else if 0 < Int.negSucc n then ∞ else 0

Tactic:
simp [-Nat.cast_add, -Int.natCast_add]

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

Goal state before:
pp: case inr.inl.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
i : ι
hi : f i = 0
⊢ ∞ * 0 = 0

pp: case inr.inl.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
i : ι
hi : f i = 0
⊢ ∀ (b : ℝ≥0∞), ⊥ < b → ∃ i, ∞ * f i < b

pp: case inr.inl.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
i : ι
hi : f i = 0
⊢ ∀ (b : ℝ≥0∞), ⊥ < b → ∃ i, f i < b

Tactic:
mul_zero

Goal state after:
case inr.inl.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
i : ι
hi : f i = 0
⊢ 0 = 0

case inr.inl.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
i : ι
hi : f i = 0
⊢ ∀ (b : ℝ≥0∞), ⊥ < b → ∃ i, ∞ * f i < b

case inr.inl.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
i : ι
hi : f i = 0
⊢ ∀ (b : ℝ≥0∞), ⊥ < b → ∃ i, f i < b
Module: Mathlib.Analysis.Normed.Group.Defs

Goal state before:
pp: case a
𝓕 : 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✝² : Norm E
inst✝¹ : Group E
inst✝ : PseudoMetricSpace E
h₁ : ∀ (x : E), ‖x‖ = dist 1 x
h₂ : ∀ (x y z : E), dist x y ≤ dist (z * x) (z * y)
x y : E
⊢ dist 1 (x⁻¹ * y) ≤ dist x y

Tactic:
simpa only [mul_inv_cancel, mul_one, ← mul_assoc, one_mul] using h₂ 1 (x⁻¹ * y) x

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

Goal state before:
pp: case a
𝓕 : 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✝² : Norm E
inst✝¹ : Group E
inst✝ : PseudoMetricSpace E
h₁ : ∀ (x : E), ‖x‖ = dist 1 x
h₂ : ∀ (x y z : E), dist (z * x) (z * y) ≤ dist x y
x y : E
⊢ dist x y ≤ dist 1 (x⁻¹ * y)

Tactic:
simpa only [mul_inv_cancel, mul_one, ← mul_assoc, one_mul] using h₂ 1 (x⁻¹ * y) x

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
h : y ∈ ball x (ε / 2)
⊢ dist y x ≤ ε / 2

Tactic:
exact le_of_lt h

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
⊢ BoundedSpace α ↔ ∃ C, ∀ (a b : α), nndist a b ≤ C

Tactic:
rw [← isBounded_univ, Metric.isBounded_iff_nndist]
  simp

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ), 0 < ε → ∃ x, p x ∧ f x ≤ ε
⊢ (𝓤 α).HasBasis p fun x ↦ {p | dist p.1 p.2 ≤ f x}

Tactic:
by
  refine ⟨fun s => uniformity_basis_dist.mem_iff.trans ?_⟩
  constructor
  · rintro ⟨ε, ε₀, hε⟩
    rcases exists_between ε₀ with ⟨ε', hε'⟩
    rcases hf ε' hε'.1 with ⟨i, hi, H⟩
    exact ⟨i, hi, fun x (hx : _ ≤ _) => hε <| lt_of_le_of_lt (le_trans hx H) hε'.2⟩
  · exact fun ⟨i, hi, H⟩ => ⟨f i, hf₀ i hi, fun x (hx : _ < _) => H (mem_ofPred.2 hx.le)⟩

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 : Type u_3
e : PseudoEMetricSpace X
dist : X → X → ℝ
dist_nonneg : ∀ (x y : X), 0 ≤ dist x y
h : ∀ (x y : X), edist x y = ENNReal.ofReal (dist x y)
x : X
⊢ dist x x = 0

Tactic:
by simpa [h, (dist_nonneg _ _).ge_iff_eq', -edist_self] using edist_self x

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
s : Finset (HeightOneSpectrum R) := ⋯
this : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := ⋯
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
⊢ a p' ∈ J * ∏ q ∈ s, q.asIdeal

Tactic:
have := IsDedekindDomain.inf_pow_eq_prod_of_prime s (fun i ↦ i.asIdeal) (fun _ ↦ 1)
    (fun i _ ↦ i.prime) (fun i _ j _ e ↦ mt HeightOneSpectrum.ext e)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this✝ : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : (s.inf fun i ↦ i.asIdeal ^ 1) = ∏ i ∈ s, i.asIdeal ^ 1
⊢ a p' ∈ J * ∏ q ∈ s, q.asIdeal
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ closure[inst✝³] (Ico a b) = Icc a b

Tactic:
by
  apply Subset.antisymm
  · exact closure_minimal Ico_subset_Icc_self isClosed_Icc
  · apply Subset.trans _ (closure_mono Ioo_subset_Ico_self)
    rw [closure_Ioo hab]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMaxOrder α
a b x : α
⊢ Ioc a b ∈ 𝓝 x ↔ x ∈ Ioo a b

Tactic:
by
  rw [← interior_Ioc, mem_interior_iff_mem_nhds]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
⊢ {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}.Countable

Tactic:
have : ∀ c ∈ t, ∃ x, ∃ y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c := fun c hc ↦ hc

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
this : ∀ c ∈ t, ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c
⊢ {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}.Countable
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
H : (x '' t).Countable
⊢ InjOn x t

Tactic:
intro c

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
H : (x '' t).Countable
c : β
⊢ c ∈ t → ∀ ⦃x₂ : β⦄, x₂ ∈ t → x c = x x₂ → c = x₂
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
⊢ ∀ a ∈ t, ∀ a_2 ∈ t, x a ≠ x a_2 → Disjoint (Ioo (x a) (y (f (x a)))) (Ioo (x a_2) (y (f (x a_2))))

Tactic:
intro c

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
c : β
⊢ c ∈ t → ∀ a ∈ t, x c ≠ x a → Disjoint (Ioo (x c) (y (f (x c)))) (Ioo (x a) (y (f (x a))))
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 y : α
h_nonempty : (Ioo x y).Nonempty
Mf : MonotoneOn f (Ioo x y)
h_bdd : BddBelow (f '' Ioo x y)
⊢ Tendsto f (𝓝[>] x) (𝓝 (sInf (f '' Ioo x y)))

Tactic:
refine tendsto_order.2 ⟨fun l hl => ?_, fun m hm => ?_⟩
  · rcases h_nonempty with ⟨p, hy, hx⟩
    filter_upwards [Ioo_mem_nhdsGT (hy.trans hx)] with w hw
    exact hl.trans_le <| csInf_le h_bdd (mem_image_of_mem _ hw)
  · obtain ⟨z, ⟨xz, zy⟩, zm⟩ : ∃ a : α, a ∈ Ioo x y ∧ f a < m := by
      simpa [mem_image, exists_prop, exists_exists_and_eq_and] using
        exists_lt_of_csInf_lt (h_nonempty.image _) hm
    filter_upwards [Ioo_mem_nhdsGT xz] with w hw
    exact (Mf ⟨hw.1, hw.2.trans zy⟩ ⟨xz, zy⟩ hw.2.le).trans_lt zm

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
v : HeightOneSpectrum R
I J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
H' : I'.divMod I J' = 0
⊢ J' = I'

Tactic:
by simpa [H'] using divMod_spec h' hJ' hI

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

Goal state before:
pp: case inr.refine_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst✝³] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z < f x y
⊢ ∀ᶠ (b : γ) in 𝓝 x, z < sSup (f b '' K)

pp: case inr.refine_2
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst✝³] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z > f x y
⊢ ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < z

Tactic:
· refine (this.1 z hz).mono fun x' hx' =>
      hx'.trans_le <| le_csSup ?_ <| mem_image_of_mem (f x') hyK
    exact hK.bddAbove_image (hf.comp <| .prodMk_right x').continuousOn

Goal state after:
case inr.refine_2
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous[instTopologicalSpaceProd, inst✝³] ↿f
h0K : K.Nonempty
x : γ
y : β
hyK : y ∈ K
h2y : sSup (f x '' K) = f x y
hy : ∀ y_1 ∈ K, f x y_1 ≤ f x y
this : (∀ a' < f x y, ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ a' > f x y, ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z > f x y
⊢ ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < z
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: α : Type u_2
E : Type u_5
inst✝ : SeminormedGroup E
f : α → E
l : Filter α
⊢ (∀ ε > 0, ∀ᶠ (x : α) in l, dist (f x) 1 < ε) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε

Tactic:
by simp only [dist_one_right]

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

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

Tactic:
mem_closedBall_iff_norm''

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a : E
r : ℝ
x : E
⊢ x ∈ {x | x / a ∈ closedBall 1 r} ↔ ‖x / a‖ ≤ r
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ a * b ∈ closedBall a r ↔ ‖b‖ ≤ r

Tactic:
mem_closedBall_iff_norm''

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ ‖a * b / a‖ ≤ r ↔ ‖b‖ ≤ r
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

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

Tactic:
by
  refine tendsto_atTop.2 fun b => ?_
  obtain ⟨n : ℕ, hn : 1 ≤ n • r⟩ := Archimedean.arch 1 hr
  rw [nsmul_eq_mul'] at hn
  filter_upwards [tendsto_atTop.1 hf (n * max b 0)] with x hx
  calc
    b ≤ 1 * max b 0 := by
    { rw [one_mul]
      exact le_max_left _ _ }
    _ ≤ r * n * max b 0 := by gcongr
    _ = r * (n * max b 0) := by rw [mul_assoc]
    _ ≤ r * f x := by gcongr

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

Goal state before:
pp: m n : ℤ
⊢ dist m n = ↑|m - n|

Tactic:
rw [dist_eq]

Goal state after:
m n : ℤ
⊢ |↑m - ↑n| = ↑|m - n|
Module: Mathlib.Topology.Instances.Int

Goal state before:
pp: m n : ℤ
hne : m ≠ n
⊢ 1 ≤ dist m n

Tactic:
rw [dist_eq]

Goal state after:
m n : ℤ
hne : m ≠ n
⊢ 1 ≤ |↑m - ↑n|
Module: Mathlib.Topology.Instances.Int

Goal state before:
pp: m n : ℤ
hne : m ≠ n
⊢ m - n ≠ 0

Tactic:
sub_ne_zero

Goal state after:
m n : ℤ
hne : m ≠ n
⊢ m ≠ n
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
inst✝¹ : PseudoMetricSpace β
inst✝ : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝³] f
x₀ : β
h : Bornology.IsBounded {x | f x ≤ f x₀}
⊢ IsCompact {x | f x₀ < f x}ᶜ

Tactic:
simp only [Set.compl_ofPred, not_lt]

Goal state after:
α : Type u_3
β : Type u_4
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
inst✝¹ : PseudoMetricSpace β
inst✝ : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝³] f
x₀ : β
h : Bornology.IsBounded {x | f x ≤ f x₀}
⊢ IsCompact {a | f a ≤ f x₀}
Module: Mathlib.Topology.Bornology.Real

Goal state before:
pp: r : ℝ
⊢ BddAbove (closedBall 0 r)

Tactic:
by
  obtain hr | hr := le_or_gt 0 r <;> simp [closedBall_zero_eq_Icc, *]

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

Goal state before:
pp: α : Type u_1
s : Finset α
hs : s.Nonempty
f g : α → ℝ≥0∞
Hlt : ∀ i ∈ s, f i < g i
⊢ ∑ i ∈ s, f i < ∑ i ∈ s, g i

Tactic:
by
  induction hs using Finset.Nonempty.cons_induction with
  | singleton => simp [Hlt _ (Finset.mem_singleton_self _)]
  | cons _ _ _ _ ih =>
    simp only [Finset.sum_cons, forall_mem_cons] at Hlt ⊢
    exact ENNReal.add_lt_add Hlt.1 (ih Hlt.2)

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map u f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a
⊢ ∀ (a : β), (∀ᶠ (x : β) in map (fun a ↦ max (u a) (v a)) f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a

Tactic:
intro c

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map u f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a
c : β
⊢ (∀ᶠ (x : β) in map (fun a ↦ max (u a) (v a)) f, (fun x1 x2 ↦ x1 ≤ x2) x c) → (fun x1 x2 ↦ x1 ≤ x2) b c
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a
⊢ ∀ (a : β), (∀ᶠ (x : β) in map (fun a ↦ max (u a) (v a)) f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a

Tactic:
intro c

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) b a
c : β
⊢ (∀ᶠ (x : β) in map (fun a ↦ max (u a) (v a)) f, (fun x1 x2 ↦ x1 ≤ x2) x c) → (fun x1 x2 ↦ x1 ≤ x2) b c