ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : AntilipschitzWith K f<VAR>ε : ℝ≥0∞<VAR>h₀ : 0 < ε<GOAL>∃ i, 0 < i ∧ Prod.map f f ⁻¹' {p | edist p.1 p.2 < i} ⊆ {p | edist p.1 p.2 < ε}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : AntilipschitzWith K f<VAR>ε : ℝ≥0∞<VAR>h₀ : 0 < ε<GOAL>Prod.map f f ⁻¹' {p | edist p.1 p.2 < (↑K)⁻¹ * ε} ⊆ {p | edist p.1 p.2 < ε}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : AntilipschitzWith K f<VAR>ε : ℝ≥0∞<VAR>h₀ : 0 < ε<VAR>x : α × α<VAR>hx : x ∈ Prod.map f f ⁻¹' {p | edist p.1 p.2 < (↑K)⁻¹ * ε}<GOAL>↑K * edist (f x.1) (f x.2) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : AntilipschitzWith K f<VAR>ε : ℝ≥0∞<VAR>h₀ : 0 < ε<VAR>x : α × α<VAR>hx : x ∈ Prod.map f f ⁻¹' {p | edist p.1 p.2 < ε / ↑K}<GOAL>↑K * edist (f x.1) (f x.2) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K : ℝ≥0<VAR>f : α → β<VAR>hf : AntilipschitzWith K f<VAR>ε : ℝ≥0∞<VAR>h₀ : 0 < ε<VAR>x : α × α<VAR>hx : x ∈ Prod.map f f ⁻¹' {p | edist p.1 p.2 < ε / ↑K}<GOAL>edist (f x.1) (f x.2) * ↑K < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>e : α ≃o β<VAR>a b : α<GOAL>⇑e '' Ico a b = Ico (e a) (e b)
<VAR>f : Char → Bool<VAR>x✝ : Substring<VAR>h✝ : x✝.Valid<VAR>w✝² w✝¹ w✝ : List Char<VAR>h : ValidFor w✝² w✝¹ w✝ x✝<GOAL>x✝.any f = x✝.toString.data.any f
<VAR>s : ℝ<VAR>hs : -1 ≤ s<VAR>hs' : s ≠ 0<VAR>p : ℝ<VAR>hp : 1 < p<GOAL>1 + p * s < (1 + s) ^ p
<VAR>s : ℝ<VAR>hs : -1 ≤ s<VAR>hs' : s ≠ 0<VAR>p : ℝ<VAR>hp : 1 < p<VAR>hp' : 0 < p<GOAL>1 + p * s < (1 + s) ^ p
<VAR>p : ℝ<VAR>hp : 1 < p<VAR>hp' : 0 < p<VAR>hs : -1 ≤ -1<VAR>hs' : -1 ≠ 0<GOAL>1 + p * -1 < (1 + -1) ^ p
<VAR>s : ℝ<VAR>hs✝ : -1 ≤ s<VAR>hs' : s ≠ 0<VAR>p : ℝ<VAR>hp : 1 < p<VAR>hp' : 0 < p<VAR>hs : -1 < s<GOAL>1 + p * s < (1 + s) ^ p
<VAR>s : ℝ<VAR>hs✝ : -1 ≤ s<VAR>hs' : s ≠ 0<VAR>p : ℝ<VAR>hp : 1 < p<VAR>hp' : 0 < p<VAR>hs : -1 < s<VAR>hs1 : 0 < 1 + s<GOAL>1 + p * s < (1 + s) ^ p
<VAR>s : ℝ<VAR>hs✝ : -1 ≤ s<VAR>hs' : s ≠ 0<VAR>p : ℝ<VAR>hp : 1 < p<VAR>hp' : 0 < p<VAR>hs : -1 < s<VAR>hs1 : 0 < 1 + s<VAR>hs2 : 1 + p * s ≤ 0<GOAL>1 + p * s < (1 + s) ^ p
<VAR>s : ℝ<VAR>hs✝ : -1 ≤ s<VAR>hs' : s ≠ 0<VAR>p : ℝ<VAR>hp : 1 < p<VAR>hp' : 0 < p<VAR>hs : -1 < s<VAR>hs1 : 0 < 1 + s<VAR>hs2 : 0 < 1 + p * s<GOAL>1 + p * s < (1 + s) ^ p
<VAR>s : ℝ<VAR>hs✝ : -1 ≤ s<VAR>hs' : s ≠ 0<VAR>p : ℝ<VAR>hp : 1 < p<VAR>hp' : 0 < p<VAR>hs : -1 < s<VAR>hs1 : 0 < 1 + s<VAR>hs2 : 0 < 1 + p * s<VAR>hs3 : 1 + s ≠ 1<GOAL>1 + p * s < (1 + s) ^ p
<VAR>s : ℝ<VAR>hs✝ : -1 ≤ s<VAR>hs' : s ≠ 0<VAR>p : ℝ<VAR>hp : 1 < p<VAR>hp' : 0 < p<VAR>hs : -1 < s<VAR>hs1 : 0 < 1 + s<VAR>hs2 : 0 < 1 + p * s<VAR>hs3 : 1 + s ≠ 1<VAR>hs4 : 1 + p * s ≠ 1<GOAL>1 + p * s < (1 + s) ^ p
<VAR>s : ℝ<VAR>hs✝ : -1 ≤ s<VAR>hs' : s ≠ 0<VAR>p : ℝ<VAR>hp : 1 < p<VAR>hp' : 0 < p<VAR>hs : -1 < s<VAR>hs1 : 0 < 1 + s<VAR>hs2 : 0 < 1 + p * s<VAR>hs3 : 1 + s ≠ 1<VAR>hs4 : 1 + p * s ≠ 1<GOAL>rexp (log (1 + p * s)) < rexp (log (1 + s) * p)
<VAR>s : ℝ<VAR>hs✝ : -1 ≤ s<VAR>hs' : s ≠ 0<VAR>p : ℝ<VAR>hp : 1 < p<VAR>hp' : 0 < p<VAR>hs : -1 < s<VAR>hs1 : 0 < 1 + s<VAR>hs2 : 0 < 1 + p * s<VAR>hs3 : 1 + s ≠ 1<VAR>hs4 : 1 + p * s ≠ 1<GOAL>log (1 + p * s) < log (1 + s) * p
<VAR>s : ℝ<VAR>hs✝ : -1 ≤ s<VAR>hs'✝ : s ≠ 0<VAR>p : ℝ<VAR>hp : 1 < p<VAR>hp' : 0 < p<VAR>hs : -1 < s<VAR>hs1 : 0 < 1 + s<VAR>hs2 : 0 < 1 + p * s<VAR>hs3 : 1 + s ≠ 1<VAR>hs4 : 1 + p * s ≠ 1<VAR>hs' : s < 0<GOAL>log (1 + p * s) < log (1 + s) * p
<VAR>s : ℝ<VAR>hs✝ : -1 ≤ s<VAR>hs'✝ : s ≠ 0<VAR>p : ℝ<VAR>hp : 1 < p<VAR>hp' : 0 < p<VAR>hs : -1 < s<VAR>hs1 : 0 < 1 + s<VAR>hs2 : 0 < 1 + p * s<VAR>hs3 : 1 + s ≠ 1<VAR>hs4 : 1 + p * s ≠ 1<VAR>hs' : s > 0<GOAL>log (1 + p * s) < log (1 + s) * p
<VAR>R : Type u<VAR>ι : Type v<VAR>inst✝³ : CommRing R<VAR>L : ι → Type w<VAR>inst✝² : (i : ι) → LieRing (L i)<VAR>inst✝¹ : (i : ι) → LieAlgebra R (L i)<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>x : L i<VAR>y : L j<GOAL>⁅(of L i) x, (of L j) y⁆ = if hij : i = j then (of L i) ⁅x, Eq.recOn ⋯ y⁆ else 0
<VAR>R : Type u<VAR>ι : Type v<VAR>inst✝³ : CommRing R<VAR>L : ι → Type w<VAR>inst✝² : (i : ι) → LieRing (L i)<VAR>inst✝¹ : (i : ι) → LieAlgebra R (L i)<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>x y : L i<GOAL>⁅(of L i) x, (of L i) y⁆ = if hij : i = i then (of L i) ⁅x, Eq.recOn ⋯ y⁆ else 0
<VAR>R : Type u<VAR>ι : Type v<VAR>inst✝³ : CommRing R<VAR>L : ι → Type w<VAR>inst✝² : (i : ι) → LieRing (L i)<VAR>inst✝¹ : (i : ι) → LieAlgebra R (L i)<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>x : L i<VAR>y : L j<VAR>hij : i ≠ j<GOAL>⁅(of L i) x, (of L j) y⁆ = if hij : i = j then (of L i) ⁅x, Eq.recOn ⋯ y⁆ else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝ t : Set α<VAR>a✝ b x✝ : α<VAR>f : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>x : Set α<VAR>hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))<VAR>y : Set β<VAR>a : α<GOAL>a ∈ x ∩ f ⁻¹' minimals s (f '' x ∩ y) ↔ a ∈ minimals r (x ∩ f ⁻¹' y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝ t : Set α<VAR>a✝ b x✝ : α<VAR>f : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>x : Set α<VAR>hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))<VAR>y : Set β<VAR>a : α<GOAL>(a ∈ x ∧ ((∃ x_1 ∈ x, f x_1 = f a) ∧ f a ∈ y) ∧ ∀ a_1 ∈ x, f a_1 ∈ y → s (f a_1) (f a) → s (f a) (f a_1)) ↔ (a ∈ x ∧ f a ∈ y) ∧ ∀ ⦃b : α⦄, b ∈ x → f b ∈ y → r b a → r a b
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>hurwitzZetaOdd (-a) s = -hurwitzZetaOdd a s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>γ✝ : Path x y<VAR>a b : X<VAR>γ : Path a b<VAR>t : ℝ<VAR>key : Continuous fun x => (t, x)<GOAL>Continuous ↿(γ.truncate t)
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x✝ y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>x : α<VAR>E : Set α<VAR>h : x ∉ closure E<GOAL>∃ ε, 0 < ε ∧ ENNReal.ofReal ε < infEdist x E
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x✝ y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>x : α<VAR>E : Set α<VAR>h : ∃ r, 0 ≤ r ∧ 0 < ENNReal.ofReal r ∧ ENNReal.ofReal r < infEdist x E<GOAL>∃ ε, 0 < ε ∧ ENNReal.ofReal ε < infEdist x E
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x✝ y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>x : α<VAR>E : Set α<VAR>ε : ℝ<VAR>left✝ : 0 ≤ ε<VAR>ε_pos : 0 < ENNReal.ofReal ε<VAR>ε_lt : ENNReal.ofReal ε < infEdist x E<GOAL>∃ ε, 0 < ε ∧ ENNReal.ofReal ε < infEdist x E
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>F✝ : LaxFunctor B C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F : LaxFunctor B C<VAR>G : LaxFunctor C D<VAR>a✝ b✝ c✝ : B<VAR>f✝ f'✝ : a✝ ⟶ b✝<VAR>η : f✝ ⟶ f'✝<VAR>g : b✝ ⟶ c✝<GOAL>(G.mapComp (F.map f✝) (F.map g) ≫ G.map₂ (F.mapComp f✝ g)) ≫ G.map₂ (F.map₂ (η ▷ g)) = G.map₂ (F.map₂ η) ▷ G.map (F.map g) ≫ G.mapComp (F.map f'✝) (F.map g) ≫ G.map₂ (F.mapComp f'✝ g)
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>F✝ : LaxFunctor B C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F : LaxFunctor B C<VAR>G : LaxFunctor C D<VAR>a✝ b✝ c✝ : B<VAR>f : a✝ ⟶ b✝<VAR>x✝¹ x✝ : b✝ ⟶ c✝<VAR>η : x✝¹ ⟶ x✝<GOAL>(G.mapComp (F.map f) (F.map x✝¹) ≫ G.map₂ (F.mapComp f x✝¹)) ≫ G.map₂ (F.map₂ (f ◁ η)) = G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x✝) ≫ G.map₂ (F.mapComp f x✝)
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>F✝ : LaxFunctor B C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F : LaxFunctor B C<VAR>G : LaxFunctor C D<VAR>a✝ b✝ c✝ d✝ : B<VAR>f : a✝ ⟶ b✝<VAR>g : b✝ ⟶ c✝<VAR>h : c✝ ⟶ d✝<GOAL>(G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.mapComp f g)) ▷ G.map (F.map h) ≫ (G.mapComp (F.map (f ≫ g)) (F.map h) ≫ G.map₂ (F.mapComp (f ≫ g) h)) ≫ G.map₂ (F.map₂ (α_ f g h).hom) = (α_ (G.map (F.map f)) (G.map (F.map g)) (G.map (F.map h))).hom ≫ G.map (F.map f) ◁ (G.mapComp (F.map g) (F.map h) ≫ G.map₂ (F.mapComp g h)) ≫ G.mapComp (F.map f) (F.map (g ≫ h)) ≫ G.map₂ (F.mapComp f (g ≫ h))
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>F✝ : LaxFunctor B C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F : LaxFunctor B C<VAR>G : LaxFunctor C D<VAR>a✝ b✝ c✝ d✝ : B<VAR>f : a✝ ⟶ b✝<VAR>g : b✝ ⟶ c✝<VAR>h : c✝ ⟶ d✝<GOAL>(G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.mapComp f g)) ▷ G.map (F.map h) ≫ (G.mapComp (F.map (f ≫ g)) (F.map h) ≫ G.map₂ (F.mapComp (f ≫ g) h)) ≫ G.map₂ (F.map₂ (α_ f g h).hom) = (G.mapComp (F.map f) (F.map g) ▷ G.map (F.map h) ≫ G.mapComp (F.map f ≫ F.map g) (F.map h) ≫ G.map₂ (α_ (F.map f) (F.map g) (F.map h)).hom ≫ G.map₂ (F.map f ◁ F.mapComp g h)) ≫ G.map₂ (F.mapComp f (g ≫ h))
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>F✝ : LaxFunctor B C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F : LaxFunctor B C<VAR>G : LaxFunctor C D<VAR>a✝ b✝ c✝ d✝ : B<VAR>f : a✝ ⟶ b✝<VAR>g : b✝ ⟶ c✝<VAR>h : c✝ ⟶ d✝<GOAL>(G.mapComp (F.map f) (F.map g) ≫ G.map₂ (F.mapComp f g)) ▷ G.map (F.map h) ≫ (G.mapComp (F.map (f ≫ g)) (F.map h) ≫ G.map₂ (F.mapComp (f ≫ g) h)) ≫ G.map₂ (F.map₂ (α_ f g h).hom) = G.mapComp (F.map f) (F.map g) ▷ G.map (F.map h) ≫ G.mapComp (F.map f ≫ F.map g) (F.map h) ≫ G.map₂ (F.mapComp f g ▷ F.map h) ≫ G.map₂ (F.mapComp (f ≫ g) h) ≫ G.map₂ (F.map₂ (α_ f g h).hom)
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>F✝ : LaxFunctor B C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F : LaxFunctor B C<VAR>G : LaxFunctor C D<VAR>a✝ b✝ c✝ d✝ : B<VAR>f : a✝ ⟶ b✝<VAR>g : b✝ ⟶ c✝<VAR>h : c✝ ⟶ d✝<GOAL>(G.mapComp (F.map f) (F.map g) ▷ G.map (F.map h) ≫ G.mapComp (F.map f ≫ F.map g) (F.map h) ≫ G.map₂ (F.mapComp f g ▷ F.map h) ≫ G.map₂ (F.mapComp (f ≫ g) h)) ≫ G.map₂ (F.map₂ (α_ f g h).hom) = G.mapComp (F.map f) (F.map g) ▷ G.map (F.map h) ≫ G.mapComp (F.map f ≫ F.map g) (F.map h) ≫ G.map₂ (F.mapComp f g ▷ F.map h) ≫ G.map₂ (F.mapComp (f ≫ g) h) ≫ G.map₂ (F.map₂ (α_ f g h).hom)
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>F✝ : LaxFunctor B C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F : LaxFunctor B C<VAR>G : LaxFunctor C D<VAR>a✝ b✝ : B<VAR>f : a✝ ⟶ b✝<GOAL>G.map₂ (F.map₂ (λ_ f).inv) = (λ_ (G.map (F.map f))).inv ≫ (G.mapId (F.obj a✝) ≫ G.map₂ (F.mapId a✝)) ▷ G.map (F.map f) ≫ G.mapComp (F.map (𝟙 a✝)) (F.map f) ≫ G.map₂ (F.mapComp (𝟙 a✝) f)
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>F✝ : LaxFunctor B C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F : LaxFunctor B C<VAR>G : LaxFunctor C D<VAR>a✝ b✝ : B<VAR>f : a✝ ⟶ b✝<GOAL>G.map₂ (F.map₂ (ρ_ f).inv) = (ρ_ (G.map (F.map f))).inv ≫ G.map (F.map f) ◁ (G.mapId (F.obj b✝) ≫ G.map₂ (F.mapId b✝)) ≫ G.mapComp (F.map f) (F.map (𝟙 b✝)) ≫ G.map₂ (F.mapComp f (𝟙 b✝))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : LocalRing R<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Nontrivial S<VAR>f : R →+* S<VAR>inst✝ : IsLocalRingHom f<VAR>hf : Function.Surjective ⇑f<VAR>a b : R<VAR>hab : IsUnit (f a + f b)<GOAL>IsUnit (f a) ∨ IsUnit (f b)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : LocalRing R<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Nontrivial S<VAR>f : R →+* S<VAR>inst✝ : IsLocalRingHom f<VAR>hf : Function.Surjective ⇑f<VAR>a b : R<VAR>hab : IsUnit (f (a + b))<GOAL>IsUnit (f a) ∨ IsUnit (f b)
<VAR>E : Type uE<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>inst✝¹ : T2Space M<VAR>inst✝ : SmoothManifoldWithCorners I M<GOAL>Smooth I 𝓘(ℝ, ℝ) ↑f
<VAR>E : Type uE<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x✝ : M<VAR>inst✝¹ : T2Space M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>x : M<VAR>hx : x ∈ tsupport ↑f<GOAL>ContMDiffAt I 𝓘(ℝ, ℝ) ⊤ (↑f) x
<VAR>E : Type uE<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x✝ : M<VAR>inst✝¹ : T2Space M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>x : M<VAR>hx : x ∈ tsupport ↑f<VAR>this : x ∈ (chartAt H c).source<GOAL>ContMDiffAt I 𝓘(ℝ, ℝ) ⊤ (↑f) x
<VAR>E : Type uE<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace H M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x✝ : M<VAR>inst✝¹ : T2Space M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>x : M<VAR>hx : x ∈ tsupport ↑f<VAR>this : x ∈ (chartAt H c).source<GOAL>ContMDiffAt I 𝓘(ℝ, ℝ) ⊤ (↑f.toContDiffBump ∘ ↑(extChartAt I c)) x
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hPz : P z = 0<GOAL>W'.addXYZ P Q = (P x * Q z) • Q
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>a < 1 / b ↔ b < 1 / a
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₃ : Type u_9<VAR>V : Type u_10<VAR>V₂ : Type u_11<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring R₂<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R₂ M₂<VAR>p✝ p'✝ : Submodule R M<VAR>q : Submodule R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_12<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>p p' : Submodule R M<VAR>h : p ≤ p'<GOAL>ker (inclusion h) = ⊥
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>A B : Cᵒᵖ<VAR>g : A ⟶ B<GOAL>(imageUnopOp g).hom ≫ image.ι g = (factorThruImage g.unop).op
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j k : ι<VAR>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>inst✝¹ : K.HasHomology j<VAR>inst✝ : (K.sc' i j k).HasHomology<GOAL>K.pOpcycles j ≫ ShortComplex.opcyclesMap ((natIsoSc' C c i j k hi hk).hom.app K) = (K.sc' i j k).pOpcycles
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j k : ι<VAR>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>inst✝¹ : K.HasHomology j<VAR>inst✝ : (K.sc' i j k).HasHomology<GOAL>((natIsoSc' C c i j k hi hk).hom.app K).τ₂ ≫ (K.sc' i j k).pOpcycles = (K.sc' i j k).pOpcycles
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x y : α<VAR>inst✝² : DecidableRel f✝.SameCycle<VAR>inst✝¹ : DecidableRel g.SameCycle<VAR>f : Perm α<VAR>inst✝ : DecidableRel f.SameCycle<VAR>hx : f x ≠ x<GOAL>(f.cycleOf x) x ≠ x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x y✝ : α<VAR>inst✝² : DecidableRel f✝.SameCycle<VAR>inst✝¹ : DecidableRel g.SameCycle<VAR>f : Perm α<VAR>inst✝ : DecidableRel f.SameCycle<VAR>hx : f x ≠ x<VAR>this : (f.cycleOf x) x ≠ x<VAR>y : α<VAR>h : (f.cycleOf x) y ≠ y<VAR>hxy : f.SameCycle x y<VAR>i : ℤ<VAR>hi : (f ^ i) x = y<GOAL>(f.cycleOf x ^ i) x = y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x y✝ : α<VAR>inst✝² : DecidableRel f✝.SameCycle<VAR>inst✝¹ : DecidableRel g.SameCycle<VAR>f : Perm α<VAR>inst✝ : DecidableRel f.SameCycle<VAR>hx : f x ≠ x<VAR>this : (f.cycleOf x) x ≠ x<VAR>y : α<VAR>h : (f.cycleOf x) y ≠ y<VAR>hxy : ¬f.SameCycle x y<GOAL>(f.cycleOf x).SameCycle x y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x y✝ : α<VAR>inst✝² : DecidableRel f✝.SameCycle<VAR>inst✝¹ : DecidableRel g.SameCycle<VAR>f : Perm α<VAR>inst✝ : DecidableRel f.SameCycle<VAR>hx : f x ≠ x<VAR>this : (f.cycleOf x) x ≠ x<VAR>y : α<VAR>h : y ≠ y<VAR>hxy : ¬f.SameCycle x y<GOAL>(f.cycleOf x).SameCycle x y
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<GOAL>LinearMap.rTensor (Module.Dual K V) (contractLeft K V) ∘ₗ ↑(TensorProduct.assoc K (Module.Dual K V) V (Module.Dual K V)).symm ∘ₗ LinearMap.lTensor (Module.Dual K V) (coevaluation K V) = ↑(TensorProduct.lid K (Module.Dual K V)).symm ∘ₗ ↑(TensorProduct.rid K (Module.Dual K V))
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<GOAL>(mk K (Module.Dual K V) K).compr₂ (LinearMap.rTensor (Module.Dual K V) (contractLeft K V) ∘ₗ ↑(TensorProduct.assoc K (Module.Dual K V) V (Module.Dual K V)).symm ∘ₗ LinearMap.lTensor (Module.Dual K V) (coevaluation K V)) = (mk K (Module.Dual K V) K).compr₂ (↑(TensorProduct.lid K (Module.Dual K V)).symm ∘ₗ ↑(TensorProduct.rid K (Module.Dual K V)))
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<GOAL>∀ (i : ↑(Basis.ofVectorSpaceIndex K V)), ((mk K (Module.Dual K V) K).compr₂ (LinearMap.rTensor (Module.Dual K V) (contractLeft K V) ∘ₗ ↑(TensorProduct.assoc K (Module.Dual K V) V (Module.Dual K V)).symm ∘ₗ LinearMap.lTensor (Module.Dual K V) (coevaluation K V))) ((Basis.ofVectorSpace K V).dualBasis i) = ((mk K (Module.Dual K V) K).compr₂ (↑(TensorProduct.lid K (Module.Dual K V)).symm ∘ₗ ↑(TensorProduct.rid K (Module.Dual K V)))) ((Basis.ofVectorSpace K V).dualBasis i)
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<VAR>j : ↑(Basis.ofVectorSpaceIndex K V)<GOAL>((mk K (Module.Dual K V) K).compr₂ (LinearMap.rTensor (Module.Dual K V) (contractLeft K V) ∘ₗ ↑(TensorProduct.assoc K (Module.Dual K V) V (Module.Dual K V)).symm ∘ₗ LinearMap.lTensor (Module.Dual K V) (coevaluation K V))) ((Basis.ofVectorSpace K V).dualBasis j) = ((mk K (Module.Dual K V) K).compr₂ (↑(TensorProduct.lid K (Module.Dual K V)).symm ∘ₗ ↑(TensorProduct.rid K (Module.Dual K V)))) ((Basis.ofVectorSpace K V).dualBasis j)
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<VAR>j : ↑(Basis.ofVectorSpaceIndex K V)<GOAL>(((mk K (Module.Dual K V) K).compr₂ (LinearMap.rTensor (Module.Dual K V) (contractLeft K V) ∘ₗ ↑(TensorProduct.assoc K (Module.Dual K V) V (Module.Dual K V)).symm ∘ₗ LinearMap.lTensor (Module.Dual K V) (coevaluation K V))) ((Basis.ofVectorSpace K V).dualBasis j)) 1 = (((mk K (Module.Dual K V) K).compr₂ (↑(TensorProduct.lid K (Module.Dual K V)).symm ∘ₗ ↑(TensorProduct.rid K (Module.Dual K V)))) ((Basis.ofVectorSpace K V).dualBasis j)) 1
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<VAR>j : ↑(Basis.ofVectorSpaceIndex K V)<GOAL>(LinearMap.rTensor (Module.Dual K V) (contractLeft K V) ∘ₗ ↑(TensorProduct.assoc K (Module.Dual K V) V (Module.Dual K V)).symm ∘ₗ LinearMap.lTensor (Module.Dual K V) (coevaluation K V)) ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] 1) = (↑(TensorProduct.lid K (Module.Dual K V)).symm ∘ₗ ↑(TensorProduct.rid K (Module.Dual K V))) ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] 1)
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<VAR>j : ↑(Basis.ofVectorSpaceIndex K V)<GOAL>(LinearMap.rTensor (Module.Dual K V) (contractLeft K V)) ((TensorProduct.assoc K (Module.Dual K V) V (Module.Dual K V)).symm ((LinearMap.lTensor (Module.Dual K V) (coevaluation K V)) ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] 1))) = (TensorProduct.lid K (Module.Dual K V)).symm ((TensorProduct.rid K (Module.Dual K V)) ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] 1))
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<VAR>j : ↑(Basis.ofVectorSpaceIndex K V)<GOAL>(LinearMap.rTensor (Module.Dual K V) (contractLeft K V)) ((TensorProduct.assoc K (Module.Dual K V) V (Module.Dual K V)).symm ((LinearMap.lTensor (Module.Dual K V) (coevaluation K V)) ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] 1))) = 1 ⊗ₜ[K] (Basis.ofVectorSpace K V).dualBasis j
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<VAR>j : ↑(Basis.ofVectorSpaceIndex K V)<GOAL>(LinearMap.rTensor (Module.Dual K V) (contractLeft K V)) ((TensorProduct.assoc K (Module.Dual K V) V (Module.Dual K V)).symm ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] ∑ i : ↑(Basis.ofVectorSpaceIndex K V), (Basis.ofVectorSpace K V) i ⊗ₜ[K] (Basis.ofVectorSpace K V).coord i)) = 1 ⊗ₜ[K] (Basis.ofVectorSpace K V).dualBasis j
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<VAR>j : ↑(Basis.ofVectorSpaceIndex K V)<GOAL>(LinearMap.rTensor (Module.Dual K V) (contractLeft K V)) (∑ x : ↑(Basis.ofVectorSpaceIndex K V), (TensorProduct.assoc K (Module.Dual K V) V (Module.Dual K V)).symm ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] (Basis.ofVectorSpace K V) x ⊗ₜ[K] (Basis.ofVectorSpace K V).coord x)) = 1 ⊗ₜ[K] (Basis.ofVectorSpace K V).dualBasis j