ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>inst✝ : Monad m<VAR>as : Array α<VAR>b✝ : β<VAR>f : α → β → m (ForInStep β)<VAR>i : Nat<VAR>x✝¹ : i + 1 ≤ as.size<VAR>x✝ : β<VAR>j : Nat<VAR>ij : j + (i + 1) = as.size<VAR>j_eq : j = as.size - 1 - i<VAR>this✝ : as.size - 1 - i < as.size<VAR>this : as[as.size - 1 - i] :: List.drop (j + 1) as.data = List.drop j as.data<VAR>x : ForInStep β<VAR>b : β<GOAL>forIn.loop as f i ⋯ b = forIn (List.drop (j + 1) as.data) b f
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>inst✝ : Monad m<VAR>as : Array α<VAR>b✝ : β<VAR>f : α → β → m (ForInStep β)<VAR>i : Nat<VAR>x✝¹ : i + 1 ≤ as.size<VAR>x✝ : β<VAR>j : Nat<VAR>ij : j + (i + 1) = as.size<VAR>j_eq : j = as.size - 1 - i<VAR>this✝ : as.size - 1 - i < as.size<VAR>this : as[as.size - 1 - i] :: List.drop (j + 1) as.data = List.drop j as.data<VAR>x : ForInStep β<VAR>b : β<GOAL>j + 1 + i = as.size
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>inst✝ : Monad m<VAR>as : Array α<VAR>b✝ : β<VAR>f : α → β → m (ForInStep β)<VAR>i : Nat<VAR>x✝¹ : i + 1 ≤ as.size<VAR>x✝ : β<VAR>j : Nat<VAR>ij : j + (i + 1) = as.size<VAR>j_eq : j = as.size - 1 - i<VAR>this✝ : as.size - 1 - i < as.size<VAR>this : as[as.size - 1 - i] :: List.drop (j + 1) as.data = List.drop j as.data<VAR>x : ForInStep β<VAR>b : β<GOAL>(j + i).succ = j + (i + 1)
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>inst✝ : Monad m<VAR>as : Array α<VAR>b : β<VAR>f : α → β → m (ForInStep β)<GOAL>forIn.loop as f as.size ⋯ b = forIn as.data b f
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>inst✝ : Monad m<VAR>as : Array α<VAR>b : β<VAR>f : α → β → m (ForInStep β)<GOAL>forIn (List.drop 0 as.data) b f = forIn as.data b f
<VAR>α : Type u_1<VAR>s : Set α<VAR>t : Set ↑s<VAR>x : α<VAR>x✝ : x ∈ val '' t<VAR>y : { x // x ∈ s }<VAR>left✝ : y ∈ t<VAR>yvaleq : ↑y = x<GOAL>↑y ∈ s
<VAR>R : Type u<VAR>ι : Type w<VAR>inst✝ : CommSemiring R<VAR>f✝ : ι → R[X]<VAR>t : Multiset R[X]<VAR>f : ι → R[X]<VAR>n : ℕ<VAR>l : Multiset ι<VAR>hl : l.Nodup<VAR>h : ∀ p ∈ { val := l, nodup := hl }, (f p).natDegree ≤ n<GOAL>(∏ i ∈ { val := l, nodup := hl }, f i).coeff ({ val := l, nodup := hl }.card * n) = ∏ i ∈ { val := l, nodup := hl }, (f i).coeff n
<VAR>R : Type u<VAR>ι : Type w<VAR>inst✝ : CommSemiring R<VAR>f✝ : ι → R[X]<VAR>t : Multiset R[X]<VAR>f : ι → R[X]<VAR>n : ℕ<VAR>l : Multiset ι<VAR>hl : l.Nodup<VAR>h : ∀ p ∈ { val := l, nodup := hl }, (f p).natDegree ≤ n<GOAL>{ val := l, nodup := hl }.card = Multiset.card (Multiset.map f l)
<VAR>R : Type u<VAR>ι : Type w<VAR>inst✝ : CommSemiring R<VAR>f✝ : ι → R[X]<VAR>t : Multiset R[X]<VAR>f : ι → R[X]<VAR>n : ℕ<VAR>l : Multiset ι<VAR>hl : l.Nodup<VAR>h : ∀ p ∈ { val := l, nodup := hl }, (f p).natDegree ≤ n<GOAL>∏ i ∈ { val := l, nodup := hl }, (f i).coeff n = (Multiset.map (fun p => p.coeff n) (Multiset.map f l)).prod
<VAR>R : Type u<VAR>ι : Type w<VAR>inst✝ : CommSemiring R<VAR>f✝ : ι → R[X]<VAR>t : Multiset R[X]<VAR>f : ι → R[X]<VAR>n : ℕ<VAR>l : Multiset ι<VAR>hl : l.Nodup<VAR>h : ∀ p ∈ { val := l, nodup := hl }, (f p).natDegree ≤ n<GOAL>∀ p ∈ Multiset.map f l, p.natDegree ≤ n
<VAR>M₀ : Type u_1<VAR>G₀ : Type u_2<VAR>inst✝ : GroupWithZero G₀<VAR>s : Set G₀<VAR>a b : G₀<GOAL>center G₀ˣ ⊆ Units.val ⁻¹' center G₀
<VAR>M₀ : Type u_1<VAR>G₀ : Type u_2<VAR>inst✝ : GroupWithZero G₀<VAR>s : Set G₀<VAR>a b : G₀<GOAL>∀ (x : G₀ˣ), (∀ (g : G₀ˣ), g * x = x * g) → ∀ (g : G₀), g * ↑x = ↑x * g
<VAR>M₀ : Type u_1<VAR>G₀ : Type u_2<VAR>inst✝ : GroupWithZero G₀<VAR>s : Set G₀<VAR>a✝ b : G₀<VAR>u : G₀ˣ<VAR>hu : ∀ (g : G₀ˣ), g * u = u * g<VAR>a : G₀<GOAL>a * ↑u = ↑u * a
<VAR>M₀ : Type u_1<VAR>G₀ : Type u_2<VAR>inst✝ : GroupWithZero G₀<VAR>s : Set G₀<VAR>a b : G₀<VAR>u : G₀ˣ<VAR>hu : ∀ (g : G₀ˣ), g * u = u * g<GOAL>0 * ↑u = ↑u * 0
<VAR>M₀ : Type u_1<VAR>G₀ : Type u_2<VAR>inst✝ : GroupWithZero G₀<VAR>s : Set G₀<VAR>a✝ b : G₀<VAR>u : G₀ˣ<VAR>hu : ∀ (g : G₀ˣ), g * u = u * g<VAR>a : G₀<VAR>ha : a ≠ 0<GOAL>a * ↑u = ↑u * a
<VAR>α : Type u_1<VAR>p q : Perm α<VAR>x : α<GOAL>x ∈ {x | p⁻¹ x ≠ x} ↔ x ∈ {x | p x ≠ x}
<VAR>α : Type u_1<VAR>p q : Perm α<VAR>x : α<GOAL>¬p⁻¹ x = x ↔ ¬p x = x
<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>e : S₁ ≅ S₂<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<GOAL>homologyMap e.hom ≫ homologyMap e.inv = 𝟙 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>e : S₁ ≅ S₂<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<GOAL>homologyMap e.inv ≫ homologyMap e.hom = 𝟙 S₂.homology
<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>H₁ : Type u_6<VAR>inst✝⁷ : TopologicalSpace H₁<VAR>H₂ : Type u_7<VAR>inst✝⁶ : TopologicalSpace H₂<VAR>H₃ : Type u_8<VAR>inst✝⁵ : TopologicalSpace H₃<VAR>inst✝⁴ : ChartedSpace H₁ H₂<VAR>inst✝³ : ChartedSpace H₂ H₃<VAR>G₁ : StructureGroupoid H₁<VAR>inst✝² : HasGroupoid H₂ G₁<VAR>inst✝¹ : ClosedUnderRestriction G₁<VAR>G₂ : StructureGroupoid H₂<VAR>inst✝ : HasGroupoid H₃ G₂<VAR>H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e) e.source<VAR>x✝ : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃<VAR>e : PartialHomeomorph H₃ H₂<VAR>he : e ∈ atlas H₂ H₃<VAR>f : PartialHomeomorph H₂ H₁<VAR>hf : f ∈ atlas H₁ H₂<VAR>e' : PartialHomeomorph H₃ H₂<VAR>he' : e' ∈ atlas H₂ H₃<VAR>f' : PartialHomeomorph H₂ H₁<VAR>hf' : f' ∈ atlas H₁ H₂<GOAL>(e ≫ₕ f).symm ≫ₕ e' ≫ₕ f' ∈ G₁
<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>H₁ : Type u_6<VAR>inst✝⁷ : TopologicalSpace H₁<VAR>H₂ : Type u_7<VAR>inst✝⁶ : TopologicalSpace H₂<VAR>H₃ : Type u_8<VAR>inst✝⁵ : TopologicalSpace H₃<VAR>inst✝⁴ : ChartedSpace H₁ H₂<VAR>inst✝³ : ChartedSpace H₂ H₃<VAR>G₁ : StructureGroupoid H₁<VAR>inst✝² : HasGroupoid H₂ G₁<VAR>inst✝¹ : ClosedUnderRestriction G₁<VAR>G₂ : StructureGroupoid H₂<VAR>inst✝ : HasGroupoid H₃ G₂<VAR>H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e) e.source<VAR>x✝ : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃<VAR>e : PartialHomeomorph H₃ H₂<VAR>he : e ∈ atlas H₂ H₃<VAR>f : PartialHomeomorph H₂ H₁<VAR>hf : f ∈ atlas H₁ H₂<VAR>e' : PartialHomeomorph H₃ H₂<VAR>he' : e' ∈ atlas H₂ H₃<VAR>f' : PartialHomeomorph H₂ H₁<VAR>hf' : f' ∈ atlas H₁ H₂<GOAL>∀ x ∈ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').source, ∃ s, IsOpen s ∧ x ∈ s ∧ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁
<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>H₁ : Type u_6<VAR>inst✝⁷ : TopologicalSpace H₁<VAR>H₂ : Type u_7<VAR>inst✝⁶ : TopologicalSpace H₂<VAR>H₃ : Type u_8<VAR>inst✝⁵ : TopologicalSpace H₃<VAR>inst✝⁴ : ChartedSpace H₁ H₂<VAR>inst✝³ : ChartedSpace H₂ H₃<VAR>G₁ : StructureGroupoid H₁<VAR>inst✝² : HasGroupoid H₂ G₁<VAR>inst✝¹ : ClosedUnderRestriction G₁<VAR>G₂ : StructureGroupoid H₂<VAR>inst✝ : HasGroupoid H₃ G₂<VAR>H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e) e.source<VAR>x✝ : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃<VAR>e : PartialHomeomorph H₃ H₂<VAR>he : e ∈ atlas H₂ H₃<VAR>f : PartialHomeomorph H₂ H₁<VAR>hf : f ∈ atlas H₁ H₂<VAR>e' : PartialHomeomorph H₃ H₂<VAR>he' : e' ∈ atlas H₂ H₃<VAR>f' : PartialHomeomorph H₂ H₁<VAR>hf' : f' ∈ atlas H₁ H₂<VAR>x : H₁<VAR>hx : (x ∈ f.target ∧ ↑f.symm x ∈ e.target) ∧ ↑e.symm (↑f.symm x) ∈ e'.source ∧ ↑e' (↑e.symm (↑f.symm x)) ∈ f'.source<VAR>hxs : x ∈ ↑f.symm ⁻¹' (e.symm ≫ₕ e').source<VAR>hxs' : x ∈ f.target ∩ ↑f.symm ⁻¹' ((e.symm ≫ₕ e').source ∩ ↑(e.symm ≫ₕ e') ⁻¹' f'.source)<GOAL>∃ s, IsOpen s ∧ x ∈ s ∧ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁
<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>H₁ : Type u_6<VAR>inst✝⁷ : TopologicalSpace H₁<VAR>H₂ : Type u_7<VAR>inst✝⁶ : TopologicalSpace H₂<VAR>H₃ : Type u_8<VAR>inst✝⁵ : TopologicalSpace H₃<VAR>inst✝⁴ : ChartedSpace H₁ H₂<VAR>inst✝³ : ChartedSpace H₂ H₃<VAR>G₁ : StructureGroupoid H₁<VAR>inst✝² : HasGroupoid H₂ G₁<VAR>inst✝¹ : ClosedUnderRestriction G₁<VAR>G₂ : StructureGroupoid H₂<VAR>inst✝ : HasGroupoid H₃ G₂<VAR>H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e) e.source<VAR>x✝ : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃<VAR>e : PartialHomeomorph H₃ H₂<VAR>he : e ∈ atlas H₂ H₃<VAR>f : PartialHomeomorph H₂ H₁<VAR>hf : f ∈ atlas H₁ H₂<VAR>e' : PartialHomeomorph H₃ H₂<VAR>he' : e' ∈ atlas H₂ H₃<VAR>f' : PartialHomeomorph H₂ H₁<VAR>hf' : f' ∈ atlas H₁ H₂<VAR>x : H₁<VAR>hx : (x ∈ f.target ∧ ↑f.symm x ∈ e.target) ∧ ↑e.symm (↑f.symm x) ∈ e'.source ∧ ↑e' (↑e.symm (↑f.symm x)) ∈ f'.source<VAR>hxs : x ∈ ↑f.symm ⁻¹' (e.symm ≫ₕ e').source<VAR>hxs' : x ∈ f.target ∩ ↑f.symm ⁻¹' ((e.symm ≫ₕ e').source ∩ ↑(e.symm ≫ₕ e') ⁻¹' f'.source)<VAR>φ : PartialHomeomorph H₁ H₁<VAR>hφG₁ : φ ∈ G₁<VAR>hφ : EqOn (↑f' ∘ ↑(e.symm ≫ₕ e') ∘ ↑f.symm) (↑φ.toPartialEquiv) (↑f.symm ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)<VAR>hφ_dom : x ∈ φ.source<GOAL>∃ s, IsOpen s ∧ x ∈ s ∧ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁
<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>H₁ : Type u_6<VAR>inst✝⁷ : TopologicalSpace H₁<VAR>H₂ : Type u_7<VAR>inst✝⁶ : TopologicalSpace H₂<VAR>H₃ : Type u_8<VAR>inst✝⁵ : TopologicalSpace H₃<VAR>inst✝⁴ : ChartedSpace H₁ H₂<VAR>inst✝³ : ChartedSpace H₂ H₃<VAR>G₁ : StructureGroupoid H₁<VAR>inst✝² : HasGroupoid H₂ G₁<VAR>inst✝¹ : ClosedUnderRestriction G₁<VAR>G₂ : StructureGroupoid H₂<VAR>inst✝ : HasGroupoid H₃ G₂<VAR>H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e) e.source<VAR>x✝ : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃<VAR>e : PartialHomeomorph H₃ H₂<VAR>he : e ∈ atlas H₂ H₃<VAR>f : PartialHomeomorph H₂ H₁<VAR>hf : f ∈ atlas H₁ H₂<VAR>e' : PartialHomeomorph H₃ H₂<VAR>he' : e' ∈ atlas H₂ H₃<VAR>f' : PartialHomeomorph H₂ H₁<VAR>hf' : f' ∈ atlas H₁ H₂<VAR>x : H₁<VAR>hx : (x ∈ f.target ∧ ↑f.symm x ∈ e.target) ∧ ↑e.symm (↑f.symm x) ∈ e'.source ∧ ↑e' (↑e.symm (↑f.symm x)) ∈ f'.source<VAR>hxs : x ∈ ↑f.symm ⁻¹' (e.symm ≫ₕ e').source<VAR>hxs' : x ∈ f.target ∩ ↑f.symm ⁻¹' ((e.symm ≫ₕ e').source ∩ ↑(e.symm ≫ₕ e') ⁻¹' f'.source)<VAR>φ : PartialHomeomorph H₁ H₁<VAR>hφG₁ : φ ∈ G₁<VAR>hφ_dom : x ∈ φ.source<VAR>hφ : EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f')) (↑φ.toPartialEquiv) (↑f.symm ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)<GOAL>∃ s, IsOpen s ∧ x ∈ s ∧ ((e ≫ₕ f).symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁
<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>H₁ : Type u_6<VAR>inst✝⁷ : TopologicalSpace H₁<VAR>H₂ : Type u_7<VAR>inst✝⁶ : TopologicalSpace H₂<VAR>H₃ : Type u_8<VAR>inst✝⁵ : TopologicalSpace H₃<VAR>inst✝⁴ : ChartedSpace H₁ H₂<VAR>inst✝³ : ChartedSpace H₂ H₃<VAR>G₁ : StructureGroupoid H₁<VAR>inst✝² : HasGroupoid H₂ G₁<VAR>inst✝¹ : ClosedUnderRestriction G₁<VAR>G₂ : StructureGroupoid H₂<VAR>inst✝ : HasGroupoid H₃ G₂<VAR>H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e) e.source<VAR>x✝ : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃<VAR>e : PartialHomeomorph H₃ H₂<VAR>he : e ∈ atlas H₂ H₃<VAR>f : PartialHomeomorph H₂ H₁<VAR>hf : f ∈ atlas H₁ H₂<VAR>e' : PartialHomeomorph H₃ H₂<VAR>he' : e' ∈ atlas H₂ H₃<VAR>f' : PartialHomeomorph H₂ H₁<VAR>hf' : f' ∈ atlas H₁ H₂<VAR>x : H₁<VAR>hx : (x ∈ f.target ∧ ↑f.symm x ∈ e.target) ∧ ↑e.symm (↑f.symm x) ∈ e'.source ∧ ↑e' (↑e.symm (↑f.symm x)) ∈ f'.source<VAR>hxs : x ∈ ↑f.symm ⁻¹' (e.symm ≫ₕ e').source<VAR>hxs' : x ∈ f.target ∩ ↑f.symm ⁻¹' ((e.symm ≫ₕ e').source ∩ ↑(e.symm ≫ₕ e') ⁻¹' f'.source)<VAR>φ : PartialHomeomorph H₁ H₁<VAR>hφG₁ : φ ∈ G₁<VAR>hφ_dom : x ∈ φ.source<VAR>hφ : EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f')) (↑φ.toPartialEquiv) (↑f.symm ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)<GOAL>∃ s, IsOpen s ∧ x ∈ s ∧ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁
<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>H₁ : Type u_6<VAR>inst✝⁷ : TopologicalSpace H₁<VAR>H₂ : Type u_7<VAR>inst✝⁶ : TopologicalSpace H₂<VAR>H₃ : Type u_8<VAR>inst✝⁵ : TopologicalSpace H₃<VAR>inst✝⁴ : ChartedSpace H₁ H₂<VAR>inst✝³ : ChartedSpace H₂ H₃<VAR>G₁ : StructureGroupoid H₁<VAR>inst✝² : HasGroupoid H₂ G₁<VAR>inst✝¹ : ClosedUnderRestriction G₁<VAR>G₂ : StructureGroupoid H₂<VAR>inst✝ : HasGroupoid H₃ G₂<VAR>H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e) e.source<VAR>x✝ : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃<VAR>e : PartialHomeomorph H₃ H₂<VAR>he : e ∈ atlas H₂ H₃<VAR>f : PartialHomeomorph H₂ H₁<VAR>hf : f ∈ atlas H₁ H₂<VAR>e' : PartialHomeomorph H₃ H₂<VAR>he' : e' ∈ atlas H₂ H₃<VAR>f' : PartialHomeomorph H₂ H₁<VAR>hf' : f' ∈ atlas H₁ H₂<VAR>x : H₁<VAR>hx : (x ∈ f.target ∧ ↑f.symm x ∈ e.target) ∧ ↑e.symm (↑f.symm x) ∈ e'.source ∧ ↑e' (↑e.symm (↑f.symm x)) ∈ f'.source<VAR>hxs : x ∈ ↑f.symm ⁻¹' (e.symm ≫ₕ e').source<VAR>hxs' : x ∈ f.target ∩ ↑f.symm ⁻¹' ((e.symm ≫ₕ e').source ∩ ↑(e.symm ≫ₕ e') ⁻¹' f'.source)<VAR>φ : PartialHomeomorph H₁ H₁<VAR>hφG₁ : φ ∈ G₁<VAR>hφ_dom : x ∈ φ.source<VAR>hφ : EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f')) (↑φ.toPartialEquiv) (↑f.symm ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)<VAR>hs : IsOpen (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source<GOAL>∃ s, IsOpen s ∧ x ∈ s ∧ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').restr s ∈ G₁
<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>H₁ : Type u_6<VAR>inst✝⁷ : TopologicalSpace H₁<VAR>H₂ : Type u_7<VAR>inst✝⁶ : TopologicalSpace H₂<VAR>H₃ : Type u_8<VAR>inst✝⁵ : TopologicalSpace H₃<VAR>inst✝⁴ : ChartedSpace H₁ H₂<VAR>inst✝³ : ChartedSpace H₂ H₃<VAR>G₁ : StructureGroupoid H₁<VAR>inst✝² : HasGroupoid H₂ G₁<VAR>inst✝¹ : ClosedUnderRestriction G₁<VAR>G₂ : StructureGroupoid H₂<VAR>inst✝ : HasGroupoid H₃ G₂<VAR>H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e) e.source<VAR>x✝ : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃<VAR>e : PartialHomeomorph H₃ H₂<VAR>he : e ∈ atlas H₂ H₃<VAR>f : PartialHomeomorph H₂ H₁<VAR>hf : f ∈ atlas H₁ H₂<VAR>e' : PartialHomeomorph H₃ H₂<VAR>he' : e' ∈ atlas H₂ H₃<VAR>f' : PartialHomeomorph H₂ H₁<VAR>hf' : f' ∈ atlas H₁ H₂<VAR>x : H₁<VAR>hx : (x ∈ f.target ∧ ↑f.symm x ∈ e.target) ∧ ↑e.symm (↑f.symm x) ∈ e'.source ∧ ↑e' (↑e.symm (↑f.symm x)) ∈ f'.source<VAR>hxs : x ∈ ↑f.symm ⁻¹' (e.symm ≫ₕ e').source<VAR>hxs' : x ∈ f.target ∩ ↑f.symm ⁻¹' ((e.symm ≫ₕ e').source ∩ ↑(e.symm ≫ₕ e') ⁻¹' f'.source)<VAR>φ : PartialHomeomorph H₁ H₁<VAR>hφG₁ : φ ∈ G₁<VAR>hφ_dom : x ∈ φ.source<VAR>hφ : EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f')) (↑φ.toPartialEquiv) (↑f.symm ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)<VAR>hs : IsOpen (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source<GOAL>x ∈ (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source ∩ φ.source
<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>H₁ : Type u_6<VAR>inst✝⁷ : TopologicalSpace H₁<VAR>H₂ : Type u_7<VAR>inst✝⁶ : TopologicalSpace H₂<VAR>H₃ : Type u_8<VAR>inst✝⁵ : TopologicalSpace H₃<VAR>inst✝⁴ : ChartedSpace H₁ H₂<VAR>inst✝³ : ChartedSpace H₂ H₃<VAR>G₁ : StructureGroupoid H₁<VAR>inst✝² : HasGroupoid H₂ G₁<VAR>inst✝¹ : ClosedUnderRestriction G₁<VAR>G₂ : StructureGroupoid H₂<VAR>inst✝ : HasGroupoid H₃ G₂<VAR>H : ∀ e ∈ G₂, LiftPropOn G₁.IsLocalStructomorphWithinAt (↑e) e.source<VAR>x✝ : ChartedSpace H₁ H₃ := ChartedSpace.comp H₁ H₂ H₃<VAR>e : PartialHomeomorph H₃ H₂<VAR>he : e ∈ atlas H₂ H₃<VAR>f : PartialHomeomorph H₂ H₁<VAR>hf : f ∈ atlas H₁ H₂<VAR>e' : PartialHomeomorph H₃ H₂<VAR>he' : e' ∈ atlas H₂ H₃<VAR>f' : PartialHomeomorph H₂ H₁<VAR>hf' : f' ∈ atlas H₁ H₂<VAR>x : H₁<VAR>hx : (x ∈ f.target ∧ ↑f.symm x ∈ e.target) ∧ ↑e.symm (↑f.symm x) ∈ e'.source ∧ ↑e' (↑e.symm (↑f.symm x)) ∈ f'.source<VAR>hxs : x ∈ ↑f.symm ⁻¹' (e.symm ≫ₕ e').source<VAR>hxs' : x ∈ f.target ∩ ↑f.symm ⁻¹' ((e.symm ≫ₕ e').source ∩ ↑(e.symm ≫ₕ e') ⁻¹' f'.source)<VAR>φ : PartialHomeomorph H₁ H₁<VAR>hφG₁ : φ ∈ G₁<VAR>hφ_dom : x ∈ φ.source<VAR>hφ : EqOn (↑(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f')) (↑φ.toPartialEquiv) (↑f.symm ⁻¹' (e.symm ≫ₕ e').source ∩ φ.source)<VAR>hs : IsOpen (f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source<GOAL>(f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').restr ((f.symm ≫ₕ e.symm ≫ₕ e' ≫ₕ f').source ∩ φ.source) ∈ G₁
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f✝ : Y ⟶ X<VAR>S✝ R✝ : Sieve X<VAR>f : Y ⟶ X<VAR>S R : Sieve X<GOAL>pullback f (S ⊓ R) = pullback f S ⊓ pullback f R
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<VAR>hI_ss : ∀ t ∈ I, t ⊆ s<VAR>inst✝ : DecidableEq (Set α)<GOAL>⋃₀ ↑(I ∪ hC.diffFinset₀ hs hI) = s
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<VAR>hI_ss : ∀ t ∈ I, t ⊆ s<VAR>inst✝ : DecidableEq (Set α)<GOAL>⋃₀ ↑(I ∪ hC.diffFinset₀ hs hI) = ⋃₀ ↑I ∪ ⋃₀ ↑(hC.diffFinset₀ hs hI)
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<VAR>hI_ss : ∀ t ∈ I, t ⊆ s<VAR>inst✝ : DecidableEq (Set α)<GOAL>⋃₀ (↑I ∪ ↑(hC.diffFinset₀ hs hI)) = ⋃₀ ↑I ∪ ⋃₀ ↑(hC.diffFinset₀ hs hI)
<VAR>m n✝ n : ℕ<VAR>a b : ZMod n<VAR>h : a.val * b.val < n<GOAL>(a * b).val = a.val * b.val
<VAR>m n✝ n : ℕ<VAR>a b : ZMod n<VAR>h : a.val * b.val < n<GOAL>a.val * b.val % n = a.val * b.val
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : CommRing R<VAR>x y : 𝕎 R<GOAL>(x * y).coeff 0 = x.coeff 0 * y.coeff 0
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<GOAL>X n ^ e = (monomial (Finsupp.single n e)) 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : HeytingAlgebra α<VAR>a b c : α<GOAL>Disjoint aᶜᶜ b ↔ Disjoint a b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>a b : A<VAR>f g : End R M<GOAL>(tensorProduct R A M M) ((a * b) ⊗ₜ[R] (f * g)) = (tensorProduct R A M M) (a ⊗ₜ[R] f) * (tensorProduct R A M M) (b ⊗ₜ[R] g)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>a b : A<VAR>f g : End R M<GOAL>∀ (x : A ⊗[R] M), ((tensorProduct R A M M) ((a * b) ⊗ₜ[R] (f * g))) x = ((tensorProduct R A M M) (a ⊗ₜ[R] f) * (tensorProduct R A M M) (b ⊗ₜ[R] g)) x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>a b : A<VAR>f g : End R M<VAR>x : A ⊗[R] M<GOAL>((tensorProduct R A M M) ((a * b) ⊗ₜ[R] (f * g))) x = ((tensorProduct R A M M) (a ⊗ₜ[R] f) * (tensorProduct R A M M) (b ⊗ₜ[R] g)) x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<GOAL>(tensorProduct R A M M) (1 ⊗ₜ[R] 1) = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<GOAL>∀ (x : A ⊗[R] M), ((tensorProduct R A M M) (1 ⊗ₜ[R] 1)) x = 1 x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>x : A ⊗[R] M<GOAL>((tensorProduct R A M M) (1 ⊗ₜ[R] 1)) x = 1 x