harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filter_cons :
    (x :: xs : List α).filter p = if p x then x :: (xs.filter p) else xs.filter p

Proof state:
α : Type u_1
x : α
xs : List α
p : α → Bool
⊢ filter p (x :: xs) = if p x = true then x :: filter p xs else filter p xs

Tactic:
split <;> simp [*]

Result:
no goals
-- Mathlib/Analysis/Convex/Segment.lean
theorem right_mem_openSegment_iff [DenselyOrdered 𝕜] [NoZeroSMulDivisors 𝕜 E] :
    y ∈ openSegment 𝕜 x y ↔ x = y

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
x y : E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
⊢ y ∈ openSegment 𝕜 x y ↔ x = y

Tactic:
rw [openSegment_symm, left_mem_openSegment_iff, eq_comm]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem basicOpen_eq_bot_iff (f : R) : basicOpen f = ⊥ ↔ IsNilpotent f

Proof state:
R : Type u
inst✝ : CommSemiring R
f : R
⊢ (zeroLocus {f})ᶜ = ↑⊥ ↔ IsNilpotent f

Tactic:
simp only [Set.eq_univ_iff_forall, Set.singleton_subset_iff, TopologicalSpace.Opens.coe_bot,
  nilpotent_iff_mem_prime, Set.compl_empty_iff, mem_zeroLocus, SetLike.mem_coe]

Result:
R : Type u
inst✝ : CommSemiring R
f : R
⊢ (∀ (x : PrimeSpectrum R), f ∈ x.asIdeal) ↔ ∀ (J : Ideal R), J.IsPrime → f ∈ J

Proof state:
R : Type u
inst✝ : CommSemiring R
f : R
⊢ basicOpen f = ⊥ ↔ IsNilpotent f

Tactic:
rw [← TopologicalSpace.Opens.coe_inj, basicOpen_eq_zeroLocus_compl]

Result:
R : Type u
inst✝ : CommSemiring R
f : R
⊢ (zeroLocus {f})ᶜ = ↑⊥ ↔ IsNilpotent f

Proof state:
R : Type u
inst✝ : CommSemiring R
f : R
⊢ (∀ (x : PrimeSpectrum R), f ∈ x.asIdeal) ↔ ∀ (J : Ideal R), J.IsPrime → f ∈ J

Tactic:
exact ⟨fun h I hI => h ⟨I, hI⟩, fun h ⟨I, hI⟩ => h I hI⟩

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/ErdosKaplansky.lean
theorem rank_lt_rank_dual {K V : Type u} [Field K] [AddCommGroup V] [Module K V]
    (h : ℵ₀ ≤ Module.rank K V) : Module.rank K V < Module.rank K (V →ₗ[K] K)

Proof state:
case h.e'_3
K V : Type u
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank K V = lift.{u, u} (Module.rank K V)

Tactic:
rw [lift_id]

Result:
no goals

Proof state:
K V : Type u
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank K V < Module.rank K (V →ₗ[K] K)

Tactic:
convert lift_rank_lt_rank_dual h

Result:
case h.e'_3
K V : Type u
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank K V = lift.{u, u} (Module.rank K V)
-- Mathlib/Combinatorics/Additive/Corner/Roth.lean
theorem rothNumberNat_isLittleO_id :
    IsLittleO atTop (fun N ↦ (rothNumberNat N : ℝ)) (fun N ↦ (N : ℝ))

