ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>a b : β<GOAL>pure a -ᵥ pure b = pure (a -ᵥ b)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>f₁ f₂ g₁ g₂ : Filter β<GOAL>f₁ ≤ f₂ → g₁ ≤ g₂ → f₁ -ᵥ g₁ ≤ f₂ -ᵥ g₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>f g₁ g₂ : Filter β<GOAL>g₁ ≤ g₂ → f -ᵥ g₁ ≤ f -ᵥ g₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>f₁ f₂ g : Filter β<GOAL>f₁ ≤ f₂ → f₁ -ᵥ g ≤ f₂ -ᵥ g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>f g : Filter β<VAR>h : Filter α<GOAL>h ≤ f -ᵥ g ↔ ∀ ⦃s : Set β⦄, s ∈ f → ∀ ⦃t : Set β⦄, t ∈ g → s -ᵥ t ∈ h
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>f : Filter β<VAR>a : α<GOAL>Filter.map (fun b => a • b) f = a • f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>f : Filter β<VAR>a : α<GOAL>Filter.map (fun b => a +ᵥ b) f = a +ᵥ f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>f : Filter β<VAR>s : Set β<VAR>a : α<GOAL>s ∈ a +ᵥ f ↔ (fun x => a +ᵥ x) ⁻¹' s ∈ f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>f : Filter β<VAR>s : Set β<VAR>a : α<GOAL>s ∈ a • f ↔ (fun x => a • x) ⁻¹' s ∈ f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>f : Filter β<VAR>s : Set β<VAR>a : α<GOAL>s ∈ f → a • s ∈ a • f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>f : Filter β<VAR>s : Set β<VAR>a : α<GOAL>s ∈ f → a +ᵥ s ∈ a +ᵥ f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>a : α<GOAL>a • ⊥ = ⊥
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>a : α<GOAL>a +ᵥ ⊥ = ⊥
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>f : Filter β<VAR>a : α<GOAL>a • f = ⊥ ↔ f = ⊥
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>f : Filter β<VAR>a : α<GOAL>a +ᵥ f = ⊥ ↔ f = ⊥
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>f : Filter β<VAR>a : α<GOAL>(a • f).NeBot ↔ f.NeBot
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>f : Filter β<VAR>a : α<GOAL>(a +ᵥ f).NeBot ↔ f.NeBot
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>f : Filter β<VAR>a : α<GOAL>f.NeBot → (a +ᵥ f).NeBot
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>f : Filter β<VAR>a : α<GOAL>f.NeBot → (a • f).NeBot
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>f : Filter β<VAR>a : α<GOAL>(a • f).NeBot → f.NeBot
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>f : Filter β<VAR>a : α<GOAL>(a +ᵥ f).NeBot → f.NeBot
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>f : Filter β<VAR>a : α<VAR>f.NeBot<GOAL>(a +ᵥ f).NeBot
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>f : Filter β<VAR>a : α<VAR>f.NeBot<GOAL>(a • f).NeBot
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>f₁ f₂ : Filter β<VAR>a : α<VAR>hf : f₁ ≤ f₂<GOAL>a • f₁ ≤ a • f₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>f₁ f₂ : Filter β<VAR>a : α<VAR>hf : f₁ ≤ f₂<GOAL>a +ᵥ f₁ ≤ a +ᵥ f₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>f : Filter α<VAR>hf : f.NeBot<GOAL>0 ≤ f • 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>g : Filter β<VAR>hg : g.NeBot<GOAL>0 ≤ 0 • g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>g : Filter β<GOAL>0 • g ≤ 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>g : Filter β<VAR>hg : g.NeBot<GOAL>0 • g = 0
<VAR>α : Type u_3<VAR>LE α<VAR>self : NoBotOrder α<VAR>a : α<GOAL>∃ b, ¬a ≤ b
<VAR>α : Type u_3<VAR>LE α<VAR>self : NoTopOrder α<VAR>a : α<GOAL>∃ b, ¬b ≤ a
<VAR>α : Type u_3<VAR>LT α<VAR>self : NoMinOrder α<VAR>a : α<GOAL>∃ b, b < a
<VAR>α : Type u_3<VAR>LT α<VAR>self : NoMaxOrder α<VAR>a : α<GOAL>∃ b, a < b
<VAR>α : Type u_3<VAR>LinearOrder α<VAR>NoBotOrder α<GOAL>NoMinOrder α
<VAR>α : Type u_3<VAR>LinearOrder α<VAR>NoTopOrder α<GOAL>NoMaxOrder α
<VAR>α : Type u_3<VAR>LinearOrder α<GOAL>NoBotOrder α ↔ NoMinOrder α
<VAR>α : Type u_3<VAR>LinearOrder α<GOAL>NoTopOrder α ↔ NoMaxOrder α
<VAR>α : Type u_1<VAR>LT α<VAR>NoMinOrder α<VAR>a : α<GOAL>¬Acc (fun x x_1 => x < x_1) a
<VAR>α : Type u_1<VAR>LT α<VAR>NoMaxOrder α<VAR>a : α<GOAL>¬Acc (fun x x_1 => x > x_1) a
<VAR>α : Type u_1<VAR>LE α<VAR>NoBotOrder α<VAR>a : α<GOAL>¬IsBot a
<VAR>α : Type u_1<VAR>LE α<VAR>NoTopOrder α<VAR>a : α<GOAL>¬IsTop a
<VAR>α : Type u_1<VAR>LE α<VAR>a : α<VAR>h : IsBot a<GOAL>IsMin a
<VAR>α : Type u_1<VAR>LE α<VAR>a : α<VAR>h : IsTop a<GOAL>IsMax a
<VAR>α : Type u_1<VAR>LE α<VAR>a : α<GOAL>IsBot (OrderDual.toDual a) ↔ IsTop a
<VAR>α : Type u_1<VAR>LE α<VAR>a : α<GOAL>IsTop (OrderDual.toDual a) ↔ IsBot a
<VAR>α : Type u_1<VAR>LE α<VAR>a : α<GOAL>IsMin (OrderDual.toDual a) ↔ IsMax a
<VAR>α : Type u_1<VAR>LE α<VAR>a : α<GOAL>IsMax (OrderDual.toDual a) ↔ IsMin a
<VAR>α : Type u_1<VAR>LE α<VAR>a : αᵒᵈ<GOAL>IsBot (OrderDual.ofDual a) ↔ IsTop a
<VAR>α : Type u_1<VAR>LE α<VAR>a : αᵒᵈ<GOAL>IsTop (OrderDual.ofDual a) ↔ IsBot a
<VAR>α : Type u_1<VAR>LE α<VAR>a : αᵒᵈ<GOAL>IsMin (OrderDual.ofDual a) ↔ IsMax a
<VAR>α : Type u_1<VAR>LE α<VAR>a : αᵒᵈ<GOAL>IsMax (OrderDual.ofDual a) ↔ IsMin a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>ha : IsBot a<VAR>h : b ≤ a<GOAL>IsBot b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>ha : IsTop a<VAR>h : a ≤ b<GOAL>IsTop b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>ha : IsMin a<VAR>h : b ≤ a<GOAL>IsMin b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>ha : IsMax a<VAR>h : a ≤ b<GOAL>IsMax b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : IsMin a<GOAL>¬b < a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : IsMax a<GOAL>¬a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : b < a<GOAL>¬IsMin a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>h : a < b<GOAL>¬IsMax a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>IsMin a ↔ ∀ (b : α), ¬b < a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>IsMax a ↔ ∀ (b : α), ¬a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>¬IsMin a ↔ ∃ b, b < a
<VAR>α : Type u_1<VAR>Preorder α<VAR>a : α<GOAL>¬IsMax a ↔ ∃ b, a < b
<VAR>α : Type u_1<VAR>Preorder α<VAR>NoMinOrder α<VAR>a : α<GOAL>¬IsMin a
<VAR>α : Type u_1<VAR>Preorder α<VAR>NoMaxOrder α<VAR>a : α<GOAL>¬IsMax a
<VAR>α : Type u_1<VAR>Preorder α<VAR>Subsingleton α<VAR>a : α<GOAL>IsBot a
<VAR>α : Type u_1<VAR>Preorder α<VAR>Subsingleton α<VAR>a : α<GOAL>IsTop a
<VAR>α : Type u_1<VAR>Preorder α<VAR>Subsingleton α<VAR>a : α<GOAL>IsMin a
<VAR>α : Type u_1<VAR>Preorder α<VAR>Subsingleton α<VAR>a : α<GOAL>IsMax a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>ha : IsMin a<VAR>h : b ≤ a<GOAL>b = a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>ha : IsMin a<VAR>h : b ≤ a<GOAL>a = b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>ha : IsMax a<VAR>h : a ≤ b<GOAL>a = b
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>a b : α<VAR>ha : IsMax a<VAR>h : a ≤ b<GOAL>b = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>a : α<VAR>b : β<VAR>ha : IsBot a<VAR>hb : IsBot b<GOAL>IsBot (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>a : α<VAR>b : β<VAR>ha : IsTop a<VAR>hb : IsTop b<GOAL>IsTop (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>a : α<VAR>b : β<VAR>ha : IsMin a<VAR>hb : IsMin b<GOAL>IsMin (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>a : α<VAR>b : β<VAR>ha : IsMax a<VAR>hb : IsMax b<GOAL>IsMax (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>x : α × β<VAR>hx : IsBot x<GOAL>IsBot x.1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>x : α × β<VAR>hx : IsBot x<GOAL>IsBot x.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>x : α × β<VAR>hx : IsTop x<GOAL>IsTop x.1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>x : α × β<VAR>hx : IsTop x<GOAL>IsTop x.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>x : α × β<VAR>hx : IsMin x<GOAL>IsMin x.1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>x : α × β<VAR>hx : IsMin x<GOAL>IsMin x.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>x : α × β<VAR>hx : IsMax x<GOAL>IsMax x.1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>x : α × β<VAR>hx : IsMax x<GOAL>IsMax x.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>x : α × β<GOAL>IsBot x ↔ IsBot x.1 ∧ IsBot x.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>x : α × β<GOAL>IsTop x ↔ IsTop x.1 ∧ IsTop x.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>x : α × β<GOAL>IsMin x ↔ IsMin x.1 ∧ IsMin x.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder α<VAR>Preorder β<VAR>x : α × β<GOAL>IsMax x ↔ IsMax x.1 ∧ IsMax x.2
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>⇑1 = id
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>e₁ e₂ : r ≃r r<GOAL>⇑(e₁ * e₂) = ⇑e₁ ∘ ⇑e₂
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>e₁ e₂ : r ≃r r<VAR>x : α<GOAL>(e₁ * e₂) x = e₁ (e₂ x)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>e : r ≃r r<VAR>x : α<GOAL>e⁻¹ (e x) = x
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>e : r ≃r r<VAR>x : α<GOAL>e (e⁻¹ x) = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_5<VAR>SemilatticeInf α<VAR>LinearOrder β<VAR>FunLike F β α<VAR>RelHomClass F (fun x x_1 => x < x_1) fun x x_1 => x < x_1<VAR>a : F<VAR>m n : β<GOAL>a (m ⊓ n) = a m ⊓ a n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_5<VAR>SemilatticeSup α<VAR>LinearOrder β<VAR>FunLike F β α<VAR>RelHomClass F (fun x x_1 => x > x_1) fun x x_1 => x > x_1<VAR>a : F<VAR>m n : β<GOAL>a (m ⊔ n) = a m ⊔ a n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>e : r ≃r s<GOAL>Set.range ⇑e = Set.univ
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>p : Set α<VAR>a b : ↑p<GOAL>Subrel r p a b ↔ r ↑a ↑b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>p : Set α<VAR>a : ↑p<GOAL>(Subrel.relEmbedding r p) a = ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>p : Set β<VAR>f : r ↪r s<VAR>H : ∀ (a : α), f a ∈ p<VAR>a : α<GOAL>(RelEmbedding.codRestrict p f H) a = ⟨f a, ⋯⟩
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>e : r ≃r s<VAR>t : Set α<GOAL>⇑e '' t = ⇑e.symm ⁻¹' t
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>e : r ≃r s<VAR>t : Set β<GOAL>⇑e ⁻¹' t = ⇑e.symm '' t
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsPartialOrder α r<GOAL>∃ s, IsLinearOrder α s ∧ r ≤ s
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>HeytingAlgebra α<VAR>HeytingAlgebra β<VAR>self : HeytingHom α β<GOAL>self.toFun ⊥ = ⊥
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>HeytingAlgebra α<VAR>HeytingAlgebra β<VAR>self : HeytingHom α β<VAR>a b : α<GOAL>self.toFun (a ⇨ b) = self.toFun a ⇨ self.toFun b
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>CoheytingAlgebra α<VAR>CoheytingAlgebra β<VAR>self : CoheytingHom α β<GOAL>self.toFun ⊤ = ⊤
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>CoheytingAlgebra α<VAR>CoheytingAlgebra β<VAR>self : CoheytingHom α β<VAR>a b : α<GOAL>self.toFun (a \ b) = self.toFun a \ self.toFun b
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>BiheytingAlgebra α<VAR>BiheytingAlgebra β<VAR>self : BiheytingHom α β<VAR>a b : α<GOAL>self.toFun (a ⇨ b) = self.toFun a ⇨ self.toFun b
<VAR>α : Type u_6<VAR>β : Type u_7<VAR>BiheytingAlgebra α<VAR>BiheytingAlgebra β<VAR>self : BiheytingHom α β<VAR>a b : α<GOAL>self.toFun (a \ b) = self.toFun a \ self.toFun b
<VAR>F : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>HeytingAlgebra α<VAR>HeytingAlgebra β<VAR>FunLike F α β<VAR>self : HeytingHomClass F α β<VAR>f : F<GOAL>f ⊥ = ⊥
<VAR>F : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>HeytingAlgebra α<VAR>HeytingAlgebra β<VAR>FunLike F α β<VAR>self : HeytingHomClass F α β<VAR>f : F<VAR>a b : α<GOAL>f (a ⇨ b) = f a ⇨ f b
<VAR>F : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>CoheytingAlgebra α<VAR>CoheytingAlgebra β<VAR>FunLike F α β<VAR>self : CoheytingHomClass F α β<VAR>f : F<GOAL>f ⊤ = ⊤
<VAR>F : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>CoheytingAlgebra α<VAR>CoheytingAlgebra β<VAR>FunLike F α β<VAR>self : CoheytingHomClass F α β<VAR>f : F<VAR>a b : α<GOAL>f (a \ b) = f a \ f b
<VAR>F : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>BiheytingAlgebra α<VAR>BiheytingAlgebra β<VAR>FunLike F α β<VAR>self : BiheytingHomClass F α β<VAR>f : F<VAR>a b : α<GOAL>f (a \ b) = f a \ f b
<VAR>F : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>BiheytingAlgebra α<VAR>BiheytingAlgebra β<VAR>FunLike F α β<VAR>self : BiheytingHomClass F α β<VAR>f : F<VAR>a b : α<GOAL>f (a ⇨ b) = f a ⇨ f b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>FunLike F α β<VAR>BooleanAlgebra α<VAR>BooleanAlgebra β<VAR>BoundedLatticeHomClass F α β<GOAL>BiheytingHomClass F α β
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>FunLike F α β<VAR>HeytingAlgebra α<VAR>HeytingAlgebra β<VAR>HeytingHomClass F α β<VAR>f : F<VAR>a : α<GOAL>f aᶜ = (f a)ᶜ
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>FunLike F α β<VAR>HeytingAlgebra α<VAR>HeytingAlgebra β<VAR>HeytingHomClass F α β<VAR>f : F<VAR>a b : α<GOAL>f (bihimp a b) = bihimp (f a) (f b)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>FunLike F α β<VAR>CoheytingAlgebra α<VAR>CoheytingAlgebra β<VAR>CoheytingHomClass F α β<VAR>f : F<VAR>a : α<GOAL>f (￢a) = ￢f a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>FunLike F α β<VAR>CoheytingAlgebra α<VAR>CoheytingAlgebra β<VAR>CoheytingHomClass F α β<VAR>f : F<VAR>a b : α<GOAL>f (symmDiff a b) = symmDiff (f a) (f b)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>HeytingAlgebra α<VAR>HeytingAlgebra β<VAR>f : HeytingHom α β<GOAL>f.toFun = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>HeytingAlgebra α<VAR>HeytingAlgebra β<VAR>f : HeytingHom α β<GOAL>⇑f.toLatticeHom = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>HeytingAlgebra α<VAR>HeytingAlgebra β<VAR>f g : HeytingHom α β<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>HeytingAlgebra α<VAR>HeytingAlgebra β<VAR>f : HeytingHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>HeytingAlgebra α<VAR>HeytingAlgebra β<VAR>f : HeytingHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_2<VAR>HeytingAlgebra α<GOAL>⇑(HeytingHom.id α) = id
<VAR>α : Type u_2<VAR>HeytingAlgebra α<VAR>a : α<GOAL>(HeytingHom.id α) a = a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>HeytingAlgebra α<VAR>HeytingAlgebra β<VAR>HeytingAlgebra γ<VAR>f : HeytingHom β γ<VAR>g : HeytingHom α β<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>HeytingAlgebra α<VAR>HeytingAlgebra β<VAR>HeytingAlgebra γ<VAR>f : HeytingHom β γ<VAR>g : HeytingHom α β<VAR>a : α<GOAL>(f.comp g) a = f (g a)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>HeytingAlgebra α<VAR>HeytingAlgebra β<VAR>HeytingAlgebra γ<VAR>HeytingAlgebra δ<VAR>f : HeytingHom γ δ<VAR>g : HeytingHom β γ<VAR>h : HeytingHom α β<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>HeytingAlgebra α<VAR>HeytingAlgebra β<VAR>f : HeytingHom α β<GOAL>f.comp (HeytingHom.id α) = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>HeytingAlgebra α<VAR>HeytingAlgebra β<VAR>f : HeytingHom α β<GOAL>(HeytingHom.id β).comp f = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>HeytingAlgebra α<VAR>HeytingAlgebra β<VAR>HeytingAlgebra γ<VAR>f : HeytingHom α β<VAR>g₁ g₂ : HeytingHom β γ<VAR>hf : Function.Surjective ⇑f<GOAL>g₁.comp f = g₂.comp f ↔ g₁ = g₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>HeytingAlgebra α<VAR>HeytingAlgebra β<VAR>HeytingAlgebra γ<VAR>f₁ f₂ : HeytingHom α β<VAR>g : HeytingHom β γ<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CoheytingAlgebra α<VAR>CoheytingAlgebra β<VAR>f : CoheytingHom α β<GOAL>f.toFun = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CoheytingAlgebra α<VAR>CoheytingAlgebra β<VAR>f : CoheytingHom α β<GOAL>⇑f.toLatticeHom = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CoheytingAlgebra α<VAR>CoheytingAlgebra β<VAR>f g : CoheytingHom α β<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CoheytingAlgebra α<VAR>CoheytingAlgebra β<VAR>f : CoheytingHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CoheytingAlgebra α<VAR>CoheytingAlgebra β<VAR>f : CoheytingHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<GOAL>⇑(CoheytingHom.id α) = id
<VAR>α : Type u_2<VAR>CoheytingAlgebra α<VAR>a : α<GOAL>(CoheytingHom.id α) a = a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>CoheytingAlgebra α<VAR>CoheytingAlgebra β<VAR>CoheytingAlgebra γ<VAR>f : CoheytingHom β γ<VAR>g : CoheytingHom α β<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>CoheytingAlgebra α<VAR>CoheytingAlgebra β<VAR>CoheytingAlgebra γ<VAR>f : CoheytingHom β γ<VAR>g : CoheytingHom α β<VAR>a : α<GOAL>(f.comp g) a = f (g a)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>CoheytingAlgebra α<VAR>CoheytingAlgebra β<VAR>CoheytingAlgebra γ<VAR>CoheytingAlgebra δ<VAR>f : CoheytingHom γ δ<VAR>g : CoheytingHom β γ<VAR>h : CoheytingHom α β<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CoheytingAlgebra α<VAR>CoheytingAlgebra β<VAR>f : CoheytingHom α β<GOAL>f.comp (CoheytingHom.id α) = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CoheytingAlgebra α<VAR>CoheytingAlgebra β<VAR>f : CoheytingHom α β<GOAL>(CoheytingHom.id β).comp f = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>CoheytingAlgebra α<VAR>CoheytingAlgebra β<VAR>CoheytingAlgebra γ<VAR>f : CoheytingHom α β<VAR>g₁ g₂ : CoheytingHom β γ<VAR>hf : Function.Surjective ⇑f<GOAL>g₁.comp f = g₂.comp f ↔ g₁ = g₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>CoheytingAlgebra α<VAR>CoheytingAlgebra β<VAR>CoheytingAlgebra γ<VAR>f₁ f₂ : CoheytingHom α β<VAR>g : CoheytingHom β γ<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>BiheytingAlgebra α<VAR>BiheytingAlgebra β<VAR>f : BiheytingHom α β<GOAL>f.toFun = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>BiheytingAlgebra α<VAR>BiheytingAlgebra β<VAR>f : BiheytingHom α β<GOAL>⇑f.toLatticeHom = ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>BiheytingAlgebra α<VAR>BiheytingAlgebra β<VAR>f g : BiheytingHom α β<VAR>h : ∀ (a : α), f a = g a<GOAL>f = g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>BiheytingAlgebra α<VAR>BiheytingAlgebra β<VAR>f : BiheytingHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>BiheytingAlgebra α<VAR>BiheytingAlgebra β<VAR>f : BiheytingHom α β<VAR>f' : α → β<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>α : Type u_2<VAR>BiheytingAlgebra α<GOAL>⇑(BiheytingHom.id α) = id
<VAR>α : Type u_2<VAR>BiheytingAlgebra α<VAR>a : α<GOAL>(BiheytingHom.id α) a = a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>BiheytingAlgebra α<VAR>BiheytingAlgebra β<VAR>BiheytingAlgebra γ<VAR>f : BiheytingHom β γ<VAR>g : BiheytingHom α β<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>BiheytingAlgebra α<VAR>BiheytingAlgebra β<VAR>BiheytingAlgebra γ<VAR>f : BiheytingHom β γ<VAR>g : BiheytingHom α β<VAR>a : α<GOAL>(f.comp g) a = f (g a)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>BiheytingAlgebra α<VAR>BiheytingAlgebra β<VAR>BiheytingAlgebra γ<VAR>BiheytingAlgebra δ<VAR>f : BiheytingHom γ δ<VAR>g : BiheytingHom β γ<VAR>h : BiheytingHom α β<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>BiheytingAlgebra α<VAR>BiheytingAlgebra β<VAR>f : BiheytingHom α β<GOAL>f.comp (BiheytingHom.id α) = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>BiheytingAlgebra α<VAR>BiheytingAlgebra β<VAR>f : BiheytingHom α β<GOAL>(BiheytingHom.id β).comp f = f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>BiheytingAlgebra α<VAR>BiheytingAlgebra β<VAR>BiheytingAlgebra γ<VAR>f : BiheytingHom α β<VAR>g₁ g₂ : BiheytingHom β γ<VAR>hf : Function.Surjective ⇑f<GOAL>g₁.comp f = g₂.comp f ↔ g₁ = g₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>BiheytingAlgebra α<VAR>BiheytingAlgebra β<VAR>BiheytingAlgebra γ<VAR>f₁ f₂ : BiheytingHom α β<VAR>g : BiheytingHom β γ<VAR>hg : Function.Injective ⇑g<GOAL>g.comp f₁ = g.comp f₂ ↔ f₁ = f₂
<VAR>G : Type u_1<VAR>Group G<VAR>D H : Subgroup G<VAR>D.FiniteIndex<VAR>hD_le_H : D ≤ H<GOAL>∃ t, ↑t ∈ Subgroup.leftTransversals ↑(D.subgroupOf H) ∧ ⋃ g ∈ t, ↑g • ↑D = ↑H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>D H : AddSubgroup G<VAR>D.FiniteIndex<VAR>hD_le_H : D ≤ H<GOAL>∃ t, ↑t ∈ AddSubgroup.leftTransversals ↑(D.addSubgroupOf H) ∧ ⋃ g ∈ t, ↑g +ᵥ ↑D = ↑H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>H : AddSubgroup G<VAR>g : ι → G<GOAL>⋃ i ∈ s, g i +ᵥ ↑H = Set.univ ↔ Set.SurjOn (fun x => ↑(g x)) (↑s) Set.univ
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>H : Subgroup G<VAR>g : ι → G<GOAL>⋃ i ∈ s, g i • ↑H = Set.univ ↔ Set.SurjOn (fun x => ↑(g x)) (↑s) Set.univ
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>H : AddSubgroup G<VAR>g : ι → G<VAR>hcovers : ⋃ i ∈ s, g i +ᵥ ↑H = Set.univ<GOAL>H.FiniteIndex
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>H : Subgroup G<VAR>g : ι → G<VAR>hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ<GOAL>H.FiniteIndex
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>H : Subgroup G<VAR>g : ι → G<VAR>hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ<GOAL>H.index ≤ s.card
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>H : AddSubgroup G<VAR>g : ι → G<VAR>hcovers : ⋃ i ∈ s, g i +ᵥ ↑H = Set.univ<GOAL>H.index ≤ s.card
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>H : Subgroup G<VAR>g : ι → G<VAR>hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ<VAR>hind : H.index = s.card<GOAL>(↑s).PairwiseDisjoint fun x => g x • ↑H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>H : AddSubgroup G<VAR>g : ι → G<VAR>hcovers : ⋃ i ∈ s, g i +ᵥ ↑H = Set.univ<VAR>hind : H.index = s.card<GOAL>(↑s).PairwiseDisjoint fun x => g x +ᵥ ↑H
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Type u_2<VAR>H : ι → AddSubgroup G<VAR>g : ι → G<VAR>s : Finset ι<VAR>hcovers : ⋃ i ∈ s, g i +ᵥ ↑(H i) = Set.univ<VAR>DecidableEq (AddSubgroup G)<VAR>j : ι<VAR>hj : j ∈ s<VAR>hcovers' : ⋃ i ∈ Finset.filter (fun x => H x = H j) s, g i +ᵥ ↑(H i) ≠ Set.univ<GOAL>∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Type u_2<VAR>H : ι → Subgroup G<VAR>g : ι → G<VAR>s : Finset ι<VAR>hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ<VAR>DecidableEq (Subgroup G)<VAR>j : ι<VAR>hj : j ∈ s<VAR>hcovers' : ⋃ i ∈ Finset.filter (fun x => H x = H j) s, g i • ↑(H i) ≠ Set.univ<GOAL>∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Type u_2<VAR>H : ι → Subgroup G<VAR>g : ι → G<VAR>s : Finset ι<VAR>hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ<GOAL>∃ k ∈ s, (H k).FiniteIndex
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Type u_2<VAR>H : ι → AddSubgroup G<VAR>g : ι → G<VAR>s : Finset ι<VAR>hcovers : ⋃ i ∈ s, g i +ᵥ ↑(H i) = Set.univ<GOAL>∃ k ∈ s, (H k).FiniteIndex
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Type u_2<VAR>H : ι → AddSubgroup G<VAR>g : ι → G<VAR>s : Finset ι<VAR>hcovers : ⋃ i ∈ s, g i +ᵥ ↑(H i) = Set.univ<VAR>DecidablePred AddSubgroup.FiniteIndex<GOAL>⋃ k ∈ Finset.filter (fun i => (H i).FiniteIndex) s, g k +ᵥ ↑(H k) = Set.univ ∧ 1 ≤ ∑ i ∈ s, (↑(H i).index)⁻¹ ∧ (∑ i ∈ s, (↑(H i).index)⁻¹ = 1 → (↑(Finset.filter (fun i => (H i).FiniteIndex) s)).PairwiseDisjoint fun i => g i +ᵥ ↑(H i))
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Type u_2<VAR>H : ι → Subgroup G<VAR>g : ι → G<VAR>s : Finset ι<VAR>hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ<VAR>DecidablePred Subgroup.FiniteIndex<GOAL>⋃ k ∈ Finset.filter (fun i => (H i).FiniteIndex) s, g k • ↑(H k) = Set.univ ∧ 1 ≤ ∑ i ∈ s, (↑(H i).index)⁻¹ ∧ (∑ i ∈ s, (↑(H i).index)⁻¹ = 1 → (↑(Finset.filter (fun i => (H i).FiniteIndex) s)).PairwiseDisjoint fun i => g i • ↑(H i))
<VAR>G : Type u_1<VAR>Group G<VAR>ι : Type u_2<VAR>H : ι → Subgroup G<VAR>g : ι → G<VAR>s : Finset ι<VAR>hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ<VAR>DecidablePred Subgroup.FiniteIndex<GOAL>⋃ k ∈ Finset.filter (fun i => (H i).FiniteIndex) s, g k • ↑(H k) = Set.univ
<VAR>G : Type u_1<VAR>AddGroup G<VAR>ι : Type u_2<VAR>H : ι → AddSubgroup G<VAR>g : ι → G<VAR>s : Finset ι<VAR>hcovers : ⋃ i ∈ s, g i +ᵥ ↑(H i) = Set.univ<VAR>DecidablePred AddSubgroup.FiniteIndex<GOAL>⋃ k ∈ Finset.filter (fun i => (H i).FiniteIndex) s, g k +ᵥ ↑(H k) = Set.univ