harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem thickening_thickening (hε : 0 < ε) (hδ : 0 < δ) (s : Set E) :
    thickening ε (thickening δ s) = thickening (ε + δ) s :=
  (thickening_thickening_subset _ _ _).antisymm fun x => by
    simp_rw [mem_thickening_iff]
    rintro ⟨z, hz, hxz⟩
    rw [add_comm] at hxz
    obtain ⟨y, hxy, hyz⟩ := exists_dist_lt_lt hε hδ hxz
    exact ⟨y, ⟨_, hz, hyz⟩, hxy⟩

Proof state:
case intro.intro.intro.intro
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
s : Set E
x z : E
hz : z ∈ s
hxz : dist x z < δ + ε
y : E
hxy : dist x y < ε
hyz : dist y z < δ
⊢ ∃ z, (∃ z_1 ∈ s, dist z z_1 < δ) ∧ dist x z < ε

Tactic:
exact ⟨y, ⟨_, hz, hyz⟩, hxy⟩

Result:
no goals

Proof state:
case intro.intro
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
s : Set E
x z : E
hz : z ∈ s
hxz : dist x z < ε + δ
⊢ ∃ z, (∃ z_1 ∈ s, dist z z_1 < δ) ∧ dist x z < ε

Tactic:
rw [add_comm] at hxz

Result:
case intro.intro
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
s : Set E
x z : E
hz : z ∈ s
hxz : dist x z < δ + ε
⊢ ∃ z, (∃ z_1 ∈ s, dist z z_1 < δ) ∧ dist x z < ε

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
s : Set E
x : E
⊢ x ∈ thickening (ε + δ) s → x ∈ thickening ε (thickening δ s)

Tactic:
simp_rw [mem_thickening_iff]

Result:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
s : Set E
x : E
⊢ (∃ z ∈ s, dist x z < ε + δ) → ∃ z, (∃ z_1 ∈ s, dist z z_1 < δ) ∧ dist x z < ε

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
s : Set E
x : E
⊢ (∃ z ∈ s, dist x z < ε + δ) → ∃ z, (∃ z_1 ∈ s, dist z z_1 < δ) ∧ dist x z < ε

Tactic:
rintro ⟨z, hz, hxz⟩

Result:
case intro.intro
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
s : Set E
x z : E
hz : z ∈ s
hxz : dist x z < ε + δ
⊢ ∃ z, (∃ z_1 ∈ s, dist z z_1 < δ) ∧ dist x z < ε

Proof state:
case intro.intro
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
s : Set E
x z : E
hz : z ∈ s
hxz : dist x z < δ + ε
⊢ ∃ z, (∃ z_1 ∈ s, dist z z_1 < δ) ∧ dist x z < ε

Tactic:
obtain ⟨y, hxy, hyz⟩ := exists_dist_lt_lt hε hδ hxz

Result:
case intro.intro.intro.intro
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
s : Set E
x z : E
hz : z ∈ s
hxz : dist x z < δ + ε
y : E
hxy : dist x y < ε
hyz : dist y z < δ
⊢ ∃ z, (∃ z_1 ∈ s, dist z z_1 < δ) ∧ dist x z < ε
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem len_le_of_mono {x y : SimplexCategory} {f : x ⟶ y} : Mono f → x.len ≤ y.len

Proof state:
x y : SimplexCategory
f : x ⟶ y
⊢ Mono f → x.len ≤ y.len

Tactic:
intro hyp_f_mono

Result:
x y : SimplexCategory
f : x ⟶ y
hyp_f_mono : Mono f
⊢ x.len ≤ y.len

Proof state:
x y : SimplexCategory
f : x ⟶ y
hyp_f_mono : Mono f
f_inj : Function.Injective (Hom.toOrderHom f).toFun
⊢ x.len ≤ y.len

Tactic:
simpa using Fintype.card_le_of_injective f.toOrderHom.toFun f_inj

Result:
no goals

Proof state:
x y : SimplexCategory
f : x ⟶ y
hyp_f_mono : Mono f
⊢ x.len ≤ y.len

Tactic:
have f_inj : Function.Injective f.toOrderHom.toFun := mono_iff_injective.1 hyp_f_mono

