harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Fourier/FourierTransform.lean
lemma fourierIntegral_eq' (f : V → E) (w : V) :
    𝓕 f w = ∫ v, Complex.exp ((↑(-2 * π * ⟪v, w⟫) * Complex.I)) • f v

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : V → E
w : V
⊢ 𝓕 f w = ∫ (v : V), Complex.exp (↑(-2 * π * inner v w) * Complex.I) • f v

Tactic:
simp_rw [fourierIntegral_eq, Circle.smul_def, Real.fourierChar_apply, mul_neg, neg_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem eraseIdx_eq_empty_iff {l : Array α} {i : Nat} {h} : eraseIdx l i = #[] ↔ l.size = 1 ∧ i = 0

Proof state:
case mk
α : Type u_1
i : Nat
l : List α
h : i < { toList := l }.size
⊢ l = [] → l.length = 1 ∧ i = 0

Tactic:
rintro rfl

Result:
case mk
α : Type u_1
i : Nat
h : i < { toList := [] }.size
⊢ [].length = 1 ∧ i = 0

Proof state:
case mk
α : Type u_1
i : Nat
l : List α
h : i < { toList := l }.size
⊢ { toList := l }.eraseIdx i h = #[] ↔ { toList := l }.size = 1 ∧ i = 0

Tactic:
simp only [List.eraseIdx_toArray, mk.injEq, List.eraseIdx_eq_nil_iff, size_toArray,
  or_iff_right_iff_imp]

Result:
case mk
α : Type u_1
i : Nat
l : List α
h : i < { toList := l }.size
⊢ l = [] → l.length = 1 ∧ i = 0

Proof state:
case mk
α : Type u_1
i : Nat
h : i < { toList := [] }.size
⊢ [].length = 1 ∧ i = 0

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
l : Array α
i : Nat
h : i < l.size
⊢ l.eraseIdx i h = #[] ↔ l.size = 1 ∧ i = 0

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
i : Nat
l : List α
h : i < { toList := l }.size
⊢ { toList := l }.eraseIdx i h = #[] ↔ { toList := l }.size = 1 ∧ i = 0
-- Mathlib/GroupTheory/Subgroup/Center.lean
theorem _root_.CommGroup.center_eq_top {G : Type*} [CommGroup G] : center G = ⊤

Proof state:
G : Type u_2
inst✝ : CommGroup G
x : G
⊢ x ∈ center G

Tactic:
rw [Subgroup.mem_center_iff]

Result:
G : Type u_2
inst✝ : CommGroup G
x : G
⊢ ∀ (g : G), g * x = x * g

Proof state:
G : Type u_2
inst✝ : CommGroup G
x : G
⊢ ∀ (g : G), g * x = x * g

Tactic:
intro y

Result:
G : Type u_2
inst✝ : CommGroup G
x y : G
⊢ y * x = x * y

Proof state:
G : Type u_2
inst✝ : CommGroup G
⊢ center G = ⊤

Tactic:
rw [eq_top_iff']

Result:
G : Type u_2
inst✝ : CommGroup G
⊢ ∀ (x : G), x ∈ center G

Proof state:
G : Type u_2
inst✝ : CommGroup G
⊢ ∀ (x : G), x ∈ center G

Tactic:
intro x

Result:
G : Type u_2
inst✝ : CommGroup G
x : G
⊢ x ∈ center G

Proof state:
G : Type u_2
inst✝ : CommGroup G
x y : G
⊢ y * x = x * y

Tactic:
exact mul_comm y x

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/Basic.lean
theorem exists_one_le_pow_mul_dist {Z N R : Type*} [PseudoMetricSpace R] {d : N → ℝ}
    {j : Z → N → R} {f : R → R} {α : R} {ε M : ℝ}
    -- denominators are positive
    (d0 : ∀ a : N, 1 ≤ d a)
    (e0 : 0 < ε)
    -- function is Lipschitz at α
    (B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M)
    -- clear denominators
    (L : ∀ ⦃z : Z⦄, ∀ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))) :
    ∃ A : ℝ, 0 < A ∧ ∀ z : Z, ∀ a : N, 1 ≤ d a * (dist α (j z a) * A)

