harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem card_compl_support_modEq [DecidableEq α] {p n : ℕ} [hp : Fact p.Prime] {σ : Perm α}
    (hσ : σ ^ p ^ n = 1) : σ.supportᶜ.card ≡ Fintype.card α [MOD p]

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
m : ℕ
hm : orderOf σ = p ^ m
l : ℕ
hk : p ^ l ∈ σ.cycleType
⊢ p ∣ p ^ l

Tactic:
exact dvd_pow_self _ fun h => (one_lt_of_mem_cycleType hk).ne <| by rw [h, pow_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
k : ℕ
hk : k ∈ σ.cycleType
⊢ p ∣ k

Tactic:
obtain ⟨m, -, hm⟩ := (Nat.dvd_prime_pow hp.out).mp (orderOf_dvd_of_pow_eq_one hσ)

Result:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
k : ℕ
hk : k ∈ σ.cycleType
m : ℕ
hm : orderOf σ = p ^ m
⊢ p ∣ k

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
m : ℕ
hm : orderOf σ = p ^ m
l : ℕ
hk : p ^ l ∈ σ.cycleType
h : l = 0
⊢ 1 = p ^ l

Tactic:
rw [h, pow_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
⊢ p ∣ σ.cycleType.sum

Tactic:
refine Multiset.dvd_sum fun k hk => ?_

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
k : ℕ
hk : k ∈ σ.cycleType
⊢ p ∣ k

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
⊢ σ.supportᶜ.card ≤ Fintype.card α

Tactic:
exact Finset.card_le_univ _

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
⊢ σ.supportᶜ.card ≡ Fintype.card α [MOD p]

Tactic:
rw [Nat.modEq_iff_dvd', ← Finset.card_compl, compl_compl, ← sum_cycleType]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
⊢ p ∣ σ.cycleType.sum

α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
⊢ σ.supportᶜ.card ≤ Fintype.card α

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
k : ℕ
hk : k ∈ σ.cycleType
m : ℕ
hm : orderOf σ = p ^ m
⊢ p ∣ k

Tactic:
obtain ⟨l, -, rfl⟩ := (Nat.dvd_prime_pow hp.out).mp
  ((congr_arg _ hm).mp (dvd_of_mem_cycleType hk))

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
m : ℕ
hm : orderOf σ = p ^ m
l : ℕ
hk : p ^ l ∈ σ.cycleType
⊢ p ∣ p ^ l
-- Mathlib/Data/Nat/Choose/Cast.lean
theorem cast_add_choose {a b : ℕ} : ((a + b).choose a : K) = (a + b)! / (a ! * b !)

Proof state:
K : Type u_1
inst✝¹ : DivisionSemiring K
inst✝ : CharZero K
a b : ℕ
⊢ ↑((a + b).choose a) = ↑(a + b)! / (↑a ! * ↑b !)

Tactic:
rw [cast_choose K (_root_.le_add_right le_rfl), add_tsub_cancel_left]

Result:
no goals
-- Mathlib/Computability/Tape.lean
theorem ListBlank.cons_head_tail {Γ} [Inhabited Γ] : ∀ l : ListBlank Γ, l.tail.cons l.head = l

Proof state:
case h
Γ : Type u_1
inst✝ : Inhabited Γ
l : List Γ
⊢ BlankExtends l (head (Quotient.mk'' l) :: l.tail)

Tactic:
cases l

Result:
case h.nil
Γ : Type u_1
inst✝ : Inhabited Γ
⊢ BlankExtends [] (head (Quotient.mk'' []) :: [].tail)

case h.cons
Γ : Type u_1
inst✝ : Inhabited Γ
head✝ : Γ
tail✝ : List Γ
⊢ BlankExtends (head✝ :: tail✝) (head (Quotient.mk'' (head✝ :: tail✝)) :: (head✝ :: tail✝).tail)

Proof state:
case h
Γ : Type u_1
inst✝ : Inhabited Γ
⊢ ∀ (a : List Γ), cons (head (Quotient.mk'' a)) (tail (Quotient.mk'' a)) = Quotient.mk'' a

Tactic:
refine fun l ↦ Quotient.sound' (Or.inr ?_)

Result:
case h
Γ : Type u_1
inst✝ : Inhabited Γ
l : List Γ
⊢ BlankExtends l (head (Quotient.mk'' l) :: l.tail)

Proof state:
case h.cons
Γ : Type u_1
inst✝ : Inhabited Γ
head✝ : Γ
tail✝ : List Γ
⊢ BlankExtends (head✝ :: tail✝) (head (Quotient.mk'' (head✝ :: tail✝)) :: (head✝ :: tail✝).tail)

Tactic:
rfl

Result:
no goals

Proof state:
case h.nil
Γ : Type u_1
inst✝ : Inhabited Γ
⊢ BlankExtends [] (head (Quotient.mk'' []) :: [].tail)

Tactic:
exact ⟨1, rfl⟩

Result:
no goals

Proof state:
Γ : Type u_1
inst✝ : Inhabited Γ
⊢ ∀ (l : ListBlank Γ), cons l.head l.tail = l

Tactic:
apply Quotient.ind'

Result:
case h
Γ : Type u_1
inst✝ : Inhabited Γ
⊢ ∀ (a : List Γ), cons (head (Quotient.mk'' a)) (tail (Quotient.mk'' a)) = Quotient.mk'' a
-- Mathlib/Analysis/SpecialFunctions/MulExpNegMulSqIntegral.lean
theorem integrable_mulExpNegMulSq_comp (f : C(E, ℝ)) (hε : 0 < ε) :
    Integrable (fun x => mulExpNegMulSq ε (f x)) P

Proof state:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
f : C(E, ℝ)
hε : 0 < ε
⊢ Integrable (fun x => ε.mulExpNegMulSq (f x)) P

Tactic:
apply integrable P ⟨⟨fun x => mulExpNegMulSq ε (f x), by fun_prop⟩, ⟨2 * (sqrt ε)⁻¹, _⟩⟩

Result:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
f : C(E, ℝ)
hε : 0 < ε
⊢ ∀ (x y : E),
    dist ({ toFun := fun x => ε.mulExpNegMulSq (f x), continuous_toFun := ⋯ }.toFun x)
        ({ toFun := fun x => ε.mulExpNegMulSq (f x), continuous_toFun := ⋯ }.toFun y) ≤
      2 * (√ε)⁻¹

Proof state:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
f : C(E, ℝ)
hε : 0 < ε
⊢ ∀ (x y : E),
    dist ({ toFun := fun x => ε.mulExpNegMulSq (f x), continuous_toFun := ⋯ }.toFun x)
        ({ toFun := fun x => ε.mulExpNegMulSq (f x), continuous_toFun := ⋯ }.toFun y) ≤
      2 * (√ε)⁻¹

Tactic:
exact fun x y => dist_mulExpNegMulSq_le_two_mul_sqrt hε (f x) (f y)

Result:
no goals

Proof state:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
f : C(E, ℝ)
hε : 0 < ε
⊢ Continuous fun x => ε.mulExpNegMulSq (f x)

Tactic:
fun_prop

Result:
no goals
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nadd_assoc (a b c) : a ♯ b ♯ c = a ♯ (b ♯ c)

Proof state:
a b c : Ordinal.{u_1}
⊢ a ♯ b ♯ c = a ♯ (b ♯ c)

Tactic:
unfold nadd

Result:
a b c : Ordinal.{u_1}
⊢ (⨆ x, succ (↑x ♯ c)) ⊔ ⨆ x, succ (a ♯ b ♯ ↑x) = (⨆ x, succ (↑x ♯ (b ♯ c))) ⊔ ⨆ x, succ (a ♯ ↑x)

Proof state:
a b c : Ordinal.{u_1}
⊢ Monotone fun b' => succ (a ♯ b')

Tactic:
exact succ_mono.comp fun x y h ↦ nadd_le_nadd_left h _

Result:
no goals

Proof state:
a b c : Ordinal.{u_1}
⊢ (⨆ a', succ (↑a' ♯ b ♯ c)) ⊔ ((⨆ b', succ (a ♯ ↑b' ♯ c)) ⊔ ⨆ x, succ (a ♯ b ♯ ↑x)) =
    (⨆ x, succ (↑x ♯ (b ♯ c))) ⊔ ((⨆ a', succ (a ♯ (↑a' ♯ c))) ⊔ ⨆ b', succ (a ♯ (b ♯ ↑b')))

