harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/ModelTheory/Skolem.lean
theorem card_functions_sum_skolem₁_le : #(Σ n, (L.sum L.skolem₁).Functions n) ≤ max ℵ₀ L.card

Proof state:
L : Language
⊢ #((n : ℕ) × L.BoundedFormula Empty (n + 1)) ≤ #((n : ℕ) × L.BoundedFormula Empty n)

Tactic:
exact
  ⟨⟨Sigma.map Nat.succ fun _ => id,
      Nat.succ_injective.sigma_map fun _ => Function.injective_id⟩⟩

Result:
no goals

Proof state:
L : Language
⊢ lift.{max u v, max u v} (ℵ₀ ⊔ (lift.{max u v, 0} #Empty + lift.{0, max u v} L.card)) ≤
    lift.{max u v, max u v} (ℵ₀ ⊔ L.card)

Tactic:
simp only [mk_empty, lift_zero, lift_uzero, zero_add]

Result:
L : Language
⊢ lift.{max u v, max u v} (ℵ₀ ⊔ L.card) ≤ lift.{max u v, max u v} (ℵ₀ ⊔ L.card)

Proof state:
L : Language
⊢ lift.{max u v, max u v} (ℵ₀ ⊔ L.card) ≤ lift.{max u v, max u v} (ℵ₀ ⊔ L.card)

Tactic:
rfl

Result:
no goals

Proof state:
L : Language
⊢ #((n : ℕ) × L.BoundedFormula Empty n) ≤ ℵ₀ ⊔ L.card

Tactic:
refine _root_.trans BoundedFormula.card_le (lift_le.{max u v}.1 ?_)

Result:
L : Language
⊢ lift.{max u v, max u v} (ℵ₀ ⊔ (lift.{max u v, 0} #Empty + lift.{0, max u v} L.card)) ≤
    lift.{max u v, max u v} (ℵ₀ ⊔ L.card)

Proof state:
L : Language
⊢ #((n : ℕ) × (L.sum L.skolem₁).Functions n) ≤ ℵ₀ ⊔ L.card

Tactic:
rw [card_functions_sum_skolem₁]

Result:
L : Language
⊢ #((n : ℕ) × L.BoundedFormula Empty (n + 1)) ≤ ℵ₀ ⊔ L.card

Proof state:
L : Language
⊢ #((n : ℕ) × L.BoundedFormula Empty (n + 1)) ≤ ℵ₀ ⊔ L.card

Tactic:
trans #(Σ n, L.BoundedFormula Empty n)

Result:
L : Language
⊢ #((n : ℕ) × L.BoundedFormula Empty (n + 1)) ≤ #((n : ℕ) × L.BoundedFormula Empty n)

L : Language
⊢ #((n : ℕ) × L.BoundedFormula Empty n) ≤ ℵ₀ ⊔ L.card
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
theorem quotQuotEquivComm_symm : (quotQuotEquivComm I J).symm = quotQuotEquivComm J I

Proof state:
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ (quotQuotEquivComm I J).symm = quotQuotEquivComm J I

Tactic:
change (((quotQuotEquivQuotSup I J).trans (quotEquivOfEq (sup_comm ..))).trans
  (quotQuotEquivQuotSup J I).symm).symm =
    ((quotQuotEquivQuotSup J I).trans (quotEquivOfEq (sup_comm ..))).trans
      (quotQuotEquivQuotSup I J).symm

Result:
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ (((quotQuotEquivQuotSup I J).trans (quotEquivOfEq ⋯)).trans (quotQuotEquivQuotSup J I).symm).symm =
    ((quotQuotEquivQuotSup J I).trans (quotEquivOfEq ⋯)).trans (quotQuotEquivQuotSup I J).symm

Proof state:
R : Type u
inst✝ : CommRing R
I J : Ideal R
⊢ (((quotQuotEquivQuotSup I J).trans (quotEquivOfEq ⋯)).trans (quotQuotEquivQuotSup J I).symm).symm =
    ((quotQuotEquivQuotSup J I).trans (quotEquivOfEq ⋯)).trans (quotQuotEquivQuotSup I J).symm

Tactic:
ext r

Result:
case h
R : Type u
inst✝ : CommRing R
I J : Ideal R
r : (R ⧸ J) ⧸ map (Ideal.Quotient.mk J) I
⊢ (((quotQuotEquivQuotSup I J).trans (quotEquivOfEq ⋯)).trans (quotQuotEquivQuotSup J I).symm).symm r =
    (((quotQuotEquivQuotSup J I).trans (quotEquivOfEq ⋯)).trans (quotQuotEquivQuotSup I J).symm) r

Proof state:
case h
R : Type u
inst✝ : CommRing R
I J : Ideal R
r : (R ⧸ J) ⧸ map (Ideal.Quotient.mk J) I
⊢ (quotQuotEquivQuotSup I J).symm ((quotEquivOfEq ⋯).symm ((quotQuotEquivQuotSup J I) r)) =
    (quotQuotEquivQuotSup I J).symm ((quotEquivOfEq ⋯) ((quotQuotEquivQuotSup J I) r))

Tactic:
rfl

Result:
no goals

Proof state:
case h
R : Type u
inst✝ : CommRing R
I J : Ideal R
r : (R ⧸ J) ⧸ map (Ideal.Quotient.mk J) I
⊢ (((quotQuotEquivQuotSup I J).trans (quotEquivOfEq ⋯)).trans (quotQuotEquivQuotSup J I).symm).symm r =
    (((quotQuotEquivQuotSup J I).trans (quotEquivOfEq ⋯)).trans (quotQuotEquivQuotSup I J).symm) r

Tactic:
dsimp

Result:
case h
R : Type u
inst✝ : CommRing R
I J : Ideal R
r : (R ⧸ J) ⧸ map (Ideal.Quotient.mk J) I
⊢ (quotQuotEquivQuotSup I J).symm ((quotEquivOfEq ⋯).symm ((quotQuotEquivQuotSup J I) r)) =
    (quotQuotEquivQuotSup I J).symm ((quotEquivOfEq ⋯) ((quotQuotEquivQuotSup J I) r))
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVecOperator/Zip.lean
theorem zip_le_size {aig : AIG α} (target : ZipTarget aig len) :
    aig.decls.size ≤ (zip aig target).1.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
aig : AIG α
target : ZipTarget aig len
⊢ aig.decls.size ≤ (zip aig target).aig.decls.size

Tactic:
unfold zip

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
aig : AIG α
target : ZipTarget aig len
⊢ aig.decls.size ≤ (zip.go aig 0 empty ⋯ target.input.lhs target.input.rhs target.func).aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
len : Nat
aig : AIG α
target : ZipTarget aig len
⊢ aig.decls.size ≤ (zip.go aig 0 empty ⋯ target.input.lhs target.input.rhs target.func).aig.decls.size

Tactic:
apply zip.go_le_size

Result:
no goals
-- Mathlib/Analysis/Calculus/Gradient/Basic.lean
theorem DifferentiableAt.hasGradientAt (h : DifferentiableAt 𝕜 f x) :
    HasGradientAt f (∇ f x) x

Proof state:
𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
f : F → 𝕜
x : F
h : DifferentiableAt 𝕜 f x
⊢ HasFDerivAt f (fderiv 𝕜 f x) x

Tactic:
exact h.hasFDerivAt

Result:
no goals

Proof state:
𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
f : F → 𝕜
x : F
h : DifferentiableAt 𝕜 f x
⊢ HasGradientAt f (∇ f x) x

Tactic:
rw [hasGradientAt_iff_hasFDerivAt, gradient, (toDual 𝕜 F).apply_symm_apply (fderiv 𝕜 f x)]

Result:
𝕜 : Type u_1
F : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace F
f : F → 𝕜
x : F
h : DifferentiableAt 𝕜 f x
⊢ HasFDerivAt f (fderiv 𝕜 f x) x
-- Mathlib/RingTheory/Support.lean
lemma LocalizedModule.subsingleton_iff_support_subset {f : R} :
    Subsingleton (LocalizedModule (.powers f) M) ↔
      Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}

Proof state:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
⊢ (∀ (m : M), ∃ r ∈ Submonoid.powers f, r • m = 0) → Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}

Tactic:
rintro H x hx' f rfl

Result:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : PrimeSpectrum R
hx' : x ∈ Module.support R M
f : R
H : ∀ (m : M), ∃ r ∈ Submonoid.powers f, r • m = 0
⊢ f ∈ ↑x.asIdeal

Proof state:
case neg.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
h : ¬(Submodule.span R {m}).annihilator = ⊤
n : ℕ
hn : f ^ n ∈ (Submodule.span R {m}).annihilator
⊢ ∃ r ∈ Submonoid.powers f, r • m = 0

Tactic:
exact ⟨_, ⟨n, rfl⟩, (Submodule.mem_annihilator_span_singleton _ _).mp hn⟩

Result:
no goals
-- Mathlib/Data/List/Destutter.lean
theorem mem_destutter' (a) : a ∈ l.destutter' R a

Proof state:
case nil
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a : α
⊢ a ∈ destutter' R a []

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
l : List α
hl : a ∈ destutter' R a l
⊢ a ∈ destutter' R a (b :: l)

Tactic:
rw [destutter']

Result:
case cons
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
l : List α
hl : a ∈ destutter' R a l
⊢ a ∈ if R a b then a :: destutter' R b l else destutter' R a l

Proof state:
case pos
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
l : List α
hl : a ∈ destutter' R a l
h✝ : R a b
⊢ a ∈ a :: destutter' R b l

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a : α
⊢ a ∈ destutter' R a l

Tactic:
induction' l with b l hl

Result:
case nil
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a : α
⊢ a ∈ destutter' R a []

case cons
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
l : List α
hl : a ∈ destutter' R a l
⊢ a ∈ destutter' R a (b :: l)

Proof state:
case neg
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
l : List α
hl : a ∈ destutter' R a l
h✝ : ¬R a b
⊢ a ∈ destutter' R a l

Tactic:
assumption

Result:
no goals

Proof state:
case cons
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
l : List α
hl : a ∈ destutter' R a l
⊢ a ∈ if R a b then a :: destutter' R b l else destutter' R a l

Tactic:
split_ifs

Result:
case pos
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
l : List α
hl : a ∈ destutter' R a l
h✝ : R a b
⊢ a ∈ a :: destutter' R b l

case neg
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
l : List α
hl : a ∈ destutter' R a l
h✝ : ¬R a b
⊢ a ∈ destutter' R a l
-- Mathlib/RepresentationTheory/Rep.lean
theorem ρ_self_inv_apply {G : Type u} [Group G] {A : Rep k G} (g : G) (x : A) :
    A.ρ g (A.ρ g⁻¹ x) = x :=
  show (A.ρ g * A.ρ g⁻¹) x = x by rw [← map_mul, mul_inv_cancel, map_one, LinearMap.one_apply]

Proof state:
k : Type u
inst✝¹ : CommRing k
G : Type u
inst✝ : Group G
A : Rep k G
g : G
x : ↑A.V
⊢ (A.ρ g * A.ρ g⁻¹) x = x

Tactic:
rw [← map_mul, mul_inv_cancel, map_one, LinearMap.one_apply]

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem dist_of_re_eq (h : z.re = w.re) : dist z w = dist (log z.im) (log w.im)

Proof state:
z w : ℍ
h : z.re = w.re
⊢ 0 < z.im / w.im

Tactic:
positivity

Result:
no goals

Proof state:
case e_a
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ z.im * (w.im * z.im * 2) - w.im * (z.im * z.im + w.im * w.im) = w.im * (z.im * z.im - w.im * w.im)

Tactic:
ring

Result:
no goals

Proof state:
z w : ℍ
h : z.re = w.re
⊢ dist z w = dist (log z.im) (log w.im)

Tactic:
have h₀ : 0 < z.im / w.im := by positivity

Result:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ dist z w = dist (log z.im) (log w.im)

Proof state:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ dist z.im (w.im * ((z.im / w.im + w.im / z.im) / 2)) = |w.im| * |(z.im / w.im - w.im / z.im) / 2|

Tactic:
simp only [← _root_.abs_mul, coe_im, Real.dist_eq]

Result:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ |z.im - w.im * ((z.im / w.im + w.im / z.im) / 2)| = |w.im * ((z.im / w.im - w.im / z.im) / 2)|

Proof state:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ dist z.im (w.im * ((z.im / w.im + w.im / z.im) / 2)) = w.im * |(z.im / w.im - w.im / z.im) / 2|

Tactic:
nth_rw 4 [← abs_of_pos w.im_pos]

Result:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ dist z.im (w.im * ((z.im / w.im + w.im / z.im) / 2)) = |w.im| * |(z.im / w.im - w.im / z.im) / 2|

Proof state:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ dist z w = dist (log z.im) (log w.im)

Tactic:
rw [dist_eq_iff_dist_coe_center_eq, Real.dist_eq, ← abs_sinh, ← log_div z.im_ne_zero w.im_ne_zero,
  sinh_log h₀, dist_of_re_eq, coe_im, coe_im, center_im, cosh_abs, cosh_log h₀, inv_div] <;>
[skip; exact h]

Result:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ dist z.im (w.im * ((z.im / w.im + w.im / z.im) / 2)) = w.im * |(z.im / w.im - w.im / z.im) / 2|

Proof state:
case e_a
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ z.im - w.im * ((z.im / w.im + w.im / z.im) / 2) = w.im * ((z.im / w.im - w.im / z.im) / 2)

Tactic:
field_simp

Result:
case e_a
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ z.im * (w.im * z.im * 2) - w.im * (z.im * z.im + w.im * w.im) = w.im * (z.im * z.im - w.im * w.im)

Proof state:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ |z.im - w.im * ((z.im / w.im + w.im / z.im) / 2)| = |w.im * ((z.im / w.im - w.im / z.im) / 2)|

Tactic:
congr 1

Result:
case e_a
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ z.im - w.im * ((z.im / w.im + w.im / z.im) / 2) = w.im * ((z.im / w.im - w.im / z.im) / 2)
-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem finprod_heightOneSpectrum_factorization {I : FractionalIdeal R⁰ K} (hI : I ≠ 0) {a : R}
    {J : Ideal R} (haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J) :
    ∏ᶠ v : HeightOneSpectrum R, (v.asIdeal : FractionalIdeal R⁰ K) ^
      ((Associates.mk v.asIdeal).count (Associates.mk J).factors -
        (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors : ℤ) = I

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
hJ_ne_zero : J ≠ 0
hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J
ha_ne_zero : Ideal.span {a} ≠ 0
ha :
  ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
    ↑(Ideal.span {a})
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)) =
    (∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors)) *
      ∏ᶠ (x : HeightOneSpectrum R),
        ↑x.asIdeal ^ (-↑((Associates.mk x.asIdeal).count (Associates.mk (Ideal.span {a})).factors))

Tactic:
rw [← finprod_mul_distrib (Ideal.finite_mulSupport_coe hJ_ne_zero)
  (Ideal.finite_mulSupport_inv ha_ne_zero)]

Result:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
hJ_ne_zero : J ≠ 0
hJ : ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) = ↑J
ha_ne_zero : Ideal.span {a} ≠ 0
ha :
  ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) =
    ↑(Ideal.span {a})
