harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/CharP/Defs.lean
lemma expChar_ne_zero (p : ℕ) [hR : ExpChar R p] : p ≠ 0

Proof state:
R : Type u_1
inst✝ : AddMonoidWithOne R
p : ℕ
hR : ExpChar R p
⊢ p ≠ 0

Tactic:
cases hR

Result:
case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
⊢ 1 ≠ 0

case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
p : ℕ
hprime✝ : Nat.Prime p
hchar✝ : CharP R p
⊢ p ≠ 0

Proof state:
case prime
R : Type u_1
inst✝ : AddMonoidWithOne R
p : ℕ
hprime✝ : Nat.Prime p
hchar✝ : CharP R p
⊢ p ≠ 0

Tactic:
exact ‹p.Prime›.ne_zero

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝¹ : AddMonoidWithOne R
inst✝ : CharZero R
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.lean
theorem blastShiftRightConst.go_le_size (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w)
    (curr : Nat) (hcurr : curr ≤ w) (s : AIG.RefVec aig curr) :
    aig.decls.size ≤ (go aig input distance curr hcurr s).aig.decls.size

Proof state:
case isTrue.isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
h✝¹ : curr < w
h✝ : distance + curr < w
⊢ aig.decls.size ≤ (go aig input distance (curr + 1) ⋯ (s.push (input.get (distance + curr) ⋯))).aig.decls.size

Tactic:
refine Nat.le_trans ?_ (by apply go_le_size)

Result:
case isTrue.isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
h✝¹ : curr < w
h✝ : distance + curr < w
⊢ aig.decls.size ≤ aig.decls.size

Proof state:
case isTrue.isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
h✝¹ : curr < w
h✝ : ¬distance + curr < w
⊢ aig.decls.size ≤
    (go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
            ((s.cast ⋯).push (aig.mkConstCached false).ref)).aig.decls.size

Tactic:
refine Nat.le_trans ?_ (by apply go_le_size)

Result:
case isTrue.isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefVec curr
h✝¹ : curr < w
h✝ : ¬distance + curr < w
⊢ aig.decls.size ≤ (aig.mkConstCached false).aig.decls.size
-- Mathlib/SetTheory/Game/PGame.lean
theorem star_lf_zero : star ⧏ 0

Proof state:
⊢ ∃ j, ∀ (i : (star.moveRight j).LeftMoves), (star.moveRight j).moveLeft i ⧏ 0

Tactic:
use default

Result:
case h

⊢ ∀ (i : (star.moveRight default).LeftMoves), (star.moveRight default).moveLeft i ⧏ 0

Proof state:
⊢ star ⧏ 0

Tactic:
rw [lf_zero]

Result:
⊢ ∃ j, ∀ (i : (star.moveRight j).LeftMoves), (star.moveRight j).moveLeft i ⧏ 0

Proof state:
case h

⊢ ∀ (i : (star.moveRight default).LeftMoves), (star.moveRight default).moveLeft i ⧏ 0

Tactic:
rintro ⟨⟩

Result:
no goals
-- Mathlib/Topology/Algebra/Module/StrongTopology.lean
theorem isVonNBounded_iff {R : Type*} [NormedDivisionRing R]
    [TopologicalSpace F] [IsTopologicalAddGroup F]
    [Module R F] [ContinuousConstSMul R F] [SMulCommClass 𝕜₂ R F]
    {𝔖 : Set (Set E)} {S : Set (UniformConvergenceCLM σ F 𝔖)} :
    IsVonNBounded R S ↔ ∀ s ∈ 𝔖, IsVonNBounded R (Set.image2 (fun f x ↦ f x) S s)

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NormedField 𝕜₁
inst✝¹¹ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜₁ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
R : Type u_5
inst✝⁵ : NormedDivisionRing R
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : Module R F
inst✝¹ : ContinuousConstSMul R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (UniformConvergenceCLM σ F 𝔖)
h : ∀ s ∈ 𝔖, IsVonNBounded R (image2 (fun f x => f x) S s)
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : U ∈ 𝓝 0
⊢ ∀ᶠ (a : R) in cobounded R, S ⊆ a • {f | MapsTo (⇑f) s U}

