harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem integrableOn_Icc_iff_integrableOn_Ico :
    IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ :=
  integrableOn_Icc_iff_integrableOn_Ico' (by rw [measure_singleton]; exact ENNReal.zero_ne_top)

Proof state:
α : Type u_1
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
inst✝ : NoAtoms μ
⊢ 0 ≠ ⊤

Tactic:
exact ENNReal.zero_ne_top

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
inst✝ : NoAtoms μ
⊢ μ {b} ≠ ⊤

Tactic:
rw [measure_singleton]

Result:
α : Type u_1
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
inst✝ : NoAtoms μ
⊢ 0 ≠ ⊤
-- Mathlib/Data/Fintype/Pigeonhole.lean
theorem Finite.exists_infinite_fiber [Infinite α] [Finite β] (f : α → β) :
    ∃ y : β, Infinite (f ⁻¹' {y})

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), ¬Infinite ↑(f ⁻¹' {y})
⊢ False

Tactic:
cases nonempty_fintype β

Result:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), ¬Infinite ↑(f ⁻¹' {y})
val✝ : Fintype β
⊢ False

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), ¬Infinite ↑(f ⁻¹' {y})
val✝ : Fintype β
this : (y : β) → Fintype ↑(f ⁻¹' {y})
key : Fintype α := { elems := univ.biUnion fun y => (f ⁻¹' {y}).toFinset, complete := ⋯ }
⊢ False

Tactic:
exact key.false

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
⊢ ∃ y, Infinite ↑(f ⁻¹' {y})

Tactic:
classical
  by_contra! hf
  cases nonempty_fintype β
  haveI := fun y => fintypeOfNotInfinite <| hf y
  let key : Fintype α :=
    { elems := univ.biUnion fun y : β => (f ⁻¹' {y}).toFinset
      complete := by simp }
  exact key.false

Result:
no goals

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), ¬Infinite ↑(f ⁻¹' {y})
val✝ : Fintype β
⊢ False

Tactic:
haveI := fun y => fintypeOfNotInfinite <| hf y

Result:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), ¬Infinite ↑(f ⁻¹' {y})
val✝ : Fintype β
this : (y : β) → Fintype ↑(f ⁻¹' {y})
⊢ False

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
⊢ ∃ y, Infinite ↑(f ⁻¹' {y})

Tactic:
by_contra! hf

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), ¬Infinite ↑(f ⁻¹' {y})
⊢ False

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), ¬Infinite ↑(f ⁻¹' {y})
val✝ : Fintype β
this : (y : β) → Fintype ↑(f ⁻¹' {y})
⊢ False

Tactic:
let key : Fintype α :=
  { elems := univ.biUnion fun y : β => (f ⁻¹' {y}).toFinset
    complete := by simp }

Result:
case intro
α : Type u_1
β : Type u_2
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), ¬Infinite ↑(f ⁻¹' {y})
val✝ : Fintype β
this : (y : β) → Fintype ↑(f ⁻¹' {y})
key : Fintype α := { elems := univ.biUnion fun y => (f ⁻¹' {y}).toFinset, complete := ⋯ }
⊢ False

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Infinite α
inst✝ : Finite β
f : α → β
hf : ∀ (y : β), ¬Infinite ↑(f ⁻¹' {y})
val✝ : Fintype β
this : (y : β) → Fintype ↑(f ⁻¹' {y})
⊢ ∀ (x : α), x ∈ univ.biUnion fun y => (f ⁻¹' {y}).toFinset

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/Basic.lean
@[simp] lemma GradedRing.projZeroRingHom'_apply_coe (a : 𝒜 0) :
    GradedRing.projZeroRingHom' 𝒜 a = a

Proof state:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a : ↥(𝒜 0)
⊢ (projZeroRingHom' 𝒜) ↑a = a

Tactic:
ext

Result:
case a
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a : ↥(𝒜 0)
⊢ ↑((projZeroRingHom' 𝒜) ↑a) = ↑a

Proof state:
case a
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid ι
inst✝⁴ : PartialOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a : ↥(𝒜 0)
⊢ ↑((projZeroRingHom' 𝒜) ↑a) = ↑a

Tactic:
simp only [coe_projZeroRingHom'_apply, projZeroRingHom_apply, decompose_coe, of_eq_same]

Result:
no goals
-- Mathlib/Computability/PartrecCode.lean
theorem const_prim : Primrec Code.const :=
  (_root_.Primrec.id.nat_iterate (_root_.Primrec.const zero)
    (comp_prim.comp (_root_.Primrec.const succ) Primrec.snd).to₂).of_eq
    fun n => by simp; induction n <;>
      simp [*, Code.const, Function.iterate_succ', -Function.iterate_succ]

Proof state:
n : ℕ
⊢ (fun b => succ.comp (n, b).2)^[id n] zero = Code.const n

Tactic:
simp

Result:
n : ℕ
⊢ (fun b => succ.comp b)^[n] zero = Code.const n

Proof state:
n : ℕ
⊢ (fun b => succ.comp b)^[n] zero = Code.const n

Tactic:
induction n <;>
simp [*, Code.const, Function.iterate_succ', -Function.iterate_succ]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Sort.lean
theorem antitone_pair_of_not_sorted' (h : f ∘ σ ≠ f ∘ sort f) :
    ∃ i j, i < j ∧ (f ∘ σ) j < (f ∘ σ) i

Proof state:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : f ∘ ⇑σ ≠ f ∘ ⇑(sort f)
⊢ ∃ i j, i < j ∧ (f ∘ ⇑σ) j < (f ∘ ⇑σ) i

Tactic:
contrapose! h

Result:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : ∀ (i j : Fin n), i < j → (f ∘ ⇑σ) i ≤ (f ∘ ⇑σ) j
⊢ f ∘ ⇑σ = f ∘ ⇑(sort f)

Proof state:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : ∀ (i j : Fin n), i < j → (f ∘ ⇑σ) i ≤ (f ∘ ⇑σ) j
⊢ f ∘ ⇑σ = f ∘ ⇑(sort f)

Tactic:
exact comp_sort_eq_comp_iff_monotone.mpr (monotone_iff_forall_lt.mpr h)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_pi_div_four : cos (π / 4) = √2 / 2

Proof state:
case e_x.e_a

⊢ 4 = 2 ^ 2

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ cos (π / 2 ^ 2) = √2 / 2

Tactic:
simp

Result:
no goals

Proof state:
⊢ cos (π / 4) = √2 / 2

Tactic:
trans cos (π / 2 ^ 2)

Result:
⊢ cos (π / 4) = cos (π / 2 ^ 2)


⊢ cos (π / 2 ^ 2) = √2 / 2

Proof state:
⊢ cos (π / 4) = cos (π / 2 ^ 2)

Tactic:
congr

Result:
case e_x.e_a

⊢ 4 = 2 ^ 2
-- Mathlib/CategoryTheory/Sites/Coherent/SequentialLimit.lean
private lemma exists_effectiveEpi (n : ℕ) (X : C) (y : (F.obj ⟨n⟩).val.obj ⟨X⟩) :
    ∃ (X' : C) (φ : X' ⟶ X) (_ : EffectiveEpi φ) (x : (F.obj ⟨n + 1⟩).val.obj ⟨X'⟩),
      ((F.map (homOfLE (n.le_add_right 1)).op).val.app ⟨X'⟩) x = ((F.obj ⟨n⟩).val.map φ.op) y

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preregular C
inst✝ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
n : ℕ
X : C
y : (F.obj (op n)).val.obj (op X)
⊢ ∃ X' φ, ∃ (_ : EffectiveEpi φ), ∃ x, (F.map (homOfLE ⋯).op).val.app (op X') x = (F.obj (op n)).val.map φ.op y

Tactic:
have := hF n

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preregular C
inst✝ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
n : ℕ
X : C
y : (F.obj (op n)).val.obj (op X)
this : Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
⊢ ∃ X' φ, ∃ (_ : EffectiveEpi φ), ∃ x, (F.map (homOfLE ⋯).op).val.app (op X') x = (F.obj (op n)).val.map φ.op y

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preregular C
inst✝ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
n : ℕ
X : C
y : (F.obj (op n)).val.obj (op X)
this : Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
⊢ ∃ X' φ, ∃ (_ : EffectiveEpi φ), ∃ x, (F.map (homOfLE ⋯).op).val.app (op X') x = (F.obj (op n)).val.map φ.op y

Tactic:
rw [coherentTopology.isLocallySurjective_iff, regularTopology.isLocallySurjective_iff] at this

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preregular C
inst✝ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
n : ℕ
X : C
y : (F.obj (op n)).val.obj (op X)
this :
  ∀ (X : C) (y : ToType ((F.obj (op n)).val.obj (op X))),
    ∃ X' φ,
      ∃ (_ : EffectiveEpi φ),
        ∃ x,
          (ConcreteCategory.hom ((F.map (homOfLE ⋯).op).val.app (op X'))) x =
            (ConcreteCategory.hom ((F.obj (op n)).val.map (op φ))) y
⊢ ∃ X' φ, ∃ (_ : EffectiveEpi φ), ∃ x, (F.map (homOfLE ⋯).op).val.app (op X') x = (F.obj (op n)).val.map φ.op y

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preregular C
inst✝ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
n : ℕ
X : C
y : (F.obj (op n)).val.obj (op X)
this :
  ∀ (X : C) (y : ToType ((F.obj (op n)).val.obj (op X))),
    ∃ X' φ,
      ∃ (_ : EffectiveEpi φ),
        ∃ x,
          (ConcreteCategory.hom ((F.map (homOfLE ⋯).op).val.app (op X'))) x =
            (ConcreteCategory.hom ((F.obj (op n)).val.map (op φ))) y
⊢ ∃ X' φ, ∃ (_ : EffectiveEpi φ), ∃ x, (F.map (homOfLE ⋯).op).val.app (op X') x = (F.obj (op n)).val.map φ.op y

Tactic:
exact this X y

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
theorem lt_inv_iff_mul_lt {r p : ℝ≥0} (h : p ≠ 0) : r < p⁻¹ ↔ r * p < 1

Proof state:
r p : ℝ≥0
h : p ≠ 0
⊢ r < p⁻¹ ↔ r * p < 1

Tactic:
rw [← mul_lt_mul_left (pos_iff_ne_zero.2 h), mul_inv_cancel₀ h, mul_comm]

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem int_add (h : Irrational x) (m : ℤ) : Irrational (m + x)

Proof state:
x : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (↑m + x)

Tactic:
rw [← cast_intCast]

Result:
x : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (↑↑m + x)

Proof state:
x : ℝ
h : Irrational x
m : ℤ
⊢ Irrational (↑↑m + x)

Tactic:
exact h.rat_add m

Result:
no goals
-- Mathlib/Computability/MyhillNerode.lean
theorem leftQuotient_accepts_apply (M : DFA α σ) (x : List α) :
    leftQuotient M.accepts x = M.acceptsFrom (M.eval x)

Proof state:
case h
α : Type u
σ : Type v
M : DFA α σ
x y : List α
⊢ y ∈ M.accepts.leftQuotient x ↔ y ∈ M.acceptsFrom (M.eval x)

Tactic:
simp [DFA.mem_accepts, DFA.mem_acceptsFrom, DFA.eval, DFA.evalFrom_of_append]

Result:
no goals

Proof state:
α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ M.accepts.leftQuotient x = M.acceptsFrom (M.eval x)

Tactic:
ext y

Result:
case h
α : Type u
σ : Type v
M : DFA α σ
x y : List α
⊢ y ∈ M.accepts.leftQuotient x ↔ y ∈ M.acceptsFrom (M.eval x)
-- Mathlib/CategoryTheory/FiberedCategory/HomLift.lean
lemma id_lift_eqToHom_codomain {p : 𝒳 ⥤ 𝒮} {R S : 𝒮} (hRS : R = S) {b : 𝒳} (hb : p.obj b = S) :
    p.IsHomLift (eqToHom hRS) (𝟙 b)

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
hRS : R = S
b : 𝒳
hb : p.obj b = S
⊢ p.IsHomLift (eqToHom hRS) (𝟙 b)

Tactic:
subst hRS hb

Result:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
b : 𝒳
⊢ p.IsHomLift (eqToHom ⋯) (𝟙 b)

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
b : 𝒳
⊢ p.IsHomLift (eqToHom ⋯) (𝟙 b)

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Perm/List.lean
theorem zipWith_swap_prod_support' (l l' : List α) :
    { x | (zipWith swap l l').prod x ≠ x } ≤ l.toFinset ⊔ l'.toFinset := fun _ h ↦ by
  simpa using mem_or_mem_of_zipWith_swap_prod_ne h

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
x✝ : α
h : x✝ ∈ {x | (zipWith swap l l').prod x ≠ x}
⊢ x✝ ∈ ↑(l.toFinset ⊔ l'.toFinset)

Tactic:
simpa using mem_or_mem_of_zipWith_swap_prod_ne h

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem cof_cof (a : Ordinal.{u}) : cof (cof a).ord = cof a

Proof state:
a : Ordinal.{u}
⊢ a.cof.ord.cof = a.cof

Tactic:
obtain ⟨f, hf⟩ := exists_fundamental_sequence a

Result:
case intro
a : Ordinal.{u}
f : (b : Ordinal.{u}) → b < a.cof.ord → Ordinal.{u}
hf : a.IsFundamentalSequence a.cof.ord f
⊢ a.cof.ord.cof = a.cof

Proof state:
case intro
a : Ordinal.{u}
f : (b : Ordinal.{u}) → b < a.cof.ord → Ordinal.{u}
hf : a.IsFundamentalSequence a.cof.ord f
⊢ a.cof.ord.cof = a.cof

Tactic:
obtain ⟨g, hg⟩ := exists_fundamental_sequence a.cof.ord

Result:
case intro.intro
a : Ordinal.{u}
f : (b : Ordinal.{u}) → b < a.cof.ord → Ordinal.{u}
hf : a.IsFundamentalSequence a.cof.ord f
g : (b : Ordinal.{u}) → b < a.cof.ord.cof.ord → Ordinal.{u}
hg : a.cof.ord.IsFundamentalSequence a.cof.ord.cof.ord g
⊢ a.cof.ord.cof = a.cof

Proof state:
case intro.intro
a : Ordinal.{u}
f : (b : Ordinal.{u}) → b < a.cof.ord → Ordinal.{u}
hf : a.IsFundamentalSequence a.cof.ord f
g : (b : Ordinal.{u}) → b < a.cof.ord.cof.ord → Ordinal.{u}
hg : a.cof.ord.IsFundamentalSequence a.cof.ord.cof.ord g
⊢ a.cof.ord.cof = a.cof

Tactic:
exact ord_injective (hf.trans hg).cof_eq.symm

Result:
no goals
-- Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
@[simp]
lemma finsuppRight_apply_tmul_apply (m : M) (p : ι →₀ N) (i : ι) :
    finsuppRight R M N ι (m ⊗ₜ[R] p) i = m ⊗ₜ[R] p i

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
m : M
p : ι →₀ N
i : ι
⊢ ((finsuppRight R M N ι) (m ⊗ₜ[R] p)) i = m ⊗ₜ[R] p i

Tactic:
rw [finsuppRight_apply_tmul, Finsupp.sum_apply,
  Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne) (by simp), Finsupp.single_eq_same]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
m : M
p : ι →₀ N
i : ι
⊢ p i = 0 → (Finsupp.single i (m ⊗ₜ[R] 0)) i = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem left_le_or : ∀ x y : Bool, x ≤ (x || y)

Proof state:
⊢ ∀ (x y : Bool), x ≤ (x || y)

Tactic:
decide

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
lemma isBigO_deriv_rpow_const_atTop (p : ℝ) :
    deriv (fun (x : ℝ) => x ^ p) =O[atTop] fun x => x ^ (p-1)

Proof state:
p : ℝ
⊢ (deriv fun x => x ^ p) =O[atTop] fun x => x ^ (p - 1)

Tactic:
rcases eq_or_ne p 0 with rfl | hp

Result:
case inl

⊢ (deriv fun x => x ^ 0) =O[atTop] fun x => x ^ (0 - 1)

case inr
p : ℝ
hp : p ≠ 0
⊢ (deriv fun x => x ^ p) =O[atTop] fun x => x ^ (p - 1)

Proof state:
p : ℝ
hp : p ≠ 0
⊢ (deriv fun x => x ^ p) =O[atTop] fun x => x ^ (p - 1)

Tactic:
exact (isTheta_deriv_rpow_const_atTop hp).1

Result:
no goals

Proof state:
case inr
p : ℝ
hp : p ≠ 0
⊢ (deriv fun x => x ^ p) =O[atTop] fun x => x ^ (p - 1)

Tactic:
case inr =>
  exact (isTheta_deriv_rpow_const_atTop hp).1

Result:
no goals

Proof state:
case inl

⊢ (deriv fun x => x ^ 0) =O[atTop] fun x => x ^ (0 - 1)

case inr
p : ℝ
hp : p ≠ 0
⊢ (deriv fun x => x ^ p) =O[atTop] fun x => x ^ (p - 1)

Tactic:
case inl =>
  simp [zero_sub, Real.rpow_neg_one, Real.rpow_zero, deriv_const', Asymptotics.isBigO_zero]

Result:
case inr
p : ℝ
hp : p ≠ 0
⊢ (deriv fun x => x ^ p) =O[atTop] fun x => x ^ (p - 1)

Proof state:
⊢ (deriv fun x => x ^ 0) =O[atTop] fun x => x ^ (0 - 1)

Tactic:
simp [zero_sub, Real.rpow_neg_one, Real.rpow_zero, deriv_const', Asymptotics.isBigO_zero]

Result:
no goals
-- Mathlib/Probability/Variance.lean
theorem evariance_eq_lintegral_ofReal :
    evariance X μ = ∫⁻ ω, ENNReal.ofReal ((X ω - μ[X]) ^ 2) ∂μ

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ eVar[X; μ] = ∫⁻ (ω : Ω), ENNReal.ofReal ((X ω - ∫ (x : Ω), X x ∂μ) ^ 2) ∂μ

Tactic:
simp [evariance, ← enorm_pow, Real.enorm_of_nonneg (sq_nonneg _)]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
lemma iSup_psigma {ι : Sort*} {κ : ι → Sort*} (f : (Σ' i, κ i) → α) :
    ⨆ ij, f ij = ⨆ i, ⨆ j, f ⟨i, j⟩ :=
  eq_of_forall_ge_iff fun c ↦ by simp only [iSup_le_iff, PSigma.forall]

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_8
κ : ι → Sort u_9
f : (i : ι) ×' κ i → α
c : α
⊢ ⨆ ij, f ij ≤ c ↔ ⨆ i, ⨆ j, f ⟨i, j⟩ ≤ c

Tactic:
simp only [iSup_le_iff, PSigma.forall]

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Finset.lean
/-- Given a nonempty Finset `s` and a function `f` from `s` to `ℕ`, if `d = s.gcd`,
then the `gcd` of `(f i) / d` is equal to `1`. -/
lemma gcd_div_eq_one (his : i ∈ s) (hfi : f i ≠ 0) : s.gcd (fun j ↦ f j / s.gcd f) = 1

Proof state:
case intro.intro.ha
ι : Type u_1
α : Type u_2
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizedGCDMonoid α
inst✝¹ : Div α
inst✝ : MulDivCancelClass α
f : ι → α
s : Finset ι
i : ι
his : i ∈ s
hfi : f i ≠ 0
g : ι → α
he : ∀ b ∈ s, f b = s.gcd f * g b
hg : s.gcd g = 1
a : ι
ha : a ∈ s
⊢ s.gcd f ≠ 0

Tactic:
exact mt Finset.gcd_eq_zero_iff.1 fun h ↦ hfi <| h i his

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizedGCDMonoid α
inst✝¹ : Div α
inst✝ : MulDivCancelClass α
f : ι → α
s : Finset ι
i : ι
his : i ∈ s
hfi : f i ≠ 0
⊢ (s.gcd fun j => f j / s.gcd f) = 1

Tactic:
obtain ⟨g, he, hg⟩ := Finset.extract_gcd f ⟨i, his⟩

Result:
case intro.intro
ι : Type u_1
α : Type u_2
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizedGCDMonoid α
inst✝¹ : Div α
inst✝ : MulDivCancelClass α
f : ι → α
s : Finset ι
i : ι
his : i ∈ s
hfi : f i ≠ 0
g : ι → α
he : ∀ b ∈ s, f b = s.gcd f * g b
hg : s.gcd g = 1
⊢ (s.gcd fun j => f j / s.gcd f) = 1

Proof state:
case intro.intro
ι : Type u_1
α : Type u_2
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizedGCDMonoid α
inst✝¹ : Div α
inst✝ : MulDivCancelClass α
f : ι → α
s : Finset ι
i : ι
his : i ∈ s
hfi : f i ≠ 0
g : ι → α
he : ∀ b ∈ s, f b = s.gcd f * g b
hg : s.gcd g = 1
⊢ (s.gcd fun j => f j / s.gcd f) = 1

Tactic:
refine (Finset.gcd_congr rfl fun a ha ↦ ?_).trans hg

Result:
case intro.intro
ι : Type u_1
α : Type u_2
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizedGCDMonoid α
inst✝¹ : Div α
inst✝ : MulDivCancelClass α
f : ι → α
s : Finset ι
i : ι
his : i ∈ s
hfi : f i ≠ 0
g : ι → α
he : ∀ b ∈ s, f b = s.gcd f * g b
hg : s.gcd g = 1
a : ι
ha : a ∈ s
⊢ f a / s.gcd f = g a

Proof state:
case intro.intro
ι : Type u_1
α : Type u_2
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizedGCDMonoid α
inst✝¹ : Div α
inst✝ : MulDivCancelClass α
f : ι → α
s : Finset ι
i : ι
his : i ∈ s
hfi : f i ≠ 0
g : ι → α
he : ∀ b ∈ s, f b = s.gcd f * g b
hg : s.gcd g = 1
a : ι
ha : a ∈ s
⊢ f a / s.gcd f = g a

Tactic:
rw [he a ha, mul_div_cancel_left₀]

Result:
case intro.intro.ha
ι : Type u_1
α : Type u_2
inst✝³ : CancelCommMonoidWithZero α
inst✝² : NormalizedGCDMonoid α
inst✝¹ : Div α
inst✝ : MulDivCancelClass α
f : ι → α
s : Finset ι
i : ι
his : i ∈ s
hfi : f i ≠ 0
g : ι → α
he : ∀ b ∈ s, f b = s.gcd f * g b
hg : s.gcd g = 1
a : ι
ha : a ∈ s
⊢ s.gcd f ≠ 0
-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace/ResidueField.lean
lemma residue_comp_residueFieldMap_eq_stalkMap_comp_residue (x : X) :
    CommRingCat.ofHom (IsLocalRing.residue (Y.presheaf.stalk (f.base x))) ≫
      residueFieldMap f x = f.stalkMap x ≫
      CommRingCat.ofHom (IsLocalRing.residue (X.presheaf.stalk x))

Proof state:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
⊢ CommRingCat.ofHom (IsLocalRing.residue ↑(Y.presheaf.stalk ((ConcreteCategory.hom f.base) x))) ≫ residueFieldMap f x =
    Hom.stalkMap f x ≫ CommRingCat.ofHom (IsLocalRing.residue ↑(X.presheaf.stalk x))

Tactic:
simp [residueFieldMap]

Result:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
⊢ CommRingCat.ofHom (IsLocalRing.residue ↑(Y.presheaf.stalk ((ConcreteCategory.hom f.base) x))) ≫
      CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f x))) =
    Hom.stalkMap f x ≫ CommRingCat.ofHom (IsLocalRing.residue ↑(X.presheaf.stalk x))

Proof state:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
⊢ CommRingCat.ofHom (IsLocalRing.residue ↑(Y.presheaf.stalk ((ConcreteCategory.hom f.base) x))) ≫
      CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f x))) =
    Hom.stalkMap f x ≫ CommRingCat.ofHom (IsLocalRing.residue ↑(X.presheaf.stalk x))

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem exists_erase_eq [LawfulBEq α] {a : α} {l : Array α} (h : a ∈ l) :
    ∃ l₁ l₂, a ∉ l₁ ∧ l = l₁.push a ++ l₂ ∧ l.erase a = l₁ ++ l₂

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
h : a ∈ l
w✝ : α
l₁ l₂ : Array α
h₁ : ∀ (b : α), b ∈ l₁ → ¬(a == b) = true
e : (a == w✝) = true
h₂ : l = l₁.push w✝ ++ l₂
h₃ : l.eraseP (BEq.beq a) = l₁ ++ l₂
⊢ ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁.push a ++ l₂ ∧ l.erase a = l₁ ++ l₂

Tactic:
rw [erase_eq_eraseP]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
h : a ∈ l
w✝ : α
l₁ l₂ : Array α
h₁ : ∀ (b : α), b ∈ l₁ → ¬(a == b) = true
e : (a == w✝) = true
h₂ : l = l₁.push w✝ ++ l₂
h₃ : l.eraseP (BEq.beq a) = l₁ ++ l₂
⊢ ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁.push a ++ l₂ ∧ (l.eraseP fun x => a == x) = l₁ ++ l₂

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
h : a ∈ l
⊢ ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁.push a ++ l₂ ∧ l.erase a = l₁ ++ l₂

Tactic:
let ⟨_, l₁, l₂, h₁, e, h₂, h₃⟩ := exists_of_eraseP h (beq_self_eq_true _)

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
h : a ∈ l
w✝ : α
l₁ l₂ : Array α
h₁ : ∀ (b : α), b ∈ l₁ → ¬(a == b) = true
e : (a == w✝) = true
h₂ : l = l₁.push w✝ ++ l₂
h₃ : l.eraseP (BEq.beq a) = l₁ ++ l₂
⊢ ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁.push a ++ l₂ ∧ l.erase a = l₁ ++ l₂

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
h : a ∈ l
w✝ : α
l₁ l₂ : Array α
h₁ : ∀ (b : α), b ∈ l₁ → ¬(a == b) = true
e : (a == w✝) = true
h₂ : l = l₁.push w✝ ++ l₂
h₃ : l.eraseP (BEq.beq a) = l₁ ++ l₂
⊢ ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁.push a ++ l₂ ∧ (l.eraseP fun x => a == x) = l₁ ++ l₂

Tactic:
exact ⟨l₁, l₂, fun h => h₁ _ h (beq_self_eq_true _), eq_of_beq e ▸ h₂, h₃⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filterMap_filter (p : α → Bool) (f : α → Option β) (l : List α) :
    filterMap f (filter p l) = filterMap (fun x => if p x then f x else none) l

Proof state:
α : Type u_1
β : Type u_2
p : α → Bool
f : α → Option β
l : List α
⊢ filterMap (fun x => (Option.guard (fun x => p x = true) x).bind f) l =
    filterMap (fun x => if p x = true then f x else none) l

Tactic:
congr

Result:
case e_f
α : Type u_1
β : Type u_2
p : α → Bool
f : α → Option β
l : List α
⊢ (fun x => (Option.guard (fun x => p x = true) x).bind f) = fun x => if p x = true then f x else none

Proof state:
α : Type u_1
β : Type u_2
p : α → Bool
f : α → Option β
l : List α
⊢ filterMap f (filter p l) = filterMap (fun x => if p x = true then f x else none) l

Tactic:
rw [← filterMap_eq_filter, filterMap_filterMap]

Result:
α : Type u_1
β : Type u_2
p : α → Bool
f : α → Option β
l : List α
⊢ filterMap (fun x => (Option.guard (fun x => p x = true) x).bind f) l =
    filterMap (fun x => if p x = true then f x else none) l

Proof state:
case e_f
α : Type u_1
β : Type u_2
p : α → Bool
f : α → Option β
l : List α
⊢ (fun x => (Option.guard (fun x => p x = true) x).bind f) = fun x => if p x = true then f x else none

Tactic:
funext x

Result:
case e_f.h
α : Type u_1
β : Type u_2
p : α → Bool
f : α → Option β
l : List α
x : α
⊢ (Option.guard (fun x => p x = true) x).bind f = if p x = true then f x else none

Proof state:
case e_f.h
α : Type u_1
β : Type u_2
p : α → Bool
f : α → Option β
l : List α
x : α
⊢ (Option.guard (fun x => p x = true) x).bind f = if p x = true then f x else none

Tactic:
by_cases h : p x <;> simp [Option.guard, h]

Result:
no goals