ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁸ : Category.{u_3, u_1} C<VAR>inst✝⁷ : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>inst✝⁶ : HasShift C ℤ<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝² : Pretriangulated C<VAR>inst✝¹ : HasShift D ℤ<VAR>inst✝ : L.CommShift ℤ<VAR>H : ∀ (T₁' T₂' : Triangle C), T₁' ∈ distinguishedTriangles → T₂' ∈ distinguishedTriangles → ∀ (a : L.obj T₁'.obj₁ ⟶ L.obj T₂'.obj₁) (b : L.obj T₁'.obj₂ ⟶ L.obj T₂'.obj₂), L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ → ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b<VAR>T₁ T₂ : Triangle D<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<VAR>T₁' : Triangle C<VAR>e₁ : T₁ ≅ L.mapTriangle.obj T₁'<VAR>hT₁' : T₁' ∈ distinguishedTriangles<VAR>T₂' : Triangle C<VAR>e₂ : T₂ ≅ L.mapTriangle.obj T₂'<VAR>hT₂' : T₂' ∈ distinguishedTriangles<VAR>comm₁ : (L.mapTriangle.obj T₁').mor₁ ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁<VAR>comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ (L.mapTriangle.obj T₂').mor₁<VAR>comm₂ : T₁.mor₂ ≫ e₁.hom.hom₃ = e₁.hom.hom₂ ≫ (L.mapTriangle.obj T₁').mor₂<VAR>comm₂' : T₂.mor₂ ≫ e₂.hom.hom₃ = e₂.hom.hom₂ ≫ (L.mapTriangle.obj T₂').mor₂<VAR>comm₃ : (L.mapTriangle.obj T₁').mor₃ ≫ (shiftFunctor D 1).map e₁.inv.hom₁ = e₁.inv.hom₃ ≫ T₁.mor₃<VAR>comm₃' : T₂.mor₃ ≫ (shiftFunctor D 1).map e₂.hom.hom₁ = e₂.hom.hom₃ ≫ (L.mapTriangle.obj T₂').mor₃<GOAL>∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor D 1).map a = c ≫ T₂.mor₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁸ : Category.{u_3, u_1} C<VAR>inst✝⁷ : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>inst✝⁶ : HasShift C ℤ<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝² : Pretriangulated C<VAR>inst✝¹ : HasShift D ℤ<VAR>inst✝ : L.CommShift ℤ<VAR>H : ∀ (T₁' T₂' : Triangle C), T₁' ∈ distinguishedTriangles → T₂' ∈ distinguishedTriangles → ∀ (a : L.obj T₁'.obj₁ ⟶ L.obj T₂'.obj₁) (b : L.obj T₁'.obj₂ ⟶ L.obj T₂'.obj₂), L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ → ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b<VAR>T₁ T₂ : Triangle D<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<VAR>T₁' : Triangle C<VAR>e₁ : T₁ ≅ L.mapTriangle.obj T₁'<VAR>hT₁' : T₁' ∈ distinguishedTriangles<VAR>T₂' : Triangle C<VAR>e₂ : T₂ ≅ L.mapTriangle.obj T₂'<VAR>hT₂' : T₂' ∈ distinguishedTriangles<VAR>comm₁ : L.map T₁'.mor₁ ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁<VAR>comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ L.map T₂'.mor₁<VAR>comm₂ : T₁.mor₂ ≫ e₁.hom.hom₃ = e₁.hom.hom₂ ≫ L.map T₁'.mor₂<VAR>comm₂' : T₂.mor₂ ≫ e₂.hom.hom₃ = e₂.hom.hom₂ ≫ L.map T₂'.mor₂<VAR>comm₃ : (L.map T₁'.mor₃ ≫ (L.commShiftIso 1).hom.app T₁'.obj₁) ≫ (shiftFunctor D 1).map e₁.inv.hom₁ = e₁.inv.hom₃ ≫ T₁.mor₃<VAR>comm₃' : T₂.mor₃ ≫ (shiftFunctor D 1).map e₂.hom.hom₁ = e₂.hom.hom₃ ≫ L.map T₂'.mor₃ ≫ (L.commShiftIso 1).hom.app T₂'.obj₁<GOAL>∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor D 1).map a = c ≫ T₂.mor₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁸ : Category.{u_3, u_1} C<VAR>inst✝⁷ : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>inst✝⁶ : HasShift C ℤ<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝² : Pretriangulated C<VAR>inst✝¹ : HasShift D ℤ<VAR>inst✝ : L.CommShift ℤ<VAR>H : ∀ (T₁' T₂' : Triangle C), T₁' ∈ distinguishedTriangles → T₂' ∈ distinguishedTriangles → ∀ (a : L.obj T₁'.obj₁ ⟶ L.obj T₂'.obj₁) (b : L.obj T₁'.obj₂ ⟶ L.obj T₂'.obj₂), L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ → ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b<VAR>T₁ T₂ : Triangle D<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<VAR>T₁' : Triangle C<VAR>e₁ : T₁ ≅ L.mapTriangle.obj T₁'<VAR>hT₁' : T₁' ∈ distinguishedTriangles<VAR>T₂' : Triangle C<VAR>e₂ : T₂ ≅ L.mapTriangle.obj T₂'<VAR>hT₂' : T₂' ∈ distinguishedTriangles<VAR>comm₁ : L.map T₁'.mor₁ ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁<VAR>comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ L.map T₂'.mor₁<VAR>comm₂ : T₁.mor₂ ≫ e₁.hom.hom₃ = e₁.hom.hom₂ ≫ L.map T₁'.mor₂<VAR>comm₂' : T₂.mor₂ ≫ e₂.hom.hom₃ = e₂.hom.hom₂ ≫ L.map T₂'.mor₂<VAR>comm₃' : T₂.mor₃ ≫ (shiftFunctor D 1).map e₂.hom.hom₁ = e₂.hom.hom₃ ≫ L.map T₂'.mor₃ ≫ (L.commShiftIso 1).hom.app T₂'.obj₁<VAR>comm₃ : L.map T₁'.mor₃ ≫ (L.commShiftIso 1).hom.app T₁'.obj₁ ≫ (shiftFunctor D 1).map e₁.inv.hom₁ = e₁.inv.hom₃ ≫ T₁.mor₃<GOAL>∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor D 1).map a = c ≫ T₂.mor₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁸ : Category.{u_3, u_1} C<VAR>inst✝⁷ : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>inst✝⁶ : HasShift C ℤ<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝² : Pretriangulated C<VAR>inst✝¹ : HasShift D ℤ<VAR>inst✝ : L.CommShift ℤ<VAR>H : ∀ (T₁' T₂' : Triangle C), T₁' ∈ distinguishedTriangles → T₂' ∈ distinguishedTriangles → ∀ (a : L.obj T₁'.obj₁ ⟶ L.obj T₂'.obj₁) (b : L.obj T₁'.obj₂ ⟶ L.obj T₂'.obj₂), L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ → ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b<VAR>T₁ T₂ : Triangle D<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<VAR>T₁' : Triangle C<VAR>e₁ : T₁ ≅ L.mapTriangle.obj T₁'<VAR>hT₁' : T₁' ∈ distinguishedTriangles<VAR>T₂' : Triangle C<VAR>e₂ : T₂ ≅ L.mapTriangle.obj T₂'<VAR>hT₂' : T₂' ∈ distinguishedTriangles<VAR>comm₁ : L.map T₁'.mor₁ ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁<VAR>comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ L.map T₂'.mor₁<VAR>comm₂ : T₁.mor₂ ≫ e₁.hom.hom₃ = e₁.hom.hom₂ ≫ L.map T₁'.mor₂<VAR>comm₂' : T₂.mor₂ ≫ e₂.hom.hom₃ = e₂.hom.hom₂ ≫ L.map T₂'.mor₂<VAR>comm₃' : T₂.mor₃ ≫ (shiftFunctor D 1).map e₂.hom.hom₁ = e₂.hom.hom₃ ≫ L.map T₂'.mor₃ ≫ (L.commShiftIso 1).hom.app T₂'.obj₁<VAR>comm₃ : L.map T₁'.mor₃ ≫ (L.commShiftIso 1).hom.app T₁'.obj₁ ≫ (shiftFunctor D 1).map e₁.inv.hom₁ = e₁.inv.hom₃ ≫ T₁.mor₃<VAR>φ : L.mapTriangle.obj T₁' ⟶ L.mapTriangle.obj T₂'<VAR>hφ₁ : φ.hom₁ = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁<VAR>hφ₂ : φ.hom₂ = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂<GOAL>∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor D 1).map a = c ≫ T₂.mor₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁸ : Category.{u_3, u_1} C<VAR>inst✝⁷ : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>inst✝⁶ : HasShift C ℤ<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝² : Pretriangulated C<VAR>inst✝¹ : HasShift D ℤ<VAR>inst✝ : L.CommShift ℤ<VAR>H : ∀ (T₁' T₂' : Triangle C), T₁' ∈ distinguishedTriangles → T₂' ∈ distinguishedTriangles → ∀ (a : L.obj T₁'.obj₁ ⟶ L.obj T₂'.obj₁) (b : L.obj T₁'.obj₂ ⟶ L.obj T₂'.obj₂), L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ → ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b<VAR>T₁ T₂ : Triangle D<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<VAR>T₁' : Triangle C<VAR>e₁ : T₁ ≅ L.mapTriangle.obj T₁'<VAR>hT₁' : T₁' ∈ distinguishedTriangles<VAR>T₂' : Triangle C<VAR>e₂ : T₂ ≅ L.mapTriangle.obj T₂'<VAR>hT₂' : T₂' ∈ distinguishedTriangles<VAR>comm₁ : L.map T₁'.mor₁ ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁<VAR>comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ L.map T₂'.mor₁<VAR>comm₂ : T₁.mor₂ ≫ e₁.hom.hom₃ = e₁.hom.hom₂ ≫ L.map T₁'.mor₂<VAR>comm₂' : T₂.mor₂ ≫ e₂.hom.hom₃ = e₂.hom.hom₂ ≫ L.map T₂'.mor₂<VAR>comm₃' : T₂.mor₃ ≫ (shiftFunctor D 1).map e₂.hom.hom₁ = e₂.hom.hom₃ ≫ L.map T₂'.mor₃ ≫ (L.commShiftIso 1).hom.app T₂'.obj₁<VAR>comm₃ : L.map T₁'.mor₃ ≫ (L.commShiftIso 1).hom.app T₁'.obj₁ ≫ (shiftFunctor D 1).map e₁.inv.hom₁ = e₁.inv.hom₃ ≫ T₁.mor₃<VAR>φ : L.mapTriangle.obj T₁' ⟶ L.mapTriangle.obj T₂'<VAR>hφ₁ : φ.hom₁ = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁<VAR>hφ₂ : φ.hom₂ = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂<VAR>h₂ : (L.mapTriangle.obj T₁').mor₂ ≫ φ.hom₃ = φ.hom₂ ≫ (L.mapTriangle.obj T₂').mor₂<GOAL>∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor D 1).map a = c ≫ T₂.mor₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁸ : Category.{u_3, u_1} C<VAR>inst✝⁷ : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>inst✝⁶ : HasShift C ℤ<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝² : Pretriangulated C<VAR>inst✝¹ : HasShift D ℤ<VAR>inst✝ : L.CommShift ℤ<VAR>H : ∀ (T₁' T₂' : Triangle C), T₁' ∈ distinguishedTriangles → T₂' ∈ distinguishedTriangles → ∀ (a : L.obj T₁'.obj₁ ⟶ L.obj T₂'.obj₁) (b : L.obj T₁'.obj₂ ⟶ L.obj T₂'.obj₂), L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ → ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b<VAR>T₁ T₂ : Triangle D<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<VAR>T₁' : Triangle C<VAR>e₁ : T₁ ≅ L.mapTriangle.obj T₁'<VAR>hT₁' : T₁' ∈ distinguishedTriangles<VAR>T₂' : Triangle C<VAR>e₂ : T₂ ≅ L.mapTriangle.obj T₂'<VAR>hT₂' : T₂' ∈ distinguishedTriangles<VAR>comm₁ : L.map T₁'.mor₁ ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁<VAR>comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ L.map T₂'.mor₁<VAR>comm₂ : T₁.mor₂ ≫ e₁.hom.hom₃ = e₁.hom.hom₂ ≫ L.map T₁'.mor₂<VAR>comm₂' : T₂.mor₂ ≫ e₂.hom.hom₃ = e₂.hom.hom₂ ≫ L.map T₂'.mor₂<VAR>comm₃' : T₂.mor₃ ≫ (shiftFunctor D 1).map e₂.hom.hom₁ = e₂.hom.hom₃ ≫ L.map T₂'.mor₃ ≫ (L.commShiftIso 1).hom.app T₂'.obj₁<VAR>comm₃ : L.map T₁'.mor₃ ≫ (L.commShiftIso 1).hom.app T₁'.obj₁ ≫ (shiftFunctor D 1).map e₁.inv.hom₁ = e₁.inv.hom₃ ≫ T₁.mor₃<VAR>φ : L.mapTriangle.obj T₁' ⟶ L.mapTriangle.obj T₂'<VAR>hφ₁ : φ.hom₁ = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁<VAR>hφ₂ : φ.hom₂ = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂<VAR>h₂ : (L.mapTriangle.obj T₁').mor₂ ≫ φ.hom₃ = φ.hom₂ ≫ (L.mapTriangle.obj T₂').mor₂<VAR>h₃ : (L.mapTriangle.obj T₁').mor₃ ≫ (shiftFunctor D 1).map φ.hom₁ = φ.hom₃ ≫ (L.mapTriangle.obj T₂').mor₃<GOAL>∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor D 1).map a = c ≫ T₂.mor₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁸ : Category.{u_3, u_1} C<VAR>inst✝⁷ : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>inst✝⁶ : HasShift C ℤ<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝² : Pretriangulated C<VAR>inst✝¹ : HasShift D ℤ<VAR>inst✝ : L.CommShift ℤ<VAR>H : ∀ (T₁' T₂' : Triangle C), T₁' ∈ distinguishedTriangles → T₂' ∈ distinguishedTriangles → ∀ (a : L.obj T₁'.obj₁ ⟶ L.obj T₂'.obj₁) (b : L.obj T₁'.obj₂ ⟶ L.obj T₂'.obj₂), L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ → ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b<VAR>T₁ T₂ : Triangle D<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<VAR>T₁' : Triangle C<VAR>e₁ : T₁ ≅ L.mapTriangle.obj T₁'<VAR>hT₁' : T₁' ∈ distinguishedTriangles<VAR>T₂' : Triangle C<VAR>e₂ : T₂ ≅ L.mapTriangle.obj T₂'<VAR>hT₂' : T₂' ∈ distinguishedTriangles<VAR>comm₁ : L.map T₁'.mor₁ ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁<VAR>comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ L.map T₂'.mor₁<VAR>comm₂ : T₁.mor₂ ≫ e₁.hom.hom₃ = e₁.hom.hom₂ ≫ L.map T₁'.mor₂<VAR>comm₂' : T₂.mor₂ ≫ e₂.hom.hom₃ = e₂.hom.hom₂ ≫ L.map T₂'.mor₂<VAR>comm₃' : T₂.mor₃ ≫ (shiftFunctor D 1).map e₂.hom.hom₁ = e₂.hom.hom₃ ≫ L.map T₂'.mor₃ ≫ (L.commShiftIso 1).hom.app T₂'.obj₁<VAR>comm₃ : L.map T₁'.mor₃ ≫ (L.commShiftIso 1).hom.app T₁'.obj₁ ≫ (shiftFunctor D 1).map e₁.inv.hom₁ = e₁.inv.hom₃ ≫ T₁.mor₃<VAR>φ : L.mapTriangle.obj T₁' ⟶ L.mapTriangle.obj T₂'<VAR>hφ₁ : φ.hom₁ = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁<VAR>hφ₂ : φ.hom₂ = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂<VAR>h₂ : L.map T₁'.mor₂ ≫ φ.hom₃ = φ.hom₂ ≫ L.map T₂'.mor₂<VAR>h₃ : (L.map T₁'.mor₃ ≫ (L.commShiftIso 1).hom.app T₁'.obj₁) ≫ (shiftFunctor D 1).map φ.hom₁ = φ.hom₃ ≫ L.map T₂'.mor₃ ≫ (L.commShiftIso 1).hom.app T₂'.obj₁<GOAL>∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor D 1).map a = c ≫ T₂.mor₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁸ : Category.{u_3, u_1} C<VAR>inst✝⁷ : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>inst✝⁶ : HasShift C ℤ<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝² : Pretriangulated C<VAR>inst✝¹ : HasShift D ℤ<VAR>inst✝ : L.CommShift ℤ<VAR>H : ∀ (T₁' T₂' : Triangle C), T₁' ∈ distinguishedTriangles → T₂' ∈ distinguishedTriangles → ∀ (a : L.obj T₁'.obj₁ ⟶ L.obj T₂'.obj₁) (b : L.obj T₁'.obj₂ ⟶ L.obj T₂'.obj₂), L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ → ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b<VAR>T₁ T₂ : Triangle D<VAR>a : T₁.obj₁ ⟶ T₂.obj₁<VAR>b : T₁.obj₂ ⟶ T₂.obj₂<VAR>fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁<VAR>T₁' : Triangle C<VAR>e₁ : T₁ ≅ L.mapTriangle.obj T₁'<VAR>hT₁' : T₁' ∈ distinguishedTriangles<VAR>T₂' : Triangle C<VAR>e₂ : T₂ ≅ L.mapTriangle.obj T₂'<VAR>hT₂' : T₂' ∈ distinguishedTriangles<VAR>comm₁ : L.map T₁'.mor₁ ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁<VAR>comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ L.map T₂'.mor₁<VAR>comm₂ : T₁.mor₂ ≫ e₁.hom.hom₃ = e₁.hom.hom₂ ≫ L.map T₁'.mor₂<VAR>comm₂' : T₂.mor₂ ≫ e₂.hom.hom₃ = e₂.hom.hom₂ ≫ L.map T₂'.mor₂<VAR>comm₃' : T₂.mor₃ ≫ (shiftFunctor D 1).map e₂.hom.hom₁ = e₂.hom.hom₃ ≫ L.map T₂'.mor₃ ≫ (L.commShiftIso 1).hom.app T₂'.obj₁<VAR>comm₃ : L.map T₁'.mor₃ ≫ (L.commShiftIso 1).hom.app T₁'.obj₁ ≫ (shiftFunctor D 1).map e₁.inv.hom₁ = e₁.inv.hom₃ ≫ T₁.mor₃<VAR>φ : L.mapTriangle.obj T₁' ⟶ L.mapTriangle.obj T₂'<VAR>hφ₁ : φ.hom₁ = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁<VAR>hφ₂ : φ.hom₂ = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂<VAR>h₂ : L.map T₁'.mor₂ ≫ φ.hom₃ = φ.hom₂ ≫ L.map T₂'.mor₂<VAR>h₃ : L.map T₁'.mor₃ ≫ (L.commShiftIso 1).hom.app T₁'.obj₁ ≫ (shiftFunctor D 1).map φ.hom₁ = φ.hom₃ ≫ L.map T₂'.mor₃ ≫ (L.commShiftIso 1).hom.app T₂'.obj₁<GOAL>∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor D 1).map a = c ≫ T₂.mor₃
<VAR>f✝ f g : ℝ → ℝ<VAR>hf✝ : GrowsPolynomially f<VAR>hg✝ : GrowsPolynomially g<VAR>hf' : 0 ≤ᶠ[atTop] f<VAR>hg' : 0 ≤ᶠ[atTop] g<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ > 0<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<VAR>c₃ : ℝ<VAR>hc₃_mem : c₃ > 0<VAR>c₄ : ℝ<VAR>left✝ : c₄ > 0<VAR>hg : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)<GOAL>∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => f x + g x) u ∈ Set.Icc (min c₁ c₃ * (fun x => f x + g x) x) (max c₂ c₄ * (fun x => f x + g x) x)
<VAR>f✝ f g : ℝ → ℝ<VAR>hf✝¹ : GrowsPolynomially f<VAR>hg✝¹ : GrowsPolynomially g<VAR>hf'✝ : 0 ≤ᶠ[atTop] f<VAR>hg'✝ : 0 ≤ᶠ[atTop] g<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ > 0<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hf✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<VAR>c₃ : ℝ<VAR>hc₃_mem : c₃ > 0<VAR>c₄ : ℝ<VAR>left✝ : c₄ > 0<VAR>hg✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)<VAR>x : ℝ<VAR>hf : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<VAR>hg : ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)<VAR>hf' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ f y<VAR>hg' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ g y<VAR>hx_pos : 0 ≤ x<GOAL>∀ u ∈ Set.Icc (b * x) x, f u + g u ∈ Set.Icc (min c₁ c₃ * (f x + g x)) (max c₂ c₄ * (f x + g x))
<VAR>f✝ f g : ℝ → ℝ<VAR>hf✝¹ : GrowsPolynomially f<VAR>hg✝¹ : GrowsPolynomially g<VAR>hf'✝ : 0 ≤ᶠ[atTop] f<VAR>hg'✝ : 0 ≤ᶠ[atTop] g<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ > 0<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hf✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<VAR>c₃ : ℝ<VAR>hc₃_mem : c₃ > 0<VAR>c₄ : ℝ<VAR>left✝ : c₄ > 0<VAR>hg✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)<VAR>x : ℝ<VAR>hf : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<VAR>hg : ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)<VAR>hf' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ f y<VAR>hg' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ g y<VAR>hx_pos : 0 ≤ x<VAR>u : ℝ<VAR>hu : u ∈ Set.Icc (b * x) x<GOAL>f u + g u ∈ Set.Icc (min c₁ c₃ * (f x + g x)) (max c₂ c₄ * (f x + g x))
<VAR>f✝ f g : ℝ → ℝ<VAR>hf✝¹ : GrowsPolynomially f<VAR>hg✝¹ : GrowsPolynomially g<VAR>hf'✝ : 0 ≤ᶠ[atTop] f<VAR>hg'✝ : 0 ≤ᶠ[atTop] g<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ > 0<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hf✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<VAR>c₃ : ℝ<VAR>hc₃_mem : c₃ > 0<VAR>c₄ : ℝ<VAR>left✝ : c₄ > 0<VAR>hg✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)<VAR>x : ℝ<VAR>hf : ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)<VAR>hg : ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₃ * g x) (c₄ * g x)<VAR>hf' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ f y<VAR>hg' : ∀ (y : ℝ), b * id x ≤ y → 0 y ≤ g y<VAR>hx_pos : 0 ≤ x<VAR>u : ℝ<VAR>hu : u ∈ Set.Icc (b * x) x<VAR>hbx : b * x ≤ x<GOAL>f u + g u ∈ Set.Icc (min c₁ c₃ * (f x + g x)) (max c₂ c₄ * (f x + g x))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>R : α → β → Prop<VAR>S : γ → δ → Prop<VAR>s1 : Computation α<VAR>s2 : Computation β<VAR>f1 : α → γ<VAR>f2 : β → δ<VAR>h1 : LiftRel R s1 s2<VAR>h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)<GOAL>LiftRel S (map f1 s1) (map f2 s2)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>R : α → β → Prop<VAR>S : γ → δ → Prop<VAR>s1 : Computation α<VAR>s2 : Computation β<VAR>f1 : α → γ<VAR>f2 : β → δ<VAR>h1 : LiftRel R s1 s2<VAR>h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)<GOAL>LiftRel S (s1.bind (pure ∘ f1)) (s2.bind (pure ∘ f2))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>R : α → β → Prop<VAR>S : γ → δ → Prop<VAR>s1 : Computation α<VAR>s2 : Computation β<VAR>f1 : α → γ<VAR>f2 : β → δ<VAR>h1 : LiftRel R s1 s2<VAR>h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)<GOAL>∀ {a : α} {b : β}, R a b → LiftRel S ((pure ∘ f1) a) ((pure ∘ f2) b)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>R : α → β → Prop<VAR>S : γ → δ → Prop<VAR>s1 : Computation α<VAR>s2 : Computation β<VAR>f1 : α → γ<VAR>f2 : β → δ<VAR>h1 : LiftRel R s1 s2<VAR>h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)<GOAL>∀ {a : α} {b : β}, R a b → ∃ a_2, a_2 ∈ pure (f1 a) ∧ S a_2 (f2 b)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>R : α → β → Prop<VAR>S : γ → δ → Prop<VAR>s1 : Computation α<VAR>s2 : Computation β<VAR>f1 : α → γ<VAR>f2 : β → δ<VAR>h1 : LiftRel R s1 s2<VAR>h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)<VAR>a : α<VAR>b : β<VAR>h : R a b<GOAL>∃ a_1, a_1 ∈ pure (f1 a) ∧ S a_1 (f2 b)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ : α<VAR>n : ℕ<VAR>a : α<GOAL>⌊↑n + a⌋ = ↑n + ⌊a⌋
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝³ : MulOneClass α<VAR>inst✝² : Zero α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : MulPosStrictMono α<VAR>hb : 0 < b<VAR>h : 1 < a<GOAL>b < a * b
<VAR>a✝ b c : Ordinal.{u}<VAR>h : b ≤ c<VAR>a : Ordinal.{u}<GOAL>b ♯ a ≤ c ♯ a
<VAR>a✝ b c : Ordinal.{u}<VAR>h✝ : b ≤ c<VAR>a : Ordinal.{u}<VAR>h : b < c<GOAL>b ♯ a ≤ c ♯ a
<VAR>a✝ b a : Ordinal.{u}<VAR>h : b ≤ b<GOAL>b ♯ a ≤ b ♯ a
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup X<VAR>inst✝¹ : NormedSpace ℝ X<VAR>inst✝ : HasContDiffBump E<VAR>c✝ : E<VAR>f✝ : ContDiffBump c✝<VAR>x : E<VAR>n : ℕ∞<VAR>c g : X → E<VAR>f : (x : X) → ContDiffBump (c x)<VAR>hc : ContDiff ℝ n c<VAR>hr : ContDiff ℝ n fun x => (f x).rIn<VAR>hR : ContDiff ℝ n fun x => (f x).rOut<VAR>hg : ContDiff ℝ n g<GOAL>ContDiff ℝ n fun x => ↑(f x) (g x)
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup X<VAR>inst✝¹ : NormedSpace ℝ X<VAR>inst✝ : HasContDiffBump E<VAR>c✝ : E<VAR>f✝ : ContDiffBump c✝<VAR>x : E<VAR>n : ℕ∞<VAR>c g : X → E<VAR>f : (x : X) → ContDiffBump (c x)<VAR>hc : ∀ (x : X), ContDiffAt ℝ n c x<VAR>hr : ∀ (x : X), ContDiffAt ℝ n (fun x => (f x).rIn) x<VAR>hR : ∀ (x : X), ContDiffAt ℝ n (fun x => (f x).rOut) x<VAR>hg : ∀ (x : X), ContDiffAt ℝ n g x<GOAL>∀ (x : X), ContDiffAt ℝ n (fun x => ↑(f x) (g x)) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>u v w : Set α<VAR>hu : MeasurableSet u<VAR>hv : MeasurableSet v<VAR>hw : MeasurableSet w<VAR>hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u<VAR>hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v<VAR>hs : ↑s (u ∆ v) = 0<GOAL>↑s (w ∩ u) = ↑s (w ∩ v)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>u v w : Set α<VAR>hu : MeasurableSet u<VAR>hv : MeasurableSet v<VAR>hw : MeasurableSet w<VAR>hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u<VAR>hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v<VAR>hs : ↑s (u ∆ v) = 0<VAR>hwuv : ↑s ((w ∩ u) ∆ (w ∩ v)) = 0<GOAL>↑s (w ∩ u) = ↑s (w ∩ v)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>u v w : Set α<VAR>hu : MeasurableSet u<VAR>hv : MeasurableSet v<VAR>hw : MeasurableSet w<VAR>hsu : VectorMeasure.restrict 0 u ≤ VectorMeasure.restrict s u<VAR>hsv : VectorMeasure.restrict 0 v ≤ VectorMeasure.restrict s v<VAR>hs : ↑s (u ∆ v) = 0<VAR>hwuv : ↑s ((w ∩ u) ∆ (w ∩ v)) = 0<VAR>huv : ↑s ((w ∩ u) \ (w ∩ v)) = 0<VAR>hvu : ↑s ((w ∩ v) \ (w ∩ u)) = 0<GOAL>↑s (w ∩ u) = ↑s (w ∩ v)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁵ : CommSemiring R<VAR>inst✝¹⁴ : StarRing R<VAR>inst✝¹³ : MetricSpace R<VAR>inst✝¹² : TopologicalSemiring R<VAR>inst✝¹¹ : ContinuousStar R<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : Ring A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : ContinuousFunctionalCalculus R p<VAR>f✝ g : R → R<VAR>a✝ : A<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>hf✝ : autoParam (ContinuousOn f✝ (spectrum R a✝)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a✝)) _auto✝<VAR>inst✝⁵ : UniqueContinuousFunctionalCalculus R A<VAR>S : Type u_3<VAR>inst✝⁴ : SMul S R<VAR>inst✝³ : ContinuousConstSMul S R<VAR>inst✝² : SMulZeroClass S A<VAR>inst✝¹ : IsScalarTower S R A<VAR>inst✝ : IsScalarTower S R (R → R)<VAR>s : S<VAR>f : R → R<VAR>a : A<VAR>hf : autoParam (ContinuousOn f ((fun x => s • x) '' spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>cfc (fun x => f (s • x)) a = cfc f (s • a)
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>inst✝⁶ : ConcreteCategory C<VAR>inst✝⁵ : HasForget₂ C Ab<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : (forget₂ C Ab).Additive<VAR>inst✝² : (forget₂ C Ab).PreservesHomology<VAR>inst✝¹ : HasZeroObject C<VAR>S : ShortComplex C<VAR>inst✝ : S.HasHomology<GOAL>S.Exact ↔ ∀ (x₂ : ↑((forget₂ C Ab).obj S.X₂)), ((forget₂ C Ab).map S.g) x₂ = 0 → ∃ x₁, ((forget₂ C Ab).map S.f) x₁ = x₂
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>inst✝⁶ : ConcreteCategory C<VAR>inst✝⁵ : HasForget₂ C Ab<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : (forget₂ C Ab).Additive<VAR>inst✝² : (forget₂ C Ab).PreservesHomology<VAR>inst✝¹ : HasZeroObject C<VAR>S : ShortComplex C<VAR>inst✝ : S.HasHomology<GOAL>(∀ (x₂ : ↑(S.map (forget₂ C Ab)).X₂), (S.map (forget₂ C Ab)).g x₂ = 0 → ∃ x₁, (S.map (forget₂ C Ab)).f x₁ = x₂) ↔ ∀ (x₂ : ↑((forget₂ C Ab).obj S.X₂)), ((forget₂ C Ab).map S.g) x₂ = 0 → ∃ x₁, ((forget₂ C Ab).map S.f) x₁ = x₂
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α✝ : ι → Type u_3<VAR>inst✝³ : Fintype ι<VAR>m✝¹ : (i : ι) → OuterMeasure (α✝ i)<VAR>m✝ : (i : ι) → MeasurableSpace (α✝ i)<VAR>μ✝ : (i : ι) → Measure (α✝ i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>inst✝¹ : Fintype ι'<VAR>α : Type u<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<GOAL>MeasurePreserving (⇑MeasurableEquiv.finTwoArrow) (Measure.pi fun x => μ) (μ.prod μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝¹ : DivisionMonoid K<VAR>inst✝ : HasDistribNeg K<VAR>a✝ b✝ a b : K<GOAL>-(b / a) = -b / a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : SigmaCompactSpace X<VAR>e : Y → X<VAR>he : ClosedEmbedding e<GOAL>⋃ n, (fun n => e ⁻¹' compactCovering X n) n = univ
<VAR>b : ℕ<VAR>hb : 1 < b<VAR>x : ℕ<VAR>hx : 1 < x<GOAL>b ^ (clog b x).pred < x
<VAR>b : ℕ<VAR>hb : 1 < b<VAR>x : ℕ<VAR>hx : 1 < x<GOAL>(clog b x).pred < clog b x
<VAR>T : ℝ<VAR>n : ℤ<GOAL>(fourier n) 0 = 1
<VAR>b o : Ordinal.{u_1}<VAR>ho : o ≠ 0<GOAL>0 < o / b ^ log b o
<VAR>o : Ordinal.{u_1}<VAR>ho : o ≠ 0<GOAL>0 < o / 0 ^ log 0 o