harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
theorem ediam_image_le (hf : LipschitzWith K f) (s : Set α) :
    EMetric.diam (f '' s) ≤ K * EMetric.diam s

Proof state:
case h
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
s : Set α
⊢ ∀ x ∈ f '' s, ∀ y ∈ f '' s, edist x y ≤ ↑K * diam s

Tactic:
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩

Result:
case h.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
s : Set α
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ edist (f x) (f y) ≤ ↑K * diam s

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
s : Set α
⊢ diam (f '' s) ≤ ↑K * diam s

Tactic:
apply EMetric.diam_le

Result:
case h
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
s : Set α
⊢ ∀ x ∈ f '' s, ∀ y ∈ f '' s, edist x y ≤ ↑K * diam s

Proof state:
case h.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
s : Set α
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ edist (f x) (f y) ≤ ↑K * diam s

Tactic:
exact hf.edist_le_mul_of_le (EMetric.edist_le_diam_of_mem hx hy)

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
lemma Ici_eq_singleton_iff_isTop {x : α} : (Ici x = {x}) ↔ IsTop x

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
x : α
h : IsTop x
y : α
⊢ y ∈ Ici x ↔ y ∈ {x}

Tactic:
simp [(h y).ge_iff_eq]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
x : α
⊢ Ici x = {x} ↔ IsTop x

Tactic:
refine ⟨fun h y ↦ ?_, fun h ↦ by ext y; simp [(h y).ge_iff_eq]⟩

Result:
α : Type u_1
inst✝ : LinearOrder α
x : α
h : Ici x = {x}
y : α
⊢ y ≤ x

Proof state:
α : Type u_1
inst✝ : LinearOrder α
x : α
h : Ici x = {x}
y : α
H : x < y
⊢ False

Tactic:
have : y ∈ Ici x := H.le

Result:
α : Type u_1
inst✝ : LinearOrder α
x : α
h : Ici x = {x}
y : α
H : x < y
this : y ∈ Ici x
⊢ False

Proof state:
α : Type u_1
inst✝ : LinearOrder α
x : α
h : Ici x = {x}
y : α
⊢ y ≤ x

Tactic:
by_contra! H

Result:
α : Type u_1
inst✝ : LinearOrder α
x : α
h : Ici x = {x}
y : α
H : x < y
⊢ False

Proof state:
α : Type u_1
inst✝ : LinearOrder α
x : α
h : Ici x = {x}
y : α
H : x < y
this : y ∈ Ici x
⊢ False

Tactic:
rw [h, mem_singleton_iff] at this

Result:
α : Type u_1
inst✝ : LinearOrder α
x : α
h : Ici x = {x}
y : α
H : x < y
this : y = x
⊢ False

Proof state:
α : Type u_1
inst✝ : LinearOrder α
x : α
h : IsTop x
⊢ Ici x = {x}

Tactic:
ext y

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
x : α
h : IsTop x
y : α
⊢ y ∈ Ici x ↔ y ∈ {x}

Proof state:
α : Type u_1
inst✝ : LinearOrder α
x : α
h : Ici x = {x}
y : α
H : x < y
this : y = x
⊢ False

Tactic:
exact lt_irrefl y (this.le.trans_lt H)

Result:
no goals
-- Mathlib/Probability/Martingale/BorelCantelli.lean
theorem stoppedValue_stoppedValue_leastGE (f : ℕ → Ω → ℝ) (π : Ω → ℕ) (r : ℝ) {n : ℕ}
    (hπn : ∀ ω, π ω ≤ n) : stoppedValue (fun i => stoppedValue f (leastGE f r i)) π =
      stoppedValue (stoppedProcess f (leastGE f r n)) π

Proof state:
case h
Ω : Type u_1
f : ℕ → Ω → ℝ
π : Ω → ℕ
r : ℝ
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
ω : Ω
⊢ stoppedValue (fun i => stoppedValue f (leastGE f r i)) π ω = stoppedValue (stoppedProcess f (leastGE f r n)) π ω

Tactic:
simp (config := { unfoldPartialApp := true }) only [stoppedProcess, stoppedValue]