Proof state:
Z : Type u_1
N : Type u_2
R : Type u_3
inst✝ : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
me0 : 0 < 1 / ε ⊔ M
⊢ ∃ A, 0 < A ∧ ∀ (z : Z) (a : N), 1 ≤ d a * (dist α (j z a) * A)

Tactic:
refine ⟨max (1 / ε) M, me0, fun z a => ?_⟩

Result:
Z : Type u_1
N : Type u_2
R : Type u_3
inst✝ : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
me0 : 0 < 1 / ε ⊔ M
z : Z
a : N
⊢ 1 ≤ d a * (dist α (j z a) * (1 / ε ⊔ M))

Proof state:
Z : Type u_1
N : Type u_2
R : Type u_3
inst✝ : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
me0 : 0 < 1 / ε ⊔ M
z : Z
a : N
dm1 : ¬1 ≤ dist α (j z a) * (1 / ε ⊔ M)
⊢ j z a ∈ closedBall α ε

Tactic:
refine mem_closedBall'.mp (le_trans ?_ ((one_div_le me0 e0).mpr (le_max_left _ _)))

Result:
Z : Type u_1
N : Type u_2
R : Type u_3
inst✝ : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
me0 : 0 < 1 / ε ⊔ M
z : Z
a : N
dm1 : ¬1 ≤ dist α (j z a) * (1 / ε ⊔ M)
⊢ dist α (j z a) ≤ 1 / (1 / ε ⊔ M)
-- Mathlib/CategoryTheory/Enriched/FunctorCategory.lean
lemma functorHomEquiv_comp [HasFunctorEnrichedHom V F₁ F₂] [HasEnrichedHom V F₁ F₂]
    [HasFunctorEnrichedHom V F₂ F₃] [HasEnrichedHom V F₂ F₃]
    [HasFunctorEnrichedHom V F₁ F₃] [HasEnrichedHom V F₁ F₃]
    (f : F₁ ⟶ F₂) (g : F₂ ⟶ F₃) :
    (functorHomEquiv V) (f ≫ g) = (λ_ (𝟙_ (J ⥤ V))).inv ≫
      ((functorHomEquiv V) f ⊗ (functorHomEquiv V) g) ≫ functorEnrichedComp V F₁ F₂ F₃

Proof state:
case w.h.h
V : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} V
inst✝⁹ : MonoidalCategory V
C : Type u₂
inst✝⁸ : Category.{v₂, u₂} C
J : Type u₃
inst✝⁷ : Category.{v₃, u₃} J
inst✝⁶ : EnrichedOrdinaryCategory V C
F₁ F₂ F₃ : J ⥤ C
inst✝⁵ : HasFunctorEnrichedHom V F₁ F₂
inst✝⁴ : HasEnrichedHom V F₁ F₂
inst✝³ : HasFunctorEnrichedHom V F₂ F₃
inst✝² : HasEnrichedHom V F₂ F₃
inst✝¹ : HasFunctorEnrichedHom V F₁ F₃
inst✝ : HasEnrichedHom V F₁ F₃
f : F₁ ⟶ F₂
g : F₂ ⟶ F₃
j : J
k : Under j
⊢ (λ_ (𝟙_ V)).inv ≫
      ((homEquiv V) f ⊗ (homEquiv V) g) ≫
        enrichedComp V F₁ F₂ F₃ ≫
          enrichedHomπ V F₁ F₃ ((Under.forget j).obj k) ≫
            eHomWhiskerRight V ((Iso.refl (Under.forget j ⋙ F₁)).inv.app k) (F₃.obj ((Under.forget j).obj k)) ≫
              eHomWhiskerLeft V ((Under.forget j ⋙ F₁).obj k) ((Iso.refl (Under.forget j ⋙ F₃)).hom.app k) =
    (λ_ (𝟙_ V)).inv ≫
      ((homEquiv V) f ≫ precompEnrichedHom V F₁ F₂ (Under.forget j) ⊗
          (homEquiv V) g ≫ precompEnrichedHom V F₂ F₃ (Under.forget j)) ≫
        (end_.π (diagram V (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₂)) k ⊗
            end_.π (diagram V (Under.forget j ⋙ F₂) (Under.forget j ⋙ F₃)) k) ≫
          eComp V (Opposite.unop ((Under.forget j ⋙ F₁).op.obj (Opposite.op k))) ((Under.forget j ⋙ F₂).obj k)
            ((Under.forget j ⋙ F₃).obj k)

