harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Bool/Basic.lean
theorem or_eq_false_eq_eq_false_and_eq_false (a b : Bool) :
    ((a || b) = false) = (a = false ∧ b = false)

Proof state:
a b : Bool
⊢ ((a || b) = false) = (a = false ∧ b = false)

Tactic:
cases a <;> cases b <;> simp

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_univ {f : β → α} : ⨆ x ∈ (univ : Set β), f x = ⨆ x, f x

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
⊢ ⨆ x ∈ univ, f x = ⨆ x, f x

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/WittVector/Frobenius.lean
theorem frobenius_eq_map_frobenius : @frobenius p R _ _ = map (_root_.frobenius R p)

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

Tactic:
ext (x n)

Result:
case a.h
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
⊢ (frobenius x).coeff n = ((map (_root_.frobenius R p)) x).coeff n

Proof state:
case a.h
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
⊢ (frobenius x).coeff n = ((map (_root_.frobenius R p)) x).coeff n

Tactic:
simp only [coeff_frobenius_charP, map_coeff, frobenius_def]

Result:
no goals
-- Mathlib/Topology/List.lean
theorem tendsto_cons_iff {β : Type*} {f : List α → β} {b : Filter β} {a : α} {l : List α} :
    Tendsto f (𝓝 (a::l)) b ↔ Tendsto (fun p : α × List α => f (p.1::p.2)) (𝓝 a ×ˢ 𝓝 l) b

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
β : Type u_3
f : List α → β
b : Filter β
a : α
l : List α
⊢ 𝓝 (a :: l) = Filter.map (fun p => p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l)

Tactic:
simp only [nhds_cons, Filter.prod_eq, (Filter.map_def _ _).symm,
  (Filter.seq_eq_filter_seq _ _).symm]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
β : Type u_3
f : List α → β
b : Filter β
a : α
l : List α
⊢ cons <$> 𝓝 a <*> 𝓝 l = (fun p => p.1 :: p.2) <$> (Prod.mk <$> 𝓝 a <*> 𝓝 l)

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
β : Type u_3
f : List α → β
b : Filter β
a : α
l : List α
this : 𝓝 (a :: l) = Filter.map (fun p => p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l)
⊢ Tendsto f (𝓝 (a :: l)) b ↔ Tendsto (fun p => f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) b