Result:
case h
Ω : Type u_1
f : ℕ → Ω → ℝ
π : Ω → ℕ
r : ℝ
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
ω : Ω
⊢ f (leastGE f r (π ω) ω) ω = f (π ω ⊓ leastGE f r n ω) ω

Proof state:
Ω : Type u_1
f : ℕ → Ω → ℝ
π : Ω → ℕ
r : ℝ
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
⊢ stoppedValue (fun i => stoppedValue f (leastGE f r i)) π = stoppedValue (stoppedProcess f (leastGE f r n)) π

Tactic:
ext1 ω

Result:
case h
Ω : Type u_1
f : ℕ → Ω → ℝ
π : Ω → ℕ
r : ℝ
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
ω : Ω
⊢ stoppedValue (fun i => stoppedValue f (leastGE f r i)) π ω = stoppedValue (stoppedProcess f (leastGE f r n)) π ω

Proof state:
case h
Ω : Type u_1
f : ℕ → Ω → ℝ
π : Ω → ℕ
r : ℝ
n : ℕ
hπn : ∀ (ω : Ω), π ω ≤ n
ω : Ω
⊢ f (leastGE f r (π ω) ω) ω = f (π ω ⊓ leastGE f r n ω) ω

Tactic:
rw [leastGE_eq_min _ _ _ hπn]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Abs.lean
theorem abs_sub_le_of_nonneg_of_le {a b n : α} (a_nonneg : 0 ≤ a) (a_le_n : a ≤ n)
    (b_nonneg : 0 ≤ b) (b_le_n : b ≤ n) : |a - b| ≤ n

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b n : α
a_nonneg : 0 ≤ a
a_le_n : a ≤ n
b_nonneg : 0 ≤ b
b_le_n : b ≤ n
⊢ |a - b| ≤ n

Tactic:
rw [abs_sub_le_iff, sub_le_iff_le_add, sub_le_iff_le_add]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b n : α
a_nonneg : 0 ≤ a
a_le_n : a ≤ n
b_nonneg : 0 ≤ b
b_le_n : b ≤ n
⊢ a ≤ n + b ∧ b ≤ n + a

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b n : α
a_nonneg : 0 ≤ a
a_le_n : a ≤ n
b_nonneg : 0 ≤ b
b_le_n : b ≤ n
⊢ a ≤ n + b ∧ b ≤ n + a

Tactic:
exact ⟨le_add_of_le_of_nonneg a_le_n b_nonneg, le_add_of_le_of_nonneg b_le_n a_nonneg⟩

Result:
no goals
-- Mathlib/AlgebraicGeometry/ValuativeCriterion.lean
/-- The **valuative criterion** for universally closed morphisms. -/
@[stacks 01KF]
lemma UniversallyClosed.eq_valuativeCriterion :
    @UniversallyClosed = ValuativeCriterion.Existence ⊓ @QuasiCompact

Proof state:
⊢ @UniversallyClosed = ValuativeCriterion.Existence ⊓ @QuasiCompact

Tactic:
rw [universallyClosed_eq_universallySpecializing, ValuativeCriterion.Existence.eq]

Result:
no goals
-- Mathlib/Topology/Instances/RatLemmas.lean
theorem not_countably_generated_cocompact : ¬IsCountablyGenerated (cocompact ℚ)

Proof state:
case intro
H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hx : Tendsto x atTop (cocompact ℚ) ∧ Tendsto x atTop (𝓝 0)
⊢ False

Tactic:
rcases hx with ⟨hxc, hx0⟩

Result:
case intro.intro
H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hxc : Tendsto x atTop (cocompact ℚ)
hx0 : Tendsto x atTop (𝓝 0)
⊢ False

Proof state:
case intro.intro
H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hxc : Tendsto x atTop (cocompact ℚ)
hx0 : Tendsto x atTop (𝓝 0)
⊢ False

Tactic:
obtain ⟨n, hn⟩ : ∃ n : ℕ, x n ∉ insert (0 : ℚ) (range x) :=
  (hxc.eventually hx0.isCompact_insert_range.compl_mem_cocompact).exists

