ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝⁶ : Semiring R<VAR>ι : Type u_2<VAR>V : Type u<VAR>inst✝⁵ : Category.{v, u} V<VAR>inst✝⁴ : Preadditive V<VAR>c✝ : ComplexShape ι<VAR>W : Type u_3<VAR>inst✝³ : Category.{?u.37324, u_3} W<VAR>inst✝² : Preadditive W<VAR>F G : V ⥤ W<VAR>inst✝¹ : F.Additive<VAR>inst✝ : G.Additive<VAR>α : F ⟶ G<VAR>c : ComplexShape ι<VAR>C D : HomologicalComplex V c<VAR>f✝ : { as := C } ⟶ { as := D }<VAR>f : C ⟶ D<GOAL>(F.mapHomotopyCategory c).map (Quot.mk (Quotient.CompClosure (homotopic V c)) f) ≫ (fun C => (HomotopyCategory.quotient W c).map ((mapHomologicalComplex α c).app C.as)) { as := D } = (fun C => (HomotopyCategory.quotient W c).map ((mapHomologicalComplex α c).app C.as)) { as := C } ≫ (G.mapHomotopyCategory c).map (Quot.mk (Quotient.CompClosure (homotopic V c)) f)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>p : Finset (Finset α) → Prop<VAR>𝒜 : Finset (Finset α)<VAR>empty : p ∅<VAR>singleton_empty : p {∅}<VAR>subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜<VAR>u : Finset α := 𝒜.sup id<GOAL>p 𝒜
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>p : Finset (Finset α) → Prop<VAR>𝒜 : Finset (Finset α)<VAR>empty : p ∅<VAR>singleton_empty : p {∅}<VAR>subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜<VAR>u : Finset α := 𝒜.sup id<VAR>hu : ∀ s ∈ 𝒜, s ⊆ u<GOAL>p 𝒜
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>p : Finset (Finset α) → Prop<VAR>𝒜 : Finset (Finset α)<VAR>empty : p ∅<VAR>singleton_empty : p {∅}<VAR>subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜<VAR>u : Finset α<VAR>hu : ∀ s ∈ 𝒜, s ⊆ u<GOAL>p 𝒜
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>p : Finset (Finset α) → Prop<VAR>empty : p ∅<VAR>singleton_empty : p {∅}<VAR>subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜<VAR>𝒜 : Finset (Finset α)<VAR>hu : ∀ s ∈ 𝒜, s ⊆ ∅<GOAL>p 𝒜
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a✝¹ : α<VAR>p : Finset (Finset α) → Prop<VAR>empty : p ∅<VAR>singleton_empty : p {∅}<VAR>subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜<VAR>a : α<VAR>u : Finset α<VAR>a✝ : a ∉ u<VAR>ih : ∀ (𝒜 : Finset (Finset α)), (∀ s ∈ 𝒜, s ⊆ u) → p 𝒜<VAR>𝒜 : Finset (Finset α)<VAR>hu : ∀ s ∈ 𝒜, s ⊆ insert a u<GOAL>p 𝒜
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝³ : Semiring R₁<VAR>inst✝² : Semiring R₂<VAR>inst✝¹ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>σ : R₁ →+* R₂<VAR>σ' : R₂ →+* R₁<VAR>inst✝ : RingHomInvPair σ σ'<VAR>x : R₂<GOAL>σ (σ' x) = x
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝³ : Semiring R₁<VAR>inst✝² : Semiring R₂<VAR>inst✝¹ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>σ : R₁ →+* R₂<VAR>σ' : R₂ →+* R₁<VAR>inst✝ : RingHomInvPair σ σ'<VAR>x : R₂<GOAL>(RingHom.id R₂) x = x
<VAR>F : Type w<VAR>R : Type u<VAR>S : Type v<VAR>T : Type u_1<VAR>inst✝⁴ : NonUnitalNonAssocRing R<VAR>inst✝³ : NonUnitalNonAssocRing S<VAR>inst✝² : NonUnitalNonAssocRing T<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : NonUnitalRingHomClass F R S<VAR>g : S →ₙ+* T<VAR>f✝ : R →ₙ+* S<VAR>s : NonUnitalSubring R<VAR>f : R →ₙ+* S<GOAL>↑f.range = ↑⊤ ↔ Set.range ⇑f = Set.univ
<VAR>R✝ : Type u_1<VAR>inst✝¹ : Semiring R✝<VAR>r✝ : R✝<VAR>f✝ : R✝[X]<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>f : R[X]<VAR>r s : R<GOAL>(taylor r) ((taylor s) f) = (taylor (r + s)) f
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : GroupWithZero α<VAR>s t : Finset α<VAR>hs : s.Nonempty<GOAL>0 ⊆ 0 / s
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>h : x ≠ 0<VAR>r : ℝ<GOAL>(o.oangle x (x + r • (o.rotation ↑(π / 2)) x)).tan = r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>h : IntegrableOn f s (μ.restrict t)<GOAL>IntegrableOn f (s ∩ t) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>h : IntegrableOn f s (μ.restrict t)<VAR>this : IntegrableOn f (s ∩ t) (μ.restrict t)<GOAL>IntegrableOn f (s ∩ t) μ
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>inst✝ : Inhabited I<VAR>l : Products I<VAR>hl : ↑l ≠ []<VAR>hlh : (↑l).head! = term I ho<VAR>hlc : List.Chain' (fun x x_1 => x > x_1) (term I ho :: ↑l.Tail)<GOAL>(Linear_CC' C hsC ho) (eval C l) = eval (C' C ho) l.Tail
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>inst✝ : Inhabited I<VAR>l : Products I<VAR>hl : ↑l ≠ []<VAR>hlh : (↑l).head! = term I ho<VAR>hlc : List.Chain' (fun x x_1 => x > x_1) (term I ho :: ↑l.Tail)<GOAL>(Linear_CC' C hsC ho) (e C (term I ho) * eval C ⟨↑l.Tail, ⋯⟩) = eval (C' C ho) (Tail ⟨term I ho :: ↑l.Tail, hlc⟩)
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>inst✝ : Inhabited I<VAR>l : Products I<VAR>hl : ↑l ≠ []<VAR>hlh : (↑l).head! = term I ho<VAR>hlc : List.Chain' (fun x x_1 => x > x_1) (term I ho :: ↑l.Tail)<VAR>x : ↑(C' C ho)<GOAL>((Linear_CC' C hsC ho) (e C (term I ho) * eval C ⟨↑l.Tail, ⋯⟩)) x = (eval (C' C ho) (Tail ⟨term I ho :: ↑l.Tail, hlc⟩)) x
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>inst✝ : Inhabited I<VAR>l : Products I<VAR>hl : ↑l ≠ []<VAR>hlh : (↑l).head! = term I ho<VAR>hlc : List.Chain' (fun x x_1 => x > x_1) (term I ho :: ↑l.Tail)<VAR>x : ↑(C' C ho)<GOAL>(e C (term I ho)) (CC'₁ C hsC ho x) * (eval C l.Tail) (CC'₁ C hsC ho x) - (e C (term I ho)) (CC'₀ C ho x) * (eval C l.Tail) (CC'₀ C ho x) = (eval (C' C ho) (Tail ⟨term I ho :: ↑l.Tail, hlc⟩)) x
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>inst✝ : Inhabited I<VAR>l : Products I<VAR>hl : ↑l ≠ []<VAR>hlh : (↑l).head! = term I ho<VAR>hlc : List.Chain' (fun x x_1 => x > x_1) (term I ho :: ↑l.Tail)<VAR>x : ↑(C' C ho)<GOAL>(((e C (term I ho)) ⟨SwapTrue o ↑x, ⋯⟩ * if ∀ i ∈ ↑l.Tail, ↑⟨SwapTrue o ↑x, ⋯⟩ i = true then 1 else 0) - (e C (term I ho)) ⟨↑x, ⋯⟩ * if ∀ i ∈ ↑l.Tail, ↑⟨↑x, ⋯⟩ i = true then 1 else 0) = if ∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true then 1 else 0
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>inst✝ : Inhabited I<VAR>l : Products I<VAR>hl : ↑l ≠ []<VAR>hlh : (↑l).head! = term I ho<VAR>hlc : List.Chain' (fun x x_1 => x > x_1) (term I ho :: ↑l.Tail)<VAR>x : ↑(C' C ho)<GOAL>((if ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true then (e C (term I ho)) ⟨SwapTrue o ↑x, ⋯⟩ else 0) - if ∀ i ∈ ↑l.Tail, ↑x i = true then (e C (term I ho)) ⟨↑x, ⋯⟩ else 0) = if ∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true then 1 else 0
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>inst✝ : Inhabited I<VAR>l : Products I<VAR>hl : ↑l ≠ []<VAR>hlh : (↑l).head! = term I ho<VAR>hlc : List.Chain' (fun x x_1 => x > x_1) (term I ho :: ↑l.Tail)<VAR>x : ↑(C' C ho)<VAR>hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i<GOAL>((if ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true then (e C (term I ho)) ⟨SwapTrue o ↑x, ⋯⟩ else 0) - if ∀ i ∈ ↑l.Tail, ↑x i = true then (e C (term I ho)) ⟨↑x, ⋯⟩ else 0) = if ∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true then 1 else 0
<VAR>I : Type u<VAR>inst✝² : LinearOrder I<VAR>inst✝¹ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>inst✝ : Inhabited I<VAR>l : Products I<VAR>hl : ↑l ≠ []<VAR>hlh : (↑l).head! = term I ho<VAR>hlc : List.Chain' (fun x x_1 => x > x_1) (term I ho :: ↑l.Tail)<VAR>x : ↑(C' C ho)<VAR>hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i<VAR>H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true<GOAL>((if ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true then (e C (term I ho)) ⟨SwapTrue o ↑x, ⋯⟩ else 0) - if ∀ i ∈ ↑l.Tail, ↑x i = true then (e C (term I ho)) ⟨↑x, ⋯⟩ else 0) = if ∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true then 1 else 0
<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>φ : S₁ ⟶ S₂<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<GOAL>S₁.homologyπ ≫ homologyMap φ = cyclesMap φ ≫ S₂.homologyπ
<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>φ : S₁ ⟶ S₂<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<GOAL>S₁.homologyπ ≫ S₁.leftHomologyIso.inv ≫ leftHomologyMap φ = cyclesMap φ ≫ S₂.leftHomologyπ
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>V₃ : Type u_5<VAR>inst✝⁷ : SeminormedAddCommGroup V<VAR>inst✝⁶ : SeminormedAddCommGroup W<VAR>inst✝⁵ : SeminormedAddCommGroup V₁<VAR>inst✝⁴ : SeminormedAddCommGroup V₂<VAR>inst✝³ : SeminormedAddCommGroup V₃<VAR>f : NormedAddGroupHom V W<VAR>W₁ : Type u_6<VAR>W₂ : Type u_7<VAR>W₃ : Type u_8<VAR>inst✝² : SeminormedAddCommGroup W₁<VAR>inst✝¹ : SeminormedAddCommGroup W₂<VAR>inst✝ : SeminormedAddCommGroup W₃<VAR>g : NormedAddGroupHom V W<VAR>f₁ g₁ : NormedAddGroupHom V₁ W₁<VAR>f₂ g₂ : NormedAddGroupHom V₂ W₂<VAR>f₃ g₃ : NormedAddGroupHom V₃ W₃<VAR>ψ : NormedAddGroupHom V₁ ↥(f.equalizer g)<GOAL>f.comp ((ι f g).comp ψ) = g.comp ((ι f g).comp ψ)
<VAR>σ₁ : Type u_1<VAR>σ₂ : Type u_2<VAR>f₁ : σ₁ → Option σ₁<VAR>f₂ : σ₂ → Option σ₂<VAR>tr : σ₁ → σ₂ → Prop<VAR>H : Respects f₁ f₂ tr<VAR>a₁ b₁ : σ₁<VAR>a₂ : σ₂<VAR>aa : tr a₁ a₂<VAR>ab : b₁ ∈ eval f₁ a₁<GOAL>∃ b₂, tr b₁ b₂ ∧ b₂ ∈ eval f₂ a₂
<VAR>σ₁ : Type u_1<VAR>σ₂ : Type u_2<VAR>f₁ : σ₁ → Option σ₁<VAR>f₂ : σ₂ → Option σ₂<VAR>tr : σ₁ → σ₂ → Prop<VAR>H : Respects f₁ f₂ tr<VAR>a₁ b₁ : σ₁<VAR>a₂ : σ₂<VAR>aa : tr a₁ a₂<VAR>ab✝ : b₁ ∈ eval f₁ a₁<VAR>ab : Reaches f₁ a₁ b₁<VAR>b0 : f₁ b₁ = none<GOAL>∃ b₂, tr b₁ b₂ ∧ b₂ ∈ eval f₂ a₂
<VAR>σ₁ : Type u_1<VAR>σ₂ : Type u_2<VAR>f₁ : σ₁ → Option σ₁<VAR>f₂ : σ₂ → Option σ₂<VAR>tr : σ₁ → σ₂ → Prop<VAR>H : Respects f₁ f₂ tr<VAR>a₁ b₁ : σ₁<VAR>a₂ : σ₂<VAR>aa : tr a₁ a₂<VAR>ab✝¹ : b₁ ∈ eval f₁ a₁<VAR>ab✝ : Reaches f₁ a₁ b₁<VAR>b0 : f₁ b₁ = none<VAR>b₂ : σ₂<VAR>bb : tr b₁ b₂<VAR>ab : Reaches f₂ a₂ b₂<GOAL>∃ b₂, tr b₁ b₂ ∧ b₂ ∈ eval f₂ a₂
<VAR>σ₁ : Type u_1<VAR>σ₂ : Type u_2<VAR>f₁ : σ₁ → Option σ₁<VAR>f₂ : σ₂ → Option σ₂<VAR>tr : σ₁ → σ₂ → Prop<VAR>H : Respects f₁ f₂ tr<VAR>a₁ b₁ : σ₁<VAR>a₂ : σ₂<VAR>aa : tr a₁ a₂<VAR>ab✝¹ : b₁ ∈ eval f₁ a₁<VAR>ab✝ : Reaches f₁ a₁ b₁<VAR>b0 : f₁ b₁ = none<VAR>b₂ : σ₂<VAR>bb : tr b₁ b₂<VAR>ab : Reaches f₂ a₂ b₂<GOAL>f₂ b₂ = none
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<GOAL>Nat.card (α × β) = Nat.card α * Nat.card β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>p : α → Prop<GOAL>(∃ x ∈ insert a s, p x) ↔ p a ∨ ∃ x ∈ s, p x
<VAR>x y : ℝ<GOAL>Real.toEReal ⁻¹' Icc ↑x ↑y = Icc x y
<VAR>x y : ℝ<GOAL>Real.toEReal ⁻¹' (Ici ↑x ∩ Iic ↑y) = Ici x ∩ Iic y
<VAR>α : Type u_1<GOAL>nil.lists = ↑[[]]
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : Fintype ι'<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>b : Basis ι ℝ E<VAR>e : ι ≃ ι'<GOAL>(b.reindex e).addHaar = b.addHaar
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>i : ι<VAR>r : A<VAR>hr : r ∈ ⊥<GOAL>↑(((decompose 𝒜) r) i) ∈ ⊥
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>i : ι<VAR>r : A<VAR>hr : r = 0<GOAL>↑(((decompose 𝒜) r) i) ∈ ⊥
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>i : ι<VAR>r : A<VAR>hr : r = 0<GOAL>↑0 ∈ ⊥
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝ : Monoid α<VAR>a✝ : α<VAR>n : ℕ<VAR>a : α<GOAL>IsSquare (a ^ (n + n))
<VAR>G : Type w<VAR>inst✝¹ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝ : R1Space G<VAR>U : ℕ → Opens G<VAR>h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), (fun s => ↑(μ.toFun s)) (t.sup K) ≤ ∑ i ∈ t, (fun s => ↑(μ.toFun s)) (K i)<GOAL>μ.innerContent (⨆ i, U i) ≤ ∑' (i : ℕ), μ.innerContent (U i)
<VAR>G : Type w<VAR>inst✝¹ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝ : R1Space G<VAR>U : ℕ → Opens G<VAR>h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), (fun s => ↑(μ.toFun s)) (t.sup K) ≤ ∑ i ∈ t, (fun s => ↑(μ.toFun s)) (K i)<VAR>K : Compacts G<VAR>hK : ↑K ⊆ ↑(⨆ i, U i)<GOAL>(fun s => ↑(μ.toFun s)) K ≤ ∑' (i : ℕ), μ.innerContent (U i)
<VAR>G : Type w<VAR>inst✝¹ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝ : R1Space G<VAR>U : ℕ → Opens G<VAR>h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), (fun s => ↑(μ.toFun s)) (t.sup K) ≤ ∑ i ∈ t, (fun s => ↑(μ.toFun s)) (K i)<VAR>K : Compacts G<VAR>hK : ↑K ⊆ ↑(⨆ i, U i)<VAR>t : Finset ℕ<VAR>ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)<GOAL>(fun s => ↑(μ.toFun s)) K ≤ ∑' (i : ℕ), μ.innerContent (U i)
<VAR>G : Type w<VAR>inst✝¹ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝ : R1Space G<VAR>U : ℕ → Opens G<VAR>h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), (fun s => ↑(μ.toFun s)) (t.sup K) ≤ ∑ i ∈ t, (fun s => ↑(μ.toFun s)) (K i)<VAR>K : Compacts G<VAR>hK : ↑K ⊆ ↑(⨆ i, U i)<VAR>t : Finset ℕ<VAR>ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)<VAR>K' : ℕ → Set G<VAR>h1K' : ∀ (i : ℕ), IsCompact (K' i)<VAR>h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i<VAR>h3K' : ↑K = ⋃ i ∈ t, K' i<GOAL>(fun s => ↑(μ.toFun s)) K ≤ ∑' (i : ℕ), μ.innerContent (U i)
<VAR>G : Type w<VAR>inst✝¹ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝ : R1Space G<VAR>U : ℕ → Opens G<VAR>h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), (fun s => ↑(μ.toFun s)) (t.sup K) ≤ ∑ i ∈ t, (fun s => ↑(μ.toFun s)) (K i)<VAR>K : Compacts G<VAR>hK : ↑K ⊆ ↑(⨆ i, U i)<VAR>t : Finset ℕ<VAR>ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)<VAR>K' : ℕ → Set G<VAR>h1K' : ∀ (i : ℕ), IsCompact (K' i)<VAR>h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i<VAR>h3K' : ↑K = ⋃ i ∈ t, K' i<VAR>L : ℕ → Compacts G := fun n => { carrier := K' n, isCompact' := ⋯ }<GOAL>(fun s => ↑(μ.toFun s)) K ≤ ∑' (i : ℕ), μ.innerContent (U i)
<VAR>G : Type w<VAR>inst✝¹ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝ : R1Space G<VAR>U : ℕ → Opens G<VAR>h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), (fun s => ↑(μ.toFun s)) (t.sup K) ≤ ∑ i ∈ t, (fun s => ↑(μ.toFun s)) (K i)<VAR>K : Compacts G<VAR>hK : ↑K ⊆ ↑(⨆ i, U i)<VAR>t : Finset ℕ<VAR>ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)<VAR>K' : ℕ → Set G<VAR>h1K' : ∀ (i : ℕ), IsCompact (K' i)<VAR>h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i<VAR>h3K' : ↑K = ⋃ i ∈ t, K' i<VAR>L : ℕ → Compacts G := fun n => { carrier := K' n, isCompact' := ⋯ }<GOAL>K = t.sup L
<VAR>G : Type w<VAR>inst✝¹ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝ : R1Space G<VAR>U : ℕ → Opens G<VAR>h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), (fun s => ↑(μ.toFun s)) (t.sup K) ≤ ∑ i ∈ t, (fun s => ↑(μ.toFun s)) (K i)<VAR>K : Compacts G<VAR>hK : ↑K ⊆ ↑(⨆ i, U i)<VAR>t : Finset ℕ<VAR>ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)<VAR>K' : ℕ → Set G<VAR>h1K' : ∀ (i : ℕ), IsCompact (K' i)<VAR>h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i<VAR>h3K' : ↑K = ⋃ i ∈ t, K' i<VAR>L : ℕ → Compacts G := fun n => { carrier := K' n, isCompact' := ⋯ }<GOAL>∑ i ∈ t, (fun s => ↑(μ.toFun s)) (L i) ≤ ∑' (i : ℕ), μ.innerContent (U i)
<VAR>G : Type w<VAR>inst✝¹ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝ : R1Space G<VAR>U : ℕ → Opens G<VAR>h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), (fun s => ↑(μ.toFun s)) (t.sup K) ≤ ∑ i ∈ t, (fun s => ↑(μ.toFun s)) (K i)<VAR>K : Compacts G<VAR>hK : ↑K ⊆ ↑(⨆ i, U i)<VAR>t : Finset ℕ<VAR>ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)<VAR>K' : ℕ → Set G<VAR>h1K' : ∀ (i : ℕ), IsCompact (K' i)<VAR>h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i<VAR>h3K' : ↑K = ⋃ i ∈ t, K' i<VAR>L : ℕ → Compacts G := fun n => { carrier := K' n, isCompact' := ⋯ }<GOAL>∀ i ∈ t, (fun s => ↑(μ.toFun s)) (L i) ≤ μ.innerContent (U i)
<VAR>G : Type w<VAR>inst✝¹ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝ : R1Space G<VAR>U : ℕ → Opens G<VAR>h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), (fun s => ↑(μ.toFun s)) (t.sup K) ≤ ∑ i ∈ t, (fun s => ↑(μ.toFun s)) (K i)<VAR>K : Compacts G<VAR>hK : ↑K ⊆ ↑(⨆ i, U i)<VAR>t : Finset ℕ<VAR>ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)<VAR>K' : ℕ → Set G<VAR>h1K' : ∀ (i : ℕ), IsCompact (K' i)<VAR>h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i<VAR>h3K' : ↑K = ⋃ i ∈ t, K' i<VAR>L : ℕ → Compacts G := fun n => { carrier := K' n, isCompact' := ⋯ }<VAR>i : ℕ<VAR>a✝ : i ∈ t<GOAL>(fun s => ↑(μ.toFun s)) (L i) ≤ μ.innerContent (U i)
<VAR>G : Type w<VAR>inst✝¹ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝ : R1Space G<VAR>U : ℕ → Opens G<VAR>h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), (fun s => ↑(μ.toFun s)) (t.sup K) ≤ ∑ i ∈ t, (fun s => ↑(μ.toFun s)) (K i)<VAR>K : Compacts G<VAR>hK : ↑K ⊆ ↑(⨆ i, U i)<VAR>t : Finset ℕ<VAR>ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)<VAR>K' : ℕ → Set G<VAR>h1K' : ∀ (i : ℕ), IsCompact (K' i)<VAR>h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i<VAR>h3K' : ↑K = ⋃ i ∈ t, K' i<VAR>L : ℕ → Compacts G := fun n => { carrier := K' n, isCompact' := ⋯ }<VAR>i : ℕ<VAR>a✝ : i ∈ t<GOAL>(fun s => ↑(μ.toFun s)) (L i) ≤ ⨆ (_ : ↑(L i) ⊆ ↑(U i)), (fun s => ↑(μ.toFun s)) (L i)
<VAR>G : Type w<VAR>inst✝¹ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝ : R1Space G<VAR>U : ℕ → Opens G<VAR>h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), (fun s => ↑(μ.toFun s)) (t.sup K) ≤ ∑ i ∈ t, (fun s => ↑(μ.toFun s)) (K i)<VAR>K : Compacts G<VAR>hK : ↑K ⊆ ↑(⨆ i, U i)<VAR>t : Finset ℕ<VAR>ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)<VAR>K' : ℕ → Set G<VAR>h1K' : ∀ (i : ℕ), IsCompact (K' i)<VAR>h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i<VAR>h3K' : ↑K = ⋃ i ∈ t, K' i<VAR>L : ℕ → Compacts G := fun n => { carrier := K' n, isCompact' := ⋯ }<VAR>i : ℕ<VAR>a✝ : i ∈ t<GOAL>(fun s => ↑(μ.toFun s)) (L i) ≤ (fun s => ↑(μ.toFun s)) (L i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝¹⁶ : TopologicalSpace α<VAR>inst✝¹⁵ : AddCommGroup α<VAR>inst✝¹⁴ : TopologicalAddGroup α<VAR>inst✝¹³ : TopologicalSpace β<VAR>inst✝¹² : AddCommGroup β<VAR>inst✝¹¹ : TopologicalAddGroup β<VAR>inst✝¹⁰ : TopologicalSpace γ<VAR>inst✝⁹ : AddCommGroup γ<VAR>inst✝⁸ : TopologicalAddGroup γ<VAR>inst✝⁷ : TopologicalSpace δ<VAR>inst✝⁶ : AddCommGroup δ<VAR>inst✝⁵ : TopologicalAddGroup δ<VAR>inst✝⁴ : UniformSpace G<VAR>inst✝³ : AddCommGroup G<VAR>inst✝² : UniformAddGroup G<VAR>inst✝¹ : T0Space G<VAR>inst✝ : CompleteSpace G<VAR>e : β →+ α<VAR>de : DenseInducing ⇑e<VAR>f : δ →+ γ<VAR>df : DenseInducing ⇑f<VAR>φ : β →+ δ →+ G<VAR>hφ : Continuous fun p => (φ p.1) p.2<VAR>W' : Set G<VAR>W'_nhd : W' ∈ 𝓝 0<GOAL>Continuous (⋯.extend fun p => (φ p.1) p.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝¹⁶ : TopologicalSpace α<VAR>inst✝¹⁵ : AddCommGroup α<VAR>inst✝¹⁴ : TopologicalAddGroup α<VAR>inst✝¹³ : TopologicalSpace β<VAR>inst✝¹² : AddCommGroup β<VAR>inst✝¹¹ : TopologicalAddGroup β<VAR>inst✝¹⁰ : TopologicalSpace γ<VAR>inst✝⁹ : AddCommGroup γ<VAR>inst✝⁸ : TopologicalAddGroup γ<VAR>inst✝⁷ : TopologicalSpace δ<VAR>inst✝⁶ : AddCommGroup δ<VAR>inst✝⁵ : TopologicalAddGroup δ<VAR>inst✝⁴ : UniformSpace G<VAR>inst✝³ : AddCommGroup G<VAR>inst✝² : UniformAddGroup G<VAR>inst✝¹ : T0Space G<VAR>inst✝ : CompleteSpace G<VAR>e : β →+ α<VAR>de : DenseInducing ⇑e<VAR>f : δ →+ γ<VAR>df : DenseInducing ⇑f<VAR>φ : β →+ δ →+ G<VAR>hφ : Continuous fun p => (φ p.1) p.2<VAR>W' : Set G<VAR>W'_nhd : W' ∈ 𝓝 0<GOAL>∀ (b : α × γ), Cauchy (map (fun p => (φ p.1) p.2) (comap (fun p => (e p.1, f p.2)) (𝓝 b)))
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>W X Y Z X₁ X₂ X₃ Y₁ Y₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₁<VAR>f₃ : X₂ ⟶ Y₂<VAR>f₄ : X₃ ⟶ Y₂<VAR>inst✝⁵ : HasPullback f₁ f₂<VAR>inst✝⁴ : HasPullback f₃ f₄<VAR>inst✝³ : HasPullback (sorryAx (?m.103896 ⟶ X₂) true ≫ f₃) f₄<VAR>inst✝² : HasPullback f₁ (sorryAx (?m.109347 ⟶ X₂) true ≫ f₂)<VAR>inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄<VAR>inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)<GOAL>(pullbackAssoc f₁ f₂ f₃ f₄).inv ≫ pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂ = pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>W X Y Z X₁ X₂ X₃ Y₁ Y₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₁<VAR>f₃ : X₂ ⟶ Y₂<VAR>f₄ : X₃ ⟶ Y₂<VAR>inst✝⁵ : HasPullback f₁ f₂<VAR>inst✝⁴ : HasPullback f₃ f₄<VAR>inst✝³ : HasPullback (sorryAx (?m.103896 ⟶ X₂) true ≫ f₃) f₄<VAR>inst✝² : HasPullback f₁ (sorryAx (?m.109347 ⟶ X₂) true ≫ f₂)<VAR>inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄<VAR>inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)<GOAL>(pullbackAssoc f₁ f₂ f₃ f₄).inv ≫ pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂ = pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂)) (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯ ≫ pullback.fst f₁ f₂
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>W X Y Z X₁ X₂ X₃ Y₁ Y₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₁<VAR>f₃ : X₂ ⟶ Y₂<VAR>f₄ : X₃ ⟶ Y₂<VAR>inst✝⁵ : HasPullback f₁ f₂<VAR>inst✝⁴ : HasPullback f₃ f₄<VAR>inst✝³ : HasPullback (sorryAx (?m.103896 ⟶ X₂) true ≫ f₃) f₄<VAR>inst✝² : HasPullback f₁ (sorryAx (?m.109347 ⟶ X₂) true ≫ f₂)<VAR>inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄<VAR>inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)<GOAL>pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂)) (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯ ≫ pullback.fst f₁ f₂ = pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>κ : Type u_1<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : DecidableEq κ<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>h : κ → ι<VAR>h' : ι → κ<VAR>hh' : Function.LeftInverse h' h<VAR>k : κ<VAR>x : β (h k)<VAR>i : κ<GOAL>(comapDomain' h hh' (single (h k) x)) i = (single k x) i