harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem mul_meas_ge_le_integral_of_nonneg {f : α → ℝ} (hf_nonneg : 0 ≤ᵐ[μ] f)
    (hf_int : Integrable f μ) (ε : ℝ) : ε * (μ { x | ε ≤ f x }).toReal ≤ ∫ x, f x ∂μ

Proof state:
case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hf_int : Integrable f μ
ε : ℝ
hμ : μ {x | ε ≤ f x} = ⊤
⊢ ε * (μ {x | ε ≤ f x}).toReal ≤ ∫ (x : α), f x ∂μ

Tactic:
simpa [hμ] using integral_nonneg_of_ae hf_nonneg

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hf_int : Integrable f μ
ε : ℝ
⊢ ε * (μ {x | ε ≤ f x}).toReal ≤ ∫ (x : α), f x ∂μ

Tactic:
rcases eq_top_or_lt_top (μ {x | ε ≤ f x}) with hμ | hμ

Result:
case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hf_int : Integrable f μ
ε : ℝ
hμ : μ {x | ε ≤ f x} = ⊤
⊢ ε * (μ {x | ε ≤ f x}).toReal ≤ ∫ (x : α), f x ∂μ

case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hf_int : Integrable f μ
ε : ℝ
hμ : μ {x | ε ≤ f x} < ⊤
⊢ ε * (μ {x | ε ≤ f x}).toReal ≤ ∫ (x : α), f x ∂μ

Proof state:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hf_int : Integrable f μ
ε : ℝ
hμ : μ {x | ε ≤ f x} < ⊤
this : Fact (μ {x | ε ≤ f x} < ⊤)
⊢ ε * (μ {x | ε ≤ f x}).toReal ≤ ∫ (x : α), f x ∂μ

Tactic:
calc
  ε * (μ { x | ε ≤ f x }).toReal = ∫ _ in {x | ε ≤ f x}, ε ∂μ := by simp [mul_comm]
  _ ≤ ∫ x in {x | ε ≤ f x}, f x ∂μ :=
    integral_mono_ae (integrable_const _) (hf_int.mono_measure μ.restrict_le_self) <|
      ae_restrict_mem₀ <| hf_int.aemeasurable.nullMeasurable measurableSet_Ici
  _ ≤ _ := integral_mono_measure μ.restrict_le_self hf_nonneg hf_int

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hf_int : Integrable f μ
ε : ℝ
hμ : μ {x | ε ≤ f x} < ⊤
this : Fact (μ {x | ε ≤ f x} < ⊤)
⊢ ε * (μ {x | ε ≤ f x}).toReal = ∫ (x : α) in {x | ε ≤ f x}, ε ∂μ

Tactic:
simp [mul_comm]

Result:
no goals

Proof state:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hf_int : Integrable f μ
ε : ℝ
hμ : μ {x | ε ≤ f x} < ⊤
⊢ ε * (μ {x | ε ≤ f x}).toReal ≤ ∫ (x : α), f x ∂μ

Tactic:
have := Fact.mk hμ