Tactic:
rw [this, Filter.tendsto_map'_iff]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
β : Type u_3
f : List α → β
b : Filter β
a : α
l : List α
this : 𝓝 (a :: l) = Filter.map (fun p => p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l)
⊢ Tendsto (f ∘ fun p => p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l) b ↔ Tendsto (fun p => f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) b

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
β : Type u_3
f : List α → β
b : Filter β
a : α
l : List α
⊢ cons <$> 𝓝 a <*> 𝓝 l = (fun p => p.1 :: p.2) <$> (Prod.mk <$> 𝓝 a <*> 𝓝 l)

Tactic:
simp [-Filter.map_def, Function.comp_def, functor_norm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
β : Type u_3
f : List α → β
b : Filter β
a : α
l : List α
this : 𝓝 (a :: l) = Filter.map (fun p => p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l)
⊢ Tendsto (f ∘ fun p => p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l) b ↔ Tendsto (fun p => f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) b

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
β : Type u_3
f : List α → β
b : Filter β
a : α
l : List α
⊢ Tendsto f (𝓝 (a :: l)) b ↔ Tendsto (fun p => f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) b

Tactic:
have : 𝓝 (a::l) = (𝓝 a ×ˢ 𝓝 l).map fun p : α × List α => p.1::p.2 := by
  simp only [nhds_cons, Filter.prod_eq, (Filter.map_def _ _).symm,
    (Filter.seq_eq_filter_seq _ _).symm]
  simp [-Filter.map_def, Function.comp_def, functor_norm]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
β : Type u_3
f : List α → β
b : Filter β
a : α
l : List α
this : 𝓝 (a :: l) = Filter.map (fun p => p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l)
⊢ Tendsto f (𝓝 (a :: l)) b ↔ Tendsto (fun p => f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) b
-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
theorem isHomogeneous_C (r : R) : IsHomogeneous (C r : MvPolynomial σ R) 0

Proof state:
case hn
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
r : R
⊢ degree 0 = 0

Tactic:
simp only [Finsupp.degree, Finsupp.zero_apply, Finset.sum_const_zero]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
r : R
⊢ (C r).IsHomogeneous 0

Tactic:
apply isHomogeneous_monomial

Result:
case hn
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
r : R
⊢ degree 0 = 0
-- Mathlib/Combinatorics/SimpleGraph/Circulant.lean
theorem cycleGraph_EulerianCircuit_cons_length (n : ℕ) : ∀ m : Fin (n + 3),
    (cycleGraph_EulerianCircuit_cons n m).length = m.val
  | ⟨0, h⟩ => by
    unfold cycleGraph_EulerianCircuit_cons
    rfl
  | ⟨m + 1, h⟩ => by
    unfold cycleGraph_EulerianCircuit_cons
    simp only [Walk.length_cons]
    rw [cycleGraph_EulerianCircuit_cons_length n]

Proof state:
n m : ℕ
h : m + 1 < n + 3
⊢ (SimpleGraph.cycleGraph_EulerianCircuit_cons n ⟨m, ⋯⟩).length + 1 = m + 1

Tactic:
rw [cycleGraph_EulerianCircuit_cons_length n]

Result:
no goals

Proof state:
n m : ℕ
h : m + 1 < n + 3
⊢ (let_fun hadj := ⋯;
      Walk.cons hadj (SimpleGraph.cycleGraph_EulerianCircuit_cons n ⟨m, ⋯⟩)).length =
    ↑⟨m + 1, h⟩

Tactic:
simp only [Walk.length_cons]

Result:
n m : ℕ
h : m + 1 < n + 3
⊢ (SimpleGraph.cycleGraph_EulerianCircuit_cons n ⟨m, ⋯⟩).length + 1 = m + 1

Proof state:
n : ℕ
h : 0 < n + 3
⊢ Walk.nil.length = ↑⟨0, h⟩

Tactic:
rfl

Result:
no goals

Proof state:
n m : ℕ
h : m + 1 < n + 3
⊢ (SimpleGraph.cycleGraph_EulerianCircuit_cons n ⟨m + 1, h⟩).length = ↑⟨m + 1, h⟩

Tactic:
unfold cycleGraph_EulerianCircuit_cons

Result:
n m : ℕ
h : m + 1 < n + 3
⊢ (let_fun hadj := ⋯;
      Walk.cons hadj (SimpleGraph.cycleGraph_EulerianCircuit_cons n ⟨m, ⋯⟩)).length =
    ↑⟨m + 1, h⟩

Proof state:
n : ℕ
h : 0 < n + 3
⊢ (SimpleGraph.cycleGraph_EulerianCircuit_cons n ⟨0, h⟩).length = ↑⟨0, h⟩

Tactic:
unfold cycleGraph_EulerianCircuit_cons

Result:
n : ℕ
h : 0 < n + 3
⊢ Walk.nil.length = ↑⟨0, h⟩
-- Mathlib/Data/Nat/Choose/Multinomial.lean
theorem multinomial_filter_ne [DecidableEq α] (a : α) (m : Multiset α) :
    m.multinomial = m.card.choose (m.count a) * (m.filter (a ≠ ·)).multinomial

Proof state:
case h.e'_3.h.e'_6.h.e'_2.h
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
⊢ (if a✝ ≠ a then count a m else 0) = Function.update (⇑(toFinsupp m)) a✝ 0 a

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
h : a✝ ≠ a
⊢ count a m = Function.update (⇑(toFinsupp m)) a✝ 0 a

case neg
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
h : ¬a✝ ≠ a
⊢ 0 = Function.update (⇑(toFinsupp m)) a✝ 0 a

Proof state:
case h.e'_3.h.e'_6.h.e'_2
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ toFinsupp (filter (fun x => a ≠ x) m) = (toFinsupp m).update a 0

Tactic:
ext1 a

Result:
case h.e'_3.h.e'_6.h.e'_2.h
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
⊢ (toFinsupp (filter (fun x => a✝ ≠ x) m)) a = ((toFinsupp m).update a✝ 0) a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ m.multinomial = m.card.choose (count a m) * (filter (fun x => a ≠ x) m).multinomial

Tactic:
dsimp only [multinomial]

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ (toFinsupp m).multinomial = m.card.choose (count a m) * (toFinsupp (filter (fun x => a ≠ x) m)).multinomial

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
h : a✝ ≠ a
⊢ count a m = Function.update (⇑(toFinsupp m)) a✝ 0 a

Tactic:
rw [Function.update_of_ne h.symm, toFinsupp_apply]

Result:
no goals

Proof state:
case h.e'_3.h.e'_6.h.e'_2.h
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
⊢ (toFinsupp (filter (fun x => a✝ ≠ x) m)) a = ((toFinsupp m).update a✝ 0) a

Tactic:
rw [toFinsupp_apply, count_filter, Finsupp.coe_update]

Result:
case h.e'_3.h.e'_6.h.e'_2.h
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
⊢ (if a✝ ≠ a then count a m else 0) = Function.update (⇑(toFinsupp m)) a✝ 0 a

Proof state:
case h.e'_3.h.e'_5.h.e'_1
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ m.card = (toFinsupp m).sum fun x => id

Tactic:
rw [← Finsupp.card_toMultiset, m.toFinsupp_toMultiset]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ (toFinsupp m).multinomial = m.card.choose (count a m) * (toFinsupp (filter (fun x => a ≠ x) m)).multinomial

Tactic:
convert Finsupp.multinomial_update a _

Result:
case h.e'_3.h.e'_5.h.e'_1
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ m.card = (toFinsupp m).sum fun x => id

case h.e'_3.h.e'_6.h.e'_2
α : Type u_1
inst✝ : DecidableEq α
a : α
m : Multiset α
⊢ toFinsupp (filter (fun x => a ≠ x) m) = (toFinsupp m).update a 0

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
h : ¬a✝ ≠ a
⊢ 0 = Function.update (⇑(toFinsupp m)) a✝ 0 a

Tactic:
rw [not_ne_iff.1 h, Function.update_self]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem Matrix.toLin_mul_apply [Finite l] [DecidableEq m] (A : Matrix l m R) (B : Matrix m n R)
    (x) : Matrix.toLin v₁ v₃ (A * B) x = (Matrix.toLin v₂ v₃ A) (Matrix.toLin v₁ v₂ B x)

Proof state:
R : Type u_1
inst✝¹¹ : CommSemiring R
l : Type u_2
m : Type u_3
n : Type u_4
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype m
inst✝⁸ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type u_7
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₃
v₃ : Basis l R M₃
inst✝¹ : Finite l
inst✝ : DecidableEq m
A : Matrix l m R
B : Matrix m n R
x : M₁
⊢ ((toLin v₁ v₃) (A * B)) x = ((toLin v₂ v₃) A) (((toLin v₁ v₂) B) x)

Tactic:
rw [Matrix.toLin_mul v₁ v₂, LinearMap.comp_apply]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem norm_I_of_ne_zero (hI : (I : K) ≠ 0) : ‖(I : K)‖ = 1

Proof state:
K : Type u_1
inst✝ : RCLike K
hI : I ≠ 0
⊢ ‖I‖ = 1

Tactic:
rw [← mul_self_inj_of_nonneg (norm_nonneg I) zero_le_one, one_mul, ← norm_mul,
  I_mul_I_of_nonzero hI, norm_neg, norm_one]

Result:
no goals
-- Mathlib/Analysis/MeanInequalitiesPow.lean
theorem add_rpow_le_one_of_add_le_one {p : ℝ} (a b : ℝ≥0) (hab : a + b ≤ 1) (hp1 : 1 ≤ p) :
    a ^ p + b ^ p ≤ 1

Proof state:
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
h_le_one : ∀ x ≤ 1, x ^ p ≤ x
ha : a ≤ 1
⊢ a ^ p + b ^ p ≤ 1

Tactic:
have hb : b ≤ 1 := (self_le_add_left b a).trans hab

Result:
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
h_le_one : ∀ x ≤ 1, x ^ p ≤ x
ha : a ≤ 1
hb : b ≤ 1
⊢ a ^ p + b ^ p ≤ 1

Proof state:
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
h_le_one : ∀ x ≤ 1, x ^ p ≤ x
ha : a ≤ 1
hb : b ≤ 1
⊢ a ^ p + b ^ p ≤ 1

Tactic:
exact (add_le_add (h_le_one a ha) (h_le_one b hb)).trans hab

Result:
no goals

Proof state:
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ 1

Tactic:
have h_le_one : ∀ x : ℝ≥0, x ≤ 1 → x ^ p ≤ x := fun x hx => rpow_le_self_of_le_one hx hp1

Result:
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
h_le_one : ∀ x ≤ 1, x ^ p ≤ x
⊢ a ^ p + b ^ p ≤ 1

Proof state:
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
h_le_one : ∀ x ≤ 1, x ^ p ≤ x
⊢ a ^ p + b ^ p ≤ 1

Tactic:
have ha : a ≤ 1 := (self_le_add_right a b).trans hab

Result:
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
h_le_one : ∀ x ≤ 1, x ^ p ≤ x
ha : a ≤ 1
⊢ a ^ p + b ^ p ≤ 1
-- Mathlib/Data/Finsupp/Order.lean
lemma sum_le_sum_index [DecidableEq ι] {f₁ f₂ : ι →₀ α} {h : ι → α → β} (hf : f₁ ≤ f₂)
    (hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i))
    (hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0) : f₁.sum h ≤ f₂.sum h

Proof state:
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : Zero α
inst✝² : Preorder α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : DecidableEq ι
f₁ f₂ : ι →₀ α
h : ι → α → β
hf : f₁ ≤ f₂
hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)
hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0
⊢ f₁.sum h ≤ f₂.sum h