Result:
case intro.intro.intro
H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hxc : Tendsto x atTop (cocompact ℚ)
hx0 : Tendsto x atTop (𝓝 0)
n : ℕ
hn : x n ∉ insert 0 (range x)
⊢ False

Proof state:
case intro
H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hx : Tendsto x atTop (cocompact ℚ ⊓ 𝓝 0)
⊢ False

Tactic:
rw [tendsto_inf] at hx

Result:
case intro
H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hx : Tendsto x atTop (cocompact ℚ) ∧ Tendsto x atTop (𝓝 0)
⊢ False

Proof state:
H : (cocompact ℚ).IsCountablyGenerated
⊢ False

Tactic:
rcases exists_seq_tendsto (cocompact ℚ ⊓ 𝓝 0) with ⟨x, hx⟩

Result:
case intro
H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hx : Tendsto x atTop (cocompact ℚ ⊓ 𝓝 0)
⊢ False

Proof state:
case intro.intro.intro
H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hxc : Tendsto x atTop (cocompact ℚ)
hx0 : Tendsto x atTop (𝓝 0)
n : ℕ
hn : x n ∉ insert 0 (range x)
⊢ False

Tactic:
exact hn (Or.inr ⟨n, rfl⟩)

Result:
no goals

Proof state:
⊢ ¬(cocompact ℚ).IsCountablyGenerated

Tactic:
intro H

Result:
H : (cocompact ℚ).IsCountablyGenerated
⊢ False
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nmul_nadd_le {a' b' : Ordinal} (ha : a' ≤ a) (hb : b' ≤ b) :
    a' ⨳ b ♯ a ⨳ b' ≤ a ⨳ b ♯ a' ⨳ b'

Proof state:
a b a' b' : Ordinal.{u}
ha : a' ≤ a
hb : b' ≤ b
⊢ a' ⨳ b ♯ a ⨳ b' ≤ a ⨳ b ♯ a' ⨳ b'

Tactic:
rcases lt_or_eq_of_le ha with (ha | rfl)

Result:
case inl
a b a' b' : Ordinal.{u}
ha✝ : a' ≤ a
hb : b' ≤ b
ha : a' < a
⊢ a' ⨳ b ♯ a ⨳ b' ≤ a ⨳ b ♯ a' ⨳ b'

case inr
b a' b' : Ordinal.{u}
hb : b' ≤ b
ha : a' ≤ a'
⊢ a' ⨳ b ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a' ⨳ b'

Proof state:
case inr
b a' b' : Ordinal.{u}
hb : b' ≤ b
ha : a' ≤ a'
⊢ a' ⨳ b ♯ a' ⨳ b' ≤ a' ⨳ b ♯ a' ⨳ b'

Tactic:
exact le_rfl

Result:
no goals

Proof state:
case inl
a b a' b' : Ordinal.{u}
ha✝ : a' ≤ a
hb : b' ≤ b
ha : a' < a
⊢ a' ⨳ b ♯ a ⨳ b' ≤ a ⨳ b ♯ a' ⨳ b'

Tactic:
rcases lt_or_eq_of_le hb with (hb | rfl)

Result:
case inl.inl
a b a' b' : Ordinal.{u}
ha✝ : a' ≤ a
hb✝ : b' ≤ b
ha : a' < a
hb : b' < b
⊢ a' ⨳ b ♯ a ⨳ b' ≤ a ⨳ b ♯ a' ⨳ b'

case inl.inr
a a' b' : Ordinal.{u}
ha✝ : a' ≤ a
ha : a' < a
hb : b' ≤ b'
⊢ a' ⨳ b' ♯ a ⨳ b' ≤ a ⨳ b' ♯ a' ⨳ b'

Proof state:
case inl.inl
a b a' b' : Ordinal.{u}
ha✝ : a' ≤ a
hb✝ : b' ≤ b
ha : a' < a
hb : b' < b
⊢ a' ⨳ b ♯ a ⨳ b' ≤ a ⨳ b ♯ a' ⨳ b'

Tactic:
exact (nmul_nadd_lt ha hb).le

Result:
no goals