Proof state:
case intro.intro.intro
ε : ℝ
hε : 0 < ε
n : ℕ
hn : n ≥ cornersTheoremBound (ε / 3)
A : Finset ℕ
hs₁ : A ⊆ range n
hs₂ : #A = rothNumberNat n
hs₃ : ThreeAPFree ↑A
⊢ ¬ε * ↑n < ↑(#A)

Tactic:
exact fun hδn ↦ roth_3ap_theorem_nat ε hε hn _ hs₁ hδn.le hs₃

Result:
no goals

Proof state:
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∃ a, ∀ b ≥ a, ↑(rothNumberNat b) ≤ c * ↑b

Tactic:
refine fun ε hε ↦ ⟨cornersTheoremBound (ε / 3), fun n hn ↦ ?_⟩

Result:
ε : ℝ
hε : 0 < ε
n : ℕ
hn : n ≥ cornersTheoremBound (ε / 3)
⊢ ↑(rothNumberNat n) ≤ ε * ↑n

Proof state:
ε : ℝ
hε : 0 < ε
n : ℕ
hn : n ≥ cornersTheoremBound (ε / 3)
⊢ ↑(rothNumberNat n) ≤ ε * ↑n

Tactic:
obtain ⟨A, hs₁, hs₂, hs₃⟩ := rothNumberNat_spec n

Result:
case intro.intro.intro
ε : ℝ
hε : 0 < ε
n : ℕ
hn : n ≥ cornersTheoremBound (ε / 3)
A : Finset ℕ
hs₁ : A ⊆ range n
hs₂ : #A = rothNumberNat n
hs₃ : ThreeAPFree ↑A
⊢ ↑(rothNumberNat n) ≤ ε * ↑n

Proof state:
case intro.intro.intro
ε : ℝ
hε : 0 < ε
n : ℕ
hn : n ≥ cornersTheoremBound (ε / 3)
A : Finset ℕ
hs₁ : A ⊆ range n
hs₂ : #A = rothNumberNat n
hs₃ : ThreeAPFree ↑A
⊢ ↑(rothNumberNat n) ≤ ε * ↑n

Tactic:
rw [← hs₂, ← not_lt]

Result:
case intro.intro.intro
ε : ℝ
hε : 0 < ε
n : ℕ
hn : n ≥ cornersTheoremBound (ε / 3)
A : Finset ℕ
hs₁ : A ⊆ range n
hs₂ : #A = rothNumberNat n
hs₃ : ThreeAPFree ↑A
⊢ ¬ε * ↑n < ↑(#A)

Proof state:
⊢ (fun N => ↑(rothNumberNat N)) =o[atTop] fun N => ↑N

Tactic:
simp only [isLittleO_iff, eventually_atTop, RCLike.norm_natCast]

Result:
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∃ a, ∀ b ≥ a, ↑(rothNumberNat b) ≤ c * ↑b
-- Mathlib/Algebra/Ring/Divisibility/Lemmas.lean
lemma dvd_mul_sub_mul_mul_left_of_dvd {p a b c d x y : R}
    (h1 : p ∣ a * x + b * y) (h2 : p ∣ c * x + d * y) : p ∣ (a * d - b * c) * x

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
p a b c d x y : R
h2 : p ∣ c * x + d * y
k1 : R
hk1 : a * x + b * y = p * k1
⊢ p ∣ (a * d - b * c) * x

Tactic:
obtain ⟨k2, hk2⟩ := h2

Result:
case intro.intro
R : Type u_1
inst✝ : CommRing R
p a b c d x y k1 : R
hk1 : a * x + b * y = p * k1
k2 : R
hk2 : c * x + d * y = p * k2
⊢ p ∣ (a * d - b * c) * x

Proof state:
R : Type u_1
inst✝ : CommRing R
p a b c d x y : R
h1 : p ∣ a * x + b * y
h2 : p ∣ c * x + d * y
⊢ p ∣ (a * d - b * c) * x

Tactic:
obtain ⟨k1, hk1⟩ := h1

Result:
case intro
R : Type u_1
inst✝ : CommRing R
p a b c d x y : R
h2 : p ∣ c * x + d * y
k1 : R
hk1 : a * x + b * y = p * k1
⊢ p ∣ (a * d - b * c) * x

Proof state:
R : Type u_1
inst✝ : CommRing R
p a b c d x y k1 : R
hk1 : a * x + b * y = p * k1
k2 : R
hk2 : c * x + d * y = p * k2
⊢ (a * d - b * c) * x = a * x * d - c * x * b

Tactic:
ring

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
inst✝ : CommRing R
p a b c d x y k1 : R
hk1 : a * x + b * y = p * k1
k2 : R
hk2 : c * x + d * y = p * k2
⊢ p ∣ (a * d - b * c) * x

Tactic:
refine ⟨d * k1 - b * k2, ?_⟩

Result:
case intro.intro
R : Type u_1
inst✝ : CommRing R
p a b c d x y k1 : R
hk1 : a * x + b * y = p * k1
k2 : R
hk2 : c * x + d * y = p * k2
⊢ (a * d - b * c) * x = p * (d * k1 - b * k2)

Proof state:
case intro.intro
R : Type u_1
inst✝ : CommRing R
p a b c d x y k1 : R
hk1 : a * x + b * y = p * k1
k2 : R
hk2 : c * x + d * y = p * k2
⊢ (a * d - b * c) * x = p * (d * k1 - b * k2)

Tactic:
rw [show (a * d - b * c) * x = a * x * d - c * x * b by ring, eq_sub_of_add_eq hk1,
  eq_sub_of_add_eq hk2]

Result:
case intro.intro
R : Type u_1
inst✝ : CommRing R
p a b c d x y k1 : R
hk1 : a * x + b * y = p * k1
k2 : R
hk2 : c * x + d * y = p * k2
⊢ (p * k1 - b * y) * d - (p * k2 - d * y) * b = p * (d * k1 - b * k2)

Proof state:
case intro.intro
R : Type u_1
inst✝ : CommRing R
p a b c d x y k1 : R
hk1 : a * x + b * y = p * k1
k2 : R
hk2 : c * x + d * y = p * k2
⊢ (p * k1 - b * y) * d - (p * k2 - d * y) * b = p * (d * k1 - b * k2)

Tactic:
ring

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Preadditive.lean
theorem leftDistributor_inv_comp_biproduct_π {J : Type} [Fintype J] (X : C) (f : J → C) (j : J) :
    (leftDistributor X f).inv ≫ (X ◁ biproduct.π _ j) = biproduct.π _ j

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j : J
⊢ (leftDistributor X f).inv ≫ X ◁ biproduct.π f j = biproduct.π (fun j => X ⊗ f j) j

Tactic:
classical
simp [leftDistributor_inv, Preadditive.sum_comp, ← MonoidalCategory.whiskerLeft_comp,
  biproduct.ι_π, whiskerLeft_dite, comp_dite]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j : J
⊢ (leftDistributor X f).inv ≫ X ◁ biproduct.π f j = biproduct.π (fun j => X ⊗ f j) j

Tactic:
simp [leftDistributor_inv, Preadditive.sum_comp, ← MonoidalCategory.whiskerLeft_comp,
  biproduct.ι_π, whiskerLeft_dite, comp_dite]

Result:
no goals
-- Mathlib/Analysis/Convex/Deriv.lean
theorem concaveOn_of_deriv2_nonpos {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ} (hf : ContinuousOn f D)
    (hf' : DifferentiableOn ℝ f (interior D)) (hf'' : DifferentiableOn ℝ (deriv f) (interior D))
    (hf''_nonpos : ∀ x ∈ interior D, deriv^[2] f x ≤ 0) : ConcaveOn ℝ D f :=
  (antitoneOn_of_deriv_nonpos hD.interior hf''.continuousOn (by rwa [interior_interior]) <| by
        rwa [interior_interior]).concaveOn_of_deriv
    hD hf hf'

Proof state:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'' : DifferentiableOn ℝ (deriv f) (interior D)
hf''_nonpos : ∀ x ∈ interior D, deriv^[2] f x ≤ 0
⊢ ∀ x ∈ interior (interior D), deriv (deriv f) x ≤ 0

Tactic:
rwa [interior_interior]

Result:
no goals

Proof state:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'' : DifferentiableOn ℝ (deriv f) (interior D)
hf''_nonpos : ∀ x ∈ interior D, deriv^[2] f x ≤ 0
⊢ DifferentiableOn ℝ (deriv f) (interior (interior D))

Tactic:
rwa [interior_interior]

Result:
no goals
-- Mathlib/Probability/Process/Stopping.lean
theorem memLp_stoppedProcess_of_mem_finset (hτ : IsStoppingTime ℱ τ) (hu : ∀ n, MemLp (u n) p μ)
    (n : ι) {s : Finset ι} (hbdd : ∀ ω, τ ω < n → τ ω ∈ s) : MemLp (stoppedProcess u τ n) p μ

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s
⊢ MemLp (stoppedProcess u τ n) p μ

Tactic:
rw [stoppedProcess_eq_of_mem_finset n hbdd]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
μ : Measure Ω
τ : Ω → ι
E : Type u_4
p : ℝ≥0∞
u : ι → Ω → E
inst✝⁴ : LinearOrder ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
inst✝¹ : FirstCountableTopology ι
ℱ : Filtration ι m
inst✝ : NormedAddCommGroup E
hτ : IsStoppingTime ℱ τ
hu : ∀ (n : ι), MemLp (u n) p μ
n : ι
s : Finset ι
hbdd : ∀ (ω : Ω), τ ω < n → τ ω ∈ s
⊢ MemLp ({a | n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.filter (fun x => x < n) s, {ω | τ ω = i}.indicator (u i)) p μ
-- Mathlib/Data/DFinsupp/BigOperators.lean
theorem sum_single [∀ i, AddCommMonoid (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] {f : Π₀ i, β i} :
    f.sum single = f

Proof state:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
⊢ f.sum single = f

Tactic:
have := DFunLike.congr_fun (liftAddHom_singleAddHom (β := β)) f

Result:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
this : (liftAddHom (singleAddHom β)) f = (AddMonoidHom.id (Π₀ (i : ι), β i)) f
⊢ f.sum single = f

Proof state:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
this : (liftAddHom (singleAddHom β)) f = (AddMonoidHom.id (Π₀ (i : ι), β i)) f
⊢ f.sum single = f

Tactic:
rw [liftAddHom_apply, sumAddHom_apply] at this

Result:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
this : (f.sum fun x => ⇑(singleAddHom β x)) = (AddMonoidHom.id (Π₀ (i : ι), β i)) f
⊢ f.sum single = f

Proof state:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
this : (f.sum fun x => ⇑(singleAddHom β x)) = (AddMonoidHom.id (Π₀ (i : ι), β i)) f
⊢ f.sum single = f

Tactic:
exact this

Result:
no goals
-- Mathlib/Topology/MetricSpace/Bounded.lean
theorem _root_.CauchySeq.isBounded_range {f : ℕ → α} (hf : CauchySeq f) : IsBounded (range f) :=
  isBounded_range_of_cauchy_map_cofinite <| by rwa [Nat.cofinite_eq_atTop]

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
hf : CauchySeq f
⊢ Cauchy (map f Filter.cofinite)

Tactic:
rwa [Nat.cofinite_eq_atTop]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem Filter.EventuallyEq.mdifferentiableWithinAt_iff (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) :
    MDifferentiableWithinAt I I' f s x ↔ MDifferentiableWithinAt I I' f₁ s x

Proof state:
case mp
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f f₁ : M → M'
x : M
s : Set M
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ MDifferentiableWithinAt I I' f s x → MDifferentiableWithinAt I I' f₁ s x

Tactic:
intro h

Result:
case mp
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f f₁ : M → M'
x : M
s : Set M
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
h : MDifferentiableWithinAt I I' f s x
⊢ MDifferentiableWithinAt I I' f₁ s x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f f₁ : M → M'
x : M
s : Set M
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
h : MDifferentiableWithinAt I I' f₁ s x
⊢ ∀ (x : M), f₁ x = f x → f x = f₁ x

Tactic:
intro y

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f f₁ : M → M'
x : M
s : Set M
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
h : MDifferentiableWithinAt I I' f₁ s x
y : M
⊢ f₁ y = f y → f y = f₁ y
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
lemma bot_isUniform (hε : 0 < ε) : (⊥ : Finpartition A).IsUniform G ε

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
⊢ 0 ≤ ↑(#A * (#A - 1)) * ε

Tactic:
exact mul_nonneg (Nat.cast_nonneg _) hε.le

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
⊢ ⊥.IsUniform G ε

Tactic:
rw [Finpartition.IsUniform, Finpartition.card_bot, nonUniforms_bot _ hε, Finset.card_empty,
  Nat.cast_zero]

Result:
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
⊢ 0 ≤ ↑(#A * (#A - 1)) * ε
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem integral_piecewise [DecidablePred (· ∈ s)] (hs : MeasurableSet s) (hf : IntegrableOn f s μ)
    (hg : IntegrableOn g sᶜ μ) :
    ∫ x, s.piecewise f g x ∂μ = ∫ x in s, f x ∂μ + ∫ x in sᶜ, g x ∂μ

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f g : X → E
s : Set X
μ : Measure X
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : IntegrableOn f s μ
hg : IntegrableOn g sᶜ μ
⊢ ∫ (x : X), s.piecewise f g x ∂μ = ∫ (x : X) in s, f x ∂μ + ∫ (x : X) in sᶜ, g x ∂μ

Tactic:
rw [← Set.indicator_add_compl_eq_piecewise,
  integral_add' (hf.integrable_indicator hs) (hg.integrable_indicator hs.compl),
  integral_indicator hs, integral_indicator hs.compl]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
lemma decomp_to {i : ℤ} {A : C} (f : A ⟶ (mappingCone φ).X i) (j : ℤ) (hij : i + 1 = j) :
    ∃ (a : A ⟶ F.X j) (b : A ⟶ G.X i), f = a ≫ (inl φ).v j i (by omega) + b ≫ (inr φ).f i :=
  ⟨f ≫ (fst φ).1.v i j hij, f ≫ (snd φ).v i i (add_zero i),
    by apply ext_to φ i j hij <;> simp⟩

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.64339, u_1} C
inst✝³ : Category.{?u.64343, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i : ℤ
A : C
f : A ⟶ (mappingCone φ).X i
j : ℤ
hij : i + 1 = j
a : A ⟶ F.X j
b : A ⟶ G.X i
⊢ j + -1 = i

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i : ℤ
A : C
f : A ⟶ (mappingCone φ).X i
j : ℤ
hij : i + 1 = j
⊢ f = (f ≫ (↑(fst φ)).v i j hij) ≫ (inl φ).v j i ⋯ + (f ≫ (snd φ).v i i ⋯) ≫ (inr φ).f i

Tactic:
apply ext_to φ i j hij <;> simp

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Dickson.lean
theorem dickson_two_zero : ∀ n : ℕ, dickson 2 (0 : R) n = X ^ n
  | 0 => by
    simp only [dickson_zero, pow_zero]
    norm_num
  | 1 => by simp only [dickson_one, pow_one]
  | n + 2 => by
    simp only [dickson_add_two, C_0, zero_mul, sub_zero]
    rw [dickson_two_zero (n + 1), pow_add X (n + 1) 1, mul_comm, pow_one]

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ dickson 2 0 0 = X ^ 0

Tactic:
simp only [dickson_zero, pow_zero]

Result:
R : Type u_1
inst✝ : CommRing R
⊢ 3 - ↑2 = 1

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ dickson 2 0 (n + 2) = X ^ (n + 2)

Tactic:
simp only [dickson_add_two, C_0, zero_mul, sub_zero]

Result:
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ X * dickson 2 0 (n + 1) = X ^ (n + 2)

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ 3 - ↑2 = 1

Tactic:
norm_num

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ dickson 2 0 1 = X ^ 1

Tactic:
simp only [dickson_one, pow_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
⊢ X * dickson 2 0 (n + 1) = X ^ (n + 2)

Tactic:
rw [dickson_two_zero (n + 1), pow_add X (n + 1) 1, mul_comm, pow_one]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem rotate'_eq_drop_append_take :
    ∀ {l : List α} {n : ℕ}, n ≤ l.length → l.rotate' n = l.drop n ++ l.take n
  | [], n, h => by simp [drop_append_of_le_length h]
  | l, 0, h => by simp [take_append_of_le_length h]
  | a :: l, n + 1, h => by
    have hnl : n ≤ l.length := le_of_succ_le_succ h
    have hnl' : n ≤ (l ++ [a]).length

Proof state:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
⊢ n ≤ l.length + (0 + 1)

Tactic:
exact le_of_succ_le h

Result:
no goals

Proof state:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
⊢ n ≤ (l ++ [a]).length

Tactic:
rw [length_append, length_cons, List.length]

Result:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
⊢ n ≤ l.length + (0 + 1)

Proof state:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
hnl' : n ≤ (l ++ [a]).length
⊢ drop n l ++ [a] ++ take n l = drop n l ++ a :: take n l

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
⊢ (a :: l).rotate' (n + 1) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)

Tactic:
have hnl' : n ≤ (l ++ [a]).length := by
  rw [length_append, length_cons, List.length]; exact le_of_succ_le h

Result:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
hnl' : n ≤ (l ++ [a]).length
⊢ (a :: l).rotate' (n + 1) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)

Proof state:
α : Type u
l : List α
h : 0 ≤ l.length
⊢ l.rotate' 0 = drop 0 l ++ take 0 l

Tactic:
simp [take_append_of_le_length h]

Result:
no goals

Proof state:
α : Type u
n : ℕ
h : n ≤ [].length
⊢ [].rotate' n = drop n [] ++ take n []

Tactic:
simp [drop_append_of_le_length h]

Result:
no goals

Proof state:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
hnl' : n ≤ (l ++ [a]).length
⊢ (a :: l).rotate' (n + 1) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)

Tactic:
rw [rotate'_cons_succ, rotate'_eq_drop_append_take hnl', drop, take,
    drop_append_of_le_length hnl, take_append_of_le_length hnl]

Result:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
hnl' : n ≤ (l ++ [a]).length
⊢ drop n l ++ [a] ++ take n l = drop n l ++ a :: take n l

Proof state:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
⊢ (a :: l).rotate' (n + 1) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)

Tactic:
have hnl : n ≤ l.length := le_of_succ_le_succ h

Result:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
⊢ (a :: l).rotate' (n + 1) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)
-- Mathlib/Topology/EMetricSpace/Basic.lean
theorem cauchy_iff {f : Filter α} :
    Cauchy f ↔ f ≠ ⊥ ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x, x ∈ t → ∀ y, y ∈ t → edist x y < ε

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
f : Filter α
⊢ Cauchy f ↔ f ≠ ⊥ ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε

Tactic:
rw [← neBot_iff]

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
f : Filter α
⊢ Cauchy f ↔ f.NeBot ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
f : Filter α
⊢ Cauchy f ↔ f.NeBot ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε

Tactic:
exact uniformity_basis_edist.cauchy_iff

Result:
no goals
-- Mathlib/RingTheory/WittVector/Identities.lean
theorem verschiebung_frobenius_comm [CharP R p] :
    Function.Commute (verschiebung : 𝕎 R → 𝕎 R) frobenius := fun x => by
  rw [verschiebung_frobenius, frobenius_verschiebung]

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
⊢ verschiebung (frobenius x) = frobenius (verschiebung x)

Tactic:
rw [verschiebung_frobenius, frobenius_verschiebung]

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
theorem measure_le_le_exp_cgf [IsFiniteMeasure μ] (ε : ℝ) (ht : t ≤ 0)
    (h_int : Integrable (fun ω => exp (t * X ω)) μ) :
    (μ {ω | X ω ≤ ε}).toReal ≤ exp (-t * ε + cgf X μ t)

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω => rexp (t * X ω)) μ
⊢ rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε + cgf X μ t)

Tactic:
rw [exp_add]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω => rexp (t * X ω)) μ
⊢ rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε) * rexp (cgf X μ t)

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω => rexp (t * X ω)) μ
⊢ (μ {ω | X ω ≤ ε}).toReal ≤ rexp (-t * ε + cgf X μ t)

Tactic:
refine (measure_le_le_exp_mul_mgf ε ht h_int).trans ?_

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω => rexp (t * X ω)) μ
⊢ rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε + cgf X μ t)

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
ε : ℝ
ht : t ≤ 0
h_int : Integrable (fun ω => rexp (t * X ω)) μ
⊢ rexp (-t * ε) * mgf X μ t ≤ rexp (-t * ε) * rexp (cgf X μ t)

Tactic:
exact mul_le_mul le_rfl (le_exp_log _) mgf_nonneg (exp_pos _).le

Result:
no goals