Tactic:
classical
rw [sum_of_support_subset _ Finset.subset_union_left _ hh₀,
  sum_of_support_subset _ Finset.subset_union_right _ hh₀]
exact Finset.sum_le_sum fun i hi ↦ hh _ hi <| hf _

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : Zero α
inst✝² : Preorder α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : DecidableEq ι
f₁ f₂ : ι →₀ α
h : ι → α → β
hf : f₁ ≤ f₂
hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)
hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0
⊢ f₁.sum h ≤ f₂.sum h

Tactic:
rw [sum_of_support_subset _ Finset.subset_union_left _ hh₀,
  sum_of_support_subset _ Finset.subset_union_right _ hh₀]

Result:
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : Zero α
inst✝² : Preorder α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : DecidableEq ι
f₁ f₂ : ι →₀ α
h : ι → α → β
hf : f₁ ≤ f₂
hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)
hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0
⊢ ∑ x ∈ f₁.support ∪ f₂.support, h x (f₁ x) ≤ ∑ x ∈ f₁.support ∪ f₂.support, h x (f₂ x)

Proof state:
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : Zero α
inst✝² : Preorder α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : DecidableEq ι
f₁ f₂ : ι →₀ α
h : ι → α → β
hf : f₁ ≤ f₂
hh : ∀ i ∈ f₁.support ∪ f₂.support, Monotone (h i)
hh₀ : ∀ i ∈ f₁.support ∪ f₂.support, h i 0 = 0
⊢ ∑ x ∈ f₁.support ∪ f₂.support, h x (f₁ x) ≤ ∑ x ∈ f₁.support ∪ f₂.support, h x (f₂ x)