Tactic:
congr <;> ext x <;> cases x <;> apply congr_arg _ (nadd_assoc _ _ _)

Result:
no goals

Proof state:
a b c : Ordinal.{u_1}
⊢ Monotone fun a' => succ (a' ♯ c)

Tactic:
exact succ_mono.comp fun x y h ↦ nadd_le_nadd_right h _

Result:
no goals

Proof state:
a b c : Ordinal.{u_1}
⊢ (⨆ x, succ (↑x ♯ c)) ⊔ ⨆ x, succ (a ♯ b ♯ ↑x) = (⨆ x, succ (↑x ♯ (b ♯ c))) ⊔ ⨆ x, succ (a ♯ ↑x)

Tactic:
rw [iSup_nadd_of_monotone fun a' ↦ succ (a' ♯ c), iSup_nadd_of_monotone fun b' ↦ succ (a ♯ b'),
  max_assoc]

Result:
a b c : Ordinal.{u_1}
⊢ (⨆ a', succ (↑a' ♯ b ♯ c)) ⊔ ((⨆ b', succ (a ♯ ↑b' ♯ c)) ⊔ ⨆ x, succ (a ♯ b ♯ ↑x)) =
    (⨆ x, succ (↑x ♯ (b ♯ c))) ⊔ ((⨆ a', succ (a ♯ (↑a' ♯ c))) ⊔ ⨆ b', succ (a ♯ (b ♯ ↑b')))

