ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>E : ι → Type u_2<VAR>inst✝ : (i : ι) → MetricSpace (E i)<VAR>i j : ι<VAR>h : i ≠ j<VAR>x : E i<VAR>y : E j<GOAL>1 ≤ dist x ⋯.some + 1 + dist ⋯.some y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a✝ b✝ c d a b : α<VAR>h : Disjoint a b<GOAL>a ∆ b = a ⊔ b
<VAR>α : Type u_1<VAR>inst✝ : EMetricSpace α<VAR>cs : CompleteSpace α<VAR>K : ℝ≥0<VAR>f : α → α<GOAL>¬1 - ↑K = ⊤
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>S✝ : Type u_3<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : Semiring S✝<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M₂<VAR>inst✝⁹ : AddCommMonoid M₃<VAR>inst✝⁸ : AddCommMonoid M₄<VAR>inst✝⁷ : AddCommMonoid M₅<VAR>inst✝⁶ : AddCommMonoid M₆<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M₄<VAR>inst✝¹ : Module R M₅<VAR>inst✝ : Module R M₆<VAR>f✝ : M →ₗ[R] M₂<VAR>f : M →ₗ[R] M₃<VAR>g : M₂ →ₗ[R] M₃<VAR>S : Submodule R M<VAR>S' : Submodule R M₂<GOAL>↑(Submodule.map (f.coprod g) (S.prod S')) = ↑(Submodule.map f S ⊔ Submodule.map g S')
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>S✝ : Type u_3<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : Semiring S✝<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M₂<VAR>inst✝⁹ : AddCommMonoid M₃<VAR>inst✝⁸ : AddCommMonoid M₄<VAR>inst✝⁷ : AddCommMonoid M₅<VAR>inst✝⁶ : AddCommMonoid M₆<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M₄<VAR>inst✝¹ : Module R M₅<VAR>inst✝ : Module R M₆<VAR>f✝ : M →ₗ[R] M₂<VAR>f : M →ₗ[R] M₃<VAR>g : M₂ →ₗ[R] M₃<VAR>S : Submodule R M<VAR>S' : Submodule R M₂<GOAL>(fun a => f a.1 + g a.2) '' ↑(S.prod S') = ⇑f '' ↑S + ⇑g '' ↑S'
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>S✝ : Type u_3<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : Semiring S✝<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M₂<VAR>inst✝⁹ : AddCommMonoid M₃<VAR>inst✝⁸ : AddCommMonoid M₄<VAR>inst✝⁷ : AddCommMonoid M₅<VAR>inst✝⁶ : AddCommMonoid M₆<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module R M₃<VAR>inst✝² : Module R M₄<VAR>inst✝¹ : Module R M₅<VAR>inst✝ : Module R M₆<VAR>f✝ : M →ₗ[R] M₂<VAR>f : M →ₗ[R] M₃<VAR>g : M₂ →ₗ[R] M₃<VAR>S : Submodule R M<VAR>S' : Submodule R M₂<GOAL>(fun a => f a.1 + g a.2) '' ↑(S.prod S') = Set.image2 (fun a b => f a + g b) ↑S ↑S'
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>P : R[X]<VAR>x : S<VAR>h : (aeval x) P = 0<GOAL>IsFixedPt P.newtonMap x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>x : α<GOAL>x - 1 / 2 < ↑(round x)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>x : α<GOAL>x + 1 / 2 - 1 < ↑⌊x + 1 / 2⌋
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIcoMod hp a (b + p) = toIcoMod hp a b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a✝ b✝ c d a b : α<VAR>h : a ≤ b<GOAL>a ⇔ b = b ⇨ a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝ : CommRing A<GOAL>(rescale (-1)) X = -X
<VAR>x✝ y x : ℝ<GOAL>cosh x ^ 2 - sinh x ^ 2 = 1
<VAR>x✝ y x : ℝ<GOAL>↑(cosh x ^ 2 - sinh x ^ 2) = ↑1
<VAR>R : Type u<VAR>inst✝⁸ : Ring R<VAR>ι : Type v<VAR>inst✝⁷ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁶ : (i : ι) → AddCommGroup (G i)<VAR>inst✝⁵ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝⁴ : DecidableEq ι<VAR>P : Type u₁<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>g : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝ : (i : ι) → (k : G i) → Decidable (k ≠ 0)<VAR>x : DirectSum ι G<VAR>i j : ι<VAR>hij : i ≤ j<VAR>hx : ∀ k ∈ DFinsupp.support x, k ≤ i<GOAL>(DirectSum.toModule R ι (G j) fun k => totalize G f k j) x = (f i j hij) ((DirectSum.toModule R ι (G i) fun k => totalize G f k i) x)
<VAR>R : Type u<VAR>inst✝⁸ : Ring R<VAR>ι : Type v<VAR>inst✝⁷ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁶ : (i : ι) → AddCommGroup (G i)<VAR>inst✝⁵ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝⁴ : DecidableEq ι<VAR>P : Type u₁<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>g : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝ : (i : ι) → (k : G i) → Decidable (k ≠ 0)<VAR>x : DirectSum ι G<VAR>i j : ι<VAR>hij : i ≤ j<VAR>hx : ∀ k ∈ DFinsupp.support x, k ≤ i<GOAL>(DirectSum.toModule R ι (G j) fun k => totalize G f k j) (DFinsupp.sum x DFinsupp.single) = (f i j hij) ((DirectSum.toModule R ι (G i) fun k => totalize G f k i) (DFinsupp.sum x DFinsupp.single))
<VAR>R : Type u<VAR>inst✝⁸ : Ring R<VAR>ι : Type v<VAR>inst✝⁷ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁶ : (i : ι) → AddCommGroup (G i)<VAR>inst✝⁵ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝⁴ : DecidableEq ι<VAR>P : Type u₁<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>g : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝ : (i : ι) → (k : G i) → Decidable (k ≠ 0)<VAR>x : DirectSum ι G<VAR>i j : ι<VAR>hij : i ≤ j<VAR>hx : ∀ k ∈ DFinsupp.support x, k ≤ i<GOAL>(DirectSum.toModule R ι (G j) fun k => totalize G f k j) (∑ i ∈ DFinsupp.support x, DFinsupp.single i (x i)) = (f i j hij) ((DirectSum.toModule R ι (G i) fun k => totalize G f k i) (∑ i ∈ DFinsupp.support x, DFinsupp.single i (x i)))
<VAR>R : Type u<VAR>inst✝⁸ : Ring R<VAR>ι : Type v<VAR>inst✝⁷ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁶ : (i : ι) → AddCommGroup (G i)<VAR>inst✝⁵ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝⁴ : DecidableEq ι<VAR>P : Type u₁<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>g : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝ : (i : ι) → (k : G i) → Decidable (k ≠ 0)<VAR>x : DirectSum ι G<VAR>i j : ι<VAR>hij : i ≤ j<VAR>hx : ∀ k ∈ DFinsupp.support x, k ≤ i<GOAL>∑ x_1 ∈ DFinsupp.support x, (DirectSum.toModule R ι (G j) fun k => totalize G f k j) (DFinsupp.single x_1 (x x_1)) = ∑ x_1 ∈ DFinsupp.support x, (f i j hij) ((DirectSum.toModule R ι (G i) fun k => totalize G f k i) (DFinsupp.single x_1 (x x_1)))
<VAR>R : Type u<VAR>inst✝⁸ : Ring R<VAR>ι : Type v<VAR>inst✝⁷ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝⁶ : (i : ι) → AddCommGroup (G i)<VAR>inst✝⁵ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝⁴ : DecidableEq ι<VAR>P : Type u₁<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>g : (i : ι) → G i →ₗ[R] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝¹ : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝ : (i : ι) → (k : G i) → Decidable (k ≠ 0)<VAR>x : DirectSum ι G<VAR>i j : ι<VAR>hij : i ≤ j<VAR>hx : ∀ k ∈ DFinsupp.support x, k ≤ i<VAR>k : ι<VAR>hk : k ∈ DFinsupp.support x<GOAL>(DirectSum.toModule R ι (G j) fun k => totalize G f k j) (DFinsupp.single k (x k)) = (f i j hij) ((DirectSum.toModule R ι (G i) fun k => totalize G f k i) (DFinsupp.single k (x k)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>fa : α → α<VAR>fb : β → β<VAR>f : α → β<VAR>g : β → γ<VAR>s t : Set α<VAR>h : Semiconj f fa fb<VAR>ha : InjOn fa s<VAR>hf : InjOn f (fa '' s)<VAR>x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>hy : y ∈ s<VAR>H : fb (f x) = fb (f y)<GOAL>f x = f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>fa : α → α<VAR>fb : β → β<VAR>f : α → β<VAR>g : β → γ<VAR>s t : Set α<VAR>h : Semiconj f fa fb<VAR>ha : InjOn fa s<VAR>hf : InjOn f (fa '' s)<VAR>x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>hy : y ∈ s<VAR>H : f (fa x) = f (fa y)<GOAL>f x = f y
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : DecidableEq β<VAR>s : Finset α<VAR>f : α → Multiset β<VAR>b : β<VAR>this : DecidableEq α := Classical.decEq α<GOAL>count b (s.sup f) = s.sup fun a => count b (f a)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : DecidableEq β<VAR>s : Finset α<VAR>f : α → Multiset β<VAR>b : β<VAR>this : DecidableEq α := Classical.decEq α<GOAL>count b (∅.sup f) = ∅.sup fun a => count b (f a)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : DecidableEq β<VAR>s : Finset α<VAR>f : α → Multiset β<VAR>b : β<VAR>this : DecidableEq α := Classical.decEq α<GOAL>∀ ⦃a : α⦄ {s : Finset α}, a ∉ s → (count b (s.sup f) = s.sup fun a => count b (f a)) → count b ((insert a s).sup f) = (insert a s).sup fun a => count b (f a)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : IsAlgClosed k<VAR>a₁ a₂ : 𝕎 k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>ha₂ : a₂.coeff 0 ≠ 0<VAR>h : frobeniusRotation p ha₁ ha₂ = 0<GOAL>False
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>inst✝¹ : CharP k p<VAR>inst✝ : IsAlgClosed k<VAR>a₁ a₂ : 𝕎 k<VAR>ha₁ : a₁.coeff 0 ≠ 0<VAR>ha₂ : a₂.coeff 0 ≠ 0<VAR>h : frobeniusRotation p ha₁ ha₂ = 0<GOAL>solution p a₁ a₂ = 0
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>r s t r' s' t' : R<VAR>h : r ≠ 0<GOAL>(if _hr : r = 0 then (r', s', t') else let q := r' / r; let_fun x := ⋯; xgcdAux (r' % r) (s' - q * s) (t' - q * t) r s t) = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>β' : Type u_5<VAR>γ : Type u_6<VAR>γ' : Type u_7<VAR>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>q : Type u_12<VAR>r : Type u_13<VAR>l' : Type u_14<VAR>m' : Type u_15<VAR>n' : Type u_16<VAR>p' : Type u_17<VAR>inst✝⁷ : Zero α<VAR>inst✝⁶ : Zero β<VAR>inst✝⁵ : Zero γ<VAR>inst✝⁴ : One α<VAR>inst✝³ : One β<VAR>inst✝² : One γ<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : DecidableEq n<VAR>f : α → β → γ<VAR>hf₁ : ∀ (b : β), f 0 b = 0<VAR>hf₂ : ∀ (a : α), f a 0 = 0<VAR>hf₃ : f 1 1 = 1<GOAL>(diagonal fun mn => f 1 1) = 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>inst✝¹ : IsModularLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>s : Set ι<VAR>f : ι → α<VAR>h : ∀ i ∈ s, ComplementedLattice ↑(Iic (f i))<VAR>h' : ⨆ i ∈ s, f i = ⊤<GOAL>ComplementedLattice α
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>inst✝¹ : IsModularLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>s : Set ι<VAR>f : ι → α<VAR>h : ∀ i ∈ s, ComplementedLattice ↑(Iic (f i))<VAR>h' : ⨆ i ∈ s, f i = ⊤<GOAL>sSup {a | IsAtom a} = ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>inst✝¹ : IsModularLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>s : Set ι<VAR>f : ι → α<VAR>h : ∀ i ∈ s, ComplementedLattice ↑(Iic (f i))<VAR>h' : ⨆ i ∈ s, f i = ⊤<VAR>t : (i : ι) → i ∈ s → Set α<VAR>ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a)<VAR>ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1<VAR>u : Set α := ⋃ i, ⋃ (hi : i ∈ s), t i hi<VAR>hu₁ : u ⊆ {a | IsAtom a}<GOAL>sSup {a | IsAtom a} = ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>inst✝¹ : IsModularLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>s : Set ι<VAR>f : ι → α<VAR>h : ∀ i ∈ s, ComplementedLattice ↑(Iic (f i))<VAR>h' : ⨆ i ∈ s, f i = ⊤<VAR>t : (i : ι) → i ∈ s → Set α<VAR>ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a)<VAR>ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1<VAR>u : Set α := ⋃ i, ⋃ (hi : i ∈ s), t i hi<VAR>hu₁ : u ⊆ {a | IsAtom a}<VAR>hu₂ : sSup u = ⨆ i ∈ s, f i<GOAL>sSup {a | IsAtom a} = ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>inst✝¹ : IsModularLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>s : Set ι<VAR>f : ι → α<VAR>h : ∀ i ∈ s, ComplementedLattice ↑(Iic (f i))<VAR>h' : ⨆ i ∈ s, f i = ⊤<VAR>t : (i : ι) → i ∈ s → Set α<VAR>ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a)<VAR>ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1<VAR>u : Set α := ⋃ i, ⋃ (hi : i ∈ s), t i hi<VAR>hu₁ : u ⊆ {a | IsAtom a}<VAR>hu₂ : sSup u = ⨆ i ∈ s, f i<GOAL>sSup u ≤ sSup {a | IsAtom a}
<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✝⁵ : SeminormedCommRing 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝⁴ : RingHomIsometric σ₁₂<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜₂ E₂<VAR>p : Seminorm 𝕜₂ E₂<VAR>f : E →ₛₗ[σ₁₂] E₂<VAR>c : 𝕜₂<VAR>x✝ : E<GOAL>(p.comp (c • f)) x✝ = (‖c‖₊ • p.comp f) x✝
<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>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : Monoid P<VAR>l l₁ l₂ : List M<VAR>a✝ x : M<VAR>xs : List M<VAR>i : ℕ<VAR>a : M<GOAL>((x :: xs).set (i + 1) a).prod = ((take (i + 1) (x :: xs)).prod * if i + 1 < (x :: xs).length then a else 1) * (drop (i + 1 + 1) (x :: xs)).prod
<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>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : Monoid P<VAR>l l₁ l₂ : List M<VAR>a : M<VAR>x✝¹ : ℕ<VAR>x✝ : M<GOAL>([].set x✝¹ x✝).prod = ((take x✝¹ []).prod * if x✝¹ < [].length then x✝ else 1) * (drop (x✝¹ + 1) []).prod
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ε : Type u_6<VAR>inst✝ : Monoid α<VAR>f g : Filter α<VAR>s : Set α<VAR>a : α<VAR>m n : ℕ<VAR>hf : 1 ≤ f<GOAL>f * ⊤ = ⊤
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ε : Type u_6<VAR>inst✝ : Monoid α<VAR>f g : Filter α<VAR>s✝ : Set α<VAR>a : α<VAR>m n : ℕ<VAR>hf : 1 ≤ f<VAR>s : Set α<GOAL>s ∈ f * ⊤ → s ∈ ⊤
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ε : Type u_6<VAR>inst✝ : Monoid α<VAR>f g : Filter α<VAR>s✝ : Set α<VAR>a : α<VAR>m n : ℕ<VAR>hf : 1 ≤ f<VAR>s : Set α<GOAL>(∃ t₁ ∈ f, t₁ * univ ⊆ s) → s = univ
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ε : Type u_6<VAR>inst✝ : Monoid α<VAR>f g : Filter α<VAR>s✝ : Set α<VAR>a : α<VAR>m n : ℕ<VAR>hf : 1 ≤ f<VAR>s t : Set α<VAR>ht : t ∈ f<VAR>hs : t * univ ⊆ s<GOAL>s = univ
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : NoZeroDivisors R<VAR>p : ℕ<VAR>hp : CharP R p<VAR>p_ne_zero : p ≠ 0<GOAL>Nat.Prime p
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : NoZeroDivisors R<VAR>p : ℕ<VAR>hp : CharP R p<VAR>p_ne_zero : p ≠ 0<VAR>h : Nat.Prime p<GOAL>Nat.Prime p
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : NoZeroDivisors R<VAR>p : ℕ<VAR>hp : CharP R p<VAR>p_ne_zero : p ≠ 0<VAR>h : p = 0<GOAL>Nat.Prime p
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>p q : ℕ<VAR>cardα : Fintype.card α = p<VAR>cardβ : Fintype.card β = q<VAR>h0p : 0 < p<VAR>hpq : p < q<VAR>x : β × (K →+* ℂ) → ℤ<VAR>hxl : x ≠ 0<VAR>hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0<VAR>hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))<VAR>H : NumberField.house.ξ K x = 0<VAR>l : β<VAR>r : K →+* ℂ<GOAL>x (l, r) = 0 (l, r)
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>p q : ℕ<VAR>cardα : Fintype.card α = p<VAR>cardβ : Fintype.card β = q<VAR>h0p : 0 < p<VAR>hpq : p < q<VAR>x : β × (K →+* ℂ) → ℤ<VAR>hxl : x ≠ 0<VAR>hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0<VAR>hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))<VAR>H : ∀ (a : β), NumberField.house.ξ K x a = 0 a<VAR>l : β<VAR>r : K →+* ℂ<GOAL>x (l, r) = 0 (l, r)
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>p q : ℕ<VAR>cardα : Fintype.card α = p<VAR>cardβ : Fintype.card β = q<VAR>h0p : 0 < p<VAR>hpq : p < q<VAR>x : β × (K →+* ℂ) → ℤ<VAR>hxl : x ≠ 0<VAR>hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0<VAR>hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))<VAR>H : ∀ (a : β), NumberField.house.ξ K x a = 0 a<VAR>l : β<VAR>r : K →+* ℂ<VAR>hblin : LinearIndependent ℤ ⇑(NumberField.house.newBasis K)<GOAL>x (l, r) = 0 (l, r)
<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>inst✝² : DecidableEq (K →+* ℂ)<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>a : Matrix α β (𝓞 K)<VAR>ha : a ≠ 0<VAR>p q : ℕ<VAR>cardα : Fintype.card α = p<VAR>cardβ : Fintype.card β = q<VAR>h0p : 0 < p<VAR>hpq : p < q<VAR>x : β × (K →+* ℂ) → ℤ<VAR>hxl : x ≠ 0<VAR>hmulvec0 : NumberField.house.asiegel K a *ᵥ x = 0<VAR>hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖NumberField.house.asiegel K a‖) ^ (↑p / (↑q - ↑p))<VAR>H : ∀ (a : β), NumberField.house.ξ K x a = 0 a<VAR>l : β<VAR>r : K →+* ℂ<VAR>hblin : ∀ (g : (K →+* ℂ) → ℤ), ∑ x : K →+* ℂ, ↑(g x) * (NumberField.house.newBasis K) x = 0 → ∀ (i : K →+* ℂ), g i = 0<GOAL>x (l, r) = 0 (l, r)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>h : HasMFDerivWithinAt I I' f s x f'<VAR>hxs : UniqueMDiffWithinAt I s x<VAR>x✝ : TangentSpace I x<GOAL>(_root_.mfderivWithin I I' f s x) x✝ = f' x✝
<VAR>s : ℝ<VAR>hs : s ≠ 0<GOAL>(Complex.Gamma ↑(s + 1)).re = s * (Complex.Gamma ↑s).re
<VAR>s : ℝ<VAR>hs : s ≠ 0<GOAL>↑s ≠ 0
<VAR>α : Type u<VAR>inst✝¹ : CanonicallyOrderedCommMonoid α<VAR>a b c d : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<GOAL>a < b ↔ ∃ c, c > 1 ∧ b = a * c
<VAR>α : Type u<VAR>inst✝¹ : CanonicallyOrderedCommMonoid α<VAR>a b c d : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<GOAL>(∃ x, b = a * x ∧ a ≠ b) ↔ ∃ c, c > 1 ∧ b = a * c
<VAR>α : Type u<VAR>inst✝¹ : CanonicallyOrderedCommMonoid α<VAR>a b c d : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<GOAL>∀ (a_1 : α), b = a * a_1 ∧ a ≠ b ↔ a_1 > 1 ∧ b = a * a_1
<VAR>α : Type u<VAR>inst✝¹ : CanonicallyOrderedCommMonoid α<VAR>a b c✝ d : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>c : α<GOAL>b = a * c ∧ a ≠ b ↔ c > 1 ∧ b = a * c
<VAR>α : Type u<VAR>inst✝¹ : CanonicallyOrderedCommMonoid α<VAR>a b c✝ d : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>c : α<GOAL>b = a * c → (a ≠ b ↔ 1 < c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_4}<VAR>h : o.IsLimit<GOAL>1 < o
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>γ : Type w<VAR>inst✝ : EMetricSpace γ<VAR>x y : γ<GOAL>0 < edist x y ↔ x ≠ y
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>a✝ : ℕ<GOAL>a✝ ∈ f.integralNormalization.support → a✝ ∈ f.support
<VAR>n✝ : ℕ<VAR>i j : Fin (n✝ + 1)<GOAL>i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ
<VAR>n✝ : ℕ<VAR>i j : Fin (n✝ + 1)<VAR>hlt : j < i<GOAL>i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ
<VAR>n✝ : ℕ<VAR>i j : Fin (n✝ + 1)<VAR>heq : j = i<GOAL>i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ
<VAR>n✝ : ℕ<VAR>i j : Fin (n✝ + 1)<VAR>hgt : i < j<GOAL>i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>Φ : LinearMap.BilinForm R M<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>N : LieSubmodule R L M<VAR>x : L<VAR>y : M<GOAL>y ∈ __spread✝⁻⁰.carrier → ⁅x, y⁆ ∈ __spread✝⁻⁰.carrier
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>Φ : LinearMap.BilinForm R M<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>N : LieSubmodule R L M<VAR>x : L<VAR>y : M<GOAL>(∀ n ∈ N, (Φ n) y = 0) → ∀ n ∈ N, (Φ n) ⁅x, y⁆ = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>Φ : LinearMap.BilinForm R M<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>N : LieSubmodule R L M<VAR>x : L<VAR>y : M<VAR>H : ∀ n ∈ N, (Φ n) y = 0<VAR>a : M<VAR>ha : a ∈ N<GOAL>(Φ a) ⁅x, y⁆ = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>Φ : LinearMap.BilinForm R M<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>N : LieSubmodule R L M<VAR>x : L<VAR>y : M<VAR>H : ∀ n ∈ N, (Φ n) y = 0<VAR>a : M<VAR>ha : a ∈ N<GOAL>(Φ ⁅x, a⁆) y = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>N : Type u_9<VAR>N₂ : Type u_10<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : CommSemiring R₂<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R₂ M₂<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : AddCommMonoid N₂<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R N₂<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₁ : R₂ →+* R<VAR>inst✝¹ : RingHomInvPair τ₁₂ τ₂₁<VAR>inst✝ : RingHomInvPair τ₂₁ τ₁₂<VAR>p : Submodule R M<VAR>q : Submodule R₂ M₂<VAR>pₗ : Submodule R N<VAR>qₗ : Submodule R N₂<VAR>fₗ : N →ₗ[R] N₂<VAR>c : R<GOAL>comap fₗ qₗ ≤ comap (c • fₗ) qₗ