harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/List.lean
theorem range_list_getElem? :
    range (l[·]? : ℕ → Option α) = insert none (some '' { x | x ∈ l })

Proof state:
case refine_1
α : Type u_1
l : List α
n : ℕ
⊢ l[n]? ∈ insert none (range (some ∘ l.get))

Tactic:
exact (le_or_lt l.length n).imp getElem?_eq_none_iff.mpr
  (fun hlt => ⟨⟨_, hlt⟩, (getElem?_eq_getElem hlt).symm⟩)

Result:
no goals

Proof state:
α : Type u_1
l : List α
⊢ (range fun x => l[x]?) = insert none (some '' {x | x ∈ l})

Tactic:
rw [← range_list_get, ← range_comp]

Result:
α : Type u_1
l : List α
⊢ (range fun x => l[x]?) = insert none (range (some ∘ l.get))

Proof state:
case refine_3
α : Type u_1
l : List α
⊢ range (some ∘ l.get) ⊆ range fun x => l[x]?

Tactic:
exact range_subset_iff.2 fun k => ⟨_, getElem?_eq_getElem _⟩

Result:
no goals

Proof state:
α : Type u_1
l : List α
⊢ (range fun x => l[x]?) = insert none (range (some ∘ l.get))

Tactic:
refine (range_subset_iff.2 fun n => ?_).antisymm (insert_subset_iff.2 ⟨?_, ?_⟩)

Result:
case refine_1
α : Type u_1
l : List α
n : ℕ
⊢ l[n]? ∈ insert none (range (some ∘ l.get))

case refine_2
α : Type u_1
l : List α
⊢ none ∈ range fun x => l[x]?

case refine_3
α : Type u_1
l : List α
⊢ range (some ∘ l.get) ⊆ range fun x => l[x]?

Proof state:
case refine_2
α : Type u_1
l : List α
⊢ none ∈ range fun x => l[x]?

Tactic:
exact ⟨_, getElem?_eq_none_iff.mpr le_rfl⟩

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
theorem aestronglyMeasurable_condExpL1CLM (f : α →₁[μ] F') :
    AEStronglyMeasurable[m] (condExpL1CLM F' hm μ f) μ

Proof state:
case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : ↥(Lp F' 1 μ)
⊢ ∀ ⦃f g : α → F'⦄ (hf : MemLp f 1 μ) (hg : MemLp g 1 μ),
    Disjoint (Function.support f) (Function.support g) →
      (fun f => AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) f)) μ) (MemLp.toLp f hf) →
        (fun f => AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) f)) μ) (MemLp.toLp g hg) →
          (fun f => AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) f)) μ) (MemLp.toLp f hf + MemLp.toLp g hg)

Tactic:
intro f g hf hg _ hfm hgm

Result:
case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f✝ : ↥(Lp F' 1 μ)
f g : α → F'
hf : MemLp f 1 μ
hg : MemLp g 1 μ
a✝ : Disjoint (Function.support f) (Function.support g)
hfm : AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf))) μ
hgm : AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg))) μ
⊢ AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf + MemLp.toLp g hg))) μ