a b c : Ordinal.{u_1}
⊢ Monotone fun b' => succ (a ♯ b')

a b c : Ordinal.{u_1}
⊢ Monotone fun a' => succ (a' ♯ c)
-- Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean
lemma hasColimitsOfShape_discrete (X Y : C) (p : X ⟶ Y) :
    HasColimitsOfShape
      (Discrete (FunctorObjIndex I.homFamily p)) C

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
p : X ⟶ Y
this : LocallySmall.{w, v, u} C
⊢ HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C

Tactic:
haveI := isSmall I κ

Result:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
p : X ⟶ Y
this✝ : LocallySmall.{w, v, u} C
this : IsSmall.{w, v, u} I
⊢ HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
p : X ⟶ Y
⊢ HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C

Tactic:
haveI := locallySmall I κ

Result:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
p : X ⟶ Y
this : LocallySmall.{w, v, u} C
⊢ HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
p : X ⟶ Y
this✝ : LocallySmall.{w, v, u} C
this : IsSmall.{w, v, u} I
⊢ HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C

Tactic:
haveI := hasCoproducts I κ

Result:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
p : X ⟶ Y
this✝¹ : LocallySmall.{w, v, u} C
this✝ : IsSmall.{w, v, u} I
this : HasCoproducts C
⊢ HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
p : X ⟶ Y
this✝¹ : LocallySmall.{w, v, u} C
this✝ : IsSmall.{w, v, u} I
this : HasCoproducts C
⊢ HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C

Tactic:
exact hasColimitsOfShape_of_equivalence
  (Discrete.equivalence (equivShrink.{w} _)).symm

Result:
no goals
-- Mathlib/Order/Defs/LinearOrder.lean
lemma compare_ge_iff_ge : compare a b ≠ .lt ↔ a ≥ b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ compare a b ≠ Ordering.lt ↔ a ≥ b

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

Result:
case lt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ a < b

case eq
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ b ≤ a

case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ b ≤ a

Proof state:
case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ b ≤ a

Tactic:
exact le_of_lt <| compare_gt_iff_gt.1 h

Result:
no goals

Proof state:
case lt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ a < b

Tactic:
exact compare_lt_iff_lt.1 h

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_exchange (ha : a ∉ s) (hb : b ∈ s) : (insert a (s \ {b})).encard = s.encard

Proof state:
α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ a ∉ s \ {b}

Tactic:
simp_all only [not_true, mem_diff, mem_singleton_iff, false_and, not_false_eq_true]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ (insert a (s \ {b})).encard = s.encard

Tactic:
rw [encard_insert_of_not_mem, encard_diff_singleton_add_one hb]

