ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>coequalizer.π (M.actRight ▷ { X := Y.X, actLeft := Y.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := Y.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X) ((α_ M.X Y.X { X := Y.X, actLeft := Y.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := Y.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X).hom ≫ M.X ◁ { X := Y.X, actLeft := Y.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := Y.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.actLeft) ≫ (whiskerRight f { X := Y.X, actLeft := Y.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := Y.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }).hom = coequalizer.π (M.actRight ▷ { X := Y.X, actLeft := Y.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := Y.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X) ((α_ M.X Y.X { X := Y.X, actLeft := Y.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := Y.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X).hom ≫ M.X ◁ { X := Y.X, actLeft := Y.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := Y.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.actLeft) ≫ ((isoOfIso { hom := RightUnitorBimod.hom M, inv := RightUnitorBimod.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯ ⋯).hom ≫ f ≫ (isoOfIso { hom := RightUnitorBimod.hom N, inv := RightUnitorBimod.inv N, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯ ⋯).inv).hom
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>coequalizer.π (M.actRight ▷ Y.X) ((α_ M.X Y.X Y.X).hom ≫ M.X ◁ Y.mul) ≫ colimMap (parallelPairHom (M.actRight ▷ Y.X) ((α_ M.X Y.X Y.X).hom ≫ M.X ◁ Y.mul) (N.actRight ▷ Y.X) ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ Y.mul) (f.hom ▷ Y.X ▷ Y.X) (f.hom ▷ Y.X) ⋯ ⋯) = coequalizer.π (M.actRight ▷ Y.X) ((α_ M.X Y.X Y.X).hom ≫ M.X ◁ Y.mul) ≫ RightUnitorBimod.hom M ≫ f.hom ≫ RightUnitorBimod.inv N
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>f.hom ▷ Y.X ≫ colimit.ι (parallelPair (N.actRight ▷ Y.X) ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ Y.mul)) WalkingParallelPair.one = coequalizer.π (M.actRight ▷ Y.X) ((α_ M.X Y.X Y.X).hom ≫ M.X ◁ Y.mul) ≫ RightUnitorBimod.hom M ≫ f.hom ≫ RightUnitorBimod.inv N
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>f.hom ▷ Y.X ≫ colimit.ι (parallelPair (N.actRight ▷ Y.X) ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ Y.mul)) WalkingParallelPair.one = coequalizer.π (M.actRight ▷ Y.X) ((α_ M.X Y.X Y.X).hom ≫ M.X ◁ Y.mul) ≫ coequalizer.desc M.actRight ⋯ ≫ f.hom ≫ RightUnitorBimod.inv N
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>f.hom ▷ Y.X ≫ colimit.ι (parallelPair (N.actRight ▷ Y.X) ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ Y.mul)) WalkingParallelPair.one = (M.actRight ≫ f.hom) ≫ RightUnitorBimod.inv N
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>f.hom ▷ Y.X ≫ colimit.ι (parallelPair (N.actRight ▷ Y.X) ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ Y.mul)) WalkingParallelPair.one = (M.actRight ≫ f.hom) ≫ (ρ_ N.X).inv ≫ N.X ◁ Y.one ≫ coequalizer.π (N.actRight ▷ Y.X) ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ Y.mul)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>f.hom ▷ Y.X ≫ colimit.ι (parallelPair (N.actRight ▷ Y.X) ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ Y.mul)) WalkingParallelPair.one = (((f.hom ▷ Y.X ≫ N.actRight) ≫ (ρ_ N.X).inv) ≫ N.X ◁ Y.one) ≫ coequalizer.π (N.actRight ▷ Y.X) ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ Y.mul)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>f.hom ▷ Y.X ≫ colimit.ι (parallelPair (N.actRight ▷ Y.X) ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ Y.mul)) WalkingParallelPair.one = f.hom ▷ Y.X ≫ (((ρ_ (N.X ⊗ Y.X)).inv ≫ N.actRight ▷ 𝟙_ C) ≫ N.X ◁ Y.one) ≫ coequalizer.π (N.actRight ▷ Y.X) ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ Y.mul)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>f.hom ▷ Y.X ≫ colimit.ι (parallelPair (N.actRight ▷ Y.X) ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ Y.mul)) WalkingParallelPair.one = f.hom ▷ Y.X ≫ (ρ_ (N.X ⊗ Y.X)).inv ≫ ((N.X ⊗ Y.X) ◁ Y.one ≫ N.actRight ▷ Y.X) ≫ coequalizer.π (N.actRight ▷ Y.X) ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ Y.mul)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>f.hom ▷ Y.X ≫ colimit.ι (parallelPair (N.actRight ▷ Y.X) ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ Y.mul)) WalkingParallelPair.one = f.hom ▷ Y.X ≫ (ρ_ (N.X ⊗ Y.X)).inv ≫ (N.X ⊗ Y.X) ◁ Y.one ≫ ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ Y.mul) ≫ coequalizer.π (N.actRight ▷ Y.X) ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ Y.mul)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>f.hom ▷ Y.X ≫ colimit.ι (parallelPair (N.actRight ▷ Y.X) ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ Y.mul)) WalkingParallelPair.one = f.hom ▷ Y.X ≫ (ρ_ (N.X ⊗ Y.X)).inv ≫ (((α_ N.X Y.X (𝟙_ C)).hom ≫ N.X ◁ Y.X ◁ Y.one) ≫ N.X ◁ Y.mul) ≫ coequalizer.π (N.actRight ▷ Y.X) ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ Y.mul)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>f.hom ▷ Y.X ≫ colimit.ι (parallelPair (N.actRight ▷ Y.X) ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ Y.mul)) WalkingParallelPair.one = f.hom ▷ Y.X ≫ (ρ_ (N.X ⊗ Y.X)).inv ≫ (α_ N.X Y.X (𝟙_ C)).hom ≫ N.X ◁ (ρ_ Y.X).hom ≫ coequalizer.π (N.actRight ▷ Y.X) ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ Y.mul)
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : NatPowAssoc R<VAR>a b : R<VAR>k : ℕ<GOAL>(-1) ^ k * a * b = (-1) ^ k * (a * b)
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>v : K<VAR>n : ℕ<VAR>inst✝ : FloorRing K<VAR>terminates : (of v).Terminates<GOAL>∀ᶠ (n : ℕ) in atTop, v = (of v).convs n
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>v : K<VAR>n : ℕ<VAR>inst✝ : FloorRing K<VAR>terminates : (of v).Terminates<GOAL>∃ a, ∀ b ≥ a, v = (of v).convs b
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>v : K<VAR>n✝ : ℕ<VAR>inst✝ : FloorRing K<VAR>n : ℕ<VAR>terminatedAt_n : (of v).TerminatedAt n<GOAL>∃ a, ∀ b ≥ a, v = (of v).convs b
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>v : K<VAR>n✝ : ℕ<VAR>inst✝ : FloorRing K<VAR>n : ℕ<VAR>terminatedAt_n : (of v).TerminatedAt n<GOAL>∀ b ≥ n, v = (of v).convs b
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>v : K<VAR>n✝ : ℕ<VAR>inst✝ : FloorRing K<VAR>n : ℕ<VAR>terminatedAt_n : (of v).TerminatedAt n<VAR>m : ℕ<VAR>m_geq_n : m ≥ n<GOAL>v = (of v).convs m
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>v : K<VAR>n✝ : ℕ<VAR>inst✝ : FloorRing K<VAR>n : ℕ<VAR>terminatedAt_n : (of v).TerminatedAt n<VAR>m : ℕ<VAR>m_geq_n : m ≥ n<GOAL>v = (of v).convs n
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>N : Type u_9<VAR>N₁ : Type u_10<VAR>N₂ : Type u_11<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : AddCommGroup N₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N₁<VAR>inst✝² : Monoid S<VAR>inst✝¹ : DistribMulAction S M<VAR>inst✝ : SMulCommClass R S M<VAR>f' : M →ₗ[R] M<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>h : Surjective ⇑(f' ^ n)<GOAL>Surjective ⇑f'
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>N : Type u_9<VAR>N₁ : Type u_10<VAR>N₂ : Type u_11<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : AddCommGroup N₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N₁<VAR>inst✝² : Monoid S<VAR>inst✝¹ : DistribMulAction S M<VAR>inst✝ : SMulCommClass R S M<VAR>f' : M →ₗ[R] M<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>h : Surjective (⇑f' ∘ ⇑(f' ^ n.pred))<GOAL>Surjective ⇑f'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : TopologicalSpace α<VAR>μ : Measure α<VAR>p q : Set α → Prop<VAR>U s✝ : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>h : μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤<VAR>A s : Set α<VAR>s_meas : MeasurableSet s<VAR>hs : (μ.restrict A) s ≠ ⊤<VAR>r : ℝ≥0∞<VAR>hr : r < (μ.restrict A) s<GOAL>∃ K ⊆ s, p K ∧ r < (μ.restrict A) K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : TopologicalSpace α<VAR>μ : Measure α<VAR>p q : Set α → Prop<VAR>U s✝ : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>h : μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤<VAR>A s : Set α<VAR>s_meas : MeasurableSet s<VAR>hs : μ (s ∩ A) ≠ ⊤<VAR>r : ℝ≥0∞<VAR>hr : r < (μ.restrict A) s<GOAL>∃ K ⊆ s, p K ∧ r < (μ.restrict A) K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : TopologicalSpace α<VAR>μ : Measure α<VAR>p q : Set α → Prop<VAR>U s✝ : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>h : μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤<VAR>A s : Set α<VAR>s_meas : MeasurableSet s<VAR>hs : μ (s ∩ A) ≠ ⊤<VAR>r : ℝ≥0∞<VAR>hr : r < (μ.restrict A) s<VAR>K : Set α<VAR>K_subs : K ⊆ toMeasurable μ (s ∩ A) ∩ s<VAR>pK : p K<VAR>rK : r < μ K<GOAL>∃ K ⊆ s, p K ∧ r < (μ.restrict A) K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : TopologicalSpace α<VAR>μ : Measure α<VAR>p q : Set α → Prop<VAR>U s✝ : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>h : μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤<VAR>A s : Set α<VAR>s_meas : MeasurableSet s<VAR>hs : μ (s ∩ A) ≠ ⊤<VAR>r : ℝ≥0∞<VAR>hr : r < (μ.restrict A) s<VAR>K : Set α<VAR>K_subs : K ⊆ toMeasurable μ (s ∩ A) ∩ s<VAR>pK : p K<VAR>rK : r < μ K<GOAL>r < (μ.restrict A) K
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<GOAL>[].prod⁻¹ = (List.map Inv.inv [].reverse).prod
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A✝ B A : Matrix n n α<VAR>Xs : List (Matrix n n α)<GOAL>(A :: Xs).prod⁻¹ = (List.map Inv.inv (A :: Xs).reverse).prod
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>A : C<VAR>inst✝ : S.HasHomology<VAR>h : S.LeftHomologyData<GOAL>(S.leftHomologyIso.symm ≪≫ h.leftHomologyIso).hom ≫ h.leftHomologyIso.inv = S.leftHomologyIso.inv
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<GOAL>infDist x s = ⨅ y, dist x ↑y
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<GOAL>⨅ i, (edist x ↑i).toReal = ⨅ y, dist x ↑y
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<GOAL>∀ (i : { y // y ∈ s }), edist x ↑i ≠ ⊤
<VAR>R✝ : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring R✝<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R✝ S<VAR>I✝ : Ideal S<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>hI : IsNilpotent I<VAR>x : R<GOAL>IsUnit ((Ideal.Quotient.mk I) x) ↔ IsUnit x
<VAR>R✝ : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring R✝<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R✝ S<VAR>I✝ : Ideal S<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>hI : IsNilpotent I<VAR>x : R<GOAL>IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x
<VAR>R✝ : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring R✝<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R✝ S<VAR>I✝ : Ideal S<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>hI : IsNilpotent I<GOAL>∀ {x : R}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x
<VAR>R✝ : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring R✝<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R✝ S<VAR>I : Ideal S<VAR>R : Type u_3<VAR>inst✝ : CommRing R<GOAL>∀ ⦃S : Type u_3⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → ∀ {x : S}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x
<VAR>R✝ : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring R✝<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R✝ S<VAR>I : Ideal S<VAR>R : Type u_3<VAR>inst✝ : CommRing R<GOAL>∀ ⦃S : Type u_3⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → (∀ {x : S}, IsUnit ((Ideal.Quotient.mk I) x) → IsUnit x) → (∀ {x : S ⧸ I}, IsUnit ((Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk I) J)) x) → IsUnit x) → ∀ {x : S}, IsUnit ((Ideal.Quotient.mk J) x) → IsUnit x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>E : IntermediateField K L<VAR>inst✝ : FiniteDimensional K ↥E<VAR>h_basis : E.fixingSubgroup.carrier ∈ galGroupBasis K L<GOAL>IsOpen ↑E.fixingSubgroup
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>E : IntermediateField K L<VAR>inst✝ : FiniteDimensional K ↥E<VAR>h_basis : E.fixingSubgroup.carrier ∈ galGroupBasis K L<VAR>h_nhd : E.fixingSubgroup.carrier ∈ 𝓝 1<GOAL>IsOpen ↑E.fixingSubgroup
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : Group α<VAR>inst✝¹ : IsCyclic α<VAR>inst✝ : Fintype α<GOAL>exponent α = Fintype.card α
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : Group α<VAR>inst✝¹ : IsCyclic α<VAR>inst✝ : Fintype α<VAR>g : α<VAR>hg : ∀ (x : α), x ∈ Subgroup.zpowers g<GOAL>exponent α = Fintype.card α
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : Group α<VAR>inst✝¹ : IsCyclic α<VAR>inst✝ : Fintype α<VAR>g : α<VAR>hg : ∀ (x : α), x ∈ Subgroup.zpowers g<GOAL>exponent α ∣ Fintype.card α
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : Group α<VAR>inst✝¹ : IsCyclic α<VAR>inst✝ : Fintype α<VAR>g : α<VAR>hg : ∀ (x : α), x ∈ Subgroup.zpowers g<GOAL>Fintype.card α ∣ exponent α
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : Group α<VAR>inst✝¹ : IsCyclic α<VAR>inst✝ : Fintype α<VAR>g : α<VAR>hg : ∀ (x : α), x ∈ Subgroup.zpowers g<GOAL>orderOf g ∣ exponent α
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>s1 s2 : Set (Set Ω)<VAR>hs1 : ∀ s ∈ s1, MeasurableSet s<VAR>hs2 : ∀ s ∈ s2, MeasurableSet s<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<GOAL>(∀ (t1 t2 : Set Ω), t1 ∈ s1 → t2 ∈ s2 → ∀ᵐ (a : Ω) ∂μ.trim hm', ((condexpKernel μ m') a) (t1 ∩ t2) = ((condexpKernel μ m') a) t1 * ((condexpKernel μ m') a) t2) ↔ ∀ (t1 t2 : Set Ω), t1 ∈ s1 → t2 ∈ s2 → μ[(t1 ∩ t2).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[t1.indicator fun ω => 1|m'] * μ[t2.indicator fun ω => 1|m']
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>s1 s2 : Set (Set Ω)<VAR>hs1 : ∀ s ∈ s1, MeasurableSet s<VAR>hs2 : ∀ s ∈ s2, MeasurableSet s<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hs1_eq : ∀ s ∈ s1, (fun ω => (((condexpKernel μ m') ω) s).toReal) =ᶠ[ae μ] μ[s.indicator fun ω => 1|m']<GOAL>(∀ (t1 t2 : Set Ω), t1 ∈ s1 → t2 ∈ s2 → ∀ᵐ (a : Ω) ∂μ.trim hm', ((condexpKernel μ m') a) (t1 ∩ t2) = ((condexpKernel μ m') a) t1 * ((condexpKernel μ m') a) t2) ↔ ∀ (t1 t2 : Set Ω), t1 ∈ s1 → t2 ∈ s2 → μ[(t1 ∩ t2).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[t1.indicator fun ω => 1|m'] * μ[t2.indicator fun ω => 1|m']
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>s1 s2 : Set (Set Ω)<VAR>hs1 : ∀ s ∈ s1, MeasurableSet s<VAR>hs2 : ∀ s ∈ s2, MeasurableSet s<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hs1_eq : ∀ s ∈ s1, (fun ω => (((condexpKernel μ m') ω) s).toReal) =ᶠ[ae μ] μ[s.indicator fun ω => 1|m']<VAR>hs2_eq : ∀ s ∈ s2, (fun ω => (((condexpKernel μ m') ω) s).toReal) =ᶠ[ae μ] μ[s.indicator fun ω => 1|m']<GOAL>(∀ (t1 t2 : Set Ω), t1 ∈ s1 → t2 ∈ s2 → ∀ᵐ (a : Ω) ∂μ.trim hm', ((condexpKernel μ m') a) (t1 ∩ t2) = ((condexpKernel μ m') a) t1 * ((condexpKernel μ m') a) t2) ↔ ∀ (t1 t2 : Set Ω), t1 ∈ s1 → t2 ∈ s2 → μ[(t1 ∩ t2).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[t1.indicator fun ω => 1|m'] * μ[t2.indicator fun ω => 1|m']
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>s1 s2 : Set (Set Ω)<VAR>hs1 : ∀ s ∈ s1, MeasurableSet s<VAR>hs2 : ∀ s ∈ s2, MeasurableSet s<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hs1_eq : ∀ s ∈ s1, (fun ω => (((condexpKernel μ m') ω) s).toReal) =ᶠ[ae μ] μ[s.indicator fun ω => 1|m']<VAR>hs2_eq : ∀ s ∈ s2, (fun ω => (((condexpKernel μ m') ω) s).toReal) =ᶠ[ae μ] μ[s.indicator fun ω => 1|m']<VAR>hs12_eq : ∀ s ∈ s1, ∀ t ∈ s2, (fun ω => (((condexpKernel μ m') ω) (s ∩ t)).toReal) =ᶠ[ae μ] μ[(s ∩ t).indicator fun ω => 1|m']<GOAL>(∀ (t1 t2 : Set Ω), t1 ∈ s1 → t2 ∈ s2 → ∀ᵐ (a : Ω) ∂μ.trim hm', ((condexpKernel μ m') a) (t1 ∩ t2) = ((condexpKernel μ m') a) t1 * ((condexpKernel μ m') a) t2) ↔ ∀ (t1 t2 : Set Ω), t1 ∈ s1 → t2 ∈ s2 → μ[(t1 ∩ t2).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[t1.indicator fun ω => 1|m'] * μ[t2.indicator fun ω => 1|m']
<VAR>n : ℕ<VAR>this✝ : ↑n + 1 ≠ 0<VAR>this : ↑n + 1 + 1 ≠ 0<VAR>h : ↑n + 2 ≠ 0<GOAL>gosperCatalan (n + 1) (n + 1) - gosperCatalan (n + 1) 0 = ↑(n + 1).centralBinom / (↑n + 2)
<VAR>n : ℕ<VAR>this✝ : ↑n + 1 ≠ 0<VAR>this : ↑n + 1 + 1 ≠ 0<VAR>h : ↑n + 2 ≠ 0<GOAL>↑(n + 1).centralBinom * ↑1 * (2 * ↑(n + 1) - ↑(n + 1)) / (2 * ↑(n + 1) * (↑(n + 1) + 1)) - ↑1 * ↑(n + 1).centralBinom * (2 * ↑0 - ↑(n + 1)) / (2 * ↑(n + 1) * (↑(n + 1) + 1)) = ↑(n + 1).centralBinom / (↑n + 2)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>K : ℝ≥0<VAR>f : α → β<VAR>x y : α<VAR>r : ℝ<GOAL>LipschitzWith 1 Real.toNNReal
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>K : ℝ≥0<VAR>f : α → β<VAR>x✝ y✝ : α<VAR>r x y : ℝ<GOAL>dist x.toNNReal y.toNNReal ≤ ↑1 * dist x y
<VAR>ι : Sort u_1<VAR>f g : ι → ℝ≥0∞<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>hf : ∀ (i : ι), f i ≠ ⊤<GOAL>(iSup f).toReal = ⨆ i, (f i).toReal
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>J : Type u_4<VAR>inst✝¹⁵ : Category.{u_7, u_1} C<VAR>inst✝¹⁴ : Category.{u_6, u_2} D<VAR>inst✝¹³ : Category.{?u.111353, u_3} E<VAR>inst✝¹² : Category.{?u.111357, u_4} J<VAR>F₁ F₂ F₃ : C ⥤ D<VAR>τ : F₁ ⟶ F₂<VAR>τ' : F₂ ⟶ F₃<VAR>e : F₁ ≅ F₂<VAR>G G' : D ⥤ E<VAR>τ'' : G ⟶ G'<VAR>H : E ⥤ J<VAR>A : Type u_5<VAR>inst✝¹¹ : AddMonoid A<VAR>inst✝¹⁰ : HasShift C A<VAR>inst✝⁹ : HasShift D A<VAR>inst✝⁸ : HasShift E A<VAR>inst✝⁷ : HasShift J A<VAR>inst✝⁶ : F₁.CommShift A<VAR>inst✝⁵ : F₂.CommShift A<VAR>inst✝⁴ : F₃.CommShift A<VAR>inst✝³ : G.CommShift A<VAR>inst✝² : G'.CommShift A<VAR>inst✝¹ : H.CommShift A<VAR>inst✝ : CommShift τ A<VAR>a : A<VAR>X : C<GOAL>τ.app ((shiftFunctor C a).obj X) = (F₁.commShiftIso a).hom.app X ≫ (shiftFunctor D a).map (τ.app X) ≫ (F₂.commShiftIso a).inv.app 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>inst✝ : HasGroupoid M G<VAR>hG : G.LocalInvariantProp G Q<VAR>hQ : ∀ (y : H), Q id univ y<VAR>he : e ∈ maximalAtlas M G<VAR>x : M<VAR>hx : x ∈ e.source<GOAL>LiftPropWithinAt Q (↑e) e.source 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>inst✝ : HasGroupoid M G<VAR>hG : G.LocalInvariantProp G Q<VAR>hQ : ∀ (y : H), Q id univ y<VAR>he : e ∈ maximalAtlas M G<VAR>x : M<VAR>hx : x ∈ e.source<GOAL>e.source ∈ 𝓝 x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : OrderedSemiring R<VAR>a✝ b✝ x y : R<VAR>n✝ m : ℕ<VAR>a b : R<VAR>ha : 0 ≤ a<VAR>hab : a ≤ b<VAR>n : ℕ<GOAL>a ^ (n + 1) ≤ b ^ (n + 1)
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<GOAL>(range Real.toEReal).OrdConnected
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<GOAL>(Ioo ⊥ ⊤).OrdConnected
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>c : Chain (Part α)<VAR>a b : α<VAR>hb : some b ∈ c<VAR>i : ℕ<VAR>ha : some a = c i<GOAL>a = b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>c : Chain (Part α)<VAR>a b : α<VAR>hb : some b ∈ c<VAR>i : ℕ<VAR>ha : c i = some a<GOAL>a = b