Proof state:
case inl.inr
a a' b' : Ordinal.{u}
ha✝ : a' ≤ a
ha : a' < a
hb : b' ≤ b'
⊢ a' ⨳ b' ♯ a ⨳ b' ≤ a ⨳ b' ♯ a' ⨳ b'

Tactic:
rw [nadd_comm]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
lemma hausdorffMeasure_of_finrank_lt [MeasurableSpace E] [BorelSpace E] {d : ℝ}
    (hd : finrank ℝ E < d) : (μH[d] : Measure E) = 0

Proof state:
case intro
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ≥0
hd : ↑(finrank ℝ E) < ↑d
⊢ μH[↑d] univ = 0

Tactic:
apply hausdorffMeasure_of_dimH_lt

Result:
case intro.h
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ≥0
hd : ↑(finrank ℝ E) < ↑d
⊢ dimH univ < ↑d

Proof state:
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ
hd : ↑(finrank ℝ E) < d
⊢ μH[d] = 0

Tactic:
lift d to ℝ≥0 using (Nat.cast_nonneg _).trans hd.le

Result:
case intro
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ≥0
hd : ↑(finrank ℝ E) < ↑d
⊢ μH[↑d] = 0

Proof state:
case intro
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ≥0
hd : ↑(finrank ℝ E) < ↑d
⊢ μH[↑d] = 0

Tactic:
rw [← measure_univ_eq_zero]

Result:
case intro
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ≥0
hd : ↑(finrank ℝ E) < ↑d
⊢ μH[↑d] univ = 0

Proof state:
case intro.h
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ≥0
hd : ↑(finrank ℝ E) < ↑d
⊢ dimH univ < ↑d

Tactic:
rw [dimH_univ_eq_finrank]

Result:
case intro.h
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ≥0
hd : ↑(finrank ℝ E) < ↑d
⊢ ↑(finrank ℝ E) < ↑d

Proof state:
case intro.h
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
d : ℝ≥0
hd : ↑(finrank ℝ E) < ↑d
⊢ ↑(finrank ℝ E) < ↑d

Tactic:
exact mod_cast hd

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem finite_setOf_isRoot {p : R[X]} (hp : p ≠ 0) : Set.Finite { x | IsRoot p x }

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ 0
⊢ {x | p.IsRoot x}.Finite

Tactic:
classical
simpa only [← Finset.setOf_mem, Multiset.mem_toFinset, mem_roots hp]
  using p.roots.toFinset.finite_toSet

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ 0
⊢ {x | p.IsRoot x}.Finite

Tactic:
simpa only [← Finset.setOf_mem, Multiset.mem_toFinset, mem_roots hp]
  using p.roots.toFinset.finite_toSet

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldl_hom (f : α₁ → α₂) (g₁ : α₁ → β → α₁) (g₂ : α₂ → β → α₂) (l : Vector β n) (init : α₁)
    (H : ∀ x y, g₂ (f x) y = f (g₁ x y)) : l.foldl g₂ (f init) = f (l.foldl g₁ init)

Proof state:
case mk
α₁ : Type u_1
α₂ : Type u_2
β : Type u_3
f : α₁ → α₂
g₁ : α₁ → β → α₁
g₂ : α₂ → β → α₂
init : α₁
H : ∀ (x : α₁) (y : β), g₂ (f x) y = f (g₁ x y)
l : Array β
⊢ Array.foldl g₂ (f init) l = f (Array.foldl g₁ init l)

Tactic:
rw [Array.foldl_hom _ _ _ _ _ H]

Result:
no goals

Proof state:
case mk
α₁ : Type u_1
α₂ : Type u_2
β : Type u_3
f : α₁ → α₂
g₁ : α₁ → β → α₁
g₂ : α₂ → β → α₂
init : α₁
H : ∀ (x : α₁) (y : β), g₂ (f x) y = f (g₁ x y)
l : Array β
⊢ foldl g₂ (f init) { toArray := l, size_toArray := ⋯ } = f (foldl g₁ init { toArray := l, size_toArray := ⋯ })

Tactic:
simp