Tactic:
exact Finset.sum_le_sum fun i hi ↦ hh _ hi <| hf _

Result:
no goals
-- Mathlib/Analysis/Fourier/PoissonSummation.lean
theorem isBigO_norm_Icc_restrict_atBot {f : C(ℝ, E)} {b : ℝ} (hb : 0 < b)
    (hf : f =O[atBot] fun x : ℝ => |x| ^ (-b)) (R S : ℝ) :
    (fun x : ℝ => ‖f.restrict (Icc (x + R) (x + S))‖) =O[atBot] fun x : ℝ => |x| ^ (-b)

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ⇑(f.comp { toFun := fun a => -a, continuous_toFun := ⋯ }) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x =>
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (f.comp { toFun := fun a => -a, continuous_toFun := ⋯ })‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x : ℝ
⊢ ‖‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖‖ ≤
    ‖((fun x =>
            ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (f.comp { toFun := fun a => -a, continuous_toFun := ⋯ })‖) ∘
          Neg.neg)
        x‖

Tactic:
rw [norm_norm, Function.comp_apply, norm_norm, ContinuousMap.norm_le _ (norm_nonneg _)]

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ⇑(f.comp { toFun := fun a => -a, continuous_toFun := ⋯ }) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x =>
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (f.comp { toFun := fun a => -a, continuous_toFun := ⋯ })‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x : ℝ
⊢ ∀ (x_1 : ↑(Icc (x + R) (x + S))),
    ‖(ContinuousMap.restrict (Icc (x + R) (x + S)) f) x_1‖ ≤
      ‖ContinuousMap.restrict (Icc (-x + -S) (-x + -R)) (f.comp { toFun := fun a => -a, continuous_toFun := ⋯ })‖

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ⇑(f.comp { toFun := fun a => -a, continuous_toFun := ⋯ }) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x =>
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (f.comp { toFun := fun a => -a, continuous_toFun := ⋯ })‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ -x✝ + -S ≤ -x

