ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>S : Type u_1<VAR>M : Type u_2<VAR>G : Type u_3<VAR>inst✝ : Semigroup S<VAR>a b x y z x' y' : S<VAR>ha : SemiconjBy a y z<VAR>hb : SemiconjBy b x y<GOAL>a * b * x = z * (a * b)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x y : R<VAR>h : IsCoprime x y<VAR>z : R<GOAL>IsCoprime (x + y * z + y * -z) y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : (i : ι) → κ i → Set α<VAR>t : Set α<GOAL>(⋂ i, ⋂ j, s i j) ∪ t = ⋂ i, ⋂ j, s i j ∪ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : DistribLattice α<VAR>inst✝² : BoundedOrder α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<GOAL>a ∈ upperClosure ↑(s ⊻ t) ↔ a ∈ upperClosure ↑s ∧ a ∈ upperClosure ↑t
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>ha : 0 < a<GOAL>a⁻¹ ≤ b ↔ 1 ≤ b * a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>ha : 0 < a<GOAL>1 / a ≤ b ↔ 1 ≤ b * a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>u : δ → δ → Prop<VAR>f : α → β<VAR>hf : Surjective f<VAR>o : ∀ {a b : α}, r a b ↔ s (f a) (f b)<VAR>a✝ b✝ : β<VAR>h : s a✝ b✝<GOAL>r (surjInv hf a✝) (surjInv hf b✝)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>K : ℝ≥0<VAR>f : α → β<VAR>x y : α<VAR>r : ℝ<VAR>hf : LipschitzWith K f<VAR>u : ℕ → α<VAR>hu : CauchySeq u<GOAL>CauchySeq (f ∘ u)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>K : ℝ≥0<VAR>f : α → β<VAR>x y : α<VAR>r : ℝ<VAR>hf : LipschitzWith K f<VAR>u : ℕ → α<VAR>hu : CauchySeq u<VAR>b : ℕ → ℝ<VAR>b_nonneg : ∀ (n : ℕ), 0 ≤ b n<VAR>hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N<VAR>blim : Tendsto b atTop (𝓝 0)<GOAL>CauchySeq (f ∘ u)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>K : ℝ≥0<VAR>f : α → β<VAR>x y : α<VAR>r : ℝ<VAR>hf : LipschitzWith K f<VAR>u : ℕ → α<VAR>hu : CauchySeq u<VAR>b : ℕ → ℝ<VAR>b_nonneg : ∀ (n : ℕ), 0 ≤ b n<VAR>hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N<VAR>blim : Tendsto b atTop (𝓝 0)<GOAL>∀ (n : ℕ), 0 ≤ (fun n => ↑K * b n) n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>K : ℝ≥0<VAR>f : α → β<VAR>x y : α<VAR>r : ℝ<VAR>hf : LipschitzWith K f<VAR>u : ℕ → α<VAR>hu : CauchySeq u<VAR>b : ℕ → ℝ<VAR>b_nonneg : ∀ (n : ℕ), 0 ≤ b n<VAR>hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N<VAR>blim : Tendsto b atTop (𝓝 0)<GOAL>∀ (n m N : ℕ), N ≤ n → N ≤ m → dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun n => ↑K * b n) N
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoMetricSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>K : ℝ≥0<VAR>f : α → β<VAR>x y : α<VAR>r : ℝ<VAR>hf : LipschitzWith K f<VAR>u : ℕ → α<VAR>hu : CauchySeq u<VAR>b : ℕ → ℝ<VAR>b_nonneg : ∀ (n : ℕ), 0 ≤ b n<VAR>hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N<VAR>blim : Tendsto b atTop (𝓝 0)<GOAL>Tendsto (fun n => ↑K * b n) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝² : ConditionallyCompleteLattice α<VAR>s t : Set α<VAR>a b : α<VAR>inst✝¹ : NoMinOrder α<VAR>inst✝ : DenselyOrdered α<VAR>w : α<VAR>hw : w < a<GOAL>∃ a_1 ∈ Iio a, w < a_1
<VAR>x z : ℝ<VAR>h : ↑x + ⊤ ≤ ↑x + ↑z<GOAL>⊤ ≤ ↑z
<VAR>x y z : ℝ<VAR>h : ↑x + ↑y ≤ ↑x + ↑z<GOAL>↑y ≤ ↑z
<VAR>R : Type u_1<VAR>inst✝¹⁵ : Semiring R<VAR>M : Type u_2<VAR>inst✝¹⁴ : AddCommMonoid M<VAR>inst✝¹³ : Module R M<VAR>N : Type u_3<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : Module R N<VAR>P : Type u_4<VAR>inst✝¹⁰ : AddCommMonoid P<VAR>inst✝⁹ : Module R P<VAR>M' : Type u_5<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : Module R M'<VAR>N' : Type u_6<VAR>inst✝⁶ : AddCommGroup N'<VAR>inst✝⁵ : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M₂<VAR>M₃ : Type u_11<VAR>inst✝² : AddCommMonoid M₃<VAR>inst✝¹ : Module R M₃<VAR>f f' : M [⋀^ι]→ₗ[R] N<VAR>g g₂ : M [⋀^ι]→ₗ[R] N'<VAR>g' : M' [⋀^ι]→ₗ[R] N'<VAR>v : ι → M<VAR>v' : ι → M'<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>f (update (update v j (v i)) i (v j)) + f v = 0
<VAR>R : Type u_1<VAR>inst✝¹⁵ : Semiring R<VAR>M : Type u_2<VAR>inst✝¹⁴ : AddCommMonoid M<VAR>inst✝¹³ : Module R M<VAR>N : Type u_3<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : Module R N<VAR>P : Type u_4<VAR>inst✝¹⁰ : AddCommMonoid P<VAR>inst✝⁹ : Module R P<VAR>M' : Type u_5<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : Module R M'<VAR>N' : Type u_6<VAR>inst✝⁶ : AddCommGroup N'<VAR>inst✝⁵ : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M₂<VAR>M₃ : Type u_11<VAR>inst✝² : AddCommMonoid M₃<VAR>inst✝¹ : Module R M₃<VAR>f f' : M [⋀^ι]→ₗ[R] N<VAR>g g₂ : M [⋀^ι]→ₗ[R] N'<VAR>g' : M' [⋀^ι]→ₗ[R] N'<VAR>v : ι → M<VAR>v' : ι → M'<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>hij : i ≠ j<GOAL>f (update (update v j (v i)) i (v j)) + f v = f (update (update v i (v i + v j)) j (v i + v j))
<VAR>m n : ℤ<VAR>k : ℕ<GOAL>(m.ldiff n).testBit k = (m.testBit k && !n.testBit k)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>g : Y ⟶ Z<VAR>W : C<VAR>h : Z ⟶ W<VAR>inst✝³ : HasImage (g ≫ h)<VAR>inst✝² : HasImage (f ≫ g ≫ h)<VAR>inst✝¹ : HasImage h<VAR>inst✝ : HasImage ((f ≫ g) ≫ h)<GOAL>preComp f (g ≫ h) ≫ preComp g h = eqToHom ⋯ ≫ preComp (f ≫ g) h
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>g : Y ⟶ Z<VAR>W : C<VAR>h : Z ⟶ W<VAR>inst✝³ : HasImage (g ≫ h)<VAR>inst✝² : HasImage (f ≫ g ≫ h)<VAR>inst✝¹ : HasImage h<VAR>inst✝ : HasImage ((f ≫ g) ≫ h)<GOAL>(preComp f (g ≫ h) ≫ preComp g h) ≫ ι h = (eqToHom ⋯ ≫ preComp (f ≫ g) h) ≫ ι h
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>g : Y ⟶ Z<VAR>W : C<VAR>h : Z ⟶ W<VAR>inst✝³ : HasImage (g ≫ h)<VAR>inst✝² : HasImage (f ≫ g ≫ h)<VAR>inst✝¹ : HasImage h<VAR>inst✝ : HasImage ((f ≫ g) ≫ h)<GOAL>(lift (MonoFactorisation.mk (image (g ≫ h)) (ι (g ≫ h)) (f ≫ factorThruImage (g ≫ h)) ⋯) ≫ lift (MonoFactorisation.mk (image h) (ι h) (g ≫ factorThruImage h) ⋯)) ≫ ι h = (lift (MonoFactorisation.mk (image ((f ≫ g) ≫ h)) (ι ((f ≫ g) ≫ h)) (factorThruImage ((f ≫ g) ≫ h)) ⋯) ≫ lift (MonoFactorisation.mk (image h) (ι h) ((f ≫ g) ≫ factorThruImage h) ⋯)) ≫ ι h
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<VAR>g : Y ⟶ Z<VAR>W : C<VAR>h : Z ⟶ W<VAR>inst✝³ : HasImage (g ≫ h)<VAR>inst✝² : HasImage (f ≫ g ≫ h)<VAR>inst✝¹ : HasImage h<VAR>inst✝ : HasImage ((f ≫ g) ≫ h)<GOAL>ι (f ≫ g ≫ h) = lift (MonoFactorisation.mk (image ((f ≫ g) ≫ h)) (ι ((f ≫ g) ≫ h)) (factorThruImage ((f ≫ g) ≫ h)) ⋯) ≫ lift (MonoFactorisation.mk (image h) (ι h) ((f ≫ g) ≫ factorThruImage h) ⋯) ≫ ι h
<VAR>R : Type uR<VAR>M : Type uM<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>Q : QuadraticForm R M<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝ f : EvenHom Q A<VAR>this : AddCommGroup ↥(CliffordAlgebra.even.lift.S f) := AddSubgroupClass.toAddCommGroup (CliffordAlgebra.even.lift.S f)<GOAL>CliffordAlgebra Q →ₗ[R] A
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>g : β → γ<VAR>s : WSeq α<GOAL>Seq.map (Option.map (g ∘ f)) s = Seq.map (Option.map g) (Seq.map (Option.map f) s)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>g : β → γ<VAR>s : WSeq α<GOAL>Seq.map (Option.map (g ∘ f)) s = Seq.map (Option.map g ∘ Option.map f) s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>g : β → γ<VAR>s : WSeq α<GOAL>Option.map (g ∘ f) = Option.map g ∘ Option.map f
<VAR>a b m n p✝ p r i : ℕ<VAR>pp : Prime p<VAR>hr0 : r ≠ 0<GOAL>¬p ∣ r ↔ (p * i + r).factorization p = 0
<VAR>a b m n p✝ p r i : ℕ<VAR>pp : Prime p<VAR>hr0 : r ≠ 0<VAR>h : (p * i + r).factorization p = 0<GOAL>¬p ∣ r
<VAR>a b m n p✝ p r i : ℕ<VAR>pp : Prime p<VAR>hr0 : r ≠ 0<VAR>h : ¬Prime p ∨ ¬p ∣ p * i + r ∨ p * i + r = 0<GOAL>¬p ∣ r
<VAR>a b m n p✝ p r i : ℕ<VAR>pp : Prime p<VAR>hr0 : r ≠ 0<VAR>h : p ∣ r<GOAL>Prime p ∧ p ∣ p * i + r ∧ p * i + r ≠ 0
<VAR>ι : Type u_1<VAR>𝕜✝ : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedRing A<VAR>f✝ g : ℝ → E<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>𝕜 : Type u_6<VAR>f : ℝ → 𝕜<VAR>inst✝ : NormedField 𝕜<VAR>h : IntervalIntegrable f μ a b<VAR>c : 𝕜<GOAL>IntervalIntegrable (fun x => f x / c) μ a b
<VAR>M : Type u_1<VAR>G : Type u_2<VAR>inst✝ : Monoid M<VAR>a : M<VAR>x y : Mˣ<VAR>h : SemiconjBy a ↑x ↑y<VAR>n : ℕ<GOAL>SemiconjBy a ↑(x ^ ↑n) ↑(y ^ ↑n)
<VAR>M : Type u_1<VAR>G : Type u_2<VAR>inst✝ : Monoid M<VAR>a : M<VAR>x y : Mˣ<VAR>h : SemiconjBy a ↑x ↑y<VAR>n : ℕ<GOAL>SemiconjBy a ↑(x ^ -[n+1]) ↑(y ^ -[n+1])
<VAR>R : Type u<VAR>inst✝³ : CommSemiring R<VAR>S : Type v<VAR>inst✝² : CommSemiring S<VAR>p✝ q : ℕ<VAR>A : Type u_1<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>p : ℕ<VAR>P : R[X]<VAR>r : A<GOAL>(aeval r) ((expand R p) P) = (aeval (r ^ p)) P
<VAR>R : Type u<VAR>inst✝³ : CommSemiring R<VAR>S : Type v<VAR>inst✝² : CommSemiring S<VAR>p✝ q : ℕ<VAR>A : Type u_1<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>p : ℕ<VAR>P : R[X]<VAR>r : A<VAR>f g : R[X]<VAR>hf : (aeval r) ((expand R p) f) = (aeval (r ^ p)) f<VAR>hg : (aeval r) ((expand R p) g) = (aeval (r ^ p)) g<GOAL>(aeval r) ((expand R p) (f + g)) = (aeval (r ^ p)) (f + g)
<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>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>fst R M M₂ ⊔ snd R M M₂ = ⊤
<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>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>⊤ ≤ fst R M M₂ ⊔ snd R M M₂
<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>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<VAR>m : M<VAR>n : M₂<GOAL>(m, 0) + (0, n) ∈ fst R M M₂ ⊔ snd R M M₂
<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>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<VAR>m : M<VAR>n : M₂<GOAL>(m, 0) ∈ fst R M M₂ ⊔ snd R M M₂
<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>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<VAR>m : M<VAR>n : M₂<GOAL>(0, n) ∈ fst R M M₂ ⊔ snd R M M₂
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>s s₁ s₂ : Finset ι<VAR>i : ι<VAR>a : α<VAR>f g : ι → α<VAR>inst✝ : NonUnitalSemiring α<VAR>h : ∀ i ∈ s, a ∣ f i<VAR>y : α<VAR>hy : y ∈ Multiset.map (fun i => f i) s.val<GOAL>a ∣ y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>s s₁ s₂ : Finset ι<VAR>i : ι<VAR>a : α<VAR>f g : ι → α<VAR>inst✝ : NonUnitalSemiring α<VAR>h : ∀ i ∈ s, a ∣ f i<VAR>x : ι<VAR>hx : x ∈ s.val<VAR>hy : f x ∈ Multiset.map (fun i => f i) s.val<GOAL>a ∣ f x
<VAR>R : Type u_1<VAR>inst✝⁵ : Ring R<VAR>A : Type u_2<VAR>inst✝⁴ : CommRing A<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>U U₁ U₂ : Submodule R M<VAR>x x₁ x₂ y y₁ y₂ z z₁ z₂ : M<VAR>N : Type u_4<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>V V₁ V₂ : Submodule R N<GOAL>x ≡ y [SMOD ⊥] ↔ x = y
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α β : Type u_4<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsWellOrder α r<VAR>inst✝ : IsWellOrder β s<VAR>c : Ordinal.{u_4}<VAR>h : (type s).IsLimit<VAR>H : ∀ b' < type s, type r * b' ≤ c<VAR>l : c < type r * type s<GOAL>False
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α β : Type u_4<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsWellOrder α r<VAR>inst✝ : IsWellOrder β s<VAR>c : Ordinal.{u_4}<VAR>h : (type s).IsLimit<VAR>H : ∀ b' < type s, type r * b' ≤ c<VAR>l : c < type r * type s<GOAL>∀ (a : α) (b : β), Prod.Lex s r (b, a) (enum (Prod.Lex s r) c l)
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α β : Type u_4<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsWellOrder α r<VAR>inst✝ : IsWellOrder β s<VAR>c : Ordinal.{u_4}<VAR>h : (type s).IsLimit<VAR>H : ∀ b' < type s, type r * b' ≤ c<VAR>l : c < type r * type s<VAR>a : α<VAR>b : β<GOAL>Prod.Lex s r (b, a) (enum (Prod.Lex s r) c l)
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α β : Type u_4<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsWellOrder α r<VAR>inst✝ : IsWellOrder β s<VAR>c : Ordinal.{u_4}<VAR>h : (type s).IsLimit<VAR>H : ∀ b' < type s, type r * b' ≤ c<VAR>l : c < type r * type s<VAR>a : α<VAR>b : β<GOAL>typein (Prod.Lex s r) (b, a) < c
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α β : Type u_4<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsWellOrder α r<VAR>inst✝ : IsWellOrder β s<VAR>c : Ordinal.{u_4}<VAR>h : (type s).IsLimit<VAR>H : ∀ b' < type s, type r * b' ≤ c<VAR>l : c < type r * type s<VAR>a : α<VAR>b : β<VAR>this : type r * succ (typein s b) ≤ c<GOAL>typein (Prod.Lex s r) (b, a) < c
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α β : Type u_4<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsWellOrder α r<VAR>inst✝ : IsWellOrder β s<VAR>c : Ordinal.{u_4}<VAR>h : (type s).IsLimit<VAR>H : ∀ b' < type s, type r * b' ≤ c<VAR>l : c < type r * type s<VAR>a : α<VAR>b : β<VAR>this : type r * typein s b + type r ≤ c<GOAL>typein (Prod.Lex s r) (b, a) < c
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α β : Type u_4<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsWellOrder α r<VAR>inst✝ : IsWellOrder β s<VAR>c : Ordinal.{u_4}<VAR>h : (type s).IsLimit<VAR>H : ∀ b' < type s, type r * b' ≤ c<VAR>l : c < type r * type s<VAR>a : α<VAR>b : β<VAR>this✝ : type r * typein s b + type r ≤ c<VAR>this : type r * typein s b + typein r a < c<GOAL>typein (Prod.Lex s r) (b, a) < c
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α β : Type u_4<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsWellOrder α r<VAR>inst✝ : IsWellOrder β s<VAR>c : Ordinal.{u_4}<VAR>h : (type s).IsLimit<VAR>H : ∀ b' < type s, type r * b' ≤ c<VAR>l : c < type r * type s<VAR>a✝ : α<VAR>b : β<VAR>this✝ : type r * typein s b + type r ≤ c<VAR>this : type r * typein s b + typein r a✝ < c<VAR>a : ↑{b_1 | Prod.Lex s r b_1 (b, a✝)}<GOAL>↑{b_1 | s b_1 b} × α ⊕ ↑{b | r b a✝}
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α β : Type u_4<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsWellOrder α r<VAR>inst✝ : IsWellOrder β s<VAR>c : Ordinal.{u_4}<VAR>h : (type s).IsLimit<VAR>H : ∀ b' < type s, type r * b' ≤ c<VAR>l : c < type r * type s<VAR>a✝ : α<VAR>b✝ : β<VAR>this✝ : type r * typein s b✝ + type r ≤ c<VAR>this : type r * typein s b✝ + typein r a✝ < c<VAR>a b : ↑{b | Prod.Lex s r b (b✝, a✝)}<GOAL>Subrel (Prod.Lex s r) {b | Prod.Lex s r b (b✝, a✝)} a b → Sum.Lex (Prod.Lex (Subrel s {b | s b b✝}) r) (Subrel r {b | r b a✝}) ((fun a => ?m.90264 a) a) ((fun a => ?m.90264 a) b)
<VAR>n : ℕ<VAR>a : ℝ<VAR>h : (↑0 / ↑1).sqrtTwoAddSeries n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2<GOAL>a < π
<VAR>n : ℕ<VAR>a : ℝ<VAR>h : (↑0 / ↑1).sqrtTwoAddSeries n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2<GOAL>a ≤ 2 ^ (n + 1) * √(2 - sqrtTwoAddSeries 0 n)
<VAR>n : ℕ<VAR>a : ℝ<VAR>h : (↑0 / ↑1).sqrtTwoAddSeries n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2<GOAL>a ≤ √(2 - sqrtTwoAddSeries 0 n) * 2 ^ (n + 1)
<VAR>n : ℕ<VAR>a : ℝ<VAR>h : (↑0 / ↑1).sqrtTwoAddSeries n ≤ 2 - (a / 2 ^ (n + 1)) ^ 2<GOAL>(a / 2 ^ (n + 1)) ^ 2 ≤ 2 - sqrtTwoAddSeries 0 n
<VAR>n✝ m✝ n m : ℕ<VAR>a b : Fin m<GOAL>natAdd n a = natAdd n b → a = b
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>w : σ → M<VAR>n✝ : M<VAR>φ ψ : MvPolynomial σ R<VAR>n : M<VAR>r : R<GOAL>(weightedHomogeneousComponent w n) (C r * φ) = C r * (weightedHomogeneousComponent w n) φ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁵ : CommRing R₁<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>N L : Submodule R M<VAR>B : BilinForm K V<VAR>x : V<VAR>hx : ¬B.IsOrtho x x<GOAL>Submodule.span K {x} ⊔ B.orthogonal (Submodule.span K {x}) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁵ : CommRing R₁<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>N L : Submodule R M<VAR>B : BilinForm K V<VAR>x : V<VAR>hx : ¬B.IsOrtho x x<GOAL>Submodule.span K {x} ⊔ ker (B.toLinHomAux₁ x) = ⊤
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g : ℝ → ℝ<VAR>a✝ b✝ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → ℝ<VAR>a b : ℝ<VAR>hfi : IntervalIntegrable f volume a b<VAR>hpos : ∀ x ∈ Ioo a b, 0 < f x<VAR>hab : a < b<GOAL>0 < ∫ (x : ℝ) in a..b, f x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g : ℝ → ℝ<VAR>a✝ b✝ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → ℝ<VAR>a b : ℝ<VAR>hfi : IntervalIntegrable f volume a b<VAR>hpos : ∀ x ∈ Ioo a b, 0 < f x<VAR>hab : a < b<VAR>hsupp : Ioo a b ⊆ support f ∩ Ioc a b<GOAL>0 < ∫ (x : ℝ) in a..b, f x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g : ℝ → ℝ<VAR>a✝ b✝ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → ℝ<VAR>a b : ℝ<VAR>hfi : IntervalIntegrable f volume a b<VAR>hpos : ∀ x ∈ Ioo a b, 0 < f x<VAR>hab : a < b<VAR>hsupp : Ioo a b ⊆ support f ∩ Ioc a b<VAR>h₀ : 0 ≤ᶠ[ae (volume.restrict (Ι a b))] f<GOAL>0 < ∫ (x : ℝ) in a..b, f x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f✝ g : ℝ → ℝ<VAR>a✝ b✝ : ℝ<VAR>μ : Measure ℝ<VAR>f : ℝ → ℝ<VAR>a b : ℝ<VAR>hfi : IntervalIntegrable f volume a b<VAR>hpos : ∀ x ∈ Ioo a b, 0 < f x<VAR>hab : a < b<VAR>hsupp : Ioo a b ⊆ support f ∩ Ioc a b<VAR>h₀ : 0 ≤ᶠ[ae (volume.restrict (Ι a b))] f<GOAL>a < b ∧ 0 < volume (support f ∩ Ioc a b)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<GOAL>∡ p₁ p₂ p₃ = ↑π ↔ Sbtw ℝ p₁ p₂ p₃
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : Preorder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : Topology.IsLowerSet α<VAR>s : Set α<VAR>a : α<GOAL>closure {a} = Ici a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : Preorder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : Topology.IsLowerSet α<VAR>s : Set α<VAR>a : α<GOAL>↑(UpperSet.Ici a) = Ici a
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>δ✝ : ℝ<VAR>s : Set α<VAR>x✝ : α<VAR>X : Type u<VAR>inst✝ : PseudoMetricSpace X<VAR>x : X<VAR>E : Set X<VAR>hx : x ∈ E<VAR>δ : ℝ<GOAL>ball x δ ⊆ thickening δ {x}
<VAR>R S T : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : CommRing T<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra R T<GOAL>(pullbackSpecIso R S T).hom ≫ Spec.map (ofHom ↑includeRight) = pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R T)))
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>p : M → Prop<VAR>hp₀ : p 1<VAR>hp₁ : ∀ (x y : M), p x → p y → p (x * y)<VAR>hp₂ : ∀ (i : α), p (f i)<GOAL>p (∏ᶠ (i : α), f i)
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>p : M → Prop<VAR>hp₀ : p 1<VAR>hp₁ : ∀ (x y : M), p x → p y → p (x * y)<VAR>hp₂ : ∀ (i : α), p (f i)<GOAL>p (if h : (mulSupport ((fun i => f i) ∘ PLift.down)).Finite then ∏ i ∈ h.toFinset, f i.down else 1)
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>p : M → Prop<VAR>hp₀ : p 1<VAR>hp₁ : ∀ (x y : M), p x → p y → p (x * y)<VAR>hp₂ : ∀ (i : α), p (f i)<VAR>h✝ : (mulSupport ((fun i => f i) ∘ PLift.down)).Finite<GOAL>p (∏ i ∈ h✝.toFinset, f i.down)
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>p : M → Prop<VAR>hp₀ : p 1<VAR>hp₁ : ∀ (x y : M), p x → p y → p (x * y)<VAR>hp₂ : ∀ (i : α), p (f i)<VAR>h✝ : ¬(mulSupport ((fun i => f i) ∘ PLift.down)).Finite<GOAL>p 1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>h : X ≃ₜ Y<GOAL>Inducing (⇑h.symm ∘ ⇑h)
<VAR>α : Type u_1<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<VAR>P : Finpartition a<VAR>Q : (i : α) → i ∈ P.parts → Finpartition i<GOAL>b ∈ (P.bind Q).parts ↔ ∃ A, ∃ (hA : A ∈ P.parts), b ∈ (Q A hA).parts