Result:
case mk
α₁ : Type u_1
α₂ : Type u_2
β : Type u_3
f : α₁ → α₂
g₁ : α₁ → β → α₁
g₂ : α₂ → β → α₂
init : α₁
H : ∀ (x : α₁) (y : β), g₂ (f x) y = f (g₁ x y)
l : Array β
⊢ Array.foldl g₂ (f init) l = f (Array.foldl g₁ init l)

Proof state:
α₁ : Type u_1
α₂ : Type u_2
β : Type u_3
n : Nat
f : α₁ → α₂
g₁ : α₁ → β → α₁
g₂ : α₂ → β → α₂
l : Vector β n
init : α₁
H : ∀ (x : α₁) (y : β), g₂ (f x) y = f (g₁ x y)
⊢ foldl g₂ (f init) l = f (foldl g₁ init l)

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α₁ : Type u_1
α₂ : Type u_2
β : Type u_3
f : α₁ → α₂
g₁ : α₁ → β → α₁
g₂ : α₂ → β → α₂
init : α₁
H : ∀ (x : α₁) (y : β), g₂ (f x) y = f (g₁ x y)
l : Array β
⊢ foldl g₂ (f init) { toArray := l, size_toArray := ⋯ } = f (foldl g₁ init { toArray := l, size_toArray := ⋯ })
-- Mathlib/Topology/Order/PartialSups.lean
protected lemma ContinuousWithinAt.partialSups (hf : ∀ k ≤ n, ContinuousWithinAt (f k) s x) :
    ContinuousWithinAt (partialSups f n) s x

Proof state:
L : Type u_1
inst✝³ : SemilatticeSup L
inst✝² : TopologicalSpace L
inst✝¹ : ContinuousSup L
X : Type u_2
inst✝ : TopologicalSpace X
f : ℕ → X → L
n : ℕ
s : Set X
x : X
hf : ∀ k ≤ n, ContinuousWithinAt (f k) s x
⊢ ContinuousWithinAt ((partialSups f) n) s x

Tactic:
simpa only [← Pi.partialSups_apply] using ContinuousWithinAt.partialSups_apply hf

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.eq_bot_iff (hl : l.HasBasis p s) : l = ⊥ ↔ ∃ i, p i ∧ s i = ∅ :=
  not_iff_not.1 <| neBot_iff.symm.trans <|
    hl.neBot_iff.trans <| by simp only [not_exists, not_and, nonempty_iff_ne_empty]

Proof state:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
⊢ (∀ {i : ι}, p i → (s i).Nonempty) ↔ ¬∃ i, p i ∧ s i = ∅

Tactic:
simp only [not_exists, not_and, nonempty_iff_ne_empty]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma div_lt_div₀' (hac : a ≤ c) (hdb : d < b) (hc : 0 < c) (hd : 0 < d) : a / b < c / d

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : LinearOrder G₀
inst✝² : ZeroLEOneClass G₀
a b c d : G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : MulPosStrictMono G₀
hac : a ≤ c
hdb : d < b
hc : 0 < c
hd : 0 < d
⊢ a * b⁻¹ < c * d⁻¹

Tactic:
exact mul_lt_mul' hac ((inv_lt_inv₀ (hd.trans hdb) hd).2 hdb)
  (inv_nonneg.2 <| hd.le.trans hdb.le) hc

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : LinearOrder G₀
inst✝² : ZeroLEOneClass G₀
a b c d : G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : MulPosStrictMono G₀
hac : a ≤ c
hdb : d < b
hc : 0 < c
hd : 0 < d
⊢ a / b < c / d

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv]