Tactic:
linarith [hx.2]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/RationalRoot.lean
theorem num_dvd_of_is_root {p : A[X]} {r : K} (hr : aeval r p = 0) : num A r ∣ p.coeff 0

Proof state:
case convert_2
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
⊢ ∀ (j : ℕ), j ≠ 0 → num A r ∣ (p.scaleRoots ↑(den A r)).coeff j * num A r ^ j

Tactic:
intro j hj

Result:
case convert_2
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
j : ℕ
hj : j ≠ 0
⊢ num A r ∣ (p.scaleRoots ↑(den A r)).coeff j * num A r ^ j

Proof state:
case neg
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr✝ : (aeval r) p = 0
this : num A r ∣ p.coeff 0 * ↑(den A r) ^ p.natDegree
inst : (a : Prop) → Decidable a
hr : ¬num A r = 0
q : A
dvd_num : q ∣ num A r
dvd_denom_pow : q ∣ ↑(den A r) ^ p.natDegree
hq : Prime q
⊢ IsUnit q

Tactic:
exact num_den_reduced A r dvd_num (hq.dvd_of_dvd_pow dvd_denom_pow)

Result:
no goals

Proof state:
case h.e'_4
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
⊢ (p.scaleRoots ↑(den A r)).coeff 0 = (p.scaleRoots ↑(den A r)).coeff 0 * num A r ^ 0

Tactic:
rw [pow_zero, mul_one]

Result:
no goals

Proof state:
case h.e'_3
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
p : A[X]
r : K
hr : (aeval r) p = 0
j : ℕ
hj : j ≠ 0
⊢ num A r = num A r ^ ⊥.succ

Tactic:
exact (pow_one _).symm

Result:
no goals
-- Mathlib/Data/List/Infix.lean
@[gcongr] lemma IsPrefix.take (h : l₁ <+: l₂) (n : ℕ) : l₁.take n <+: l₂.take n

Proof state:
α : Type u_1
l₁ l₂ : List α
h : l₁ <+: l₂
n : ℕ
⊢ List.take n l₁ <+: List.take n l₂

Tactic:
simpa [prefix_take_iff, Nat.min_le_left] using (take_prefix n l₁).trans h

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
lemma one_succAbove_zero {n : ℕ} : (1 : Fin (n + 2)).succAbove 0 = 0