Tactic:
filter_upwards [h s hs hU, eventually_ne_cobounded 0] with c hc hc₀ f hf

Result:
case h
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NormedField 𝕜₁
inst✝¹¹ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜₁ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
R : Type u_5
inst✝⁵ : NormedDivisionRing R
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : Module R F
inst✝¹ : ContinuousConstSMul R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (UniformConvergenceCLM σ F 𝔖)
h : ∀ s ∈ 𝔖, IsVonNBounded R (image2 (fun f x => f x) S s)
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : U ∈ 𝓝 0
c : R
hc : image2 (fun f x => f x) S s ⊆ c • U
hc₀ : c ≠ 0
f : UniformConvergenceCLM σ F 𝔖
hf : f ∈ S
⊢ f ∈ c • {f | MapsTo (⇑f) s U}

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NormedField 𝕜₁
inst✝¹¹ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜₁ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
R : Type u_5
inst✝⁵ : NormedDivisionRing R
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : Module R F
inst✝¹ : ContinuousConstSMul R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (UniformConvergenceCLM σ F 𝔖)
h : ∀ s ∈ 𝔖, IsVonNBounded R (image2 (fun f x => f x) S s)
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : U ∈ 𝓝 0
⊢ {f | MapsTo (⇑f) s U} ∈ absorbing R S

Tactic:
rw [Filter.mem_absorbing, Absorbs]

Result:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝¹² : NormedField 𝕜₁
inst✝¹¹ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜₁ E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜₂ F
R : Type u_5
inst✝⁵ : NormedDivisionRing R
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup F
inst✝² : Module R F
inst✝¹ : ContinuousConstSMul R F
inst✝ : SMulCommClass 𝕜₂ R F
𝔖 : Set (Set E)
S : Set (UniformConvergenceCLM σ F 𝔖)
h : ∀ s ∈ 𝔖, IsVonNBounded R (image2 (fun f x => f x) S s)
s : Set E
hs : s ∈ 𝔖
U : Set F
hU : U ∈ 𝓝 0
⊢ ∀ᶠ (a : R) in cobounded R, S ⊆ a • {f | MapsTo (⇑f) s U}
-- Mathlib/RingTheory/Ideal/GoingDown.lean
/-- An `R`-algebra `S` has the going down property if and only if generalizations lift
along `Spec S → Spec R`. -/
@[stacks 00HW "(1)"]
lemma iff_generalizingMap_primeSpectrumComap :
    Algebra.HasGoingDown R S ↔
      GeneralizingMap (PrimeSpectrum.comap (algebraMap R S))

Proof state:
case refine_1
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : HasGoingDown R S
Q : PrimeSpectrum S
p : PrimeSpectrum R
hp : p ⤳ (PrimeSpectrum.comap (algebraMap R S)) Q
⊢ ∃ a', (fun x1 x2 => x1 ⤳ x2) a' Q ∧ (PrimeSpectrum.comap (algebraMap R S)) a' = p

Tactic:
rw [← PrimeSpectrum.le_iff_specializes] at hp

Result:
case refine_1
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : HasGoingDown R S
Q : PrimeSpectrum S
p : PrimeSpectrum R
hp : p ≤ (PrimeSpectrum.comap (algebraMap R S)) Q
⊢ ∃ a', (fun x1 x2 => x1 ⤳ x2) a' Q ∧ (PrimeSpectrum.comap (algebraMap R S)) a' = p

