ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>f : G' →* G<VAR>hf : Function.Surjective ⇑f<VAR>this✝ : Setoid G := QuotientGroup.leftRel H<VAR>this : Setoid G' := QuotientGroup.leftRel (comap f H)<VAR>key : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (f x) (f y)<GOAL>(comap f H).index = H.index
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>f : G' →* G<VAR>hf : Function.Surjective ⇑f<VAR>this✝ : Setoid G := QuotientGroup.leftRel H<VAR>this : Setoid G' := QuotientGroup.leftRel (comap f H)<VAR>key : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (f x) (f y)<GOAL>Function.Injective (Quotient.map' ⇑f ⋯)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>f : G' →* G<VAR>hf : Function.Surjective ⇑f<VAR>this✝ : Setoid G := QuotientGroup.leftRel H<VAR>this : Setoid G' := QuotientGroup.leftRel (comap f H)<VAR>key : ∀ (x y : G'), Setoid.r x y ↔ Setoid.r (f x) (f y)<GOAL>Function.Surjective (Quotient.map' ⇑f ⋯)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f✝ f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>f : M → M'<GOAL>LiftPropWithinAt P f s x ↔ ContinuousWithinAt f s x ∧ P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) ((chartAt H x).target ∩ ↑(chartAt H x).symm ⁻¹' (s ∩ f ⁻¹' (chartAt H' (f x)).source)) (↑(chartAt H x) x)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f✝ f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>f : M → M'<GOAL>ContinuousWithinAt f s x ∧ P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x) ↔ ContinuousWithinAt f s x ∧ P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) ((chartAt H x).target ∩ ↑(chartAt H x).symm ⁻¹' (s ∩ f ⁻¹' (chartAt H' (f x)).source)) (↑(chartAt H x) x)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f✝ f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>f : M → M'<VAR>hf : ContinuousWithinAt f s x<GOAL>↑(chartAt H x).symm ⁻¹' s =ᶠ[𝓝 (↑(chartAt H x) x)] (chartAt H x).target ∩ ↑(chartAt H x).symm ⁻¹' (s ∩ f ⁻¹' (chartAt H' (f x)).source)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R✝ : ℝ<VAR>z✝ w✝ : ℂ<VAR>R : ℝ<VAR>hR : 0 < R<VAR>f : ℂ → E<VAR>z w : ℂ<VAR>hf : ContinuousOn f (sphere z R)<VAR>hw : w ∈ ball z R<GOAL>Continuous (circleTransformDeriv R z w f)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R✝ : ℝ<VAR>z✝ w✝ : ℂ<VAR>R : ℝ<VAR>hR : 0 < R<VAR>f : ℂ → E<VAR>z w : ℂ<VAR>hf : ContinuousOn f (sphere z R)<VAR>hw : w ∈ ball z R<GOAL>Continuous fun θ => (circleMap z R θ - w)⁻¹ • circleTransform R z w f θ
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>x_ne_zero : x ≠ 0<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 (fun x => x⁻¹) s x = smulRight 1 (-(x ^ 2)⁻¹)
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>x_ne_zero : x ≠ 0<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderiv 𝕜 (fun x => x⁻¹) x = smulRight 1 (-(x ^ 2)⁻¹)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<GOAL>((HomologicalComplex.cyclesIsoSc' (inhomogeneousCochains A) 1 2 3 isoTwoCocycles.proof_2 isoTwoCocycles.proof_3).hom ≫ cyclesMap { τ₁ := ↑(oneCochainsLequiv A), τ₂ := ↑(twoCochainsLequiv A), τ₃ := ↑(threeCochainsLequiv A), comm₁₂ := ⋯, comm₂₃ := ⋯ } ≫ (shortComplexH2 A).moduleCatCyclesIso.hom) ≫ ModuleCat.ofHom (twoCocycles A).subtype = iCocycles A 2 ≫ ↑(twoCochainsLequiv A)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<GOAL>(HomologicalComplex.cyclesIsoSc' (inhomogeneousCochains A) 1 2 3 isoTwoCocycles.proof_2 isoTwoCocycles.proof_3).hom ≫ cyclesMap { τ₁ := ↑(oneCochainsLequiv A), τ₂ := ↑(twoCochainsLequiv A), τ₃ := ↑(threeCochainsLequiv A), comm₁₂ := ⋯, comm₂₃ := ⋯ } ≫ (shortComplexH2 A).moduleCatCyclesIso.hom ≫ ModuleCat.ofHom (twoCocycles A).subtype = iCocycles A 2 ≫ ↑(twoCochainsLequiv A)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<GOAL>(HomologicalComplex.cyclesIsoSc' (inhomogeneousCochains A) 1 2 3 isoTwoCocycles.proof_2 isoTwoCocycles.proof_3).hom ≫ cyclesMap { τ₁ := ↑(oneCochainsLequiv A), τ₂ := ↑(twoCochainsLequiv A), τ₃ := ↑(threeCochainsLequiv A), comm₁₂ := ⋯, comm₂₃ := ⋯ } ≫ (shortComplexH2 A).iCycles = iCocycles A 2 ≫ ↑(twoCochainsLequiv A)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>φ φ' : B → F ≃L[𝕜] F<VAR>U U' : Set B<VAR>hU : IsOpen U<VAR>hφ : ContinuousOn (fun x => ↑(φ x)) U<VAR>h2φ : ContinuousOn (fun x => ↑(φ x).symm) U<VAR>hU' : IsOpen U'<VAR>hφ' : ContinuousOn (fun x => ↑(φ' x)) U'<VAR>h2φ' : ContinuousOn (fun x => ↑(φ' x).symm) U'<GOAL>({ toFun := fun x => (x.1, (φ x.1) x.2), invFun := fun x => (x.1, (φ x.1).symm x.2), source := U ×ˢ univ, target := U ×ˢ univ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯, open_source := ⋯, open_target := ⋯, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ } ≫ₕ { toFun := fun x => (x.1, (φ' x.1) x.2), invFun := fun x => (x.1, (φ' x.1).symm x.2), source := U' ×ˢ univ, target := U' ×ˢ univ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯, open_source := ⋯, open_target := ⋯, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }).source = (U ∩ U') ×ˢ univ
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>n : ℕ<GOAL>(N₁Γ₀.inv.app K).f.f n = (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom.f.f n
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>n : ℕ<GOAL>((toKaroubi (ChainComplex C ℕ)).map (Γ₀NondegComplexIso K).inv ≫ (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom).f.f n = (Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom.f.f n
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J J₁ J₂ : LieIdeal R L'<VAR>h : f.IsIdealMorphism<GOAL>map f ⁅comap f J₁, comap f J₂⁆ = ⁅f.idealRange ⊓ J₁, f.idealRange ⊓ J₂⁆
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J J₁ J₂ : LieIdeal R L'<VAR>h : f.IsIdealMorphism<GOAL>⁅f.idealRange ⊓ J₁, f.idealRange ⊓ J₂⁆ ≤ f.idealRange
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x y : TruncatedWittVector p n R<VAR>h : x.out = y.out<VAR>i : Fin n<GOAL>coeff i x = coeff i y
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x y : TruncatedWittVector p n R<VAR>h : ∀ (n_1 : ℕ), x.out.coeff n_1 = y.out.coeff n_1<VAR>i : Fin n<GOAL>coeff i x = coeff i y
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f g : ι → Set X<VAR>hf : LocallyFinite f<VAR>hc : ∀ (i : ι), IsClosed (f i)<VAR>x : X<GOAL>⋂ i, ⋂ (_ : x ∉ f i), (f i)ᶜ ∈ 𝓝 x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f g : ι → Set X<VAR>hf : LocallyFinite f<VAR>hc : ∀ (i : ι), IsClosed (f i)<VAR>x : X<GOAL>IsOpen (⋂ i, ⋂ (_ : x ∉ f i), (f i)ᶜ)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f g : ι → Set X<VAR>hf : LocallyFinite f<VAR>hc : ∀ (i : ι), IsClosed (f i)<VAR>x : X<GOAL>IsClosed (⋃ i, f ↑i)
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>X : Type x<VAR>Y : Type y<VAR>inst✝⁴ : UniformSpace X<VAR>inst✝³ : UniformSpace Y<VAR>inst✝² : SMul M X<VAR>inst✝¹ : SMul M Y<VAR>inst✝ : UniformContinuousConstSMul M Y<VAR>f : X → Y<VAR>hf : UniformInducing f<VAR>hsmul : ∀ (c : M) (x : X), f (c • x) = c • f x<VAR>c : M<GOAL>UniformContinuous fun x => c • x
<VAR>G : Type u_1<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : CompleteSpace G<VAR>H : Type u_2<VAR>inst✝ : NormedAddCommGroup H<VAR>f : NormedAddGroupHom G H<VAR>K : AddSubgroup H<VAR>C ε : ℝ<VAR>hC : 0 < C<VAR>hε : 0 < ε<VAR>hyp : f.SurjectiveOnWith K C<VAR>h : H<VAR>h_in : h ∈ K.topologicalClosure<VAR>hyp_h : ¬h = 0<VAR>b : ℕ → ℝ := fun i => (1 / 2) ^ i * (ε * ‖h‖ / 2) / C<VAR>b_pos : ∀ (i : ℕ), 0 < b i<GOAL>∃ g, f g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
<VAR>G : Type u_1<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : CompleteSpace G<VAR>H : Type u_2<VAR>inst✝ : NormedAddCommGroup H<VAR>f : NormedAddGroupHom G H<VAR>K : AddSubgroup H<VAR>C ε : ℝ<VAR>hC : 0 < C<VAR>hε : 0 < ε<VAR>hyp : f.SurjectiveOnWith K C<VAR>h : H<VAR>h_in : h ∈ K.topologicalClosure<VAR>hyp_h : ¬h = 0<VAR>b : ℕ → ℝ := fun i => (1 / 2) ^ i * (ε * ‖h‖ / 2) / C<VAR>b_pos : ∀ (i : ℕ), 0 < b i<VAR>v : ℕ → H<VAR>lim_v : Tendsto (fun n => ∑ k ∈ range (n + 1), v k) atTop (𝓝 h)<VAR>v_in : ∀ (n : ℕ), v n ∈ K<VAR>hv₀ : ‖v 0 - h‖ < b 0<VAR>hv : ∀ n > 0, ‖v n‖ < b n<GOAL>∃ g, f g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
<VAR>G : Type u_1<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : CompleteSpace G<VAR>H : Type u_2<VAR>inst✝ : NormedAddCommGroup H<VAR>f : NormedAddGroupHom G H<VAR>K : AddSubgroup H<VAR>C ε : ℝ<VAR>hC : 0 < C<VAR>hε : 0 < ε<VAR>hyp : f.SurjectiveOnWith K C<VAR>h : H<VAR>h_in : h ∈ K.topologicalClosure<VAR>hyp_h : ¬h = 0<VAR>b : ℕ → ℝ := fun i => (1 / 2) ^ i * (ε * ‖h‖ / 2) / C<VAR>b_pos : ∀ (i : ℕ), 0 < b i<VAR>v : ℕ → H<VAR>lim_v : Tendsto (fun n => ∑ k ∈ range (n + 1), v k) atTop (𝓝 h)<VAR>v_in : ∀ (n : ℕ), v n ∈ K<VAR>hv₀ : ‖v 0 - h‖ < b 0<VAR>hv : ∀ n > 0, ‖v n‖ < b n<VAR>u : ℕ → G<VAR>hu : ∀ (n : ℕ), f (u n) = v n<VAR>hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖<VAR>s : ℕ → G := fun n => ∑ k ∈ range (n + 1), u k<VAR>this : CauchySeq s<GOAL>∃ g, f g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
<VAR>G : Type u_1<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : CompleteSpace G<VAR>H : Type u_2<VAR>inst✝ : NormedAddCommGroup H<VAR>f : NormedAddGroupHom G H<VAR>K : AddSubgroup H<VAR>C ε : ℝ<VAR>hC : 0 < C<VAR>hε : 0 < ε<VAR>hyp : f.SurjectiveOnWith K C<VAR>h : H<VAR>h_in : h ∈ K.topologicalClosure<VAR>hyp_h : ¬h = 0<VAR>b : ℕ → ℝ := fun i => (1 / 2) ^ i * (ε * ‖h‖ / 2) / C<VAR>b_pos : ∀ (i : ℕ), 0 < b i<VAR>v : ℕ → H<VAR>lim_v : Tendsto (fun n => ∑ k ∈ range (n + 1), v k) atTop (𝓝 h)<VAR>v_in : ∀ (n : ℕ), v n ∈ K<VAR>hv₀ : ‖v 0 - h‖ < b 0<VAR>hv : ∀ n > 0, ‖v n‖ < b n<VAR>u : ℕ → G<VAR>hu : ∀ (n : ℕ), f (u n) = v n<VAR>hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖<VAR>s : ℕ → G := fun n => ∑ k ∈ range (n + 1), u k<VAR>this : CauchySeq s<VAR>g : G<VAR>hg : Tendsto s atTop (𝓝 g)<GOAL>∃ g, f g = h ∧ ‖g‖ ≤ (C + ε) * ‖h‖
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>κ : ι → Sort u_3<VAR>A B : Set (Finset α)<VAR>s : Finset α<VAR>r : ℕ<VAR>f : (i : ι) → κ i → Set (Finset α)<GOAL>Sized r (⋃ i, ⋃ j, f i j) ↔ ∀ (i : ι) (j : κ i), Sized r (f i j)
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>n : ℕ<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁴ : Fintype ι<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁹ : (i : ι) → NormedAddCommGroup (E₁ i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁷ : (i : ι') → NormedAddCommGroup (E' i)<VAR>inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁵ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>inst✝⁴ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => Ei i.succ) G<VAR>m : Ei 0<VAR>x : (i : Fin n) → Ei i.succ<GOAL>(f.uncurryLeft.curryLeft m) x = (f m) x
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>β' : Type u_5<VAR>γ : Type u_6<VAR>γ' : Type u_7<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>q : Type u_12<VAR>r : Type u_13<VAR>l' : Type u_14<VAR>m' : Type u_15<VAR>n' : Type u_16<VAR>p' : Type u_17<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing R<VAR>A : Matrix m m R<VAR>B : Matrix n n R<GOAL>(kroneckerMap (fun x x_1 => x * x_1) A B).det = A.det ^ Fintype.card n * B.det ^ Fintype.card m
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>β' : Type u_5<VAR>γ : Type u_6<VAR>γ' : Type u_7<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>q : Type u_12<VAR>r : Type u_13<VAR>l' : Type u_14<VAR>m' : Type u_15<VAR>n' : Type u_16<VAR>p' : Type u_17<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing R<VAR>A : Matrix m m R<VAR>B : Matrix n n R<GOAL>(A.map fun a => ((Algebra.lmul ℕ R).toLinearMap a) 1).det ^ Fintype.card n * (B.map fun b => ((Algebra.lmul ℕ R).toLinearMap 1) b).det ^ Fintype.card m = A.det ^ Fintype.card n * B.det ^ Fintype.card m
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<VAR>hc : P.c = 0<GOAL>P.toPoly.degree ≤ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : CommGroup G<VAR>inst✝ : TopologicalGroup G<VAR>f : α → G<VAR>hf : Multipliable f<VAR>e : Set G<VAR>he : e ∈ 𝓝 1<GOAL>∃ s, ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<GOAL>wittNeg p 0 = -X (0, 0)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<GOAL>(map (Int.castRingHom ℚ)) (wittNeg p 0) = (map (Int.castRingHom ℚ)) (-X (0, 0))
<VAR>p q : ℤ[X]<GOAL>p.IsUnitTrinomial ↔ (p * p.mirror).coeff (((p * p.mirror).natDegree + (p * p.mirror).natTrailingDegree) / 2) = 3
<VAR>p q : ℤ[X]<GOAL>p.IsUnitTrinomial ↔ (p.sum fun n x => x ^ 2) = 3
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>Q : AffineSubspace k P<GOAL>(↑Q).Nonempty ↔ Q ≠ ⊥
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>Q : AffineSubspace k P<GOAL>↑Q ≠ ∅ ↔ Q ≠ ⊥
<VAR>M : Type u<VAR>N : Type v<VAR>inst✝¹ : Monoid M<VAR>inst✝ : Monoid N<VAR>e : M ≃* N<GOAL>𝟭 (SingleObj M) = e.toMonoidHom.toFunctor ⋙ e.symm.toMonoidHom.toFunctor
<VAR>M : Type u<VAR>N : Type v<VAR>inst✝¹ : Monoid M<VAR>inst✝ : Monoid N<VAR>e : M ≃* N<GOAL>(MonoidHom.id M).toFunctor = (e.symm.toMonoidHom.comp e.toMonoidHom).toFunctor
<VAR>M : Type u<VAR>N : Type v<VAR>inst✝¹ : Monoid M<VAR>inst✝ : Monoid N<VAR>e : M ≃* N<GOAL>e.symm.toMonoidHom.toFunctor ⋙ e.toMonoidHom.toFunctor = 𝟭 (SingleObj N)
<VAR>M : Type u<VAR>N : Type v<VAR>inst✝¹ : Monoid M<VAR>inst✝ : Monoid N<VAR>e : M ≃* N<GOAL>(e.toMonoidHom.comp e.symm.toMonoidHom).toFunctor = (MonoidHom.id N).toFunctor
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>σ : Type u_1<VAR>inst✝⁴ : DecidableEq σ<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>e : σ →₀ ℕ<VAR>r : R<VAR>n : N<VAR>d : σ →₀ ℕ<GOAL>(scalarRTensor ((monomial e) r ⊗ₜ[R] n)) d = if e = d then r • n else 0
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>A : Type u_5<VAR>B : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>inst✝⁷ : Monoid M<VAR>inst✝⁶ : MulAction M α<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MulAction G α<VAR>g✝ : G<VAR>a✝ b : α<VAR>inst✝³ : Group H<VAR>inst✝² : MulAction G H<VAR>inst✝¹ : SMulCommClass G H H<VAR>inst✝ : IsScalarTower G H H<VAR>g : G<VAR>a : H<GOAL>g • a * g⁻¹ • a⁻¹ = 1
<VAR>η : Type u_1<VAR>α : Type u_2<VAR>ι : Type u_3<VAR>κ : Type u_4<VAR>l : Line α ι<VAR>i : ι<VAR>a x : α<VAR>C : (ι → α) → κ<GOAL>Subspace.IsMono C l.toSubspaceUnit ↔ IsMono C l
<VAR>η : Type u_1<VAR>α : Type u_2<VAR>ι : Type u_3<VAR>κ : Type u_4<VAR>l : Line α ι<VAR>i : ι<VAR>a x : α<VAR>C : (ι → α) → κ<GOAL>(∃ c, ∀ (x : Unit → α), (C fun i => (l.idxFun i).getD (x ())) = c) ↔ ∃ c, ∀ (x : α), (C fun i => (l.idxFun i).getD x) = c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s✝ : Finset α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>g : γ → α<VAR>s : Finset γ<VAR>H : ∀ x ∈ s, ∀ y ∈ s, g x = g y → x = y<GOAL>fold op b f (image g s) = fold op b (f ∘ g) s
<VAR>u v : PrimeMultiset<GOAL>u.prod ∣ v.prod ↔ u ≤ v
<VAR>u v : PrimeMultiset<VAR>h : u.prod.factorMultiset ≤ v ↔ u.prod ∣ v.prod := PNat.factorMultiset_le_iff'<GOAL>u.prod ∣ v.prod ↔ u ≤ v
<VAR>u v : PrimeMultiset<VAR>h : u ≤ v ↔ u.prod ∣ v.prod<GOAL>u.prod ∣ v.prod ↔ u ≤ v
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M K' L' : HomologicalComplex C c<VAR>f : K ⟶ L<VAR>i j k : ι<VAR>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>inst✝³ : K.HasHomology j<VAR>inst✝² : L.HasHomology j<VAR>inst✝¹ : (K.sc' i j k).HasHomology<VAR>inst✝ : (L.sc' i j k).HasHomology<GOAL>QuasiIsoAt f j ↔ ShortComplex.QuasiIso ((shortComplexFunctor' C c i j k).map f)
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M K' L' : HomologicalComplex C c<VAR>f : K ⟶ L<VAR>i j k : ι<VAR>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>inst✝³ : K.HasHomology j<VAR>inst✝² : L.HasHomology j<VAR>inst✝¹ : (K.sc' i j k).HasHomology<VAR>inst✝ : (L.sc' i j k).HasHomology<GOAL>ShortComplex.QuasiIso ((shortComplexFunctor C c j).map f) ↔ ShortComplex.QuasiIso ((shortComplexFunctor' C c i j k).map f)
<VAR>α : Type u<VAR>β : Type v<VAR>f g : α → α<VAR>h : Commute f g<VAR>n : ℕ<GOAL>(f ∘ g)^[n] = f^[n] ∘ g^[n]
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f✝ f g : R[X]<VAR>fg : f.leadingCoeff * g.leadingCoeff ≠ 0<GOAL>reflect (f * g).natDegree (f * g) = reflect f.natDegree f * reflect g.natDegree g
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n✝ : ℤ<VAR>γ✝ γ₁ γ₂ : Cochain K L n✝<VAR>n' a : ℤ<VAR>γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'<VAR>n : ℤ<VAR>hn : n + a = n'<VAR>x : Rˣ<GOAL>(x • γ).leftUnshift n hn = x • γ.leftUnshift n hn
<VAR>ι : Sort u_1<VAR>f : ι → ℝ≥0<VAR>a g : ℝ≥0<VAR>h : ι → ℝ≥0<VAR>H : ∀ (j : ι), g * h j ≤ a<GOAL>g * iSup h ≤ a
<VAR>ι : Sort u_1<VAR>f : ι → ℝ≥0<VAR>a g : ℝ≥0<VAR>h : ι → ℝ≥0<VAR>H : ∀ (j : ι), g * h j ≤ a<GOAL>⨆ i, g * h i ≤ a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : SMul 𝕜 α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : StrictConcaveOn 𝕜 univ ⇑f<GOAL>StrictConvexOn 𝕜 univ ⇑f.symm
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : SMul 𝕜 α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : StrictConcaveOn 𝕜 univ ⇑f<VAR>x : β<VAR>x✝¹ : x ∈ univ<VAR>y : β<VAR>x✝ : y ∈ univ<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>f.symm (a • x + b • y) < a • f.symm x + b • f.symm y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : SMul 𝕜 α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : StrictConcaveOn 𝕜 univ ⇑f<VAR>x : β<VAR>x✝¹ : x ∈ univ<VAR>y : β<VAR>x✝ : y ∈ univ<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>x' : α<VAR>hx'' : x = f x'<GOAL>f.symm (a • x + b • y) < a • f.symm x + b • f.symm y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : SMul 𝕜 α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : StrictConcaveOn 𝕜 univ ⇑f<VAR>x : β<VAR>x✝¹ : x ∈ univ<VAR>y : β<VAR>x✝ : y ∈ univ<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>x' : α<VAR>hx'' : x = f x'<VAR>y' : α<VAR>hy'' : y = f y'<GOAL>f.symm (a • x + b • y) < a • f.symm x + b • f.symm y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : SMul 𝕜 α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : StrictConcaveOn 𝕜 univ ⇑f<VAR>x : β<VAR>x✝¹ : x ∈ univ<VAR>y : β<VAR>x✝ : y ∈ univ<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>x' : α<VAR>hx'' : x = f x'<VAR>y' : α<VAR>hy'' : y = f y'<VAR>hxy' : x' ≠ y'<GOAL>f.symm (a • x + b • y) < a • f.symm x + b • f.symm y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : OrderedAddCommMonoid α<VAR>inst✝² : SMul 𝕜 α<VAR>inst✝¹ : OrderedAddCommMonoid β<VAR>inst✝ : SMul 𝕜 β<VAR>f : α ≃o β<VAR>hf : StrictConcaveOn 𝕜 univ ⇑f<VAR>x : β<VAR>x✝¹ : x ∈ univ<VAR>y : β<VAR>x✝ : y ∈ univ<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>x' : α<VAR>hx'' : x = f x'<VAR>y' : α<VAR>hy'' : y = f y'<VAR>hxy' : x' ≠ y'<GOAL>f.symm (a • f x' + b • f y') < a • x' + b • y'