Result:
α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ a ∉ s \ {b}
-- Mathlib/Probability/Moments/ComplexMGF.lean
lemma norm_complexMGF_le_mgf : ‖complexMGF X μ z‖ ≤ mgf X μ z.re

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
⊢ ‖∫ (x : Ω), cexp (↑z.re * ↑(X x)) * cexp (↑z.im * I * ↑(X x)) ∂μ‖ ≤ mgf X μ z.re

Tactic:
calc ‖∫ ω, cexp (z.re * X ω) * cexp (z.im * I * X ω) ∂μ‖
_ ≤ ∫ ω, ‖cexp (z.re * X ω) * cexp (z.im * I * X ω)‖ ∂μ := norm_integral_le_integral_norm _
_ = ∫ ω, rexp (z.re * X ω) ∂μ := by simp [Complex.norm_exp]

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
⊢ ∫ (ω : Ω), ‖cexp (↑z.re * ↑(X ω)) * cexp (↑z.im * I * ↑(X ω))‖ ∂μ = ∫ (ω : Ω), rexp (z.re * X ω) ∂μ

Tactic:
simp [Complex.norm_exp]

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
⊢ ‖complexMGF X μ z‖ ≤ mgf X μ z.re

Tactic:
rw [complexMGF, ← re_add_im z]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
⊢ ‖∫ (x : Ω), (fun ω => cexp ((↑z.re + ↑z.im * I) * ↑(X ω))) x ∂μ‖ ≤ mgf X μ (↑z.re + ↑z.im * I).re

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
⊢ ‖∫ (x : Ω), (fun ω => cexp ((↑z.re + ↑z.im * I) * ↑(X ω))) x ∂μ‖ ≤ mgf X μ (↑z.re + ↑z.im * I).re

Tactic:
simp_rw [add_mul, Complex.exp_add, re_add_im]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
⊢ ‖∫ (x : Ω), cexp (↑z.re * ↑(X x)) * cexp (↑z.im * I * ↑(X x)) ∂μ‖ ≤ mgf X μ z.re
-- Mathlib/MeasureTheory/Integral/Gamma.lean
theorem Complex.integral_exp_neg_mul_rpow {p b : ℝ} (hp : 1 ≤ p) (hb : 0 < b) :
    ∫ x : ℂ, rexp (- b * ‖x‖ ^ p) = π * b ^ (-2 / p) * Real.Gamma (2 / p + 1)

Proof state:
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
⊢ ∫ (x : ℂ), rexp (-b * ‖x‖ ^ p) = π * b ^ (-2 / p) * Real.Gamma (2 / p + 1)

Tactic:
convert (integral_rpow_mul_exp_neg_mul_rpow hp (by linarith : (-2 : ℝ) < 0)) hb using 1

Result:
case h.e'_2
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
⊢ ∫ (x : ℂ), rexp (-b * ‖x‖ ^ p) = ∫ (x : ℂ), ‖x‖ ^ 0 * rexp (-b * ‖x‖ ^ p)

case h.e'_3
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
⊢ π * b ^ (-2 / p) * Real.Gamma (2 / p + 1) = 2 * π / p * b ^ (-(0 + 2) / p) * Real.Gamma ((0 + 2) / p)

Proof state:
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
⊢ -2 < 0

Tactic:
linarith

Result:
no goals

Proof state:
case h.e'_3
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
⊢ π * b ^ (-2 / p) * (2 / p * Real.Gamma (2 / p)) = 2 * π / p * b ^ (-2 / p) * Real.Gamma (2 / p)

Tactic:
ring

Result:
no goals

Proof state:
case h.e'_3
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
⊢ π * b ^ (-2 / p) * Real.Gamma (2 / p + 1) = 2 * π / p * b ^ (-(0 + 2) / p) * Real.Gamma ((0 + 2) / p)

Tactic:
rw [zero_add, Real.Gamma_add_one (div_ne_zero two_ne_zero (by linarith))]

Result:
case h.e'_3
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
⊢ π * b ^ (-2 / p) * (2 / p * Real.Gamma (2 / p)) = 2 * π / p * b ^ (-2 / p) * Real.Gamma (2 / p)

Proof state:
case h.e'_2
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
⊢ ∫ (x : ℂ), rexp (-b * ‖x‖ ^ p) = ∫ (x : ℂ), ‖x‖ ^ 0 * rexp (-b * ‖x‖ ^ p)

Tactic:
simp_rw [rpow_zero, one_mul]

Result:
no goals