Result:
x y : SimplexCategory
f : x ⟶ y
hyp_f_mono : Mono f
f_inj : Function.Injective (Hom.toOrderHom f).toFun
⊢ x.len ≤ y.len
-- Mathlib/Topology/Order/ScottTopology.lean
@[simp] lemma scottContinuous_iff_continuous {D : Set (Set α)} [Topology.IsScott α D]
    (hD : ∀ a b : α, a ≤ b → {a, b} ∈ D) : ScottContinuousOn D f ↔ Continuous f

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
⊢ ScottContinuousOn D f ↔ Continuous f

Tactic:
refine ⟨fun h ↦ continuous_def.2 fun u hu ↦ ?_, ?_⟩

Result:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
h : ScottContinuousOn D f
u : Set β
hu : IsOpen u
⊢ IsOpen (f ⁻¹' u)

case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
⊢ Continuous f → ScottContinuousOn D f

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : Continuous f
t : Set α
h₀ : t ∈ D
d₁ : t.Nonempty
d₂ : DirectedOn (fun x1 x2 => x1 ≤ x2) t
a : α
d₃ : IsLUB t a
b : β
hb : b ∈ upperBounds (f '' t)
h : ¬f a ≤ b
⊢ False

Tactic:
let u := (Iic b)ᶜ

Result:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : Continuous f
t : Set α
h₀ : t ∈ D
d₁ : t.Nonempty
d₂ : DirectedOn (fun x1 x2 => x1 ≤ x2) t
a : α
d₃ : IsLUB t a
b : β
hb : b ∈ upperBounds (f '' t)
h : ¬f a ≤ b
u : Set β := (Iic b)ᶜ
⊢ False

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : Continuous f
t : Set α
h₀ : t ∈ D
d₁ : t.Nonempty
d₂ : DirectedOn (fun x1 x2 => x1 ≤ x2) t
a : α
d₃ : IsLUB t a
b : β
hb : b ∈ upperBounds (f '' t)
⊢ f a ≤ b

Tactic:
by_contra h

Result:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : Continuous f
t : Set α
h₀ : t ∈ D
d₁ : t.Nonempty
d₂ : DirectedOn (fun x1 x2 => x1 ≤ x2) t
a : α
d₃ : IsLUB t a
b : β
hb : b ∈ upperBounds (f '' t)
h : ¬f a ≤ b
⊢ False
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem dropInfix?_eq_some_iff [BEq α] {l i p s : List α} :
    dropInfix? l i = some (p, s) ↔
      -- `i` is an infix up to `==`
      (∃ i', l = p ++ i' ++ s ∧ i' == i) ∧
        -- and there is no shorter prefix for which that is the case
        (∀ p' i' s', l = p' ++ i' ++ s' → i' == i → p'.length ≥ p.length)

Proof state:
α : Type u_1
inst✝ : BEq α
l i p s : List α
⊢ (∃ p',
      p = [].reverse ++ p' ∧
        (∃ i', l = p' ++ i' ++ s ∧ (i' == i) = true) ∧
          ∀ (p'' i'' s'' : List α), l = p'' ++ i'' ++ s'' → (i'' == i) = true → p''.length ≥ p'.length) ↔
    (∃ i', l = p ++ i' ++ s ∧ (i' == i) = true) ∧
      ∀ (p' i' s' : List α), l = p' ++ i' ++ s' → (i' == i) = true → p'.length ≥ p.length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
l i p s : List α
⊢ l.dropInfix? i = some (p, s) ↔
    (∃ i', l = p ++ i' ++ s ∧ (i' == i) = true) ∧
      ∀ (p' i' s' : List α), l = p' ++ i' ++ s' → (i' == i) = true → p'.length ≥ p.length

Tactic:
unfold dropInfix?

Result:
α : Type u_1
inst✝ : BEq α
l i p s : List α
⊢ dropInfix?.go i l [] = some (p, s) ↔
    (∃ i', l = p ++ i' ++ s ∧ (i' == i) = true) ∧
      ∀ (p' i' s' : List α), l = p' ++ i' ++ s' → (i' == i) = true → p'.length ≥ p.length

Proof state:
α : Type u_1
inst✝ : BEq α
l i p s : List α
⊢ dropInfix?.go i l [] = some (p, s) ↔
    (∃ i', l = p ++ i' ++ s ∧ (i' == i) = true) ∧
      ∀ (p' i' s' : List α), l = p' ++ i' ++ s' → (i' == i) = true → p'.length ≥ p.length

Tactic:
rw [dropInfix?_go_eq_some_iff]

Result:
α : Type u_1
inst✝ : BEq α
l i p s : List α
⊢ (∃ p',
      p = [].reverse ++ p' ∧
        (∃ i', l = p' ++ i' ++ s ∧ (i' == i) = true) ∧
          ∀ (p'' i'' s'' : List α), l = p'' ++ i'' ++ s'' → (i'' == i) = true → p''.length ≥ p'.length) ↔
    (∃ i', l = p ++ i' ++ s ∧ (i' == i) = true) ∧
      ∀ (p' i' s' : List α), l = p' ++ i' ++ s' → (i' == i) = true → p'.length ≥ p.length
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_inj : map f = map g ↔ f = g

Proof state:
case mpr
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
⊢ f = g → map f = map g

Tactic:
intro h

Result:
case mpr
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
h : f = g
⊢ map f = map g

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
⊢ map f = map g ↔ f = g

Tactic:
constructor

Result:
case mp
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
⊢ map f = map g → f = g

case mpr
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
⊢ f = g → map f = map g

Proof state:
case mpr
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
⊢ map f = map f

Tactic:
rfl

Result:
no goals

Proof state:
case mp
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
⊢ map f = map g → f = g

Tactic:
intro h

Result:
case mp
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
h : map f = map g
⊢ f = g

Proof state:
case mp.h
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
h : map f = map g
a : α✝¹
⊢ f a = g a

Tactic:
replace h := congrFun h [a]

Result:
case mp.h
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
a : α✝¹
h : map f [a] = map g [a]
⊢ f a = g a

Proof state:
case mp.h
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
a : α✝¹
h : map f [a] = map g [a]
⊢ f a = g a

Tactic:
simpa using h

Result:
no goals

Proof state:
case mp
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
h : map f = map g
⊢ f = g

Tactic:
ext a

Result:
case mp.h
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
h : map f = map g
a : α✝¹
⊢ f a = g a

Proof state:
case mpr
α✝¹ : Type u_1
α✝ : Type u_2
f g : α✝¹ → α✝
h : f = g
⊢ map f = map g

Tactic:
subst h

Result:
case mpr
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
⊢ map f = map f
-- Mathlib/NumberTheory/LSeries/SumCoeff.lean
theorem lemma₁ (hlim : Tendsto (fun n : ℕ ↦ (∑ k ∈ Icc 1 n, f k) / n) atTop (𝓝 l))
    {s : ℝ} (hs : 1 < s) :
    IntegrableOn (fun t : ℝ ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (t : ℂ) ^ (-(s : ℂ) - 1)) (Set.Ici 1)

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
⊢ IntegrableOn (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume

Tactic:
have h₁ : LocallyIntegrableOn (fun t : ℝ ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * (t : ℂ) ^ (-(s : ℂ) - 1))
      (Set.Ici 1) := by
  simp_rw [mul_comm]
  refine locallyIntegrableOn_mul_sum_Icc f zero_le_one ?_
  refine ContinuousOn.locallyIntegrableOn (fun t ht ↦ ?_) measurableSet_Ici
  exact (continuousAt_ofReal_cpow_const _ _ <|
    Or.inr (zero_lt_one.trans_le ht).ne').continuousWithinAt

Result:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
⊢ IntegrableOn (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
⊢ Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑(↑n ^ 1)) atTop (𝓝 l)

Tactic:
simpa using hlim

Result:
no goals

Proof state:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
this : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑(↑n ^ 1)) atTop (𝓝 l)
⊢ (fun t => ∑ k ∈ Icc 1 ⌊t⌋₊, f k) =O[atTop] fun x => ↑⌊x⌋₊

Tactic:
simpa using (isBigO_atTop_natCast_rpow_of_tendsto_div_rpow this).comp_tendsto
    tendsto_nat_floor_atTop

Result:
no goals

Proof state:
case refine_1
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n => (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t => (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
h₂ : (fun t => ∑ k ∈ Icc 1 ⌊t⌋₊, f k) =O[atTop] fun t => t ^ 1
⊢ (fun t => ↑t ^ (-↑s - 1)) =O[atTop] fun t => t ^ (-s - 1)

Tactic:
exact (norm_ofReal_cpow_eventually_eq_atTop _).isBigO.of_norm_left

Result:
no goals
-- Mathlib/Topology/Homotopy/HomotopyGroup.lean
theorem homotopicTo (i : N) {p q : Ω^ N X x} :
    Homotopic p q → (toLoop i p).Homotopic (toLoop i q)

Proof state:
case refine_4
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (x_1 : ↑I),
    { toFun := fun t => ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯ }.toFun (1, x_1) =
      (toLoop i q).toContinuousMap x_1

case refine_3.H
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ H ((0, x✝).1, (Cube.insertAt i) ((0, x✝).2, y✝)) = p ((Cube.insertAt i) (x✝, y✝))

case refine_5
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (t x_1 : ↑I),
    x_1 ∈ {0, 1} →
      {
            toFun := fun x_2 =>
              { toFun := fun t => ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ⋯,
                    map_one_left := ?refine_4 }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        (toLoop i p).toContinuousMap x_1

Tactic:
intro

Result:
case refine_4
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
⊢ { toFun := fun t => ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯ }.toFun (1, x✝) = (toLoop i q).toContinuousMap x✝

case refine_3.H
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ H ((0, x✝).1, (Cube.insertAt i) ((0, x✝).2, y✝)) = p ((Cube.insertAt i) (x✝, y✝))

case refine_5
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (t x_1 : ↑I),
    x_1 ∈ {0, 1} →
      {
            toFun := fun x_2 =>
              { toFun := fun t => ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ⋯,
                    map_one_left := ⋯ }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        (toLoop i p).toContinuousMap x_1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filter_eq_cons_iff {l} {a} {as} :
    filter p l = a :: as ↔
      ∃ l₁ l₂, l = l₁ ++ a :: l₂ ∧ (∀ x, x ∈ l₁ → ¬p x) ∧ p a ∧ filter p l₂ = as

Proof state:
case mp.cons.isTrue.intro
α✝ : Type u_1
p : α✝ → Bool
x : α✝
l : List α✝
w : p x = true
ih :
  filter p l = x :: filter p l →
    ∃ l₁ l₂, l = l₁ ++ x :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p x = true ∧ filter p l₂ = filter p l
⊢ ∃ l₁ l₂, x :: l = l₁ ++ x :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p x = true ∧ filter p l₂ = filter p l

Tactic:
refine ⟨[], l, ?_⟩

Result:
case mp.cons.isTrue.intro
α✝ : Type u_1
p : α✝ → Bool
x : α✝
l : List α✝
w : p x = true
ih :
  filter p l = x :: filter p l →
    ∃ l₁ l₂, l = l₁ ++ x :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p x = true ∧ filter p l₂ = filter p l
⊢ x :: l = [] ++ x :: l ∧ (∀ (x : α✝), x ∈ [] → ¬p x = true) ∧ p x = true ∧ filter p l = filter p l

Proof state:
α✝ : Type u_1
p : α✝ → Bool
l : List α✝
a : α✝
as : List α✝
⊢ filter p l = a :: as ↔ ∃ l₁ l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as

Tactic:
constructor

Result:
case mp
α✝ : Type u_1
p : α✝ → Bool
l : List α✝
a : α✝
as : List α✝
⊢ filter p l = a :: as → ∃ l₁ l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as

case mpr
α✝ : Type u_1
p : α✝ → Bool
l : List α✝
a : α✝
as : List α✝
⊢ (∃ l₁ l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as) →
    filter p l = a :: as

Proof state:
case mp.cons
α✝ : Type u_1
p : α✝ → Bool
a : α✝
as : List α✝
x : α✝
l : List α✝
ih :
  filter p l = a :: as → ∃ l₁ l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as
h : (if p x = true then x :: filter p l else filter p l) = a :: as
⊢ ∃ l₁ l₂, x :: l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as

Tactic:
split at h <;> rename_i w

Result:
case mp.cons.isTrue
α✝ : Type u_1
p : α✝ → Bool
a : α✝
as : List α✝
x : α✝
l : List α✝
ih :
  filter p l = a :: as → ∃ l₁ l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as
w : p x = true
h : x :: filter p l = a :: as
⊢ ∃ l₁ l₂, x :: l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as

case mp.cons.isFalse
α✝ : Type u_1
p : α✝ → Bool
a : α✝
as : List α✝
x : α✝
l : List α✝
ih :
  filter p l = a :: as → ∃ l₁ l₂, l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as
w : ¬p x = true
h : filter p l = a :: as
⊢ ∃ l₁ l₂, x :: l = l₁ ++ a :: l₂ ∧ (∀ (x : α✝), x ∈ l₁ → ¬p x = true) ∧ p a = true ∧ filter p l₂ = as
-- Mathlib/Analysis/Convex/Continuous.lean
lemma ConvexOn.locallyLipschitzOn_iff_continuousOn (hC : IsOpen C) (hf : ConvexOn ℝ C f) :
    LocallyLipschitzOn C f ↔ ContinuousOn f C

Proof state:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen C
hf : ConvexOn ℝ C f
hC' : C.Nonempty
⊢ LocallyLipschitzOn C f ↔ ContinuousOn f C

Tactic:
exact (hf.continuousOn_tfae hC hC').out 0 1

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen C
hf : ConvexOn ℝ C f
⊢ LocallyLipschitzOn C f ↔ ContinuousOn f C

Tactic:
obtain rfl | hC' := C.eq_empty_or_nonempty

Result:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
hC : IsOpen ∅
hf : ConvexOn ℝ ∅ f
⊢ LocallyLipschitzOn ∅ f ↔ ContinuousOn f ∅

case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen C
hf : ConvexOn ℝ C f
hC' : C.Nonempty
⊢ LocallyLipschitzOn C f ↔ ContinuousOn f C

Proof state:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
hC : IsOpen ∅
hf : ConvexOn ℝ ∅ f
⊢ LocallyLipschitzOn ∅ f ↔ ContinuousOn f ∅

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma IsAlternating.spanningCoe (halt : G.IsAlternating G') (H : Subgraph G)  :
    H.spanningCoe.IsAlternating G'

Proof state:
V : Type u_1
G G' : SimpleGraph V
halt : G.IsAlternating G'
H : G.Subgraph
v w w' : V
hww' : w ≠ w'
hvw : H.spanningCoe.Adj v w
hvv' : H.spanningCoe.Adj v w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'

Tactic:
simp only [Subgraph.spanningCoe_adj] at hvw hvv'

Result:
V : Type u_1
G G' : SimpleGraph V
halt : G.IsAlternating G'
H : G.Subgraph
v w w' : V
hww' : w ≠ w'
hvw : H.Adj v w
hvv' : H.Adj v w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'

Proof state:
V : Type u_1
G G' : SimpleGraph V
halt : G.IsAlternating G'
H : G.Subgraph
v w w' : V
hww' : w ≠ w'
hvw : H.Adj v w
hvv' : H.Adj v w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'

Tactic:
exact halt hww' hvw.adj_sub hvv'.adj_sub

Result:
no goals

Proof state:
V : Type u_1
G G' : SimpleGraph V
halt : G.IsAlternating G'
H : G.Subgraph
⊢ H.spanningCoe.IsAlternating G'

Tactic:
intro v w w' hww' hvw hvv'

Result:
V : Type u_1
G G' : SimpleGraph V
halt : G.IsAlternating G'
H : G.Subgraph
v w w' : V
hww' : w ≠ w'
hvw : H.spanningCoe.Adj v w
hvv' : H.spanningCoe.Adj v w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_eq_zero (h : 0 ≤ x) : √x = 0 ↔ x = 0

Proof state:
x : ℝ
h : 0 ≤ x
⊢ √x = 0 ↔ x = 0

Tactic:
simpa using sqrt_inj h le_rfl

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem div_le_one_of_neg (hb : b < 0) : a / b ≤ 1 ↔ b ≤ a

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
hb : b < 0
⊢ a / b ≤ 1 ↔ b ≤ a

Tactic:
rw [div_le_iff_of_neg hb, one_mul]

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma genEigenspace_inf_le_add
    (f₁ f₂ : End R M) (μ₁ μ₂ : R) (k₁ k₂ : ℕ∞) (h : Commute f₁ f₂) :
    (f₁.genEigenspace μ₁ k₁) ⊓ (f₂.genEigenspace μ₂ k₂) ≤
    (f₁ + f₂).genEigenspace (μ₁ + μ₂) (k₁ + k₂)

Proof state:
case h.right
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
m : M
l₁ : ℕ
hlk₁ : ↑l₁ ≤ k₁
hl₁ : ((f₁ - μ₁ • 1) ^ l₁) m = 0
l₂ : ℕ
hlk₂ : ↑l₂ ≤ k₂
hl₂ : ((f₂ - μ₂ • 1) ^ l₂) m = 0
this : f₁ + f₂ - (μ₁ + μ₂) • 1 = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)
h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1)
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal (l₁ + l₂)
⊢ ((l₁ + l₂).choose (i, j).1 • ((f₁ - μ₁ • 1) ^ (i, j).1 * (f₂ - μ₂ • 1) ^ (i, j).2)) m = 0

Tactic:
suffices (((f₁ - μ₁ • 1) ^ i) * ((f₂ - μ₂ • 1) ^ j)) m = 0 by
  rw [LinearMap.smul_apply, this, smul_zero]

Result:
case h.right
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
m : M
l₁ : ℕ
hlk₁ : ↑l₁ ≤ k₁
hl₁ : ((f₁ - μ₁ • 1) ^ l₁) m = 0
l₂ : ℕ
hlk₂ : ↑l₂ ≤ k₂
hl₂ : ((f₂ - μ₂ • 1) ^ l₂) m = 0
this : f₁ + f₂ - (μ₁ + μ₂) • 1 = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)
h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1)
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal (l₁ + l₂)
⊢ ((f₁ - μ₁ • 1) ^ i * (f₂ - μ₂ • 1) ^ j) m = 0
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable (μ : Measure α) {f : α → ℝ≥0∞}
    (f_meas : Measurable f) (g : α → ℝ≥0∞) {s : Set α} (hs : MeasurableSet s)
    (hf : ∀ᵐ x ∂μ.restrict s, f x < ∞) :
    ∫⁻ a in s, g a ∂μ.withDensity f = ∫⁻ a in s, (f * g) a ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (x : α) ∂μ.restrict s, f x < ⊤
⊢ ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ

Tactic:
rw [restrict_withDensity hs, lintegral_withDensity_eq_lintegral_mul_non_measurable _ f_meas hf]

Result:
no goals
-- Mathlib/Tactic/Qify.lean
@[qify_simps] lemma intCast_ne (a b : ℤ) : a ≠ b ↔ (a : ℚ) ≠ (b : ℚ)

Proof state:
a b : ℤ
⊢ a ≠ b ↔ ↑a ≠ ↑b

Tactic:
simp only [ne_eq, Int.cast_inj]

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean
theorem exists_eigenvalue [IsAlgClosed K] [FiniteDimensional K V] [Nontrivial V] (f : End K V) :
    ∃ c : K, f.HasEigenvalue c

Proof state:
K : Type u_1
V : Type u_2
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : IsAlgClosed K
inst✝¹ : FiniteDimensional K V
inst✝ : Nontrivial V
f : End K V
⊢ ∃ c, f.HasEigenvalue c

Tactic:
simp_rw [hasEigenvalue_iff_mem_spectrum]

Result:
K : Type u_1
V : Type u_2
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : IsAlgClosed K
inst✝¹ : FiniteDimensional K V
inst✝ : Nontrivial V
f : End K V
⊢ ∃ c, c ∈ spectrum K f

Proof state:
K : Type u_1
V : Type u_2
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : IsAlgClosed K
inst✝¹ : FiniteDimensional K V
inst✝ : Nontrivial V
f : End K V
⊢ ∃ c, c ∈ spectrum K f

Tactic:
exact spectrum.nonempty_of_isAlgClosed_of_finiteDimensional K f

Result:
no goals