harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem Orthonormal.exists_orthonormalBasis_extension (hv : Orthonormal 𝕜 ((↑) : v → E)) :
    ∃ (u : Finset E) (b : OrthonormalBasis u 𝕜 E), v ⊆ u ∧ ⇑b = ((↑) : u → E)

Proof state:
case intro.intro.intro
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : u₀.Finite
u : Finset E := hu₀_finite.toFinset
fu : { x // x ∈ u } ≃ ↑u₀ := hu₀_finite.subtypeEquivToFinset.symm
hu : Orthonormal 𝕜 Subtype.val
⊢ ∃ u b, v ⊆ ↑u ∧ ⇑b = Subtype.val

Tactic:
refine ⟨u, OrthonormalBasis.mkOfOrthogonalEqBot hu ?_, ?_, ?_⟩

Result:
case intro.intro.intro.refine_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : u₀.Finite
u : Finset E := hu₀_finite.toFinset
fu : { x // x ∈ u } ≃ ↑u₀ := hu₀_finite.subtypeEquivToFinset.symm
hu : Orthonormal 𝕜 Subtype.val
⊢ (span 𝕜 (range Subtype.val))ᗮ = ⊥

case intro.intro.intro.refine_2
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : u₀.Finite
u : Finset E := hu₀_finite.toFinset
fu : { x // x ∈ u } ≃ ↑u₀ := hu₀_finite.subtypeEquivToFinset.symm
hu : Orthonormal 𝕜 Subtype.val
⊢ v ⊆ ↑u

case intro.intro.intro.refine_3
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
u₀ : Set E
hu₀s : u₀ ⊇ v
hu₀ : Orthonormal 𝕜 Subtype.val
hu₀_max : (span 𝕜 u₀)ᗮ = ⊥
hu₀_finite : u₀.Finite
u : Finset E := hu₀_finite.toFinset
fu : { x // x ∈ u } ≃ ↑u₀ := hu₀_finite.subtypeEquivToFinset.symm
hu : Orthonormal 𝕜 Subtype.val
⊢ ⇑(OrthonormalBasis.mkOfOrthogonalEqBot hu ?intro.intro.intro.refine_1) = Subtype.val
-- Mathlib/Analysis/Normed/MulAction.lean
theorem BoundedSMul.of_norm_smul_le (h : ∀ (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖) :
    BoundedSMul α β :=
  { dist_smul_pair' := fun a b₁ b₂ => by simpa [smul_sub, dist_eq_norm] using h a (b₁ - b₂)
    dist_pair_smul' := fun a₁ a₂ b => by simpa [sub_smul, dist_eq_norm] using h (a₁ - a₂) b }

Proof state:
α : Type u_1
β : Type u_2
inst✝² : SeminormedRing α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Module α β
h : ∀ (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖
a₁ a₂ : α
b : β
⊢ dist (a₁ • b) (a₂ • b) ≤ dist a₁ a₂ * dist b 0

Tactic:
simpa [sub_smul, dist_eq_norm] using h (a₁ - a₂) b

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : SeminormedRing α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Module α β
h : ∀ (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖
a : α
b₁ b₂ : β
⊢ dist (a • b₁) (a • b₂) ≤ dist a 0 * dist b₁ b₂

Tactic:
simpa [smul_sub, dist_eq_norm] using h a (b₁ - b₂)

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Pointwise.lean
theorem mul_eq_closure_mul_set (M N : AddSubmonoid R) :
    M * N = closure ((M : Set R) * (N : Set R))

Proof state:
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
M N : AddSubmonoid R
⊢ M * N = closure (↑M * ↑N)

Tactic:
rw [← closure_mul_closure, closure_eq, closure_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_eq_keys_contains [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
    {a : α} : containsKey a l = (keys l).contains a

Proof state:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a : α
⊢ containsKey a [] = (keys []).contains a

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ : containsKey a tail✝ = (keys tail✝).contains a
⊢ containsKey a (⟨k✝, v✝⟩ :: tail✝) = (keys (⟨k✝, v✝⟩ :: tail✝)).contains a

Tactic:
next k _ l ih => simp [ih, BEq.comm]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a k : α
v✝ : β k
l : List ((a : α) × β a)
ih : containsKey a l = (keys l).contains a
⊢ containsKey a (⟨k, v✝⟩ :: l) = (keys (⟨k, v✝⟩ :: l)).contains a

Tactic:
simp [ih, BEq.comm]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a : α
⊢ containsKey a l = (keys l).contains a

Tactic:
induction l using assoc_induction

Result:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a : α
⊢ containsKey a [] = (keys []).contains a

case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ : containsKey a tail✝ = (keys tail✝).contains a
⊢ containsKey a (⟨k✝, v✝⟩ :: tail✝) = (keys (⟨k✝, v✝⟩ :: tail✝)).contains a
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean
@[aesop safe apply (rule_sets := [CStarAlgebra])]
lemma _root_.IsSelfAdjoint.exp_nonneg {𝕜 : Type*} [Field 𝕜] [Algebra 𝕜 A]
    [PartialOrder A] [StarOrderedRing A] {a : A} (ha : IsSelfAdjoint a) :
    0 ≤ exp 𝕜 a

Proof state:
A : Type u_1
inst✝⁹ : NormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : IsTopologicalRing A
inst✝⁶ : NormedAlgebra ℝ A
inst✝⁵ : CompleteSpace A
inst✝⁴ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : Algebra 𝕜 A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
⊢ 0 ≤ exp 𝕜 a

Tactic:
rw [exp_eq_exp 𝕜 ℝ, ← real_exp_eq_normedSpace_exp]

Result:
A : Type u_1
inst✝⁹ : NormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : IsTopologicalRing A
inst✝⁶ : NormedAlgebra ℝ A
inst✝⁵ : CompleteSpace A
inst✝⁴ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : Algebra 𝕜 A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
⊢ 0 ≤ cfc Real.exp a

Proof state:
A : Type u_1
inst✝⁹ : NormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : IsTopologicalRing A
inst✝⁶ : NormedAlgebra ℝ A
inst✝⁵ : CompleteSpace A
inst✝⁴ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : Algebra 𝕜 A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
⊢ 0 ≤ cfc Real.exp a

Tactic:
exact cfc_nonneg fun x _ => Real.exp_nonneg x

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_sin_pow_three :
    ∫ x in a..b, sin x ^ 3 = cos a - cos b - (cos a ^ 3 - cos b ^ 3) / 3

Proof state:
a b : ℝ
this : ∫ (x : ℝ) in a..b, sin x ^ (2 * 1 + 1) * cos x ^ 0 = ∫ (u : ℝ) in cos b..cos a, u ^ 0 * (1 - u ^ 2) ^ 1
⊢ ∫ (x : ℝ) in a..b, sin x ^ 3 = cos a - cos b - (cos a ^ 3 - cos b ^ 3) / 3

Tactic:
norm_num at this

Result:
a b : ℝ
this : ∫ (x : ℝ) in a..b, sin x ^ 3 = cos a - cos b - (cos a ^ 3 - cos b ^ 3) / 3
⊢ ∫ (x : ℝ) in a..b, sin x ^ 3 = cos a - cos b - (cos a ^ 3 - cos b ^ 3) / 3

Proof state:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, sin x ^ 3 = cos a - cos b - (cos a ^ 3 - cos b ^ 3) / 3

Tactic:
have := @integral_sin_pow_odd_mul_cos_pow a b 1 0

Result:
a b : ℝ
this : ∫ (x : ℝ) in a..b, sin x ^ (2 * 1 + 1) * cos x ^ 0 = ∫ (u : ℝ) in cos b..cos a, u ^ 0 * (1 - u ^ 2) ^ 1
⊢ ∫ (x : ℝ) in a..b, sin x ^ 3 = cos a - cos b - (cos a ^ 3 - cos b ^ 3) / 3

Proof state:
a b : ℝ
this : ∫ (x : ℝ) in a..b, sin x ^ 3 = cos a - cos b - (cos a ^ 3 - cos b ^ 3) / 3
⊢ ∫ (x : ℝ) in a..b, sin x ^ 3 = cos a - cos b - (cos a ^ 3 - cos b ^ 3) / 3

Tactic:
exact this

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem IsBasis.union_isBasis_union (hIX : M.IsBasis I X) (hJY : M.IsBasis J Y)
    (h : M.Indep (I ∪ J)) : M.IsBasis (I ∪ J) (X ∪ Y)

Proof state:
case refine_2
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
⊢ M.Indep (⋃ i, bif i then I else J)

Tactic:
rwa [← union_eq_iUnion]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
⊢ M.IsBasis J Y ∧ M.IsBasis I X

Tactic:
exact ⟨hJY, hIX⟩

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
⊢ M.IsBasis (⋃ b, bif b then I else J) (⋃ b, bif b then X else Y)

Tactic:
refine IsBasis.iUnion_isBasis_iUnion _ _ ?_ ?_

Result:
case refine_1
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
⊢ ∀ (i : Bool), M.IsBasis (bif i then I else J) (bif i then X else Y)

case refine_2
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
⊢ M.Indep (⋃ i, bif i then I else J)

Proof state:
case refine_1
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
⊢ ∀ (i : Bool), M.IsBasis (bif i then I else J) (bif i then X else Y)

Tactic:
simp only [Bool.forall_bool, cond_false, cond_true]

Result:
case refine_1
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
⊢ M.IsBasis J Y ∧ M.IsBasis I X

Proof state:
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
⊢ M.IsBasis (I ∪ J) (X ∪ Y)

Tactic:
rw [union_eq_iUnion, union_eq_iUnion]

Result:
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
⊢ M.IsBasis (⋃ b, bif b then I else J) (⋃ b, bif b then X else Y)
-- Mathlib/RingTheory/LaurentSeries.lean
theorem powerSeriesPart_eq_zero (x : R⸨X⸩) : x.powerSeriesPart = 0 ↔ x = 0

Proof state:
case mp
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ x.powerSeriesPart = 0 → x = 0

Tactic:
contrapose!

Result:
case mp
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ x ≠ 0 → x.powerSeriesPart ≠ 0

Proof state:
case mp
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ ¬x = 0 → ¬x.powerSeriesPart = 0

Tactic:
intro h

Result:
case mp
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
h : ¬x = 0
⊢ ¬x.powerSeriesPart = 0

Proof state:
case mp
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ x ≠ 0 → x.powerSeriesPart ≠ 0

Tactic:
simp only [ne_eq]

Result:
case mp
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ ¬x = 0 → ¬x.powerSeriesPart = 0

Proof state:
case mp
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
h : ¬x = 0
⊢ ∃ x_1, ¬(PowerSeries.coeff R x_1) x.powerSeriesPart = (PowerSeries.coeff R x_1) 0

Tactic:
refine ⟨0, ?_⟩

Result:
case mp
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
h : ¬x = 0
⊢ ¬(PowerSeries.coeff R 0) x.powerSeriesPart = (PowerSeries.coeff R 0) 0

Proof state:
case mpr
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ x = 0 → x.powerSeriesPart = 0

Tactic:
rintro rfl

Result:
case mpr
R : Type u_1
inst✝ : Semiring R
⊢ powerSeriesPart 0 = 0

Proof state:
case mp
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
h : ¬x = 0
⊢ ¬(PowerSeries.coeff R 0) x.powerSeriesPart = (PowerSeries.coeff R 0) 0

Tactic:
simp [coeff_order_ne_zero h]

Result:
no goals

Proof state:
case mp
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
h : ¬x = 0
⊢ ¬x.powerSeriesPart = 0

Tactic:
rw [PowerSeries.ext_iff, not_forall]

Result:
case mp
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
h : ¬x = 0
⊢ ∃ x_1, ¬(PowerSeries.coeff R x_1) x.powerSeriesPart = (PowerSeries.coeff R x_1) 0

Proof state:
case mpr
R : Type u_1
inst✝ : Semiring R
⊢ powerSeriesPart 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ x.powerSeriesPart = 0 ↔ x = 0

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ x.powerSeriesPart = 0 → x = 0

case mpr
R : Type u_1
inst✝ : Semiring R
x : R⸨X⸩
⊢ x = 0 → x.powerSeriesPart = 0
-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem AffineIndependent.affineIndependent_of_not_mem_span {p : ι → P} {i : ι}
    (ha : AffineIndependent k fun x : { y // y ≠ i } => p x)
    (hi : p i ∉ affineSpan k (p '' { x | x ≠ i })) : AffineIndependent k p

Proof state:
case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : p i ∉ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∉ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x => w ↑x
⊢ ∀ i ∈ s, w i = 0

Tactic:
have hw' : ∑ x ∈ s', w' x = 0 := by
  simp_rw [w', s', Finset.sum_subtype_eq_sum_filter]
  rw [Finset.sum_filter_of_ne, hw]
  rintro x hxs hwx rfl
  exact hwx (his.neg_resolve_left hxs)

Result:
case neg
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : p i ∉ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∉ s ∨ w i = 0
w' : { y // y ≠ i } → k := fun x => w ↑x
hw' : ∑ x ∈ s', w' x = 0
⊢ ∀ i ∈ s, w i = 0

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : p i ∉ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : (s.weightedVSub p) wm = 0
hwm : ∑ x ∈ filter (fun x => x ≠ i) s, wm x + ∑ x ∈ filter (fun x => ¬x ≠ i) s, wm x = 0
hwmi : wm i = -1
w' : { y // y ≠ i } → k := fun x => wm ↑x
⊢ ∑ x ∈ filter (fun x => x ≠ i) s, wm x = 1

Tactic:
simp_rw [Classical.not_not] at hwm

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
ι : Type u_4
p : ι → P
i : ι
ha : AffineIndependent k fun x => p ↑x
hi : p i ∉ affineSpan k (p '' {x | x ≠ i})
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 0
hs : (s.weightedVSub p) w = 0
s' : Finset { y // y ≠ i } := Finset.subtype (fun x => x ≠ i) s
p' : { y // y ≠ i } → P := fun x => p ↑x
his : i ∈ s ∧ w i ≠ 0
wm : ι → k := -(w i)⁻¹ • w
hms : (s.weightedVSub p) wm = 0
hwmi : wm i = -1
w' : { y // y ≠ i } → k := fun x => wm ↑x
hwm : ∑ x ∈ filter (fun x => x ≠ i) s, wm x + ∑ x ∈ filter (fun x => x = i) s, wm x = 0
⊢ ∑ x ∈ filter (fun x => x ≠ i) s, wm x = 1
-- Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean
theorem unitLattice_inter_ball_finite (r : ℝ) :
    ((unitLattice K : Set ({ w : InfinitePlace K // w ≠ w₀} → ℝ)) ∩
      Metric.closedBall 0 r).Finite

Proof state:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : 0 ≤ r
⊢ ((fun x => (algebraMap (𝓞 K) K) ↑x) ''
      {x |
        IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑x) ∧
          ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)}).Finite

Tactic:
refine (Embeddings.finite_of_norm_le K ℂ
    (Real.exp ((Fintype.card (InfinitePlace K)) * r))).subset ?_

Result:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : 0 ≤ r
⊢ (fun x => (algebraMap (𝓞 K) K) ↑x) ''
      {x |
        IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑x) ∧
          ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)} ⊆
    {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)}

Proof state:
case intro.intro.intro.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : 0 ≤ r
this :
  {x |
      IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑x) ∧
        ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)}.Finite
x : Additive (𝓞 K)ˣ
left✝ : x ∈ ↑⊤
hx : (logEmbedding K).toIntLinearMap x ∈ Metric.closedBall 0 r
w : InfinitePlace K
⊢ 0 < w ((algebraMap (𝓞 K) K) ↑x)

Tactic:
exact pos_iff.mpr (coe_ne_zero x)

Result:
no goals

Proof state:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : 0 ≤ r
⊢ {x |
      IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑x) ∧
        ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)}.Finite

Tactic:
refine Set.Finite.of_finite_image ?_ (coe_injective K).injOn

Result:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
hr : 0 ≤ r
⊢ ((fun x => (algebraMap (𝓞 K) K) ↑x) ''
      {x |
        IsIntegral ℤ ((algebraMap (𝓞 K) K) ↑x) ∧
          ∀ (φ : K →+* ℂ), ‖φ ((algebraMap (𝓞 K) K) ↑x)‖ ≤ Real.exp (↑(Fintype.card (InfinitePlace K)) * r)}).Finite
-- Mathlib/Probability/Moments/IntegrableExpMul.lean
/-- If `exp ((v + t) * X)` and `exp ((v - t) * X)` are integrable
then for any `n : ℕ` and any `x ∈ [0, |t|)`,
`|X| ^ n * exp (v * X + x * |X|)` is integrable. -/
lemma integrable_pow_abs_mul_exp_add_of_integrable_exp_mul {x : ℝ}
    (h_int_pos : Integrable (fun ω ↦ exp ((v + t) * X ω)) μ)
    (h_int_neg : Integrable (fun ω ↦ exp ((v - t) * X ω)) μ) (h_nonneg : 0 ≤ x) (hx : x < |t|)
    (n : ℕ) :
    Integrable (fun a ↦ |X a| ^ n * exp (v * X a + x * |X a|)) μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
n : ℕ
⊢ Integrable (fun a => |X a| ^ n * rexp (v * X a + x * |X a|)) μ

Tactic:
convert integrable_rpow_abs_mul_exp_add_of_integrable_exp_mul h_int_pos h_int_neg h_nonneg hx
  n.cast_nonneg

Result:
case h.e'_6.h.h.e'_5
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
n : ℕ
x✝ : Ω
⊢ |X x✝| ^ n = |X x✝| ^ ↑n

Proof state:
case h.e'_6.h.h.e'_5
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω => rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω => rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
n : ℕ
x✝ : Ω
⊢ |X x✝| ^ n = |X x✝| ^ ↑n

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean
theorem tendsto_exp_mul_div_rpow_atTop (s : ℝ) (b : ℝ) (hb : 0 < b) :
    Tendsto (fun x : ℝ => exp (b * x) / x ^ s) atTop atTop

Proof state:
case h
s b : ℝ
hb : 0 < b
x : ℝ
hx₀ : 0 ≤ x
⊢ ((fun x => x ^ b) ∘ fun x => rexp x / x ^ (s / b)) x = rexp (b * x) / x ^ s

Tactic:
simp [Real.div_rpow, (exp_pos x).le, rpow_nonneg, ← Real.rpow_mul, ← exp_mul,
  mul_comm x, hb.ne', *]

Result:
no goals

Proof state:
s b : ℝ
hb : 0 < b
⊢ Tendsto (fun x => rexp (b * x) / x ^ s) atTop atTop

Tactic:
refine ((tendsto_rpow_atTop hb).comp (tendsto_exp_div_rpow_atTop (s / b))).congr' ?_

Result:
s b : ℝ
hb : 0 < b
⊢ ((fun x => x ^ b) ∘ fun x => rexp x / x ^ (s / b)) =ᶠ[atTop] fun x => rexp (b * x) / x ^ s

Proof state:
s b : ℝ
hb : 0 < b
⊢ ((fun x => x ^ b) ∘ fun x => rexp x / x ^ (s / b)) =ᶠ[atTop] fun x => rexp (b * x) / x ^ s

Tactic:
filter_upwards [eventually_ge_atTop (0 : ℝ)] with x hx₀

Result:
case h
s b : ℝ
hb : 0 < b
x : ℝ
hx₀ : 0 ≤ x
⊢ ((fun x => x ^ b) ∘ fun x => rexp x / x ^ (s / b)) x = rexp (b * x) / x ^ s
-- Mathlib/Analysis/Complex/Polynomial/Basic.lean
lemma Polynomial.mul_star_dvd_of_aeval_eq_zero_im_ne_zero (p : ℝ[X]) {z : ℂ} (h0 : aeval z p = 0)
    (hz : z.im ≠ 0) : (X - C ((starRingEnd ℂ) z)) * (X - C z) ∣ map (algebraMap ℝ ℂ) p

Proof state:
p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ (X - C ((starRingEnd ℂ) z)) * (X - C z) ∣ map (algebraMap ℝ ℂ) p

Tactic:
apply IsCoprime.mul_dvd

Result:
case H
p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ IsCoprime (X - C ((starRingEnd ℂ) z)) (X - C z)

case H1
p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ X - C ((starRingEnd ℂ) z) ∣ map (algebraMap ℝ ℂ) p

case H2
p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ X - C z ∣ map (algebraMap ℝ ℂ) p

Proof state:
case H
p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ IsCoprime (X - C ((starRingEnd ℂ) z)) (X - C z)

Tactic:
exact isCoprime_X_sub_C_of_isUnit_sub <| .mk0 _ <| sub_ne_zero.2 <| mt conj_eq_iff_im.1 hz

Result:
no goals

Proof state:
case H2
p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ X - C z ∣ map (algebraMap ℝ ℂ) p

Tactic:
simpa [dvd_iff_isRoot]

Result:
no goals

Proof state:
case H1
p : ℝ[X]
z : ℂ
h0 : (aeval z) p = 0
hz : z.im ≠ 0
⊢ X - C ((starRingEnd ℂ) z) ∣ map (algebraMap ℝ ℂ) p

Tactic:
simpa [dvd_iff_isRoot, aeval_conj]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma isUnramified_smul_iff :
    IsUnramified k (σ • w) ↔ IsUnramified k w

Proof state:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
σ : K ≃ₐ[k] K
w : InfinitePlace K
⊢ IsUnramified k (σ • w) ↔ IsUnramified k w

Tactic:
rw [isUnramified_iff, isUnramified_iff, isReal_smul_iff, comap_smul,
  ← AlgEquiv.toAlgHom_toRingHom, AlgHom.comp_algebraMap]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem disjoint_prod : Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s₁ s₂ : LowerSet α
t₁ t₂ : LowerSet β
⊢ Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂

Tactic:
simp_rw [disjoint_iff, prod_inf_prod, prod_eq_bot]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
lemma rnDeriv_zero (ν : Measure α) : (0 : Measure α).rnDeriv ν =ᵐ[ν] 0

Proof state:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
⊢ 0 ⟂ₘ ν

Tactic:
exact MutuallySingular.zero_left

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
⊢ rnDeriv 0 ν =ᶠ[ae ν] 0

Tactic:
rw [rnDeriv_eq_zero]

Result:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
⊢ 0 ⟂ₘ ν
-- Mathlib/Combinatorics/SetFamily/Shadow.lean
theorem _root_.Set.Sized.shadow (h𝒜 : (𝒜 : Set (Finset α)).Sized r) :
    (∂ 𝒜 : Set (Finset α)).Sized (r - 1)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
A : Finset α
h : A ∈ ↑(∂ 𝒜)
⊢ #A = r - 1

Tactic:
obtain ⟨A, hA, i, hi, rfl⟩ := mem_shadow_iff.1 h

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
A : Finset α
hA : A ∈ 𝒜
i : α
hi : i ∈ A
h : A.erase i ∈ ↑(∂ 𝒜)
⊢ #(A.erase i) = r - 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
⊢ Set.Sized (r - 1) ↑(∂ 𝒜)

Tactic:
intro A h

Result:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
A : Finset α
h : A ∈ ↑(∂ 𝒜)
⊢ #A = r - 1

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
A : Finset α
hA : A ∈ 𝒜
i : α
hi : i ∈ A
h : A.erase i ∈ ↑(∂ 𝒜)
⊢ #(A.erase i) = r - 1

Tactic:
rw [card_erase_of_mem hi, h𝒜 hA]

Result:
no goals