Proof state:
case refine_3
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : ↥(Lp F' 1 μ)
this :
  {f | AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) f)) μ} =
    ⇑(condExpL1CLM F' hm μ) ⁻¹' {f | AEStronglyMeasurable (↑↑f) μ}
⊢ IsClosed (⇑(condExpL1CLM F' hm μ) ⁻¹' {f | AEStronglyMeasurable (↑↑f) μ})

Tactic:
refine IsClosed.preimage (condExpL1CLM F' hm μ).continuous ?_

Result:
case refine_3
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : ↥(Lp F' 1 μ)
this :
  {f | AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) f)) μ} =
    ⇑(condExpL1CLM F' hm μ) ⁻¹' {f | AEStronglyMeasurable (↑↑f) μ}
⊢ IsClosed {f | AEStronglyMeasurable (↑↑f) μ}

Proof state:
case refine_1
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : ↥(Lp F' 1 μ)
c : F'
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ AEStronglyMeasurable (↑↑((condExpL1CLM F' hm μ) ↑(simpleFunc.indicatorConst 1 hs ⋯ c))) μ

Tactic:
rw [condExpL1CLM_indicatorConst hs hμs.ne c]

Result:
case refine_1
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f : ↥(Lp F' 1 μ)
c : F'
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ AEStronglyMeasurable (↑↑((condExpInd F' hm μ s) c)) μ
-- Mathlib/Topology/Constructions.lean
theorem frontier_univ_prod_eq (s : Set Y) :
    frontier ((univ : Set X) ×ˢ s) = univ ×ˢ frontier s

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
⊢ frontier (univ ×ˢ s) = univ ×ˢ frontier s

Tactic:
simp [frontier_prod_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem fst_lt_add_of_mem_enumFrom {x : Nat × α} {n : Nat} {l : List α} (h : x ∈ enumFrom n l) :
    x.1 < n + length l

Proof state:
α : Type u_1
x : Nat × α
n : Nat
l : List α
h : x ∈ enumFrom n l
⊢ x.fst < n + l.length

Tactic:
rcases mem_iff_get.1 h with ⟨i, rfl⟩

Result:
case intro
α : Type u_1
n : Nat
l : List α
i : Fin (enumFrom n l).length
h : (enumFrom n l).get i ∈ enumFrom n l
⊢ ((enumFrom n l).get i).fst < n + l.length

Proof state:
case intro
α : Type u_1
n : Nat
l : List α
i : Fin (enumFrom n l).length
h : (enumFrom n l).get i ∈ enumFrom n l
⊢ ((enumFrom n l).get i).fst < n + l.length

Tactic:
simpa using i.isLt

Result:
no goals
-- Mathlib/Tactic/LinearCombination'.lean
theorem eq_of_add [AddGroup α] (p : (a:α) = b) (H : (a' - b') - (a - b) = 0) : a' = b'

Proof state:
α : Type u_1
a a' b b' : α
inst✝ : AddGroup α
p : a = b
H : a' - b' - (a - b) = 0
⊢ a' = b'

Tactic:
rw [← sub_eq_zero] at p ⊢

Result:
α : Type u_1
a a' b b' : α
inst✝ : AddGroup α
p : a - b = 0
H : a' - b' - (a - b) = 0
⊢ a' - b' = 0

Proof state:
α : Type u_1
a a' b b' : α
inst✝ : AddGroup α
p : a - b = 0
H : a' - b' - (a - b) = 0
⊢ a' - b' = 0

Tactic:
rwa [sub_eq_zero, p] at H

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
theorem prodComparisonBifunctorNatTrans_comp {E : Type u₂} [Category.{v₂} E]
    [ChosenFiniteProducts E] (G : D ⥤ E) : prodComparisonBifunctorNatTrans (F ⋙ G) =
      whiskerRight (prodComparisonBifunctorNatTrans F) ((whiskeringRight _ _ _).obj G) ≫
        whiskerLeft F (whiskerRight (prodComparisonBifunctorNatTrans G)
          ((whiskeringLeft _ _ _).obj F))

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ChosenFiniteProducts C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : ChosenFiniteProducts D
F : C ⥤ D
E : Type u₂
inst✝¹ : Category.{v₂, u₂} E
inst✝ : ChosenFiniteProducts E
G : D ⥤ E
⊢ prodComparisonBifunctorNatTrans (F ⋙ G) =
    whiskerRight (prodComparisonBifunctorNatTrans F) ((whiskeringRight C D E).obj G) ≫
      whiskerLeft F (whiskerRight (prodComparisonBifunctorNatTrans G) ((whiskeringLeft C D E).obj F))

Tactic:
ext

Result:
case w.h.w.h
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ChosenFiniteProducts C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : ChosenFiniteProducts D
F : C ⥤ D
E : Type u₂
inst✝¹ : Category.{v₂, u₂} E
inst✝ : ChosenFiniteProducts E
G : D ⥤ E
x✝¹ x✝ : C
⊢ ((prodComparisonBifunctorNatTrans (F ⋙ G)).app x✝¹).app x✝ =
    ((whiskerRight (prodComparisonBifunctorNatTrans F) ((whiskeringRight C D E).obj G) ≫
              whiskerLeft F (whiskerRight (prodComparisonBifunctorNatTrans G) ((whiskeringLeft C D E).obj F))).app
          x✝¹).app
      x✝

Proof state:
case w.h.w.h
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ChosenFiniteProducts C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : ChosenFiniteProducts D
F : C ⥤ D
E : Type u₂
inst✝¹ : Category.{v₂, u₂} E
inst✝ : ChosenFiniteProducts E
G : D ⥤ E
x✝¹ x✝ : C
⊢ ((prodComparisonBifunctorNatTrans (F ⋙ G)).app x✝¹).app x✝ =
    ((whiskerRight (prodComparisonBifunctorNatTrans F) ((whiskeringRight C D E).obj G) ≫
              whiskerLeft F (whiskerRight (prodComparisonBifunctorNatTrans G) ((whiskeringLeft C D E).obj F))).app
          x✝¹).app
      x✝

Tactic:
simp [prodComparison_comp]

Result:
no goals
-- Mathlib/Data/List/Duplicate.lean
theorem Duplicate.mono_sublist {l' : List α} (hx : x ∈+ l) (h : l <+ l') : x ∈+ l'

Proof state:
case slnil
α : Type u_1
l : List α
x : α
l' : List α
hx : x ∈+ []
⊢ x ∈+ []

Tactic:
exact hx

Result:
no goals

Proof state:
case cons₂.inr
α : Type u_1
l : List α
x : α
l' l₁ l₂ : List α
y : α
h : l₁ <+ l₂
IH : x ∈+ l₁ → x ∈+ l₂
hx : x ∈+ l₁
⊢ y = x ∧ x ∈ l₂ ∨ x ∈+ l₂

Tactic:
simp [IH hx]

Result:
no goals

Proof state:
case cons₂.inl.intro
α : Type u_1
l l' l₁ l₂ : List α
y : α
h : l₁ <+ l₂
IH : y ∈+ l₁ → y ∈+ l₂
hx : y ∈ l₁
⊢ y = y ∧ y ∈ l₂ ∨ y ∈+ l₂

Tactic:
simp [h.subset hx]

Result:
no goals

Proof state:
case cons
α : Type u_1
l : List α
x : α
l' l₁ l₂ : List α
y : α
a✝ : l₁ <+ l₂
IH : x ∈+ l₁ → x ∈+ l₂
hx : x ∈+ l₁
⊢ x ∈+ y :: l₂

Tactic:
exact (IH hx).duplicate_cons _

Result:
no goals

Proof state:
case cons₂
α : Type u_1
l : List α
x : α
l' l₁ l₂ : List α
y : α
h : l₁ <+ l₂
IH : x ∈+ l₁ → x ∈+ l₂
hx : y = x ∧ x ∈ l₁ ∨ x ∈+ l₁
⊢ y = x ∧ x ∈ l₂ ∨ x ∈+ l₂

Tactic:
rcases hx with (⟨rfl, hx⟩ | hx)

Result:
case cons₂.inl.intro
α : Type u_1
l l' l₁ l₂ : List α
y : α
h : l₁ <+ l₂
IH : y ∈+ l₁ → y ∈+ l₂
hx : y ∈ l₁
⊢ y = y ∧ y ∈ l₂ ∨ y ∈+ l₂

case cons₂.inr
α : Type u_1
l : List α
x : α
l' l₁ l₂ : List α
y : α
h : l₁ <+ l₂
IH : x ∈+ l₁ → x ∈+ l₂
hx : x ∈+ l₁
⊢ y = x ∧ x ∈ l₂ ∨ x ∈+ l₂

Proof state:
α : Type u_1
l : List α
x : α
l' : List α
hx : x ∈+ l
h : l <+ l'
⊢ x ∈+ l'

Tactic:
induction' h with l₁ l₂ y _ IH l₁ l₂ y h IH

Result:
case slnil
α : Type u_1
l : List α
x : α
l' : List α
hx : x ∈+ []
⊢ x ∈+ []

case cons
α : Type u_1
l : List α
x : α
l' l₁ l₂ : List α
y : α
a✝ : l₁ <+ l₂
IH : x ∈+ l₁ → x ∈+ l₂
hx : x ∈+ l₁
⊢ x ∈+ y :: l₂

case cons₂
α : Type u_1
l : List α
x : α
l' l₁ l₂ : List α
y : α
h : l₁ <+ l₂
IH : x ∈+ l₁ → x ∈+ l₂
hx : x ∈+ y :: l₁
⊢ x ∈+ y :: l₂

Proof state:
case cons₂
α : Type u_1
l : List α
x : α
l' l₁ l₂ : List α
y : α
h : l₁ <+ l₂
IH : x ∈+ l₁ → x ∈+ l₂
hx : x ∈+ y :: l₁
⊢ x ∈+ y :: l₂

Tactic:
rw [duplicate_cons_iff] at hx ⊢

Result:
case cons₂
α : Type u_1
l : List α
x : α
l' l₁ l₂ : List α
y : α
h : l₁ <+ l₂
IH : x ∈+ l₁ → x ∈+ l₂
hx : y = x ∧ x ∈ l₁ ∨ x ∈+ l₁
⊢ y = x ∧ x ∈ l₂ ∨ x ∈+ l₂
-- Mathlib/Geometry/Manifold/WhitneyEmbedding.lean
theorem embeddingPiTangent_ker_mfderiv (x : M) (hx : x ∈ s) :
    LinearMap.ker (mfderiv I 𝓘(ℝ, ι → E × ℝ) f.embeddingPiTangent x) = ⊥

Proof state:
case h
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
⊢ LinearMap.ker (mfderiv I 𝓘(ℝ, ι → E × ℝ) (⇑f.embeddingPiTangent) x) ≤
    LinearMap.ker
      (((ContinuousLinearMap.fst ℝ E ℝ).comp (ContinuousLinearMap.proj (f.ind x hx))).comp
        (mfderiv I 𝓘(ℝ, ι → E × ℝ) (⇑f.embeddingPiTangent) x))

Tactic:
exact LinearMap.ker_le_ker_comp _ _

Result:
no goals

Proof state:
case h
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
⊢ LinearMap.ker (mfderiv I 𝓘(ℝ, ι → E × ℝ) (⇑f.embeddingPiTangent) x) ≤ ⊥

Tactic:
rw [← (mdifferentiable_chart (f.c (f.ind x hx))).ker_mfderiv_eq_bot
    (f.mem_chartAt_ind_source x hx),
  ← comp_embeddingPiTangent_mfderiv]

Result:
case h
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
⊢ LinearMap.ker (mfderiv I 𝓘(ℝ, ι → E × ℝ) (⇑f.embeddingPiTangent) x) ≤
    LinearMap.ker
      (((ContinuousLinearMap.fst ℝ E ℝ).comp (ContinuousLinearMap.proj (f.ind x hx))).comp
        (mfderiv I 𝓘(ℝ, ι → E × ℝ) (⇑f.embeddingPiTangent) x))

Proof state:
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
⊢ LinearMap.ker (mfderiv I 𝓘(ℝ, ι → E × ℝ) (⇑f.embeddingPiTangent) x) = ⊥

Tactic:
apply bot_unique

Result:
case h
ι : Type uι
E : Type uE
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I ∞ M
inst✝¹ : T2Space M
inst✝ : Fintype ι
s : Set M
f : SmoothBumpCovering ι I M s
x : M
hx : x ∈ s
⊢ LinearMap.ker (mfderiv I 𝓘(ℝ, ι → E × ℝ) (⇑f.embeddingPiTangent) x) ≤ ⊥
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoDiv_zsmul_add (a b : α) (m : ℤ) : toIcoDiv hp a (m • p + b) = m + toIcoDiv hp a b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoDiv hp a (m • p + b) = m + toIcoDiv hp a b

Tactic:
rw [add_comm, toIcoDiv_add_zsmul, add_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem borel_le_caratheodory (hm : IsMetric μ) : borel X ≤ μ.caratheodory

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed s}
s : Set X
S : ℕ → Set X := fun n => {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEdist x t}
Ssep : ∀ (n : ℕ), Metric.AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), Metric.AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : ¬μ (s \ t) = ⊤
r n : ℕ
this : ∀ (i j : ℕ), i < j → Metric.AreSeparated (S (2 * i + 1 + r)) (s \ S (2 * j + r))
i : ℕ
x✝¹ : i ∈ Finset.range n
j : ℕ
x✝ : j ∈ Finset.range n
hij : i ≠ j
h : j < i
x : X
hx : x ∈ S (2 * i + 1 + r) \ S (2 * i + r)
⊢ x ∈ s \ S (2 * i + r)

Tactic:
exact ⟨hx.1.1, hx.2⟩

Result:
no goals

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed s}
s : Set X
S : ℕ → Set X := fun n => {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEdist x t}
Ssep : ∀ (n : ℕ), Metric.AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), Metric.AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : ¬μ (s \ t) = ⊤
r n i j : ℕ
hj : i < j
⊢ (↑(2 * j + r))⁻¹ < (↑(2 * i + 1 + r))⁻¹

Tactic:
rw [ENNReal.inv_lt_inv, Nat.cast_lt]

Result:
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed s}
s : Set X
S : ℕ → Set X := fun n => {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEdist x t}
Ssep : ∀ (n : ℕ), Metric.AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), Metric.AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : ¬μ (s \ t) = ⊤
r n i j : ℕ
hj : i < j
⊢ 2 * i + 1 + r < 2 * j + r

Proof state:
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
⊢ MeasurableSpace.generateFrom {s | IsClosed s} ≤ μ.caratheodory

Tactic:
refine MeasurableSpace.generateFrom_le fun t ht => μ.isCaratheodory_iff_le.2 fun s => ?_

Result:
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed s}
s : Set X
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ s
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem mul_inv_mul_cancel (a : G₀) : a * a⁻¹ * a = a

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a * a⁻¹ * a = a

Tactic:
by_cases h : a = 0

Result:
case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a = 0
⊢ a * a⁻¹ * a = a

case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : ¬a = 0
⊢ a * a⁻¹ * a = a

Proof state:
case neg
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : ¬a = 0
⊢ a * a⁻¹ * a = a

Tactic:
rw [mul_inv_cancel₀ h, one_mul]

Result:
no goals

Proof state:
case pos
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : a = 0
⊢ a * a⁻¹ * a = a

Tactic:
rw [h, inv_zero, mul_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem le_zero_iff {x : BitVec w} : x ≤ 0#w ↔ x = 0#w

Proof state:
case mp
w : Nat
x : BitVec w
h : x ≤ 0#w
this : x ≥ 0
⊢ x = 0#w

Tactic:
exact Eq.symm (BitVec.le_antisymm this h)

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ x ≤ 0#w ↔ x = 0#w

Tactic:
constructor

Result:
case mp
w : Nat
x : BitVec w
⊢ x ≤ 0#w → x = 0#w

case mpr
w : Nat
x : BitVec w
⊢ x = 0#w → x ≤ 0#w

Proof state:
case mpr
w : Nat
x : BitVec w
⊢ x = 0#w → x ≤ 0#w

Tactic:
simp_all

Result:
no goals

Proof state:
case mp
w : Nat
x : BitVec w
⊢ x ≤ 0#w → x = 0#w

Tactic:
intro h

Result:
case mp
w : Nat
x : BitVec w
h : x ≤ 0#w
⊢ x = 0#w

Proof state:
case mp
w : Nat
x : BitVec w
h : x ≤ 0#w
⊢ x = 0#w

Tactic:
have : x ≥ 0 := not_lt_iff_le.mp not_lt_zero

Result:
case mp
w : Nat
x : BitVec w
h : x ≤ 0#w
this : x ≥ 0
⊢ x = 0#w
-- Mathlib/Topology/JacobsonSpace.lean
lemma Topology.IsClosedEmbedding.preimage_closedPoints (hf : IsClosedEmbedding f) :
    f ⁻¹' closedPoints Y = closedPoints X

Proof state:
case h
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsClosedEmbedding f
x : X
⊢ x ∈ f ⁻¹' closedPoints Y ↔ x ∈ closedPoints X

Tactic:
simp [mem_closedPoints_iff, ← Set.image_singleton, hf.isClosed_iff_image_isClosed]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ f ⁻¹' closedPoints Y = closedPoints X

Tactic:
ext x

Result:
case h
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsClosedEmbedding f
x : X
⊢ x ∈ f ⁻¹' closedPoints Y ↔ x ∈ closedPoints X
-- Mathlib/Order/Bounds/Basic.lean
theorem isLUB_Ioo {a b : γ} (hab : a < b) : IsLUB (Ioo a b) b

Proof state:
γ : Type v
inst✝¹ : SemilatticeInf γ
inst✝ : DenselyOrdered γ
a b : γ
hab : a < b
⊢ IsLUB (Ioo a b) b

Tactic:
simpa only [dual_Ioo] using isGLB_Ioo hab.dual

Result:
no goals
-- Mathlib/Order/Estimator.lean
theorem Estimator.improveUntilAux_spec (a : Thunk α) (p : α → Bool)
    [Estimator a ε] [WellFoundedGT (range (bound a : ε → α))] (e : ε) (r : Bool) :
    match Estimator.improveUntilAux a p e r with
    | .error _ => ¬ p a.get
    | .ok e' => p (bound a e')

Proof state:
case neg
α : Type u_1
ε : Type u_2
inst✝² : Preorder α
a : Thunk α
p : α → Bool
inst✝¹ : Estimator a ε
inst✝ : WellFoundedGT ↑(range (bound a))
e : ε
r : Bool
h : ¬p (bound a e) = true
⊢ match
    if false = true then pure e
    else
      match improve a e, ⋯ with
      | none, x => Except.error (if r = true then none else some e)
      | some e', x => improveUntilAux a p e' true with
  | Except.error a_1 => ¬p a.get = true
  | Except.ok e' => p (bound a e') = true

Tactic:
match improve a e, improve_spec e with
| none, eq =>
  simp only [Bool.not_eq_true]
  rw [eq] at h
  exact Bool.bool_eq_false h
| some e', _ =>
  exact Estimator.improveUntilAux_spec a p e' true

Result:
no goals

Proof state:
case pos
α : Type u_1
ε : Type u_2
inst✝² : Preorder α
a : Thunk α
p : α → Bool
inst✝¹ : Estimator a ε
inst✝ : WellFoundedGT ↑(range (bound a))
e : ε
r : Bool
h : p (bound a e) = true
⊢ match
    if True then pure e
    else
      match improve a e, ⋯ with
      | none, x => Except.error (if r = true then none else some e)
      | some e', x => improveUntilAux a p e' true with
  | Except.error a_1 => ¬p a.get = true
  | Except.ok e' => p (bound a e') = true

Tactic:
exact h

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma coverMincard_univ (T : X → X) {F : Set X} (h : F.Nonempty) (n : ℕ) :
    coverMincard T F univ n = 1

Proof state:
case intro
X : Type u_1
T : X → X
F : Set X
n : ℕ
x : X
h✝ : x ∈ F
this : IsDynCoverOf T F univ n ↑{x}
⊢ ↑{x}.card = 1

Tactic:
rw [Finset.card_singleton, Nat.cast_one]

Result:
no goals

Proof state:
case intro
X : Type u_1
T : X → X
F : Set X
n : ℕ
x : X
h✝ : x ∈ F
this : IsDynCoverOf T F univ n {x}
⊢ coverMincard T F univ n ≤ 1

Tactic:
rw [← Finset.coe_singleton] at this

Result:
case intro
X : Type u_1
T : X → X
F : Set X
n : ℕ
x : X
h✝ : x ∈ F
this : IsDynCoverOf T F univ n ↑{x}
⊢ coverMincard T F univ n ≤ 1

Proof state:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
n : ℕ
⊢ coverMincard T F univ n ≤ 1

Tactic:
rcases h with ⟨x, _⟩

Result:
case intro
X : Type u_1
T : X → X
F : Set X
n : ℕ
x : X
h✝ : x ∈ F
⊢ coverMincard T F univ n ≤ 1

Proof state:
case intro
X : Type u_1
T : X → X
F : Set X
n : ℕ
x : X
h✝ : x ∈ F
this : IsDynCoverOf T F univ n ↑{x}
⊢ coverMincard T F univ n ≤ 1

Tactic:
apply this.coverMincard_le_card.trans_eq

Result:
case intro
X : Type u_1
T : X → X
F : Set X
n : ℕ
x : X
h✝ : x ∈ F
this : IsDynCoverOf T F univ n ↑{x}
⊢ ↑{x}.card = 1

Proof state:
case intro
X : Type u_1
T : X → X
F : Set X
n : ℕ
x : X
h✝ : x ∈ F
⊢ coverMincard T F univ n ≤ 1

Tactic:
have := isDynCoverOf_univ T F n (singleton_nonempty x)

Result:
case intro
X : Type u_1
T : X → X
F : Set X
n : ℕ
x : X
h✝ : x ∈ F
this : IsDynCoverOf T F univ n {x}
⊢ coverMincard T F univ n ≤ 1

Proof state:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
n : ℕ
⊢ coverMincard T F univ n = 1

Tactic:
apply le_antisymm _ ((one_le_coverMincard_iff T F univ n).2 h)

Result:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
n : ℕ
⊢ coverMincard T F univ n ≤ 1
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem iterate_derivative_C_mul (a : R) (p : R[X]) (k : ℕ) :
    derivative^[k] (C a * p) = C a * derivative^[k] p

Proof state:
R : Type u
inst✝ : Semiring R
a : R
p : R[X]
k : ℕ
⊢ (⇑derivative)^[k] (C a * p) = C a * (⇑derivative)^[k] p

Tactic:
simp_rw [← smul_eq_C_mul, iterate_derivative_smul]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
theorem Cofork.app_zero_eq_comp_π_left (s : Cofork f g) : s.ι.app zero = f ≫ s.π

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Cofork f g
⊢ s.ι.app zero = f ≫ s.π

Tactic:
rw [← s.app_one_eq_π, ← s.w left, parallelPair_map_left]

Result:
no goals
-- Mathlib/Data/Rat/Lemmas.lean
theorem substr_num_den' (q r : ℚ) :
    (q - r).num * q.den * r.den = (q.num * r.den - r.num * q.den) * (q - r).den

Proof state:
q r : ℚ
⊢ (q - r).num * ↑q.den * ↑r.den = (q.num * ↑r.den - r.num * ↑q.den) * ↑(q - r).den

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, ← neg_mul, ← num_neg_eq_neg_num, ← den_neg_eq_den r,
  add_num_den' q (-r)]

Result:
no goals