Proof state:
case refine_2.intro.intro
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : GeneralizingMap ⇑(PrimeSpectrum.comap (algebraMap R S))
p : Ideal R
hp : p.IsPrime
Q : Ideal S
hQ : Q.IsPrime
hlt : p < Ideal.under R Q
this : { asIdeal := p, isPrime := hp } ⤳ (PrimeSpectrum.comap (algebraMap R S)) { asIdeal := Q, isPrime := hQ }
P : PrimeSpectrum S
hs : P ⤳ { asIdeal := Q, isPrime := hQ }
heq : (PrimeSpectrum.comap (algebraMap R S)) P = { asIdeal := p, isPrime := hp }
⊢ p = Ideal.under R P.asIdeal

Tactic:
simpa [PrimeSpectrum.ext_iff] using heq.symm

Result:
no goals
-- Mathlib/CategoryTheory/Closed/Enrichment.lean
lemma enrichedOrdinaryCategorySelf_eHomWhiskerRight {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) :
    eHomWhiskerRight C f Y = (pre f).app Y

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
X₁ X₂ : C
f : X₁ ⟶ X₂
Y : C
⊢ (λ_ ((ihom X₂).obj Y)).inv ≫ curry' f ▷ (ihom X₂).obj Y ≫ comp X₁ X₂ Y = (pre f).app Y

