ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>U : Set E<VAR>f : ℂ → ℂ<VAR>g : E → ℂ<VAR>z₀✝ w : ℂ<VAR>ε r✝ m : ℝ<VAR>z₀ : E<VAR>hg : AnalyticAt ℂ g z₀<VAR>ray : E → ℂ → E := fun z t => z₀ + t • z<VAR>gray : E → ℂ → ℂ := fun z => g ∘ ray z<VAR>r : ℝ<VAR>hr : r > 0<VAR>hgr : ball z₀ r ⊆ {x | AnalyticAt ℂ g x}<GOAL>(∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀) ∨ 𝓝 (g z₀) ≤ map g (𝓝 z₀)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<GOAL>cs.rightInvSeq ω.reverse = (cs.leftInvSeq ω).reverse
<VAR>p : ℝ[X]<GOAL>p.roots.toFinset.card ≤ ((derivative p).roots.toFinset \ p.roots.toFinset).card + 1
<VAR>p : ℝ[X]<VAR>hp' : derivative p = 0<GOAL>p.roots.toFinset.card ≤ ((derivative p).roots.toFinset \ p.roots.toFinset).card + 1
<VAR>p : ℝ[X]<VAR>hp' : derivative p ≠ 0<GOAL>p.roots.toFinset.card ≤ ((derivative p).roots.toFinset \ p.roots.toFinset).card + 1
<VAR>p : ℝ[X]<VAR>hp' : derivative p ≠ 0<VAR>hp : p ≠ 0<GOAL>p.roots.toFinset.card ≤ ((derivative p).roots.toFinset \ p.roots.toFinset).card + 1
<VAR>p : ℝ[X]<VAR>hp' : derivative p ≠ 0<VAR>hp : p ≠ 0<VAR>x : ℝ<VAR>hx : x ∈ p.roots.toFinset<VAR>y : ℝ<VAR>hy : y ∈ p.roots.toFinset<VAR>hxy : x < y<VAR>hxy' : ∀ z ∈ p.roots.toFinset, z ∉ Set.Ioo x y<GOAL>∃ z ∈ (derivative p).roots.toFinset, x < z ∧ z < y
<VAR>p : ℝ[X]<VAR>hp' : derivative p ≠ 0<VAR>hp : p ≠ 0<VAR>x : ℝ<VAR>hx : p.IsRoot x<VAR>y : ℝ<VAR>hy : p.IsRoot y<VAR>hxy : x < y<VAR>hxy' : ∀ z ∈ p.roots.toFinset, z ∉ Set.Ioo x y<GOAL>∃ z ∈ (derivative p).roots.toFinset, x < z ∧ z < y
<VAR>p : ℝ[X]<VAR>hp' : derivative p ≠ 0<VAR>hp : p ≠ 0<VAR>x : ℝ<VAR>hx : p.IsRoot x<VAR>y : ℝ<VAR>hy : p.IsRoot y<VAR>hxy : x < y<VAR>hxy' : ∀ z ∈ p.roots.toFinset, z ∉ Set.Ioo x y<VAR>z : ℝ<VAR>hz1 : z ∈ Set.Ioo x y<VAR>hz2 : deriv (fun x => eval x p) z = 0<GOAL>∃ z ∈ (derivative p).roots.toFinset, x < z ∧ z < y
<VAR>p : ℝ[X]<VAR>hp' : derivative p ≠ 0<VAR>hp : p ≠ 0<VAR>x : ℝ<VAR>hx : p.IsRoot x<VAR>y : ℝ<VAR>hy : p.IsRoot y<VAR>hxy : x < y<VAR>hxy' : ∀ z ∈ p.roots.toFinset, z ∉ Set.Ioo x y<VAR>z : ℝ<VAR>hz1 : z ∈ Set.Ioo x y<VAR>hz2 : deriv (fun x => eval x p) z = 0<GOAL>z ∈ (derivative p).roots.toFinset
<VAR>q : ℚ<VAR>x y : ℝ<VAR>h : Irrational x<VAR>m : ℤ<GOAL>Irrational (↑m + x)
<VAR>q : ℚ<VAR>x y : ℝ<VAR>h : Irrational x<VAR>m : ℤ<GOAL>Irrational (↑↑m + x)
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n✝ m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>n : σ<VAR>f : MvPolynomial σ R<VAR>d : ℕ<VAR>h : 0 < d<GOAL>degreeOf n f < d ↔ ∀ m ∈ f.support, m n < d
<VAR>L : Language<VAR>L' : Language<VAR>M✝ : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : L.Structure M✝<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<VAR>M : Type w<VAR>inst✝ : L[[α]].Structure M<VAR>s : Set α<GOAL>M ⊨ L.distinctConstantsTheory s ↔ Set.InjOn (fun i => ↑(L.con i)) s
<VAR>L : Language<VAR>L' : Language<VAR>M✝ : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : L.Structure M✝<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<VAR>M : Type w<VAR>inst✝ : L[[α]].Structure M<VAR>s : Set α<GOAL>(∀ (φ : L[[α]].Sentence) (x x_1 : α), (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → ((L.con x).term.equal (L.con x_1).term).not = φ → M ⊨ φ) ↔ Set.InjOn (fun i => ↑(L.con i)) s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>m : M<GOAL>-(e0 Q * (v Q) m) = (v Q) m * e0 Q
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>m : M<GOAL>(algebraMap R (CliffordAlgebra (Q' Q))) (QuadraticMap.polar ⇑(Q' Q) (0, 1) ((LinearMap.inl R M R) m)) = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>m : M<GOAL>(algebraMap R (CliffordAlgebra (Q' Q))) (Q (0 + m) + -((1 + 0) * (1 + 0)) - (Q 0 + -(1 * 1)) - (Q m + -(0 * 0))) = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_4, u_1} C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>X : I₁ ⊕ I₂ → C<VAR>c : Cofan X<VAR>c₁ : Cofan (X ∘ Sum.inl)<VAR>c₂ : Cofan (X ∘ Sum.inr)<VAR>hc : IsColimit c<VAR>hc₁ : IsColimit c₁<VAR>hc₂ : IsColimit c₂<VAR>inst✝ : MonoCoprod C<VAR>inl : c₁.pt ⟶ c.pt<VAR>hinl : ∀ (i₁ : I₁), c₁.inj i₁ ≫ inl = c.inj (Sum.inl i₁)<GOAL>Mono inl
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_4, u_1} C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>X : I₁ ⊕ I₂ → C<VAR>c : Cofan X<VAR>c₁ : Cofan (X ∘ Sum.inl)<VAR>c₂ : Cofan (X ∘ Sum.inr)<VAR>hc : IsColimit c<VAR>hc₁ : IsColimit c₁<VAR>hc₂ : IsColimit c₂<VAR>inst✝ : MonoCoprod C<VAR>inl : c₁.pt ⟶ c.pt<VAR>hinl : ∀ (i₁ : I₁), c₁.inj i₁ ≫ inl = c.inj (Sum.inl i₁)<GOAL>inl = (binaryCofanSum c c₁ c₂ hc₁ hc₂).inl
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>hfin : Finite a b<VAR>hdiv : a ∣ b<GOAL>0 < (multiplicity a b).get hfin
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Monoid α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>hfin : Finite a b<VAR>hdiv : a ∣ b<VAR>h : (multiplicity a b).get hfin = 0<GOAL>False
<VAR>n x y : ℕ<VAR>hc : x.Coprime y<VAR>h : ↑n = ↑x ^ 2 + ↑y ^ 2<GOAL>IsSquare (-1)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : LieRing L<VAR>inst✝³ : LieAlgebra R L<VAR>inst✝² : LieRing L'<VAR>inst✝¹ : LieAlgebra R L'<VAR>I J : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>inst✝ : IsSolvable R L<GOAL>radical R L = ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : LieRing L<VAR>inst✝³ : LieAlgebra R L<VAR>inst✝² : LieRing L'<VAR>inst✝¹ : LieAlgebra R L'<VAR>I J : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>inst✝ : IsSolvable R L<GOAL>⊤ ≤ radical R L
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>a : α<VAR>s t : Set α<VAR>h : t ∈ 𝓝[s] a<GOAL>insert a t ∈ 𝓝[insert a s] a
<VAR>d x y : ℤ<GOAL>IsPell { re := x, im := y } ↔ IsPell (star { re := x, im := y })
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>G : Cᵒᵖ<GOAL>IsSeparator (unop G) ↔ IsCoseparator G
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<GOAL>IsPreirreducible s ↔ ∀ (z₁ z₂ : Set X), IsClosed z₁ → IsClosed z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t z₁ z₂ : Set X<GOAL>IsOpen z₁ᶜ → IsOpen z₂ᶜ → (s ∩ z₁ᶜ).Nonempty → (s ∩ z₂ᶜ).Nonempty → (s ∩ (z₁ᶜ ∩ z₂ᶜ)).Nonempty ↔ IsClosed z₁ → IsClosed z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t z₁ z₂ : Set X<GOAL>IsClosed z₁ → IsClosed z₂ → ¬s ⊆ z₁ → ¬s ⊆ z₂ → ¬s ⊆ z₁ ∪ z₂ ↔ IsClosed z₁ → IsClosed z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t z₁ z₂ : Set X<VAR>x✝¹ : IsClosed z₁<VAR>x✝ : IsClosed z₂<GOAL>¬s ⊆ z₁ → ¬s ⊆ z₂ → ¬s ⊆ z₁ ∪ z₂ ↔ s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A✝ : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d✝ : ℝ<VAR>f : ℝ → E<VAR>d : ℝ<VAR>A : MeasurableEmbedding fun x => x + d<GOAL>∫ (x : ℝ) in a..b, f (x + d) = ∫ (x : ℝ) in a + d..b + d, f x ∂Measure.map (fun x => x + d) volume
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A✝ : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d✝ : ℝ<VAR>f : ℝ → E<VAR>d : ℝ<VAR>A : MeasurableEmbedding fun x => x + d<GOAL>∫ (x : ℝ) in a + d..b + d, f x ∂Measure.map (fun x => x + d) volume = ∫ (x : ℝ) in a + d..b + d, f x
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasFiniteCoproducts C<VAR>inst✝¹ : HasCokernels C<VAR>inst✝ : NormalEpiCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>l : IsLimit (KernelFork.ofι 0 ⋯)<VAR>Z✝ : C<VAR>u v : Z✝ ⟶ X<VAR>huv : u ≫ f = v ≫ f<VAR>W : C<VAR>w : W ⟶ X<VAR>hw : w ≫ coequalizer.π u v = 0<VAR>hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)<VAR>m : coequalizer u v ⟶ Y<VAR>hm : coequalizer.π u v ≫ m = f<GOAL>u = v
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasFiniteCoproducts C<VAR>inst✝¹ : HasCokernels C<VAR>inst✝ : NormalEpiCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>l : IsLimit (KernelFork.ofι 0 ⋯)<VAR>Z✝ : C<VAR>u v : Z✝ ⟶ X<VAR>huv : u ≫ f = v ≫ f<VAR>W : C<VAR>w : W ⟶ X<VAR>hw : w ≫ coequalizer.π u v = 0<VAR>hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)<VAR>m : coequalizer u v ⟶ Y<VAR>hm : coequalizer.π u v ≫ m = f<VAR>reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h<GOAL>u = v
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasFiniteCoproducts C<VAR>inst✝¹ : HasCokernels C<VAR>inst✝ : NormalEpiCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>l : IsLimit (KernelFork.ofι 0 ⋯)<VAR>Z✝ : C<VAR>u v : Z✝ ⟶ X<VAR>huv : u ≫ f = v ≫ f<VAR>W : C<VAR>w : W ⟶ X<VAR>hw : w ≫ coequalizer.π u v = 0<VAR>hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)<VAR>m : coequalizer u v ⟶ Y<VAR>hm : coequalizer.π u v ≫ m = f<VAR>reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h<VAR>hwf : w ≫ f = 0<GOAL>u = v
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasFiniteCoproducts C<VAR>inst✝¹ : HasCokernels C<VAR>inst✝ : NormalEpiCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>l : IsLimit (KernelFork.ofι 0 ⋯)<VAR>Z✝ : C<VAR>u v : Z✝ ⟶ X<VAR>huv : u ≫ f = v ≫ f<VAR>W : C<VAR>w : W ⟶ X<VAR>hw : w ≫ coequalizer.π u v = 0<VAR>hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)<VAR>m : coequalizer u v ⟶ Y<VAR>hm : coequalizer.π u v ≫ m = f<VAR>reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h<VAR>hwf : w ≫ f = 0<VAR>n : W ⟶ (KernelFork.ofι 0 ⋯).pt<VAR>hn : n ≫ Fork.ι (KernelFork.ofι 0 ⋯) = w<GOAL>u = v
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasFiniteCoproducts C<VAR>inst✝¹ : HasCokernels C<VAR>inst✝ : NormalEpiCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>l : IsLimit (KernelFork.ofι 0 ⋯)<VAR>Z✝ : C<VAR>u v : Z✝ ⟶ X<VAR>huv : u ≫ f = v ≫ f<VAR>W : C<VAR>w : W ⟶ X<VAR>hw : w ≫ coequalizer.π u v = 0<VAR>hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)<VAR>m : coequalizer u v ⟶ Y<VAR>hm : coequalizer.π u v ≫ m = f<VAR>reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h<VAR>hwf : w ≫ f = 0<VAR>n : W ⟶ (KernelFork.ofι 0 ⋯).pt<VAR>hn : 0 = w<GOAL>u = v
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasFiniteCoproducts C<VAR>inst✝¹ : HasCokernels C<VAR>inst✝ : NormalEpiCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>l : IsLimit (KernelFork.ofι 0 ⋯)<VAR>Z✝ : C<VAR>u v : Z✝ ⟶ X<VAR>huv : u ≫ f = v ≫ f<VAR>W : C<VAR>w : W ⟶ X<VAR>hw : w ≫ coequalizer.π u v = 0<VAR>hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)<VAR>m : coequalizer u v ⟶ Y<VAR>hm : coequalizer.π u v ≫ m = f<VAR>reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h<VAR>hwf : w ≫ f = 0<VAR>n : W ⟶ (KernelFork.ofι 0 ⋯).pt<VAR>hn : 0 = w<VAR>this : IsIso (coequalizer.π u v)<GOAL>u = v
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasFiniteCoproducts C<VAR>inst✝¹ : HasCokernels C<VAR>inst✝ : NormalEpiCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>l : IsLimit (KernelFork.ofι 0 ⋯)<VAR>Z✝ : C<VAR>u v : Z✝ ⟶ X<VAR>huv : u ≫ f = v ≫ f<VAR>W : C<VAR>w : W ⟶ X<VAR>hw : w ≫ coequalizer.π u v = 0<VAR>hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)<VAR>m : coequalizer u v ⟶ Y<VAR>hm : coequalizer.π u v ≫ m = f<VAR>reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h<VAR>hwf : w ≫ f = 0<VAR>n : W ⟶ (KernelFork.ofι 0 ⋯).pt<VAR>hn : 0 = w<VAR>this : IsIso (coequalizer.π u v)<GOAL>u ≫ coequalizer.π u v = v ≫ coequalizer.π u v
<VAR>a x✝ z x : ℂ<GOAL>abs x * Real.sin x.arg = x.im
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Monoid K<VAR>inst✝³ : (i : ι) → Group (G i)<VAR>inst✝² : Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Transversal φ<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (G i)<VAR>i : ι<VAR>g : G i<VAR>w : NormalWord d<VAR>hmw : w.fstIdx ≠ some i<VAR>hgr : g ∉ (φ i).range<GOAL>(cons g w hmw hgr).prod = (of i) g * w.prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>A B : LinearOrder α<VAR>A_le A_lt : α → α → Prop<VAR>le_refl✝¹ : ∀ (a : α), a ≤ a<VAR>le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c<VAR>lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a<VAR>le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b<VAR>A_min A_max : α → α → α<VAR>A_compare : α → α → Ordering<VAR>le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a<VAR>A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1<VAR>A_decidableEq : DecidableEq α<VAR>A_decidableLT : DecidableRel fun x x_1 => x < x_1<VAR>A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b<VAR>A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a<VAR>A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b<VAR>B_min B_max : α → α → α<VAR>B_compare : α → α → Ordering<VAR>B_decidableEq : DecidableEq α<VAR>le_refl✝ : ∀ (a : α), a ≤ a<VAR>le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c<VAR>lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a<VAR>le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b<VAR>le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a<VAR>B_decidableLE : DecidableRel fun x x_1 => x ≤ x_1<VAR>B_decidableLT : DecidableRel fun x x_1 => x < x_1<VAR>B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b<VAR>B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a<VAR>B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b<GOAL>mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT A_min_def A_max_def A_compare_canonical = mk le_total✝ B_decidableLE B_decidableEq B_decidableLT B_min_def B_max_def B_compare_canonical
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>A B : LinearOrder α<VAR>A_le A_lt : α → α → Prop<VAR>le_refl✝¹ : ∀ (a : α), a ≤ a<VAR>le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c<VAR>lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a<VAR>le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b<VAR>A_min A_max : α → α → α<VAR>A_compare : α → α → Ordering<VAR>le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a<VAR>A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1<VAR>A_decidableEq : DecidableEq α<VAR>A_decidableLT : DecidableRel fun x x_1 => x < x_1<VAR>A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b<VAR>A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a<VAR>A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b<VAR>B_min B_max : α → α → α<VAR>B_compare : α → α → Ordering<VAR>B_decidableEq : DecidableEq α<VAR>le_refl✝ : ∀ (a : α), a ≤ a<VAR>le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c<VAR>lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a<VAR>le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b<VAR>le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a<VAR>B_decidableLT : DecidableRel fun x x_1 => x < x_1<VAR>B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b<VAR>B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b<VAR>B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a<GOAL>mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT A_min_def A_max_def A_compare_canonical = mk le_total✝ A_decidableLE B_decidableEq B_decidableLT B_min_def B_max_def B_compare_canonical
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>A B : LinearOrder α<VAR>A_le A_lt : α → α → Prop<VAR>le_refl✝¹ : ∀ (a : α), a ≤ a<VAR>le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c<VAR>lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a<VAR>le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b<VAR>A_min A_max : α → α → α<VAR>A_compare : α → α → Ordering<VAR>le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a<VAR>A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1<VAR>A_decidableEq : DecidableEq α<VAR>A_decidableLT : DecidableRel fun x x_1 => x < x_1<VAR>A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b<VAR>A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a<VAR>A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b<VAR>B_min B_max : α → α → α<VAR>B_compare : α → α → Ordering<VAR>le_refl✝ : ∀ (a : α), a ≤ a<VAR>le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c<VAR>lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a<VAR>le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b<VAR>le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a<VAR>B_decidableLT : DecidableRel fun x x_1 => x < x_1<VAR>B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b<VAR>B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a<VAR>B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b<GOAL>mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT A_min_def A_max_def A_compare_canonical = mk le_total✝ A_decidableLE A_decidableEq B_decidableLT B_min_def B_max_def B_compare_canonical
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>A B : LinearOrder α<VAR>A_le A_lt : α → α → Prop<VAR>le_refl✝¹ : ∀ (a : α), a ≤ a<VAR>le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c<VAR>lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a<VAR>le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b<VAR>A_min A_max : α → α → α<VAR>A_compare : α → α → Ordering<VAR>le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a<VAR>A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1<VAR>A_decidableEq : DecidableEq α<VAR>A_decidableLT : DecidableRel fun x x_1 => x < x_1<VAR>A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b<VAR>A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a<VAR>A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b<VAR>B_min B_max : α → α → α<VAR>B_compare : α → α → Ordering<VAR>le_refl✝ : ∀ (a : α), a ≤ a<VAR>le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c<VAR>lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a<VAR>le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b<VAR>le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a<VAR>B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b<VAR>B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a<VAR>B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b<GOAL>mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT A_min_def A_max_def A_compare_canonical = mk le_total✝ A_decidableLE A_decidableEq A_decidableLT B_min_def B_max_def B_compare_canonical
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>A B : LinearOrder α<VAR>A_le A_lt : α → α → Prop<VAR>le_refl✝¹ : ∀ (a : α), a ≤ a<VAR>le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c<VAR>lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a<VAR>le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b<VAR>A_min A_max : α → α → α<VAR>A_compare : α → α → Ordering<VAR>le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a<VAR>A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1<VAR>A_decidableEq : DecidableEq α<VAR>A_decidableLT : DecidableRel fun x x_1 => x < x_1<VAR>A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b<VAR>A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a<VAR>A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b<VAR>B_min B_max : α → α → α<VAR>B_compare : α → α → Ordering<VAR>le_refl✝ : ∀ (a : α), a ≤ a<VAR>le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c<VAR>lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a<VAR>le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b<VAR>le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a<VAR>B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b<VAR>B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a<VAR>B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b<VAR>this : A_min = B_min<GOAL>mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT A_min_def A_max_def A_compare_canonical = mk le_total✝ A_decidableLE A_decidableEq A_decidableLT B_min_def B_max_def B_compare_canonical
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>A B : LinearOrder α<VAR>A_le A_lt : α → α → Prop<VAR>le_refl✝¹ : ∀ (a : α), a ≤ a<VAR>le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c<VAR>lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a<VAR>le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b<VAR>A_min A_max : α → α → α<VAR>A_compare : α → α → Ordering<VAR>le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a<VAR>A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1<VAR>A_decidableEq : DecidableEq α<VAR>A_decidableLT : DecidableRel fun x x_1 => x < x_1<VAR>A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b<VAR>A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a<VAR>A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b<VAR>B_max : α → α → α<VAR>B_compare : α → α → Ordering<VAR>le_refl✝ : ∀ (a : α), a ≤ a<VAR>le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c<VAR>lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a<VAR>le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b<VAR>le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a<VAR>B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a<VAR>B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b<VAR>B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b<GOAL>mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT A_min_def A_max_def A_compare_canonical = mk le_total✝ A_decidableLE A_decidableEq A_decidableLT B_min_def B_max_def B_compare_canonical
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>A B : LinearOrder α<VAR>A_le A_lt : α → α → Prop<VAR>le_refl✝¹ : ∀ (a : α), a ≤ a<VAR>le_trans✝¹ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c<VAR>lt_iff_le_not_le✝¹ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a<VAR>le_antisymm✝¹ : ∀ (a b : α), a ≤ b → b ≤ a → a = b<VAR>A_min A_max : α → α → α<VAR>A_compare : α → α → Ordering<VAR>le_total✝¹ : ∀ (a b : α), a ≤ b ∨ b ≤ a<VAR>A_decidableLE : DecidableRel fun x x_1 => x ≤ x_1<VAR>A_decidableEq : DecidableEq α<VAR>A_decidableLT : DecidableRel fun x x_1 => x < x_1<VAR>A_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b<VAR>A_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a<VAR>A_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b<VAR>B_max : α → α → α<VAR>B_compare : α → α → Ordering<VAR>le_refl✝ : ∀ (a : α), a ≤ a<VAR>le_trans✝ : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c<VAR>lt_iff_le_not_le✝ : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a<VAR>le_antisymm✝ : ∀ (a b : α), a ≤ b → b ≤ a → a = b<VAR>le_total✝ : ∀ (a b : α), a ≤ b ∨ b ≤ a<VAR>B_max_def : ∀ (a b : α), max a b = if a ≤ b then b else a<VAR>B_compare_canonical : ∀ (a b : α), compare a b = compareOfLessAndEq a b<VAR>B_min_def : ∀ (a b : α), min a b = if a ≤ b then a else b<VAR>this : A_max = B_max<GOAL>mk le_total✝¹ A_decidableLE A_decidableEq A_decidableLT A_min_def A_max_def A_compare_canonical = mk le_total✝ A_decidableLE A_decidableEq A_decidableLT B_min_def B_max_def B_compare_canonical