Result:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf_nonneg : 0 ≤ᶠ[ae μ] f
hf_int : Integrable f μ
ε : ℝ
hμ : μ {x | ε ≤ f x} < ⊤
this : Fact (μ {x | ε ≤ f x} < ⊤)
⊢ ε * (μ {x | ε ≤ f x}).toReal ≤ ∫ (x : α), f x ∂μ
-- Mathlib/Algebra/Homology/BifunctorAssociator.lean
@[reassoc]
lemma mapBifunctorAssociatorX_hom_D₃ (j j' : ι₄) :
    (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom ≫
      mapBifunctor₂₃.D₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j' =
        mapBifunctor₁₂.D₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' ≫
        (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j').hom

Proof state:
case neg
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝³³ : Category.{u_16, u_1} C₁
inst✝³² : Category.{u_17, u_2} C₂
inst✝³¹ : Category.{u_15, u_5} C₃
inst✝³⁰ : Category.{u_13, u_6} C₄
inst✝²⁹ : Category.{u_14, u_3} C₁₂
inst✝²⁸ : Category.{u_18, u_4} C₂₃
inst✝²⁷ : HasZeroMorphisms C₁
inst✝²⁶ : HasZeroMorphisms C₂
inst✝²⁵ : HasZeroMorphisms C₃
inst✝²⁴ : Preadditive C₁₂
inst✝²³ : Preadditive C₂₃
inst✝²² : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
inst✝²¹ : F₁₂.PreservesZeroMorphisms
inst✝²⁰ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝¹⁹ : G.Additive
inst✝¹⁸ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
inst✝¹⁷ : G₂₃.PreservesZeroMorphisms
inst✝¹⁶ : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹⁵ : F.PreservesZeroMorphisms
inst✝¹⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst✝¹³ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₂₃ : ComplexShape ι₂₃
c₄ : ComplexShape ι₄
inst✝¹² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹¹ : TotalComplexShape c₁₂ c₃ c₄
inst✝¹⁰ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁹ : TotalComplexShape c₁ c₂₃ c₄
inst✝⁸ : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝⁷ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝⁶ : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝⁵ : DecidableEq ι₁₂
inst✝⁴ : DecidableEq ι₂₃
inst✝³ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
inst✝² : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
inst✝¹ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
inst✝ : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄
j j' : ι₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
h₁ : ¬c₃.Rel i₃ (c₃.next i₃)
⊢ ((associator.hom.app (K₁.X i₁)).app (K₂.X i₂)).app (K₃.X i₃) ≫
      mapBifunctor₂₃.d₃ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j' =
    mapBifunctor₁₂.d₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j' ≫
      (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j').hom

Tactic:
rw [mapBifunctor₁₂.d₃_eq_zero _ _ _ _ _ _ _ _ _ _ _ h₁,
  mapBifunctor₂₃.d₃_eq_zero _ _ _ _ _ _ _ _ _ _ _ _ h₁, comp_zero, zero_comp]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Basic.lean
theorem lift_unique (F : MonoidAlgebra k G →ₐ[k] A) (f : MonoidAlgebra k G) :
    F f = f.sum fun a b => b • F (single a 1)

Proof state:
k : Type u₁
G : Type u₂
inst✝³ : CommSemiring k
inst✝² : Monoid G
A : Type u₃
inst✝¹ : Semiring A
inst✝ : Algebra k A
F : MonoidAlgebra k G →ₐ[k] A
f : MonoidAlgebra k G
⊢ F f = sum f fun a b => b • F (single a 1)

Tactic:
conv_lhs =>
  rw [lift_unique' F]
  simp [lift_apply]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem nthRoots_zero (r : R) : nthRoots 0 r = 0

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
r : R
⊢ nthRoots 0 r = 0

Tactic:
simp only [empty_eq_zero, pow_zero, nthRoots, ← C_1, ← C_sub, roots_C]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem next : ∀ {it}, ValidFor l (c :: r) it → ValidFor (c :: l) r it.next
  | it, h => by
    cases h.out'
    simp only [Iterator.next, next_of_valid l.reverse c r]
    rw [← List.reverseAux_eq, utf8Len_reverse]; constructor

Proof state:
case refl
l : List Char
c : Char
r : List Char
h : ValidFor l (c :: r) { s := { data := l.reverse ++ c :: r }, i := { byteIdx := utf8Len l.reverse } }
⊢ ValidFor (c :: l) r { s := { data := l.reverse ++ c :: r }, i := { byteIdx := utf8Len l.reverse + c.utf8Size } }

Tactic:
rw [← List.reverseAux_eq, utf8Len_reverse]

Result:
case refl
l : List Char
c : Char
r : List Char
h : ValidFor l (c :: r) { s := { data := l.reverse ++ c :: r }, i := { byteIdx := utf8Len l.reverse } }
⊢ ValidFor (c :: l) r { s := { data := l.reverseAux (c :: r) }, i := { byteIdx := utf8Len l + c.utf8Size } }

Proof state:
case refl
l : List Char
c : Char
r : List Char
h : ValidFor l (c :: r) { s := { data := l.reverse ++ c :: r }, i := { byteIdx := utf8Len l.reverse } }
⊢ ValidFor (c :: l) r { s := { data := l.reverseAux (c :: r) }, i := { byteIdx := utf8Len l + c.utf8Size } }

Tactic:
constructor

Result:
no goals

Proof state:
case refl
l : List Char
c : Char
r : List Char
h : ValidFor l (c :: r) { s := { data := l.reverse ++ c :: r }, i := { byteIdx := utf8Len l.reverse } }
⊢ ValidFor (c :: l) r { s := { data := l.reverse ++ c :: r }, i := { byteIdx := utf8Len l.reverse } }.next

Tactic:
simp only [Iterator.next, next_of_valid l.reverse c r]

Result:
case refl
l : List Char
c : Char
r : List Char
h : ValidFor l (c :: r) { s := { data := l.reverse ++ c :: r }, i := { byteIdx := utf8Len l.reverse } }
⊢ ValidFor (c :: l) r { s := { data := l.reverse ++ c :: r }, i := { byteIdx := utf8Len l.reverse + c.utf8Size } }

Proof state:
l : List Char
c : Char
r : List Char
it : Iterator
h : ValidFor l (c :: r) it
⊢ ValidFor (c :: l) r it.next

Tactic:
cases h.out'

Result:
case refl
l : List Char
c : Char
r : List Char
h : ValidFor l (c :: r) { s := { data := l.reverse ++ c :: r }, i := { byteIdx := utf8Len l.reverse } }
⊢ ValidFor (c :: l) r { s := { data := l.reverse ++ c :: r }, i := { byteIdx := utf8Len l.reverse } }.next
-- Mathlib/Order/CompleteBooleanAlgebra.lean
theorem iSup_disjoint_iff {f : ι → α} : Disjoint (⨆ i, f i) a ↔ ∀ i, Disjoint (f i) a

Proof state:
α : Type u
ι : Sort w
inst✝ : Frame α
a : α
f : ι → α
⊢ Disjoint (⨆ i, f i) a ↔ ∀ (i : ι), Disjoint (f i) a

Tactic:
simp only [disjoint_iff, iSup_inf_eq, iSup_eq_bot]

Result:
no goals
-- Mathlib/Analysis/Convex/Join.lean
theorem convexHull_insert (hs : s.Nonempty) :
    convexHull 𝕜 (insert x s) = convexJoin 𝕜 {x} (convexHull 𝕜 s)

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
hs : s.Nonempty
⊢ (convexHull 𝕜) (insert x s) = convexJoin 𝕜 {x} ((convexHull 𝕜) s)

Tactic:
rw [insert_eq, convexHull_union (singleton_nonempty _) hs, convexHull_singleton]

Result:
no goals
-- Mathlib/Topology/MetricSpace/IsometricSMul.lean
theorem preimage_mul_right_closedBall [IsometricSMul Gᵐᵒᵖ G] (a b : G) (r : ℝ≥0∞) :
    (fun x => x * a) ⁻¹' closedBall b r = closedBall (b / a) r

Proof state:
G : Type v
inst✝² : Group G
inst✝¹ : PseudoEMetricSpace G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
⊢ (fun x => x * a) ⁻¹' closedBall b r = closedBall (b * a⁻¹) r

Tactic:
exact preimage_smul_closedBall (MulOpposite.op a) b r

Result:
no goals

Proof state:
G : Type v
inst✝² : Group G
inst✝¹ : PseudoEMetricSpace G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
⊢ (fun x => x * a) ⁻¹' closedBall b r = closedBall (b / a) r

Tactic:
rw [div_eq_mul_inv]

Result:
G : Type v
inst✝² : Group G
inst✝¹ : PseudoEMetricSpace G
inst✝ : IsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
⊢ (fun x => x * a) ⁻¹' closedBall b r = closedBall (b * a⁻¹) r
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem getElem?_mapFinIdx (a : Array α) (f : (i : Nat) → α → (h : i < a.size) → β) (i : Nat) :
    (a.mapFinIdx f)[i]? =
      a[i]?.pbind fun b h => f i b (getElem?_eq_some_iff.1 h).1

Proof state:
α : Type u_1
β : Type u_2
a : Array α
f : (i : Nat) → α → i < a.size → β
i : Nat
⊢ (a.mapFinIdx f)[i]? = a[i]?.pbind fun b h => some (f i b ⋯)

Tactic:
simp only [getElem?_def, size_mapFinIdx, getElem_mapFinIdx]

Result:
α : Type u_1
β : Type u_2
a : Array α
f : (i : Nat) → α → i < a.size → β
i : Nat
⊢ (if h : i < a.size then some (f i a[i] ⋯) else none) =
    (if h : i < a.size then some a[i] else none).pbind fun a_1 h => some (f i a_1 ⋯)

Proof state:
α : Type u_1
β : Type u_2
a : Array α
f : (i : Nat) → α → i < a.size → β
i : Nat
⊢ (if h : i < a.size then some (f i a[i] ⋯) else none) =
    (if h : i < a.size then some a[i] else none).pbind fun a_1 h => some (f i a_1 ⋯)

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Data/ZMod/Units.lean
@[simp]
lemma unitsMap_self (n : ℕ) : unitsMap (dvd_refl n) = MonoidHom.id _

Proof state:
n : ℕ
⊢ unitsMap ⋯ = MonoidHom.id (ZMod n)ˣ

Tactic:
simp [unitsMap, castHom_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem getElem?_zipWith' {f : α → β → γ} {i : Nat} :
    (zipWith f l₁ l₂)[i]? = (l₁[i]?.map f).bind fun g => l₂[i]?.map g

Proof state:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l₂ : List β
i : Nat
⊢ (zipWith f [] l₂)[i]? = (Option.map f [][i]?).bind fun g => Option.map g l₂[i]?

Tactic:
rw [zipWith] <;> simp

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
head : α
tail : List α
tail_ih✝ :
  ∀ {l₂ : List β} {i : Nat}, (zipWith f tail l₂)[i]? = (Option.map f tail[i]?).bind fun g => Option.map g l₂[i]?
i : Nat
head✝ : β
tail✝ : List β
⊢ (zipWith f (head :: tail) (head✝ :: tail✝))[i]? =
    (Option.map f (head :: tail)[i]?).bind fun g => Option.map g (head✝ :: tail✝)[i]?

Tactic:
cases i <;> simp_all

Result:
no goals

Proof state:
case cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
head : α
tail : List α
tail_ih✝ :
  ∀ {l₂ : List β} {i : Nat}, (zipWith f tail l₂)[i]? = (Option.map f tail[i]?).bind fun g => Option.map g l₂[i]?
i : Nat
⊢ (zipWith f (head :: tail) [])[i]? = (Option.map f (head :: tail)[i]?).bind fun g => Option.map g [][i]?

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
head : α
tail : List α
tail_ih✝ :
  ∀ {l₂ : List β} {i : Nat}, (zipWith f tail l₂)[i]? = (Option.map f tail[i]?).bind fun g => Option.map g l₂[i]?
l₂ : List β
i : Nat
⊢ (zipWith f (head :: tail) l₂)[i]? = (Option.map f (head :: tail)[i]?).bind fun g => Option.map g l₂[i]?

Tactic:
cases l₂

Result:
case cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
head : α
tail : List α
tail_ih✝ :
  ∀ {l₂ : List β} {i : Nat}, (zipWith f tail l₂)[i]? = (Option.map f tail[i]?).bind fun g => Option.map g l₂[i]?
i : Nat
⊢ (zipWith f (head :: tail) [])[i]? = (Option.map f (head :: tail)[i]?).bind fun g => Option.map g [][i]?

case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
head : α
tail : List α
tail_ih✝ :
  ∀ {l₂ : List β} {i : Nat}, (zipWith f tail l₂)[i]? = (Option.map f tail[i]?).bind fun g => Option.map g l₂[i]?
i : Nat
head✝ : β
tail✝ : List β
⊢ (zipWith f (head :: tail) (head✝ :: tail✝))[i]? =
    (Option.map f (head :: tail)[i]?).bind fun g => Option.map g (head✝ :: tail✝)[i]?
-- Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
/-- The iterated derivative commutes with shifting the function by a constant on the left. -/
lemma iteratedDeriv_comp_const_add (n : ℕ) (f : 𝕜 → F) (s : 𝕜) :
    iteratedDeriv n (fun z ↦ f (s + z)) = fun t ↦ iteratedDeriv n f (s + t)

Proof state:
case succ
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : 𝕜
n : ℕ
IH : (iteratedDeriv n fun z => f (s + z)) = fun t => iteratedDeriv n f (s + t)
⊢ (iteratedDeriv (n + 1) fun z => f (s + z)) = fun t => iteratedDeriv (n + 1) f (s + t)

Tactic:
simpa only [iteratedDeriv_succ, IH] using funext <| deriv_comp_const_add _ s

Result:
no goals

Proof state:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
s : 𝕜
⊢ (iteratedDeriv n fun z => f (s + z)) = fun t => iteratedDeriv n f (s + t)

Tactic:
induction n with
| zero => simp only [iteratedDeriv_zero]
| succ n IH =>
  simpa only [iteratedDeriv_succ, IH] using funext <| deriv_comp_const_add _ s

Result:
no goals

Proof state:
case zero
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : 𝕜
⊢ (iteratedDeriv 0 fun z => f (s + z)) = fun t => iteratedDeriv 0 f (s + t)

Tactic:
simp only [iteratedDeriv_zero]

Result:
no goals
-- Mathlib/Data/Real/Pi/Bounds.lean
theorem pi_lower_bound_start (n : ℕ) {a}
    (h : sqrtTwoAddSeries ((0 : ℕ) / (1 : ℕ)) n ≤ (2 : ℝ) - (a / (2 : ℝ) ^ (n + 1)) ^ 2) :
    a < π

Proof state:
n : ℕ
a : ℝ
h : (↑0 / ↑1).sqrtTwoAddSeries n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ 0 = ↑0 / ↑1

Tactic:
rw [Nat.cast_zero, zero_div]

Result:
no goals

Proof state:
n : ℕ
a : ℝ
h : (↑0 / ↑1).sqrtTwoAddSeries n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ a < π

Tactic:
refine lt_of_le_of_lt ?_ (pi_gt_sqrtTwoAddSeries n)

Result:
n : ℕ
a : ℝ
h : (↑0 / ↑1).sqrtTwoAddSeries n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ a ≤ 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n)

Proof state:
n : ℕ
a : ℝ
h : (↑0 / ↑1).sqrtTwoAddSeries n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ a ≤ √(2 - sqrtTwoAddSeries 0 n) * 2 ^ (n + 1)

Tactic:
refine (div_le_iff₀ (pow_pos (by norm_num) _)).mp (le_sqrt_of_sq_le ?_)

Result:
n : ℕ
a : ℝ
h : (↑0 / ↑1).sqrtTwoAddSeries n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ (a / 2 ^ (n + 1)) ^ 2 ≤ 2 - sqrtTwoAddSeries 0 n

Proof state:
n : ℕ
a : ℝ
h : (↑0 / ↑1).sqrtTwoAddSeries n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ 0 < 2

Tactic:
norm_num

Result:
no goals

Proof state:
n : ℕ
a : ℝ
h : (↑0 / ↑1).sqrtTwoAddSeries n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ a ≤ 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n)

Tactic:
rw [mul_comm]

Result:
n : ℕ
a : ℝ
h : (↑0 / ↑1).sqrtTwoAddSeries n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ a ≤ √(2 - sqrtTwoAddSeries 0 n) * 2 ^ (n + 1)

Proof state:
n : ℕ
a : ℝ
h : (↑0 / ↑1).sqrtTwoAddSeries n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2
⊢ (a / 2 ^ (n + 1)) ^ 2 ≤ 2 - sqrtTwoAddSeries 0 n

Tactic:
rwa [le_sub_comm, show (0 : ℝ) = (0 : ℕ) / (1 : ℕ) by rw [Nat.cast_zero, zero_div]]

Result:
no goals
-- Mathlib/Data/Set/Finite/Lattice.lean
theorem finite_subset_iUnion {s : Set α} (hs : s.Finite) {ι} {t : ι → Set α} (h : s ⊆ ⋃ i, t i) :
    ∃ I : Set ι, I.Finite ∧ s ⊆ ⋃ i ∈ I, t i

Proof state:
α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ i, t i
this : Finite ↑s
f : ↑s → ι
hf : ∀ (x : ↑s), ↑x ∈ t (f x)
x : α
hx : x ∈ s
⊢ ∃ i, x ∈ t (f i)

Tactic:
exact ⟨⟨x, hx⟩, hf _⟩

Result:
no goals

Proof state:
α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ i, t i
this : Finite ↑s
⊢ ∃ I, I.Finite ∧ s ⊆ ⋃ i ∈ I, t i

Tactic:
choose f hf using show ∀ x : s, ∃ i, x.1 ∈ t i by simpa [subset_def] using h

Result:
α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ i, t i
this : Finite ↑s
f : ↑s → ι
hf : ∀ (x : ↑s), ↑x ∈ t (f x)
⊢ ∃ I, I.Finite ∧ s ⊆ ⋃ i ∈ I, t i

Proof state:
α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ i, t i
this : Finite ↑s
f : ↑s → ι
hf : ∀ (x : ↑s), ↑x ∈ t (f x)
⊢ ∃ I, I.Finite ∧ s ⊆ ⋃ i ∈ I, t i

Tactic:
refine ⟨range f, finite_range f, fun x hx => ?_⟩

Result:
α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ i, t i
this : Finite ↑s
f : ↑s → ι
hf : ∀ (x : ↑s), ↑x ∈ t (f x)
x : α
hx : x ∈ s
⊢ x ∈ ⋃ i ∈ range f, t i

Proof state:
α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ i, t i
this : Finite ↑s
⊢ ∀ (x : ↑s), ∃ i, ↑x ∈ t i

Tactic:
simpa [subset_def] using h

Result:
no goals

Proof state:
α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ i, t i
⊢ ∃ I, I.Finite ∧ s ⊆ ⋃ i ∈ I, t i

Tactic:
have := hs.to_subtype

Result:
α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ i, t i
this : Finite ↑s
⊢ ∃ I, I.Finite ∧ s ⊆ ⋃ i ∈ I, t i

Proof state:
α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ i, t i
this : Finite ↑s
f : ↑s → ι
hf : ∀ (x : ↑s), ↑x ∈ t (f x)
x : α
hx : x ∈ s
⊢ x ∈ ⋃ i ∈ range f, t i

Tactic:
rw [biUnion_range, mem_iUnion]

Result:
α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ i, t i
this : Finite ↑s
f : ↑s → ι
hf : ∀ (x : ↑s), ↑x ∈ t (f x)
x : α
hx : x ∈ s
⊢ ∃ i, x ∈ t (f i)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem getLsbD_neg {i : Nat} {x : BitVec w} :
    getLsbD (-x) i =
      (getLsbD x i ^^ decide (i < w) && decide (∃ j < i, getLsbD x j = true))

Proof state:
w : Nat
x : BitVec w
this : 0 < w
n✝ : Nat
hi : n✝ + 1 < w
h : ∀ (j : Nat), j ≤ n✝ → j < w ∧ x.getLsbD j = false
j : Nat
hj : j < n✝ + 1
⊢ j ≤ n✝

Tactic:
omega

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem support_single_ne_zero {i : ι} {b : β i} (hb : b ≠ 0) : (single i b).support = {i}

Proof state:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
b : β i
hb : b ≠ 0
⊢ (single i b).support = {i}

Tactic:
ext j

Result:
case h
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
b : β i
hb : b ≠ 0
j : ι
⊢ j ∈ (single i b).support ↔ j ∈ {i}

Proof state:
case neg
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
b : β i
hb : b ≠ 0
j : ι
h : ¬i = j
⊢ j ∈ (single i b).support ↔ j ∈ {i}

Tactic:
simp [Ne.symm h, h]

Result:
no goals

Proof state:
case pos
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
b : β i
hb : b ≠ 0
⊢ i ∈ (single i b).support ↔ i ∈ {i}

Tactic:
simp [hb]

Result:
no goals

Proof state:
case pos
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
b : β i
hb : b ≠ 0
j : ι
h : i = j
⊢ j ∈ (single i b).support ↔ j ∈ {i}

Tactic:
subst h

Result:
case pos
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
b : β i
hb : b ≠ 0
⊢ i ∈ (single i b).support ↔ i ∈ {i}

Proof state:
case h
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
b : β i
hb : b ≠ 0
j : ι
⊢ j ∈ (single i b).support ↔ j ∈ {i}

Tactic:
by_cases h : i = j

Result:
case pos
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
b : β i
hb : b ≠ 0
j : ι
h : i = j
⊢ j ∈ (single i b).support ↔ j ∈ {i}

case neg
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
b : β i
hb : b ≠ 0
j : ι
h : ¬i = j
⊢ j ∈ (single i b).support ↔ j ∈ {i}
-- Mathlib/CategoryTheory/Functor/Flat.lean
theorem flat_iff_lan_flat (F : C ⥤ D) :
    RepresentablyFlat F ↔ RepresentablyFlat (F.op.lan : _ ⥤ Dᵒᵖ ⥤ Type u₁) :=
  ⟨fun _ => inferInstance, fun H => by
    haveI := preservesFiniteLimits_of_flat (F.op.lan : _ ⥤ Dᵒᵖ ⥤ Type u₁)
    haveI : PreservesFiniteLimits F

Proof state:
case h
C D : Type u₁
inst✝² : SmallCategory C
inst✝¹ : SmallCategory D
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat F.op.lan
this : PreservesFiniteLimits F.op.lan
J✝ : Type u₁
𝒥✝ : SmallCategory J✝
x✝ : FinCategory J✝
⊢ PreservesLimitsOfShape J✝ F

Tactic:
apply preservesLimit_of_lan_preservesLimit

Result:
no goals

Proof state:
C D : Type u₁
inst✝² : SmallCategory C
inst✝¹ : SmallCategory D
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat F.op.lan
this : PreservesFiniteLimits F.op.lan
⊢ RepresentablyFlat F

Tactic:
haveI : PreservesFiniteLimits F := by
  apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize.{u₁}
  intros; apply preservesLimit_of_lan_preservesLimit

Result:
C D : Type u₁
inst✝² : SmallCategory C
inst✝¹ : SmallCategory D
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat F.op.lan
this✝ : PreservesFiniteLimits F.op.lan
this : PreservesFiniteLimits F
⊢ RepresentablyFlat F

Proof state:
C D : Type u₁
inst✝² : SmallCategory C
inst✝¹ : SmallCategory D
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat F.op.lan
this✝ : PreservesFiniteLimits F.op.lan
this : PreservesFiniteLimits F
⊢ RepresentablyFlat F

Tactic:
apply flat_of_preservesFiniteLimits

Result:
no goals

Proof state:
case h
C D : Type u₁
inst✝² : SmallCategory C
inst✝¹ : SmallCategory D
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat F.op.lan
this : PreservesFiniteLimits F.op.lan
⊢ ∀ (J : Type u₁) {𝒥 : SmallCategory J}, FinCategory J → PreservesLimitsOfShape J F

Tactic:
intros

Result:
case h
C D : Type u₁
inst✝² : SmallCategory C
inst✝¹ : SmallCategory D
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat F.op.lan
this : PreservesFiniteLimits F.op.lan
J✝ : Type u₁
𝒥✝ : SmallCategory J✝
x✝ : FinCategory J✝
⊢ PreservesLimitsOfShape J✝ F

Proof state:
C D : Type u₁
inst✝² : SmallCategory C
inst✝¹ : SmallCategory D
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat F.op.lan
this : PreservesFiniteLimits F.op.lan
⊢ PreservesFiniteLimits F

Tactic:
apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize.{u₁}

Result:
case h
C D : Type u₁
inst✝² : SmallCategory C
inst✝¹ : SmallCategory D
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat F.op.lan
this : PreservesFiniteLimits F.op.lan
⊢ ∀ (J : Type u₁) {𝒥 : SmallCategory J}, FinCategory J → PreservesLimitsOfShape J F

Proof state:
C D : Type u₁
inst✝² : SmallCategory C
inst✝¹ : SmallCategory D
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat F.op.lan
⊢ RepresentablyFlat F

Tactic:
haveI := preservesFiniteLimits_of_flat (F.op.lan : _ ⥤ Dᵒᵖ ⥤ Type u₁)

Result:
C D : Type u₁
inst✝² : SmallCategory C
inst✝¹ : SmallCategory D
inst✝ : HasFiniteLimits C
F : C ⥤ D
H : RepresentablyFlat F.op.lan
this : PreservesFiniteLimits F.op.lan
⊢ RepresentablyFlat F