harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem isNormal_derivFamily [Small.{u} ι] (f : ι → Ordinal.{u} → Ordinal.{u}) :
    IsNormal (derivFamily f)

Proof state:
case refine_1
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
⊢ succ (derivFamily f o) ≤ nfpFamily f (succ (derivFamily f o))

Tactic:
exact le_nfpFamily _ _

Result:
no goals

Proof state:
case refine_1
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
⊢ derivFamily f o < derivFamily f (succ o)

Tactic:
rw [derivFamily_succ, ← succ_le_iff]

Result:
case refine_1
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
⊢ succ (derivFamily f o) ≤ nfpFamily f (succ (derivFamily f o))

Proof state:
case refine_2
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
h : o.IsLimit
a : Ordinal.{u}
⊢ derivFamily f o ≤ a ↔ ∀ b < o, derivFamily f b ≤ a

Tactic:
simp_rw [derivFamily_limit _ h, Ordinal.iSup_le_iff, Subtype.forall, Set.mem_Iio]

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
⊢ IsNormal (derivFamily f)

Tactic:
refine ⟨fun o ↦ ?_, fun o h a ↦ ?_⟩

Result:
case refine_1
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
⊢ derivFamily f o < derivFamily f (succ o)

case refine_2
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
h : o.IsLimit
a : Ordinal.{u}
⊢ derivFamily f o ≤ a ↔ ∀ b < o, derivFamily f b ≤ a
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
@[simp]
lemma cfcₙ_zero : cfcₙ (0 : R → R) a = 0

Proof state:
case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
a : A
ha : ¬p a
⊢ cfcₙ 0 a = 0

Tactic:
rw [cfcₙ_apply_of_not_predicate a ha]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
a : A
⊢ cfcₙ 0 a = 0

Tactic:
by_cases ha : p a

Result:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
a : A
ha : p a
⊢ cfcₙ 0 a = 0

case neg
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
a : A
ha : ¬p a
⊢ cfcₙ 0 a = 0

Proof state:
case pos
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
a : A
ha : p a
⊢ cfcₙ 0 a = 0

Tactic:
exact cfcₙ_apply (0 : R → R) a ▸ map_zero (cfcₙHom ha)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem and_pow_two_sub_one_of_lt_two_pow {x : Nat} (lt : x < 2^n) : x &&& 2^n - 1 = x

Proof state:
n x : Nat
lt : x < 2 ^ n
⊢ x &&& 2 ^ n - 1 = x

Tactic:
rw [and_pow_two_sub_one_eq_mod]

Result:
n x : Nat
lt : x < 2 ^ n
⊢ x % 2 ^ n = x

Proof state:
n x : Nat
lt : x < 2 ^ n
⊢ x % 2 ^ n = x

Tactic:
apply Nat.mod_eq_of_lt lt