Proof state:
p b : ℝ
hp : 1 ≤ p
hb : 0 < b
⊢ p ≠ 0

Tactic:
linarith

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Maps.lean
theorem mapEdgeSet.injective (hinj : Function.Injective f) : Function.Injective f.mapEdgeSet

Proof state:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective ⇑f
⊢ Injective f.mapEdgeSet

Tactic:
rintro ⟨e₁, h₁⟩ ⟨e₂, h₂⟩

Result:
case mk.mk
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective ⇑f
e₁ : Sym2 V
h₁ : e₁ ∈ G.edgeSet
e₂ : Sym2 V
h₂ : e₂ ∈ G.edgeSet
⊢ f.mapEdgeSet ⟨e₁, h₁⟩ = f.mapEdgeSet ⟨e₂, h₂⟩ → ⟨e₁, h₁⟩ = ⟨e₂, h₂⟩

Proof state:
case mk.mk
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective ⇑f
e₁ : Sym2 V
h₁ : e₁ ∈ G.edgeSet
e₂ : Sym2 V
h₂ : e₂ ∈ G.edgeSet
⊢ ⟨Sym2.map (⇑f) e₁, ⋯⟩ = ⟨Sym2.map (⇑f) e₂, ⋯⟩ → ⟨e₁, h₁⟩ = ⟨e₂, h₂⟩

Tactic:
repeat rw [Subtype.mk_eq_mk]

Result:
case mk.mk
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective ⇑f
e₁ : Sym2 V
h₁ : e₁ ∈ G.edgeSet
e₂ : Sym2 V
h₂ : e₂ ∈ G.edgeSet
⊢ Sym2.map (⇑f) e₁ = Sym2.map (⇑f) e₂ → e₁ = e₂

Proof state:
case mk.mk
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective ⇑f
e₁ : Sym2 V
h₁ : e₁ ∈ G.edgeSet
e₂ : Sym2 V
h₂ : e₂ ∈ G.edgeSet
⊢ Sym2.map (⇑f) e₁ = Sym2.map (⇑f) e₂ → ⟨e₁, h₁⟩ = ⟨e₂, h₂⟩

Tactic:
rw [Subtype.mk_eq_mk]

Result:
case mk.mk
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective ⇑f
e₁ : Sym2 V
h₁ : e₁ ∈ G.edgeSet
e₂ : Sym2 V
h₂ : e₂ ∈ G.edgeSet
⊢ Sym2.map (⇑f) e₁ = Sym2.map (⇑f) e₂ → e₁ = e₂

Proof state:
case mk.mk
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective ⇑f
e₁ : Sym2 V
h₁ : e₁ ∈ G.edgeSet
e₂ : Sym2 V
h₂ : e₂ ∈ G.edgeSet
⊢ Sym2.map (⇑f) e₁ = Sym2.map (⇑f) e₂ → e₁ = e₂

Tactic:
apply Sym2.map.injective hinj

Result:
no goals

Proof state:
case mk.mk
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective ⇑f
e₁ : Sym2 V
h₁ : e₁ ∈ G.edgeSet
e₂ : Sym2 V
h₂ : e₂ ∈ G.edgeSet
⊢ f.mapEdgeSet ⟨e₁, h₁⟩ = f.mapEdgeSet ⟨e₂, h₂⟩ → ⟨e₁, h₁⟩ = ⟨e₂, h₂⟩

Tactic:
dsimp [Hom.mapEdgeSet]

Result:
case mk.mk
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective ⇑f
e₁ : Sym2 V
h₁ : e₁ ∈ G.edgeSet
e₂ : Sym2 V
h₂ : e₂ ∈ G.edgeSet
⊢ ⟨Sym2.map (⇑f) e₁, ⋯⟩ = ⟨Sym2.map (⇑f) e₂, ⋯⟩ → ⟨e₁, h₁⟩ = ⟨e₂, h₂⟩
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
@[simp]
lemma leadingCoeff_mul (p q : R[X]) : leadingCoeff (p * q) = leadingCoeff p * leadingCoeff q

Proof state:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : p = 0
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff

Tactic:
simp only [hp, zero_mul, leadingCoeff_zero]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
exact mul_ne_zero (mt leadingCoeff_eq_zero.1 hp) (mt leadingCoeff_eq_zero.1 hq)