Proof state:
n : ℕ
⊢ succAbove 1 0 = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[reassoc (attr := simp)]
lemma d_fst_v' (i j : ℤ) (hij : i + 1 = j) :
    (mappingCone φ).d (i - 1) i ≫ (fst φ).1.v i j hij =
      -(fst φ).1.v (i - 1) i (by omega) ≫ F.d i j :=
  d_fst_v φ (i - 1) i j (by omega) hij

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.99175, u_1} C
inst✝³ : Category.{?u.99179, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
⊢ i - 1 + 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 j : ℤ
hij : i + 1 = j
⊢ i - 1 + 1 = i

Tactic:
omega

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CondCDF.lean
lemma isRatCondKernelCDFAux_preCDF (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] :
    IsRatCondKernelCDFAux (fun p r ↦ (preCDF ρ r p.2).toReal)
      (Kernel.const Unit ρ) (Kernel.const Unit ρ.fst) where
  measurable := measurable_preCDF'.comp measurable_snd
  mono' a r r' hrr'

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
x✝ : Antitone s
hs_tendsto : Tendsto s atTop atBot
h : Tendsto (fun r => (ρ.IicSnd ↑r) univ) atBot (𝓝 0)
h0 : Tendsto ENNReal.toReal (𝓝 0) (𝓝 0)
⊢ Tendsto (fun m => ((ρ.IicSnd ↑(s m)) univ).toReal) atTop (𝓝 (ENNReal.toReal 0))

Tactic:
exact h0.comp (h.comp hs_tendsto)

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
q : ℚ
⊢ ∀ᵐ (c : α) ∂(Kernel.const Unit ρ.fst) a, (preCDF ρ q (a, c).2).toReal ≤ 1

Tactic:
simp only [Kernel.const_apply, forall_const]

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
q : ℚ
⊢ ∀ᵐ (c : α) ∂ρ.fst, (preCDF ρ q c).toReal ≤ 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/GetLit.lean
theorem toArrayLit_eq (as : Array α) (n : Nat) (hsz : as.size = n) : as = toArrayLit as n hsz

Proof state:
α : Type u_1
as : Array α
n : Nat
hsz : as.size = n
i : Nat
hi : i ≤ as.size
⊢ as.toListLitAux n hsz i hi (List.drop i as.toList) = as.toList

Tactic:
induction i <;> simp only [List.drop, toListLitAux, getLit_eq, List.getElem_cons_drop_succ_eq_drop, *]

Result:
no goals

Proof state:
case h
α : Type u_1
as : Array α
n : Nat
hsz : as.size = n
hle : n ≤ as.size
hge : as.size ≤ n
this : as.toListLitAux n hsz n hle (List.drop n as.toList) = as.toList
⊢ as.toList = as.toListLitAux n hsz n ⋯ List.nil

Tactic:
rw [List.drop_eq_nil_of_le hge] at this

Result:
case h
α : Type u_1
as : Array α
n : Nat
hsz : as.size = n
hle : n ≤ as.size
hge : as.size ≤ n
this : as.toListLitAux n hsz n hle List.nil = as.toList
⊢ as.toList = as.toListLitAux n hsz n ⋯ List.nil

Proof state:
α : Type u_1
as : Array α
n : Nat
hsz : as.size = n
⊢ as = as.toArrayLit n hsz

Tactic:
apply ext'

Result:
case h
α : Type u_1
as : Array α
n : Nat
hsz : as.size = n
⊢ as.toList = (as.toArrayLit n hsz).toList

Proof state:
case h
α : Type u_1
as : Array α
n : Nat
hsz : as.size = n
hle : n ≤ as.size
hge : as.size ≤ n
⊢ as.toList = as.toListLitAux n hsz n ⋯ List.nil

Tactic:
have := go n hle

Result:
case h
α : Type u_1
as : Array α
n : Nat
hsz : as.size = n
hle : n ≤ as.size
hge : as.size ≤ n
this : as.toListLitAux n hsz n hle (List.drop n as.toList) = as.toList
⊢ as.toList = as.toListLitAux n hsz n ⋯ List.nil

Proof state:
case h
α : Type u_1
as : Array α
n : Nat
hsz : as.size = n
hle : n ≤ as.size
⊢ as.toList = as.toListLitAux n hsz n ⋯ List.nil

Tactic:
have hge : as.size ≤ n := hsz ▸ Nat.le_refl _

Result:
case h
α : Type u_1
as : Array α
n : Nat
hsz : as.size = n
hle : n ≤ as.size
hge : as.size ≤ n
⊢ as.toList = as.toListLitAux n hsz n ⋯ List.nil

Proof state:
case h
α : Type u_1
as : Array α
n : Nat
hsz : as.size = n
hle : n ≤ as.size
hge : as.size ≤ n
this : as.toListLitAux n hsz n hle List.nil = as.toList
⊢ as.toList = as.toListLitAux n hsz n ⋯ List.nil

Tactic:
rw [this]

Result:
no goals

Proof state:
case h
α : Type u_1
as : Array α
n : Nat
hsz : as.size = n
⊢ as.toList = as.toListLitAux n hsz n ⋯ List.nil

Tactic:
have hle : n ≤ as.size := hsz ▸ Nat.le_refl _

Result:
case h
α : Type u_1
as : Array α
n : Nat
hsz : as.size = n
hle : n ≤ as.size
⊢ as.toList = as.toListLitAux n hsz n ⋯ List.nil

Proof state:
case h
α : Type u_1
as : Array α
n : Nat
hsz : as.size = n
⊢ as.toList = (as.toArrayLit n hsz).toList

Tactic:
simp [toArrayLit, toList_toArray]

Result:
case h
α : Type u_1
as : Array α
n : Nat
hsz : as.size = n
⊢ as.toList = as.toListLitAux n hsz n ⋯ List.nil
-- Mathlib/Order/Interval/Set/OrdConnected.lean
lemma ordConnected_inter_Icc_iff (hx : x ∈ s) (hy : y ∈ s) :
    OrdConnected (s ∩ Icc x y) ↔ Ioo x y ⊆ s

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ (s ∩ Icc x y).OrdConnected ↔ Ioo x y ⊆ s

Tactic:
refine ⟨fun h ↦ Ioo_subset_Icc_self.trans fun z hz ↦ ?_, ordConnected_inter_Icc_of_subset⟩

Result:
α : Type u_1
inst✝ : PartialOrder α
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
h : (s ∩ Icc x y).OrdConnected
z : α
hz : z ∈ Icc x y
⊢ z ∈ s

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
h : (s ∩ Icc x y).OrdConnected
z : α
hz : z ∈ Icc x y
hxy : x ≤ y
⊢ z ∈ s

Tactic:
exact h.out ⟨hx, left_mem_Icc.2 hxy⟩ ⟨hy, right_mem_Icc.2 hxy⟩ hz |>.1

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
h : (s ∩ Icc x y).OrdConnected
z : α
hz : z ∈ Icc x y
⊢ z ∈ s

Tactic:
have hxy : x ≤ y := hz.1.trans hz.2

Result:
α : Type u_1
inst✝ : PartialOrder α
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
h : (s ∩ Icc x y).OrdConnected
z : α
hz : z ∈ Icc x y
hxy : x ≤ y
⊢ z ∈ s
-- Mathlib/Data/Seq/WSeq.lean
theorem productive_congr {s t : WSeq α} (h : s ~ʷ t) : Productive s ↔ Productive t

Proof state:
α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ s.Productive ↔ t.Productive

Tactic:
simp only [productive_iff]

Result:
α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ (∀ (n : ℕ), (s.get? n).Terminates) ↔ ∀ (n : ℕ), (t.get? n).Terminates

Proof state:
α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ (∀ (n : ℕ), (s.get? n).Terminates) ↔ ∀ (n : ℕ), (t.get? n).Terminates

Tactic:
exact forall_congr' fun n => terminates_congr <| get?_congr h _

Result:
no goals