harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Matroid/Closure.lean
@[simp] lemma freeOn_closure_eq (E X : Set α) : (freeOn E).closure X = X ∩ E

Proof state:
α : Type u_2
E X : Set α
⊢ (freeOn E).closure X = X ∩ E

Tactic:
simp (config := {contextual := true}) [← closure_inter_ground _ X, Set.ext_iff, and_comm,
  insert_subset_iff, freeOn_indep_iff, (freeOn_indep inter_subset_right).mem_closure_iff']

Result:
no goals
-- Mathlib/Data/List/MinMax.lean
theorem maximum_cons (a : α) (l : List α) : maximum (a :: l) = max ↑a (maximum l) :=
  List.reverseRecOn l (by simp [@max_eq_left (WithBot α) _ _ _ bot_le]) fun tl hd ih => by
    rw [← cons_append, maximum_concat, ih, maximum_concat, max_assoc]

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a : α
l tl : List α
hd : α
ih : (a :: tl).maximum = ↑a ⊔ tl.maximum
⊢ (a :: (tl ++ [hd])).maximum = ↑a ⊔ (tl ++ [hd]).maximum

Tactic:
rw [← cons_append, maximum_concat, ih, maximum_concat, max_assoc]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a : α
l : List α
⊢ [a].maximum = ↑a ⊔ [].maximum

Tactic:
simp [@max_eq_left (WithBot α) _ _ _ bot_le]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_nnnorm_eq_add (hp : p ≠ ∞) (f : WithLp p (α × β)) :
    ‖f‖₊ = (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ (1 / p.toReal)

Proof state:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
hp : p ≠ ⊤
f : WithLp p (α × β)
⊢ ‖f‖₊ = (‖f.1‖₊ ^ p.toReal + ‖f.2‖₊ ^ p.toReal) ^ (1 / p.toReal)

Tactic:
ext

Result:
case a
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
hp : p ≠ ⊤
f : WithLp p (α × β)
⊢ ↑‖f‖₊ = ↑((‖f.1‖₊ ^ p.toReal + ‖f.2‖₊ ^ p.toReal) ^ (1 / p.toReal))

Proof state:
case a
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
hp : p ≠ ⊤
f : WithLp p (α × β)
⊢ ↑‖f‖₊ = ↑((‖f.1‖₊ ^ p.toReal + ‖f.2‖₊ ^ p.toReal) ^ (1 / p.toReal))

Tactic:
simp [prod_norm_eq_add (p.toReal_pos_iff_ne_top.mpr hp)]

Result:
no goals
-- Mathlib/Algebra/Group/Center.lean
@[to_additive (attr := simp) neg_mem_addCentralizer]
lemma inv_mem_centralizer (ha : a ∈ centralizer S) : a⁻¹ ∈ centralizer S :=
  fun g hg ↦ by rw [mul_inv_eq_iff_eq_mul, mul_assoc, eq_inv_mul_iff_mul_eq, ha g hg]

Proof state:
M : Type u_1
S : Set M
inst✝ : Group M
a : M
ha : a ∈ S.centralizer
g : M
hg : g ∈ S
⊢ g * a⁻¹ = a⁻¹ * g

Tactic:
rw [mul_inv_eq_iff_eq_mul, mul_assoc, eq_inv_mul_iff_mul_eq, ha g hg]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Theta.lean
theorem IsTheta.fiberwise_right :
    f =Θ[l ×ˢ l'] g → ∀ᶠ x in l, (f ⟨x, ·⟩) =Θ[l'] (g ⟨x, ·⟩)

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ f =O[l ×ˢ l'] g ∧ g =O[l ×ˢ l'] f →
    (∀ᶠ (x : α) in l, (fun x_1 => f (x, x_1)) =O[l'] fun x_1 => g (x, x_1)) ∧
      ∀ᶠ (x : α) in l, (fun x_1 => g (x, x_1)) =O[l'] fun x_1 => f (x, x_1)

Tactic:
exact fun ⟨h₁, h₂⟩ ↦ ⟨h₁.fiberwise_right, h₂.fiberwise_right⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ f =Θ[l ×ˢ l'] g → ∀ᶠ (x : α) in l, (fun x_1 => f (x, x_1)) =Θ[l'] fun x_1 => g (x, x_1)

Tactic:
simp only [IsTheta, eventually_and]

Result:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f : α × β → E
g : α × β → F
l' : Filter β
⊢ f =O[l ×ˢ l'] g ∧ g =O[l ×ˢ l'] f →
    (∀ᶠ (x : α) in l, (fun x_1 => f (x, x_1)) =O[l'] fun x_1 => g (x, x_1)) ∧
      ∀ᶠ (x : α) in l, (fun x_1 => g (x, x_1)) =O[l'] fun x_1 => f (x, x_1)
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ici_bot [OrderBot α] [Fintype α] : Ici (⊥ : α) = univ

Proof state:
case h
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : OrderBot α
inst✝ : Fintype α
a : α
⊢ a ∈ Ici ⊥ ↔ a ∈ univ

Tactic:
simp only [mem_Ici, bot_le, mem_univ]

Result:
no goals

Proof state:
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : OrderBot α
inst✝ : Fintype α
⊢ Ici ⊥ = univ

Tactic:
ext a

Result:
case h
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : OrderBot α
inst✝ : Fintype α
a : α
⊢ a ∈ Ici ⊥ ↔ a ∈ univ
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem preimage_setOf_dist (hf : Isometry f) (x : α) (p : ℝ → Prop) :
    f ⁻¹' { y | p (dist y (f x)) } = { y | p (dist y x) }

Proof state:
case h
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
hf : Isometry f
x : α
p : ℝ → Prop
y : α
⊢ y ∈ f ⁻¹' {y | p (dist y (f x))} ↔ y ∈ {y | p (dist y x)}

Tactic:
simp [hf.dist_eq]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
hf : Isometry f
x : α
p : ℝ → Prop
⊢ f ⁻¹' {y | p (dist y (f x))} = {y | p (dist y x)}

Tactic:
ext y

Result:
case h
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
hf : Isometry f
x : α
p : ℝ → Prop
y : α
⊢ y ∈ f ⁻¹' {y | p (dist y (f x))} ↔ y ∈ {y | p (dist y x)}
-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
theorem isField_of_isIntegral_of_isField' [CommRing R] [CommRing S] [IsDomain S]
    [Algebra R S] [Algebra.IsIntegral R S] (hR : IsField R) : IsField S where
  exists_pair_ne := ⟨0, 1, zero_ne_one⟩
  mul_comm := mul_comm
  mul_inv_cancel {x} hx

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
hR : IsField R
this : Field R := hR.toField
y : Sˣ
hx : ↑y ≠ 0
⊢ ∃ b, ↑y * b = 1

Tactic:
exact ⟨y.inv, y.val_inv⟩

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
hR : IsField R
x : S
hx : x ≠ 0
this : Field R := hR.toField
⊢ ∃ b, x * b = 1

Tactic:
obtain ⟨y, rfl⟩ := (Algebra.IsIntegral.isIntegral (R := R) x).isUnit hx

Result:
case intro
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
hR : IsField R
this : Field R := hR.toField
y : Sˣ
hx : ↑y ≠ 0
⊢ ∃ b, ↑y * b = 1

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
hR : IsField R
x : S
hx : x ≠ 0
⊢ ∃ b, x * b = 1

Tactic:
letI := hR.toField

Result:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
hR : IsField R
x : S
hx : x ≠ 0
this : Field R := hR.toField
⊢ ∃ b, x * b = 1
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem Hom.comm {A B : HomologicalComplex V c} (f : A.Hom B) (i j : ι) :
    f.f i ≫ B.d i j = A.d i j ≫ f.f j

Proof state:
case pos
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
A B : HomologicalComplex V c
f : A.Hom B
i j : ι
hij : c.Rel i j
⊢ f.f i ≫ B.d i j = A.d i j ≫ f.f j

Tactic:
exact f.comm' i j hij

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
A B : HomologicalComplex V c
f : A.Hom B
i j : ι
⊢ f.f i ≫ B.d i j = A.d i j ≫ f.f j

Tactic:
by_cases hij : c.Rel i j

Result:
case pos
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
A B : HomologicalComplex V c
f : A.Hom B
i j : ι
hij : c.Rel i j
⊢ f.f i ≫ B.d i j = A.d i j ≫ f.f j

case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
A B : HomologicalComplex V c
f : A.Hom B
i j : ι
hij : ¬c.Rel i j
⊢ f.f i ≫ B.d i j = A.d i j ≫ f.f j

Proof state:
case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
A B : HomologicalComplex V c
f : A.Hom B
i j : ι
hij : ¬c.Rel i j
⊢ f.f i ≫ B.d i j = A.d i j ≫ f.f j

Tactic:
rw [A.shape i j hij, B.shape i j hij, comp_zero, zero_comp]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
/-- `Fintype.prod_bijective` is a variant of `Finset.prod_bij` that accepts `Function.Bijective`.

See `Function.Bijective.prod_comp` for a version without `h`. -/
@[to_additive "`Fintype.sum_bijective` is a variant of `Finset.sum_bij` that accepts
`Function.Bijective`.

See `Function.Bijective.sum_comp` for a version without `h`. "]
lemma prod_bijective (e : ι → κ) (he : e.Bijective) (f : ι → α) (g : κ → α)
    (h : ∀ x, f x = g (e x)) : ∏ x, f x = ∏ x, g x :=
  prod_equiv (.ofBijective e he) (by simp) (by simp [h])

Proof state:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝² : Fintype ι
inst✝¹ : Fintype κ
inst✝ : CommMonoid α
e : ι → κ
he : Bijective e
f : ι → α
g : κ → α
h : ∀ (x : ι), f x = g (e x)
⊢ ∀ i ∈ univ, f i = g ((Equiv.ofBijective e he) i)

Tactic:
simp [h]

Result:
no goals

Proof state:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝² : Fintype ι
inst✝¹ : Fintype κ
inst✝ : CommMonoid α
e : ι → κ
he : Bijective e
f : ι → α
g : κ → α
h : ∀ (x : ι), f x = g (e x)
⊢ ∀ (i : ι), i ∈ univ ↔ (Equiv.ofBijective e he) i ∈ univ

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem degree_monomial {d : σ →₀ ℕ} (c : R) [Decidable (c = 0)] :
    m.degree (monomial d c) = if c = 0 then 0 else d

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
d : σ →₀ ℕ
c : R
inst✝ : Decidable (c = 0)
⊢ m.degree ((monomial d) c) = if c = 0 then 0 else d

Tactic:
simp only [degree, support_monomial]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
d : σ →₀ ℕ
c : R
inst✝ : Decidable (c = 0)
⊢ m.toSyn.symm ((if c = 0 then ∅ else {d}).sup ⇑m.toSyn) = if c = 0 then 0 else d

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
d : σ →₀ ℕ
c : R
inst✝ : Decidable (c = 0)
⊢ m.toSyn.symm ((if c = 0 then ∅ else {d}).sup ⇑m.toSyn) = if c = 0 then 0 else d

Tactic:
split_ifs with hc <;> simp

Result:
no goals
-- Mathlib/Probability/Moments/MGFAnalytic.lean
lemma deriv_mgf_zero (h : 0 ∈ interior (integrableExpSet X μ)) : deriv (mgf X μ) 0 = μ[X]

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
⊢ deriv (mgf X μ) 0 = ∫ (x : Ω), X x ∂μ

Tactic:
simp [deriv_mgf h]

Result:
no goals
-- Mathlib/CategoryTheory/Galois/Decomposition.lean
/-- Any element in the fiber of an object `X` is the evaluation of a morphism from a
Galois object. -/
lemma exists_hom_from_galois_of_fiber (X : C) (x : F.obj X) :
    ∃ (A : C) (f : A ⟶ X) (a : F.obj A), IsGalois A ∧ F.map f a = x

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
x : (F.obj X).carrier
⊢ ∃ A f a, IsGalois A ∧ F.map f a = x

Tactic:
obtain ⟨A, a, h1, h2⟩ := exists_galois_representative F X

Result:
case intro.intro.intro
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
x : (F.obj X).carrier
A : C
a : (F.obj A).carrier
h1 : IsGalois A
h2 : Function.Bijective fun f => F.map f a
⊢ ∃ A f a, IsGalois A ∧ F.map f a = x

Proof state:
case intro.intro.intro
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
x : (F.obj X).carrier
A : C
a : (F.obj A).carrier
h1 : IsGalois A
h2 : Function.Bijective fun f => F.map f a
⊢ ∃ A f a, IsGalois A ∧ F.map f a = x

Tactic:
obtain ⟨f, hf⟩ := h2.surjective x

Result:
case intro.intro.intro.intro
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
x : (F.obj X).carrier
A : C
a : (F.obj A).carrier
h1 : IsGalois A
h2 : Function.Bijective fun f => F.map f a
f : A ⟶ X
hf : (fun f => F.map f a) f = x
⊢ ∃ A f a, IsGalois A ∧ F.map f a = x

Proof state:
case intro.intro.intro.intro
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
x : (F.obj X).carrier
A : C
a : (F.obj A).carrier
h1 : IsGalois A
h2 : Function.Bijective fun f => F.map f a
f : A ⟶ X
hf : (fun f => F.map f a) f = x
⊢ ∃ A f a, IsGalois A ∧ F.map f a = x

Tactic:
exact ⟨A, f, a, h1, hf⟩

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem norm_natCast (n : ℕ) : ‖(n : K)‖ = n

Proof state:
K : Type u_1
inst✝ : RCLike K
n : ℕ
⊢ ‖↑n‖ = ↑n

Tactic:
rw [← ofReal_natCast]

Result:
K : Type u_1
inst✝ : RCLike K
n : ℕ
⊢ ‖↑↑n‖ = ↑n

Proof state:
K : Type u_1
inst✝ : RCLike K
n : ℕ
⊢ ‖↑↑n‖ = ↑n

Tactic:
exact norm_of_nonneg (Nat.cast_nonneg n)

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts/FunctorCategory.lean
@[reassoc (attr := simp)]
lemma tensorHom_app_fst {F₁ F₁' F₂ F₂' : J ⥤ C} (f : F₁ ⟶ F₁') (g : F₂ ⟶ F₂') (j : J) :
    (f ⊗ g).app j ≫ fst _ _ = fst _ _ ≫ f.app j

Proof state:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₁' F₂ F₂' : J ⥤ C
f : F₁ ⟶ F₁'
g : F₂ ⟶ F₂'
j : J
⊢ (f ⊗ g).app j ≫ fst (F₁'.obj j) (F₂'.obj j) = fst (F₁.obj j) (F₂.obj j) ≫ f.app j

Tactic:
change (f ⊗ g).app j ≫ (fst F₁' F₂').app j = _

Result:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₁' F₂ F₂' : J ⥤ C
f : F₁ ⟶ F₁'
g : F₂ ⟶ F₂'
j : J
⊢ (f ⊗ g).app j ≫ (fst F₁' F₂').app j = fst (F₁.obj j) (F₂.obj j) ≫ f.app j

Proof state:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₁' F₂ F₂' : J ⥤ C
f : F₁ ⟶ F₁'
g : F₂ ⟶ F₂'
j : J
⊢ (f ⊗ g).app j ≫ (fst F₁' F₂').app j = fst (F₁.obj j) (F₂.obj j) ≫ f.app j

Tactic:
rw [← NatTrans.comp_app, tensorHom_fst, NatTrans.comp_app]

Result:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₁' F₂ F₂' : J ⥤ C
f : F₁ ⟶ F₁'
g : F₂ ⟶ F₂'
j : J
⊢ (fst F₁ F₂).app j ≫ f.app j = fst (F₁.obj j) (F₂.obj j) ≫ f.app j

Proof state:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₁' F₂ F₂' : J ⥤ C
f : F₁ ⟶ F₁'
g : F₂ ⟶ F₂'
j : J
⊢ (fst F₁ F₂).app j ≫ f.app j = fst (F₁.obj j) (F₂.obj j) ≫ f.app j

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_le_coe_iff_finite_ncard_le {k : ℕ} : s.encard ≤ k ↔ s.Finite ∧ s.ncard ≤ k

Proof state:
α : Type u_1
s : Set α
k : ℕ
hfin : s.Finite
h : s.ncard ≤ k
⊢ s.encard = ↑s.ncard

Tactic:
rw [hfin.cast_ncard_eq]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
k : ℕ
⊢ s.encard ≤ ↑k ↔ s.Finite ∧ s.ncard ≤ k

Tactic:
rw [encard_le_coe_iff, and_congr_right_iff]

Result:
α : Type u_1
s : Set α
k : ℕ
⊢ s.Finite → ((∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k) ↔ s.ncard ≤ k)

Proof state:
α : Type u_1
s : Set α
k : ℕ
hfin : s.Finite
x✝ : ∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k
n₀ : ℕ
hn₀ : s.encard = ↑n₀
hle : n₀ ≤ k
⊢ s.ncard ≤ k

Tactic:
rwa [ncard_def, hn₀, ENat.toNat_coe]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
k : ℕ
⊢ s.Finite → ((∃ n₀, s.encard = ↑n₀ ∧ n₀ ≤ k) ↔ s.ncard ≤ k)

Tactic:
exact fun hfin ↦ ⟨fun ⟨n₀, hn₀, hle⟩ ↦ by rwa [ncard_def, hn₀, ENat.toNat_coe],
  fun h ↦ ⟨s.ncard, by rw [hfin.cast_ncard_eq], h⟩⟩

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
lemma eLpNormEssSup_indicator_const_le (s : Set α) (c : G) :
    eLpNormEssSup (s.indicator fun _ : α => c) μ ≤ ‖c‖ₑ

Proof state:
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
⊢ eLpNormEssSup (s.indicator fun x => c) μ ≤ ‖c‖ₑ

Tactic:
by_cases hμ0 : μ = 0

Result:
case pos
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
hμ0 : μ = 0
⊢ eLpNormEssSup (s.indicator fun x => c) μ ≤ ‖c‖ₑ

case neg
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
hμ0 : ¬μ = 0
⊢ eLpNormEssSup (s.indicator fun x => c) μ ≤ ‖c‖ₑ

Proof state:
case pos
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
hμ0 : μ = 0
⊢ eLpNormEssSup (s.indicator fun x => c) μ ≤ ‖c‖ₑ

Tactic:
rw [hμ0, eLpNormEssSup_measure_zero]

Result:
case pos
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
hμ0 : μ = 0
⊢ 0 ≤ ‖c‖ₑ

Proof state:
case neg
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
hμ0 : ¬μ = 0
⊢ eLpNormEssSup (s.indicator fun x => c) μ ≤ ‖c‖ₑ

Tactic:
exact (eLpNormEssSup_indicator_le s fun _ => c).trans (eLpNormEssSup_const c hμ0).le

Result:
no goals

Proof state:
case pos
α : Type u_1
G : Type u_5
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup G
s : Set α
c : G
hμ0 : μ = 0
⊢ 0 ≤ ‖c‖ₑ

Tactic:
exact zero_le _

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem comap_bot_le_of_injective (hf : Function.Injective f) : comap f ⊥ ≤ I

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
I : Ideal R
inst✝ : RingHomClass F R S
hf : Function.Injective ⇑f
x : R
hx : x ∈ comap f ⊥
⊢ x ∈ ⊥

Tactic:
rw [mem_comap, Submodule.mem_bot, ← map_zero f] at hx

Result:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
I : Ideal R
inst✝ : RingHomClass F R S
hf : Function.Injective ⇑f
x : R
hx : f x = f 0
⊢ x ∈ ⊥

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
I : Ideal R
inst✝ : RingHomClass F R S
hf : Function.Injective ⇑f
⊢ comap f ⊥ ≤ I

Tactic:
refine le_trans (fun x hx => ?_) bot_le

Result:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
I : Ideal R
inst✝ : RingHomClass F R S
hf : Function.Injective ⇑f
x : R
hx : x ∈ comap f ⊥
⊢ x ∈ ⊥

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
I : Ideal R
inst✝ : RingHomClass F R S
hf : Function.Injective ⇑f
x : R
hx : f x = f 0
⊢ x ∈ ⊥

Tactic:
exact Eq.symm (hf hx) ▸ Submodule.zero_mem ⊥

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
theorem norm_iteratedFDeriv_mul_le {f : E → A} {g : E → A} {N : WithTop ℕ∞} (hf : ContDiff 𝕜 N f)
    (hg : ContDiff 𝕜 N g) (x : E) {n : ℕ} (hn : n ≤ N) :
    ‖iteratedFDeriv 𝕜 n (fun y => f y * g y) x‖ ≤ ∑ i ∈ Finset.range (n + 1),
      (n.choose i : ℝ) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_3
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
f g : E → A
N : WithTop ℕ∞
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : E
n : ℕ
hn : ↑n ≤ N
⊢ ‖iteratedFDerivWithin 𝕜 n (fun y => f y * g y) univ x‖ ≤
    ∑ x_1 ∈ Finset.range (n + 1),
      ↑(n.choose x_1) * ‖iteratedFDerivWithin 𝕜 x_1 f univ x‖ * ‖iteratedFDerivWithin 𝕜 (n - x_1) g univ x‖

Tactic:
exact norm_iteratedFDerivWithin_mul_le
  hf.contDiffOn hg.contDiffOn uniqueDiffOn_univ (mem_univ x) hn

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_3
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
f g : E → A
N : WithTop ℕ∞
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : E
n : ℕ
hn : ↑n ≤ N
⊢ ‖iteratedFDeriv 𝕜 n (fun y => f y * g y) x‖ ≤
    ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDeriv 𝕜 i f x‖ * ‖iteratedFDeriv 𝕜 (n - i) g x‖

Tactic:
simp_rw [← iteratedFDerivWithin_univ]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_3
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
f g : E → A
N : WithTop ℕ∞
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : E
n : ℕ
hn : ↑n ≤ N
⊢ ‖iteratedFDerivWithin 𝕜 n (fun y => f y * g y) univ x‖ ≤
    ∑ x_1 ∈ Finset.range (n + 1),
      ↑(n.choose x_1) * ‖iteratedFDerivWithin 𝕜 x_1 f univ x‖ * ‖iteratedFDerivWithin 𝕜 (n - x_1) g univ x‖
-- Mathlib/SetTheory/Cardinal/Finite.lean
lemma card_pos_iff : 0 < Nat.card α ↔ Nonempty α ∧ Finite α

Proof state:
α : Type u_1
⊢ 0 < Nat.card α ↔ Nonempty α ∧ Finite α

Tactic:
simp [Nat.card, mk_eq_zero_iff, mk_lt_aleph0_iff]

Result:
no goals
-- Mathlib/Computability/Ackermann.lean
theorem not_primrec_ack_self : ¬Primrec fun n => ack n n

Proof state:
⊢ ¬Nat.Primrec fun n => ack n n

Tactic:
exact not_nat_primrec_ack_self

Result:
no goals

Proof state:
⊢ ¬Primrec fun n => ack n n

Tactic:
rw [Primrec.nat_iff]

Result:
⊢ ¬Nat.Primrec fun n => ack n n
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem toNatOrdinal_cast_nat (n : ℕ) : toNatOrdinal n = n

Proof state:
n : ℕ
⊢ toNatOrdinal ↑n = ↑n

Tactic:
rw [← toOrdinal_cast_nat n]

Result:
n : ℕ
⊢ toNatOrdinal (toOrdinal ↑n) = ↑n

Proof state:
n : ℕ
⊢ toNatOrdinal (toOrdinal ↑n) = ↑n

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem natDegree_comp_le : natDegree (p.comp q) ≤ natDegree p * natDegree q :=
  letI := Classical.decEq R
  if h0 : p.comp q = 0 then by rw [h0, natDegree_zero]; exact Nat.zero_le _
  else
    WithBot.coe_le_coe.1 <|
      calc
        ↑(natDegree (p.comp q)) = degree (p.comp q) := (degree_eq_natDegree h0).symm
        _ = _ := congr_arg degree comp_eq_sum_left
        _ ≤ _ := degree_sum_le _ _
        _ ≤ _ :=
          Finset.sup_le fun n hn =>
            calc
              degree (C (coeff p n) * q ^ n) ≤ degree (C (coeff p n)) + degree (q ^ n) :=
                degree_mul_le _ _
              _ ≤ natDegree (C (coeff p n)) + n • degree q :=
                (add_le_add degree_le_natDegree (degree_pow_le _ _))
              _ ≤ natDegree (C (coeff p n)) + n • ↑(natDegree q) :=
                (add_le_add_left (nsmul_le_nsmul_right (@degree_le_natDegree _ _ q) n) _)
              _ = (n * natDegree q : ℕ)

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : ¬p.comp q = 0
n : ℕ
hn : n ∈ p.support
⊢ ↑n * ↑q.natDegree = ↑(n * q.natDegree)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : p.comp q = 0
⊢ 0 ≤ p.natDegree * q.natDegree

Tactic:
exact Nat.zero_le _

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : p.comp q = 0
⊢ (p.comp q).natDegree ≤ p.natDegree * q.natDegree

Tactic:
rw [h0, natDegree_zero]

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : p.comp q = 0
⊢ 0 ≤ p.natDegree * q.natDegree

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : ¬p.comp q = 0
n : ℕ
hn : n ∈ p.support
⊢ ↑(C (p.coeff n)).natDegree + n • ↑q.natDegree = ↑(n * q.natDegree)

Tactic:
rw [natDegree_C, Nat.cast_zero, zero_add, nsmul_eq_mul]

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
h0 : ¬p.comp q = 0
n : ℕ
hn : n ∈ p.support
⊢ ↑n * ↑q.natDegree = ↑(n * q.natDegree)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem foldr_pmap (l : List α) {P : α → Prop} (f : (a : α) → P a → β)
  (H : ∀ (a : α), a ∈ l → P a) (g : β → γ → γ) (x : γ) :
    (l.pmap f H).foldr g x = l.attach.foldr (fun a acc => g (f a.1 (H _ a.2)) acc) x

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
P : α → Prop
f : (a : α) → P a → β
H : ∀ (a : α), a ∈ l → P a
g : β → γ → γ
x : γ
⊢ foldr g x (pmap f l H) = foldr (fun a acc => g (f a.val ⋯) acc) x l.attach

Tactic:
rw [pmap_eq_map_attach, foldr_map]

Result:
no goals