ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>T : Type u_3<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<VAR>hg : g.SurjectiveOnStalks<VAR>hf : f.SurjectiveOnStalks<VAR>I : Ideal T<VAR>hI : I.IsPrime<VAR>this : Function.Surjective (⇑(Localization.localRingHom (Ideal.comap g I) I g ⋯) ∘ ⇑(Localization.localRingHom (Ideal.comap f (Ideal.comap g I)) (Ideal.comap g I) f ⋯))<GOAL>Function.Surjective ⇑(Localization.localRingHom (Ideal.comap (g.comp f) I) I (g.comp f) ⋯)
<VAR>M G : Type u<VAR>inst✝¹ : Monoid M<VAR>inst✝ : Group G<VAR>x y : SingleObj G<VAR>f : x ⟶ y<GOAL>inv f = f⁻¹
<VAR>M G : Type u<VAR>inst✝¹ : Monoid M<VAR>inst✝ : Group G<VAR>x y : SingleObj G<VAR>f : x ⟶ y<GOAL>f ≫ f⁻¹ = 𝟙 x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : AddCommMonoid N<VAR>n : ℕ<VAR>f : ℕ × ℕ → M<GOAL>∏ p ∈ antidiagonal (n + 1), f p = f (n + 1, 0) * ∏ p ∈ antidiagonal n, f (p.1, p.2 + 1)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : AddCommMonoid N<VAR>n : ℕ<VAR>f : ℕ × ℕ → M<GOAL>f (0, n + 1).swap * ∏ p ∈ antidiagonal n, f (p.swap.1 + 1, p.swap.2).swap = f (n + 1, 0) * ∏ p ∈ antidiagonal n, f (p.1, p.2 + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>h : HasFiniteIntegral f μ<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<GOAL>HasFiniteIntegral f (c • μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>h : ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<GOAL>c * ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c : α<VAR>h : a ⋖ b<GOAL>Ico a b = {a}
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>M : (i : ι) → Matroid (α i)<VAR>I X : Set ((i : ι) × α i)<GOAL>(Matroid.sigma M).Basis I X ↔ ∀ (i : ι), (M i).Basis (Sigma.mk i ⁻¹' I) (Sigma.mk i ⁻¹' X)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>M : (i : ι) → Matroid (α i)<VAR>I X : Set ((i : ι) × α i)<GOAL>(∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) → ((I ⊆ X ∧ (∀ ⦃y : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' y)) → y ⊆ X → I ⊆ y → I = y) ∧ X ⊆ univ.sigma fun i => (M i).E) ↔ (∀ (x : ι), Sigma.mk x ⁻¹' I ⊆ Sigma.mk x ⁻¹' X) ∧ (∀ (x : ι) ⦃y : Set (α x)⦄, (M x).Indep y → y ⊆ Sigma.mk x ⁻¹' X → Sigma.mk x ⁻¹' I ⊆ y → Sigma.mk x ⁻¹' I = y) ∧ ∀ (x : ι), Sigma.mk x ⁻¹' X ⊆ (M x).E)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>M : (i : ι) → Matroid (α i)<VAR>I X : Set ((i : ι) × α i)<VAR>hI : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)<VAR>x✝ : I ⊆ X ∧ (∀ ⦃y : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' y)) → y ⊆ X → I ⊆ y → I = y) ∧ X ⊆ univ.sigma fun i => (M i).E<VAR>hIX : I ⊆ X<VAR>h : ∀ ⦃y : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' y)) → y ⊆ X → I ⊆ y → I = y<VAR>h' : X ⊆ univ.sigma fun i => (M i).E<VAR>i : ι<VAR>I₀ : Set (α i)<VAR>hI₀ : (M i).Indep I₀<VAR>hI₀X : I₀ ⊆ Sigma.mk i ⁻¹' X<VAR>hII₀ : Sigma.mk i ⁻¹' I ⊆ I₀<GOAL>Sigma.mk i ⁻¹' I = I₀
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>M : (i : ι) → Matroid (α i)<VAR>I X : Set ((i : ι) × α i)<VAR>hI : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)<VAR>x✝ : I ⊆ X ∧ (∀ ⦃y : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' y)) → y ⊆ X → I ⊆ y → I = y) ∧ X ⊆ univ.sigma fun i => (M i).E<VAR>hIX : I ⊆ X<VAR>h : ∀ ⦃y : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' y)) → y ⊆ X → I ⊆ y → I = y<VAR>h' : X ⊆ univ.sigma fun i => (M i).E<GOAL>∀ (x : ι), Sigma.mk x ⁻¹' X ⊆ (M x).E
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>M : (i : ι) → Matroid (α i)<VAR>I X : Set ((i : ι) × α i)<VAR>hI : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)<VAR>x✝ : (∀ (x : ι), Sigma.mk x ⁻¹' I ⊆ Sigma.mk x ⁻¹' X) ∧ (∀ (x : ι) ⦃y : Set (α x)⦄, (M x).Indep y → y ⊆ Sigma.mk x ⁻¹' X → Sigma.mk x ⁻¹' I ⊆ y → Sigma.mk x ⁻¹' I = y) ∧ ∀ (x : ι), Sigma.mk x ⁻¹' X ⊆ (M x).E<VAR>hIX : ∀ (x : ι), Sigma.mk x ⁻¹' I ⊆ Sigma.mk x ⁻¹' X<VAR>h' : ∀ (x : ι) ⦃y : Set (α x)⦄, (M x).Indep y → y ⊆ Sigma.mk x ⁻¹' X → Sigma.mk x ⁻¹' I ⊆ y → Sigma.mk x ⁻¹' I = y<VAR>h'' : ∀ (x : ι), Sigma.mk x ⁻¹' X ⊆ (M x).E<GOAL>I ⊆ X
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>M : (i : ι) → Matroid (α i)<VAR>I X : Set ((i : ι) × α i)<VAR>hI : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)<VAR>x✝ : (∀ (x : ι), Sigma.mk x ⁻¹' I ⊆ Sigma.mk x ⁻¹' X) ∧ (∀ (x : ι) ⦃y : Set (α x)⦄, (M x).Indep y → y ⊆ Sigma.mk x ⁻¹' X → Sigma.mk x ⁻¹' I ⊆ y → Sigma.mk x ⁻¹' I = y) ∧ ∀ (x : ι), Sigma.mk x ⁻¹' X ⊆ (M x).E<VAR>hIX : ∀ (x : ι), Sigma.mk x ⁻¹' I ⊆ Sigma.mk x ⁻¹' X<VAR>h' : ∀ (x : ι) ⦃y : Set (α x)⦄, (M x).Indep y → y ⊆ Sigma.mk x ⁻¹' X → Sigma.mk x ⁻¹' I ⊆ y → Sigma.mk x ⁻¹' I = y<VAR>h'' : ∀ (x : ι), Sigma.mk x ⁻¹' X ⊆ (M x).E<GOAL>∀ ⦃y : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' y)) → y ⊆ X → I ⊆ y → I = y
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>M : (i : ι) → Matroid (α i)<VAR>I X : Set ((i : ι) × α i)<VAR>hI : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)<VAR>x✝ : (∀ (x : ι), Sigma.mk x ⁻¹' I ⊆ Sigma.mk x ⁻¹' X) ∧ (∀ (x : ι) ⦃y : Set (α x)⦄, (M x).Indep y → y ⊆ Sigma.mk x ⁻¹' X → Sigma.mk x ⁻¹' I ⊆ y → Sigma.mk x ⁻¹' I = y) ∧ ∀ (x : ι), Sigma.mk x ⁻¹' X ⊆ (M x).E<VAR>hIX : ∀ (x : ι), Sigma.mk x ⁻¹' I ⊆ Sigma.mk x ⁻¹' X<VAR>h' : ∀ (x : ι) ⦃y : Set (α x)⦄, (M x).Indep y → y ⊆ Sigma.mk x ⁻¹' X → Sigma.mk x ⁻¹' I ⊆ y → Sigma.mk x ⁻¹' I = y<VAR>h'' : ∀ (x : ι), Sigma.mk x ⁻¹' X ⊆ (M x).E<GOAL>X ⊆ univ.sigma fun i => (M i).E
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝² : LinearOrderedSemifield α<VAR>inst✝¹ : Archimedean α<VAR>inst✝ : ExistsAddOfLE α<VAR>x y ε : α<VAR>hx : 0 < x<VAR>hy : 1 < y<VAR>m : ℤ<VAR>hle : y ^ m ≤ x⁻¹<VAR>hlt : x⁻¹ < y ^ (m + 1)<VAR>hyp : 0 < y<GOAL>y ^ (-(m + 1)) < x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝² : LinearOrderedSemifield α<VAR>inst✝¹ : Archimedean α<VAR>inst✝ : ExistsAddOfLE α<VAR>x y ε : α<VAR>hx : 0 < x<VAR>hy : 1 < y<VAR>m : ℤ<VAR>hle : y ^ m ≤ x⁻¹<VAR>hlt : x⁻¹ < y ^ (m + 1)<VAR>hyp : 0 < y<GOAL>x ≤ y ^ (-(m + 1) + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>m : ℕ<VAR>hm : n ≤ m<VAR>i : Fin n<VAR>x : TruncatedWittVector p m R<GOAL>coeff i ((truncate hm) x) = coeff (Fin.castLE hm i) x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>m : ℕ<VAR>hm : n ≤ m<VAR>i : Fin n<VAR>y : 𝕎 R<GOAL>coeff i ((truncate hm) ((WittVector.truncate m) y)) = coeff (Fin.castLE hm i) ((WittVector.truncate m) y)
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<GOAL>(𝓝 ∞).HasBasis (fun s => IsClosed s ∧ IsCompact s) fun s => some '' sᶜ ∪ {∞}
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<GOAL>(map some (coclosedCompact X) ⊔ pure ∞).HasBasis (fun s => IsClosed s ∧ IsCompact s) fun s => some '' sᶜ ∪ {∞}
<VAR>F : Type u_1<VAR>inst✝⁶ : Field F<VAR>E : Type u_2<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>S : Set E<VAR>α : E<VAR>K : Type u_3<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra E K<VAR>inst✝ : IsScalarTower F E K<VAR>L : IntermediateField F K<VAR>halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L<GOAL>Module.rank E ↥(adjoin E ↑L) ≤ Module.rank F ↥L
<VAR>F : Type u_1<VAR>inst✝⁶ : Field F<VAR>E : Type u_2<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>S : Set E<VAR>α : E<VAR>K : Type u_3<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra E K<VAR>inst✝ : IsScalarTower F E K<VAR>L : IntermediateField F K<VAR>halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L<VAR>h : (adjoin E ↑L.toSubalgebra).toSubalgebra = Algebra.adjoin E ↑L.toSubalgebra<GOAL>Module.rank E ↥(adjoin E ↑L) ≤ Module.rank F ↥L
<VAR>F : Type u_1<VAR>inst✝⁶ : Field F<VAR>E : Type u_2<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>S : Set E<VAR>α : E<VAR>K : Type u_3<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra E K<VAR>inst✝ : IsScalarTower F E K<VAR>L : IntermediateField F K<VAR>halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L<VAR>h : (adjoin E ↑L.toSubalgebra).toSubalgebra = Algebra.adjoin E ↑L.toSubalgebra<VAR>this : Module.rank E ↥(Algebra.adjoin E ↑L.toSubalgebra) ≤ Module.rank F ↥L.toSubalgebra<GOAL>Module.rank E ↥(adjoin E ↑L) ≤ Module.rank F ↥L
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<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>a b : R<VAR>x y : M<VAR>t s : Set M<VAR>h : t ⊆ s<GOAL>(LinearIndependent R fun (x : ↑s) => ↑x) → LinearIndependent R fun (x : ↑t) => ↑x
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<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>a b : R<VAR>x y : M<VAR>t s : Set M<VAR>h : t ⊆ s<GOAL>Disjoint (Finsupp.supported R R s) (LinearMap.ker (Finsupp.total M M R id)) → Disjoint (Finsupp.supported R R t) (LinearMap.ker (Finsupp.total M M R id))
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : DivisionRing R<VAR>p✝ q : R[X]<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Nontrivial S<VAR>f : R →+* S<VAR>p : R[X]<GOAL>(map f p).Monic ↔ p.Monic
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : AddMonoid α<VAR>inst✝ : AddGroup β<VAR>h : Antiperiodic f c<VAR>n : ℕ<GOAL>f (x + n • c) = (-1) ^ n • f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : AddMonoid α<VAR>inst✝ : AddGroup β<VAR>h : Antiperiodic f c<VAR>k : ℕ<GOAL>f (x + (2 * k) • c) = (-1) ^ (2 * k) • f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝¹ : AddMonoid α<VAR>inst✝ : AddGroup β<VAR>h : Antiperiodic f c<VAR>k : ℕ<GOAL>f (x + (2 * k + 1) • c) = (-1) ^ (2 * k + 1) • f x
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c d e : B<GOAL>(λ_ (𝟙 a)).hom = (ρ_ (𝟙 a)).hom
<VAR>n✝ : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>n : ℕ+<VAR>inst✝ : IsDomain B<VAR>h : IsCyclotomicExtension {n} A B<VAR>ζ : B<VAR>hζ : IsPrimitiveRoot ζ ↑n<GOAL>adjoin A {ζ} = ⊤
<VAR>α : Type u_1<VAR>G G' : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>s t u : Finset α<GOAL>↑(Rel.interedges G.Adj (SimpleGraph.badVertices G ε s t) t).card ≤ ↑(SimpleGraph.badVertices G ε s t).card * ↑t.card * (↑(G.edgeDensity s t) - ε)
<VAR>R✝ : Type u_1<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>hR : HasUnitMulPowIrreducibleFactorization R<GOAL>DiscreteValuationRing R
<VAR>R✝ : Type u_1<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>hR : HasUnitMulPowIrreducibleFactorization R<VAR>this : UniqueFactorizationMonoid R := HasUnitMulPowIrreducibleFactorization.toUniqueFactorizationMonoid hR<GOAL>DiscreteValuationRing R
<VAR>R✝ : Type u_1<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>hR : HasUnitMulPowIrreducibleFactorization R<VAR>this : UniqueFactorizationMonoid R := HasUnitMulPowIrreducibleFactorization.toUniqueFactorizationMonoid hR<GOAL>∃ p, Irreducible p
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v, u'} D<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : HasFiniteProducts D<VAR>F : C ⥤ D<VAR>L : D ⥤ C<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : CartesianClosed D<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>h : L ⊣ F<VAR>A : C<VAR>i : IsIso (frobeniusMorphism F h A)<GOAL>IsIso (expComparison F A)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v, u'} D<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : HasFiniteProducts D<VAR>F : C ⥤ D<VAR>L : D ⥤ C<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : CartesianClosed D<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>h : L ⊣ F<VAR>A : C<VAR>i : IsIso (frobeniusMorphism F h A)<GOAL>IsIso ((conjugateEquiv (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h)) (frobeniusMorphism F h A))
<VAR>n : ℕ<VAR>i : Fin n<VAR>M : Type u_1<VAR>inst✝ : Zero M<VAR>y : M<VAR>t : Fin (n + 1) →₀ M<VAR>s : Fin n →₀ M<VAR>k : Fin n<GOAL>(cons y s).tail k = s k
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>X Y X' Y' : C<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>f : X ≅ Y<VAR>g : X' ≅ Y'<GOAL>(f.hom ⊗ g.hom) ≫ (f.inv ⊗ g.inv) = 𝟙 (X ⊗ X')
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>X Y X' Y' : C<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>f : X ≅ Y<VAR>g : X' ≅ Y'<GOAL>(f.inv ⊗ g.inv) ≫ (f.hom ⊗ g.hom) = 𝟙 (Y ⊗ Y')
<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>a b : α<VAR>u : αˣ<GOAL>↑u * a ∣ b ↔ a ∣ b
<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>a b : α<VAR>u : αˣ<GOAL>a * ↑u ∣ b ↔ a ∣ b
<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>x✝² x✝¹ : Scheme<VAR>x✝ : x✝² ⟶ x✝¹<GOAL>QuasiSeparated x✝ ↔ MorphismProperty.diagonal (@QuasiCompact) x✝
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>f : J → C<VAR>X Y Z : C<VAR>g h : X ⟶ ((⨁ f) ⊗ Y) ⊗ Z<VAR>w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y ▷ Z = h ≫ biproduct.π f j ▷ Y ▷ Z<GOAL>g = h
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>f : J → C<VAR>X Y Z : C<VAR>g h : X ⟶ ((⨁ f) ⊗ Y) ⊗ Z<VAR>w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y ▷ Z = h ≫ biproduct.π f j ▷ Y ▷ Z<GOAL>g ≫ (α_ (⨁ f) Y Z).hom = h ≫ (α_ (⨁ f) Y Z).hom
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : Semiring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra A B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R A B<VAR>P : R[X]<VAR>a : A<GOAL>eval a (map (algebraMap R A) P) = (aeval a) P
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>M' : Type u_3<VAR>N' : Type u_4<VAR>P : Type u_5<VAR>inst✝⁴ : MulOneClass M<VAR>inst✝³ : MulOneClass N<VAR>inst✝² : MulOneClass M'<VAR>inst✝¹ : MulOneClass N'<VAR>inst✝ : MulOneClass P<GOAL>MonoidHom.mrange inl ⊔ MonoidHom.mrange inr = ⊤
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝¹ : Group α<VAR>inst✝ : AddGroup β<VAR>f : ℤ →+ β<VAR>n : ℤ<GOAL>f n = n • f 1
<VAR>α : Type u_1<VAR>inst✝ : CommSemiring α<VAR>E : LinearRecurrence α<VAR>u : ℕ → α<VAR>init : Fin E.order → α<VAR>h : E.IsSolution u<VAR>heq : ∀ (n : Fin E.order), u ↑n = init n<VAR>n : ℕ<VAR>h' : ¬n < E.order<GOAL>u n = ∑ x : Fin E.order, E.coeffs x * E.mkSol init (n - E.order + ↑x)
<VAR>α : Type u_1<VAR>inst✝ : CommSemiring α<VAR>E : LinearRecurrence α<VAR>u : ℕ → α<VAR>init : Fin E.order → α<VAR>h : E.IsSolution u<VAR>heq : ∀ (n : Fin E.order), u ↑n = init n<VAR>n : ℕ<VAR>h' : ¬n < E.order<GOAL>∑ i : Fin E.order, E.coeffs i * u (n - E.order + ↑i) = ∑ x : Fin E.order, E.coeffs x * E.mkSol init (n - E.order + E.order - E.order + ↑x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>s : Set α<VAR>s_mble : MeasurableSet s<VAR>hsc : count s = 0<GOAL>s = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>s : Set α<VAR>s_mble : MeasurableSet s<VAR>hsc : count s = 0<VAR>hs : s.Finite<GOAL>s = ∅
<VAR>x : EReal<VAR>h : 0 < x<GOAL>⊥ * x = ⊥
<VAR>x : EReal<VAR>h : 0 < x<GOAL>x * ⊥ = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>x : M<VAR>f : Dual R M<VAR>y : M<VAR>g : Dual R M<VAR>inst✝ : NoZeroSMulDivisors ℤ M<VAR>Φ : Set M<VAR>hΦ : Φ.Finite<VAR>hfx : f x = 2<VAR>hgy : g y = 2<VAR>hgx : g x = 2<VAR>hfy : f y = 2<VAR>hxfΦ : MapsTo (⇑(preReflection x f)) Φ Φ<VAR>hygΦ : MapsTo (⇑(preReflection y g)) Φ Φ<VAR>hyΦ : y ∈ Φ<GOAL>x = y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>x : M<VAR>f : Dual R M<VAR>y : M<VAR>g : Dual R M<VAR>inst✝ : NoZeroSMulDivisors ℤ M<VAR>Φ : Set M<VAR>hΦ : _root_.Finite ↑Φ<VAR>hfx : f x = 2<VAR>hgy : g y = 2<VAR>hgx : g x = 2<VAR>hfy : f y = 2<VAR>hxfΦ : MapsTo (⇑(preReflection x f)) Φ Φ<VAR>hygΦ : MapsTo (⇑(preReflection y g)) Φ Φ<VAR>hyΦ : y ∈ Φ<GOAL>x = y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>x : M<VAR>f : Dual R M<VAR>y : M<VAR>g : Dual R M<VAR>inst✝ : NoZeroSMulDivisors ℤ M<VAR>Φ : Set M<VAR>hΦ : _root_.Finite ↑Φ<VAR>hfx : f x = 2<VAR>hgy : g y = 2<VAR>hgx : g x = 2<VAR>hfy : f y = 2<VAR>hxfΦ : MapsTo (⇑(preReflection x f)) Φ Φ<VAR>hygΦ : MapsTo (⇑(preReflection y g)) Φ Φ<VAR>hyΦ : y ∈ Φ<VAR>sxy : M ≃ₗ[R] M := reflection hgy ≪≫ₗ reflection hfx<GOAL>x = y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>x : M<VAR>f : Dual R M<VAR>y : M<VAR>g : Dual R M<VAR>inst✝ : NoZeroSMulDivisors ℤ M<VAR>Φ : Set M<VAR>hΦ : _root_.Finite ↑Φ<VAR>hfx : f x = 2<VAR>hgy : g y = 2<VAR>hgx : g x = 2<VAR>hfy : f y = 2<VAR>hxfΦ : MapsTo (⇑(preReflection x f)) Φ Φ<VAR>hygΦ : MapsTo (⇑(preReflection y g)) Φ Φ<VAR>hyΦ : y ∈ Φ<VAR>sxy : M ≃ₗ[R] M := reflection hgy ≪≫ₗ reflection hfx<VAR>hb : BijOn (⇑sxy) Φ Φ<GOAL>x = y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>x : M<VAR>f : Dual R M<VAR>y : M<VAR>g : Dual R M<VAR>inst✝ : NoZeroSMulDivisors ℤ M<VAR>Φ : Set M<VAR>hΦ : _root_.Finite ↑Φ<VAR>hfx : f x = 2<VAR>hgy : g y = 2<VAR>hgx : g x = 2<VAR>hfy : f y = 2<VAR>hxfΦ : MapsTo (⇑(preReflection x f)) Φ Φ<VAR>hygΦ : MapsTo (⇑(preReflection y g)) Φ Φ<VAR>hyΦ : y ∈ Φ<VAR>sxy : M ≃ₗ[R] M := reflection hgy ≪≫ₗ reflection hfx<VAR>hb : BijOn (⇑sxy) Φ Φ<VAR>hsxy : ∀ (n : ℕ), (⇑sxy)^[n] y = y + (2 * ↑n) • (x - y)<GOAL>x = y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>x : M<VAR>f : Dual R M<VAR>y : M<VAR>g : Dual R M<VAR>inst✝ : NoZeroSMulDivisors ℤ M<VAR>Φ : Set M<VAR>hΦ : _root_.Finite ↑Φ<VAR>hfx : f x = 2<VAR>hgy : g y = 2<VAR>hgx : g x = 2<VAR>hfy : f y = 2<VAR>hxfΦ : MapsTo (⇑(preReflection x f)) Φ Φ<VAR>hygΦ : MapsTo (⇑(preReflection y g)) Φ Φ<VAR>hyΦ : y ∈ Φ<VAR>sxy : M ≃ₗ[R] M := reflection hgy ≪≫ₗ reflection hfx<VAR>hb : BijOn (⇑sxy) Φ Φ<VAR>hsxy : ∀ (n : ℕ), (⇑sxy)^[n] y = y + (2 * ↑n) • (x - y)<VAR>f' : ℕ → ↑Φ := fun n => ⟨(⇑sxy)^[n] y, ⋯⟩<GOAL>x = y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>x : M<VAR>f : Dual R M<VAR>y : M<VAR>g : Dual R M<VAR>inst✝ : NoZeroSMulDivisors ℤ M<VAR>Φ : Set M<VAR>hΦ : _root_.Finite ↑Φ<VAR>hfx : f x = 2<VAR>hgy : g y = 2<VAR>hgx : g x = 2<VAR>hfy : f y = 2<VAR>hxfΦ : MapsTo (⇑(preReflection x f)) Φ Φ<VAR>hygΦ : MapsTo (⇑(preReflection y g)) Φ Φ<VAR>hyΦ : y ∈ Φ<VAR>sxy : M ≃ₗ[R] M := reflection hgy ≪≫ₗ reflection hfx<VAR>hb : BijOn (⇑sxy) Φ Φ<VAR>hsxy : ∀ (n : ℕ), (⇑sxy)^[n] y = y + (2 * ↑n) • (x - y)<VAR>f' : ℕ → ↑Φ := fun n => ⟨(⇑sxy)^[n] y, ⋯⟩<VAR>this : ¬Injective f'<GOAL>x = y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>x : M<VAR>f : Dual R M<VAR>y : M<VAR>g : Dual R M<VAR>inst✝ : NoZeroSMulDivisors ℤ M<VAR>Φ : Set M<VAR>hΦ : _root_.Finite ↑Φ<VAR>hfx : f x = 2<VAR>hgy : g y = 2<VAR>hgx : g x = 2<VAR>hfy : f y = 2<VAR>hxfΦ : MapsTo (⇑(preReflection x f)) Φ Φ<VAR>hygΦ : MapsTo (⇑(preReflection y g)) Φ Φ<VAR>hyΦ : y ∈ Φ<VAR>sxy : M ≃ₗ[R] M := reflection hgy ≪≫ₗ reflection hfx<VAR>hb : BijOn (⇑sxy) Φ Φ<VAR>hsxy : ∀ (n : ℕ), (⇑sxy)^[n] y = y + (2 * ↑n) • (x - y)<VAR>f' : ℕ → ↑Φ := fun n => ⟨(⇑sxy)^[n] y, ⋯⟩<VAR>this : x ≠ y<GOAL>Injective f'
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>x : M<VAR>f : Dual R M<VAR>y : M<VAR>g : Dual R M<VAR>inst✝ : NoZeroSMulDivisors ℤ M<VAR>Φ : Set M<VAR>hΦ : _root_.Finite ↑Φ<VAR>hfx : f x = 2<VAR>hgy : g y = 2<VAR>hgx : g x = 2<VAR>hfy : f y = 2<VAR>hxfΦ : MapsTo (⇑(preReflection x f)) Φ Φ<VAR>hygΦ : MapsTo (⇑(preReflection y g)) Φ Φ<VAR>hyΦ : y ∈ Φ<VAR>sxy : M ≃ₗ[R] M := reflection hgy ≪≫ₗ reflection hfx<VAR>hb : BijOn (⇑sxy) Φ Φ<VAR>hsxy : ∀ (n : ℕ), (⇑sxy)^[n] y = y + (2 * ↑n) • (x - y)<VAR>f' : ℕ → ↑Φ := fun n => ⟨(⇑sxy)^[n] y, ⋯⟩<VAR>this : x ≠ y<VAR>n m : ℕ<VAR>hnm : f' n = f' m<GOAL>n = m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>x : M<VAR>f : Dual R M<VAR>y : M<VAR>g : Dual R M<VAR>inst✝ : NoZeroSMulDivisors ℤ M<VAR>Φ : Set M<VAR>hΦ : _root_.Finite ↑Φ<VAR>hfx : f x = 2<VAR>hgy : g y = 2<VAR>hgx : g x = 2<VAR>hfy : f y = 2<VAR>hxfΦ : MapsTo (⇑(preReflection x f)) Φ Φ<VAR>hygΦ : MapsTo (⇑(preReflection y g)) Φ Φ<VAR>hyΦ : y ∈ Φ<VAR>sxy : M ≃ₗ[R] M := reflection hgy ≪≫ₗ reflection hfx<VAR>hb : BijOn (⇑sxy) Φ Φ<VAR>hsxy : ∀ (n : ℕ), (⇑sxy)^[n] y = y + (2 * ↑n) • (x - y)<VAR>f' : ℕ → ↑Φ := fun n => ⟨(⇑sxy)^[n] y, ⋯⟩<VAR>this : x ≠ y<VAR>n m : ℕ<VAR>hnm : 2 * ↑n = 2 * ↑m ∨ x = y<GOAL>n = m
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>α : Type u_3<VAR>E : Type u_4<VAR>inst✝⁶ : MeasurableSpace M<VAR>inst✝⁵ : MeasurableSpace N<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : NormedAddCommGroup E<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>inst✝² : SMul M α<VAR>inst✝¹ : SMulInvariantMeasure M α μ<VAR>inst✝ : MeasurableSMul M α<VAR>c : M<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>b : E<GOAL>μ ((fun x => c • x) ⁻¹' s) ≠ ⊤
<VAR>a b c : Ordinal.{u}<GOAL>a ♯ succ b = succ (a ♯ b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ✝ ν ν₁✝ ν₂✝ : Measure α<VAR>s t : Set α<VAR>μ ν₁ ν₂ : Measure α<VAR>inst✝ : SigmaFinite μ<GOAL>ν₁ + μ = ν₂ + μ ↔ ν₁ = ν₂
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>x : R<GOAL>eval x (derivative p) = p.sum fun n a => a * ↑n * x ^ (n - 1)
<VAR>n m : ℕ<VAR>p i : Fin (n + 1)<VAR>h : i < p<VAR>hp : optParam (p ≠ 0) ⋯<VAR>hi : optParam (i ≠ last n) ⋯<GOAL>(p.pred hp).predAbove i = i.castPred hi
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>r✝ : α → β → Prop<VAR>p : γ → δ → Prop<VAR>m : Multiset α<VAR>a : α<VAR>r : α → α → Prop<VAR>n : ℕ<VAR>h : Rel r (replicate n a) m<VAR>x : α<VAR>hx : x ∈ m<GOAL>r a x
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>r✝ : α → β → Prop<VAR>p : γ → δ → Prop<VAR>m : Multiset α<VAR>a : α<VAR>r : α → α → Prop<VAR>n : ℕ<VAR>h : Rel r (replicate n a) m<VAR>x : α<VAR>hx : x ∈ m<VAR>b : α<VAR>hb1 : b ∈ replicate n a<VAR>hb2 : flip r x b<GOAL>r a x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>hf : InjOn f (f ⁻¹' N.E)<GOAL>(N.comap f).Indep I ↔ N.Indep (f '' I)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>hf : InjOn f (f ⁻¹' N.E)<GOAL>N.Indep (f '' I) → InjOn f I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>hf : InjOn f (f ⁻¹' N.E)<VAR>hi : N.Indep (f '' I)<GOAL>I ⊆ f ⁻¹' (f '' I)