ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>G : Type u_4<VAR>Group G<VAR>H : ι → Type u_5<VAR>(i : ι) → Group (H i)<VAR>f : (i : ι) → H i →* G<VAR>α : Type u_6<VAR>MulAction G α<VAR>X : ι → Set α<VAR>hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i<VAR>i j k : ι<VAR>w : Monoid.CoprodI.NeWord H i j<VAR>hk : j ≠ k<GOAL>(Monoid.CoprodI.lift f) w.prod • X k ⊆ X i
<VAR>ι : Type u_1<VAR>G : Type u_4<VAR>Group G<VAR>H : ι → Type u_5<VAR>(i : ι) → Group (H i)<VAR>f : (i : ι) → H i →* G<VAR>α : Type u_6<VAR>MulAction G α<VAR>X : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i<VAR>i j k : ι<VAR>w : Monoid.CoprodI.NeWord H i j<VAR>hhead : k ≠ i<VAR>hlast : k ≠ j<GOAL>(Monoid.CoprodI.lift f) w.prod ≠ 1
<VAR>ι : Type u_1<VAR>hnontriv : Nontrivial ι<VAR>G : Type u_4<VAR>Group G<VAR>H : ι → Type u_5<VAR>(i : ι) → Group (H i)<VAR>f : (i : ι) → H i →* G<VAR>α : Type u_6<VAR>MulAction G α<VAR>X : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i<VAR>i : ι<VAR>w : Monoid.CoprodI.NeWord H i i<GOAL>(Monoid.CoprodI.lift f) w.prod ≠ 1
<VAR>ι : Type u_1<VAR>hnontriv : Nontrivial ι<VAR>G : Type u_4<VAR>Group G<VAR>H : ι → Type u_5<VAR>(i : ι) → Group (H i)<VAR>f : (i : ι) → H i →* G<VAR>α : Type u_6<VAR>MulAction G α<VAR>X : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i<VAR>i j : ι<VAR>w : Monoid.CoprodI.NeWord H i j<VAR>hcard : 3 ≤ Cardinal.mk (H i)<VAR>hheadtail : i ≠ j<GOAL>(Monoid.CoprodI.lift f) w.prod ≠ 1
<VAR>ι : Type u_1<VAR>hnontriv : Nontrivial ι<VAR>G : Type u_4<VAR>Group G<VAR>H : ι → Type u_5<VAR>(i : ι) → Group (H i)<VAR>f : (i : ι) → H i →* G<VAR>hcard : 3 ≤ Cardinal.mk ι ∨ ∃ i, 3 ≤ Cardinal.mk (H i)<VAR>α : Type u_6<VAR>MulAction G α<VAR>X : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i<VAR>i j : ι<VAR>w : Monoid.CoprodI.NeWord H i j<GOAL>(Monoid.CoprodI.lift f) w.prod ≠ 1
<VAR>ι : Type u_1<VAR>hnontriv : Nontrivial ι<VAR>G : Type u_4<VAR>Group G<VAR>H : ι → Type u_5<VAR>(i : ι) → Group (H i)<VAR>f : (i : ι) → H i →* G<VAR>hcard : 3 ≤ Cardinal.mk ι ∨ ∃ i, 3 ≤ Cardinal.mk (H i)<VAR>α : Type u_6<VAR>MulAction G α<VAR>X : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i<VAR>w : Monoid.CoprodI.Word H<VAR>h : (Monoid.CoprodI.lift f) w.prod = 1<GOAL>w = Monoid.CoprodI.Word.empty
<VAR>ι : Type u_1<VAR>hnontriv : Nontrivial ι<VAR>G : Type u_4<VAR>Group G<VAR>H : ι → Type u_5<VAR>(i : ι) → Group (H i)<VAR>f : (i : ι) → H i →* G<VAR>hcard : 3 ≤ Cardinal.mk ι ∨ ∃ i, 3 ≤ Cardinal.mk (H i)<VAR>α : Type u_6<VAR>MulAction G α<VAR>X : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hpp : Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i<GOAL>Function.Injective ⇑(Monoid.CoprodI.lift f)
<VAR>ι : Type u_1<VAR>a : FreeGroup ι<GOAL>freeGroupEquivCoprodI a = (FreeGroup.lift fun i => Monoid.CoprodI.of (FreeGroup.of ())) a
<VAR>ι : Type u_1<VAR>a : Monoid.CoprodI fun x => FreeGroup Unit<GOAL>freeGroupEquivCoprodI.symm a = (Monoid.CoprodI.lift fun i => FreeGroup.lift fun x => FreeGroup.of i) a
<VAR>ι : Type u_1<VAR>Nontrivial ι<VAR>G : Type u_1<VAR>Group G<VAR>a : ι → G<VAR>α : Type u_4<VAR>MulAction G α<VAR>X Y : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)<VAR>hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)<VAR>hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i<VAR>hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i<GOAL>Function.Injective ⇑(FreeGroup.lift a)
<VAR>α : Type u<VAR>DecidableEq α<VAR>Fintype α<VAR>σ τ : Equiv.Perm α<VAR>f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }<VAR>hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)<GOAL>IsConj σ τ
<VAR>α : Type u<VAR>s : Finset α<VAR>f : Equiv.Perm α<VAR>h : ∀ x ∈ s, f x ∈ s<VAR>y : α<VAR>hy : y ∈ s<GOAL>f⁻¹ y ∈ s
<VAR>α : Type u<VAR>f : Equiv.Perm α<VAR>s : Set α<VAR>Finite ↑s<VAR>h : Set.MapsTo (⇑f) s s<GOAL>Set.MapsTo (⇑f⁻¹) s s
<VAR>α : Type u<VAR>f : Equiv.Perm α<VAR>s : Set α<VAR>Finite ↑s<GOAL>Set.MapsTo (⇑f⁻¹) s s ↔ Set.MapsTo (⇑f) s s
<VAR>α : Type u<VAR>f : Equiv.Perm α<VAR>p : α → Prop<VAR>Finite { x // p x }<VAR>h : ∀ (x : α), p x → p (f x)<VAR>x : α<VAR>hx : p x<GOAL>p (f⁻¹ x)
<VAR>α : Type u<VAR>f : Equiv.Perm α<VAR>p : α → Prop<VAR>Finite { x // p x }<VAR>h : ∀ (x : α), p x → p (f x)<VAR>x : { x // p x }<GOAL>(f.subtypePermOfFintype h) x = ⟨f ↑x, ⋯⟩
<VAR>α : Type u<VAR>p : α → Prop<VAR>Finite { x // p x }<VAR>h : ∀ (x : α), p x → p (1 x)<GOAL>Equiv.Perm.subtypePermOfFintype 1 h = 1
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>Finite m<VAR>Finite n<VAR>σ : Equiv.Perm (m ⊕ n)<GOAL>Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl) ↔ Set.MapsTo (⇑σ) (Set.range Sum.inr) (Set.range Sum.inr)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>Finite m<VAR>Finite n<VAR>σ : Equiv.Perm (m ⊕ n)<VAR>h : Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)<GOAL>σ ∈ (Equiv.Perm.sumCongrHom m n).range
<VAR>α : Type u<VAR>σ τ : Equiv.Perm α<VAR>hστ : σ.Disjoint τ<GOAL>orderOf (σ * τ) = (orderOf σ).lcm (orderOf τ)
<VAR>α : Type u<VAR>β : Type v<VAR>p : β → Prop<VAR>DecidablePred p<VAR>f : α ≃ Subtype p<VAR>σ τ : Equiv.Perm α<VAR>h : σ.Disjoint τ<GOAL>(σ.extendDomain f).Disjoint (τ.extendDomain f)
<VAR>α : Type u<VAR>Finite α<VAR>σ τ π ρ : Equiv.Perm α<VAR>hc1 : IsConj σ π<VAR>hc2 : IsConj τ ρ<VAR>hd1 : σ.Disjoint τ<VAR>hd2 : π.Disjoint ρ<GOAL>IsConj (σ * τ) (π * ρ)
<VAR>α : Type u<VAR>DecidableEq α<VAR>Fintype α<VAR>σ : Equiv.Perm α<VAR>n : ℕ<VAR>h : n.Coprime (orderOf σ)<GOAL>(σ ^ n).support = σ.support
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>f : ((a : α) → Part (β a)) → (a : α) → Part (β a)<VAR>x : α<VAR>h' : ∃ i, (Part.Fix.approx f i x).Dom<GOAL>Part.fix f x = Part.Fix.approx f (Nat.find h').succ x
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>f : ((a : α) → Part (β a)) → (a : α) → Part (β a)<VAR>x : α<VAR>h' : ¬∃ i, (Part.Fix.approx f i x).Dom<GOAL>Part.fix f x = Part.none
<VAR>m : Type u → Type v<VAR>Monad m<VAR>MonadCont m<VAR>self : LawfulMonadCont m<VAR>α ω γ : Type u<VAR>cmd : m α<VAR>next : ContT.Label ω m γ → α → m ω<GOAL>(MonadCont.callCC fun f => cmd >>= next f) = do let x ← cmd MonadCont.callCC fun f => next f x
<VAR>m : Type u → Type v<VAR>Monad m<VAR>MonadCont m<VAR>self : LawfulMonadCont m<VAR>α β : Type u<VAR>dummy : m α<GOAL>(MonadCont.callCC fun x => dummy) = dummy
<VAR>m : Type u → Type v<VAR>Monad m<VAR>MonadCont m<VAR>self : LawfulMonadCont m<VAR>α : Type u<VAR>β : Type u<VAR>x : α<VAR>dead : ContT.Label α m β → β → m α<GOAL>(MonadCont.callCC fun f => ContT.goto f x >>= dead f) = pure x
<VAR>r : Type u<VAR>m : Type u → Type v<VAR>α : Type w<VAR>f : m r → m r<VAR>x : ContT r m α<GOAL>(ContT.map f x).run = f ∘ x.run
<VAR>r : Type u<VAR>m : Type u → Type v<VAR>α β : Type w<VAR>f : (β → m r) → α → m r<VAR>x : ContT r m α<GOAL>(ContT.withContT f x).run = x.run ∘ f
<VAR>r : Type u<VAR>m : Type u → Type v<VAR>α : Type w<VAR>x y : ContT r m α<VAR>h : ∀ (f : α → m r), x.run f = y.run f<GOAL>x = y
<VAR>r : Type u<VAR>m : Type u → Type v<VAR>Monad m<VAR>LawfulMonad m<VAR>α β : Type u<VAR>x : m α<VAR>f : α → m β<GOAL>ContT.monadLift (x >>= f) = ContT.monadLift x >>= ContT.monadLift ∘ f
<VAR>m : Type u → Type v<VAR>Monad m<VAR>α β ε : Type u<VAR>x : ContT.Label (Except ε α) m β<VAR>i : α<GOAL>ContT.goto (ExceptT.mkLabel x) i = ExceptT.mk (Except.ok <$> ContT.goto x (Except.ok i))
<VAR>m : Type u → Type v<VAR>Monad m<VAR>α β : Type u<VAR>x : ContT.Label (Option α) m β<VAR>i : α<GOAL>ContT.goto (OptionT.mkLabel x) i = OptionT.mk do let a ← ContT.goto x (some i) pure (some a)
<VAR>m : Type u → Type v<VAR>Monad m<VAR>α : Type u_1<VAR>β ω : Type u<VAR>EmptyCollection ω<VAR>x : ContT.Label (α × ω) m β<VAR>i : α<GOAL>ContT.goto (WriterT.mkLabel x) i = monadLift (ContT.goto x (i, ∅))
<VAR>m : Type u → Type v<VAR>Monad m<VAR>α : Type u_1<VAR>β ω : Type u<VAR>Monoid ω<VAR>x : ContT.Label (α × ω) m β<VAR>i : α<GOAL>ContT.goto (WriterT.mkLabel' x) i = monadLift (ContT.goto x (i, 1))
<VAR>m : Type u → Type v<VAR>α β σ : Type u<VAR>x : ContT.Label (α × σ) m (β × σ)<VAR>i : α<GOAL>ContT.goto (StateT.mkLabel x) i = StateT.mk fun s => ContT.goto x (i, s)
<VAR>m : Type u → Type v<VAR>α : Type u_1<VAR>ρ β : Type u<VAR>x : ContT.Label α m β<VAR>i : α<GOAL>ContT.goto (ReaderT.mkLabel ρ x) i = monadLift (ContT.goto x i)
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>A : Type u_2<VAR>CommGroup A<VAR>ϕ : ↥H →* A<VAR>R S T : ↑(Subgroup.leftTransversals ↑H)<VAR>H.FiniteIndex<GOAL>Subgroup.leftTransversals.diff ϕ R S * Subgroup.leftTransversals.diff ϕ S T = Subgroup.leftTransversals.diff ϕ R T
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>A : Type u_2<VAR>AddCommGroup A<VAR>ϕ : ↥H →+ A<VAR>R S T : ↑(AddSubgroup.leftTransversals ↑H)<VAR>H.FiniteIndex<GOAL>AddSubgroup.leftTransversals.diff ϕ R S + AddSubgroup.leftTransversals.diff ϕ S T = AddSubgroup.leftTransversals.diff ϕ R T
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>A : Type u_2<VAR>AddCommGroup A<VAR>ϕ : ↥H →+ A<VAR>T : ↑(AddSubgroup.leftTransversals ↑H)<VAR>H.FiniteIndex<GOAL>AddSubgroup.leftTransversals.diff ϕ T T = 0
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>A : Type u_2<VAR>CommGroup A<VAR>ϕ : ↥H →* A<VAR>T : ↑(Subgroup.leftTransversals ↑H)<VAR>H.FiniteIndex<GOAL>Subgroup.leftTransversals.diff ϕ T T = 1
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>A : Type u_2<VAR>CommGroup A<VAR>ϕ : ↥H →* A<VAR>S T : ↑(Subgroup.leftTransversals ↑H)<VAR>H.FiniteIndex<GOAL>(Subgroup.leftTransversals.diff ϕ S T)⁻¹ = Subgroup.leftTransversals.diff ϕ T S
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>A : Type u_2<VAR>AddCommGroup A<VAR>ϕ : ↥H →+ A<VAR>S T : ↑(AddSubgroup.leftTransversals ↑H)<VAR>H.FiniteIndex<GOAL>-AddSubgroup.leftTransversals.diff ϕ S T = AddSubgroup.leftTransversals.diff ϕ T S
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>A : Type u_2<VAR>CommGroup A<VAR>ϕ : ↥H →* A<VAR>S T : ↑(Subgroup.leftTransversals ↑H)<VAR>H.FiniteIndex<VAR>g : G<GOAL>Subgroup.leftTransversals.diff ϕ (g • S) (g • T) = Subgroup.leftTransversals.diff ϕ S T
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>A : Type u_2<VAR>AddCommGroup A<VAR>ϕ : ↥H →+ A<VAR>S T : ↑(AddSubgroup.leftTransversals ↑H)<VAR>H.FiniteIndex<VAR>g : G<GOAL>AddSubgroup.leftTransversals.diff ϕ (g +ᵥ S) (g +ᵥ T) = AddSubgroup.leftTransversals.diff ϕ S T
<VAR>G : Type u_1<VAR>AddGroup G<VAR>H : AddSubgroup G<VAR>A : Type u_2<VAR>AddCommGroup A<VAR>ϕ : ↥H →+ A<VAR>T : ↑(AddSubgroup.leftTransversals ↑H)<VAR>H.FiniteIndex<VAR>g : G<GOAL>ϕ.transfer g = AddSubgroup.leftTransversals.diff ϕ T (g +ᵥ T)
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>A : Type u_2<VAR>CommGroup A<VAR>ϕ : ↥H →* A<VAR>T : ↑(Subgroup.leftTransversals ↑H)<VAR>H.FiniteIndex<VAR>g : G<GOAL>ϕ.transfer g = Subgroup.leftTransversals.diff ϕ T (g • T)
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>A : Type u_2<VAR>CommGroup A<VAR>ϕ : ↥H →* A<VAR>H.FiniteIndex<VAR>g : G<VAR>Fintype (Quotient (MulAction.orbitRel (↥(Subgroup.zpowers g)) (G ⧸ H)))<GOAL>ϕ.transfer g = ∏ q : Quotient (MulAction.orbitRel (↥(Subgroup.zpowers g)) (G ⧸ H)), ϕ ⟨(Quotient.out' q.out')⁻¹ * g ^ Function.minimalPeriod (fun x => g • x) q.out' * Quotient.out' q.out', ⋯⟩
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>g : G<VAR>key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k<GOAL>g ^ H.index ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>A : Type u_2<VAR>CommGroup A<VAR>ϕ : ↥H →* A<VAR>H.FiniteIndex<VAR>g : G<VAR>key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k<GOAL>ϕ.transfer g = ϕ ⟨g ^ H.index, ⋯⟩
<VAR>G : Type u_1<VAR>Group G<VAR>(Subgroup.center G).FiniteIndex<VAR>g : G<GOAL>(MonoidHom.id ↥(Subgroup.center G)).transfer g = ⟨g ^ (Subgroup.center G).index, ⋯⟩
<VAR>G : Type u_1<VAR>Group G<VAR>(Subgroup.center G).FiniteIndex<VAR>g : G<GOAL>↑((MonoidHom.transferCenterPow G) g) = g ^ (Subgroup.center G).index
<VAR>G : Type u_1<VAR>Group G<VAR>p : ℕ<VAR>P : Sylow p G<VAR>hP : (↑P).normalizer ≤ Subgroup.centralizer ↑P<VAR>Fact (Nat.Prime p)<VAR>Finite (Sylow p G)<VAR>g : G<VAR>hg : g ∈ P<VAR>k : ℕ<VAR>g₀ : G<VAR>h : g₀⁻¹ * g ^ k * g₀ ∈ P<GOAL>g₀⁻¹ * g ^ k * g₀ = g ^ k
<VAR>G : Type u_1<VAR>Group G<VAR>p : ℕ<VAR>P : Sylow p G<VAR>hP : (↑P).normalizer ≤ Subgroup.centralizer ↑P<VAR>Fact (Nat.Prime p)<VAR>Finite (Sylow p G)<VAR>(↑P).FiniteIndex<VAR>g : G<VAR>hg : g ∈ P<GOAL>(MonoidHom.transferSylow P hP) g = ⟨g ^ (↑P).index, ⋯⟩
<VAR>G : Type u_1<VAR>Group G<VAR>p : ℕ<VAR>P : Sylow p G<VAR>hP : (↑P).normalizer ≤ Subgroup.centralizer ↑P<VAR>Fact (Nat.Prime p)<VAR>Finite (Sylow p G)<VAR>(↑P).FiniteIndex<GOAL>⇑((MonoidHom.transferSylow P hP).restrict ↑P) = fun x => x ^ (↑P).index
<VAR>G : Type u_1<VAR>Group G<VAR>p : ℕ<VAR>P : Sylow p G<VAR>hP : (↑P).normalizer ≤ Subgroup.centralizer ↑P<VAR>Fact (Nat.Prime p)<VAR>Finite (Sylow p G)<VAR>(↑P).FiniteIndex<GOAL>(MonoidHom.transferSylow P hP).ker.IsComplement' ↑P
<VAR>G : Type u_1<VAR>Group G<VAR>p : ℕ<VAR>P : Sylow p G<VAR>hP : (↑P).normalizer ≤ Subgroup.centralizer ↑P<VAR>Fact (Nat.Prime p)<VAR>Finite (Sylow p G)<VAR>(↑P).FiniteIndex<GOAL>¬p ∣ Nat.card ↥(MonoidHom.transferSylow P hP).ker
<VAR>G : Type u_1<VAR>Group G<VAR>p : ℕ<VAR>P : Sylow p G<VAR>hP : (↑P).normalizer ≤ Subgroup.centralizer ↑P<VAR>Fact (Nat.Prime p)<VAR>Finite (Sylow p G)<VAR>(↑P).FiniteIndex<VAR>Q : Subgroup G<VAR>hQ : IsPGroup p ↥Q<GOAL>Disjoint (MonoidHom.transferSylow P hP).ker Q
<VAR>F : Type u → Type v<VAR>α : Type u<VAR>Functor F<VAR>LawfulFunctor F<GOAL>(fun x => id <$> x) = id
<VAR>F : Type u → Type v<VAR>α β γ : Type u<VAR>Functor F<VAR>LawfulFunctor F<VAR>f : α → β<VAR>g : β → γ<GOAL>((fun x => g <$> x) ∘ fun x => f <$> x) = fun x => (g ∘ f) <$> x
<VAR>F : Type u_1 → Type u_2<VAR>F1 F2 : Functor F<VAR>LawfulFunctor F<VAR>LawfulFunctor F<GOAL>(∀ (α β : Type u_1) (f : α → β) (x : F α), f <$> x = f <$> x) → F1 = F2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x y : Functor.Const α β<VAR>h : x.run = y.run<GOAL>x = y
<VAR>F : Type u → Type w<VAR>G : Type v → Type u<VAR>α : Type v<VAR>x y : Functor.Comp F G α<GOAL>x.run = y.run → x = y
<VAR>F : Type u → Type w<VAR>G : Type v → Type u<VAR>Functor F<VAR>Functor G<VAR>α β : Type v<VAR>h : α → β<VAR>x : F (G α)<GOAL>h <$> Functor.Comp.mk x = Functor.Comp.mk ((fun x => h <$> x) <$> x)
<VAR>F : Type u → Type w<VAR>G : Type v → Type u<VAR>Functor F<VAR>Functor G<VAR>α β : Type v<VAR>h : α → β<VAR>x : Functor.Comp F G α<GOAL>(h <$> x).run = (fun x => h <$> x) <$> x.run
<VAR>F : Type u → Type w<VAR>G : Type v → Type u<VAR>Functor F<VAR>Functor G<VAR>LawfulFunctor F<VAR>LawfulFunctor G<VAR>α : Type v<VAR>x : Functor.Comp F G α<GOAL>Functor.Comp.map id x = x
<VAR>F : Type u → Type w<VAR>G : Type v → Type u<VAR>Functor F<VAR>Functor G<VAR>LawfulFunctor F<VAR>LawfulFunctor G<VAR>α β γ : Type v<VAR>g' : α → β<VAR>h : β → γ<VAR>x : Functor.Comp F G α<GOAL>Functor.Comp.map (h ∘ g') x = Functor.Comp.map h (Functor.Comp.map g' x)
<VAR>F : Type u_1 → Type u_2<VAR>AF : Functor F<VAR>LawfulFunctor F<GOAL>Functor.Comp.functor = AF
<VAR>F : Type u → Type w<VAR>G : Type v → Type u<VAR>Applicative F<VAR>Applicative G<VAR>α : Type v<VAR>x : α<GOAL>(pure x).run = pure (pure x)
<VAR>F : Type u → Type w<VAR>G : Type v → Type u<VAR>Applicative F<VAR>Applicative G<VAR>α β : Type v<VAR>f : Functor.Comp F G (α → β)<VAR>x : Functor.Comp F G α<GOAL>(Seq.seq f fun x_1 => x).run = Seq.seq ((fun x x_1 => Seq.seq x fun x => x_1) <$> f.run) fun x_1 => x.run
<VAR>F : Type u → Type u<VAR>Functor F<VAR>α : Type u<VAR>x : F α<VAR>p : α → Prop<VAR>h : Functor.Liftp p x<VAR>y : α<GOAL>y ∈ Functor.supp x → p y
<VAR>σ : Type u<VAR>m : Type u → Type v<VAR>α : Type u<VAR>f : σ → m (α × σ)<VAR>st : σ<GOAL>(StateT.mk f).run st = f st
<VAR>α ε : Type u<VAR>m : Type u → Type v<VAR>x : m (Except ε α)<GOAL>(ExceptT.mk x).run = x
<VAR>α ε : Type u<VAR>m : Type u → Type v<VAR>Monad m<VAR>n : Type u → Type u_1<VAR>MonadLiftT n m<VAR>x : n α<GOAL>(monadLift x).run = Except.ok <$> monadLift x
<VAR>α ε : Type u<VAR>m : Type u → Type v<VAR>x : ExceptT ε m α<VAR>n : Type u → Type u_1<VAR>MonadFunctorT n m<VAR>f : {α : Type u} → n α → n α<GOAL>(monadMap f x).run = monadMap f x.run
<VAR>m : Type u → Type v<VAR>α σ : Type u<VAR>f : σ → m α<VAR>r : σ<GOAL>(ReaderT.mk f).run r = f r
<VAR>α : Type u<VAR>m : Type u → Type v<VAR>x x' : OptionT m α<VAR>h : x.run = x'.run<GOAL>x = x'
<VAR>α : Type u<VAR>m : Type u → Type v<VAR>x : m (Option α)<GOAL>(OptionT.mk x).run = x
<VAR>α : Type u<VAR>m : Type u → Type v<VAR>Monad m<VAR>a : α<GOAL>(pure a).run = pure (some a)
<VAR>α β : Type u<VAR>m : Type u → Type v<VAR>x : OptionT m α<VAR>Monad m<VAR>f : α → OptionT m β<GOAL>(x >>= f).run = do let x ← x.run match x with | some a => (f a).run | none => pure none
<VAR>α β : Type u<VAR>m : Type u → Type v<VAR>x : OptionT m α<VAR>Monad m<VAR>f : α → β<VAR>LawfulMonad m<GOAL>(f <$> x).run = Option.map f <$> x.run
<VAR>α : Type u<VAR>m : Type u → Type v<VAR>Monad m<VAR>n : Type u → Type u_1<VAR>MonadLiftT n m<VAR>x : n α<GOAL>(monadLift x).run = do let a ← monadLift x pure (some a)
<VAR>α : Type u<VAR>m : Type u → Type v<VAR>x : OptionT m α<VAR>n : Type u → Type u_1<VAR>MonadFunctorT n m<VAR>f : {α : Type u} → n α → n α<GOAL>(monadMap f x).run = monadMap f x.run
<VAR>F : Type u → Type v<VAR>Applicative F<VAR>G : Type u → Type w<VAR>Applicative G<VAR>self : ApplicativeTransformation F G<VAR>α β : Type u<VAR>x : F (α → β)<VAR>y : F α<GOAL>self.app β (Seq.seq x fun x => y) = Seq.seq (self.app (α → β) x) fun x => self.app α y
<VAR>F : Type u → Type v<VAR>Applicative F<VAR>G : Type u → Type w<VAR>Applicative G<VAR>self : ApplicativeTransformation F G<VAR>α : Type u<VAR>x : α<GOAL>self.app α (pure x) = pure x
<VAR>F : Type u → Type v<VAR>Applicative F<VAR>G : Type u → Type w<VAR>Applicative G<VAR>η : ApplicativeTransformation F G<GOAL>η.app = fun {α} => η.app α
<VAR>F : Type u → Type v<VAR>Applicative F<VAR>G : Type u → Type w<VAR>Applicative G<VAR>f : (α : Type u) → F α → G α<VAR>pp : ∀ {α : Type u} (x : α), f α (pure x) = pure x<VAR>ps : ∀ {α β : Type u} (x : F (α → β)) (y : F α), f β (Seq.seq x fun x => y) = Seq.seq (f (α → β) x) fun x => f α y<GOAL>(fun {α} => { app := f, preserves_pure' := pp, preserves_seq' := ps }.app α) = f
<VAR>F : Type u → Type v<VAR>Applicative F<VAR>G : Type u → Type w<VAR>Applicative G<VAR>η η' : ApplicativeTransformation F G<VAR>h : η = η'<VAR>α : Type u<VAR>x : F α<GOAL>(fun {α} => η.app α) x = (fun {α} => η'.app α) x
<VAR>F : Type u → Type v<VAR>Applicative F<VAR>G : Type u → Type w<VAR>Applicative G<VAR>η : ApplicativeTransformation F G<VAR>α : Type u<VAR>x y : F α<VAR>h : x = y<GOAL>(fun {α} => η.app α) x = (fun {α} => η.app α) y
<VAR>F : Type u → Type v<VAR>Applicative F<VAR>G : Type u → Type w<VAR>Applicative G<VAR>η η' : ApplicativeTransformation F G<VAR>h : (fun {α} => η.app α) = fun {α} => η'.app α<GOAL>η = η'
<VAR>F : Type u → Type v<VAR>Applicative F<VAR>G : Type u → Type w<VAR>Applicative G<VAR>η η' : ApplicativeTransformation F G<VAR>h : ∀ (α : Type u) (x : F α), (fun {α} => η.app α) x = (fun {α} => η'.app α) x<GOAL>η = η'
<VAR>F : Type u → Type v<VAR>Applicative F<VAR>G : Type u → Type w<VAR>Applicative G<VAR>η η' : ApplicativeTransformation F G<GOAL>η = η' ↔ ∀ (α : Type u) (x : F α), (fun {α} => η.app α) x = (fun {α} => η'.app α) x
<VAR>F : Type u → Type v<VAR>Applicative F<VAR>G : Type u → Type w<VAR>Applicative G<VAR>η : ApplicativeTransformation F G<VAR>α : Type u<VAR>x : α<GOAL>(fun {α} => η.app α) (pure x) = pure x
<VAR>F : Type u → Type v<VAR>Applicative F<VAR>G : Type u → Type w<VAR>Applicative G<VAR>η : ApplicativeTransformation F G<VAR>α β : Type u<VAR>x : F (α → β)<VAR>y : F α<GOAL>(fun {α} => η.app α) (Seq.seq x fun x => y) = Seq.seq ((fun {α} => η.app α) x) fun x => (fun {α} => η.app α) y
<VAR>F : Type u → Type v<VAR>Applicative F<VAR>LawfulApplicative F<VAR>G : Type u → Type w<VAR>Applicative G<VAR>LawfulApplicative G<VAR>η : ApplicativeTransformation F G<VAR>α β : Type u<VAR>x : α → β<VAR>y : F α<GOAL>(fun {α} => η.app α) (x <$> y) = x <$> (fun {α} => η.app α) y
<VAR>F : Type u → Type v<VAR>Applicative F<VAR>LawfulApplicative F<VAR>G : Type u → Type w<VAR>Applicative G<VAR>LawfulApplicative G<VAR>η : ApplicativeTransformation F G<VAR>α β : Type u<VAR>x : α → β<GOAL>(fun {α} => η.app α) ∘ Functor.map x = Functor.map x ∘ fun {α} => η.app α
<VAR>F : Type u → Type v<VAR>Applicative F<VAR>G : Type u → Type w<VAR>Applicative G<VAR>H : Type u → Type s<VAR>Applicative H<VAR>η' : ApplicativeTransformation G H<VAR>η : ApplicativeTransformation F G<VAR>α : Type u<VAR>x : F α<GOAL>(fun {α} => (η'.comp η).app α) x = (fun {α} => η'.app α) ((fun {α} => η.app α) x)
<VAR>F : Type u → Type v<VAR>Applicative F<VAR>G : Type u → Type w<VAR>Applicative G<VAR>H : Type u → Type s<VAR>Applicative H<VAR>I : Type u → Type t<VAR>Applicative I<VAR>η'' : ApplicativeTransformation H I<VAR>η' : ApplicativeTransformation G H<VAR>η : ApplicativeTransformation F G<GOAL>(η''.comp η').comp η = η''.comp (η'.comp η)
<VAR>F : Type u → Type v<VAR>Applicative F<VAR>G : Type u → Type w<VAR>Applicative G<VAR>η : ApplicativeTransformation F G<GOAL>η.comp ApplicativeTransformation.idTransformation = η
<VAR>F : Type u → Type v<VAR>Applicative F<VAR>G : Type u → Type w<VAR>Applicative G<VAR>η : ApplicativeTransformation F G<GOAL>ApplicativeTransformation.idTransformation.comp η = η
<VAR>t : Type u → Type u<VAR>Traversable t<VAR>self : LawfulTraversable t<VAR>α β : Type u<VAR>f : α → β<VAR>x : t α<GOAL>traverse (pure ∘ f) x = id.mk (f <$> x)
<VAR>t : Type u → Type u<VAR>Traversable t<VAR>self : LawfulTraversable t<VAR>α : Type u<VAR>x : t α<GOAL>traverse pure x = x
<VAR>t : Type u → Type u<VAR>Traversable t<VAR>self : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>Applicative F<VAR>Applicative G<VAR>LawfulApplicative F<VAR>LawfulApplicative G<VAR>η : ApplicativeTransformation F G<VAR>α β : Type u<VAR>f : α → F β<VAR>x : t α<GOAL>(fun {α} => η.app α) (traverse f x) = traverse ((fun {α} => η.app α) ∘ f) x
<VAR>t : Type u → Type u<VAR>Traversable t<VAR>self : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>Applicative F<VAR>Applicative G<VAR>LawfulApplicative F<VAR>LawfulApplicative G<VAR>α β γ : Type u<VAR>f : β → F γ<VAR>g : α → G β<VAR>x : t α<GOAL>traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (traverse f <$> traverse g x)
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>H.IsCommutative<VAR>H.FiniteIndex<VAR>α β : ↑(Subgroup.leftTransversals ↑H)<VAR>hH : H.Normal<VAR>g : Gᵐᵒᵖ<GOAL>Subgroup.leftTransversals.diff (MonoidHom.id ↥H) (g • α) (g • β) = ⟨(MulOpposite.unop g)⁻¹ * ↑(Subgroup.leftTransversals.diff (MonoidHom.id ↥H) α β) * MulOpposite.unop g, ⋯⟩
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>H.IsCommutative<VAR>H.FiniteIndex<VAR>α β : ↑(Subgroup.leftTransversals ↑H)<VAR>H.Normal<VAR>h : ↥H<GOAL>Subgroup.leftTransversals.diff (MonoidHom.id ↥H) α (MulOpposite.op ↑h • β) = Subgroup.leftTransversals.diff (MonoidHom.id ↥H) α β * h ^ H.index
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>H.IsCommutative<VAR>H.FiniteIndex<VAR>H.Normal<VAR>hH : (Nat.card ↥H).Coprime H.index<VAR>α : H.QuotientDiff<VAR>h : ↥H<GOAL>h • α = α → h = 1
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>H.IsCommutative<VAR>H.FiniteIndex<VAR>H.Normal<VAR>hH : (Nat.card ↥H).Coprime H.index<VAR>α β : H.QuotientDiff<GOAL>∃ h, h • α = β
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>H.IsCommutative<VAR>H.FiniteIndex<VAR>H.Normal<VAR>α : H.QuotientDiff<VAR>hH : (Nat.card ↥H).Coprime H.index<GOAL>H.IsComplement' (MulAction.stabilizer G α)
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>H.IsCommutative<VAR>H.FiniteIndex<VAR>H.Normal<VAR>hH : (Nat.card ↥H).Coprime H.index<GOAL>∃ K, H.IsComplement' K