harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/SuccPred/Basic.lean
theorem isMax_iterate_succ_of_eq_of_ne {n m : ℕ} (h_eq : succ^[n] a = succ^[m] a)
    (h_ne : n ≠ m) : IsMax (succ^[n] a)

Proof state:
case inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_ne : n ≠ m
h : n ≤ m
⊢ IsMax (succ^[n] a)

Tactic:
exact isMax_iterate_succ_of_eq_of_lt h_eq (lt_of_le_of_ne h h_ne)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_ne : n ≠ m
⊢ IsMax (succ^[n] a)

Tactic:
rcases le_total n m with h | h

Result:
case inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_ne : n ≠ m
h : n ≤ m
⊢ IsMax (succ^[n] a)

case inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_ne : n ≠ m
h : m ≤ n
⊢ IsMax (succ^[n] a)

Proof state:
case inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_ne : n ≠ m
h : m ≤ n
⊢ IsMax (succ^[m] a)

Tactic:
exact isMax_iterate_succ_of_eq_of_lt h_eq.symm (lt_of_le_of_ne h h_ne.symm)

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_ne : n ≠ m
h : m ≤ n
⊢ IsMax (succ^[n] a)

Tactic:
rw [h_eq]

Result:
case inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_ne : n ≠ m
h : m ≤ n
⊢ IsMax (succ^[m] a)
-- Mathlib/Analysis/LocallyConvex/Bounded.lean
theorem Bornology.IsVonNBounded.restrict_scalars_of_nontrivial
    [NormedField 𝕜] [NormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [Nontrivial 𝕜']
    [Zero E] [TopologicalSpace E]
    [SMul 𝕜 E] [MulAction 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {s : Set E}
    (h : IsVonNBounded 𝕜' s) : IsVonNBounded 𝕜 s

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕜'
inst✝⁶ : NormedAlgebra 𝕜 𝕜'
inst✝⁵ : Nontrivial 𝕜'
inst✝⁴ : Zero E
inst✝³ : TopologicalSpace E
inst✝² : SMul 𝕜 E
inst✝¹ : MulAction 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
s : Set E
h : IsVonNBounded 𝕜' s
⊢ IsVonNBounded 𝕜 s

Tactic:
intro V hV

Result:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕜'
inst✝⁶ : NormedAlgebra 𝕜 𝕜'
inst✝⁵ : Nontrivial 𝕜'
inst✝⁴ : Zero E
inst✝³ : TopologicalSpace E
inst✝² : SMul 𝕜 E
inst✝¹ : MulAction 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
s : Set E
h : IsVonNBounded 𝕜' s
V : Set E
hV : V ∈ 𝓝 0
⊢ Absorbs 𝕜 V s

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕜'
inst✝⁶ : NormedAlgebra 𝕜 𝕜'
inst✝⁵ : Nontrivial 𝕜'
inst✝⁴ : Zero E
inst✝³ : TopologicalSpace E
inst✝² : SMul 𝕜 E
inst✝¹ : MulAction 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
s : Set E
h : IsVonNBounded 𝕜' s
V : Set E
hV : V ∈ 𝓝 0
⊢ Absorbs 𝕜 V s

Tactic:
refine (h hV).restrict_scalars <| AntilipschitzWith.tendsto_cobounded (K := ‖(1 : 𝕜')‖₊⁻¹) ?_

Result:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕜'
inst✝⁶ : NormedAlgebra 𝕜 𝕜'
inst✝⁵ : Nontrivial 𝕜'
inst✝⁴ : Zero E
inst✝³ : TopologicalSpace E
inst✝² : SMul 𝕜 E
inst✝¹ : MulAction 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
s : Set E
h : IsVonNBounded 𝕜' s
V : Set E
hV : V ∈ 𝓝 0
⊢ AntilipschitzWith ‖1‖₊⁻¹ fun x => x • 1

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕜'
inst✝⁶ : NormedAlgebra 𝕜 𝕜'
inst✝⁵ : Nontrivial 𝕜'
inst✝⁴ : Zero E
inst✝³ : TopologicalSpace E
inst✝² : SMul 𝕜 E
inst✝¹ : MulAction 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
s : Set E
h : IsVonNBounded 𝕜' s
V : Set E
hV : V ∈ 𝓝 0
⊢ AntilipschitzWith ‖1‖₊⁻¹ fun x => x • 1

Tactic:
refine AntilipschitzWith.of_le_mul_nndist fun x y ↦ ?_

Result:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕜'
inst✝⁶ : NormedAlgebra 𝕜 𝕜'
inst✝⁵ : Nontrivial 𝕜'
inst✝⁴ : Zero E
inst✝³ : TopologicalSpace E
inst✝² : SMul 𝕜 E
inst✝¹ : MulAction 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
s : Set E
h : IsVonNBounded 𝕜' s
V : Set E
hV : V ∈ 𝓝 0
x y : 𝕜
⊢ nndist x y ≤ ‖1‖₊⁻¹ * nndist (x • 1) (y • 1)

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedRing 𝕜'
inst✝⁶ : NormedAlgebra 𝕜 𝕜'
inst✝⁵ : Nontrivial 𝕜'
inst✝⁴ : Zero E
inst✝³ : TopologicalSpace E
inst✝² : SMul 𝕜 E
inst✝¹ : MulAction 𝕜' E
inst✝ : IsScalarTower 𝕜 𝕜' E
s : Set E
h : IsVonNBounded 𝕜' s
V : Set E
hV : V ∈ 𝓝 0
x y : 𝕜
⊢ nndist x y ≤ ‖1‖₊⁻¹ * nndist (x • 1) (y • 1)

Tactic:
rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← sub_smul, nnnorm_smul, ← div_eq_inv_mul,
  mul_div_cancel_right₀ _ (nnnorm_ne_zero_iff.2 one_ne_zero)]

Result:
no goals
-- Mathlib/Topology/Connected/Clopen.lean
theorem isPreconnected_iff_subset_of_disjoint_closed :
    IsPreconnected s ↔
      ∀ u v, IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

Proof state:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ u ∨ s ⊆ v
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
rcases h with h | h

Result:
case mpr.inl
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ u
⊢ (s ∩ (u ∩ v)).Nonempty

case mpr.inr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ v
⊢ (s ∩ (u ∩ v)).Nonempty

Proof state:
case mp
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty
u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
specialize h u v hu hv hs

Result:
case mp
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
⊢ s ⊆ u ∨ s ⊆ v

Proof state:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
⊢ False

Tactic:
specialize h u v hu hv hs (Set.not_nonempty_iff_eq_empty.mp H)

Result:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ u ∨ s ⊆ v
⊢ False

Proof state:
case mp
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
⊢ ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

Tactic:
intro u v hu hv hs huv

Result:
case mp
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
u v : Set α
hu : IsClosed u
hv : IsClosed v
hs : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v

Proof state:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
⊢ IsPreconnected s

Tactic:
rw [isPreconnected_closed_iff]

Result:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsClosed u → IsClosed v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
⊢ ∀ (t t' : Set α),
    IsClosed t → IsClosed t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty
-- Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
lemma HasFDerivAt.hasLineDerivAt (hf : HasFDerivAt f L x) (v : E) :
    HasLineDerivAt 𝕜 f (L v) x v

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E → F
x : E
L : E →L[𝕜] F
hf : HasFDerivAt f L x
v : E
⊢ HasLineDerivWithinAt 𝕜 f (L v) univ x v

Tactic:
exact hf.hasFDerivWithinAt.hasLineDerivWithinAt v

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E → F
x : E
L : E →L[𝕜] F
hf : HasFDerivAt f L x
v : E
⊢ HasLineDerivAt 𝕜 f (L v) x v

Tactic:
rw [← hasLineDerivWithinAt_univ]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E → F
x : E
L : E →L[𝕜] F
hf : HasFDerivAt f L x
v : E
⊢ HasLineDerivWithinAt 𝕜 f (L v) univ x v
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem contDiffAt_map_inverse [CompleteSpace E] (e : E ≃L[𝕜] F) :
    ContDiffAt 𝕜 n inverse (e : E →L[𝕜] F)

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
a✝ : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp ↑e.symm
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f
⊢ ContDiffAt 𝕜 n inverse ↑e

Tactic:
have : ContinuousLinearMap.inverse = O₁ ∘ Ring.inverse ∘ O₂ := funext (to_ring_inverse e)

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
a✝ : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp ↑e.symm
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
⊢ ContDiffAt 𝕜 n inverse ↑e

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
a✝ : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp ↑e.symm
⊢ ContDiffAt 𝕜 n inverse ↑e

Tactic:
let O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (e.symm : F →L[𝕜] E).comp f

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type uF
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
n : WithTop ℕ∞
inst✝ : CompleteSpace E
e : E ≃L[𝕜] F
a✝ : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp ↑e.symm
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f
⊢ ContDiffAt 𝕜 n inverse ↑e
-- Mathlib/Data/Matrix/Mul.lean
theorem neg_mulVec [Fintype n] (v : n → α) (A : Matrix m n α) : (-A) *ᵥ v = - (A *ᵥ v)

Proof state:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
v : n → α
A : Matrix m n α
x✝ : m
⊢ (-A *ᵥ v) x✝ = (-(A *ᵥ v)) x✝

Tactic:
apply neg_dotProduct

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
v : n → α
A : Matrix m n α
⊢ -A *ᵥ v = -(A *ᵥ v)

Tactic:
ext

Result:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
v : n → α
A : Matrix m n α
x✝ : m
⊢ (-A *ᵥ v) x✝ = (-(A *ᵥ v)) x✝
-- Mathlib/Data/Nat/Lattice.lean
/-- This combines `Nat.iInf_of_empty` with `ciInf_const`. -/
@[simp]
lemma iInf_const_zero {ι : Sort*} : ⨅ _ : ι, 0 = 0 :=
  (isEmpty_or_nonempty ι).elim (fun h ↦ by simp) fun h ↦ sInf_eq_zero.2 <| by simp

Proof state:
ι : Sort u_1
h : IsEmpty ι
⊢ ⨅ x, 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
ι : Sort u_1
h : Nonempty ι
⊢ (0 ∈ range fun x => 0) ∨ (range fun x => 0) = ∅

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean
theorem log_div_sqrt_antitoneOn : AntitoneOn (fun x : ℝ => log x / √x) { x | exp 2 ≤ x }

Proof state:
⊢ AntitoneOn (fun x => log x / √x) {x | rexp 2 ≤ x}

Tactic:
simp_rw [sqrt_eq_rpow]

Result:
⊢ AntitoneOn (fun x => log x / x ^ (1 / 2)) {x | rexp 2 ≤ x}

Proof state:
⊢ AntitoneOn (fun x => log x / x ^ (1 / 2)) {x | rexp 2 ≤ x}

Tactic:
convert @log_div_self_rpow_antitoneOn (1 / 2) (by norm_num)

Result:
case h.e'_6.h.e'_2.h.h.e'_3.h.e'_1
x✝ : ℝ
⊢ 2 = 1 / (1 / 2)

Proof state:
case h.e'_6.h.e'_2.h.h.e'_3.h.e'_1
x✝ : ℝ
⊢ 2 = 1 / (1 / 2)

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ 0 < 1 / 2

Tactic:
norm_num

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Defs.lean
theorem IsNilpotent.map [MonoidWithZero R] [MonoidWithZero S] {r : R} {F : Type*}
    [FunLike F R S] [MonoidWithZeroHomClass F R S] (hr : IsNilpotent r) (f : F) :
    IsNilpotent (f r)

Proof state:
case h
R : Type u_1
S : Type u_2
inst✝³ : MonoidWithZero R
inst✝² : MonoidWithZero S
r : R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : MonoidWithZeroHomClass F R S
hr : IsNilpotent r
f : F
⊢ f r ^ Exists.choose hr = 0

Tactic:
rw [← map_pow, hr.choose_spec, map_zero]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : MonoidWithZero R
inst✝² : MonoidWithZero S
r : R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : MonoidWithZeroHomClass F R S
hr : IsNilpotent r
f : F
⊢ IsNilpotent (f r)

Tactic:
use hr.choose

Result:
case h
R : Type u_1
S : Type u_2
inst✝³ : MonoidWithZero R
inst✝² : MonoidWithZero S
r : R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : MonoidWithZeroHomClass F R S
hr : IsNilpotent r
f : F
⊢ f r ^ Exists.choose hr = 0
-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem secondCountable_of_separable [SeparableSpace α] : SecondCountableTopology α

Proof state:
case intro.intro.intro.intro.refine_2
α : Type u
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → Set (α × α)
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen (t i)
hts : ∀ (i : ℕ), SymmetricRel (t i)
x : α
V : Set α
hxV : x ∈ V
hVo : IsOpen V
⊢ ∃ v ∈ ⋃ x ∈ s, range fun k => ball x (t k), x ∈ v ∧ v ⊆ V

Tactic:
simp only [mem_iUnion₂, mem_range, exists_prop]

Result:
case intro.intro.intro.intro.refine_2
α : Type u
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → Set (α × α)
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen (t i)
hts : ∀ (i : ℕ), SymmetricRel (t i)
x : α
V : Set α
hxV : x ∈ V
hVo : IsOpen V
⊢ ∃ v, (∃ i ∈ s, ∃ y, ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Impl.lean
theorem mergeSortTR_run_eq_mergeSort : {n : Nat} → (l : { l : List α // l.length = n }) → mergeSortTR.run le l = mergeSort l.1 le
  | 0, ⟨[], _⟩
  | 1, ⟨[a], _⟩ => by simp [mergeSortTR.run, mergeSort]
  | n+2, ⟨a :: b :: l, h⟩ => by
    cases h
    simp only [mergeSortTR.run, mergeSortTR.run, mergeSort]
    rw [merge_eq_mergeTR]
    rw [mergeSortTR_run_eq_mergeSort, mergeSortTR_run_eq_mergeSort]

Proof state:
case refl
α : Type u_1
le : α → α → Bool
a b : α
l : List α
⊢ mergeTR (mergeSortTR.run le (splitInTwo ⟨a :: b :: l, ⋯⟩).fst) (mergeSortTR.run le (splitInTwo ⟨a :: b :: l, ⋯⟩).snd)
      le =
    ((splitInTwo ⟨a :: b :: l, ⋯⟩).fst.val.mergeSort le).merge ((splitInTwo ⟨a :: b :: l, ⋯⟩).snd.val.mergeSort le) le

Tactic:
rw [merge_eq_mergeTR]

Result:
case refl
α : Type u_1
le : α → α → Bool
a b : α
l : List α
⊢ mergeTR (mergeSortTR.run le (splitInTwo ⟨a :: b :: l, ⋯⟩).fst) (mergeSortTR.run le (splitInTwo ⟨a :: b :: l, ⋯⟩).snd)
      le =
    mergeTR ((splitInTwo ⟨a :: b :: l, ⋯⟩).fst.val.mergeSort le) ((splitInTwo ⟨a :: b :: l, ⋯⟩).snd.val.mergeSort le) le

Proof state:
α : Type u_1
le : α → α → Bool
n : Nat
a b : α
l : List α
h : (a :: b :: l).length = n + 2
⊢ mergeSortTR.run le ⟨a :: b :: l, h⟩ = ⟨a :: b :: l, h⟩.val.mergeSort le

Tactic:
cases h

Result:
case refl
α : Type u_1
le : α → α → Bool
a b : α
l : List α
⊢ mergeSortTR.run le ⟨a :: b :: l, ⋯⟩ = ⟨a :: b :: l, ⋯⟩.val.mergeSort le

Proof state:
α : Type u_1
le : α → α → Bool
a : α
property✝ : [a].length = 1
⊢ mergeSortTR.run le ⟨[a], property✝⟩ = ⟨[a], property✝⟩.val.mergeSort le

Tactic:
simp [mergeSortTR.run, mergeSort]

Result:
no goals

Proof state:
case refl
α : Type u_1
le : α → α → Bool
a b : α
l : List α
⊢ mergeSortTR.run le ⟨a :: b :: l, ⋯⟩ = ⟨a :: b :: l, ⋯⟩.val.mergeSort le

Tactic:
simp only [mergeSortTR.run, mergeSortTR.run, mergeSort]

Result:
case refl
α : Type u_1
le : α → α → Bool
a b : α
l : List α
⊢ mergeTR (mergeSortTR.run le (splitInTwo ⟨a :: b :: l, ⋯⟩).fst) (mergeSortTR.run le (splitInTwo ⟨a :: b :: l, ⋯⟩).snd)
      le =
    ((splitInTwo ⟨a :: b :: l, ⋯⟩).fst.val.mergeSort le).merge ((splitInTwo ⟨a :: b :: l, ⋯⟩).snd.val.mergeSort le) le

Proof state:
case refl
α : Type u_1
le : α → α → Bool
a b : α
l : List α
⊢ mergeTR (mergeSortTR.run le (splitInTwo ⟨a :: b :: l, ⋯⟩).fst) (mergeSortTR.run le (splitInTwo ⟨a :: b :: l, ⋯⟩).snd)
      le =
    mergeTR ((splitInTwo ⟨a :: b :: l, ⋯⟩).fst.val.mergeSort le) ((splitInTwo ⟨a :: b :: l, ⋯⟩).snd.val.mergeSort le) le

Tactic:
rw [mergeSortTR_run_eq_mergeSort, mergeSortTR_run_eq_mergeSort]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Basic.lean
/-- A category with finite products in which coimage-image comparisons are all isomorphisms
is a normal epi category.
-/
lemma isNormalEpiCategory : IsNormalEpiCategory C where
  normalEpiOfEpi f m := ⟨{
      W := kernel f
      g := kernel.ι _
      w := kernel.condition _
      isColimit

Proof state:
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
aux :
  ∀ (s : CokernelCofork (kernel.ι f)),
    Cofork.π (CokernelCofork.ofπ f ⋯) ≫
        inv (imageMonoFactorisation f).m ≫
          inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) s =
      Cofork.π s
A : CokernelCofork (kernel.ι f)
g : (CokernelCofork.ofπ f ⋯).pt ⟶ A.pt
hg : f ≫ g = Cofork.π A
⊢ g =
    (fun A =>
        inv (imageMonoFactorisation f).m ≫
          inv (coimageImageComparison f) ≫ colimit.desc (parallelPair (kernel.ι f) 0) A)
      A

Tactic:
rw [← cancel_epi f, hg, ← aux, CokernelCofork.π_ofπ]

Result:
no goals
-- Mathlib/Analysis/SumIntegralComparisons.lean
theorem AntitoneOn.sum_le_integral (hf : AntitoneOn f (Icc x₀ (x₀ + a))) :
    (∑ i ∈ Finset.range a, f (x₀ + (i + 1 : ℕ))) ≤ ∫ x in x₀..x₀ + a, f x

Proof state:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ Icc (x₀ + ↑k) (x₀ + ↑(k + 1)) ⊆ Icc x₀ (x₀ + ↑a)

Tactic:
apply Icc_subset_Icc

Result:
case h₁
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ x₀ ≤ x₀ + ↑k

case h₂
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ x₀ + ↑(k + 1) ≤ x₀ + ↑a

Proof state:
case h.e'_3.h.e'_5
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ k < a, IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
⊢ x₀ = x₀ + ↑0

Tactic:
simp only [Nat.cast_zero, add_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem setLIntegral_empty (f : α → ℝ≥0∞) : ∫⁻ x in ∅, f x ∂μ = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α) in ∅, f x ∂μ = 0

Tactic:
rw [Measure.restrict_empty, lintegral_zero_measure]

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem kerase_of_not_mem_keys {a} {l : List (Sigma β)} (h : a ∉ l.keys) : kerase a l = l

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : a ∉ l.keys
⊢ kerase a l = l

Tactic:
induction l with
| nil => rfl
| cons _ _ ih => simp [not_or] at h; simp [h.1, ih h.2]

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
head✝ : Sigma β
tail✝ : List (Sigma β)
ih : a ∉ tail✝.keys → kerase a tail✝ = tail✝
h : a ∉ (head✝ :: tail✝).keys
⊢ kerase a (head✝ :: tail✝) = head✝ :: tail✝

Tactic:
simp [not_or] at h

Result:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
head✝ : Sigma β
tail✝ : List (Sigma β)
ih : a ∉ tail✝.keys → kerase a tail✝ = tail✝
h : ¬a = head✝.fst ∧ a ∉ tail✝.keys
⊢ kerase a (head✝ :: tail✝) = head✝ :: tail✝

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
head✝ : Sigma β
tail✝ : List (Sigma β)
ih : a ∉ tail✝.keys → kerase a tail✝ = tail✝
h : ¬a = head✝.fst ∧ a ∉ tail✝.keys
⊢ kerase a (head✝ :: tail✝) = head✝ :: tail✝

Tactic:
simp [h.1, ih h.2]

Result:
no goals

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
h : a ∉ [].keys
⊢ kerase a [] = []

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem get_tails : ∀ (n : ℕ) (s : Stream' α), get (tails s) n = drop n (tail s)

Proof state:
case zero
α : Type u
s✝ : Stream' α
⊢ s✝.tails.get 0 = drop 0 s✝.tail

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
⊢ ∀ (n : ℕ) (s : Stream' α), s.tails.get n = drop n s.tail

Tactic:
intro n

Result:
α : Type u
n : ℕ
⊢ ∀ (s : Stream' α), s.tails.get n = drop n s.tail

Proof state:
case succ
α : Type u
n' : ℕ
ih : ∀ (s : Stream' α), s.tails.get n' = drop n' s.tail
⊢ ∀ (s : Stream' α), s.tails.get (n' + 1) = drop (n' + 1) s.tail

Tactic:
intro s

Result:
case succ
α : Type u
n' : ℕ
ih : ∀ (s : Stream' α), s.tails.get n' = drop n' s.tail
s : Stream' α
⊢ s.tails.get (n' + 1) = drop (n' + 1) s.tail

Proof state:
α : Type u
n : ℕ
⊢ ∀ (s : Stream' α), s.tails.get n = drop n s.tail

Tactic:
induction' n with n' ih

Result:
case zero
α : Type u
⊢ ∀ (s : Stream' α), s.tails.get 0 = drop 0 s.tail

case succ
α : Type u
n' : ℕ
ih : ∀ (s : Stream' α), s.tails.get n' = drop n' s.tail
⊢ ∀ (s : Stream' α), s.tails.get (n' + 1) = drop (n' + 1) s.tail

Proof state:
case succ
α : Type u
n' : ℕ
ih : ∀ (s : Stream' α), s.tails.get n' = drop n' s.tail
s : Stream' α
⊢ s.tails.get (n' + 1) = drop (n' + 1) s.tail

Tactic:
rw [get_succ, drop_succ, tails_eq, tail_cons, ih]

Result:
no goals

Proof state:
case zero
α : Type u
⊢ ∀ (s : Stream' α), s.tails.get 0 = drop 0 s.tail

Tactic:
intros

Result:
case zero
α : Type u
s✝ : Stream' α
⊢ s✝.tails.get 0 = drop 0 s✝.tail
-- Mathlib/Order/Filter/AtTopBot/CompleteLattice.lean
theorem Subsingleton.atTop_eq (α) [Subsingleton α] [Preorder α] : (atTop : Filter α) = ⊤

Proof state:
α : Type u_6
inst✝¹ : Subsingleton α
inst✝ : Preorder α
⊢ atTop = ⊤

Tactic:
refine top_unique fun s hs x => ?_

Result:
α : Type u_6
inst✝¹ : Subsingleton α
inst✝ : Preorder α
s : Set α
hs : s ∈ atTop
x : α
⊢ x ∈ s

Proof state:
α : Type u_6
inst✝¹ : Subsingleton α
inst✝ : Preorder α
s : Set α
x : α
hs : Ici x ⊆ s
⊢ x ∈ s

Tactic:
exact hs left_mem_Ici

Result:
no goals

Proof state:
α : Type u_6
inst✝¹ : Subsingleton α
inst✝ : Preorder α
s : Set α
hs : s ∈ atTop
x : α
⊢ x ∈ s

Tactic:
rw [atTop, ciInf_subsingleton x, mem_principal] at hs

Result:
α : Type u_6
inst✝¹ : Subsingleton α
inst✝ : Preorder α
s : Set α
x : α
hs : Ici x ⊆ s
⊢ x ∈ s