ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : Ring β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>f✝ g : ℕ → β<VAR>a : ℕ → α<VAR>inst✝ : Archimedean α<VAR>f : ℕ → β<VAR>n : ℕ<VAR>r : α<VAR>hr0 : 0 ≤ r<VAR>hr1 : r < 1<VAR>h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)<VAR>har1 : |r| < 1<VAR>m : ℕ<VAR>hmn : n.succ ≤ m<VAR>hr : 0 < r<VAR>k : ℕ<VAR>hk : m - n.succ = k<GOAL>abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : Ring β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>f✝ g : ℕ → β<VAR>a : ℕ → α<VAR>inst✝ : Archimedean α<VAR>f : ℕ → β<VAR>n : ℕ<VAR>r : α<VAR>hr0 : 0 ≤ r<VAR>hr1 : r < 1<VAR>h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)<VAR>har1 : |r| < 1<VAR>m : ℕ<VAR>hmn : n.succ ≤ m<VAR>hr : 0 < r<VAR>k : ℕ<VAR>hk : m = k + n.succ<GOAL>abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p : RelSeries r<VAR>newHead : α<VAR>rel : r newHead p.head<GOAL>((singleton r newHead).append p rel).last = p.last
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p✝ : Seminorm 𝕜 E<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>x : E<VAR>r : ℝ≥0<VAR>hr : 0 < ↑r<GOAL>(s.sup p).ball x ↑r = ⋂ i ∈ s, (p i).ball x ↑r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 F<VAR>T : E →ₗ.[𝕜] F<VAR>S : F →ₗ.[𝕜] E<VAR>hT : Dense ↑T.domain<VAR>inst✝ : CompleteSpace E<VAR>h : T.IsFormalAdjoint S<VAR>x✝² : ↥S.domain<VAR>x✝¹ : ↥T†.domain<VAR>hxy : ↑x✝² = ↑x✝¹<VAR>x✝ : ↥T.domain<GOAL>⟪↑S x✝², ↑x✝⟫_𝕜 = ⟪↑x✝¹, ↑T x✝⟫_𝕜
<VAR>α : Type u<VAR>β : α → Type v<VAR>m : Multiset ((a : α) × β a)<VAR>l : List ((a : α) × β a)<GOAL>(keys (Quot.mk Setoid.r l)).Nodup ↔ NodupKeys (Quot.mk Setoid.r l)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>f : β → α<VAR>s : Multiset β<VAR>l : List β<GOAL>filter p (map f (Quot.mk Setoid.r l)) = map f (filter (p ∘ f) (Quot.mk Setoid.r l))
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>f : β → α<VAR>s : Multiset β<VAR>l : List β<GOAL>List.map f (List.filter ((fun b => decide (p b)) ∘ f) l) ~ List.map f (List.filter (fun b => decide (p (f b))) l)
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝¹² : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝¹¹ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝¹⁰ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>E : Type u_9<VAR>inst✝⁷ : AddCommMonoid E<VAR>inst✝⁶ : Module R E<VAR>F : Type u_10<VAR>inst✝⁵ : AddCommMonoid F<VAR>t : ι → Type u_11<VAR>t' : ι → Type u_12<VAR>inst✝⁴ : (i : ι) → AddCommMonoid (t i)<VAR>inst✝³ : (i : ι) → Module R (t i)<VAR>inst✝² : (i : ι) → AddCommMonoid (t' i)<VAR>inst✝¹ : (i : ι) → Module R (t' i)<VAR>g : (i : ι) → t i →ₗ[R] t' i<VAR>f : (i : ι) → s i →ₗ[R] t i<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>x : (i : ι) → s i<VAR>u : s i →ₗ[R] t i<VAR>j : ι<GOAL>(update f i u j) (x j) = update (fun j => (f j) (x j)) i (u (x i)) j
<VAR>α : Type u_1<VAR>size✝ : ℕ<VAR>l : Ordnode α<VAR>x✝ : α<VAR>r : Ordnode α<VAR>b : BalancedSz l.size r.size<VAR>bl : l.Balanced<VAR>br : r.Balanced<GOAL>BalancedSz r.dual.size l.dual.size
<VAR>α : Type u_1<VAR>size✝ : ℕ<VAR>l : Ordnode α<VAR>x✝ : α<VAR>r : Ordnode α<VAR>b : BalancedSz l.size r.size<VAR>bl : l.Balanced<VAR>br : r.Balanced<GOAL>BalancedSz r.size l.size
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>s : Setoid α<VAR>x : α<VAR>y : Quotient s<GOAL>⟦x⟧ = y ↔ x ≈ y.out
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>s : Setoid α<VAR>x : α<VAR>y : Quotient s<GOAL>⟦x⟧ = y ↔ ⟦x⟧ = ⟦y.out⟧
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Ring α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>p a b : α<VAR>h : multiplicity p b < multiplicity p a<GOAL>multiplicity p (a + b) = multiplicity p b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Ring α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>p a b : α<VAR>h : multiplicity p b < multiplicity p a<GOAL>multiplicity p (a + b) ≤ multiplicity p b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Ring α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>p a b : α<VAR>h : multiplicity p b < multiplicity p a<GOAL>multiplicity p b ≤ multiplicity p (a + b)
<VAR>R : Type u_1<VAR>inst✝²⁰ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁹ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁸ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹⁷ : AddCommMonoid M<VAR>inst✝¹⁶ : AddCommMonoid N<VAR>inst✝¹⁵ : AddCommMonoid P<VAR>inst✝¹⁴ : AddCommMonoid Q<VAR>inst✝¹³ : AddCommMonoid S<VAR>inst✝¹² : AddCommMonoid T<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module R N<VAR>inst✝⁹ : Module R P<VAR>inst✝⁸ : Module R Q<VAR>inst✝⁷ : Module R S<VAR>inst✝⁶ : Module R T<VAR>inst✝⁵ : DistribMulAction R' M<VAR>inst✝⁴ : Module R'' M<VAR>P' : Type u_10<VAR>Q' : Type u_11<VAR>inst✝³ : AddCommMonoid P'<VAR>inst✝² : Module R P'<VAR>inst✝¹ : AddCommMonoid Q'<VAR>inst✝ : Module R Q'<VAR>r : R<VAR>f : M →ₗ[R] P<VAR>g : N →ₗ[R] Q<VAR>x✝¹ : M<VAR>x✝ : N<GOAL>(((mk R M N).compr₂ (map (r • f) g)) x✝¹) x✝ = (((mk R M N).compr₂ (r • map f g)) x✝¹) x✝
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m : OuterMeasure α<VAR>s : Set α<GOAL>m.trim s = ⨅ t, m ↑t
<VAR>a n : ℕ<VAR>ha : a ∈ n.bitIndices<GOAL>2 ^ a ≤ n
<VAR>a n : ℕ<VAR>ha : a ∈ n.bitIndices<GOAL>2 ^ a ≤ (map (fun i => 2 ^ i) n.bitIndices).sum
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>k✝ : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>x y : L<VAR>m : M<VAR>k : ℕ<VAR>ih : (⇑((toEnd R L M) x ∘ₗ (toEnd R L M) y))^[k] m ∈ lowerCentralSeries R L M (2 * k)<VAR>hk : 2 * k.succ = 2 * k + 1 + 1<GOAL>(⇑((toEnd R L M) x ∘ₗ (toEnd R L M) y))^[k + 1] m ∈ lowerCentralSeries R L M (2 * (k + 1))
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>k✝ : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>x y : L<VAR>m : M<VAR>k : ℕ<VAR>ih : (⇑((toEnd R L M) x ∘ₗ (toEnd R L M) y))^[k] m ∈ lowerCentralSeries R L M (2 * k)<VAR>hk : 2 * k.succ = 2 * k + 1 + 1<GOAL>⁅x, ⁅y, (⇑((toEnd R L M) x) ∘ ⇑((toEnd R L M) y))^[k] m⁆⁆ ∈ ⁅⊤, ⁅⊤, lowerCentralSeries R L M (2 * k)⁆⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>k✝ : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>x y : L<VAR>m : M<VAR>k : ℕ<VAR>ih : (⇑((toEnd R L M) x ∘ₗ (toEnd R L M) y))^[k] m ∈ lowerCentralSeries R L M (2 * k)<VAR>hk : 2 * k.succ = 2 * k + 1 + 1<GOAL>⁅y, (⇑((toEnd R L M) x) ∘ ⇑((toEnd R L M) y))^[k] m⁆ ∈ ⁅⊤, lowerCentralSeries R L M (2 * k)⁆
<VAR>η : Type u_1<VAR>α✝ : Type u_2<VAR>ι✝ : Type u_3<VAR>κ : Type u_4<VAR>l✝ : Line α✝ ι✝<VAR>i : ι✝<VAR>a x✝ : α✝<VAR>α : Type u_5<VAR>α' : Type u_6<VAR>ι : Type u_7<VAR>f : α → α'<VAR>l : Line α ι<VAR>x : α<GOAL>(fun x i => ((map f l).idxFun i).getD x) (f x) = f ∘ (fun x i => (l.idxFun i).getD x) x
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>I : Ideal R<VAR>x : R<VAR>hxI : x ∈ I<VAR>hx : ‖1 - x‖ < 1<VAR>u : Rˣ := Units.oneSub (1 - x) hx<GOAL>1 ∈ I
<VAR>p : ℚ[X]<VAR>p_irr : Irreducible p<VAR>p_deg : Nat.Prime p.natDegree<VAR>p_roots1 : Fintype.card ↑(p.rootSet ℝ) + 1 ≤ Fintype.card ↑(p.rootSet ℂ)<VAR>p_roots2 : Fintype.card ↑(p.rootSet ℂ) ≤ Fintype.card ↑(p.rootSet ℝ) + 3<GOAL>Function.Bijective ⇑(galActionHom p ℂ)
<VAR>p : ℚ[X]<VAR>p_irr : Irreducible p<VAR>p_deg : Nat.Prime p.natDegree<VAR>p_roots1 : Fintype.card ↑(p.rootSet ℝ) + 1 ≤ Fintype.card ↑(p.rootSet ℂ)<VAR>p_roots2 : Fintype.card ↑(p.rootSet ℂ) ≤ Fintype.card ↑(p.rootSet ℝ) + 3<GOAL>Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
<VAR>p : ℚ[X]<VAR>p_irr : Irreducible p<VAR>p_deg : Nat.Prime p.natDegree<VAR>p_roots1 : Fintype.card ↑(p.rootSet ℝ) + 1 ≤ Fintype.card ↑(p.rootSet ℂ)<VAR>p_roots2 : Fintype.card ↑(p.rootSet ℂ) ≤ Fintype.card ↑(p.rootSet ℝ) + 3<VAR>n : ℕ := ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card<GOAL>Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
<VAR>p : ℚ[X]<VAR>p_irr : Irreducible p<VAR>p_deg : Nat.Prime p.natDegree<VAR>p_roots1 : Fintype.card ↑(p.rootSet ℝ) + 1 ≤ Fintype.card ↑(p.rootSet ℂ)<VAR>p_roots2 : Fintype.card ↑(p.rootSet ℂ) ≤ Fintype.card ↑(p.rootSet ℝ) + 3<VAR>n : ℕ := ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card<VAR>hn : 2 ∣ n<GOAL>Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
<VAR>p : ℚ[X]<VAR>p_irr : Irreducible p<VAR>p_deg : Nat.Prime p.natDegree<VAR>p_roots1 : Fintype.card ↑(p.rootSet ℝ) + 1 ≤ Fintype.card ↑(p.rootSet ℂ)<VAR>p_roots2 : Fintype.card ↑(p.rootSet ℂ) ≤ Fintype.card ↑(p.rootSet ℝ) + 3<VAR>n : ℕ := ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card<VAR>hn : 2 ∣ n<VAR>key : (p.rootSet ℂ).toFinset.card = (p.rootSet ℝ).toFinset.card + ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card<GOAL>Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
<VAR>p : ℚ[X]<VAR>p_irr : Irreducible p<VAR>p_deg : Nat.Prime p.natDegree<VAR>p_roots1 : Fintype.card ↑(p.rootSet ℝ) + 1 ≤ Fintype.card ↑(p.rootSet ℂ)<VAR>p_roots2 : Fintype.card ↑(p.rootSet ℂ) ≤ Fintype.card ↑(p.rootSet ℝ) + 3<VAR>n : ℕ := ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card<VAR>hn : 2 ∣ n<VAR>key : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card<GOAL>Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
<VAR>p : ℚ[X]<VAR>p_irr : Irreducible p<VAR>p_deg : Nat.Prime p.natDegree<VAR>p_roots1 : 1 ≤ ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card<VAR>p_roots2 : ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card ≤ 3<VAR>n : ℕ := ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card<VAR>hn : 2 ∣ n<VAR>key : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card<GOAL>Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2
<VAR>p : ℚ[X]<VAR>p_irr : Irreducible p<VAR>p_deg : Nat.Prime p.natDegree<VAR>p_roots1 : 1 ≤ ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card<VAR>p_roots2 : ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card ≤ 3<VAR>n : ℕ := ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card<VAR>hn : 2 ∣ n<VAR>key : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card<GOAL>((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card = 2
<VAR>p : ℚ[X]<VAR>p_irr : Irreducible p<VAR>p_deg : Nat.Prime p.natDegree<VAR>p_roots1 : 1 ≤ ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card<VAR>p_roots2 : ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card ≤ 3<VAR>n : ℕ := ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card<VAR>hn : 2 ∣ n<VAR>key : Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + ((galActionHom p ℂ) ((restrict p ℂ) (AlgEquiv.restrictScalars ℚ conjAe))).support.card<VAR>k : ℕ<VAR>h2 : 1 ≤ 2 * k<VAR>h3 : 2 * k ≤ 3<GOAL>2 * k = 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>A✝ : Matrix n n α<VAR>inst✝⁴ : NonUnitalSemiring α<VAR>inst✝³ : StarRing α<VAR>inst✝² : NonUnitalSemiring β<VAR>inst✝¹ : StarRing β<VAR>inst✝ : Fintype m<VAR>A : Matrix m m α<VAR>B : Matrix n m α<VAR>hA : A.IsHermitian<GOAL>(B * A * Bᴴ).IsHermitian
<VAR>cs cs' : List Char<GOAL>{ data := cs ++ cs' }.next { byteIdx := utf8Len cs } = { byteIdx := utf8Len cs + (cs'.headD default).utf8Size }
<VAR>cs cs' : List Char<GOAL>{ byteIdx := utf8Len cs } + cs'.headD default = { byteIdx := utf8Len cs + (cs'.headD default).utf8Size }
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H : Subgroup G<VAR>inst✝¹ : H.IsCommutative<VAR>inst✝ : H.FiniteIndex<VAR>α β : ↑(leftTransversals ↑H)<VAR>hH : H.Normal<VAR>g : Gᵐᵒᵖ<VAR>this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex<VAR>ϕ : ↥H →* ↥H := { toFun := fun h => ⟨(unop g)⁻¹ * ↑h * unop g, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }<GOAL>diff (MonoidHom.id ↥H) (g • α) (g • β) = ⟨(unop g)⁻¹ * ↑(diff (MonoidHom.id ↥H) α β) * unop g, ⋯⟩
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H : Subgroup G<VAR>inst✝¹ : H.IsCommutative<VAR>inst✝ : H.FiniteIndex<VAR>α β : ↑(leftTransversals ↑H)<VAR>hH : H.Normal<VAR>g : Gᵐᵒᵖ<VAR>this : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex<VAR>ϕ : ↥H →* ↥H := { toFun := fun h => ⟨(unop g)⁻¹ * ↑h * unop g, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }<VAR>x : G ⧸ H<GOAL>(MonoidHom.id ↥H) ⟨(↑((toEquiv ⋯) x))⁻¹ * ↑((toEquiv ⋯) x), ⋯⟩ = ϕ ((MonoidHom.id ↥H) ⟨(↑((toEquiv ⋯) ((Equiv.symm (toPerm g)) x)))⁻¹ * ↑((toEquiv ⋯) ((Equiv.symm (toPerm g)) x)), ⋯⟩)
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>S : Subalgebra R A<VAR>r : R<GOAL>(algebraMap R A) r ∈ Set.center A
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z✝ : ℤ<VAR>a : α<VAR>z : ℤ<GOAL>↑z - ↑⌊↑z⌋ = 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z✝ : ℤ<VAR>a : α<VAR>z : ℤ<GOAL>↑z - ↑z = 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>b : Set (Set α)<VAR>hb : IsTopologicalBasis b<VAR>s : Set α<VAR>a : α<GOAL>(∀ (i : Set α), i ∈ b ∧ a ∈ i → (i ∩ s).Nonempty) ↔ ∀ o ∈ b, a ∈ o → (o ∩ s).Nonempty
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝³ : Monoid β<VAR>inst✝² : Monoid γ<VAR>inst✝¹ : FunLike F β γ<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>h : a ∈ s<VAR>f : α → β<VAR>comm : (↑s).Pairwise fun a b => Commute (f a) (f b)<VAR>comm' : optParam (∀ x ∈ ↑(s.erase a), ∀ y ∈ ↑(s.erase a), x ≠ y → (fun a b => Commute (f a) (f b)) x y) ⋯<GOAL>(s.erase a).noncommProd f comm' * f a = s.noncommProd f comm
<VAR>x✝ y z x : ℝ<VAR>h : x ≠ 0<GOAL>0 ^ x = 0
<VAR>J : Type v'<VAR>inst✝³ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u''<VAR>inst✝¹ : Category.{v'', u''} D<VAR>X Y : C<VAR>inst✝ : FinitaryExtensive C<VAR>n : ℕ<VAR>F : Discrete (Fin n) ⥤ C<VAR>c : Cocone F<VAR>hc : IsColimit c<VAR>f : Fin n → C := F.obj ∘ Discrete.mk<GOAL>IsVanKampenColimit c
<VAR>J : Type v'<VAR>inst✝³ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u''<VAR>inst✝¹ : Category.{v'', u''} D<VAR>X Y : C<VAR>inst✝ : FinitaryExtensive C<VAR>n : ℕ<VAR>F : Discrete (Fin n) ⥤ C<VAR>c : Cocone F<VAR>hc : IsColimit c<VAR>f : Fin n → C := F.obj ∘ Discrete.mk<VAR>this : F = Discrete.functor f<GOAL>IsVanKampenColimit c
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace G<VAR>inst✝ : CompleteSpace F<VAR>A : E →L[𝕜] F<VAR>B : F →L[𝕜] E<GOAL>A = adjoint B ↔ ∀ (x : E) (y : F), ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace G<VAR>inst✝ : CompleteSpace F<VAR>A : E →L[𝕜] F<VAR>B : F →L[𝕜] E<VAR>h : ∀ (x : E) (y : F), ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜<GOAL>A = adjoint B
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace G<VAR>inst✝ : CompleteSpace F<VAR>A : E →L[𝕜] F<VAR>B : F →L[𝕜] E<VAR>h : ∀ (x : E) (y : F), ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜<VAR>x : E<GOAL>A x = (adjoint B) x
<VAR>G : Type u<VAR>inst✝¹ : Monoid G<VAR>inst✝ : IsCancelMul G<VAR>h : ∀ (g : G), orderOf g ∣ 2<VAR>a b : G<GOAL>Commute a b
<VAR>G : Type u<VAR>inst✝¹ : Monoid G<VAR>inst✝ : IsCancelMul G<VAR>a b : G<VAR>h : ∀ (g : G), g ^ 2 = 1<GOAL>Commute a b
<VAR>G : Type u<VAR>inst✝¹ : Monoid G<VAR>inst✝ : IsCancelMul G<VAR>a b : G<VAR>h : ∀ (g : G), g ^ 2 = 1<GOAL>a * (a * b) * b = a * (b * a) * b
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m n₁ n₂ n₁₂ : ℤ<VAR>z₁ : Cochain F G n₁<VAR>k : R<VAR>z₂ : Cochain G K n₂<VAR>h : n₁ + n₂ = n₁₂<VAR>p q : ℤ<VAR>hpq : p + n₁₂ = q<GOAL>(z₁.comp (k • z₂) h).v p q hpq = (k • z₁.comp z₂ h).v p q hpq
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : Mul α<VAR>inst✝² : Mul β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : MulHomClass F α β<VAR>m : F<VAR>s✝ t✝ : Set α<VAR>hm : Injective ⇑m<VAR>s t : Set β<VAR>hs : s ⊆ range ⇑m<VAR>ht : t ⊆ range ⇑m<GOAL>⇑m '' (⇑m ⁻¹' (s * t)) = ⇑m '' (⇑m ⁻¹' s * ⇑m ⁻¹' t)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>l : List ℕ<GOAL>l.ranges.join = range l.sum
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>c : 𝕜 → 𝕜<VAR>h : E → 𝕜<VAR>c' : 𝕜<VAR>z : E<VAR>S : Set E<VAR>hc : HasDerivWithinAt c c' s x<VAR>hx : c x ≠ 0<GOAL>HasDerivWithinAt (fun y => (c y)⁻¹) (-c' / c x ^ 2) s x
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>c : 𝕜 → 𝕜<VAR>h : E → 𝕜<VAR>c' : 𝕜<VAR>z : E<VAR>S : Set E<VAR>hc : HasDerivWithinAt c c' s x<VAR>hx : c x ≠ 0<GOAL>-c' / c x ^ 2 = -(c x ^ 2)⁻¹ * c'
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>N' : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R N'<VAR>g : N →ₗ[R] N'<VAR>f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N<VAR>v : ExteriorAlgebra R M<GOAL>(liftAlternating fun i => g.compAlternatingMap (f i)) v = (g ∘ₗ liftAlternating f) v
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>N' : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R N'<VAR>g : N →ₗ[R] N'<VAR>f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N<VAR>v : ExteriorAlgebra R M<GOAL>(liftAlternating fun i => g.compAlternatingMap (f i)) v = g ((liftAlternating f) v)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>N' : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R N'<VAR>g : N →ₗ[R] N'<VAR>r : R<VAR>f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N<GOAL>(liftAlternating fun i => g.compAlternatingMap (f i)) ((algebraMap R (CliffordAlgebra 0)) r) = g ((liftAlternating f) ((algebraMap R (CliffordAlgebra 0)) r))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>N' : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R N'<VAR>g : N →ₗ[R] N'<VAR>x y : CliffordAlgebra 0<VAR>hx : ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N), (liftAlternating fun i => g.compAlternatingMap (f i)) x = g ((liftAlternating f) x)<VAR>hy : ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N), (liftAlternating fun i => g.compAlternatingMap (f i)) y = g ((liftAlternating f) y)<VAR>f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N<GOAL>(liftAlternating fun i => g.compAlternatingMap (f i)) (x + y) = g ((liftAlternating f) (x + y))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>N' : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R N'<VAR>g : N →ₗ[R] N'<VAR>x : CliffordAlgebra 0<VAR>m : M<VAR>hx : ∀ (f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N), (liftAlternating fun i => g.compAlternatingMap (f i)) x = g ((liftAlternating f) x)<VAR>f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N<GOAL>(liftAlternating fun i => g.compAlternatingMap (f i)) ((CliffordAlgebra.ι 0) m * x) = g ((liftAlternating f) ((CliffordAlgebra.ι 0) m * x))
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Semiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module Rᵐᵒᵖ M<VAR>r : R<VAR>m : M<GOAL>r •> m + 0 •> 0 = r •> m
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>d d' : Module.Dual R M<VAR>x : CliffordAlgebra Q<GOAL>(contractLeft d) ((contractLeft d) x) = 0
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>d d' : Module.Dual R M<VAR>r : R<GOAL>(contractLeft d) ((contractLeft d) ((algebraMap R (CliffordAlgebra Q)) r)) = 0
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>d d' : Module.Dual R M<VAR>x y : CliffordAlgebra Q<VAR>hx : (contractLeft d) ((contractLeft d) x) = 0<VAR>hy : (contractLeft d) ((contractLeft d) y) = 0<GOAL>(contractLeft d) ((contractLeft d) (x + y)) = 0
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>d d' : Module.Dual R M<VAR>m : CliffordAlgebra Q<VAR>x : M<VAR>hx : (contractLeft d) ((contractLeft d) m) = 0<GOAL>(contractLeft d) ((contractLeft d) ((ι Q) x * m)) = 0