Result:
no goals

Proof state:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff

Tactic:
rw [leadingCoeff_mul']

Result:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff

Tactic:
by_cases hp : p = 0

Result:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : p = 0
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff

case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff

Proof state:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : q = 0
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff

Tactic:
simp only [hq, mul_zero, leadingCoeff_zero]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff

Tactic:
by_cases hq : q = 0

Result:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : q = 0
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff

case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff
-- Mathlib/NumberTheory/FactorisationProperties.lean
theorem Prime.not_perfect (h : Prime p) : ¬ Perfect p

Proof state:
p : ℕ
h : Prime p
⊢ ¬p.Pseudoperfect → ¬p.Perfect

Tactic:
exact not_imp_not.mpr (Perfect.pseudoperfect)

Result:
no goals

Proof state:
p : ℕ
h : Prime p
⊢ ¬p.Perfect

Tactic:
have h1 := Prime.not_pseudoperfect h

Result:
p : ℕ
h : Prime p
h1 : ¬p.Pseudoperfect
⊢ ¬p.Perfect

Proof state:
p : ℕ
h : Prime p
h1 : ¬p.Pseudoperfect
⊢ ¬p.Perfect

Tactic:
revert h1

Result:
p : ℕ
h : Prime p
⊢ ¬p.Pseudoperfect → ¬p.Perfect
-- Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
theorem pullback_lift_map_isPullback {X Y S X' Y' S' : C} (f : X ⟶ S) (g : Y ⟶ S) (f' : X' ⟶ S')
    (g' : Y' ⟶ S') (i₁ : X ⟶ X') (i₂ : Y ⟶ Y') (i₃ : S ⟶ S') (e₁ : f ≫ i₃ = i₁ ≫ f')
    (e₂ : g ≫ i₃ = i₂ ≫ g') [Mono i₃] :
    IsPullback (pullback.lift (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst _ _) (lift_fst _ _ _))
      (pullback.lift (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd _ _) (lift_snd _ _ _))
      (pullback.fst _ _) (pullback.fst _ _) :=
  IsPullback.of_iso_pullback ⟨by rw [lift_fst, lift_fst]⟩
    (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).symm (by simp) (by simp)

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).symm.hom ≫ snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) =
    lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯ ≫ fst (fst f' g') i₁ =
    lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯ ≫ fst (snd f' g') i₂

Tactic:
rw [lift_fst, lift_fst]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).symm.hom ≫ fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) =
    lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/HashMap/RawLemmas.lean
theorem ext {m m' : Raw α β} : m.inner = m'.inner → m = m'

Proof state:
case mk.mk
α : Type u
β : Type v
inner✝ : DHashMap.Raw α fun x => β
⊢ { inner := inner✝ } = { inner := { inner := inner✝ }.inner }

Tactic:
rfl

Result:
no goals

Proof state:
case mk
α : Type u
β : Type v
m' : Raw α β
inner✝ : DHashMap.Raw α fun x => β
⊢ { inner := inner✝ }.inner = m'.inner → { inner := inner✝ } = m'

Tactic:
cases m'

Result:
case mk.mk
α : Type u
β : Type v
inner✝¹ inner✝ : DHashMap.Raw α fun x => β
⊢ { inner := inner✝¹ }.inner = { inner := inner✝ }.inner → { inner := inner✝¹ } = { inner := inner✝ }

Proof state:
α : Type u
β : Type v
m m' : Raw α β
⊢ m.inner = m'.inner → m = m'

Tactic:
cases m

Result:
case mk
α : Type u
β : Type v
m' : Raw α β
inner✝ : DHashMap.Raw α fun x => β
⊢ { inner := inner✝ }.inner = m'.inner → { inner := inner✝ } = m'

Proof state:
case mk.mk
α : Type u
β : Type v
inner✝¹ inner✝ : DHashMap.Raw α fun x => β
⊢ { inner := inner✝¹ }.inner = { inner := inner✝ }.inner → { inner := inner✝¹ } = { inner := inner✝ }

Tactic:
rintro rfl

Result:
case mk.mk
α : Type u
β : Type v
inner✝ : DHashMap.Raw α fun x => β
⊢ { inner := inner✝ } = { inner := { inner := inner✝ }.inner }