ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x y : P<VAR>h : y = x<VAR>hne : y ≠ x<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁵ : GroupWithZero α<VAR>inst✝⁴ : Preorder α<VAR>inst✝³ : Preorder β<VAR>inst✝² : MulAction α β<VAR>inst✝¹ : PosSMulMono α β<VAR>inst✝ : PosSMulReflectLE α β<VAR>ha : 0 < a<GOAL>a⁻¹ • b₁ ≤ b₂ ↔ b₁ ≤ a • b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>mδ : MeasurableSpace δ<VAR>f : β → γ<VAR>g : γ → α<VAR>hf : Measurable f<VAR>a✝¹ : α<VAR>s✝ : Set γ<VAR>a✝ : MeasurableSet s✝<GOAL>((map 0 f hf) a✝¹) s✝ = (0 a✝¹) s✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>mδ : MeasurableSpace δ<VAR>f : β → γ<VAR>g : γ → α<VAR>hf : Measurable f<VAR>a✝¹ : α<VAR>s✝ : Set γ<VAR>a✝ : MeasurableSet s✝<GOAL>(Measure.map f (0 a✝¹)) s✝ = (0 a✝¹) s✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → β → Option σ<VAR>hf : Computable₂ fun a n => (decode n).bind (f a)<VAR>n : ℕ<GOAL>((↑(decode n)).bind fun a => map encode ((fun a => (do let n ← (↑fun n => encode (decode n)) a.2 ↑n.ppred).bind ↑fun b => (fun a n => (decode n).bind (f a)) (a, b).1.1 (a, b).1.2) a)) = (↑(decode n)).bind fun a => map encode ((↑fun p => f p.1 p.2) a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → β → Option σ<VAR>hf : Computable₂ fun a n => (decode n).bind (f a)<VAR>n : ℕ<GOAL>((↑((decode (Nat.unpair n).1).bind fun a => Option.some (a, (Nat.unpair n).2))).bind fun a => (↑(encode (decode a.2)).ppred).bind fun y => Part.some (encode ((decode a.2).bind fun a_1 => f a.1 a_1))) = (↑((decode (Nat.unpair n).1).bind fun a => Option.map (Prod.mk a) (decode (Nat.unpair n).2))).bind fun a => Part.some (encode (f a.1 a.2))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → β → Option σ<VAR>hf : Computable₂ f<GOAL>Computable₂ fun a n => (decode n).bind (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → β → Option σ<VAR>hf : Computable₂ f<VAR>this : Partrec fun a => Nat.casesOn (encode (decode a.2)) (Part.some Option.none) fun n => map (f a.1) ↑(decode n)<GOAL>Computable₂ fun a n => (decode n).bind (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → β → Option σ<VAR>hf : Computable₂ f<VAR>this : Partrec fun a => Nat.casesOn (encode (decode a.2)) (Part.some Option.none) fun n => map (f a.1) ↑(decode n)<VAR>a : α × ℕ<GOAL>(Nat.casesOn (encode (decode a.2)) (Part.some Option.none) fun n => map (f a.1) ↑(decode n)) = (↑fun p => (fun a n => (decode n).bind (f a)) p.1 p.2) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : α → β → Option σ<VAR>hf : Computable₂ f<VAR>this : Partrec fun a => Nat.casesOn (encode (decode a.2)) (Part.some Option.none) fun n => map (f a.1) ↑(decode n)<VAR>a : α × ℕ<GOAL>Nat.rec (Part.some Option.none) (fun n n_ih => map (f a.1) ↑(decode n)) (encode (decode a.2)) = Part.some ((decode a.2).bind (f a.1))
<VAR>α : Type u_1<VAR>inst✝² : Lattice α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b✝ a b : α<GOAL>mabs (mabs a / mabs b) ≤ mabs (a / b)
<VAR>α : Type u_1<VAR>inst✝² : Lattice α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b✝ a b : α<GOAL>mabs a / mabs b ≤ mabs (a / b) ∧ (mabs a / mabs b)⁻¹ ≤ mabs (a / b)
<VAR>m✝ n✝ m : ℕ<VAR>b : Bool<VAR>n : ℕ<GOAL>(bit b n).testBit m.succ = n.testBit m
<VAR>m✝ n✝ m : ℕ<VAR>b : Bool<VAR>n : ℕ<VAR>this : (bit b n >>> 1 >>> m).bodd = (n >>> m).bodd<GOAL>(bit b n).testBit m.succ = n.testBit m
<VAR>m✝ n✝ m : ℕ<VAR>b : Bool<VAR>n : ℕ<VAR>this : (bit b n >>> (m + 1)).bodd = (n >>> m).bodd<GOAL>(bit b n).testBit m.succ = n.testBit m
<VAR>m✝ n✝ m : ℕ<VAR>b : Bool<VAR>n : ℕ<VAR>this : (1 &&& bit b n >>> (m + 1) != 0) = (1 &&& n >>> m != 0)<GOAL>(bit b n).testBit m.succ = n.testBit m
<VAR>α : Type u<VAR>L✝ L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>inst✝ : DecidableEq α<VAR>x : FreeGroup α<VAR>L : List (α × Bool)<GOAL>(Quot.mk Red.Step L)⁻¹.toWord = invRev (toWord (Quot.mk Red.Step L))
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a : α<GOAL>⋃ n, Ioc (n • p) ((n + 1) • p) = univ
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : MulOneClass M<VAR>x✝ : M<GOAL>1 * x✝ = x✝ * 1
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : MulOneClass M<VAR>x✝¹ x✝ : M<GOAL>1 * (x✝¹ * x✝) = 1 * x✝¹ * x✝
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : MulOneClass M<VAR>x✝¹ x✝ : M<GOAL>x✝¹ * 1 * x✝ = x✝¹ * (1 * x✝)
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : MulOneClass M<VAR>x✝¹ x✝ : M<GOAL>x✝¹ * x✝ * 1 = x✝¹ * (x✝ * 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α<VAR>a✝ b a : α<VAR>s t : Finset α<GOAL>insert a (s ∪ t) = insert a s ∪ insert a t
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : NormalSpace X<VAR>u : ι → Set X<VAR>s : Set X<VAR>c : Set (PartialRefinement u s)<VAR>i : ι<VAR>ne : c.Nonempty<VAR>h : ∃ v ∈ c, i ∈ v.carrier<GOAL>h.choose ∈ c
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : NormalSpace X<VAR>u : ι → Set X<VAR>s : Set X<VAR>c : Set (PartialRefinement u s)<VAR>i : ι<VAR>ne : c.Nonempty<VAR>h : ¬∃ v ∈ c, i ∈ v.carrier<GOAL>ne.some ∈ c
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>A : Type u₂<VAR>inst✝² : Category.{v₂, u₂} A<VAR>D : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} D<VAR>inst✝ : HasWeakSheafify J D<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>hQ : Presheaf.IsSheaf J Q<GOAL>toSheafify J P ≫ sheafifyLift J η hQ = η
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>A : Type u₂<VAR>inst✝² : Category.{v₂, u₂} A<VAR>D : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} D<VAR>inst✝ : HasWeakSheafify J D<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>hQ : Presheaf.IsSheaf J Q<GOAL>(sheafificationAdjunction J D).unit.app P ≫ ((presheafToSheaf J D).map η ≫ (sheafificationAdjunction J D).counit.app { val := Q, cond := hQ }).val = η
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>A : Type u₂<VAR>inst✝² : Category.{v₂, u₂} A<VAR>D : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} D<VAR>inst✝ : HasWeakSheafify J D<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>hQ : Presheaf.IsSheaf J Q<GOAL>η ≫ (sheafificationAdjunction J D).unit.app ((sheafToPresheaf J D).obj { val := Q, cond := hQ }) ≫ (sheafToPresheaf J D).map ((sheafificationAdjunction J D).counit.app { val := Q, cond := hQ }) = η
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>A : Type u₂<VAR>inst✝² : Category.{v₂, u₂} A<VAR>D : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} D<VAR>inst✝ : HasWeakSheafify J D<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>hQ : Presheaf.IsSheaf J Q<GOAL>η ≫ 𝟙 ((sheafToPresheaf J D).obj { val := Q, cond := hQ }) = η
<VAR>α : Type u_1<VAR>inst✝³ : CompleteLattice α<VAR>inst✝² : Group α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s✝ t s : Set α<GOAL>sSup s⁻¹ = (sInf s)⁻¹
<VAR>α : Type u_1<VAR>inst✝³ : CompleteLattice α<VAR>inst✝² : Group α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s✝ t s : Set α<GOAL>⨆ a ∈ s, a⁻¹ = (sInf s)⁻¹
<VAR>α✝ : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>s✝ t : Set α✝<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>inst✝¹ : LinearOrder ι'<VAR>inst✝ : Nonempty ι'<VAR>α : ι → Type u_3<VAR>I : Set ι<VAR>s : (i : ι) → ι' → Set (α i)<VAR>hI : I.Finite<VAR>hs : ∀ i ∈ I, Monotone (s i)<GOAL>(⋃ j, I.pi fun i => s i j) = I.pi fun i => ⋃ j, s i j
<VAR>α✝ : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>s✝ t : Set α✝<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>inst✝¹ : LinearOrder ι'<VAR>inst✝ : Nonempty ι'<VAR>α : ι → Type u_3<VAR>I : Set ι<VAR>s : (i : ι) → ι' → Set (α i)<VAR>hI : I.Finite<VAR>hs : ∀ i ∈ I, Monotone (s i)<GOAL>⋃ j, ⋂ x, eval ↑x ⁻¹' s (↑x) j = ⋂ x, ⋃ i, eval ↑x ⁻¹' s (↑x) i
<VAR>α✝ : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>s✝ t : Set α✝<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>inst✝¹ : LinearOrder ι'<VAR>inst✝ : Nonempty ι'<VAR>α : ι → Type u_3<VAR>I : Set ι<VAR>s : (i : ι) → ι' → Set (α i)<VAR>hI : I.Finite<VAR>hs : ∀ i ∈ I, Monotone (s i)<VAR>this : Finite ↑I<GOAL>⋃ j, ⋂ x, eval ↑x ⁻¹' s (↑x) j = ⋂ x, ⋃ i, eval ↑x ⁻¹' s (↑x) i
<VAR>α✝ : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>γ : Type x<VAR>s✝ t : Set α✝<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>inst✝¹ : LinearOrder ι'<VAR>inst✝ : Nonempty ι'<VAR>α : ι → Type u_3<VAR>I : Set ι<VAR>s : (i : ι) → ι' → Set (α i)<VAR>hI : I.Finite<VAR>hs : ∀ i ∈ I, Monotone (s i)<VAR>this : Finite ↑I<VAR>i : ↑I<VAR>j₁ j₂ : ι'<VAR>h : j₁ ≤ j₂<GOAL>eval ↑i ⁻¹' s (↑i) j₁ ≤ eval ↑i ⁻¹' s (↑i) j₂
<VAR>m✝ n✝ : ℕ<VAR>α✝ : Fin (n✝ + 1) → Type u<VAR>x✝ : α✝ (last n✝)<VAR>q : (i : Fin (n✝ + 1)) → α✝ i<VAR>p : (i : Fin n✝) → α✝ i.castSucc<VAR>i : Fin n✝<VAR>y : α✝ i.castSucc<VAR>z : α✝ (last n✝)<VAR>n m : ℕ<VAR>α : Type u_1<VAR>xs : Fin n → α<VAR>x : α<VAR>ys : Fin m → α<GOAL>append (snoc xs x) ys = append xs (cons x ys) ∘ cast ⋯
<VAR>m✝ n✝ : ℕ<VAR>α✝ : Fin (n✝ + 1) → Type u<VAR>x✝ : α✝ (last n✝)<VAR>q : (i : Fin (n✝ + 1)) → α✝ i<VAR>p : (i : Fin n✝) → α✝ i.castSucc<VAR>i : Fin n✝<VAR>y : α✝ i.castSucc<VAR>z : α✝ (last n✝)<VAR>n m : ℕ<VAR>α : Type u_1<VAR>xs : Fin n → α<VAR>x : α<VAR>ys : Fin m → α<GOAL>(append xs (cons (cons x elim0 0) ys) ∘ cast ⋯) ∘ cast ⋯ = append xs (cons x ys) ∘ cast ⋯
<VAR>α : Type u<VAR>m n o : ℕ<VAR>m' : Type u_1<VAR>n' : Type u_2<VAR>o' : Type u_3<VAR>ho : o + 1 = m + 1 + n<VAR>x : α<VAR>u : Fin m → α<VAR>v : Fin n → α<VAR>i : Fin (o + 1)<GOAL>vecAppend ho (vecCons x u) v i = vecCons x (vecAppend ⋯ u v) i
<VAR>α : Type u<VAR>m n o : ℕ<VAR>m' : Type u_1<VAR>n' : Type u_2<VAR>o' : Type u_3<VAR>ho : o + 1 = m + 1 + n<VAR>x : α<VAR>u : Fin m → α<VAR>v : Fin n → α<VAR>i : Fin (o + 1)<GOAL>(if h : ↑i < m + 1 then vecCons x u ⟨↑i, h⟩ else v ⟨↑i - (m + 1), ⋯⟩) = vecCons x (fun i => if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩) i
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : T5Space Y<VAR>e : X → Y<VAR>he : _root_.Embedding e<GOAL>∀ ⦃s t : Set X⦄, Disjoint (closure s) t → Disjoint s (closure t) → Disjoint (𝓝ˢ s) (𝓝ˢ t)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : T5Space Y<VAR>e : X → Y<VAR>he : _root_.Embedding e<VAR>this : CompletelyNormalSpace X<GOAL>∀ ⦃s t : Set X⦄, Disjoint (closure s) t → Disjoint s (closure t) → Disjoint (𝓝ˢ s) (𝓝ˢ t)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>m : α → β → γ<VAR>f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h✝ h₁ h₂ : Filter γ<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>u : Set γ<VAR>v : Set δ<VAR>a✝ : α<VAR>b : β<VAR>c : γ<VAR>f : α → β → β<VAR>a : α<VAR>h : ∀ (b : β), f a b = b<VAR>l : Filter β<GOAL>map₂ f (pure a) l = l
<VAR>R : Type u_1<VAR>inst✝¹⁸ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁷ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁶ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹⁵ : AddCommMonoid M<VAR>inst✝¹⁴ : AddCommMonoid N<VAR>inst✝¹³ : AddCommMonoid P<VAR>inst✝¹² : AddCommMonoid Q<VAR>inst✝¹¹ : AddCommMonoid S<VAR>inst✝¹⁰ : AddCommMonoid T<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : Module R P<VAR>inst✝⁶ : Module R Q<VAR>inst✝⁵ : Module R S<VAR>inst✝⁴ : Module R T<VAR>inst✝³ : DistribMulAction R' M<VAR>inst✝² : Module R'' M<VAR>inst✝¹ : SMulCommClass R R' M<VAR>inst✝ : SMulCommClass R R'' M<VAR>x : M ⊗[R] N<VAR>this : ∀ (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n<GOAL>1 • 0 = 0
<VAR>R : Type u_1<VAR>inst✝¹⁸ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁷ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁶ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹⁵ : AddCommMonoid M<VAR>inst✝¹⁴ : AddCommMonoid N<VAR>inst✝¹³ : AddCommMonoid P<VAR>inst✝¹² : AddCommMonoid Q<VAR>inst✝¹¹ : AddCommMonoid S<VAR>inst✝¹⁰ : AddCommMonoid T<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : Module R P<VAR>inst✝⁶ : Module R Q<VAR>inst✝⁵ : Module R S<VAR>inst✝⁴ : Module R T<VAR>inst✝³ : DistribMulAction R' M<VAR>inst✝² : Module R'' M<VAR>inst✝¹ : SMulCommClass R R' M<VAR>inst✝ : SMulCommClass R R'' M<VAR>x : M ⊗[R] N<VAR>this : ∀ (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n<VAR>m : M<VAR>n : N<GOAL>1 • m ⊗ₜ[R] n = m ⊗ₜ[R] n
<VAR>R : Type u_1<VAR>inst✝¹⁸ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁷ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁶ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹⁵ : AddCommMonoid M<VAR>inst✝¹⁴ : AddCommMonoid N<VAR>inst✝¹³ : AddCommMonoid P<VAR>inst✝¹² : AddCommMonoid Q<VAR>inst✝¹¹ : AddCommMonoid S<VAR>inst✝¹⁰ : AddCommMonoid T<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : Module R P<VAR>inst✝⁶ : Module R Q<VAR>inst✝⁵ : Module R S<VAR>inst✝⁴ : Module R T<VAR>inst✝³ : DistribMulAction R' M<VAR>inst✝² : Module R'' M<VAR>inst✝¹ : SMulCommClass R R' M<VAR>inst✝ : SMulCommClass R R'' M<VAR>x✝ : M ⊗[R] N<VAR>this : ∀ (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n<VAR>x y : M ⊗[R] N<VAR>ihx : 1 • x = x<VAR>ihy : 1 • y = y<GOAL>1 • (x + y) = x + y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>f g : Filter α<VAR>s✝ t : Set α<VAR>ι : Type u_2<VAR>s : ι → Filter α<VAR>U : Set α<VAR>I : Set ι<VAR>I_fin : I.Finite<VAR>V : ↑I → Set α<VAR>hV : ∀ (i : ↑I), V i ∈ s ↑i<VAR>hU : ⋂ i, V i ⊆ U<VAR>this : Fintype ↑I<GOAL>U ∈ ⨅ i, s i
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>f g : Filter α<VAR>s✝ t : Set α<VAR>ι : Type u_2<VAR>s : ι → Filter α<VAR>U : Set α<VAR>I : Set ι<VAR>I_fin : I.Finite<VAR>V : ↑I → Set α<VAR>hV : ∀ (i : ↑I), V i ∈ s ↑i<VAR>hU : ⋂ i, V i ⊆ U<VAR>this : Fintype ↑I<VAR>i : ↑I<GOAL>V i ∈ ⨅ i, s i
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Mul M<VAR>inst✝¹ : Mul N<VAR>inst✝ : Mul P<VAR>c✝ c d : Con M<GOAL>c ⊔ d = conGen (⇑c ⊔ ⇑d)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Mul M<VAR>inst✝¹ : Mul N<VAR>inst✝ : Mul P<VAR>c✝ c d : Con M<GOAL>(conGen fun x y => c x y ∨ d x y) = conGen (⇑c ⊔ ⇑d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<VAR>o' : Ordinal.{v}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max (max u v) w}<VAR>g : (a : Ordinal.{v}) → a < o' → Ordinal.{max (max u v) w}<VAR>h : o.brange f ⊆ o'.brange g<VAR>i : Ordinal.{u}<VAR>hi : i < o<VAR>j : Ordinal.{v}<VAR>hj : j < o'<VAR>hj' : g j hj = f i hi<GOAL>g j hj ≤ o'.bsup g
<VAR>n : ℤ<VAR>k p : ℕ<VAR>hp : Nat.Prime p<VAR>h : ↑p ∣ n ^ k<GOAL>↑p ∣ n
<VAR>n : ℤ<VAR>k p : ℕ<VAR>hp : Nat.Prime p<VAR>h : ↑p ∣ n ^ k<GOAL>p ∣ n.natAbs
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t u : Set α<VAR>Φ : α → β<VAR>hs : IsClosed s<VAR>ht : IsClosed t<GOAL>hausdorffEdist s t = 0 ↔ s = t
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>n : ℕ<VAR>ha : a ≠ 0<GOAL>(C a * X ^ n).degree = ↑n
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq N<VAR>inst✝ : AddGroup N<VAR>f f₁ f₂ g g₁ g₂ : α →₀ N<GOAL>f.neLocus g = (f - g).support
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>h : P.toPoly = Q.toPoly<GOAL>P.c = Q.c
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ z : K<GOAL>normSq ((starRingEnd K) z) = normSq z
<VAR>f : ℕ → ℂ<VAR>s : ℂ<GOAL>LSeries (-f) s = -LSeries f s
<VAR>w x✝ y✝ z x y : ℝ<VAR>hx : 0 ≤ x<GOAL>(x ^ y).toNNReal = x.toNNReal ^ y
<VAR>w x✝ y✝ z x y : ℝ<VAR>hx : 0 ≤ x<GOAL>(↑x.toNNReal ^ y).toNNReal = x.toNNReal ^ y
<VAR>x : ℝ<VAR>hl : 0 ≤ x<VAR>hr : x ≤ 2 * π<GOAL>sin (x / 2) = √((1 - cos x) / 2)
<VAR>x : ℝ<VAR>hl : 0 ≤ x<VAR>hr : x ≤ 2 * π<GOAL>0 ≤ sin (x / 2)
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup G'<VAR>inst✝⁴ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>𝔸 : Type u_6<VAR>𝔸' : Type u_7<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>a b : E → 𝔸<VAR>a' b' : E →L[𝕜] 𝔸<VAR>c d✝ : E → 𝔸'<VAR>c' d' : E →L[𝕜] 𝔸'<VAR>hc : HasFDerivAt c c' x<VAR>d : 𝔸'<GOAL>HasFDerivAt (fun y => c y * d) (d • c') x
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup G'<VAR>inst✝⁴ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>𝔸 : Type u_6<VAR>𝔸' : Type u_7<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>a b : E → 𝔸<VAR>a' b' : E →L[𝕜] 𝔸<VAR>c d✝ : E → 𝔸'<VAR>c' d' : E →L[𝕜] 𝔸'<VAR>hc : HasFDerivAt c c' x<VAR>d : 𝔸'<GOAL>d • c' = c'.smulRight d
<VAR>𝕜 : Type u_1<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup G'<VAR>inst✝⁴ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>𝔸 : Type u_6<VAR>𝔸' : Type u_7<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>a b : E → 𝔸<VAR>a' b' : E →L[𝕜] 𝔸<VAR>c d✝ : E → 𝔸'<VAR>c' d' : E →L[𝕜] 𝔸'<VAR>hc : HasFDerivAt c c' x<VAR>d : 𝔸'<VAR>z : E<GOAL>(d • c') z = (c'.smulRight d) z
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>x : ↑((inhomogeneousCochains A).X 0)<VAR>y : G<GOAL>(A.ρ y) (x default) - x default = (A.ρ ((Equiv.funUnique (Fin 1) G).symm y 0)) (x fun i => (Equiv.funUnique (Fin 1) G).symm y i.succ) + ∑ j ∈ {0}, (-1) ^ (↑j + 1) • x (j.contractNth (fun x x_1 => x * x_1) ((Equiv.funUnique (Fin 1) G).symm y))
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>x : ↑((inhomogeneousCochains A).X 0)<VAR>y : G<GOAL>(A.ρ y) (x default) + -x default = (A.ρ ((Equiv.funUnique (Fin 1) G).symm y 0)) (x fun i => (Equiv.funUnique (Fin 1) G).symm y i.succ) + -x (Fin.contractNth 0 (fun x x_1 => x * x_1) ((Equiv.funUnique (Fin 1) G).symm y))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>inst✝² : CompleteSpace E<VAR>p q : Subspace 𝕜 E<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>inst✝ : FiniteDimensional 𝕜 (E ⧸ p)<VAR>hp : IsClosed ↑p<GOAL>ClosedComplemented p
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>inst✝² : CompleteSpace E<VAR>p q✝ : Subspace 𝕜 E<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>inst✝ : FiniteDimensional 𝕜 (E ⧸ p)<VAR>hp : IsClosed ↑p<VAR>q : Subspace 𝕜 E<VAR>hq : IsCompl p q<GOAL>ClosedComplemented p
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>inst✝² : CompleteSpace E<VAR>p q✝ : Subspace 𝕜 E<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>inst✝ : FiniteDimensional 𝕜 (E ⧸ p)<VAR>hp : IsClosed ↑p<VAR>q : Subspace 𝕜 E<VAR>hq : IsCompl p q<VAR>this : FiniteDimensional 𝕜 ↥q<GOAL>ClosedComplemented p
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H✝ : Type u_3<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : MeasurableSpace H✝<VAR>inst✝⁵ : Mul G<VAR>μ : Measure G<VAR>inst✝⁴ : MeasurableMul G<VAR>H : Type u_4<VAR>inst✝³ : MeasurableSpace H<VAR>inst✝² : Mul H<VAR>inst✝¹ : MeasurableMul H<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>f : G →ₙ* H<VAR>hf : Measurable ⇑f<VAR>h_surj : Surjective ⇑f<VAR>h : H<GOAL>Measure.map (fun x => h * x) (Measure.map (⇑f) μ) = Measure.map (⇑f) μ
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H✝ : Type u_3<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : MeasurableSpace H✝<VAR>inst✝⁵ : Mul G<VAR>μ : Measure G<VAR>inst✝⁴ : MeasurableMul G<VAR>H : Type u_4<VAR>inst✝³ : MeasurableSpace H<VAR>inst✝² : Mul H<VAR>inst✝¹ : MeasurableMul H<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>f : G →ₙ* H<VAR>hf : Measurable ⇑f<VAR>h_surj : Surjective ⇑f<VAR>h : H<GOAL>Measure.map ((fun x => h * x) ∘ ⇑f) μ = Measure.map (⇑f) μ
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H✝ : Type u_3<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : MeasurableSpace H✝<VAR>inst✝⁵ : Mul G<VAR>μ : Measure G<VAR>inst✝⁴ : MeasurableMul G<VAR>H : Type u_4<VAR>inst✝³ : MeasurableSpace H<VAR>inst✝² : Mul H<VAR>inst✝¹ : MeasurableMul H<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>f : G →ₙ* H<VAR>hf : Measurable ⇑f<VAR>h_surj : Surjective ⇑f<VAR>g : G<GOAL>Measure.map ((fun x => f g * x) ∘ ⇑f) μ = Measure.map (⇑f) μ
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H✝ : Type u_3<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : MeasurableSpace H✝<VAR>inst✝⁵ : Mul G<VAR>μ : Measure G<VAR>inst✝⁴ : MeasurableMul G<VAR>H : Type u_4<VAR>inst✝³ : MeasurableSpace H<VAR>inst✝² : Mul H<VAR>inst✝¹ : MeasurableMul H<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>f : G →ₙ* H<VAR>hf : Measurable ⇑f<VAR>h_surj : Surjective ⇑f<VAR>g : G<GOAL>Measure.map ((fun x => f g * x) ∘ ⇑f) μ = Measure.map (⇑f) (Measure.map (fun x => g * x) μ)