ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>B : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>inst✝³ : HasCoproduct X<VAR>inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)<VAR>inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a => pullback g (Sigma.ι X a)<VAR>inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a => pullback.fst g (Sigma.ι X a))<VAR>W : C<VAR>e : (a : α) → X a ⟶ W<VAR>h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂<VAR>Z : C<VAR>g₁ g₂ : Z ⟶ ∐ fun b => X b<VAR>hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π<VAR>a b : α<GOAL>pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a) ≫ e a = pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.fst g₁ (Sigma.ι X a) ≫ g₂ ≫ Sigma.desc e
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>B : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>inst✝³ : HasCoproduct X<VAR>inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)<VAR>inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a => pullback g (Sigma.ι X a)<VAR>inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a => pullback.fst g (Sigma.ι X a))<VAR>W : C<VAR>e : (a : α) → X a ⟶ W<VAR>h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂<VAR>Z : C<VAR>g₁ g₂ : Z ⟶ ∐ fun b => X b<VAR>hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π<VAR>a b : α<GOAL>(pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ e a = ((pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.fst g₁ (Sigma.ι X a)) ≫ g₂) ≫ Sigma.desc e
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>B : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>inst✝³ : HasCoproduct X<VAR>inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)<VAR>inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a => pullback g (Sigma.ι X a)<VAR>inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a => pullback.fst g (Sigma.ι X a))<VAR>W : C<VAR>e : (a : α) → X a ⟶ W<VAR>h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂<VAR>Z : C<VAR>g₁ g₂ : Z ⟶ ∐ fun b => X b<VAR>hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π<VAR>a b : α<GOAL>(pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ e a = (pullback.snd (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ Sigma.ι X b) ≫ Sigma.desc e
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>B : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>inst✝³ : HasCoproduct X<VAR>inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)<VAR>inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a => pullback g (Sigma.ι X a)<VAR>inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a => pullback.fst g (Sigma.ι X a))<VAR>W : C<VAR>e : (a : α) → X a ⟶ W<VAR>h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂<VAR>Z : C<VAR>g₁ g₂ : Z ⟶ ∐ fun b => X b<VAR>hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π<VAR>a b : α<GOAL>pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a) ≫ e a = pullback.snd (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ e b
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>B : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>inst✝³ : HasCoproduct X<VAR>inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)<VAR>inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a => pullback g (Sigma.ι X a)<VAR>inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a => pullback.fst g (Sigma.ι X a))<VAR>W : C<VAR>e : (a : α) → X a ⟶ W<VAR>h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂<VAR>Z : C<VAR>g₁ g₂ : Z ⟶ ∐ fun b => X b<VAR>hg : g₁ ≫ Sigma.desc π = g₂ ≫ Sigma.desc π<VAR>a b : α<GOAL>(pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ e a = pullback.snd (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ e b
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>B : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>inst✝³ : HasCoproduct X<VAR>inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)<VAR>inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a => pullback g (Sigma.ι X a)<VAR>inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a => pullback.fst g (Sigma.ι X a))<VAR>W : C<VAR>e : (a : α) → X a ⟶ W<VAR>h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂<VAR>Z : C<VAR>g₁ g₂ : Z ⟶ ∐ fun b => X b<VAR>a b : α<VAR>hg : pullback.fst g₁ (Sigma.ι X a) ≫ g₁ ≫ Sigma.desc π = pullback.fst g₁ (Sigma.ι X a) ≫ g₂ ≫ Sigma.desc π<GOAL>(pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ π a = pullback.snd (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ π b
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>B : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>inst✝³ : HasCoproduct X<VAR>inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)<VAR>inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a => pullback g (Sigma.ι X a)<VAR>inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a => pullback.fst g (Sigma.ι X a))<VAR>W : C<VAR>e : (a : α) → X a ⟶ W<VAR>h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂<VAR>Z : C<VAR>g₁ g₂ : Z ⟶ ∐ fun b => X b<VAR>a b : α<VAR>hg : (pullback.snd g₁ (Sigma.ι X a) ≫ Sigma.ι X a) ≫ Sigma.desc π = pullback.fst g₁ (Sigma.ι X a) ≫ g₂ ≫ Sigma.desc π<GOAL>(pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ π a = pullback.snd (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ π b
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>B : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>inst✝³ : HasCoproduct X<VAR>inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)<VAR>inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a => pullback g (Sigma.ι X a)<VAR>inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a => pullback.fst g (Sigma.ι X a))<VAR>W : C<VAR>e : (a : α) → X a ⟶ W<VAR>h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂<VAR>Z : C<VAR>g₁ g₂ : Z ⟶ ∐ fun b => X b<VAR>a b : α<VAR>hg : pullback.snd g₁ (Sigma.ι X a) ≫ π a = pullback.fst g₁ (Sigma.ι X a) ≫ g₂ ≫ Sigma.desc π<GOAL>(pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ π a = pullback.snd (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ π b
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>B : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>inst✝³ : HasCoproduct X<VAR>inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)<VAR>inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a => pullback g (Sigma.ι X a)<VAR>inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a => pullback.fst g (Sigma.ι X a))<VAR>W : C<VAR>e : (a : α) → X a ⟶ W<VAR>h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂<VAR>Z : C<VAR>g₁ g₂ : Z ⟶ ∐ fun b => X b<VAR>a b : α<VAR>hg : Sigma.ι (fun a_1 => pullback (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X a_1)) b ≫ (Sigma.desc fun a_1 => pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X a_1)) ≫ pullback.snd g₁ (Sigma.ι X a) ≫ π a = Sigma.ι (fun a_1 => pullback (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X a_1)) b ≫ (Sigma.desc fun a_1 => pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X a_1)) ≫ pullback.fst g₁ (Sigma.ι X a) ≫ g₂ ≫ Sigma.desc π<GOAL>(pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ π a = pullback.snd (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ π b
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>B : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>inst✝³ : HasCoproduct X<VAR>inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)<VAR>inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a => pullback g (Sigma.ι X a)<VAR>inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a => pullback.fst g (Sigma.ι X a))<VAR>W : C<VAR>e : (a : α) → X a ⟶ W<VAR>h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂<VAR>Z : C<VAR>g₁ g₂ : Z ⟶ ∐ fun b => X b<VAR>a b : α<VAR>hg : pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a) ≫ π a = pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.fst g₁ (Sigma.ι X a) ≫ g₂ ≫ Sigma.desc π<GOAL>(pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ π a = pullback.snd (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ π b
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>B : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>inst✝³ : HasCoproduct X<VAR>inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)<VAR>inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a => pullback g (Sigma.ι X a)<VAR>inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a => pullback.fst g (Sigma.ι X a))<VAR>W : C<VAR>e : (a : α) → X a ⟶ W<VAR>h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂<VAR>Z : C<VAR>g₁ g₂ : Z ⟶ ∐ fun b => X b<VAR>a b : α<VAR>hg : (pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ π a = ((pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.fst g₁ (Sigma.ι X a)) ≫ g₂) ≫ Sigma.desc π<GOAL>(pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ π a = pullback.snd (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ π b
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>B : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>inst✝³ : HasCoproduct X<VAR>inst✝² : ∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), HasPullback g (Sigma.ι X a)<VAR>inst✝¹ : ∀ {Z : C} (g : Z ⟶ ∐ X), HasCoproduct fun a => pullback g (Sigma.ι X a)<VAR>inst✝ : ∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Sigma.desc fun a => pullback.fst g (Sigma.ι X a))<VAR>W : C<VAR>e : (a : α) → X a ⟶ W<VAR>h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ = g₂ ≫ π a₂ → g₁ ≫ e a₁ = g₂ ≫ e a₂<VAR>Z : C<VAR>g₁ g₂ : Z ⟶ ∐ fun b => X b<VAR>a b : α<VAR>hg : (pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ π a = (pullback.snd (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ Sigma.ι X b) ≫ Sigma.desc π<GOAL>(pullback.fst (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ pullback.snd g₁ (Sigma.ι X a)) ≫ π a = pullback.snd (pullback.fst g₁ (Sigma.ι X a) ≫ g₂) (Sigma.ι X b) ≫ π b
<VAR>z τ : ℂ<GOAL>jacobiTheta₂' (-z) τ = -jacobiTheta₂' z τ
<VAR>z τ : ℂ<GOAL>∑' (c : ℤ), jacobiTheta₂'_term ((Equiv.neg ℤ) c) (-z) τ = ∑' (b : ℤ), -jacobiTheta₂'_term b z τ
<VAR>z τ : ℂ<VAR>n : ℤ<GOAL>2 * ↑π * I * ↑((Equiv.neg ℤ) n) * cexp (2 * ↑π * I * ↑((Equiv.neg ℤ) n) * -z + ↑π * I * ↑((Equiv.neg ℤ) n) ^ 2 * τ) = -(2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ))
<VAR>z τ : ℂ<VAR>n : ℤ<GOAL>2 * ↑π * I * ↑(-n) * cexp (2 * ↑π * I * ↑(-n) * -z + ↑π * I * ↑(-n) ^ 2 * τ) = -(2 * ↑π * I * ↑n) * cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>R : Type u_6<VAR>inst✝² : NormedDivisionRing R<VAR>inst✝¹ : NormedAlgebra 𝕜 R<VAR>inst✝ : CompleteSpace R<VAR>x : R<VAR>hx : x ≠ 0<GOAL>HasFDerivAt Inv.inv (-((mulLeftRight 𝕜 R) x⁻¹) x⁻¹) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>k : ℕ<VAR>h : s.encard ≤ ↑k<GOAL>s.Finite
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>k : ℕ<VAR>h : s.encard ≤ ↑k<GOAL>s.encard < ⊤
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<VAR>z₁ z₂ : SecondObj P S<VAR>h : ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f), Pi.π (fun f => P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ z₁ = Pi.π (fun f => P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ z₂<GOAL>z₁ = z₂
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type (max v u)<VAR>X : C<VAR>R : Presieve X<VAR>S : Sieve X<VAR>z₁ z₂ : SecondObj P S<VAR>h : ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f), Pi.π (fun f => P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ z₁ = Pi.π (fun f => P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩ z₂<GOAL>∀ (j : Discrete ((Y : C) × (Z : C) × (_ : Z ⟶ Y) × { f' // S.arrows f' })), limit.π (Discrete.functor fun f => P.obj (op f.snd.fst)) j z₁ = limit.π (Discrete.functor fun f => P.obj (op f.snd.fst)) j z₂
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α✝ : Type u_3<VAR>β✝ : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α✝<VAR>a : α✝<VAR>f✝ g : α✝ → β✝<VAR>α : Type u_6<VAR>β : Type u_7<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : Unique α<VAR>s : Finset α<VAR>f : α → β<VAR>h : s.Nonempty<GOAL>∏ x ∈ s, f x = f default
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : TopologicalSpace R<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : ContinuousAdd M<VAR>inst✝² : Module R M<VAR>inst✝¹ : ContinuousSMul R M<VAR>inst✝ : (𝓝[{x | IsUnit x}] 0).NeBot<VAR>s : Submodule R M<VAR>y : M<VAR>hy : y ∈ interior ↑s<GOAL>s = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : TopologicalSpace R<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : ContinuousAdd M<VAR>inst✝² : Module R M<VAR>inst✝¹ : ContinuousSMul R M<VAR>inst✝ : (𝓝[{x | IsUnit x}] 0).NeBot<VAR>s : Submodule R M<VAR>y : M<VAR>hy : y ∈ interior ↑s<VAR>x : M<GOAL>x ∈ s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : TopologicalSpace R<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : ContinuousAdd M<VAR>inst✝² : Module R M<VAR>inst✝¹ : ContinuousSMul R M<VAR>inst✝ : (𝓝[{x | IsUnit x}] 0).NeBot<VAR>s : Submodule R M<VAR>y : M<VAR>hy : ↑s ∈ 𝓝 y<VAR>x : M<GOAL>x ∈ s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : TopologicalSpace R<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : ContinuousAdd M<VAR>inst✝² : Module R M<VAR>inst✝¹ : ContinuousSMul R M<VAR>inst✝ : (𝓝[{x | IsUnit x}] 0).NeBot<VAR>s : Submodule R M<VAR>y : M<VAR>hy : ↑s ∈ 𝓝 y<VAR>x : M<VAR>this : Tendsto (fun c => y + c • x) (𝓝[{x | IsUnit x}] 0) (𝓝 (y + 0 • x))<GOAL>x ∈ s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : TopologicalSpace R<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : ContinuousAdd M<VAR>inst✝² : Module R M<VAR>inst✝¹ : ContinuousSMul R M<VAR>inst✝ : (𝓝[{x | IsUnit x}] 0).NeBot<VAR>s : Submodule R M<VAR>y : M<VAR>hy : ↑s ∈ 𝓝 y<VAR>x : M<VAR>this : Tendsto (fun c => y + c • x) (𝓝[{x | IsUnit x}] 0) (𝓝 y)<GOAL>x ∈ s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : TopologicalSpace R<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : ContinuousAdd M<VAR>inst✝² : Module R M<VAR>inst✝¹ : ContinuousSMul R M<VAR>inst✝ : (𝓝[{x | IsUnit x}] 0).NeBot<VAR>s : Submodule R M<VAR>y : M<VAR>hy : ↑s ∈ 𝓝 y<VAR>x : M<VAR>this : Tendsto (fun c => y + c • x) (𝓝[{x | IsUnit x}] 0) (𝓝 y)<VAR>u : Rˣ<VAR>hu : y + ↑u • x ∈ s<GOAL>x ∈ s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : TopologicalSpace R<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : ContinuousAdd M<VAR>inst✝² : Module R M<VAR>inst✝¹ : ContinuousSMul R M<VAR>inst✝ : (𝓝[{x | IsUnit x}] 0).NeBot<VAR>s : Submodule R M<VAR>y : M<VAR>hy : ↑s ∈ 𝓝 y<VAR>x : M<VAR>this : Tendsto (fun c => y + c • x) (𝓝[{x | IsUnit x}] 0) (𝓝 y)<VAR>u : Rˣ<VAR>hu : y + ↑u • x ∈ s<VAR>hy' : y ∈ s<GOAL>x ∈ s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Monoid α<VAR>inst✝ : Monoid β<VAR>x : α × β<VAR>a : α<VAR>b : β<GOAL>IsOfFinOrder a → IsOfFinOrder b → IsOfFinOrder (a, b)
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>h : 0 ∈ S<VAR>a b : LocalizedModule S M<GOAL>a = b
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>h : 0 ∈ S<VAR>m✝ m'✝ : M<VAR>s✝ s'✝ : ↥S<GOAL>mk m✝ s✝ = mk m'✝ s'✝
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<VAR>n : ℕ<GOAL>term (f - g) s n = term f s n - term g s n
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>x y : α<VAR>q : ℚ≥0<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>0 ≤ q • a
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>x y : α<VAR>q : ℚ≥0<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>0 ≤ ↑q * a
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x✝ x' : G<VAR>y y' : E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝² : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : AddGroup G<VAR>x : G<VAR>hfg : ConvolutionExistsAt f g x L μ<VAR>hfg' : ConvolutionExistsAt f' g x L μ<GOAL>((f + f') ⋆[L, μ] g) x = (f ⋆[L, μ] g) x + (f' ⋆[L, μ] g) x
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝³ : Category.{max v u, w} D<VAR>inst✝² : ConcreteCategory D<VAR>inst✝¹ : PreservesLimits (forget D)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>inst✝ : HasMultiequalizer (S.index P)<VAR>x : Meq P S<VAR>I : S.Arrow<GOAL>(Multiequalizer.ι (S.index P) I) ((equiv P S).symm x) = ↑x I
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝³ : Category.{max v u, w} D<VAR>inst✝² : ConcreteCategory D<VAR>inst✝¹ : PreservesLimits (forget D)<VAR>X : C<VAR>P : Cᵒᵖ ⥤ D<VAR>S : J.Cover X<VAR>inst✝ : HasMultiequalizer (S.index P)<VAR>x : Meq P S<VAR>I : S.Arrow<GOAL>↑((equiv P S) ((equiv P S).symm x)) I = ↑x I
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : OrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>v : 𝕜<VAR>q : E<VAR>hf : StrictConvexOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 < w i<VAR>h₁ : ∑ i ∈ t, w i = 1<VAR>hmem : ∀ i ∈ t, p i ∈ s<VAR>hp : ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k<GOAL>f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i)
<VAR>M : Type u_1<VAR>inst✝ : Monoid M<VAR>x : M<VAR>n : ℕ<VAR>hn : x ^ n = 1<VAR>m : ℕ<VAR>hm : x ^ (m + 1) = 1<GOAL>x ^ (m + 1).gcd n = 1
<VAR>M : Type u_1<VAR>inst✝ : Monoid M<VAR>n m : ℕ<VAR>y : Mˣ<VAR>hn : ↑y ^ n = 1<VAR>hm : ↑y ^ (m + 1) = 1<GOAL>↑y ^ (m + 1).gcd n = 1
<VAR>M : Type u_1<VAR>inst✝ : Monoid M<VAR>n m : ℕ<VAR>y : Mˣ<VAR>hn : y ^ ↑n = 1<VAR>hm : y ^ ↑(m + 1) = 1<GOAL>y ^ ↑((m + 1).gcd n) = 1
<VAR>M : Type u_1<VAR>N✝ : Type u_2<VAR>P : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Mul M<VAR>inst✝² : Mul N✝<VAR>inst✝¹ : Mul P<VAR>S : Subsemigroup M<VAR>N : Type u_5<VAR>inst✝ : Mul N<VAR>f : M →ₙ* N<GOAL>↑f.srange = ↑⊤ ↔ Set.range ⇑f = Set.univ
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>X✝ : Type u<GOAL>{ obj := fun X => of R (X →₀ R), map := fun {X Y} f => Finsupp.lmapDomain R R f }.map (𝟙 X✝) = 𝟙 ({ obj := fun X => of R (X →₀ R), map := fun {X Y} f => Finsupp.lmapDomain R R f }.obj X✝)
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>X✝ Y✝ Z✝ : Type u<VAR>f✝ : X✝ ⟶ Y✝<VAR>g✝ : Y✝ ⟶ Z✝<GOAL>{ obj := fun X => of R (X →₀ R), map := fun {X Y} f => Finsupp.lmapDomain R R f }.map (f✝ ≫ g✝) = { obj := fun X => of R (X →₀ R), map := fun {X Y} f => Finsupp.lmapDomain R R f }.map f✝ ≫ { obj := fun X => of R (X →₀ R), map := fun {X Y} f => Finsupp.lmapDomain R R f }.map g✝
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>L : IntermediateField F E<VAR>h : IsPurelyInseparable F ↥L<GOAL>L ≤ perfectClosure F E
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>L : IntermediateField F E<VAR>h : ∀ (x : ↥L), ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F ↥L).range<GOAL>L ≤ perfectClosure F E
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle y (y - x)).sin = ‖x‖ / ‖y - x‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<VAR>hs : (o.oangle y (y - x)).sign = 1<GOAL>(o.oangle y (y - x)).sin = ‖x‖ / ‖y - x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y z : E<VAR>δ ε : ℝ<VAR>hδ : 0 < δ<VAR>s : Set E<GOAL>closure (thickening δ s) = cthickening δ s
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i j : ι<VAR>p : B × F<GOAL>p ∈ (Z.trivChange i j).source ↔ p.1 ∈ Z.baseSet i ∩ Z.baseSet j
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i j : ι<VAR>p : B × F<GOAL>p.1 ∈ Z.baseSet i ∩ Z.baseSet j ∧ p.2 ∈ univ ↔ p.1 ∈ Z.baseSet i ∩ Z.baseSet j
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E'<VAR>inst✝³ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝² : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝¹ : TopologicalSpace M'<VAR>inst✝ : ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<GOAL>MDifferentiableAt I I' f x ↔ ContinuousAt f x ∧ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I' x f) (range ↑I) (↑(extChartAt I x) x)