ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : Module R S<VAR>inst✝² : Module S A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>s : Set S<VAR>hs : span R s = ⊤<VAR>t : Set A<VAR>p : A<VAR>hp : p ∈ restrictScalars R (span S t)<VAR>s0 : S<VAR>y : A<VAR>hy : y ∈ t<GOAL>0 • y ∈ span R (s • t)
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : Module R S<VAR>inst✝² : Module S A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>s : Set S<VAR>hs : span R s = ⊤<VAR>t : Set A<VAR>p : A<VAR>hp : p ∈ restrictScalars R (span S t)<VAR>s0 : S<VAR>y : A<VAR>hy : y ∈ t<GOAL>∀ (x y_1 : S), x • y ∈ span R (s • t) → y_1 • y ∈ span R (s • t) → (x + y_1) • y ∈ span R (s • t)
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : Module R S<VAR>inst✝² : Module S A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>s : Set S<VAR>hs : span R s = ⊤<VAR>t : Set A<VAR>p : A<VAR>hp : p ∈ restrictScalars R (span S t)<VAR>s0 : S<VAR>y : A<VAR>hy : y ∈ t<GOAL>∀ (a : R) (x : S), x • y ∈ span R (s • t) → (a • x) • y ∈ span R (s • t)
<VAR>a b : Ordinal.{u}<VAR>hb : 0 < b<VAR>hba : b ≤ a ^ ω<GOAL>nfp (fun x => a * x) b = a ^ ω
<VAR>a b : Ordinal.{u}<VAR>hb : 0 < b<VAR>hba : b ≤ a ^ ω<VAR>ha : a = 0<GOAL>nfp (fun x => a * x) b = a ^ ω
<VAR>a b : Ordinal.{u}<VAR>hb : 0 < b<VAR>hba : b ≤ a ^ ω<VAR>ha : 0 < a<GOAL>nfp (fun x => a * x) b = a ^ ω
<VAR>a b : Ordinal.{u}<VAR>hb : 0 < b<VAR>hba : b ≤ a ^ ω<VAR>ha : 0 < a<GOAL>nfp (fun x => a * x) b ≤ a ^ ω
<VAR>a b : Ordinal.{u}<VAR>hb : 0 < b<VAR>hba : b ≤ a ^ ω<VAR>ha : 0 < a<GOAL>a ^ ω ≤ nfp (fun x => a * x) b
<VAR>a b : Ordinal.{u}<VAR>hb : 0 < b<VAR>hba : b ≤ a ^ ω<VAR>ha : 0 < a<GOAL>nfp (fun x => a * x) 1 ≤ nfp (fun x => a * x) b
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : AEStronglyMeasurable f μ<VAR>A : ℝ<GOAL>Integrable (truncation f A) μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : AEStronglyMeasurable f μ<VAR>A : ℝ<GOAL>Memℒp (truncation f A) 1 μ
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>J₁ J₂ : GrothendieckTopology C<VAR>X Y : C<VAR>f : Y ⟶ X<VAR>S : Sieve X<VAR>hS : J₁.IsClosed S<VAR>Z : C<VAR>g : Z ⟶ Y<VAR>hg : J₁.Covers (Sieve.pullback f S) g<GOAL>J₁.Covers S (g ≫ f)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x✝ : α<VAR>l l' : List α<VAR>h : l ~r l'<VAR>hn : l.Nodup<VAR>x : α<VAR>hx : x ∈ l<GOAL>l.next x hx = l'.next x ⋯
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x : α<VAR>l l' : List α<VAR>h : l ~r l'<VAR>hn : l.Nodup<VAR>k : Fin l.length<VAR>hx : l.get k ∈ l<GOAL>l.next (l.get k) hx = l'.next (l.get k) ⋯
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x : α<VAR>l : List α<VAR>hn : l.Nodup<VAR>k : Fin l.length<VAR>hx : l.get k ∈ l<VAR>n : ℕ<VAR>h : l ~r l.rotate n<GOAL>l.next (l.get k) hx = (l.rotate n).next (l.get k) ⋯
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x : α<VAR>l : List α<VAR>hn : l.Nodup<VAR>k : Fin l.length<VAR>hx : l.get k ∈ l<VAR>n : ℕ<VAR>h : l ~r l.rotate n<GOAL>l.get ⟨(↑k + 1) % l.length, ⋯⟩ = (l.rotate n).next (l.get k) ⋯
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x : α<VAR>l : List α<VAR>hn : l.Nodup<VAR>k : Fin l.length<VAR>hx : l.get k ∈ l<VAR>n : ℕ<VAR>h : l ~r l.rotate n<GOAL>l.get ⟨(↑k + 1) % l.length, ⋯⟩ = (l.rotate n).next ((l.rotate n).get ⟨(l.length - n % l.length + ↑k) % l.length, ⋯⟩) ⋯
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x : α<VAR>l : List α<VAR>hn : l.Nodup<VAR>k : Fin l.length<VAR>hx : l.get k ∈ l<VAR>n : ℕ<VAR>h : l ~r l.rotate n<GOAL>(l.rotate n).get ⟨(l.length - n % l.length + ↑⟨(↑k + 1) % l.length, ⋯⟩) % l.length, ⋯⟩ = (l.rotate n).get ⟨(↑⟨(l.length - n % l.length + ↑k) % l.length, ⋯⟩ + 1) % (l.rotate n).length, ⋯⟩
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : WeierstrassCurve R<VAR>inst✝ : Nontrivial R<VAR>n : ℤ<VAR>h : ↑n ≠ 0<GOAL>W.preΨ n ≠ 0
<VAR>θ ψ : Angle<VAR>h : θ.toReal = ψ.toReal<GOAL>θ = ψ
<VAR>ψ : Angle<VAR>x✝ : ℝ<VAR>h : (↑x✝).toReal = ψ.toReal<GOAL>↑x✝ = ψ
<VAR>x✝¹ x✝ : ℝ<VAR>h : (↑x✝¹).toReal = (↑x✝).toReal<GOAL>↑x✝¹ = ↑x✝
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type u<VAR>inst✝¹ : CommRing S<VAR>P : Type u<VAR>inst✝ : CommRing P<VAR>U V : Opens ↑(PrimeSpectrum.Top R)<VAR>hUV : U = V<VAR>p : ↑(PrimeSpectrum.Top R)<VAR>hpV : p ∈ V.carrier<GOAL>p ∈ ⇑(PrimeSpectrum.comap (RingHom.id R)) ⁻¹' U.carrier
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type u<VAR>inst✝¹ : CommRing S<VAR>P : Type u<VAR>inst✝ : CommRing P<VAR>U V : Opens ↑(PrimeSpectrum.Top R)<VAR>hUV : U = V<GOAL>comap (RingHom.id R) U V ⋯ = eqToHom ⋯
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>B : ι → Set α<VAR>t : Set ι<VAR>δ : ι → ℝ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>δnonneg : ∀ a ∈ t, 0 ≤ δ a<VAR>R : ℝ<VAR>δle : ∀ a ∈ t, δ a ≤ R<VAR>hne : ∀ a ∈ t, (B a).Nonempty<VAR>T : Set (Set ι) := {u | u ⊆ t ∧ u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}<GOAL>∃ u ⊆ t, u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ δ a ≤ τ * δ b
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>B : ι → Set α<VAR>t : Set ι<VAR>δ : ι → ℝ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>δnonneg : ∀ a ∈ t, 0 ≤ δ a<VAR>R : ℝ<VAR>δle : ∀ a ∈ t, δ a ≤ R<VAR>hne : ∀ a ∈ t, (B a).Nonempty<VAR>T : Set (Set ι) := {u | u ⊆ t ∧ u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}<VAR>u : Set ι<VAR>uT : u ∈ T<VAR>hu : ∀ v ∈ T, u ⊆ v → v = u<GOAL>∃ u ⊆ t, u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ δ a ≤ τ * δ b
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>B : ι → Set α<VAR>t : Set ι<VAR>δ : ι → ℝ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>δnonneg : ∀ a ∈ t, 0 ≤ δ a<VAR>R : ℝ<VAR>δle : ∀ a ∈ t, δ a ≤ R<VAR>hne : ∀ a ∈ t, (B a).Nonempty<VAR>T : Set (Set ι) := {u | u ⊆ t ∧ u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}<VAR>u : Set ι<VAR>uT : u ∈ T<VAR>hu : ∀ v ∈ T, u ⊆ v → v = u<VAR>a : ι<VAR>hat : a ∈ t<GOAL>∃ b ∈ u, (B a ∩ B b).Nonempty ∧ δ a ≤ τ * δ b
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>B : ι → Set α<VAR>t : Set ι<VAR>δ : ι → ℝ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>δnonneg : ∀ a ∈ t, 0 ≤ δ a<VAR>R : ℝ<VAR>δle : ∀ a ∈ t, δ a ≤ R<VAR>hne : ∀ a ∈ t, (B a).Nonempty<VAR>T : Set (Set ι) := {u | u ⊆ t ∧ u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}<VAR>u : Set ι<VAR>uT : u ∈ T<VAR>a : ι<VAR>hat : a ∈ t<VAR>hu : ∀ b ∈ u, (B a ∩ B b).Nonempty → τ * δ b < δ a<GOAL>∃ v ∈ T, u ⊆ v ∧ v ≠ u
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>B : ι → Set α<VAR>t : Set ι<VAR>δ : ι → ℝ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>δnonneg : ∀ a ∈ t, 0 ≤ δ a<VAR>R : ℝ<VAR>δle : ∀ a ∈ t, δ a ≤ R<VAR>hne : ∀ a ∈ t, (B a).Nonempty<VAR>T : Set (Set ι) := {u | u ⊆ t ∧ u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}<VAR>u : Set ι<VAR>uT : u ∈ T<VAR>a : ι<VAR>hat : a ∈ t<VAR>hu : ∀ b ∈ u, (B a ∩ B b).Nonempty → τ * δ b < δ a<VAR>a_disj : ∀ c ∈ u, Disjoint (B a) (B c)<GOAL>∃ v ∈ T, u ⊆ v ∧ v ≠ u
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>B : ι → Set α<VAR>t : Set ι<VAR>δ : ι → ℝ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>δnonneg : ∀ a ∈ t, 0 ≤ δ a<VAR>R : ℝ<VAR>δle : ∀ a ∈ t, δ a ≤ R<VAR>hne : ∀ a ∈ t, (B a).Nonempty<VAR>T : Set (Set ι) := {u | u ⊆ t ∧ u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}<VAR>u : Set ι<VAR>uT : u ∈ T<VAR>a : ι<VAR>hat : a ∈ t<VAR>hu : ∀ b ∈ u, (B a ∩ B b).Nonempty → τ * δ b < δ a<VAR>a_disj : ∀ c ∈ u, Disjoint (B a) (B c)<VAR>A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}<VAR>Anonempty : A.Nonempty<VAR>m : ℝ := sSup (δ '' A)<GOAL>∃ v ∈ T, u ⊆ v ∧ v ≠ u
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>B : ι → Set α<VAR>t : Set ι<VAR>δ : ι → ℝ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>δnonneg : ∀ a ∈ t, 0 ≤ δ a<VAR>R : ℝ<VAR>δle : ∀ a ∈ t, δ a ≤ R<VAR>hne : ∀ a ∈ t, (B a).Nonempty<VAR>T : Set (Set ι) := {u | u ⊆ t ∧ u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}<VAR>u : Set ι<VAR>uT : u ∈ T<VAR>a : ι<VAR>hat : a ∈ t<VAR>hu : ∀ b ∈ u, (B a ∩ B b).Nonempty → τ * δ b < δ a<VAR>a_disj : ∀ c ∈ u, Disjoint (B a) (B c)<VAR>A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}<VAR>Anonempty : A.Nonempty<VAR>m : ℝ := sSup (δ '' A)<VAR>bddA : BddAbove (δ '' A)<GOAL>∃ v ∈ T, u ⊆ v ∧ v ≠ u
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>B : ι → Set α<VAR>t : Set ι<VAR>δ : ι → ℝ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>δnonneg : ∀ a ∈ t, 0 ≤ δ a<VAR>R : ℝ<VAR>δle : ∀ a ∈ t, δ a ≤ R<VAR>hne : ∀ a ∈ t, (B a).Nonempty<VAR>T : Set (Set ι) := {u | u ⊆ t ∧ u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}<VAR>u : Set ι<VAR>uT : u ∈ T<VAR>A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}<VAR>Anonempty : A.Nonempty<VAR>m : ℝ := sSup (δ '' A)<VAR>bddA : BddAbove (δ '' A)<VAR>a' : ι<VAR>a'A : a' ∈ A<VAR>ha' : m / τ ≤ δ a'<GOAL>∃ v ∈ T, u ⊆ v ∧ v ≠ u
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>B : ι → Set α<VAR>t : Set ι<VAR>δ : ι → ℝ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>δnonneg : ∀ a ∈ t, 0 ≤ δ a<VAR>R : ℝ<VAR>δle : ∀ a ∈ t, δ a ≤ R<VAR>hne : ∀ a ∈ t, (B a).Nonempty<VAR>T : Set (Set ι) := {u | u ⊆ t ∧ u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}<VAR>u : Set ι<VAR>uT : u ∈ T<VAR>A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}<VAR>Anonempty : A.Nonempty<VAR>m : ℝ := sSup (δ '' A)<VAR>bddA : BddAbove (δ '' A)<VAR>a' : ι<VAR>a'A : a' ∈ A<VAR>ha' : m / τ ≤ δ a'<VAR>a'_ne_u : a' ∉ u<GOAL>∃ v ∈ T, u ⊆ v ∧ v ≠ u
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>B : ι → Set α<VAR>t : Set ι<VAR>δ : ι → ℝ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>δnonneg : ∀ a ∈ t, 0 ≤ δ a<VAR>R : ℝ<VAR>δle : ∀ a ∈ t, δ a ≤ R<VAR>hne : ∀ a ∈ t, (B a).Nonempty<VAR>T : Set (Set ι) := {u | u ⊆ t ∧ u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}<VAR>u : Set ι<VAR>uT : u ∈ T<VAR>A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}<VAR>Anonempty : A.Nonempty<VAR>m : ℝ := sSup (δ '' A)<VAR>bddA : BddAbove (δ '' A)<VAR>a' : ι<VAR>a'A : a' ∈ A<VAR>ha' : m / τ ≤ δ a'<VAR>a'_ne_u : a' ∉ u<GOAL>insert a' u ⊆ t
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>B : ι → Set α<VAR>t : Set ι<VAR>δ : ι → ℝ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>δnonneg : ∀ a ∈ t, 0 ≤ δ a<VAR>R : ℝ<VAR>δle : ∀ a ∈ t, δ a ≤ R<VAR>hne : ∀ a ∈ t, (B a).Nonempty<VAR>T : Set (Set ι) := {u | u ⊆ t ∧ u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}<VAR>u : Set ι<VAR>uT : u ∈ T<VAR>A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}<VAR>Anonempty : A.Nonempty<VAR>m : ℝ := sSup (δ '' A)<VAR>bddA : BddAbove (δ '' A)<VAR>a' : ι<VAR>a'A : a' ∈ A<VAR>ha' : m / τ ≤ δ a'<VAR>a'_ne_u : a' ∉ u<GOAL>(insert a' u).PairwiseDisjoint B
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>B : ι → Set α<VAR>t : Set ι<VAR>δ : ι → ℝ<VAR>τ : ℝ<VAR>hτ : 1 < τ<VAR>δnonneg : ∀ a ∈ t, 0 ≤ δ a<VAR>R : ℝ<VAR>δle : ∀ a ∈ t, δ a ≤ R<VAR>hne : ∀ a ∈ t, (B a).Nonempty<VAR>T : Set (Set ι) := {u | u ⊆ t ∧ u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}<VAR>u : Set ι<VAR>uT : u ∈ T<VAR>A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}<VAR>Anonempty : A.Nonempty<VAR>m : ℝ := sSup (δ '' A)<VAR>bddA : BddAbove (δ '' A)<VAR>a' : ι<VAR>a'A : a' ∈ A<VAR>ha' : m / τ ≤ δ a'<VAR>a'_ne_u : a' ∉ u<GOAL>∀ a ∈ t, ∀ b ∈ insert a' u, (B a ∩ B b).Nonempty → ∃ c ∈ insert a' u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c
<VAR>α : 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>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f✝ f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Set α<VAR>t✝ t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a✝ a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<VAR>f : α → β → β<VAR>a : α<VAR>h : ∀ (b : β), f a b = b<VAR>t : Set β<GOAL>image2 f {a} t = t
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<GOAL>(loopyOn E).Base B ↔ B = ∅
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<GOAL>B = ∅ → B ⊆ ∅ → B = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : α → E<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>↑(μ.withDensityᵥ (f + g)) i = ↑(μ.withDensityᵥ f + μ.withDensityᵥ g) i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : α → E<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>∫ (x : α) in i, (f + g) x ∂μ = ∫ (x : α) in i, f x ∂μ + ∫ (x : α) in i, g x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : α → E<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>∫ (x : α) in i, f x + g x ∂μ = ∫ (x : α) in i, f x ∂μ + ∫ (x : α) in i, g x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : α → E<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>IntegrableOn f Set.univ (μ.restrict i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : α → E<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>IntegrableOn g Set.univ (μ.restrict i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>s s₁ s₂ : Finset β<VAR>f : β → α<GOAL>s.gcd f = 0 ↔ ∀ x ∈ s, f x = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>s s₁ s₂ : Finset β<VAR>f : β → α<GOAL>(∀ x ∈ Multiset.map f s.val, x = 0) ↔ ∀ x ∈ s, f x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝¹ : R1Space α<VAR>inst✝ : μ.OuterRegular<VAR>k : Set α<VAR>hk : IsCompact k<GOAL>μ (closure k) = μ k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝¹ : R1Space α<VAR>inst✝ : μ.OuterRegular<VAR>k : Set α<VAR>hk : IsCompact k<GOAL>μ (closure k) ≤ μ k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝¹ : R1Space α<VAR>inst✝ : μ.OuterRegular<VAR>k : Set α<VAR>hk : IsCompact k<GOAL>∀ (i : Set α), k ⊆ i → IsOpen i → μ (closure k) ≤ μ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝¹ : R1Space α<VAR>inst✝ : μ.OuterRegular<VAR>k : Set α<VAR>hk : IsCompact k<VAR>u : Set α<VAR>ku : k ⊆ u<VAR>u_open : IsOpen u<GOAL>μ (closure k) ≤ μ u
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a✝ b✝ c d a b : α<GOAL>a \ (a ⊓ b) = a \ b
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>n : ℕ<GOAL>(↑n).natTrailingDegree = 0
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderBot α<VAR>ha : IsWellOrderLimitElement ⊥<GOAL>False
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderBot α<VAR>ha : IsWellOrderLimitElement ⊥<VAR>b : α<VAR>hb : b < ⊥<GOAL>False
<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>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>inst✝ : IsLocalization M S<VAR>p : S[X]<VAR>i : ℕ<VAR>h : coeffIntegerNormalization M p i ≠ 0<GOAL>i ∈ p.support
<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>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>inst✝ : IsLocalization M S<VAR>p : S[X]<VAR>i : ℕ<VAR>h : i ∉ p.support<GOAL>¬coeffIntegerNormalization M p i ≠ 0
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<GOAL>((↑m + 1) / ↑m) ^ 2 ≤ 1 + ε ^ 5 / 49
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<GOAL>(1 + 1 / ↑m) ^ 2 ≤ 1 + ε ^ 5 / 49
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<GOAL>↑m ≠ 0
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>this : 1 + 1 / ↑m ≤ 1 + ε ^ 5 / 100<GOAL>(1 + 1 / ↑m) ^ 2 ≤ 1 + ε ^ 5 / 49
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>this : 1 + 1 / ↑m ≤ 1 + ε ^ 5 / 100<GOAL>0 ≤ 1 + 1 / ↑m
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>this : 1 + 1 / ↑m ≤ 1 + ε ^ 5 / 100<GOAL>(1 + ε ^ 5 / 100) ^ 2 ≤ 1 + ε ^ 5 / 49
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>this : 1 + 1 / ↑m ≤ 1 + ε ^ 5 / 100<GOAL>ε ^ 5 * ε ^ 5 ≤ ε ^ 5 * ((1 / 49 - 2 / 100) * 100 ^ 2)
<VAR>α : Type u_1<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableEq α<VAR>P : Finpartition univ<VAR>hP : P.IsEquipartition<VAR>G : SimpleGraph α<VAR>inst✝¹ : DecidableRel G.Adj<VAR>ε : ℝ<VAR>U : Finset α<VAR>hU : U ∈ P.parts<VAR>V : Finset α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Nonempty α<VAR>hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α<VAR>hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5<VAR>hε₁ : ε ≤ 1<VAR>this : 1 + 1 / ↑m ≤ 1 + ε ^ 5 / 100<GOAL>ε ^ 5 ≤ (1 / 49 - 2 / 100) * 100 ^ 2
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid α<VAR>s✝ t : Finset α<VAR>a✝ : α<VAR>m n : ℕ<VAR>a : α<VAR>s : Fin n → Finset α<GOAL>a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i => ↑(f i)).prod = a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid α<VAR>s✝ t : Finset α<VAR>a✝ : α<VAR>m n : ℕ<VAR>a : α<VAR>s : Fin n → Finset α<GOAL>(∃ f, (List.ofFn fun i => ↑(f i)).prod = a) ↔ ∃ f, (List.ofFn fun i => ↑(f i)).prod = a
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>m✝ : Multiset α<VAR>β : Type u_2<VAR>inst✝ : CommMonoid β<VAR>m : Multiset α<VAR>f : α → ℕ → β<GOAL>∏ x ∈ m.toEnumFinset, f x.1 x.2 = ∏ x : m.ToType, f x.fst ↑x.snd
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>m✝ : Multiset α<VAR>β : Type u_2<VAR>inst✝ : CommMonoid β<VAR>m : Multiset α<VAR>f : α → ℕ → β<GOAL>∏ x ∈ m.toEnumFinset, f x.1 x.2 = ∏ x : { x // x ∈ m.toEnumFinset }, f (↑x).1 (↑x).2
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>m✝ : Multiset α<VAR>β : Type u_2<VAR>inst✝ : CommMonoid β<VAR>m : Multiset α<VAR>f : α → ℕ → β<GOAL>∀ (x : m.ToType), f x.fst ↑x.snd = f (↑(m.coeEquiv x)).1 (↑(m.coeEquiv x)).2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : SupSet α<VAR>f g : ι → α<VAR>s : Set α<GOAL>sSup s = ⨆ a, ↑a
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>x : F α<GOAL>id <$> x = x
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>x : F α<GOAL>id <$> abs (repr x) = abs (repr x)
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>x : F α<VAR>a : (P F).A<VAR>f : (P F).B a → α<GOAL>id <$> abs ⟨a, f⟩ = abs ⟨a, f⟩
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>x : F α<VAR>a : (P F).A<VAR>f : (P F).B a → α<GOAL>abs ((P F).map id ⟨a, f⟩) = abs ⟨a, f⟩
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>inst✝ : Nontrivial R<GOAL>W.polynomial.natDegree = 2
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>inst✝ : Nontrivial R<GOAL>{ a := 0, b := 1, c := { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly, d := { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ }.toPoly }.toPoly.natDegree = 2
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>x y : WithLp ⊤ (α × β)<GOAL>dist x y = ↑(nndist x.1 y.1 ⊔ nndist x.2 y.2)
<VAR>u✝ : Lean.Level<VAR>arg : Q(Type u✝)<VAR>sα✝ : Q(CommSemiring «$arg»)<VAR>u : Lean.Level<VAR>α✝ : Q(Type u)<VAR>sα : Q(CommSemiring $α✝)<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>a✝ a'✝ a₁ a₂ a₃ b✝ b'✝ b₁ b₂ b₃ c c₁ c₂ : R<VAR>α β : Type u_2<VAR>inst : CSLift α β<VAR>a b : α<VAR>a' b' : β<VAR>h1 : CSLiftVal a a'<VAR>h2 : CSLiftVal b b'<VAR>h : a' = b'<GOAL>CSLift.lift a = CSLift.lift b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>p : α → Prop<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : OrderBot (Subtype p)<VAR>hbot : p ⊥<VAR>x : { x // p x }<GOAL>↑x = ⊥ ↔ x = ⊥
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<GOAL>∀ (a : List R[X]), (prod ⟦a⟧).degree ≤ (Multiset.map degree ⟦a⟧).sum