Result:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : LinearOrder G₀
inst✝² : ZeroLEOneClass G₀
a b c d : G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : MulPosStrictMono G₀
hac : a ≤ c
hdb : d < b
hc : 0 < c
hd : 0 < d
⊢ a * b⁻¹ < c * d⁻¹
-- Mathlib/Analysis/Calculus/ContDiff/RCLike.lean
theorem ContDiff.lipschitzWith_of_hasCompactSupport {f : E' → F'}
    (hf : HasCompactSupport f) (h'f : ContDiff 𝕂 n f) (hn : 1 ≤ n) :
    ∃ C, LipschitzWith C f

Proof state:
n : WithTop ℕ∞
𝕂 : Type u_1
inst✝⁴ : RCLike 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
hf : HasCompactSupport f
h'f : ContDiff 𝕂 n f
hn : 1 ≤ n
⊢ ∃ C, LipschitzWith C f

Tactic:
obtain ⟨C, hC⟩ := (hf.fderiv 𝕂).exists_bound_of_continuous (h'f.continuous_fderiv hn)

Result:
case intro
n : WithTop ℕ∞
𝕂 : Type u_1
inst✝⁴ : RCLike 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
hf : HasCompactSupport f
h'f : ContDiff 𝕂 n f
hn : 1 ≤ n
C : ℝ
hC : ∀ (x : E'), ‖fderiv 𝕂 f x‖ ≤ C
⊢ ∃ C, LipschitzWith C f

Proof state:
case intro
n : WithTop ℕ∞
𝕂 : Type u_1
inst✝⁴ : RCLike 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
hf : HasCompactSupport f
h'f : ContDiff 𝕂 n f
hn : 1 ≤ n
C : ℝ
hC : ∀ (x : E'), ‖fderiv 𝕂 f x‖ ≤ C
⊢ ∃ C, LipschitzWith C f

Tactic:
refine ⟨⟨max C 0, le_max_right _ _⟩, ?_⟩

Result:
case intro
n : WithTop ℕ∞
𝕂 : Type u_1
inst✝⁴ : RCLike 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
hf : HasCompactSupport f
h'f : ContDiff 𝕂 n f
hn : 1 ≤ n
C : ℝ
hC : ∀ (x : E'), ‖fderiv 𝕂 f x‖ ≤ C
⊢ LipschitzWith ⟨C ⊔ 0, ⋯⟩ f

Proof state:
n : WithTop ℕ∞
𝕂 : Type u_1
inst✝⁴ : RCLike 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
hf : HasCompactSupport f
h'f : ContDiff 𝕂 n f
hn : 1 ≤ n
C : ℝ
hC : ∀ (x : E'), ‖fderiv 𝕂 f x‖ ≤ C
x : E'
⊢ ‖fderiv 𝕂 f x‖₊ ≤ ⟨C ⊔ 0, ⋯⟩

Tactic:
simp [← NNReal.coe_le_coe, hC x]

Result:
no goals

Proof state:
case intro
n : WithTop ℕ∞
𝕂 : Type u_1
inst✝⁴ : RCLike 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
hf : HasCompactSupport f
h'f : ContDiff 𝕂 n f
hn : 1 ≤ n
C : ℝ
hC : ∀ (x : E'), ‖fderiv 𝕂 f x‖ ≤ C
⊢ LipschitzWith ⟨C ⊔ 0, ⋯⟩ f

Tactic:
apply lipschitzWith_of_nnnorm_fderiv_le (h'f.differentiable hn) (fun x ↦ ?_)

Result:
n : WithTop ℕ∞
𝕂 : Type u_1
inst✝⁴ : RCLike 𝕂
E' : Type u_2
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕂 E'
F' : Type u_3
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕂 F'
f : E' → F'
hf : HasCompactSupport f
h'f : ContDiff 𝕂 n f
hn : 1 ≤ n
C : ℝ
hC : ∀ (x : E'), ‖fderiv 𝕂 f x‖ ≤ C
x : E'
⊢ ‖fderiv 𝕂 f x‖₊ ≤ ⟨C ⊔ 0, ⋯⟩
-- Mathlib/Algebra/Category/Grp/EpiMono.lean
theorem fromCoset_eq_of_mem_range {b : B} (hb : b ∈ f.hom.range) :
    fromCoset ⟨b • ↑f.hom.range, b, rfl⟩ = fromCoset ⟨f.hom.range, 1, one_leftCoset _⟩

Proof state:
case e_a.e_val
A B : Grp
f : A ⟶ B
b : ↑B
hb : b ∈ (Hom.hom f).range
⊢ b • ↑(Hom.hom f).range = ↑(Hom.hom f).range

Tactic:
nth_rw 2 [show (f.hom.range : Set B) = (1 : B) • f.hom.range from (one_leftCoset _).symm]

Result:
case e_a.e_val
A B : Grp
f : A ⟶ B
b : ↑B
hb : b ∈ (Hom.hom f).range
⊢ b • ↑(Hom.hom f).range = 1 • ↑(Hom.hom f).range

Proof state:
A B : Grp
f : A ⟶ B
b : ↑B
hb : b ∈ (Hom.hom f).range
⊢ fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩ = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩

Tactic:
congr

Result:
case e_a.e_val
A B : Grp
f : A ⟶ B
b : ↑B
hb : b ∈ (Hom.hom f).range
⊢ b • ↑(Hom.hom f).range = ↑(Hom.hom f).range

Proof state:
case e_a.e_val
A B : Grp
f : A ⟶ B
b : ↑B
hb : b ∈ (Hom.hom f).range
⊢ b⁻¹ ∈ (Hom.hom f).range

Tactic:
exact Subgroup.inv_mem _ hb

Result:
no goals

Proof state:
case e_a.e_val
A B : Grp
f : A ⟶ B
b : ↑B
hb : b ∈ (Hom.hom f).range
⊢ b • ↑(Hom.hom f).range = 1 • ↑(Hom.hom f).range

Tactic:
rw [leftCoset_eq_iff, mul_one]

Result:
case e_a.e_val
A B : Grp
f : A ⟶ B
b : ↑B
hb : b ∈ (Hom.hom f).range
⊢ b⁻¹ ∈ (Hom.hom f).range
-- Mathlib/Data/List/TakeDrop.lean
theorem length_dropSlice (i j : ℕ) (xs : List α) :
    (List.dropSlice i j xs).length = xs.length - min j (xs.length - i)

Proof state:
case cons.succ
α : Type u
x : α
xs : List α
xs_ih : ∀ (i j : ℕ), (dropSlice i j xs).length = xs.length - min j (xs.length - i)
j n✝ : ℕ
⊢ xs.length - min j (xs.length - n✝) + 1 = xs.length + 1 - min j (xs.length - n✝)

Tactic:
omega

Result:
no goals

Proof state:
case cons.zero
α : Type u
x : α
xs : List α
xs_ih : ∀ (i j : ℕ), (dropSlice i j xs).length = xs.length - min j (xs.length - i)
j : ℕ
⊢ (drop j (x :: xs)).length = (x :: xs).length - min j ((x :: xs).length - 0)

Tactic:
cases j with
| zero => simp
| succ n => simp_all [xs_ih]; omega

Result:
no goals

Proof state:
case cons.zero.succ
α : Type u
x : α
xs : List α
xs_ih : ∀ (i j : ℕ), (dropSlice i j xs).length = xs.length - min j (xs.length - i)
n : ℕ
⊢ xs.length - n = xs.length + 1 - min (n + 1) (xs.length + 1)

Tactic:
omega

Result:
no goals

Proof state:
case cons.zero.succ
α : Type u
x : α
xs : List α
xs_ih : ∀ (i j : ℕ), (dropSlice i j xs).length = xs.length - min j (xs.length - i)
n : ℕ
⊢ (drop (n + 1) (x :: xs)).length = (x :: xs).length - min (n + 1) ((x :: xs).length - 0)

Tactic:
simp_all [xs_ih]

Result:
case cons.zero.succ
α : Type u
x : α
xs : List α
xs_ih : ∀ (i j : ℕ), (dropSlice i j xs).length = xs.length - min j (xs.length - i)
n : ℕ
⊢ xs.length - n = xs.length + 1 - min (n + 1) (xs.length + 1)

Proof state:
case cons.succ
α : Type u
x : α
xs : List α
xs_ih : ∀ (i j : ℕ), (dropSlice i j xs).length = xs.length - min j (xs.length - i)
j n✝ : ℕ
⊢ (x :: dropSlice n✝ j xs).length = (x :: xs).length - min j ((x :: xs).length - (n✝ + 1))

Tactic:
simp [xs_ih]

Result:
case cons.succ
α : Type u
x : α
xs : List α
xs_ih : ∀ (i j : ℕ), (dropSlice i j xs).length = xs.length - min j (xs.length - i)
j n✝ : ℕ
⊢ xs.length - min j (xs.length - n✝) + 1 = xs.length + 1 - min j (xs.length - n✝)

Proof state:
case cons.zero.zero
α : Type u
x : α
xs : List α
xs_ih : ∀ (i j : ℕ), (dropSlice i j xs).length = xs.length - min j (xs.length - i)
⊢ (drop 0 (x :: xs)).length = (x :: xs).length - min 0 ((x :: xs).length - 0)

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u
x : α
xs : List α
xs_ih : ∀ (i j : ℕ), (dropSlice i j xs).length = xs.length - min j (xs.length - i)
i j : ℕ
⊢ (dropSlice i j (x :: xs)).length = (x :: xs).length - min j ((x :: xs).length - i)

Tactic:
cases i <;> simp only [List.dropSlice]

Result:
case cons.zero
α : Type u
x : α
xs : List α
xs_ih : ∀ (i j : ℕ), (dropSlice i j xs).length = xs.length - min j (xs.length - i)
j : ℕ
⊢ (drop j (x :: xs)).length = (x :: xs).length - min j ((x :: xs).length - 0)

case cons.succ
α : Type u
x : α
xs : List α
xs_ih : ∀ (i j : ℕ), (dropSlice i j xs).length = xs.length - min j (xs.length - i)
j n✝ : ℕ
⊢ (x :: dropSlice n✝ j xs).length = (x :: xs).length - min j ((x :: xs).length - (n✝ + 1))

Proof state:
case nil
α : Type u
i j : ℕ
⊢ (dropSlice i j []).length = [].length - min j ([].length - i)

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Content.lean
theorem outerMeasure_exists_open {A : Set G} (hA : μ.outerMeasure A ≠ ∞) {ε : ℝ≥0} (hε : ε ≠ 0) :
    ∃ U : Opens G, A ⊆ U ∧ μ.outerMeasure U ≤ μ.outerMeasure A + ε

Proof state:
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
A : Set G
hA : μ.outerMeasure A ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∃ U, A ⊆ ↑U ∧ μ.outerMeasure ↑U ≤ μ.outerMeasure A + ↑ε

Tactic:
rcases inducedOuterMeasure_exists_set _ μ.innerContent_iUnion_nat μ.innerContent_mono hA
    (ENNReal.coe_ne_zero.2 hε) with
  ⟨U, hU, h2U, h3U⟩

Result:
case intro.intro.intro
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
A : Set G
hA : μ.outerMeasure A ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
U : Set G
hU : IsOpen U
h2U : A ⊆ U
h3U :
  (inducedOuterMeasure (fun s₁ hs₁ => μ.innerContent { carrier := s₁, is_open' := hs₁ }) ⋯ ⋯) U ≤
    (inducedOuterMeasure (fun s₁ hs₁ => μ.innerContent { carrier := s₁, is_open' := hs₁ }) ⋯ ⋯) A + ↑ε
⊢ ∃ U, A ⊆ ↑U ∧ μ.outerMeasure ↑U ≤ μ.outerMeasure A + ↑ε

Proof state:
case intro.intro.intro
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
A : Set G
hA : μ.outerMeasure A ≠ ⊤
ε : ℝ≥0
hε : ε ≠ 0
U : Set G
hU : IsOpen U
h2U : A ⊆ U
h3U :
  (inducedOuterMeasure (fun s₁ hs₁ => μ.innerContent { carrier := s₁, is_open' := hs₁ }) ⋯ ⋯) U ≤
    (inducedOuterMeasure (fun s₁ hs₁ => μ.innerContent { carrier := s₁, is_open' := hs₁ }) ⋯ ⋯) A + ↑ε
⊢ ∃ U, A ⊆ ↑U ∧ μ.outerMeasure ↑U ≤ μ.outerMeasure A + ↑ε

Tactic:
exact ⟨⟨U, hU⟩, h2U, h3U⟩

Result:
no goals