ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_2<VAR>Group G<VAR>n : ℕ<VAR>v : ↑(Equiv.Perm.vectorsProdEqOne G n)<VAR>j k : ℕ<GOAL>Equiv.Perm.VectorsProdEqOne.rotate (Equiv.Perm.VectorsProdEqOne.rotate v j) k = Equiv.Perm.VectorsProdEqOne.rotate v (j + k)
<VAR>G : Type u_2<VAR>Group G<VAR>n : ℕ<VAR>v : ↑(Equiv.Perm.vectorsProdEqOne G n)<GOAL>Equiv.Perm.VectorsProdEqOne.rotate v n = v
<VAR>G : Type u_3<VAR>Group G<VAR>Fintype G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hdvd : p ∣ Fintype.card G<GOAL>∃ x, orderOf x = p
<VAR>G : Type u_3<VAR>AddGroup G<VAR>Fintype G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hdvd : p ∣ Fintype.card G<GOAL>∃ x, addOrderOf x = p
<VAR>G : Type u_3<VAR>Group G<VAR>Finite G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hdvd : p ∣ Nat.card G<GOAL>∃ x, orderOf x = p
<VAR>G : Type u_3<VAR>AddGroup G<VAR>Finite G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hdvd : p ∣ Nat.card G<GOAL>∃ x, addOrderOf x = p
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>H : Subgroup (Equiv.Perm α)<VAR>d : DecidablePred fun x => x ∈ H<VAR>τ : Equiv.Perm α<VAR>h0 : Nat.Prime (Fintype.card α)<VAR>h1 : Fintype.card α ∣ Fintype.card ↥H<VAR>h2 : τ ∈ H<VAR>h3 : τ.IsSwap<GOAL>H = ⊤
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ : Equiv.Perm α<GOAL>σ.partition.parts = σ.cycleType + Multiset.replicate (Fintype.card α - σ.support.card) 1
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ : Equiv.Perm α<GOAL>Multiset.filter (fun n => 2 ≤ n) σ.partition.parts = σ.cycleType
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ τ : Equiv.Perm α<GOAL>IsConj σ τ ↔ σ.partition = τ.partition
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ : Equiv.Perm α<VAR>h : σ.IsThreeCycle<GOAL>σ.cycleType = {3}
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ : Equiv.Perm α<VAR>h : σ.IsThreeCycle<GOAL>σ.support.card = 3
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ : Equiv.Perm α<GOAL>σ.support.card = 3 ↔ σ.IsThreeCycle
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ : Equiv.Perm α<VAR>h : σ.IsThreeCycle<GOAL>σ.IsCycle
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ : Equiv.Perm α<VAR>h : σ.IsThreeCycle<GOAL>Equiv.Perm.sign σ = 1
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>f : Equiv.Perm α<VAR>h : f.IsThreeCycle<GOAL>f⁻¹.IsThreeCycle
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>f : Equiv.Perm α<GOAL>f⁻¹.IsThreeCycle ↔ f.IsThreeCycle
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>g : Equiv.Perm α<VAR>ht : g.IsThreeCycle<GOAL>orderOf g = 3
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>g : Equiv.Perm α<VAR>ht : g.IsThreeCycle<GOAL>(g * g).IsThreeCycle
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>a b c : α<VAR>ab : a ≠ b<VAR>ac : a ≠ c<VAR>bc : b ≠ c<GOAL>(Equiv.swap a b * Equiv.swap a c).IsThreeCycle
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>a b c : α<VAR>ab : a ≠ b<VAR>ac : a ≠ c<GOAL>Equiv.swap a b * Equiv.swap a c ∈ Subgroup.closure {σ | σ.IsThreeCycle}
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>σ τ : Equiv.Perm α<VAR>hσ : σ.IsSwap<VAR>hτ : τ.IsSwap<GOAL>σ * τ ∈ Subgroup.closure {σ | σ.IsThreeCycle}
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>DecidableRel f.SameCycle<VAR>x y : α<GOAL>(f.cycleOf x) y = if f.SameCycle x y then f y else y
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>DecidableRel f.SameCycle<VAR>x : α<GOAL>(f.cycleOf x)⁻¹ = f⁻¹.cycleOf x
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>DecidableRel f.SameCycle<VAR>x : α<VAR>n : ℕ<GOAL>(f.cycleOf x ^ n) x = (f ^ n) x
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>DecidableRel f.SameCycle<VAR>x : α<VAR>n : ℤ<GOAL>(f.cycleOf x ^ n) x = (f ^ n) x
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x y : α<VAR>DecidableRel f.SameCycle<GOAL>f.SameCycle x y → (f.cycleOf x) y = f y
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x y : α<VAR>DecidableRel f.SameCycle<GOAL>¬f.SameCycle x y → (f.cycleOf x) y = y
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x y : α<VAR>DecidableRel f.SameCycle<VAR>h : f.SameCycle x y<GOAL>f.cycleOf x = f.cycleOf y
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>DecidableRel f.SameCycle<VAR>x : α<VAR>k : ℤ<GOAL>(f.cycleOf x) ((f ^ k) x) = (f ^ (k + 1)) x
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>DecidableRel f.SameCycle<VAR>x : α<VAR>k : ℕ<GOAL>(f.cycleOf x) ((f ^ k) x) = (f ^ (k + 1)) x
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>DecidableRel f.SameCycle<VAR>x : α<GOAL>(f.cycleOf x) (f x) = f (f x)
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>DecidableRel f.SameCycle<VAR>x : α<GOAL>(f.cycleOf x) x = f x
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x : α<VAR>DecidableRel f.SameCycle<VAR>hf : f.IsCycle<VAR>hx : f x ≠ x<GOAL>f.cycleOf x = f
<VAR>α : Type u_2<VAR>x : α<VAR>f : Equiv.Perm α<VAR>DecidableRel f.SameCycle<GOAL>f.cycleOf x = 1 ↔ f x = x
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>DecidableRel f.SameCycle<VAR>x : α<GOAL>f.cycleOf (f x) = f.cycleOf x
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>DecidableRel f.SameCycle<VAR>n : ℕ<VAR>x : α<GOAL>f.cycleOf ((f ^ n) x) = f.cycleOf x
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>DecidableRel f.SameCycle<VAR>n : ℤ<VAR>x : α<GOAL>f.cycleOf ((f ^ n) x) = f.cycleOf x
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x : α<VAR>DecidableRel f.SameCycle<VAR>DecidableEq α<VAR>hf : f.IsCycle<GOAL>f.cycleOf x = if f x = x then 1 else f
<VAR>α : Type u_2<VAR>DecidableRel (Equiv.Perm.SameCycle 1)<VAR>x : α<GOAL>Equiv.Perm.cycleOf 1 x = 1
<VAR>α : Type u_2<VAR>x : α<VAR>f : Equiv.Perm α<VAR>DecidableRel f.SameCycle<VAR>hx : f x ≠ x<GOAL>(f.cycleOf x).IsCycle
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x : α<VAR>DecidableRel f.SameCycle<VAR>DecidableEq α<VAR>Fintype α<GOAL>2 ≤ (f.cycleOf x).support.card ↔ f x ≠ x
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x : α<VAR>DecidableRel f.SameCycle<VAR>DecidableEq α<VAR>Fintype α<GOAL>(f.cycleOf x).support.Nonempty ↔ f x ≠ x
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x : α<VAR>DecidableRel f.SameCycle<VAR>DecidableEq α<VAR>Fintype α<GOAL>0 < (f.cycleOf x).support.card ↔ f x ≠ x
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>DecidableRel f.SameCycle<VAR>n : ℕ<VAR>x : α<GOAL>(f ^ (n % orderOf (f.cycleOf x))) x = (f ^ n) x
<VAR>α : Type u_2<VAR>f g : Equiv.Perm α<VAR>DecidableRel f.SameCycle<VAR>DecidableRel (f * g).SameCycle<VAR>h : Commute f g<VAR>x : α<VAR>hx : g x = x<GOAL>(f * g).cycleOf x = f.cycleOf x
<VAR>α : Type u_2<VAR>f g : Equiv.Perm α<VAR>DecidableRel f.SameCycle<VAR>DecidableRel g.SameCycle<VAR>DecidableRel (f * g).SameCycle<VAR>DecidableRel (g * f).SameCycle<VAR>h : f.Disjoint g<VAR>x : α<GOAL>(f * g).cycleOf x = f.cycleOf x * g.cycleOf x
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x : α<VAR>DecidableRel f.SameCycle<VAR>DecidableEq α<VAR>Fintype α<GOAL>(f.cycleOf x).support = ∅ ↔ x ∉ f.support
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<VAR>x : α<GOAL>(f.cycleOf x).support ≤ f.support
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x y : α<VAR>DecidableRel f.SameCycle<VAR>DecidableEq α<VAR>Fintype α<GOAL>y ∈ (f.cycleOf x).support ↔ f.SameCycle x y ∧ x ∈ f.support
<VAR>α : Type u_2<VAR>f : Equiv.Perm α<VAR>x y : α<VAR>DecidableRel f.SameCycle<VAR>hx : f x ≠ x<VAR>DecidableEq α<VAR>Fintype α<GOAL>y ∈ (f.cycleOf x).support ↔ f.SameCycle x y
<VAR>α : Type u_2<VAR>x y : α<VAR>f : Equiv.Perm α<VAR>DecidableEq α<VAR>Fintype α<VAR>h : f.SameCycle x y<GOAL>x ∈ f.support ↔ y ∈ f.support
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<VAR>n : ℕ<VAR>x : α<GOAL>(f ^ (n % (f.cycleOf x).support.card)) x = (f ^ n) x
<VAR>α : Type u_2<VAR>x : α<VAR>f : Equiv.Perm α<VAR>DecidableRel f.SameCycle<GOAL>(f.cycleOf x).IsCycle ↔ f x ≠ x
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<VAR>x : α<GOAL>f.IsCycleOn ↑(f.cycleOf x).support
<VAR>α : Type u_2<VAR>x y : α<VAR>f : Equiv.Perm α<VAR>DecidableEq α<VAR>Fintype α<VAR>h : f.SameCycle x y<VAR>hx : x ∈ f.support<GOAL>∃ i < (f.cycleOf x).support.card, (f ^ i) x = y
<VAR>α : Type u_2<VAR>x y : α<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<VAR>h : f.SameCycle x y<GOAL>∃ i, 0 < i ∧ i ≤ (f.cycleOf x).support.card + 1 ∧ (f ^ i) x = y
<VAR>α : Type u_4<VAR>Finite α<VAR>l : List (Equiv.Perm α)<VAR>h1 : ∀ σ ∈ l, σ.IsCycle<VAR>h2 : List.Pairwise Equiv.Perm.Disjoint l<VAR>σ : Equiv.Perm α<GOAL>σ ∈ l ↔ σ.IsCycle ∧ ∀ (a : α), σ a ≠ a → σ a = l.prod a
<VAR>α : Type u_4<VAR>Finite α<VAR>l₁ l₂ : List (Equiv.Perm α)<VAR>h₀ : l₁.prod = l₂.prod<VAR>h₁l₁ : ∀ σ ∈ l₁, σ.IsCycle<VAR>h₁l₂ : ∀ σ ∈ l₂, σ.IsCycle<VAR>h₂l₁ : List.Pairwise Equiv.Perm.Disjoint l₁<VAR>h₂l₂ : List.Pairwise Equiv.Perm.Disjoint l₂<GOAL>l₁.Perm l₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>σ : Equiv.Perm α<VAR>l : List (Equiv.Perm α)<VAR>hn : l.Nodup<GOAL>σ.cycleFactorsFinset = l.toFinset ↔ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Equiv.Perm.Disjoint l ∧ l.prod = σ
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>σ : Equiv.Perm α<VAR>s : Finset (Equiv.Perm α)<GOAL>σ.cycleFactorsFinset = s ↔ (∀ f ∈ s, f.IsCycle) ∧ ∃ (h : (↑s).Pairwise Equiv.Perm.Disjoint), s.noncommProd id ⋯ = σ
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<GOAL>(↑f.cycleFactorsFinset).Pairwise Equiv.Perm.Disjoint
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<GOAL>(↑f.cycleFactorsFinset).Pairwise Commute
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<VAR>comm : (↑f.cycleFactorsFinset).Pairwise Commute := ⋯<GOAL>f.cycleFactorsFinset.noncommProd id comm = f
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>f p : Equiv.Perm α<GOAL>p ∈ f.cycleFactorsFinset ↔ p.IsCycle ∧ ∀ a ∈ p.support, p a = f a
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<VAR>x : α<GOAL>f.cycleOf x ∈ f.cycleFactorsFinset ↔ x ∈ f.support
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>p f : Equiv.Perm α<VAR>h : p ∈ f.cycleFactorsFinset<GOAL>p.support ≤ f.support
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<GOAL>f.cycleFactorsFinset = ∅ ↔ f = 1
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<GOAL>Equiv.Perm.cycleFactorsFinset 1 = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<GOAL>f.cycleFactorsFinset = {f} ↔ f.IsCycle
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>f : Equiv.Perm α<VAR>hf : f.IsCycle<GOAL>f.cycleFactorsFinset = {f}
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>f g : Equiv.Perm α<GOAL>f.cycleFactorsFinset = {g} ↔ f.IsCycle ∧ f = g
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<GOAL>Function.Injective Equiv.Perm.cycleFactorsFinset
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>f g : Equiv.Perm α<VAR>h : f.Disjoint g<GOAL>Disjoint f.cycleFactorsFinset g.cycleFactorsFinset
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>f g : Equiv.Perm α<VAR>h : f.Disjoint g<GOAL>(f * g).cycleFactorsFinset = f.cycleFactorsFinset ∪ g.cycleFactorsFinset
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>f g : Equiv.Perm α<VAR>h : f ∈ g.cycleFactorsFinset<GOAL>(g * f⁻¹).Disjoint f
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>f c : Equiv.Perm α<VAR>a : α<VAR>ha : a ∈ c.support<VAR>hc : c ∈ f.cycleFactorsFinset<GOAL>c = f.cycleOf a
<VAR>β : Type u_3<VAR>Finite β<VAR>P : Equiv.Perm β → Prop<VAR>σ : Equiv.Perm β<VAR>base_one : P 1<VAR>base_cycles : ∀ (σ : Equiv.Perm β), σ.IsCycle → P σ<VAR>induction_disjoint : ∀ (σ τ : Equiv.Perm β), σ.Disjoint τ → σ.IsCycle → P σ → P τ → P (σ * τ)<GOAL>P σ
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>f g : Equiv.Perm α<VAR>h : f ∈ g.cycleFactorsFinset<GOAL>(g * f⁻¹).cycleFactorsFinset = g.cycleFactorsFinset \ {f}
<VAR>t : Type u → Type u → Type u<VAR>Bitraversable t<VAR>LawfulBitraversable t<VAR>α β : Type u<VAR>x : t α β<GOAL>Bitraversable.tfst pure x = pure x
<VAR>t : Type u → Type u → Type u<VAR>Bitraversable t<VAR>LawfulBitraversable t<VAR>α β : Type u<GOAL>Bitraversable.tfst pure = pure
<VAR>t : Type u → Type u → Type u<VAR>Bitraversable t<VAR>LawfulBitraversable t<VAR>α β : Type u<GOAL>Bitraversable.tsnd pure = pure
<VAR>t : Type u → Type u → Type u<VAR>Bitraversable t<VAR>LawfulBitraversable t<VAR>α β : Type u<VAR>x : t α β<GOAL>Bitraversable.tsnd pure x = pure x
<VAR>t : Type u → Type u → Type u<VAR>Bitraversable t<VAR>F G : Type u → Type u<VAR>Applicative F<VAR>Applicative G<VAR>LawfulBitraversable t<VAR>LawfulApplicative F<VAR>LawfulApplicative G<VAR>α₀ α₁ α₂ β : Type u<VAR>f : α₀ → F α₁<VAR>f' : α₁ → G α₂<GOAL>Functor.Comp.mk ∘ Functor.map (Bitraversable.tfst f') ∘ Bitraversable.tfst f = Bitraversable.tfst (Functor.Comp.mk ∘ Functor.map f' ∘ f)
<VAR>t : Type u → Type u → Type u<VAR>Bitraversable t<VAR>F G : Type u → Type u<VAR>Applicative F<VAR>Applicative G<VAR>LawfulBitraversable t<VAR>LawfulApplicative F<VAR>LawfulApplicative G<VAR>α₀ α₁ α₂ β : Type u<VAR>f : α₀ → F α₁<VAR>f' : α₁ → G α₂<VAR>x : t α₀ β<GOAL>Functor.Comp.mk (Bitraversable.tfst f' <$> Bitraversable.tfst f x) = Bitraversable.tfst (Functor.Comp.mk ∘ Functor.map f' ∘ f) x
<VAR>t : Type u → Type u → Type u<VAR>Bitraversable t<VAR>F G : Type u → Type u<VAR>Applicative F<VAR>Applicative G<VAR>LawfulBitraversable t<VAR>LawfulApplicative F<VAR>LawfulApplicative G<VAR>α₀ α₁ β₀ β₁ : Type u<VAR>f : α₀ → F α₁<VAR>f' : β₀ → G β₁<VAR>x : t α₀ β₀<GOAL>Functor.Comp.mk (Bitraversable.tfst f <$> Bitraversable.tsnd f' x) = bitraverse (Functor.Comp.mk ∘ pure ∘ f) (Functor.Comp.mk ∘ Functor.map pure ∘ f') x
<VAR>t : Type u → Type u → Type u<VAR>Bitraversable t<VAR>F G : Type u → Type u<VAR>Applicative F<VAR>Applicative G<VAR>LawfulBitraversable t<VAR>LawfulApplicative F<VAR>LawfulApplicative G<VAR>α₀ α₁ β₀ β₁ : Type u<VAR>f : α₀ → F α₁<VAR>f' : β₀ → G β₁<GOAL>Functor.Comp.mk ∘ Functor.map (Bitraversable.tfst f) ∘ Bitraversable.tsnd f' = bitraverse (Functor.Comp.mk ∘ pure ∘ f) (Functor.Comp.mk ∘ Functor.map pure ∘ f')
<VAR>t : Type u → Type u → Type u<VAR>Bitraversable t<VAR>F G : Type u → Type u<VAR>Applicative F<VAR>Applicative G<VAR>LawfulBitraversable t<VAR>LawfulApplicative F<VAR>LawfulApplicative G<VAR>α₀ α₁ β₀ β₁ : Type u<VAR>f : α₀ → F α₁<VAR>f' : β₀ → G β₁<VAR>x : t α₀ β₀<GOAL>Functor.Comp.mk (Bitraversable.tsnd f' <$> Bitraversable.tfst f x) = bitraverse (Functor.Comp.mk ∘ Functor.map pure ∘ f) (Functor.Comp.mk ∘ pure ∘ f') x
<VAR>t : Type u → Type u → Type u<VAR>Bitraversable t<VAR>F G : Type u → Type u<VAR>Applicative F<VAR>Applicative G<VAR>LawfulBitraversable t<VAR>LawfulApplicative F<VAR>LawfulApplicative G<VAR>α₀ α₁ β₀ β₁ : Type u<VAR>f : α₀ → F α₁<VAR>f' : β₀ → G β₁<GOAL>Functor.Comp.mk ∘ Functor.map (Bitraversable.tsnd f') ∘ Bitraversable.tfst f = bitraverse (Functor.Comp.mk ∘ Functor.map pure ∘ f) (Functor.Comp.mk ∘ pure ∘ f')
<VAR>t : Type u → Type u → Type u<VAR>Bitraversable t<VAR>F G : Type u → Type u<VAR>Applicative F<VAR>Applicative G<VAR>LawfulBitraversable t<VAR>LawfulApplicative F<VAR>LawfulApplicative G<VAR>α β₀ β₁ β₂ : Type u<VAR>g : β₀ → F β₁<VAR>g' : β₁ → G β₂<GOAL>Functor.Comp.mk ∘ Functor.map (Bitraversable.tsnd g') ∘ Bitraversable.tsnd g = Bitraversable.tsnd (Functor.Comp.mk ∘ Functor.map g' ∘ g)
<VAR>t : Type u → Type u → Type u<VAR>Bitraversable t<VAR>F G : Type u → Type u<VAR>Applicative F<VAR>Applicative G<VAR>LawfulBitraversable t<VAR>LawfulApplicative F<VAR>LawfulApplicative G<VAR>α β₀ β₁ β₂ : Type u<VAR>g : β₀ → F β₁<VAR>g' : β₁ → G β₂<VAR>x : t α β₀<GOAL>Functor.Comp.mk (Bitraversable.tsnd g' <$> Bitraversable.tsnd g x) = Bitraversable.tsnd (Functor.Comp.mk ∘ Functor.map g' ∘ g) x
<VAR>t : Type u → Type u → Type u<VAR>Bitraversable t<VAR>LawfulBitraversable t<VAR>α α' β : Type u<VAR>f : α → α'<VAR>x : t α β<GOAL>Bitraversable.tfst (pure ∘ f) x = pure (Bifunctor.fst f x)
<VAR>t : Type u → Type u → Type u<VAR>Bitraversable t<VAR>LawfulBitraversable t<VAR>α α' β : Type u<VAR>f : α → α'<GOAL>Bitraversable.tfst (pure ∘ f) = pure ∘ Bifunctor.fst f
<VAR>t : Type u → Type u → Type u<VAR>Bitraversable t<VAR>LawfulBitraversable t<VAR>α β β' : Type u<VAR>f : β → β'<VAR>x : t α β<GOAL>Bitraversable.tsnd (pure ∘ f) x = pure (Bifunctor.snd f x)
<VAR>t : Type u → Type u → Type u<VAR>Bitraversable t<VAR>LawfulBitraversable t<VAR>α β β' : Type u<VAR>f : β → β'<GOAL>Bitraversable.tsnd (pure ∘ f) = pure ∘ Bifunctor.snd f
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Monoid (G i)<VAR>Monoid H<VAR>φ : (i : ι) → H →* G i<VAR>i : ι<GOAL>(Monoid.PushoutI.of i).comp (φ i) = Monoid.PushoutI.base φ
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Monoid (G i)<VAR>Monoid H<VAR>φ : (i : ι) → H →* G i<VAR>i : ι<VAR>x : H<GOAL>(Monoid.PushoutI.of i) ((φ i) x) = (Monoid.PushoutI.base φ) x
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>Monoid K<VAR>(i : ι) → Monoid (G i)<VAR>Monoid H<VAR>φ : (i : ι) → H →* G i<VAR>f : (i : ι) → G i →* K<VAR>k : H →* K<VAR>hf : ∀ (i : ι), (f i).comp (φ i) = k<VAR>i : ι<VAR>g : G i<GOAL>(Monoid.PushoutI.lift f k hf) ((Monoid.PushoutI.of i) g) = (f i) g
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>Monoid K<VAR>(i : ι) → Monoid (G i)<VAR>Monoid H<VAR>φ : (i : ι) → H →* G i<VAR>f : (i : ι) → G i →* K<VAR>k : H →* K<VAR>hf : ∀ (i : ι), (f i).comp (φ i) = k<VAR>g : H<GOAL>(Monoid.PushoutI.lift f k hf) ((Monoid.PushoutI.base φ) g) = k g
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>Monoid K<VAR>(i : ι) → Monoid (G i)<VAR>Monoid H<VAR>φ : (i : ι) → H →* G i<VAR>f g : Monoid.PushoutI φ →* K<VAR>h : ∀ (i : ι), f.comp (Monoid.PushoutI.of i) = g.comp (Monoid.PushoutI.of i)<VAR>hbase : f.comp (Monoid.PushoutI.base φ) = g.comp (Monoid.PushoutI.base φ)<GOAL>f = g
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>Monoid K<VAR>(i : ι) → Monoid (G i)<VAR>Monoid H<VAR>φ : (i : ι) → H →* G i<VAR>hn : Nonempty ι<VAR>f g : Monoid.PushoutI φ →* K<VAR>h : ∀ (i : ι), f.comp (Monoid.PushoutI.of i) = g.comp (Monoid.PushoutI.of i)<GOAL>f = g
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>Monoid K<VAR>(i : ι) → Monoid (G i)<VAR>Monoid H<VAR>φ : (i : ι) → H →* G i<VAR>f : { f // ∀ (i : ι), (f.1 i).comp (φ i) = f.2 }<GOAL>Monoid.PushoutI.homEquiv.symm f = Monoid.PushoutI.lift (↑f).1 (↑f).2 ⋯
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>Monoid K<VAR>(i : ι) → Monoid (G i)<VAR>Monoid H<VAR>φ : (i : ι) → H →* G i<VAR>f : Monoid.PushoutI φ →* K<GOAL>↑(Monoid.PushoutI.homEquiv f) = (fun i => f.comp (Monoid.PushoutI.of i), f.comp (Monoid.PushoutI.base φ))
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Monoid (G i)<VAR>Monoid H<VAR>φ : (i : ι) → H →* G i<VAR>i : ι<VAR>g : G i<GOAL>Monoid.PushoutI.ofCoprodI (Monoid.CoprodI.of g) = (Monoid.PushoutI.of i) g
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Monoid (G i)<VAR>Monoid H<VAR>φ : (i : ι) → H →* G i<VAR>motive : Monoid.PushoutI φ → Prop<VAR>x : Monoid.PushoutI φ<VAR>of : ∀ (i : ι) (g : G i), motive ((Monoid.PushoutI.of i) g)<VAR>base : ∀ (h : H), motive ((Monoid.PushoutI.base φ) h)<VAR>mul : ∀ (x y : Monoid.PushoutI φ), motive x → motive y → motive (x * y)<GOAL>motive x
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>self : Monoid.PushoutI.NormalWord.Transversal φ<VAR>i : ι<GOAL>Function.Injective ⇑(φ i)
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>self : Monoid.PushoutI.NormalWord.Transversal φ<VAR>i : ι<GOAL>1 ∈ self.set i
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>self : Monoid.PushoutI.NormalWord.Transversal φ<VAR>i : ι<GOAL>Subgroup.IsComplement (↑(φ i).range) (self.set i)
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>hφ : ∀ (i : ι), Function.Injective ⇑(φ i)<GOAL>Nonempty (Monoid.PushoutI.NormalWord.Transversal φ)
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Monoid.PushoutI.NormalWord.Transversal φ<VAR>self : Monoid.PushoutI.NormalWord d<VAR>i : ι<VAR>g : G i<GOAL>⟨i, g⟩ ∈ self.toList → g ∈ d.set i
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Monoid.PushoutI.NormalWord.Transversal φ<VAR>i : ι<VAR>self : Monoid.PushoutI.NormalWord.Pair d i<GOAL>∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ self.tail.toList → g ∈ d.set i_1
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Monoid.PushoutI.NormalWord.Transversal φ<GOAL>Monoid.PushoutI.NormalWord.empty.head = 1
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Monoid.PushoutI.NormalWord.Transversal φ<GOAL>Monoid.PushoutI.NormalWord.empty.toList = []
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Monoid.PushoutI.NormalWord.Transversal φ<VAR>w₁ w₂ : Monoid.PushoutI.NormalWord d<VAR>hhead : w₁.head = w₂.head<VAR>hlist : w₁.toList = w₂.toList<GOAL>w₁ = w₂
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Monoid.PushoutI.NormalWord.Transversal φ<VAR>w₁ w₂ : Monoid.PushoutI.NormalWord d<GOAL>w₁ = w₂ ↔ w₁.head = w₂.head ∧ w₁.toList = w₂.toList
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Monoid.PushoutI.NormalWord.Transversal φ<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (G i)<VAR>w : Monoid.CoprodI.Word G<VAR>i : ι<VAR>h : H<VAR>hw : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → g ∈ d.set i<VAR>hφw : ∀ (j : ι) (g : G j), ⟨j, g⟩ ∈ (Monoid.CoprodI.of ((φ i) h) • w).toList → g ∈ d.set j<GOAL>h = 1
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Monoid.PushoutI.NormalWord.Transversal φ<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (G i)<VAR>w₁ w₂ : Monoid.PushoutI.NormalWord d<VAR>i : ι<VAR>h : Monoid.CoprodI.of ((φ i) w₁.head) • w₁.toWord = Monoid.CoprodI.of ((φ i) w₂.head) • w₂.toWord<GOAL>w₁ = w₂
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Monoid.PushoutI.NormalWord.Transversal φ<VAR>i : ι<VAR>g : G i<VAR>w : Monoid.PushoutI.NormalWord d<VAR>hmw : w.fstIdx ≠ some i<VAR>hgr : g ∉ (φ i).range<GOAL>(Monoid.PushoutI.NormalWord.cons g w hmw hgr).toList = ⟨i, ↑(⋯.equiv (g * (φ i) w.head)).2⟩ :: w.toList
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Monoid.PushoutI.NormalWord.Transversal φ<VAR>i : ι<VAR>g : G i<VAR>w : Monoid.PushoutI.NormalWord d<VAR>hmw : w.fstIdx ≠ some i<VAR>hgr : g ∉ (φ i).range<GOAL>(Monoid.PushoutI.NormalWord.cons g w hmw hgr).head = (MonoidHom.ofInjective ⋯).symm (⋯.equiv (g * (φ i) w.head)).1
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Monoid.PushoutI.NormalWord.Transversal φ<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (G i)<VAR>i : ι<GOAL>Function.Injective (Monoid.PushoutI.NormalWord.rcons i)
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Monoid.PushoutI.NormalWord.Transversal φ<VAR>h : H<VAR>w : Monoid.PushoutI.NormalWord d<GOAL>h • w = { toWord := w.toWord, head := h * w.head, normalized := ⋯ }
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>(i : ι) → Group (G i)<VAR>Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Monoid.PushoutI.NormalWord.Transversal φ<VAR>DecidableEq ι<VAR>(i : ι) → DecidableEq (G i)<VAR>i : ι<VAR>g : G i<VAR>w : Monoid.PushoutI.NormalWord d<GOAL>g • w = (Monoid.PushoutI.NormalWord.equivPair i).symm (let __src := (Monoid.PushoutI.NormalWord.equivPair i) w; { head := g * ((Monoid.PushoutI.NormalWord.equivPair i) w).head, tail := __src.tail, fstIdx_ne := ⋯, normalized := ⋯ })