Tactic:
simp [← tensor_comp_assoc]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
/-- A union indexed by a finite set is totally bounded
if and only if each set of the family is totally bounded. -/
lemma totallyBounded_biUnion {ι : Type*} {I : Set ι} (hI : I.Finite) {s : ι → Set α} :
    TotallyBounded (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, TotallyBounded (s i)

Proof state:
α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
s : ι → Set α
this : Finite ↑I
⊢ TotallyBounded (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, TotallyBounded (s i)

Tactic:
rw [biUnion_eq_iUnion, totallyBounded_iUnion, Subtype.forall]

Result:
no goals

Proof state:
α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
s : ι → Set α
⊢ TotallyBounded (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, TotallyBounded (s i)

Tactic:
have := hI.to_subtype

Result:
α : Type u
uniformSpace : UniformSpace α
ι : Type u_1
I : Set ι
hI : I.Finite
s : ι → Set α
this : Finite ↑I
⊢ TotallyBounded (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, TotallyBounded (s i)
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem uniformContinuous_toFun : UniformContinuous (toFun : (α →ᵤ β) → α → β)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
⊢ ∀ (i : α), UniformContinuous fun x => toFun x i

Tactic:
intro x

Result:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
x : α
⊢ UniformContinuous fun x_1 => toFun x_1 x

Proof state:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
x : α
⊢ UniformContinuous fun x_1 => toFun x_1 x

Tactic:
exact uniformContinuous_eval β x

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
⊢ UniformContinuous ⇑toFun

Tactic:
rw [uniformContinuous_pi]

Result:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
⊢ ∀ (i : α), UniformContinuous fun x => toFun x i
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem whiskerRight_tensor_symm {X X' : C} (f : X ⟶ X') (Y Z : C) :
    f ▷ Y ▷ Z = (α_ X Y Z).hom ≫ f ▷ (Y ⊗ Z) ≫ (α_ X' Y Z).inv

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X X' : C
f : X ⟶ X'
Y Z : C
⊢ f ▷ Y ▷ Z = (α_ X Y Z).hom ≫ f ▷ (Y ⊗ Z) ≫ (α_ X' Y Z).inv

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem Decidable.imp_or [Decidable a] : (a → b ∨ c) ↔ (a → b) ∨ (a → c) :=
  if h : a then by
    rw [imp_iff_right h, imp_iff_right h, imp_iff_right h]
  else by
    rw [iff_false_intro h, false_imp_iff, false_imp_iff, true_or]

Proof state:
a b c : Prop
inst✝ : Decidable a
h : a
⊢ a → b ∨ c ↔ (a → b) ∨ (a → c)

Tactic:
rw [imp_iff_right h, imp_iff_right h, imp_iff_right h]

Result:
no goals

Proof state:
a b c : Prop
inst✝ : Decidable a
h : ¬a
⊢ a → b ∨ c ↔ (a → b) ∨ (a → c)

Tactic:
rw [iff_false_intro h, false_imp_iff, false_imp_iff, true_or]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Free.lean
theorem disjoint_span_sum : Disjoint (span R (range (u ∘ Sum.inl)))
    (span R (range (u ∘ Sum.inr)))

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
u : ι ⊕ ι' → ↑S.X₂
hw : LinearIndependent R (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr)
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
⊢ Disjoint (span R (range (u ∘ Sum.inr))) (LinearMap.ker (Hom.hom S.g))

Tactic:
exact range_ker_disjoint hw

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
u : ι ⊕ ι' → ↑S.X₂
hw : LinearIndependent R (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr)
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
⊢ Disjoint (span R (range (u ∘ Sum.inl))) (span R (range (u ∘ Sum.inr)))

Tactic:
rw [huv, disjoint_comm]

Result:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
u : ι ⊕ ι' → ↑S.X₂
hw : LinearIndependent R (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr)
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
⊢ Disjoint (span R (range (u ∘ Sum.inr))) (span R (range (⇑(ConcreteCategory.hom S.f) ∘ v)))

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
u : ι ⊕ ι' → ↑S.X₂
hw : LinearIndependent R (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr)
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
⊢ Disjoint (span R (range (u ∘ Sum.inr))) (span R (range (⇑(ConcreteCategory.hom S.f) ∘ v)))

Tactic:
refine Disjoint.mono_right (span_mono (range_comp_subset_range _ _)) ?_

Result:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
u : ι ⊕ ι' → ↑S.X₂
hw : LinearIndependent R (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr)
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
⊢ Disjoint (span R (range (u ∘ Sum.inr))) (span R (range ⇑(ConcreteCategory.hom S.f)))

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
u : ι ⊕ ι' → ↑S.X₂
hw : LinearIndependent R (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr)
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
⊢ Disjoint (span R (range (u ∘ Sum.inr))) (span R (range ⇑(ConcreteCategory.hom S.f)))

Tactic:
rw [← LinearMap.range_coe, span_eq (LinearMap.range S.f.hom), hS.moduleCat_range_eq_ker]

Result:
ι : Type u_1
ι' : Type u_2
R : Type u_3
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
hS : S.Exact
v : ι → ↑S.X₁
u : ι ⊕ ι' → ↑S.X₂
hw : LinearIndependent R (⇑(ConcreteCategory.hom S.g) ∘ u ∘ Sum.inr)
huv : u ∘ Sum.inl = ⇑(ConcreteCategory.hom S.f) ∘ v
⊢ Disjoint (span R (range (u ∘ Sum.inr))) (LinearMap.ker (Hom.hom S.g))
-- Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean
lemma esymmAlgHom_surjective (hn : Fintype.card σ ≤ n) :
    Function.Surjective (esymmAlgHom σ R n)

Proof state:
σ : Type u_1
R : Type u_3
n : ℕ
inst✝¹ : Fintype σ
inst✝ : CommRing R
hn : Fintype.card σ ≤ n
⊢ Function.Surjective
    (⇑↑(renameSymmetricSubalgebra (Fintype.equivFin σ).symm) ∘ ⇑(esymmAlgHom (Fin (Fintype.card σ)) R n))

Tactic:
exact (AlgEquiv.surjective _).comp (esymmAlgHom_fin_surjective R hn)

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_3
n : ℕ
inst✝¹ : Fintype σ
inst✝ : CommRing R
hn : Fintype.card σ ≤ n
⊢ Function.Surjective ⇑(esymmAlgHom σ R n)

Tactic:
rw [← rename_esymmAlgHom (Fintype.equivFin σ).symm, AlgHom.coe_comp]

Result:
σ : Type u_1
R : Type u_3
n : ℕ
inst✝¹ : Fintype σ
inst✝ : CommRing R
hn : Fintype.card σ ≤ n
⊢ Function.Surjective
    (⇑↑(renameSymmetricSubalgebra (Fintype.equivFin σ).symm) ∘ ⇑(esymmAlgHom (Fin (Fintype.card σ)) R n))
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem norm_constOfIsEmpty [IsEmpty ι] (x : G) : ‖constOfIsEmpty 𝕜 E x‖ = ‖x‖

Proof state:
case a
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : IsEmpty ι
x✝ : G
x : (i : ι) → E i
⊢ ‖(constOfIsEmpty 𝕜 E x✝) x‖ ≤ ‖x✝‖ * ∏ i : ι, ‖x i‖

Tactic:
rw [Fintype.prod_empty, mul_one, constOfIsEmpty_apply]

Result:
no goals

Proof state:
case a
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : IsEmpty ι
x : G
⊢ ‖constOfIsEmpty 𝕜 E x‖ ≤ ‖x‖

Tactic:
refine opNorm_le_bound (norm_nonneg _) fun x => ?_

Result:
case a
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : IsEmpty ι
x✝ : G
x : (i : ι) → E i
⊢ ‖(constOfIsEmpty 𝕜 E x✝) x‖ ≤ ‖x✝‖ * ∏ i : ι, ‖x i‖

Proof state:
case a
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : IsEmpty ι
x : G
⊢ ‖x‖ ≤ ‖constOfIsEmpty 𝕜 E x‖

Tactic:
simpa using (constOfIsEmpty 𝕜 E x).le_opNorm 0

Result:
no goals

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : IsEmpty ι
x : G
⊢ ‖constOfIsEmpty 𝕜 E x‖ = ‖x‖

Tactic:
apply le_antisymm

Result:
case a
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : IsEmpty ι
x : G
⊢ ‖constOfIsEmpty 𝕜 E x‖ ≤ ‖x‖

case a
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : IsEmpty ι
x : G
⊢ ‖x‖ ≤ ‖constOfIsEmpty 𝕜 E x‖
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
@[simp]
lemma sumCoeffsExp_p_eq_one : ∑ i, a i * (b i) ^ p a b = 1

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ?m.361359 ∈ Set.range ?m.361358

α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ Type ?u.361355

α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ Sort ?u.361354

α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ?m.361357 → ?m.361356

α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ?m.361356

Tactic:
exact R.one_mem_range_sumCoeffsExp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∑ x : α, a x * b x ^ Function.invFun (fun p => ∑ i : α, a i * b i ^ p) 1 = 1

Tactic:
exact Function.invFun_eq (by rw [← Set.mem_range]; exact R.one_mem_range_sumCoeffsExp)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∃ a, ?m.360744 a = ?m.360745

Tactic:
rw [← Set.mem_range]

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ?m.361359 ∈ Set.range ?m.361358

α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ Type ?u.361355

α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ Sort ?u.361354

α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ?m.361357 → ?m.361356

α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ?m.361356

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∑ i : α, a i * b i ^ p a b = 1

Tactic:
simp only [p]

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∑ x : α, a x * b x ^ Function.invFun (fun p => ∑ i : α, a i * b i ^ p) 1 = 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem append_ne_nil_of_ne_nil_left {s : List α} (h : s ≠ []) (t : List α) : s ++ t ≠ []

Proof state:
α : Type u_1
s : List α
h : s ≠ []
t : List α
⊢ s ++ t ≠ []

Tactic:
simp_all

Result:
no goals
-- Mathlib/Data/Pi/Interval.lean
lemma card_Iio : #(Iio b) = ∏ i, #(Iic (b i)) - 1

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrderBot (α i)
b : (i : ι) → α i
⊢ #(Iio b) = ∏ i : ι, #(Iic (b i)) - 1

Tactic:
rw [card_Iio_eq_card_Iic_sub_one, card_Iic]

Result:
no goals
-- Mathlib/Topology/Connected/PathConnected.lean
theorem exists_path_through_family {n : ℕ} (p : Fin (n + 1) → X) :
    ∃ γ : Path (p 0) (p n), ∀ i, p i ∈ range γ

Proof state:
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
this : IsPathConnected univ
γ : Path (p 0) (p ↑n)
h : ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ
⊢ ∃ γ, ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ

Tactic:
exact ⟨γ, h⟩

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
⊢ PathConnectedSpace X

Tactic:
infer_instance

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
⊢ ∃ γ, ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ

Tactic:
have : IsPathConnected (univ : Set X) := pathConnectedSpace_iff_univ.mp (by infer_instance)

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
this : IsPathConnected univ
⊢ ∃ γ, ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
this : IsPathConnected univ
⊢ ∃ γ, ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ

Tactic:
rcases this.exists_path_through_family p fun _i => True.intro with ⟨γ, -, h⟩

Result:
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PathConnectedSpace X
n : ℕ
p : Fin (n + 1) → X
this : IsPathConnected univ
γ : Path (p 0) (p ↑n)
h : ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ
⊢ ∃ γ, ∀ (i : Fin (n + 1)), p i ∈ range ⇑γ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem Sublist.eraseP : l₁ <+ l₂ → l₁.eraseP p <+ l₂.eraseP p
  | .slnil => Sublist.refl _
  | .cons a s => by
    by_cases h : p a
    · simpa [h] using s.eraseP.trans (eraseP_sublist _)
    · simpa [h] using s.eraseP.cons _
  | .cons₂ a s => by
    by_cases h : p a
    · simpa [h] using s
    · simpa [h] using s.eraseP

Proof state:
case neg
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
l₁✝ l₂✝ : List α✝
a : α✝
s : l₁✝ <+ l₂✝
h : ¬p a = true
⊢ eraseP p (a :: l₁✝) <+ eraseP p (a :: l₂✝)

Tactic:
simpa [h] using s.eraseP

Result:
no goals

Proof state:
case pos
α✝ : Type u_1
l₁✝ l₂ : List α✝
p : α✝ → Bool
l₁ l₂✝ : List α✝
a : α✝
s : l₁ <+ l₂✝
h : p a = true
⊢ eraseP p l₁ <+ eraseP p (a :: l₂✝)

Tactic:
simpa [h] using s.eraseP.trans (eraseP_sublist _)

Result:
no goals

Proof state:
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
l₁✝ l₂✝ : List α✝
a : α✝
s : l₁✝ <+ l₂✝
⊢ eraseP p (a :: l₁✝) <+ eraseP p (a :: l₂✝)

Tactic:
by_cases h : p a

Result:
case pos
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
l₁✝ l₂✝ : List α✝
a : α✝
s : l₁✝ <+ l₂✝
h : p a = true
⊢ eraseP p (a :: l₁✝) <+ eraseP p (a :: l₂✝)

case neg
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
l₁✝ l₂✝ : List α✝
a : α✝
s : l₁✝ <+ l₂✝
h : ¬p a = true
⊢ eraseP p (a :: l₁✝) <+ eraseP p (a :: l₂✝)

Proof state:
α✝ : Type u_1
l₁✝ l₂ : List α✝
p : α✝ → Bool
l₁ l₂✝ : List α✝
a : α✝
s : l₁ <+ l₂✝
⊢ eraseP p l₁ <+ eraseP p (a :: l₂✝)

Tactic:
by_cases h : p a

Result:
case pos
α✝ : Type u_1
l₁✝ l₂ : List α✝
p : α✝ → Bool
l₁ l₂✝ : List α✝
a : α✝
s : l₁ <+ l₂✝
h : p a = true
⊢ eraseP p l₁ <+ eraseP p (a :: l₂✝)

case neg
α✝ : Type u_1
l₁✝ l₂ : List α✝
p : α✝ → Bool
l₁ l₂✝ : List α✝
a : α✝
s : l₁ <+ l₂✝
h : ¬p a = true
⊢ eraseP p l₁ <+ eraseP p (a :: l₂✝)

Proof state:
case neg
α✝ : Type u_1
l₁✝ l₂ : List α✝
p : α✝ → Bool
l₁ l₂✝ : List α✝
a : α✝
s : l₁ <+ l₂✝
h : ¬p a = true
⊢ eraseP p l₁ <+ eraseP p (a :: l₂✝)

Tactic:
simpa [h] using s.eraseP.cons _

Result:
no goals

Proof state:
case pos
α✝ : Type u_1
l₁ l₂ : List α✝
p : α✝ → Bool
l₁✝ l₂✝ : List α✝
a : α✝
s : l₁✝ <+ l₂✝
h : p a = true
⊢ eraseP p (a :: l₁✝) <+ eraseP p (a :: l₂✝)

Tactic:
simpa [h] using s

Result:
no goals