harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Lie/Weights/RootSystem.lean
lemma chainBotCoeff_of_eq_zsmul_add
    (hα : α.IsNonZero) (β' : Weight K H L) (n : ℤ) (hβ' : (β' : H → K) = n • α + β) :
    chainBotCoeff α β' = chainBotCoeff α β + n

Proof state:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
β' : Weight K (↥H) L
n : ℤ
hβ' : ⇑β' = n • ⇑α + ⇑β
this : ⇑β' = -n • -⇑α + ⇑β
⊢ ↑(chainBotCoeff (⇑α) β') = ↑(chainBotCoeff (⇑α) β) + n

Tactic:
rw [chainBotCoeff, chainBotCoeff, ← Weight.coe_neg,
  chainTopCoeff_of_eq_zsmul_add (-α) β hα.neg β' (-n) this, sub_neg_eq_add]

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
β' : Weight K (↥H) L
n : ℤ
hβ' : ⇑β' = n • ⇑α + ⇑β
⊢ ⇑β' = -n • -⇑α + ⇑β

Tactic:
rwa [neg_smul, smul_neg, neg_neg]

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
β' : Weight K (↥H) L
n : ℤ
hβ' : ⇑β' = n • ⇑α + ⇑β
⊢ ↑(chainBotCoeff (⇑α) β') = ↑(chainBotCoeff (⇑α) β) + n

Tactic:
have : (β' : H → K) = -n • (-α) + β := by rwa [neg_smul, smul_neg, neg_neg]

Result:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
β' : Weight K (↥H) L
n : ℤ
hβ' : ⇑β' = n • ⇑α + ⇑β
this : ⇑β' = -n • -⇑α + ⇑β
⊢ ↑(chainBotCoeff (⇑α) β') = ↑(chainBotCoeff (⇑α) β) + n
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem ofList_cons [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} {tl : List ((a : α) × (β a))} :
    ofList (⟨k, v⟩ :: tl) = ((∅ : Raw α β).insert k v).insertMany tl

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
v : β k
tl : List ((a : α) × β a)
⊢ ofList (⟨k, v⟩ :: tl) = (∅.insert k v).insertMany tl

Tactic:
simp_to_raw

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
v : β k
tl : List ((a : α) × β a)
⊢ (Raw₀.empty.insertMany (⟨k, v⟩ :: tl)).val.val = ((Raw₀.insert ⟨Raw₀.empty.val, ⋯⟩ k v).insertMany tl).val.val

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
v : β k
tl : List ((a : α) × β a)
⊢ (Raw₀.empty.insertMany (⟨k, v⟩ :: tl)).val.val = ((Raw₀.insert ⟨Raw₀.empty.val, ⋯⟩ k v).insertMany tl).val.val

Tactic:
rw [Raw₀.insertMany_empty_list_cons]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_extract (as : Array α) (start stop : Nat) :
    (as.extract start stop).toList = as.toList.extract start stop

Proof state:
case h
α : Type u_1
as : Array α
start stop n : Nat
h₁ : n < (as.extract start stop).toList.length
h₂ : n < (as.toList.extract start stop).length
⊢ (as.extract start stop).toList[n] = (as.toList.extract start stop)[n]

Tactic:
simp

Result:
no goals

Proof state:
case h
α : Type u_1
as : Array α
start stop : Nat
⊢ ∀ (i : Nat) (h₁ : i < (as.extract start stop).toList.length) (h₂ : i < (as.toList.extract start stop).length),
    (as.extract start stop).toList[i] = (as.toList.extract start stop)[i]

Tactic:
intros n h₁ h₂

Result:
case h
α : Type u_1
as : Array α
start stop n : Nat
h₁ : n < (as.extract start stop).toList.length
h₂ : n < (as.toList.extract start stop).length
⊢ (as.extract start stop).toList[n] = (as.toList.extract start stop)[n]

Proof state:
case hl
α : Type u_1
as : Array α
start stop : Nat
⊢ min stop as.size - start = min (stop - start) (as.size - start)

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
as : Array α
start stop : Nat
⊢ (as.extract start stop).toList = as.toList.extract start stop

Tactic:
apply List.ext_getElem

Result:
case hl
α : Type u_1
as : Array α
start stop : Nat
⊢ (as.extract start stop).toList.length = (as.toList.extract start stop).length

case h
α : Type u_1
as : Array α
start stop : Nat
⊢ ∀ (i : Nat) (h₁ : i < (as.extract start stop).toList.length) (h₂ : i < (as.toList.extract start stop).length),
    (as.extract start stop).toList[i] = (as.toList.extract start stop)[i]

Proof state:
case hl
α : Type u_1
as : Array α
start stop : Nat
⊢ (as.extract start stop).toList.length = (as.toList.extract start stop).length

Tactic:
simp only [length_toList, size_extract, List.length_take, List.length_drop]

Result:
case hl
α : Type u_1
as : Array α
start stop : Nat
⊢ min stop as.size - start = min (stop - start) (as.size - start)
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem eval_whiskerLeft {f g h : C}
    {η η' : g ⟶ h} {θ : f ⊗ g ⟶ f ⊗ h}
    (e_η : η = η') (e_θ : f ◁ η' = θ) :
    f ◁ η = θ

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h : C
η η' : g ⟶ h
θ : f ⊗ g ⟶ f ⊗ h
e_η : η = η'
e_θ : f ◁ η' = θ
⊢ f ◁ η = θ

Tactic:
simp [e_η, e_θ]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurableSet_setOf : MeasurableSet {a | p a} ↔ Measurable p :=
  ⟨fun h ↦ measurable_to_prop <| by simpa only [preimage_singleton_true], fun h => by
    simpa using h (measurableSet_singleton True)⟩

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
p : α → Prop
h : Measurable p
⊢ MeasurableSet {a | p a}

Tactic:
simpa using h (measurableSet_singleton True)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
p : α → Prop
h : MeasurableSet {a | p a}
⊢ MeasurableSet (p ⁻¹' {True})

Tactic:
simpa only [preimage_singleton_true]

Result:
no goals
-- Mathlib/Data/Sign.lean
theorem nonneg_iff_ne_neg_one {a : SignType} : 0 ≤ a ↔ a ≠ -1

Proof state:
a : SignType
⊢ 0 ≤ a ↔ a ≠ -1

Tactic:
cases a <;> decide

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem memLp_congr_ae {f g : α → E} (hfg : f =ᵐ[μ] g) : MemLp f p μ ↔ MemLp g p μ

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
hfg : f =ᶠ[ae μ] g
⊢ MemLp f p μ ↔ MemLp g p μ

Tactic:
simp only [MemLp, eLpNorm_congr_ae hfg, aestronglyMeasurable_congr hfg]

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem bddAbove_iff {s : Set <| Seminorm 𝕜 E} :
    BddAbove s ↔ BddAbove ((↑) '' s : Set (E → ℝ)) :=
  ⟨fun ⟨q, hq⟩ => ⟨q, forall_mem_image.2 fun _ hp => hq hp⟩, fun H =>
    ⟨sSup s, fun p hp x => by
      dsimp
      rw [Seminorm.coe_sSup_eq' H, iSup_apply]
      rcases H with ⟨q, hq⟩
      exact
        le_ciSup ⟨q x, forall_mem_range.mpr fun i : s => hq (mem_image_of_mem _ i.2) x⟩ ⟨p, hp⟩⟩⟩

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
H : BddAbove (DFunLike.coe '' s)
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
⊢ (fun f => ⇑f) p x ≤ (fun f => ⇑f) (sSup s) x

Tactic:
dsimp

Result:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
H : BddAbove (DFunLike.coe '' s)
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
⊢ p x ≤ (sSup s) x

Proof state:
case intro
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
q : E → ℝ
hq : q ∈ upperBounds (DFunLike.coe '' s)
⊢ p x ≤ ⨆ i, ↑i x

Tactic:
exact
  le_ciSup ⟨q x, forall_mem_range.mpr fun i : s => hq (mem_image_of_mem _ i.2) x⟩ ⟨p, hp⟩

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
H : BddAbove (DFunLike.coe '' s)
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
⊢ p x ≤ ⨆ i, ↑i x

Tactic:
rcases H with ⟨q, hq⟩

Result:
case intro
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
q : E → ℝ
hq : q ∈ upperBounds (DFunLike.coe '' s)
⊢ p x ≤ ⨆ i, ↑i x

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
H : BddAbove (DFunLike.coe '' s)
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
⊢ p x ≤ (sSup s) x

Tactic:
rw [Seminorm.coe_sSup_eq' H, iSup_apply]

Result:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set (Seminorm 𝕜 E)
H : BddAbove (DFunLike.coe '' s)
p : Seminorm 𝕜 E
hp : p ∈ s
x : E
⊢ p x ≤ ⨆ i, ↑i x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem modifyHead_cons (a : α) (l : List α) (f : α → α) :
    (a :: l).modifyHead f = f a :: l

Proof state:
α : Type u
a : α
l : List α
f : α → α
⊢ modifyHead f (a :: l) = f a :: l

Tactic:
rw [modifyHead]

Result:
no goals
-- Mathlib/NumberTheory/FLT/Four.lean
theorem Int.isCoprime_of_sq_sum {r s : ℤ} (h2 : IsCoprime s r) : IsCoprime (r ^ 2 + s ^ 2) r

Proof state:
r s : ℤ
h2 : IsCoprime s r
⊢ IsCoprime (r ^ 2 + s ^ 2) r

Tactic:
rw [sq, sq]

Result:
r s : ℤ
h2 : IsCoprime s r
⊢ IsCoprime (r * r + s * s) r

Proof state:
r s : ℤ
h2 : IsCoprime s r
⊢ IsCoprime (r * r + s * s) r

Tactic:
exact (IsCoprime.mul_left h2 h2).mul_add_left_left r

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive]
lemma prod_fiberwise [DecidableEq κ] (g : ι → κ) (f : ι → α) :
    ∏ j, ∏ i : {i // g i = j}, f i = ∏ i, f i

Proof state:
case e_f.h
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : CommMonoid α
inst✝ : DecidableEq κ
g : ι → κ
f : ι → α
j : κ
⊢ ∏ i : { i // g i = j }, f ↑i = ∏ i ∈ filter (fun i => g i = j) univ, f i

Tactic:
exact (prod_subtype _ (by simp) _).symm

Result:
no goals

Proof state:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : CommMonoid α
inst✝ : DecidableEq κ
g : ι → κ
f : ι → α
⊢ ∏ j : κ, ∏ i : { i // g i = j }, f ↑i = ∏ j : κ, ∏ i ∈ filter (fun i => g i = j) univ, f i

Tactic:
congr with j

Result:
case e_f.h
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : CommMonoid α
inst✝ : DecidableEq κ
g : ι → κ
f : ι → α
j : κ
⊢ ∏ i : { i // g i = j }, f ↑i = ∏ i ∈ filter (fun i => g i = j) univ, f i

Proof state:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : CommMonoid α
inst✝ : DecidableEq κ
g : ι → κ
f : ι → α
⊢ ∏ j : κ, ∏ i : { i // g i = j }, f ↑i = ∏ i : ι, f i

Tactic:
rw [← Finset.prod_fiberwise _ g f]

Result:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : CommMonoid α
inst✝ : DecidableEq κ
g : ι → κ
f : ι → α
⊢ ∏ j : κ, ∏ i : { i // g i = j }, f ↑i = ∏ j : κ, ∏ i ∈ filter (fun i => g i = j) univ, f i

Proof state:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : CommMonoid α
inst✝ : DecidableEq κ
g : ι → κ
f : ι → α
j : κ
⊢ ∀ (x : ι), x ∈ filter (fun i => g i = j) univ ↔ g x = j

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_unitOfList_of_mem [EquivBEq α] [LawfulHashable α]
    {l : List α} {k k' : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ l) :
    getKey? (unitOfList l) k' = some k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a == b) = false) l
mem : k ∈ l
⊢ (unitOfList l).getKey? k' = some k

Tactic:
simp_to_raw using Raw₀.Const.getKey?_insertManyIfNewUnit_empty_list_of_mem

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/CompMap.lean
lemma swap_comp_eq_map {κ : Kernel α (β × γ)} : (swap β γ) ∘ₖ κ = κ.map Prod.swap

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
⊢ swap β γ ∘ₖ κ = κ.map Prod.swap

Tactic:
rw [swap, deterministic_comp_eq_map]

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem mul_floor_map_zero_le_floor_iterate_zero (n : ℕ) : ↑n * ⌊f 0⌋ ≤ ⌊f^[n] 0⌋

Proof state:
case h
f : CircleDeg1Lift
n : ℕ
⊢ 0 + ↑⌊f 0⌋ ≤ f 0

Tactic:
simp [floor_le]

Result:
no goals

Proof state:
f : CircleDeg1Lift
n : ℕ
⊢ 0 + ↑n * ↑⌊f 0⌋ ≤ (⇑f)^[n] 0

Tactic:
apply le_iterate_of_add_int_le_map

Result:
case h
f : CircleDeg1Lift
n : ℕ
⊢ 0 + ↑⌊f 0⌋ ≤ f 0

Proof state:
f : CircleDeg1Lift
n : ℕ
⊢ ↑n * ⌊f 0⌋ ≤ ⌊(⇑f)^[n] 0⌋

Tactic:
rw [le_floor, Int.cast_mul, Int.cast_natCast, ← zero_add ((n : ℝ) * _)]

Result:
f : CircleDeg1Lift
n : ℕ
⊢ 0 + ↑n * ↑⌊f 0⌋ ≤ (⇑f)^[n] 0
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem algebraMap_mk' {A : Type*} [Semiring A] [Algebra R A] (a : R) (s : S) :
    algebraMap _ _ (IsLocalization.mk' T a s) = mk (algebraMap R A a) s

Proof state:
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : R
s : ↥S
⊢ IsLocalization.mk' T a s • 1 = mk ((algebraMap R A) a) s

Tactic:
change _ • mk _ _ = _

Result:
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : R
s : ↥S
⊢ IsLocalization.mk' T a s • mk 1 1 = mk ((algebraMap R A) a) s

Proof state:
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : R
s : ↥S
⊢ (algebraMap T (LocalizedModule S A)) (IsLocalization.mk' T a s) = mk ((algebraMap R A) a) s

Tactic:
rw [Algebra.algebraMap_eq_smul_one]

Result:
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : R
s : ↥S
⊢ IsLocalization.mk' T a s • 1 = mk ((algebraMap R A) a) s

Proof state:
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : R
s : ↥S
⊢ IsLocalization.mk' T a s • mk 1 1 = mk ((algebraMap R A) a) s

Tactic:
rw [mk'_smul_mk, Algebra.algebraMap_eq_smul_one, mul_one]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Gamma.lean
theorem integral_exp_neg_rpow {p : ℝ} (hp : 0 < p) :
    ∫ x in Ioi (0 : ℝ), exp (- x ^ p) = Gamma (1 / p + 1)

Proof state:
case h.e'_2
p : ℝ
hp : 0 < p
⊢ ∫ (x : ℝ) in Ioi 0, rexp (-x ^ p) = ∫ (x : ℝ) in Ioi 0, x ^ 0 * rexp (-x ^ p)

Tactic:
simp_rw [rpow_zero, one_mul]

Result:
no goals

Proof state:
case h.e'_3
p : ℝ
hp : 0 < p
⊢ Gamma (1 / p + 1) = 1 / p * Gamma ((0 + 1) / p)

Tactic:
rw [zero_add, Gamma_add_one (one_div_ne_zero (ne_of_gt hp))]

Result:
no goals

Proof state:
p : ℝ
hp : 0 < p
⊢ ∫ (x : ℝ) in Ioi 0, rexp (-x ^ p) = Gamma (1 / p + 1)

Tactic:
convert (integral_rpow_mul_exp_neg_rpow hp neg_one_lt_zero) using 1

Result:
case h.e'_2
p : ℝ
hp : 0 < p
⊢ ∫ (x : ℝ) in Ioi 0, rexp (-x ^ p) = ∫ (x : ℝ) in Ioi 0, x ^ 0 * rexp (-x ^ p)

case h.e'_3
p : ℝ
hp : 0 < p
⊢ Gamma (1 / p + 1) = 1 / p * Gamma ((0 + 1) / p)
-- Mathlib/Analysis/Normed/Ring/SmoothingSeminorm.lean
theorem smoothingFun_nonneg (hμ1 : μ 1 ≤ 1) (x : R) : 0 ≤ smoothingFun μ x

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
⊢ ∀ᶠ (c : ℕ) in atTop, 0 ≤ smoothingSeminormSeq μ x c

Tactic:
simpa [eventually_atTop, ge_iff_le] using ⟨1, fun _ _ ↦ rpow_nonneg (apply_nonneg μ _) _⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
⊢ 0 ≤ smoothingFun μ x

Tactic:
apply ge_of_tendsto (tendsto_smoothingFun_of_map_one_le_one μ hμ1 x)

Result:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
⊢ ∀ᶠ (c : ℕ) in atTop, 0 ≤ smoothingSeminormSeq μ x c
-- Mathlib/GroupTheory/Perm/Finite.lean
theorem perm_inv_on_of_perm_on_finite {f : Perm α} {p : α → Prop} [Finite { x // p x }]
    (h : ∀ x, p x → p (f x)) {x : α} (hx : p x) : p (f⁻¹ x)

Proof state:
α : Type u
f : Perm α
p : α → Prop
inst✝ : Finite { x // p x }
h : ∀ (x : α), p x → p (f x)
x : α
hx : p x
⊢ p (f⁻¹ x)

Tactic:
have : Finite { x | p x } := by simpa

Result:
α : Type u
f : Perm α
p : α → Prop
inst✝ : Finite { x // p x }
h : ∀ (x : α), p x → p (f x)
x : α
hx : p x
this : Finite ↑{x | p x}
⊢ p (f⁻¹ x)

Proof state:
α : Type u
f : Perm α
p : α → Prop
inst✝ : Finite { x // p x }
h : ∀ (x : α), p x → p (f x)
x : α
hx : p x
this : Finite ↑{x | p x}
⊢ p (f⁻¹ x)

Tactic:
simpa using perm_inv_mapsTo_of_mapsTo (s := {x | p x}) f h hx

Result:
no goals

Proof state:
α : Type u
f : Perm α
p : α → Prop
inst✝ : Finite { x // p x }
h : ∀ (x : α), p x → p (f x)
x : α
hx : p x
⊢ Finite ↑{x | p x}

Tactic:
simpa

Result:
no goals
-- Mathlib/Algebra/Group/Units/Defs.lean
theorem inv_mul_cancel_left (a : αˣ) (b : α) : (↑a⁻¹ : α) * (a * b) = b

Proof state:
α : Type u
inst✝ : Monoid α
a : αˣ
b : α
⊢ ↑a⁻¹ * (↑a * b) = b

Tactic:
rw [← mul_assoc, inv_mul, one_mul]

Result:
no goals
-- Mathlib/Geometry/Manifold/Algebra/LieGroup.lean
theorem ContMDiffOn.div₀ (hf : ContMDiffOn I' I n f s) (hg : ContMDiffOn I' I n g s)
    (h₀ : ∀ x ∈ s, g x ≠ 0) : ContMDiffOn I' I n (f / g) s

Proof state:
𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
H : Type u_2
inst✝¹² : TopologicalSpace H
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
G : Type u_4
inst✝⁹ : TopologicalSpace G
inst✝⁸ : ChartedSpace H G
inst✝⁷ : GroupWithZero G
inst✝⁶ : ContMDiffInv₀ I n G
inst✝⁵ : ContMDiffMul I n G
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 g : M → G
s : Set M
hf : ContMDiffOn I' I n f s
hg : ContMDiffOn I' I n g s
h₀ : ∀ x ∈ s, g x ≠ 0
⊢ ContMDiffOn I' I n (f / g) s

Tactic:
simpa [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem isInducing_coeFn : IsInducing (UniformFun.ofFun ∘ (⇑) : (α →ᵇ β) → α →ᵤ β)

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
⊢ IsInducing (⇑UniformFun.ofFun ∘ DFunLike.coe)

Tactic:
rw [isInducing_iff_nhds]

Result:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
⊢ ∀ (x : α →ᵇ β), 𝓝 x = comap (⇑UniformFun.ofFun ∘ DFunLike.coe) (𝓝 ((⇑UniformFun.ofFun ∘ DFunLike.coe) x))

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f : α →ᵇ β
l : Filter (α →ᵇ β)
⊢ l ≤ 𝓝 f ↔ l ≤ comap (⇑UniformFun.ofFun ∘ DFunLike.coe) (𝓝 ((⇑UniformFun.ofFun ∘ DFunLike.coe) f))

Tactic:
rw [← tendsto_iff_comap, ← tendsto_id', tendsto_iff_tendstoUniformly,
  UniformFun.tendsto_iff_tendstoUniformly]

Result:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f : α →ᵇ β
l : Filter (α →ᵇ β)
⊢ TendstoUniformly (fun i => ⇑(id i)) (⇑f) l ↔
    TendstoUniformly (⇑UniformFun.toFun ∘ ⇑UniformFun.ofFun ∘ DFunLike.coe)
      (UniformFun.toFun ((⇑UniformFun.ofFun ∘ DFunLike.coe) f)) l

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f : α →ᵇ β
l : Filter (α →ᵇ β)
⊢ TendstoUniformly (fun i => ⇑(id i)) (⇑f) l ↔
    TendstoUniformly (⇑UniformFun.toFun ∘ ⇑UniformFun.ofFun ∘ DFunLike.coe)
      (UniformFun.toFun ((⇑UniformFun.ofFun ∘ DFunLike.coe) f)) l

Tactic:
simp [comp_def]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
⊢ ∀ (x : α →ᵇ β), 𝓝 x = comap (⇑UniformFun.ofFun ∘ DFunLike.coe) (𝓝 ((⇑UniformFun.ofFun ∘ DFunLike.coe) x))

Tactic:
refine fun f => eq_of_forall_le_iff fun l => ?_

Result:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f : α →ᵇ β
l : Filter (α →ᵇ β)
⊢ l ≤ 𝓝 f ↔ l ≤ comap (⇑UniformFun.ofFun ∘ DFunLike.coe) (𝓝 ((⇑UniformFun.ofFun ∘ DFunLike.coe) f))
-- Mathlib/Algebra/Group/Conj.lean
theorem isConj_iff_conjugatesOf_eq {a b : α} : IsConj a b ↔ conjugatesOf a = conjugatesOf b :=
  ⟨IsConj.conjugatesOf_eq, fun h => by
    have ha := mem_conjugatesOf_self (a := b)
    rwa [← h] at ha⟩

Proof state:
α : Type u
inst✝ : Monoid α
a b : α
h : conjugatesOf a = conjugatesOf b
ha : b ∈ conjugatesOf b
⊢ IsConj a b

Tactic:
rwa [← h] at ha

Result:
no goals

Proof state:
α : Type u
inst✝ : Monoid α
a b : α
h : conjugatesOf a = conjugatesOf b
⊢ IsConj a b

Tactic:
have ha := mem_conjugatesOf_self (a := b)

Result:
α : Type u
inst✝ : Monoid α
a b : α
h : conjugatesOf a = conjugatesOf b
ha : b ∈ conjugatesOf b
⊢ IsConj a b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Norm.lean
theorem eq_false_eq (p : Prop) : (p = False) = ¬p

Proof state:
p : Prop
⊢ (p = False) = ¬p

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_eq_some_getD [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} {fallback : β} :
    m.contains a = true → get? m a = some (getD m a fallback)

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a : α
fallback : β
⊢ m.contains a = true → get? m a = some (getD m a fallback)

Tactic:
simp_to_model using List.getValue?_eq_some_getValueD

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
theorem basicOpen_eq_zeroLocus_compl (r : A) :
    (basicOpen 𝒜 r : Set (ProjectiveSpectrum 𝒜)) = (zeroLocus 𝒜 {r})ᶜ :=
  Set.ext fun x => by simp only [Set.mem_compl_iff, mem_zeroLocus, Set.singleton_subset_iff]; rfl

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
r : A
x : ProjectiveSpectrum 𝒜
⊢ x ∈ ↑(basicOpen 𝒜 r) ↔ x ∈ (zeroLocus 𝒜 {r})ᶜ

Tactic:
simp only [Set.mem_compl_iff, mem_zeroLocus, Set.singleton_subset_iff]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
r : A
x : ProjectiveSpectrum 𝒜
⊢ x ∈ ↑(basicOpen 𝒜 r) ↔ r ∉ ↑x.asHomogeneousIdeal

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
r : A
x : ProjectiveSpectrum 𝒜
⊢ x ∈ ↑(basicOpen 𝒜 r) ↔ r ∉ ↑x.asHomogeneousIdeal

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/SmoothNumbers.lean
/-- The `Finset` of prime factors of an `s`-factored number is contained in `s`. -/
lemma primeFactors_subset_of_mem_factoredNumbers {s : Finset ℕ} {m : ℕ}
    (hm : m ∈ factoredNumbers s) :
    m.primeFactors ⊆ s

Proof state:
s : Finset ℕ
m : ℕ
hm : m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p ∈ s
⊢ m.primeFactors ⊆ s

Tactic:
exact fun n hn ↦ hm.2 n (mem_primeFactors_iff_mem_primeFactorsList.mp hn)

Result:
no goals

Proof state:
s : Finset ℕ
m : ℕ
hm : m ∈ factoredNumbers s
⊢ m.primeFactors ⊆ s

Tactic:
rw [mem_factoredNumbers] at hm

Result:
s : Finset ℕ
m : ℕ
hm : m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p ∈ s
⊢ m.primeFactors ⊆ s