Result:
no goals
-- Mathlib/NumberTheory/Rayleigh.lean
theorem beattySeq_symmDiff_beattySeq'_pos {r s : ℝ} (hrs : r.IsConjExponent s) :
    {beattySeq r k | k > 0} ∆ {beattySeq' s k | k > 0} = {n | 0 < n}

Proof state:
r s : ℝ
hrs : r.IsConjExponent s
j : ℤ
hj : 0 < j
hb₁ : ∀ s ≥ 0, j ∈ {x | ∃ k > 0, beattySeq s k = x} ↔ j ∈ {x | ∃ k, beattySeq s k = x}
s✝ : ℝ
hs : s✝ ≥ 0
x✝ : j ∈ {x | ∃ k, beattySeq' s✝ k = x}
k : ℤ
hk : beattySeq' s✝ k = j
⊢ k > 0

Tactic:
rw [← hk, beattySeq', sub_pos, Int.lt_ceil, Int.cast_one] at hj

Result:
r s : ℝ
hrs : r.IsConjExponent s
j : ℤ
hb₁ : ∀ s ≥ 0, j ∈ {x | ∃ k > 0, beattySeq s k = x} ↔ j ∈ {x | ∃ k, beattySeq s k = x}
s✝ : ℝ
hs : s✝ ≥ 0
x✝ : j ∈ {x | ∃ k, beattySeq' s✝ k = x}
k : ℤ
hj : 1 < ↑k * s✝
hk : beattySeq' s✝ k = j
⊢ k > 0

Proof state:
case a
r s : ℝ
hrs : r.IsConjExponent s
j : ℤ
hj : 0 < j
hb₁ : ∀ s ≥ 0, j ∈ {x | ∃ k > 0, beattySeq s k = x} ↔ j ∈ {x | ∃ k, beattySeq s k = x}
hb₂ : ∀ s ≥ 0, j ∈ {x | ∃ k > 0, beattySeq' s k = x} ↔ j ∈ {x | ∃ k, beattySeq' s k = x}
⊢ j ∈ {x | ∃ k, beattySeq r k = x} ∨ j ∉ {x | ∃ k, beattySeq r k = x}

Tactic:
exact or_not

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/BasicAux.lean
theorem append_cancel_left {as bs cs : List α} (h : as ++ bs = as ++ cs) : bs = cs

Proof state:
case cons
α : Type u_1
bs cs : List α
a : α
as : List α
ih : as ++ bs = as ++ cs → bs = cs
head_eq✝ : a = a
h : as.append bs = as.append cs
⊢ bs = cs

Tactic:
exact ih h

Result:
no goals

Proof state:
case cons
α : Type u_1
bs cs : List α
a : α
as : List α
ih : as ++ bs = as ++ cs → bs = cs
h : a :: as ++ bs = a :: as ++ cs
⊢ bs = cs

Tactic:
injection h with _ h

Result:
case cons
α : Type u_1
bs cs : List α
a : α
as : List α
ih : as ++ bs = as ++ cs → bs = cs
head_eq✝ : a = a
h : as.append bs = as.append cs
⊢ bs = cs

Proof state:
case nil
α : Type u_1
bs cs : List α
h : [] ++ bs = [] ++ cs
⊢ bs = cs

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
as bs cs : List α
h : as ++ bs = as ++ cs
⊢ bs = cs

Tactic:
induction as with
| nil => assumption
| cons a as ih =>
  injection h with _ h
  exact ih h

Result:
no goals
-- Mathlib/Algebra/Module/SpanRank.lean
theorem rank_eq_spanRank_of_free [Module.Free R M] [StrongRankCondition R] :
    Module.rank R M = (⊤ : Submodule R M).spanRank

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : StrongRankCondition R
⊢ Module.rank R M = ⊤.spanRank

Tactic:
haveI := nontrivial_of_invariantBasisNumber R

Result:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : StrongRankCondition R
this : Nontrivial R
⊢ Module.rank R M = ⊤.spanRank

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : StrongRankCondition R
this : Nontrivial R
⊢ Module.rank R M = ⊤.spanRank

Tactic:
obtain ⟨I, B⟩ := ‹Module.Free R M›

Result:
case mk.intro.mk
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : StrongRankCondition R
this : Nontrivial R
I : Type v
B : Basis I R M
⊢ Module.rank R M = ⊤.spanRank

Proof state:
case mk.intro.mk
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module.Free R M
inst✝ : StrongRankCondition R
this : Nontrivial R
I : Type v
B : Basis I R M
⊢ Module.rank R M = ⊤.spanRank

Tactic:
rw [← Basis.mk_eq_rank'' B, ← Basis.mk_eq_spanRank B, ← Cardinal.lift_id #(Set.range B),
  Cardinal.mk_range_eq_of_injective B.injective, Cardinal.lift_id _]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem letFun_body_congr {α : Sort u} {β : Sort v}  (a : α) {f f' : α → β} (h : ∀ x, f x = f' x)
    : @letFun α (fun _ => β) a f = @letFun α (fun _ => β) a f'

Proof state:
α : Sort u
β : Sort v
a : α
f f' : α → β
h : ∀ (x : α), f x = f' x
⊢ letFun a f = letFun a f'

Tactic:
rw [funext h]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
lemma inl_desc :
    (inl φ).comp (Cochain.ofHom (desc φ α β eq)) (add_zero _) = α

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
α : Cochain F K (-1)
β : G ⟶ K
eq : δ (-1) 0 α = Cochain.ofHom (φ ≫ β)
⊢ (inl φ).comp (Cochain.ofHom (desc φ α β eq)) ⋯ = α

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Radical.lean
theorem FG.eq_bot_of_le_jacobson_smul {N : Submodule R M} (fg : N.FG)
    (le : N ≤ Ring.jacobson R • N) : N = ⊥

Proof state:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
fg : N.FG
le : N ≤ Ring.jacobson R • N
⊢ N = ⊥

Tactic:
contrapose! le

Result:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
fg : N.FG
le : N ≠ ⊥
⊢ ¬N ≤ Ring.jacobson R • N

Proof state:
R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
fg : N.FG
le : N ≠ ⊥
⊢ ¬N ≤ Ring.jacobson R • N

Tactic:
exact (jacobson_smul_lt le fg).not_le

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem card_cycleType_eq_one {σ : Perm α} : Multiset.card σ.cycleType = 1 ↔ σ.IsCycle

Proof state:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsCycle
⊢ (σ.IsCycle ∧ σ = σ) ∧ (Finset.card ∘ support) σ = σ.support.card

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ (∃ a, σ.cycleType = {a}) ↔ σ.IsCycle

Tactic:
simp_rw [cycleType_def, Multiset.map_eq_singleton, ← Finset.singleton_val, Finset.val_inj,
  cycleFactorsFinset_eq_singleton_iff]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ (∃ a a_1, (σ.IsCycle ∧ σ = a_1) ∧ (Finset.card ∘ support) a_1 = a) ↔ σ.IsCycle

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ σ.cycleType.card = 1 ↔ σ.IsCycle

Tactic:
rw [card_eq_one]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ (∃ a, σ.cycleType = {a}) ↔ σ.IsCycle

Proof state:
case mp.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
w✝¹ : ℕ
w✝ : Perm α
h : σ.IsCycle
⊢ σ.IsCycle

Tactic:
exact h

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ (∃ a a_1, (σ.IsCycle ∧ σ = a_1) ∧ (Finset.card ∘ support) a_1 = a) → σ.IsCycle

Tactic:
rintro ⟨_, _, ⟨h, -⟩, -⟩

Result:
case mp.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
w✝¹ : ℕ
w✝ : Perm α
h : σ.IsCycle
⊢ σ.IsCycle

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ (∃ a a_1, (σ.IsCycle ∧ σ = a_1) ∧ (Finset.card ∘ support) a_1 = a) ↔ σ.IsCycle

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ (∃ a a_1, (σ.IsCycle ∧ σ = a_1) ∧ (Finset.card ∘ support) a_1 = a) → σ.IsCycle

case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ σ.IsCycle → ∃ a a_1, (σ.IsCycle ∧ σ = a_1) ∧ (Finset.card ∘ support) a_1 = a

Proof state:
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsCycle
⊢ ∃ a a_1, (σ.IsCycle ∧ σ = a_1) ∧ (Finset.card ∘ support) a_1 = a

Tactic:
use σ.support.card, σ

Result:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsCycle
⊢ (σ.IsCycle ∧ σ = σ) ∧ (Finset.card ∘ support) σ = σ.support.card

Proof state:
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ σ.IsCycle → ∃ a a_1, (σ.IsCycle ∧ σ = a_1) ∧ (Finset.card ∘ support) a_1 = a

Tactic:
intro h

Result:
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsCycle
⊢ ∃ a a_1, (σ.IsCycle ∧ σ = a_1) ∧ (Finset.card ∘ support) a_1 = a
-- Mathlib/Data/List/Rotate.lean
theorem isRotated_concat (hd : α) (tl : List α) : (tl ++ [hd]) ~r (hd :: tl) :=
  IsRotated.symm ⟨1, by simp⟩

Proof state:
α : Type u
hd : α
tl : List α
⊢ (hd :: tl).rotate 1 = tl ++ [hd]

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem IsClosed.smul_left_of_isCompact (ht : IsClosed t) (hs : IsCompact s) :
    IsClosed (s • t)

Proof state:
α : Type u
β : Type v
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : Group α
inst✝² : MulAction α β
inst✝¹ : ContinuousInv α
inst✝ : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed t
hs : IsCompact s
⊢ IsClosed (s • t)

Tactic:
have : ∀ x ∈ s • t, ∃ g ∈ s, g⁻¹ • x ∈ t := by
  rintro x ⟨g, hgs, y, hyt, rfl⟩
  refine ⟨g, hgs, ?_⟩
  rwa [inv_smul_smul]

Result:
α : Type u
β : Type v
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : Group α
inst✝² : MulAction α β
inst✝¹ : ContinuousInv α
inst✝ : ContinuousSMul α β
s : Set α
t : Set β
ht : IsClosed t
hs : IsCompact s
this : ∀ x ∈ s • t, ∃ g ∈ s, g⁻¹ • x ∈ t
⊢ IsClosed (s • t)
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem exists_nat_nat_continuous_surjective_of_completeSpace (α : Type*) [MetricSpace α]
    [CompleteSpace α] [SecondCountableTopology α] [Nonempty α] :
    ∃ f : (ℕ → ℕ) → α, Continuous f ∧ Surjective f

Proof state:
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x => Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
y x : ↑s
hxy : dist x y < 1
hne : x ≠ y
hne' : ↑x ≠ ↑y
dist' : dist x y = dist ↑x ↑y
n : ℕ := firstDiff ↑x ↑y - 1
⊢ 0 < firstDiff ↑x ↑y

Tactic:
by_contra! h

Result:
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x => Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
y x : ↑s
hxy : dist x y < 1
hne : x ≠ y
hne' : ↑x ≠ ↑y
dist' : dist x y = dist ↑x ↑y
n : ℕ := firstDiff ↑x ↑y - 1
h : firstDiff ↑x ↑y ≤ 0
⊢ False

Proof state:
case inl
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x => Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
x : ↑s
hxy : dist x x < 1
⊢ dist (g x) (g x) ≤ 4 * dist x x

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x => Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
y x : ↑s
hxy : dist x y < 1
hne : x ≠ y
hne' : ↑x ≠ ↑y
dist' : dist x y = dist ↑x ↑y
n : ℕ := firstDiff ↑x ↑y - 1
h : firstDiff ↑x ↑y ≤ 0
⊢ dist ↑x ↑y < (1 / 2) ^ 0

Tactic:
rw [pow_zero]

Result:
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x => Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
y x : ↑s
hxy : dist x y < 1
hne : x ≠ y
hne' : ↑x ≠ ↑y
dist' : dist x y = dist ↑x ↑y
n : ℕ := firstDiff ↑x ↑y - 1
h : firstDiff ↑x ↑y ≤ 0
⊢ dist ↑x ↑y < 1
-- Mathlib/RingTheory/ChainOfDivisors.lean
theorem element_of_chain_eq_pow_second_of_chain {q r : Associates M} {n : ℕ} (hn : n ≠ 0)
    {c : Fin (n + 1) → Associates M} (h₁ : StrictMono c) (h₂ : ∀ {r}, r ≤ q ↔ ∃ i, r = c i)
    (hr : r ∣ q) (hq : q ≠ 0) : ∃ i : Fin (n + 1), r = c 1 ^ (i : ℕ)

Proof state:
case intro.intro
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
this : (Finset.image (fun m => c 1 ^ ↑m) Finset.univ).card = i + 1
a : Fin (i + 1)
left✝ : a ∈ Finset.univ
⊢ c 1 ^ ↑a ≤ q

Tactic:
refine dvd_trans ?_ hr

Result:
case intro.intro
M : Type u_1
inst✝¹ : CancelCommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
this : (Finset.image (fun m => c 1 ^ ↑m) Finset.univ).card = i + 1
a : Fin (i + 1)
left✝ : a ∈ Finset.univ
⊢ c 1 ^ ↑a ∣ r
-- Mathlib/Analysis/Analytic/CPolynomialDef.lean
theorem FormalMultilinearSeries.hasFiniteFPowerSeriesOnBall_of_finite
    (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (hn : ∀ m, n ≤ m → p m = 0) :
    HasFiniteFPowerSeriesOnBall p.sum p 0 n ⊤ where
  r_le

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
⊢ ⊤ ≤ p.radius

Tactic:
rw [radius_eq_top_of_forall_image_add_eq_zero p n fun _ => hn _ (Nat.le_add_left _ _)]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
y : E
x✝ : y ∈ EMetric.ball 0 ⊤
⊢ HasSum (fun n => (p n) fun x => y) (p.sum y)

Tactic:
exact p.hasSum_of_finite hn y

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
y : E
x✝ : y ∈ EMetric.ball 0 ⊤
⊢ HasSum (fun n => (p n) fun x => y) (p.sum (0 + y))

Tactic:
rw [zero_add]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
y : E
x✝ : y ∈ EMetric.ball 0 ⊤
⊢ HasSum (fun n => (p n) fun x => y) (p.sum y)
-- Mathlib/NumberTheory/Harmonic/GammaDeriv.lean
lemma hasDerivAt_Gamma_one_half : HasDerivAt Gamma (-√π * (γ + 2 * log 2)) (1 / 2)

Proof state:
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
⊢ HasDerivAt Gamma (-√π * (γ + 2 * log 2)) (1 / 2)

Tactic:
have h_diff' {s : ℝ} (hs : 0 < s) : DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s :=
  .comp (g := Gamma) _ (h_diff <| mul_pos two_pos hs) (differentiableAt_id.const_mul _)

Result:
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ HasDerivAt Gamma (-√π * (γ + 2 * log 2)) (1 / 2)

Proof state:
case e_a.e_a.e_a.h.refine_2
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
this : HasDerivAt (fun x => 2 ^ (1 - 2 * x)) (-(2 * log 2)) (1 / 2)
⊢ HasDerivAt (fun s => 2 ^ (1 - 2 * s)) (-(2 * log 2)) (1 / 2)

Tactic:
exact this

Result:
no goals

Proof state:
case e_a.e_a.e_a.h
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ HasDerivAt (fun s => 2 ^ (1 - 2 * s)) (-(2 * log 2)) (1 / 2)

Tactic:
have := HasDerivAt.rpow (hasDerivAt_const (1 / 2 : ℝ) (2 : ℝ))
  (?_ : HasDerivAt (fun s : ℝ ↦ 1 - 2 * s) (-2) (1 / 2)) two_pos

Result:
case e_a.e_a.e_a.h.refine_2
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
this :
  HasDerivAt (fun x => 2 ^ (1 - 2 * x))
    (0 * (1 - 2 * (1 / 2)) * 2 ^ (1 - 2 * (1 / 2) - 1) + -2 * 2 ^ (1 - 2 * (1 / 2)) * log 2) (1 / 2)
⊢ HasDerivAt (fun s => 2 ^ (1 - 2 * s)) (-(2 * log 2)) (1 / 2)

case e_a.e_a.e_a.h.refine_1
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ HasDerivAt (fun s => 1 - 2 * s) (-2) (1 / 2)

Proof state:
case hs
h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s => Gamma (2 * s)) s
⊢ 0 < 2 * (1 / 2)

Tactic:
norm_num

Result:
no goals
-- Mathlib/Analysis/Complex/PhragmenLindelof.lean
theorem eq_zero_on_right_half_plane_of_superexponential_decay (hd : DiffContOnCl ℂ f {z | 0 < z.re})
    (hexp : ∃ c < (2 : ℝ), ∃ B,
      f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ‖z‖ ^ c))
    (hre : SuperpolynomialDecay atTop expR fun x => ‖f x‖) (him : ∃ C, ∀ x : ℝ, ‖f (x * I)‖ ≤ C) :
    EqOn f 0 {z : ℂ | 0 ≤ z.re}

Proof state:
case intro.refine_1.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hre : SuperpolynomialDecay atTop expR fun x => ‖f ↑x‖
C : ℝ
hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
g : ℕ → ℂ → E := fun n z => cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
n : ℕ
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ‖z‖ ^ c)
⊢ (fun x => ‖g n x‖) =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR ((↑n + B ⊔ 0) * ‖z‖ ^ (c ⊔ 1))

Tactic:
simp only [hg]

Result:
case intro.refine_1.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hre : SuperpolynomialDecay atTop expR fun x => ‖f ↑x‖
C : ℝ
hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
g : ℕ → ℂ → E := fun n z => cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
n : ℕ
c : ℝ
hc : c < 2
B : ℝ
hO : f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR (B * ‖z‖ ^ c)
⊢ (fun x => expR x.re ^ n * ‖f x‖) =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z => expR ((↑n + B ⊔ 0) * ‖z‖ ^ (c ⊔ 1))