ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : ℕ<VAR>α β γ : TypeVec.{u} n<VAR>F : TypeVec.{u} n → Type v<VAR>MvFunctor F<VAR>LawfulMvFunctor F<VAR>g : α ⟹ β<VAR>h : β ⟹ γ<VAR>x : F α<GOAL>h <$$> g <$$> x = (h ⊚ g) <$$> x
<VAR>n : ℕ<VAR>α β : TypeVec.{u} n<VAR>F : TypeVec.{u} n → Type v<VAR>MvFunctor F<VAR>LawfulMvFunctor F<VAR>P : F α → Prop<VAR>q : F β → Prop<VAR>f : α ⟹ β<VAR>g : β ⟹ α<VAR>h₀ : f ⊚ g = TypeVec.id<VAR>h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)<GOAL>(∃ u, P u) ↔ ∃ u, q u
<VAR>n : ℕ<VAR>α : TypeVec.{u} n<VAR>F : TypeVec.{u} n → Type v<VAR>MvFunctor F<VAR>P : α ⟹ TypeVec.repeat n Prop<VAR>LawfulMvFunctor F<VAR>x : F α<GOAL>MvFunctor.LiftP' P x ↔ ∃ u, TypeVec.subtypeVal P <$$> u = x
<VAR>n : ℕ<VAR>α : TypeVec.{u} n<VAR>F : TypeVec.{u} n → Type v<VAR>MvFunctor F<VAR>R : α ⊗ α ⟹ TypeVec.repeat n Prop<VAR>LawfulMvFunctor F<VAR>x y : F α<GOAL>MvFunctor.LiftR' R x y ↔ ∃ u, (TypeVec.prod.fst ⊚ TypeVec.subtypeVal R) <$$> u = x ∧ (TypeVec.prod.snd ⊚ TypeVec.subtypeVal R) <$$> u = y
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u_1<VAR>MvFunctor F<VAR>LawfulMvFunctor F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>P : β → Prop<VAR>x : F (α ::: β)<GOAL>MvFunctor.LiftP' (α.PredLast' P) x ↔ MvFunctor.LiftP (α.PredLast P) x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u_1<VAR>MvFunctor F<VAR>LawfulMvFunctor F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>rr : β → β → Prop<VAR>x y : F (α ::: β)<GOAL>MvFunctor.LiftR' (α.RelLast' rr) x y ↔ MvFunctor.LiftR (fun {i} => α.RelLast rr) x y
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>S : Set α<VAR>self : IsCompactlyGenerated.BooleanGenerators S<VAR>I : α<GOAL>I ∈ S → IsAtom I
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>S : Set α<VAR>self : IsCompactlyGenerated.BooleanGenerators S<VAR>s : Finset α<VAR>a : α<GOAL>↑s ⊆ S → CompleteLattice.IsCompactElement a → a ≤ s.sup id → ∃ t ⊆ s, a = t.sup id
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>S : Set α<VAR>hS : IsCompactlyGenerated.BooleanGenerators S<VAR>T : Set α<VAR>hTS : T ⊆ S<GOAL>IsCompactlyGenerated.BooleanGenerators T
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : IsCompactlyGenerated.BooleanGenerators S<VAR>a : α<VAR>ha : a ≤ sSup S<GOAL>∃ T ⊆ S, a = sSup T
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : IsCompactlyGenerated.BooleanGenerators S<VAR>h : sSup S = ⊤<GOAL>IsAtomistic α
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : IsCompactlyGenerated.BooleanGenerators S<VAR>a : α<VAR>ha : IsAtom a<VAR>haS : a ≤ sSup S<GOAL>a ∈ S
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : IsCompactlyGenerated.BooleanGenerators S<VAR>T₁ T₂ : Set α<VAR>hT₁ : T₁ ⊆ S<VAR>hT₂ : T₂ ⊆ S<GOAL>sSup (T₁ ∩ T₂) = sSup T₁ ⊓ sSup T₂
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : IsCompactlyGenerated.BooleanGenerators S<VAR>h : sSup S = ⊤<GOAL>ComplementedLattice α
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : IsCompactlyGenerated.BooleanGenerators S<VAR>X Y : Set α<VAR>hX : X ⊆ S<VAR>hY : Y ⊆ S<GOAL>sSup X ≤ sSup Y ↔ X ⊆ Y
<VAR>α : Type u_1<VAR>CompleteLattice α<VAR>IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : IsCompactlyGenerated.BooleanGenerators S<VAR>h : sSup S = ⊤<GOAL>S = {a | IsAtom a}
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>IsChain r ∅
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>hs : s.Subsingleton<GOAL>IsChain r s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<GOAL>s ⊆ t → IsChain r t → IsChain r s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>r' : α → α → Prop<VAR>h : IsChain r s<VAR>h_imp : ∀ (x y : α), r x y → r' x y<GOAL>IsChain r' s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>h : IsChain r s<GOAL>IsChain (flip r) s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsTrichotomous α r<VAR>s : Set α<GOAL>IsChain r s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>a : α<VAR>hs : IsChain r s<VAR>ha : ∀ b ∈ s, a ≠ b → r a b ∨ r b a<GOAL>IsChain r (insert a s)
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>IsChain r Set.univ ↔ IsTrichotomous α r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : α → β<VAR>h : ∀ (x y : α), r x y → s (f x) (f y)<VAR>c : Set α<VAR>hrc : IsChain r c<GOAL>IsChain s (f '' c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Monotone f<GOAL>IsChain (fun x x_1 => x ≤ x_1) (Set.range f)
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s : Set α<VAR>h : IsChain (fun x x_1 => x ≤ x_1) s<GOAL>IsChain (fun x x_1 => x < x_1) s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>x y : α<VAR>IsRefl α r<VAR>h : IsChain r s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>r x y ∨ r y x
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>IsRefl α r<VAR>H : IsChain r s<GOAL>DirectedOn r s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>IsRefl α r<VAR>f : β → α<VAR>c : Set β<VAR>h : IsChain (f ⁻¹'o r) c<GOAL>Directed r fun x => f ↑x
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>IsRefl α r<VAR>hchain : IsChain r s<VAR>IsTrans α r<VAR>a b c : α<VAR>mem1 : a ∈ s<VAR>mem2 : b ∈ s<VAR>mem3 : c ∈ s<GOAL>∃ z, ∃ (_ : z ∈ s), r a z ∧ r b z ∧ r c z
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>h : IsMaxChain r s<GOAL>IsChain r s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>h : IsMaxChain r s<GOAL>¬SuperChain r s t
<VAR>α : Type u_1<VAR>s : Set α<VAR>LE α<VAR>OrderBot α<VAR>h : IsMaxChain (fun x x_1 => x ≤ x_1) s<GOAL>⊥ ∈ s
<VAR>α : Type u_1<VAR>s : Set α<VAR>LE α<VAR>OrderTop α<VAR>h : IsMaxChain (fun x x_1 => x ≤ x_1) s<GOAL>⊤ ∈ s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>h : ∃ t, IsChain r s ∧ SuperChain r s t<GOAL>SuperChain r s (SuccChain r s)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>hs : IsChain r s<GOAL>IsChain r (SuccChain r s)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<VAR>hs₁ : IsChain r s<VAR>hs₂ : ¬IsMaxChain r s<GOAL>SuperChain r s (SuccChain r s)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set α<GOAL>s ⊆ SuccChain r s
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>ChainClosure r ∅
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>ChainClosure r (maxChain r)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>c₁ c₂ : Set α<VAR>hc₁ : ChainClosure r c₁<VAR>h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂<GOAL>SuccChain r c₂ ⊆ c₁ ∨ c₁ ⊆ c₂
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>c₁ c₂ : Set α<VAR>hc₁ : ChainClosure r c₁<VAR>hc₂ : ChainClosure r c₂<VAR>h : c₁ ⊆ c₂<GOAL>c₂ = c₁ ∨ SuccChain r c₁ ⊆ c₂
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>c₁ c₂ : Set α<VAR>hc₁ : ChainClosure r c₁<VAR>hc₂ : ChainClosure r c₂<GOAL>c₁ ⊆ c₂ ∨ c₂ ⊆ c₁
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>c₁ c₂ : Set α<VAR>hc₁ : ChainClosure r c₁<VAR>hc₂ : ChainClosure r c₂<VAR>hc : SuccChain r c₂ = c₂<GOAL>c₁ ⊆ c₂
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>c : Set α<VAR>hc : ChainClosure r c<GOAL>SuccChain r c = c ↔ c = maxChain r
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>c : Set α<VAR>hc : ChainClosure r c<GOAL>IsChain r c
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>IsMaxChain r (maxChain r)
<VAR>α : Type u_3<VAR>LE α<VAR>self : Flag α<GOAL>IsChain (fun x x_1 => x ≤ x_1) self.carrier
<VAR>α : Type u_3<VAR>LE α<VAR>self : Flag α<VAR>s : Set α<GOAL>IsChain (fun x x_1 => x ≤ x_1) s → self.carrier ⊆ s → self.carrier = s
<VAR>α : Type u_1<VAR>LE α<VAR>s t : Flag α<GOAL>↑s = ↑t → s = t
<VAR>α : Type u_1<VAR>LE α<VAR>s : Flag α<VAR>a : α<GOAL>a ∈ ↑s ↔ a ∈ s
<VAR>α : Type u_1<VAR>LE α<VAR>s : Set α<VAR>h₁ : IsChain (fun x x_1 => x ≤ x_1) s<VAR>h₂ : ∀ ⦃s_1 : Set α⦄, IsChain (fun x x_1 => x ≤ x_1) s_1 → s ⊆ s_1 → s = s_1<GOAL>↑{ carrier := s, Chain' := h₁, max_chain' := h₂ } = s
<VAR>α : Type u_1<VAR>LE α<VAR>s : Flag α<GOAL>{ carrier := ↑s, Chain' := ⋯, max_chain' := ⋯ } = s
<VAR>α : Type u_1<VAR>LE α<VAR>s : Flag α<GOAL>IsChain (fun x x_1 => x ≤ x_1) ↑s
<VAR>α : Type u_1<VAR>LE α<VAR>s : Flag α<GOAL>IsMaxChain (fun x x_1 => x ≤ x_1) ↑s
<VAR>α : Type u_1<VAR>LE α<VAR>OrderTop α<VAR>s : Flag α<GOAL>⊤ ∈ s
<VAR>α : Type u_1<VAR>LE α<VAR>OrderBot α<VAR>s : Flag α<GOAL>⊥ ∈ s
<VAR>α : Type u_1<VAR>Preorder α<VAR>a b : α<VAR>s : Flag α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>a ≤ b ∨ b ≤ a
<VAR>α : Type u_1<VAR>PartialOrder α<VAR>s : Flag α<GOAL>IsChain (fun x x_1 => x < x_1) ↑s
<VAR>α : Type u_2<VAR>s : Set α<GOAL>s ∈ Filter.cofinite ↔ sᶜ.Finite
<VAR>α : Type u_2<VAR>p : α → Prop<GOAL>(∀ᶠ (x : α) in Filter.cofinite, p x) ↔ {x | ¬p x}.Finite
<VAR>α : Type u_2<GOAL>Filter.cofinite.HasBasis (fun s => s.Finite) compl
<VAR>α : Type u_2<GOAL>Filter.cofinite = ⊥ ↔ Finite α
<VAR>α : Type u_2<VAR>Finite α<GOAL>Filter.cofinite = ⊥
<VAR>α : Type u_2<VAR>p : α → Prop<GOAL>(∃ᶠ (x : α) in Filter.cofinite, p x) ↔ {x | p x}.Infinite
<VAR>α : Type u_2<VAR>s : Set α<GOAL>(∃ᶠ (x : α) in Filter.cofinite, x ∈ s) ↔ s.Infinite
<VAR>α : Type u_2<VAR>s : Set α<GOAL>(Filter.cofinite ⊓ 𝓟 s).NeBot ↔ s.Infinite
<VAR>α : Type u_2<VAR>s : Set α<VAR>hs : s.Finite<GOAL>sᶜ ∈ Filter.cofinite
<VAR>α : Type u_2<VAR>s : Set α<VAR>hs : s.Finite<GOAL>∀ᶠ (x : α) in Filter.cofinite, x ∉ s
<VAR>α : Type u_2<VAR>s : Finset α<GOAL>∀ᶠ (x : α) in Filter.cofinite, x ∉ s
<VAR>α : Type u_2<VAR>s : Set α<GOAL>s.Infinite ↔ ∃ᶠ (x : α) in Filter.cofinite, x ∈ s
<VAR>α : Type u_2<VAR>x : α<GOAL>∀ᶠ (a : α) in Filter.cofinite, a ≠ x
<VAR>α : Type u_2<VAR>l : Filter α<GOAL>l ≤ Filter.cofinite ↔ ∀ (x : α), {x}ᶜ ∈ l
<VAR>α : Type u_2<VAR>l : Filter α<GOAL>l ≤ Filter.cofinite ↔ ∀ (x : α), ∀ᶠ (y : α) in l, y ≠ x
<VAR>α : Type u_2<VAR>Preorder α<VAR>NoMaxOrder α<GOAL>Filter.atTop ≤ Filter.cofinite
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f : α → β<GOAL>Filter.comap f Filter.cofinite ≤ Filter.cofinite
<VAR>α : Type u_2<VAR>β : Type u_3<GOAL>Filter.cofinite.coprod Filter.cofinite = Filter.cofinite
<VAR>ι : Type u_1<VAR>α : ι → Type u_4<VAR>Finite ι<GOAL>(Filter.coprodᵢ fun i => Filter.cofinite) = Filter.cofinite
<VAR>α : Type u_2<VAR>l : Filter α<GOAL>Disjoint Filter.cofinite l ↔ ∃ s ∈ l, s.Finite
<VAR>α : Type u_2<VAR>l : Filter α<GOAL>Disjoint l Filter.cofinite ↔ ∃ s ∈ l, s.Finite
<VAR>α : Type u_2<VAR>l : Filter α<VAR>l.IsCountablyGenerated<VAR>h : Filter.cofinite ≤ l<GOAL>l.kerᶜ.Countable
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f : α → β<VAR>l : Filter β<VAR>l.IsCountablyGenerated<VAR>h : Filter.Tendsto f Filter.cofinite l<GOAL>(f ⁻¹' l.ker)ᶜ.Countable
<VAR>α : Type u_2<VAR>s : Set α<VAR>hs : s.Finite<GOAL>Filter.cofinite ⊓ 𝓟 sᶜ = Filter.cofinite
<VAR>α : Type u_2<VAR>s t : Set α<VAR>ht : t.Finite<GOAL>Filter.cofinite ⊓ 𝓟 (s \ t) = Filter.cofinite ⊓ 𝓟 s
<VAR>p : ℕ → Prop<GOAL>(∃ᶠ (n : ℕ) in Filter.atTop, p n) ↔ {n | p n}.Infinite
<GOAL>∀ᶠ (k : ℕ) in Filter.atTop, 0 < k
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>LinearOrder β<VAR>s : Set α<VAR>hs : s.Nonempty<VAR>f : α → β<VAR>hf : Filter.Tendsto f Filter.cofinite Filter.atTop<GOAL>∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Nonempty α<VAR>LinearOrder β<VAR>f : α → β<VAR>hf : Filter.Tendsto f Filter.cofinite Filter.atTop<GOAL>∃ a₀, ∀ (a : α), f a₀ ≤ f a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>LinearOrder β<VAR>s : Set α<VAR>hs : s.Nonempty<VAR>f : α → β<VAR>hf : Filter.Tendsto f Filter.cofinite Filter.atBot<GOAL>∃ a₀ ∈ s, ∀ a ∈ s, f a ≤ f a₀
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Nonempty α<VAR>LinearOrder β<VAR>f : α → β<VAR>hf : Filter.Tendsto f Filter.cofinite Filter.atBot<GOAL>∃ a₀, ∀ (a : α), f a ≤ f a₀
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f : α → β<VAR>hf : Function.Surjective f<GOAL>Filter.cofinite ≤ Filter.map f Filter.cofinite
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Filter.Tendsto f Filter.cofinite Filter.cofinite
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Filter.comap f Filter.cofinite = Filter.cofinite
<VAR>f : ℕ → ℕ<VAR>hf : Function.Injective f<GOAL>Filter.Tendsto f Filter.atTop Filter.atTop
<VAR>α : Type u<VAR>as bs : List (Filter α)<GOAL>List.Forall₂ (fun x x_1 => x ≤ x_1) as bs → sequence as ≤ sequence bs
<VAR>α β γ : Type u<VAR>f : β → Filter α<VAR>s : γ → Set α<VAR>fs : List β<VAR>us : List γ<GOAL>List.Forall₂ (fun b c => s c ∈ f b) fs us → traverse s us ∈ traverse f fs
<VAR>α β : Type u<VAR>f : β → Filter α<VAR>fs : List β<VAR>t : Set (List α)<GOAL>t ∈ traverse f fs ↔ ∃ us, List.Forall₂ (fun b s => s ∈ f b) fs us ∧ sequence us ⊆ t
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>a : ↥A<GOAL>HNNExtension.t * HNNExtension.of ↑a = HNNExtension.of ↑(φ a) * HNNExtension.t
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>b : ↥B<GOAL>HNNExtension.of ↑b * HNNExtension.t = HNNExtension.t * HNNExtension.of ↑(φ.symm b)
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>a : ↥A<GOAL>HNNExtension.of ↑(φ a) = HNNExtension.t * HNNExtension.of ↑a * HNNExtension.t⁻¹
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>b : ↥B<GOAL>HNNExtension.of ↑(φ.symm b) = HNNExtension.t⁻¹ * HNNExtension.of ↑b * HNNExtension.t
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>b : ↥B<GOAL>HNNExtension.t⁻¹ * HNNExtension.of ↑b = HNNExtension.of ↑(φ.symm b) * HNNExtension.t⁻¹
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>a : ↥A<GOAL>HNNExtension.of ↑a * HNNExtension.t⁻¹ = HNNExtension.t⁻¹ * HNNExtension.of ↑(φ a)
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>Group H<VAR>f : G →* H<VAR>x : H<VAR>hx : ∀ (a : ↥A), x * f ↑a = f ↑(φ a) * x<GOAL>(HNNExtension.lift f x hx) HNNExtension.t = x
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>Group H<VAR>f : G →* H<VAR>x : H<VAR>hx : ∀ (a : ↥A), x * f ↑a = f ↑(φ a) * x<VAR>g : G<GOAL>(HNNExtension.lift f x hx) (HNNExtension.of g) = f g
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>M : Type u_3<VAR>Monoid M<VAR>f g : HNNExtension G A B φ →* M<VAR>hg : f.comp HNNExtension.of = g.comp HNNExtension.of<VAR>ht : f HNNExtension.t = g HNNExtension.t<GOAL>f = g
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>motive : HNNExtension G A B φ → Prop<VAR>x : HNNExtension G A B φ<VAR>of : ∀ (g : G), motive (HNNExtension.of g)<VAR>t : motive HNNExtension.t<VAR>mul : ∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)<VAR>inv : ∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹<GOAL>motive x
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<GOAL>HNNExtension.toSubgroup A B 1 = A
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<GOAL>HNNExtension.toSubgroup A B (-1) = B
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<GOAL>HNNExtension.toSubgroupEquiv φ 1 = φ
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<GOAL>HNNExtension.toSubgroupEquiv φ (-1) = φ.symm
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>u : ℤˣ<VAR>a : ↥(HNNExtension.toSubgroup A B u)<GOAL>↑((HNNExtension.toSubgroupEquiv φ (-u)) ((HNNExtension.toSubgroupEquiv φ u) a)) = ↑a
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>self : HNNExtension.NormalWord.TransversalPair G A B<VAR>u : ℤˣ<GOAL>Subgroup.IsComplement (↑(HNNExtension.toSubgroup A B u)) (self.set u)
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>self : HNNExtension.NormalWord.ReducedWord G A B<GOAL>List.Chain' (fun a b => a.2 ∈ HNNExtension.toSubgroup A B a.1 → a.1 = b.1) self.toList
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<GOAL>(HNNExtension.NormalWord.ReducedWord.empty G A B).head = 1
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<GOAL>(HNNExtension.NormalWord.ReducedWord.empty G A B).toList = []
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>self : HNNExtension.NormalWord d<VAR>u : ℤˣ<VAR>g : G<GOAL>(u, g) ∈ self.toList → g ∈ d.set u
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>w w' : HNNExtension.NormalWord d<VAR>h1 : w.head = w'.head<VAR>h2 : w.toList = w'.toList<GOAL>w = w'
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<GOAL>HNNExtension.NormalWord.empty.toList = []
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<GOAL>HNNExtension.NormalWord.empty.head = 1
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>g : G<GOAL>(HNNExtension.NormalWord.ofGroup g).head = g
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>g : G<GOAL>(HNNExtension.NormalWord.ofGroup g).toList = []
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>g : G<VAR>w : HNNExtension.NormalWord d<GOAL>g • w = { head := g * w.head, toList := w.toList, chain := ⋯, mem_set := ⋯ }
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>g : G<VAR>w : HNNExtension.NormalWord d<GOAL>(g • w).head = g * w.head
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>g : G<VAR>w : HNNExtension.NormalWord d<GOAL>(g • w).toList = w.toList
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>g : G<VAR>u : ℤˣ<VAR>w : HNNExtension.NormalWord d<VAR>h1 : w.head ∈ d.set u<VAR>h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ HNNExtension.toSubgroup A B u → u = u'<GOAL>(HNNExtension.NormalWord.cons g u w h1 h2).toList = (u, w.head) :: w.toList
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>g : G<VAR>u : ℤˣ<VAR>w : HNNExtension.NormalWord d<VAR>h1 : w.head ∈ d.set u<VAR>h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ HNNExtension.toSubgroup A B u → u = u'<GOAL>(HNNExtension.NormalWord.cons g u w h1 h2).head = g
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>motive : HNNExtension.NormalWord d → Sort u_4<VAR>g : G<VAR>ofGroup : (g : G) → motive (HNNExtension.NormalWord.ofGroup g)<VAR>cons : (g : G) → (u : ℤˣ) → (w : HNNExtension.NormalWord d) → (h1 : w.head ∈ d.set u) → (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ HNNExtension.toSubgroup A B u → u = u') → motive w → motive (HNNExtension.NormalWord.cons g u w h1 h2)<GOAL>HNNExtension.NormalWord.consRecOn (HNNExtension.NormalWord.ofGroup g) ofGroup cons = ofGroup g
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>motive : HNNExtension.NormalWord d → Sort u_4<VAR>g : G<VAR>u : ℤˣ<VAR>w : HNNExtension.NormalWord d<VAR>h1 : w.head ∈ d.set u<VAR>h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ HNNExtension.toSubgroup A B u → u = u'<VAR>ofGroup : (g : G) → motive (HNNExtension.NormalWord.ofGroup g)<VAR>cons : (g : G) → (u : ℤˣ) → (w : HNNExtension.NormalWord d) → (h1 : w.head ∈ d.set u) → (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ HNNExtension.toSubgroup A B u → u = u') → motive w → motive (HNNExtension.NormalWord.cons g u w h1 h2)<GOAL>HNNExtension.NormalWord.consRecOn (HNNExtension.NormalWord.cons g u w h1 h2) ofGroup cons = cons g u w h1 h2 (HNNExtension.NormalWord.consRecOn w ofGroup cons)
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>g₁ g₂ : G<VAR>u : ℤˣ<VAR>w : HNNExtension.NormalWord d<VAR>h1 : w.head ∈ d.set u<VAR>h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ HNNExtension.toSubgroup A B u → u = u'<GOAL>g₁ • HNNExtension.NormalWord.cons g₂ u w h1 h2 = HNNExtension.NormalWord.cons (g₁ * g₂) u w h1 h2
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>g₁ g₂ : G<GOAL>g₁ • HNNExtension.NormalWord.ofGroup g₂ = HNNExtension.NormalWord.ofGroup (g₁ * g₂)
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>u : ℤˣ<VAR>g : G<GOAL>(HNNExtension.NormalWord.unitsSMulGroup φ d u g).2 = (⋯.equiv g).2
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>u : ℤˣ<VAR>w : HNNExtension.NormalWord d<VAR>h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ HNNExtension.toSubgroup A B u → u = u'<GOAL>¬HNNExtension.NormalWord.Cancels u w
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>u : ℤˣ<VAR>w : HNNExtension.NormalWord d<GOAL>HNNExtension.NormalWord.Cancels (-u) (HNNExtension.NormalWord.unitsSMul φ u w) ↔ ¬HNNExtension.NormalWord.Cancels u w
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>u : ℤˣ<VAR>w : HNNExtension.NormalWord d<GOAL>HNNExtension.NormalWord.unitsSMul φ (-u) (HNNExtension.NormalWord.unitsSMul φ u w) = w
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>w : HNNExtension.NormalWord d<GOAL>(HNNExtension.NormalWord.unitsSMulEquiv φ) w = HNNExtension.NormalWord.unitsSMul φ 1 w
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>w : HNNExtension.NormalWord d<GOAL>(HNNExtension.NormalWord.unitsSMulEquiv φ).symm w = HNNExtension.NormalWord.unitsSMul φ (-1) w
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>g : ↥A<VAR>w : HNNExtension.NormalWord d<GOAL>HNNExtension.NormalWord.unitsSMul φ 1 (↑g • w) = ↑(φ g) • HNNExtension.NormalWord.unitsSMul φ 1 w
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>g : G<VAR>w : HNNExtension.NormalWord d<GOAL>HNNExtension.NormalWord.ReducedWord.prod φ (g • w).toReducedWord = HNNExtension.of g * HNNExtension.NormalWord.ReducedWord.prod φ w.toReducedWord
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>g : G<VAR>w : HNNExtension.NormalWord d<GOAL>HNNExtension.of g • w = g • w
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>w : HNNExtension.NormalWord d<GOAL>HNNExtension.t • w = HNNExtension.NormalWord.unitsSMul φ 1 w
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>u : ℤˣ<VAR>w : HNNExtension.NormalWord d<GOAL>HNNExtension.t ^ ↑u • w = HNNExtension.NormalWord.unitsSMul φ u w
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>g : G<VAR>u : ℤˣ<VAR>w : HNNExtension.NormalWord d<VAR>h1 : w.head ∈ d.set u<VAR>h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ HNNExtension.toSubgroup A B u → u = u'<GOAL>HNNExtension.NormalWord.ReducedWord.prod φ (HNNExtension.NormalWord.cons g u w h1 h2).toReducedWord = HNNExtension.of g * (HNNExtension.t ^ ↑u * HNNExtension.NormalWord.ReducedWord.prod φ w.toReducedWord)
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>u : ℤˣ<VAR>w : HNNExtension.NormalWord d<GOAL>HNNExtension.NormalWord.ReducedWord.prod φ (HNNExtension.NormalWord.unitsSMul φ u w).toReducedWord = HNNExtension.t ^ ↑u * HNNExtension.NormalWord.ReducedWord.prod φ w.toReducedWord
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<GOAL>HNNExtension.NormalWord.ReducedWord.prod φ HNNExtension.NormalWord.empty.toReducedWord = 1
<VAR>G : Type u_1<VAR>Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>d : HNNExtension.NormalWord.TransversalPair G A B<VAR>g : HNNExtension G A B φ<VAR>w : HNNExtension.NormalWord d<GOAL>HNNExtension.NormalWord.ReducedWord.prod φ (g • w).toReducedWord = g * HNNExtension.NormalWord.ReducedWord.prod φ w.toReducedWord