Tactic:
rw [curry'_whiskerRight_comp, Iso.inv_hom_id_assoc]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
X₁ X₂ : C
f : X₁ ⟶ X₂
Y : C
⊢ eHomWhiskerRight C f Y = (pre f).app Y

Tactic:
change (λ_ _).inv ≫ curry' f ▷ _ ≫ comp X₁ X₂ Y = _

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
X₁ X₂ : C
f : X₁ ⟶ X₂
Y : C
⊢ (λ_ ((ihom X₂).obj Y)).inv ≫ curry' f ▷ (ihom X₂).obj Y ≫ comp X₁ X₂ Y = (pre f).app Y
-- Mathlib/Order/UpperLower/Basic.lean
lemma sdiff_inf_upperClosure (hts : t ⊆ s) (hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t) :
    s.sdiff t ⊓ upperClosure t = s

Proof state:
case inl
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : a ∈ (⇑toDual ∘ SetLike.coe) s
hat : a ∈ t
⊢ a ∈ (⇑toDual ∘ SetLike.coe) (s.sdiff t ⊓ upperClosure t)

Tactic:
exact subset_union_right (subset_upperClosure hat)

Result:
no goals

Proof state:
case inr.intro.intro
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : a ∈ (⇑toDual ∘ SetLike.coe) s
hat : a ∉ t
b : α
hb : b ∈ t
hab : a ≤ b
⊢ False

Tactic:
exact hat <| hst _ ha _ hb hab

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : a ∈ (⇑toDual ∘ SetLike.coe) s
hat : a ∉ t
⊢ a ∈ (⇑toDual ∘ SetLike.coe) (s.sdiff t ⊓ upperClosure t)

Tactic:
refine subset_union_left ⟨ha, ?_⟩

Result:
case inr
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : a ∈ (⇑toDual ∘ SetLike.coe) s
hat : a ∉ t
⊢ a ∉ ↑(lowerClosure t)

Proof state:
case inr
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : a ∈ (⇑toDual ∘ SetLike.coe) s
hat : a ∉ t
⊢ a ∉ ↑(lowerClosure t)

Tactic:
rintro ⟨b, hb, hab⟩

Result:
case inr.intro.intro
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : a ∈ (⇑toDual ∘ SetLike.coe) s
hat : a ∉ t
b : α
hb : b ∈ t
hab : a ≤ b
⊢ False

Proof state:
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : a ∈ (⇑toDual ∘ SetLike.coe) s
⊢ a ∈ (⇑toDual ∘ SetLike.coe) (s.sdiff t ⊓ upperClosure t)

Tactic:
obtain hat | hat := em (a ∈ t)

Result:
case inl
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : a ∈ (⇑toDual ∘ SetLike.coe) s
hat : a ∈ t
⊢ a ∈ (⇑toDual ∘ SetLike.coe) (s.sdiff t ⊓ upperClosure t)

case inr
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : a ∈ (⇑toDual ∘ SetLike.coe) s
hat : a ∉ t
⊢ a ∈ (⇑toDual ∘ SetLike.coe) (s.sdiff t ⊓ upperClosure t)

Proof state:
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
⊢ s.sdiff t ⊓ upperClosure t = s

Tactic:
refine ge_antisymm (le_inf le_sdiff_left <| le_upperClosure.2 hts) fun a ha ↦ ?_

Result:
α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
hts : t ⊆ ↑s
hst : ∀ b ∈ s, ∀ c ∈ t, b ≤ c → b ∈ t
a : α
ha : a ∈ (⇑toDual ∘ SetLike.coe) s
⊢ a ∈ (⇑toDual ∘ SetLike.coe) (s.sdiff t ⊓ upperClosure t)
-- Mathlib/SetTheory/Game/Birthday.lean
theorem Relabelling.birthday_congr : ∀ {x y : PGame.{u}}, x ≡r y → birthday x = birthday y
  | ⟨xl, xr, xL, xR⟩, ⟨yl, yr, yL, yR⟩, r => by
    unfold birthday
    congr 1
    all_goals
      apply lsub_eq_of_range_eq.{u, u, u}
      ext i; constructor
    all_goals rintro ⟨j, rfl⟩
    · exact ⟨_, (r.moveLeft j).birthday_congr.symm⟩
    · exact ⟨_, (r.moveLeftSymm j).birthday_congr⟩
    · exact ⟨_, (r.moveRight j).birthday_congr.symm⟩
    · exact ⟨_, (r.moveRightSymm j).birthday_congr⟩

Proof state:
case e_a.h.mp.intro
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
j : xr
⊢ (fun i => (xR i).birthday) j ∈ Set.range fun i => (yR i).birthday

Tactic:
exact ⟨_, (r.moveRight j).birthday_congr.symm⟩

Result:
no goals

Proof state:
case e_a.h.mp.intro
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
j : xl
⊢ (fun i => (xL i).birthday) j ∈ Set.range fun i => (yL i).birthday

Tactic:
exact ⟨_, (r.moveLeft j).birthday_congr.symm⟩

Result:
no goals

Proof state:
case e_a
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
⊢ (Set.range fun i => (xR i).birthday) = Set.range fun i => (yR i).birthday

Tactic:
ext i

Result:
case e_a.h
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
r : PGame.mk xl xr xL xR ≡r PGame.mk yl yr yL yR
i : Ordinal.{u}
⊢ (i ∈ Set.range fun i => (xR i).birthday) ↔ i ∈ Set.range fun i => (yR i).birthday
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem measure_le_setAverage_pos (hμ : μ s ≠ 0) (hμ₁ : μ s ≠ ∞) (hf : IntegrableOn f s μ) :
    0 < μ ({x ∈ s | f x ≤ ⨍ a in s, f a ∂μ})

Proof state:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : IntegrableOn f s μ
H : (μ.restrict s) {x | f x ≤ ⨍ (a : α) in s, f a ∂μ} = 0
this : Fact (μ s < ⊤)
⊢ IntegrableOn (fun x => f x - ⨍ (a : α) in s, f a ∂μ) s μ

Tactic:
exact hf.sub (integrableOn_const.2 <| Or.inr <| lt_top_iff_ne_top.2 hμ₁)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean
lemma cosh_le_exp_half_sq (x : ℝ) : cosh x ≤ exp (x ^ 2 / 2)

Proof state:
x : ℝ
i : ℕ
⊢ (x ^ 2) ^ i / ↑(2 * i)! ≤ (x ^ 2) ^ i / (2 ^ i * ↑i !)

Tactic:
gcongr

Result:
case h
x : ℝ
i : ℕ
⊢ 2 ^ i * ↑i ! ≤ ↑(2 * i)!

Proof state:
case h
x : ℝ
i : ℕ
⊢ 2 ^ i * ↑i ! ≤ ↑(2 * i)!

Tactic:
norm_cast

Result:
case h
x : ℝ
i : ℕ
⊢ 2 ^ i * i ! ≤ (2 * i)!

Proof state:
x : ℝ
⊢ cosh x ≤ rexp (x ^ 2 / 2)

Tactic:
rw [cosh_eq_tsum, exp_eq_exp_ℝ, exp_eq_tsum]

Result:
x : ℝ
⊢ ∑' (n : ℕ), x ^ (2 * n) / ↑(2 * n)! ≤ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) (x ^ 2 / 2)

Proof state:
x : ℝ
⊢ ∑' (n : ℕ), x ^ (2 * n) / ↑(2 * n)! ≤ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) (x ^ 2 / 2)

Tactic:
refine tsum_le_tsum (fun i ↦ ?_) x.hasSum_cosh.summable <| expSeries_summable' (x ^ 2 / 2)

Result:
x : ℝ
i : ℕ
⊢ x ^ (2 * i) / ↑(2 * i)! ≤ (↑i !)⁻¹ • (x ^ 2 / 2) ^ i

Proof state:
x : ℝ
i : ℕ
⊢ x ^ (2 * i) / ↑(2 * i)! ≤ (↑i !)⁻¹ • (x ^ 2 / 2) ^ i

Tactic:
simp only [div_pow, pow_mul, smul_eq_mul, inv_mul_eq_div, div_div]

Result:
x : ℝ
i : ℕ
⊢ (x ^ 2) ^ i / ↑(2 * i)! ≤ (x ^ 2) ^ i / (2 ^ i * ↑i !)

Proof state:
case h
x : ℝ
i : ℕ
⊢ 2 ^ i * i ! ≤ (2 * i)!

Tactic:
exact Nat.two_pow_mul_factorial_le_factorial_two_mul _

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem orderTop_eq_top_iff {x : HahnSeries Γ R} : orderTop x = ⊤ ↔ x = 0

Proof state:
case mp
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
⊢ x.orderTop = ⊤ → x = 0

Tactic:
contrapose!

Result:
case mp
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
⊢ x ≠ 0 → x.orderTop ≠ ⊤

Proof state:
case mpr
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
⊢ x = 0 → x.orderTop = ⊤

Tactic:
simp_all only [orderTop_zero, implies_true]

Result:
no goals

Proof state:
case mp
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
⊢ x ≠ 0 → x.orderTop ≠ ⊤

Tactic:
exact ne_zero_iff_orderTop.mp

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
⊢ x.orderTop = ⊤ ↔ x = 0

Tactic:
constructor

Result:
case mp
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
⊢ x.orderTop = ⊤ → x = 0

case mpr
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
⊢ x = 0 → x.orderTop = ⊤
-- Mathlib/Topology/Compactness/SigmaCompact.lean
theorem mem_find (x : X) : x ∈ K (K.find x)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
x : X
⊢ x ∈ K (K.find x)

Tactic:
classical
exact Nat.find_spec (K.exists_mem x)

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
x : X
⊢ x ∈ K (K.find x)

Tactic:
exact Nat.find_spec (K.exists_mem x)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem lex_acc_inr (aca : ∀ a, Acc (Lex r s) (inl a)) {b} (acb : Acc s b) :
    Acc (Lex r s) (inr b)

Proof state:
case intro.h.sep
α✝ : Type u_1
r : α✝ → α✝ → Prop
β✝ : Type u_2
s : β✝ → β✝ → Prop
aca : ∀ (a : α✝), Acc (Lex r s) (inl a)
b x✝ : β✝
h✝ : ∀ (y : β✝), s y x✝ → Acc s y
IH : ∀ (y : β✝), s y x✝ → Acc (Lex r s) (inr y)
a✝ : α✝
⊢ Acc (Lex r s) (inl a✝)

Tactic:
exact aca _

Result:
no goals

Proof state:
case intro.h
α✝ : Type u_1
r : α✝ → α✝ → Prop
β✝ : Type u_2
s : β✝ → β✝ → Prop
aca : ∀ (a : α✝), Acc (Lex r s) (inl a)
b x✝ : β✝
h✝ : ∀ (y : β✝), s y x✝ → Acc s y
IH : ∀ (y : β✝), s y x✝ → Acc (Lex r s) (inr y)
y : α✝ ⊕ β✝
h : Lex r s y (inr x✝)
⊢ Acc (Lex r s) y

Tactic:
cases h with
| inr h' => exact IH _ h'
| sep => exact aca _

Result:
no goals

Proof state:
case intro.h.inr
α✝ : Type u_1
r : α✝ → α✝ → Prop
β✝ : Type u_2
s : β✝ → β✝ → Prop
aca : ∀ (a : α✝), Acc (Lex r s) (inl a)
b x✝ : β✝
h✝ : ∀ (y : β✝), s y x✝ → Acc s y
IH : ∀ (y : β✝), s y x✝ → Acc (Lex r s) (inr y)
b₁✝ : β✝
h' : s b₁✝ x✝
⊢ Acc (Lex r s) (inr b₁✝)

Tactic:
exact IH _ h'

Result:
no goals

Proof state:
case intro
α✝ : Type u_1
r : α✝ → α✝ → Prop
β✝ : Type u_2
s : β✝ → β✝ → Prop
aca : ∀ (a : α✝), Acc (Lex r s) (inl a)
b x✝ : β✝
h✝ : ∀ (y : β✝), s y x✝ → Acc s y
IH : ∀ (y : β✝), s y x✝ → Acc (Lex r s) (inr y)
⊢ Acc (Lex r s) (inr x✝)

Tactic:
constructor

Result:
case intro.h
α✝ : Type u_1
r : α✝ → α✝ → Prop
β✝ : Type u_2
s : β✝ → β✝ → Prop
aca : ∀ (a : α✝), Acc (Lex r s) (inl a)
b x✝ : β✝
h✝ : ∀ (y : β✝), s y x✝ → Acc s y
IH : ∀ (y : β✝), s y x✝ → Acc (Lex r s) (inr y)
⊢ ∀ (y : α✝ ⊕ β✝), Lex r s y (inr x✝) → Acc (Lex r s) y

Proof state:
case intro.h
α✝ : Type u_1
r : α✝ → α✝ → Prop
β✝ : Type u_2
s : β✝ → β✝ → Prop
aca : ∀ (a : α✝), Acc (Lex r s) (inl a)
b x✝ : β✝
h✝ : ∀ (y : β✝), s y x✝ → Acc s y
IH : ∀ (y : β✝), s y x✝ → Acc (Lex r s) (inr y)
⊢ ∀ (y : α✝ ⊕ β✝), Lex r s y (inr x✝) → Acc (Lex r s) y

Tactic:
intro y h

Result:
case intro.h
α✝ : Type u_1
r : α✝ → α✝ → Prop
β✝ : Type u_2
s : β✝ → β✝ → Prop
aca : ∀ (a : α✝), Acc (Lex r s) (inl a)
b x✝ : β✝
h✝ : ∀ (y : β✝), s y x✝ → Acc s y
IH : ∀ (y : β✝), s y x✝ → Acc (Lex r s) (inr y)
y : α✝ ⊕ β✝
h : Lex r s y (inr x✝)
⊢ Acc (Lex r s) y

Proof state:
α✝ : Type u_1
r : α✝ → α✝ → Prop
β✝ : Type u_2
s : β✝ → β✝ → Prop
aca : ∀ (a : α✝), Acc (Lex r s) (inl a)
b : β✝
acb : Acc s b
⊢ Acc (Lex r s) (inr b)

Tactic:
induction acb with
| intro _ _ IH =>
  constructor
  intro y h
  cases h with
  | inr h' => exact IH _ h'
  | sep => exact aca _

Result:
no goals
-- Mathlib/CategoryTheory/Limits/FunctorToTypes.lean
theorem jointly_surjective (k : K) {t : Cocone F} (h : IsColimit t) (x : t.pt.obj k)
    [∀ k, HasColimit (F.flip.obj k)] : ∃ j y, x = (t.ι.app j).app k y

Proof state:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ Type w
k : K
t : Cocone F
h : IsColimit t
x : t.pt.obj k
inst✝ : ∀ (k : K), HasColimit (F.flip.obj k)
⊢ ∃ j y, x = (t.ι.app j).app k y

Tactic:
let hev := isColimitOfPreserves ((evaluation _ _).obj k) h

Result:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ Type w
k : K
t : Cocone F
h : IsColimit t
x : t.pt.obj k
inst✝ : ∀ (k : K), HasColimit (F.flip.obj k)
hev : IsColimit (((evaluation K (Type w)).obj k).mapCocone t) := isColimitOfPreserves ((evaluation K (Type w)).obj k) h
⊢ ∃ j y, x = (t.ι.app j).app k y

Proof state:
case intro.intro
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ Type w
k : K
t : Cocone F
h : IsColimit t
inst✝ : ∀ (k : K), HasColimit (F.flip.obj k)
hev : IsColimit (((evaluation K (Type w)).obj k).mapCocone t) := isColimitOfPreserves ((evaluation K (Type w)).obj k) h
j : J
y : (F ⋙ (evaluation K (Type w)).obj k).obj j
⊢ ∃ j_1 y_1, (((evaluation K (Type w)).obj k).mapCocone t).ι.app j y = (t.ι.app j_1).app k y_1

Tactic:
exact ⟨j, y, by simp⟩

Result:
no goals

Proof state:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ Type w
k : K
t : Cocone F
h : IsColimit t
inst✝ : ∀ (k : K), HasColimit (F.flip.obj k)
hev : IsColimit (((evaluation K (Type w)).obj k).mapCocone t) := isColimitOfPreserves ((evaluation K (Type w)).obj k) h
j : J
y : (F ⋙ (evaluation K (Type w)).obj k).obj j
⊢ (((evaluation K (Type w)).obj k).mapCocone t).ι.app j y = (t.ι.app j).app k y

Tactic:
simp

Result:
no goals

Proof state:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ Type w
k : K
t : Cocone F
h : IsColimit t
x : t.pt.obj k
inst✝ : ∀ (k : K), HasColimit (F.flip.obj k)
hev : IsColimit (((evaluation K (Type w)).obj k).mapCocone t) := isColimitOfPreserves ((evaluation K (Type w)).obj k) h
⊢ ∃ j y, x = (t.ι.app j).app k y

Tactic:
obtain ⟨j, y, rfl⟩ := Types.jointly_surjective _ hev x

Result:
case intro.intro
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ Type w
k : K
t : Cocone F
h : IsColimit t
inst✝ : ∀ (k : K), HasColimit (F.flip.obj k)
hev : IsColimit (((evaluation K (Type w)).obj k).mapCocone t) := isColimitOfPreserves ((evaluation K (Type w)).obj k) h
j : J
y : (F ⋙ (evaluation K (Type w)).obj k).obj j
⊢ ∃ j_1 y_1, (((evaluation K (Type w)).obj k).mapCocone t).ι.app j y = (t.ι.app j_1).app k y_1
-- Mathlib/Algebra/Order/Hom/Monoid.lean
theorem cancel_right {g₁ g₂ : β →*₀o γ} {f : α →*₀o β} (hf : Function.Surjective f) :
    g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h => ext <| hf.forall.2 <| DFunLike.ext_iff.1 h, fun _ => by congr⟩

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : MulZeroOneClass α
inst✝¹ : MulZeroOneClass β
inst✝ : MulZeroOneClass γ
g₁ g₂ : β →*₀o γ
f : α →*₀o β
hf : Surjective ⇑f
x✝ : g₁ = g₂
⊢ g₁.comp f = g₂.comp f

Tactic:
congr

Result:
no goals