⊢ ∏ᶠ (v : HeightOneSpectrum R),
      ↑v.asIdeal ^
        (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
          ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)) =
    ∏ᶠ (i : HeightOneSpectrum R),
      ↑i.asIdeal ^ ↑((Associates.mk i.asIdeal).count (Associates.mk J).factors) *
        ↑i.asIdeal ^ (-↑((Associates.mk i.asIdeal).count (Associates.mk (Ideal.span {a})).factors))
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem exists_le_hasSum_of_le {f g : β → ℝ≥0} {r : ℝ≥0} (hgf : ∀ b, g b ≤ f b) (hfr : HasSum f r) :
    ∃ p ≤ r, HasSum g p :=
  have : (∑' b, (g b : ℝ≥0∞)) ≤ r

Proof state:
β : Type u_2
f g : β → ℝ≥0
r : ℝ≥0
hgf : ∀ (b : β), g b ≤ f b
hfr : HasSum f r
b : β
⊢ ↑(g b) ≤ ↑(f b)

Tactic:
exact ENNReal.coe_le_coe.2 (hgf _)

Result:
no goals

Proof state:
β : Type u_2
f g : β → ℝ≥0
r : ℝ≥0
hgf : ∀ (b : β), g b ≤ f b
hfr : HasSum f r
⊢ ∑' (b : β), ↑(g b) ≤ ↑r

Tactic:
refine hasSum_le (fun b => ?_) ENNReal.summable.hasSum (ENNReal.hasSum_coe.2 hfr)

Result:
β : Type u_2
f g : β → ℝ≥0
r : ℝ≥0
hgf : ∀ (b : β), g b ≤ f b
hfr : HasSum f r
b : β
⊢ ↑(g b) ≤ ↑(f b)
-- Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
theorem continuousAt_rpow_const_of_pos {x : ℝ≥0∞} {y : ℝ} (h : 0 < y) :
    ContinuousAt (fun a : ℝ≥0∞ => a ^ y) x

Proof state:
x : ℝ≥0∞
y : ℝ
h : 0 < y
⊢ ContinuousAt (fun a => a ^ y) x

Tactic:
by_cases hx : x = ⊤

Result:
case pos
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : x = ⊤
⊢ ContinuousAt (fun a => a ^ y) x

case neg
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : ¬x = ⊤
⊢ ContinuousAt (fun a => a ^ y) x

Proof state:
case neg.intro
y : ℝ
h : 0 < y
x : ℝ≥0
⊢ ContinuousAt ((fun a => a ^ y) ∘ ofNNReal) x

Tactic:
convert continuous_coe.continuousAt.comp (NNReal.continuousAt_rpow_const (Or.inr h.le)) using 1

Result:
case h.e'_5
y : ℝ
h : 0 < y
x : ℝ≥0
⊢ (fun a => a ^ y) ∘ ofNNReal = ofNNReal ∘ fun z => z ^ y

Proof state:
case h.e'_5
y : ℝ
h : 0 < y
x : ℝ≥0
⊢ (fun a => a ^ y) ∘ ofNNReal = ofNNReal ∘ fun z => z ^ y

Tactic:
ext1 x

Result:
case h.e'_5.h
y : ℝ
h : 0 < y
x✝ x : ℝ≥0
⊢ ((fun a => a ^ y) ∘ ofNNReal) x = (ofNNReal ∘ fun z => z ^ y) x

Proof state:
case h.e'_5.h.e'_3
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : x = ⊤
⊢ ⊤ ^ y = ⊤

Tactic:
simp [h]

Result:
no goals

Proof state:
case pos
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : x = ⊤
⊢ ContinuousAt (fun a => a ^ y) x

Tactic:
rw [hx, ContinuousAt]

Result:
case pos
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : x = ⊤
⊢ Tendsto (fun a => a ^ y) (𝓝 ⊤) (𝓝 (⊤ ^ y))

Proof state:
case neg.intro
y : ℝ
h : 0 < y
x : ℝ≥0
⊢ ContinuousAt (fun a => a ^ y) ↑x

Tactic:
rw [continuousAt_coe_iff]

Result:
case neg.intro
y : ℝ
h : 0 < y
x : ℝ≥0
⊢ ContinuousAt ((fun a => a ^ y) ∘ ofNNReal) x

Proof state:
case neg
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : ¬x = ⊤
⊢ ContinuousAt (fun a => a ^ y) x

Tactic:
lift x to ℝ≥0 using hx

Result:
case neg.intro
y : ℝ
h : 0 < y
x : ℝ≥0
⊢ ContinuousAt (fun a => a ^ y) ↑x

Proof state:
case pos
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : x = ⊤
⊢ Tendsto (fun a => a ^ y) (𝓝 ⊤) (𝓝 (⊤ ^ y))

Tactic:
convert ENNReal.tendsto_rpow_at_top h

Result:
case h.e'_5.h.e'_3
x : ℝ≥0∞
y : ℝ
h : 0 < y
hx : x = ⊤
⊢ ⊤ ^ y = ⊤

Proof state:
case h.e'_5.h
y : ℝ
h : 0 < y
x✝ x : ℝ≥0
⊢ ((fun a => a ^ y) ∘ ofNNReal) x = (ofNNReal ∘ fun z => z ^ y) x

Tactic:
simp [← coe_rpow_of_nonneg _ h.le]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Order.lean
theorem order_eq {φ : R⟦X⟧} {n : ℕ∞} :
    order φ = n ↔ (∀ i : ℕ, ↑i = n → coeff R i φ ≠ 0) ∧ ∀ i : ℕ, ↑i < n → coeff R i φ = 0

Proof state:
case top
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ φ.order = ⊤ ↔ (∀ (i : ℕ), ↑i = ⊤ → (coeff R i) φ ≠ 0) ∧ ∀ (i : ℕ), ↑i < ⊤ → (coeff R i) φ = 0

Tactic:
simp [ext_iff]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ∞
⊢ φ.order = n ↔ (∀ (i : ℕ), ↑i = n → (coeff R i) φ ≠ 0) ∧ ∀ (i : ℕ), ↑i < n → (coeff R i) φ = 0

Tactic:
cases n with
| top => simp [ext_iff]
| coe n => simp [order_eq_nat]

Result:
no goals

Proof state:
case coe
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
⊢ φ.order = ↑n ↔ (∀ (i : ℕ), ↑i = ↑n → (coeff R i) φ ≠ 0) ∧ ∀ (i : ℕ), ↑i < ↑n → (coeff R i) φ = 0

Tactic:
simp [order_eq_nat]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Holder.lean
theorem comp {Cg rg : ℝ≥0} {g : Y → Z} {t : Set Y} (hg : HolderOnWith Cg rg g t) {Cf rf : ℝ≥0}
    {f : X → Y} (hf : HolderOnWith Cf rf f s) (hst : MapsTo f s t) :
    HolderOnWith (Cg * Cf ^ (rg : ℝ)) (rg * rf) (g ∘ f) s

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
s : Set X
Cg rg : ℝ≥0
g : Y → Z
t : Set Y
hg : HolderOnWith Cg rg g t
Cf rf : ℝ≥0
f : X → Y
hf : HolderOnWith Cf rf f s
hst : MapsTo f s t
x : X
hx : x ∈ s
y : X
hy : y ∈ s
⊢ edist ((g ∘ f) x) ((g ∘ f) y) ≤ ↑Cg * (↑Cf * edist x y ^ ↑rf) ^ ↑rg

Tactic:
exact hg.edist_le_of_le (hst hx) (hst hy) (hf.edist_le hx hy)

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
s : Set X
Cg rg : ℝ≥0
g : Y → Z
t : Set Y
hg : HolderOnWith Cg rg g t
Cf rf : ℝ≥0
f : X → Y
hf : HolderOnWith Cf rf f s
hst : MapsTo f s t
x : X
hx : x ∈ s
y : X
hy : y ∈ s
⊢ edist ((g ∘ f) x) ((g ∘ f) y) ≤ ↑(Cg * Cf ^ ↑rg) * edist x y ^ ↑(rg * rf)

Tactic:
rw [ENNReal.coe_mul, mul_comm rg, NNReal.coe_mul, ENNReal.rpow_mul, mul_assoc,
  ENNReal.coe_rpow_of_nonneg _ rg.coe_nonneg, ← ENNReal.mul_rpow_of_nonneg _ _ rg.coe_nonneg]

Result:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
s : Set X
Cg rg : ℝ≥0
g : Y → Z
t : Set Y
hg : HolderOnWith Cg rg g t
Cf rf : ℝ≥0
f : X → Y
hf : HolderOnWith Cf rf f s
hst : MapsTo f s t
x : X
hx : x ∈ s
y : X
hy : y ∈ s
⊢ edist ((g ∘ f) x) ((g ∘ f) y) ≤ ↑Cg * (↑Cf * edist x y ^ ↑rf) ^ ↑rg

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
s : Set X
Cg rg : ℝ≥0
g : Y → Z
t : Set Y
hg : HolderOnWith Cg rg g t
Cf rf : ℝ≥0
f : X → Y
hf : HolderOnWith Cf rf f s
hst : MapsTo f s t
⊢ HolderOnWith (Cg * Cf ^ ↑rg) (rg * rf) (g ∘ f) s

Tactic:
intro x hx y hy

Result:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
s : Set X
Cg rg : ℝ≥0
g : Y → Z
t : Set Y
hg : HolderOnWith Cg rg g t
Cf rf : ℝ≥0
f : X → Y
hf : HolderOnWith Cf rf f s
hst : MapsTo f s t
x : X
hx : x ∈ s
y : X
hy : y ∈ s
⊢ edist ((g ∘ f) x) ((g ∘ f) y) ≤ ↑(Cg * Cf ^ ↑rg) * edist x y ^ ↑(rg * rf)
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem mem_sUnion {x y : Class.{u}} : y ∈ ⋃₀ x ↔ ∃ z, z ∈ x ∧ y ∈ z

Proof state:
x y : Class.{u}
⊢ y ∈ ⋃₀ x ↔ ∃ z ∈ x, y ∈ z

Tactic:
constructor

Result:
case mp
x y : Class.{u}
⊢ y ∈ ⋃₀ x → ∃ z ∈ x, y ∈ z

case mpr
x y : Class.{u}
⊢ (∃ z ∈ x, y ∈ z) → y ∈ ⋃₀ x

Proof state:
case mpr
x y : Class.{u}
⊢ (∃ z ∈ x, y ∈ z) → y ∈ ⋃₀ x

Tactic:
rintro ⟨w, hwx, z, rfl, hwz⟩

Result:
case mpr.intro.intro.intro.intro
x w : Class.{u}
hwx : w ∈ x
z : ZFSet.{u}
hwz : w z
⊢ ↑z ∈ ⋃₀ x

Proof state:
case mp.intro.intro.intro.intro
x : Class.{u}
w : ZFSet.{u}
z : Set ZFSet.{u}
hzx : z ∈ x.classToCong
hwz : w ∈ z
⊢ ∃ z ∈ x, ↑w ∈ z

Tactic:
exact ⟨z, hzx, coe_mem.2 hwz⟩

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro
x w : Class.{u}
hwx : w ∈ x
z : ZFSet.{u}
hwz : w z
⊢ ↑z ∈ ⋃₀ x

Tactic:
exact ⟨z, rfl, w, hwx, hwz⟩

Result:
no goals

Proof state:
case mp
x y : Class.{u}
⊢ y ∈ ⋃₀ x → ∃ z ∈ x, y ∈ z

Tactic:
rintro ⟨w, rfl, z, hzx, hwz⟩

Result:
case mp.intro.intro.intro.intro
x : Class.{u}
w : ZFSet.{u}
z : Set ZFSet.{u}
hzx : z ∈ x.classToCong
hwz : w ∈ z
⊢ ∃ z ∈ x, ↑w ∈ z
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem factorization_le_of_le_pow {n p b : ℕ} (hb : n ≤ p ^ b) : n.factorization p ≤ b

Proof state:
n p b : ℕ
hb : n ≤ p ^ b
hn : ¬n = 0
pp : Prime p
⊢ n.factorization p ≤ b

Tactic:
exact (Nat.pow_le_pow_iff_right pp.one_lt).1 ((ordProj_le p hn).trans hb)

Result:
no goals

Proof state:
n p b : ℕ
hb : n ≤ p ^ b
⊢ n.factorization p ≤ b

Tactic:
if hn : n = 0 then simp [hn] else
if pp : p.Prime then
  exact (Nat.pow_le_pow_iff_right pp.one_lt).1 ((ordProj_le p hn).trans hb)
else
  simp [factorization_eq_zero_of_non_prime n pp]

Result:
no goals

Proof state:
n p b : ℕ
hb : n ≤ p ^ b
hn : ¬n = 0
pp : ¬Prime p
⊢ n.factorization p ≤ b

Tactic:
simp [factorization_eq_zero_of_non_prime n pp]

Result:
no goals

Proof state:
n p b : ℕ
hb : n ≤ p ^ b
hn : n = 0
⊢ n.factorization p ≤ b

Tactic:
simp [hn]

Result:
no goals

Proof state:
n p b : ℕ
hb : n ≤ p ^ b
hn : ¬n = 0
⊢ n.factorization p ≤ b

Tactic:
if pp : p.Prime then
  exact (Nat.pow_le_pow_iff_right pp.one_lt).1 ((ordProj_le p hn).trans hb)
else
  simp [factorization_eq_zero_of_non_prime n pp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem abs_intMin {w : Nat} : (intMin w).abs = intMin w

Proof state:
w : Nat
⊢ (intMin w).abs = intMin w

Tactic:
simp [BitVec.abs, bv_toNat]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_mul (M N : Matrix n n R) : det (M * N) = det M * det N :=
  calc
    det (M * N) = ∑ p : n → n, ∑ σ : Perm n, ε σ * ∏ i, M (σ i) (p i) * N (p i) i

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M N : Matrix n n R
σ : Perm n
x✝ : σ ∈ univ
τ : Perm n
⊢ ∏ i : n, M (τ (σ⁻¹ i)) (σ (σ⁻¹ i)) = ∏ j : n, M ((τ * σ⁻¹) j) j

Tactic:
simp only [Equiv.Perm.coe_mul, apply_inv_self, Function.comp_apply]

Result:
no goals

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M N : Matrix n n R
x✝³ : n → n
x✝² : x✝³ ∈ filter (fun p => Bijective p) univ
x✝¹ : n → n
x✝ : x✝¹ ∈ filter (fun p => Bijective p) univ
h : (fun p h => ofBijective p ⋯) x✝³ x✝² = (fun p h => ofBijective p ⋯) x✝¹ x✝
⊢ x✝³ = x✝¹

Tactic:
injection h

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
lemma IsTerminal.isZero {X : C} (hX : IsTerminal X) : IsZero X

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
hX : IsTerminal X
⊢ 𝟙 X = 0

Tactic:
apply hX.hom_ext

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
hX : IsTerminal X
⊢ IsZero X

Tactic:
rw [IsZero.iff_id_eq_zero]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
hX : IsTerminal X
⊢ 𝟙 X = 0