ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁷ : OrderedRing R<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : Module R V<VAR>inst✝⁴ : AddTorsor V P<VAR>inst✝³ : AddCommGroup V'<VAR>inst✝² : Module R V'<VAR>inst✝¹ : AddTorsor V' P'<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>x y z : P<VAR>h : Wbtw R x y z<GOAL>Wbtw R y x z ↔ x = y
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>f g : α → α<VAR>h : Commute f g<VAR>hf : Monotone f<VAR>hg : StrictMono g<VAR>x : α<VAR>hx : f x < g x<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>f^[n] x < g^[n] x
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>f g : α → α<VAR>h : Commute f g<VAR>hf : Monotone f<VAR>hg : StrictMono g<VAR>x : α<VAR>hx : f x < g x<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>f^[0] x ≤ g^[0] x
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>f g : α → α<VAR>h : Commute f g<VAR>hf : Monotone f<VAR>hg : StrictMono g<VAR>x : α<VAR>hx : f x < g x<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>∀ (k : ℕ), k < n → f^[k + 1] x ≤ f (f^[k] x)
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>f g : α → α<VAR>h : Commute f g<VAR>hf : Monotone f<VAR>hg : StrictMono g<VAR>x : α<VAR>hx : f x < g x<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>∀ (k : ℕ), k < n → f (g^[k] x) < g^[k + 1] x
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m✝ : MeasurableSpace Ω<VAR>inst✝¹ : ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n i : ι<VAR>ω : Ω<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>m : ι<VAR>h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s<GOAL>u (hitting u s n m ω) ω ∈ s
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m✝ : MeasurableSpace Ω<VAR>inst✝¹ : ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n i : ι<VAR>ω : Ω<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>m : ι<VAR>h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s<GOAL>u (sInf (Set.Icc n m ∩ {i | u i ω ∈ s})) ω ∈ s
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m✝ : MeasurableSpace Ω<VAR>inst✝¹ : ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n i : ι<VAR>ω : Ω<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>m : ι<VAR>h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s<VAR>h_nonempty : (Set.Icc n m ∩ {i | u i ω ∈ s}).Nonempty<GOAL>u (sInf (Set.Icc n m ∩ {i | u i ω ∈ s})) ω ∈ s
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m✝ : MeasurableSpace Ω<VAR>inst✝¹ : ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n i : ι<VAR>ω : Ω<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>m : ι<VAR>h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s<VAR>h_nonempty : (Set.Icc n m ∩ {i | u i ω ∈ s}).Nonempty<VAR>h_mem : sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ∈ Set.Icc n m ∩ {i | u i ω ∈ s}<GOAL>u (sInf (Set.Icc n m ∩ {i | u i ω ∈ s})) ω ∈ s
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m✝ : MeasurableSpace Ω<VAR>inst✝¹ : ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n i : ι<VAR>ω : Ω<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>m : ι<VAR>h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s<VAR>h_nonempty : (Set.Icc n m ∩ {i | u i ω ∈ s}).Nonempty<VAR>h_mem : sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ∈ Set.Icc n m ∧ sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ∈ {i | u i ω ∈ s}<GOAL>u (sInf (Set.Icc n m ∩ {i | u i ω ∈ s})) ω ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Rel α β<VAR>J : Set α<GOAL>R.leftDual J ∈ R.rightFixedPoints
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Rel α β<VAR>J : Set α<GOAL>R.leftDual (R.rightDual (R.leftDual J)) ≤ R.leftDual J
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Rel α β<VAR>J : Set α<GOAL>R.leftDual J ≤ R.leftDual (R.rightDual (R.leftDual J))
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommMonoid M✝<VAR>inst✝¹ : NonAssocSemiring R<VAR>M : Type u_4<VAR>inst✝ : CommMonoid M<VAR>f : ℕ → ℕ → M<VAR>n : ℕ<GOAL>∏ ij ∈ antidiagonal (n + 1), f ij.1 ij.2 ^ (n + 1).choose ij.1 = (∏ ij ∈ antidiagonal n, f ij.1 (ij.2 + 1) ^ n.choose ij.1) * ∏ ij ∈ antidiagonal n, f (ij.1 + 1) ij.2 ^ n.choose ij.2
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommMonoid M✝<VAR>inst✝¹ : NonAssocSemiring R<VAR>M : Type u_4<VAR>inst✝ : CommMonoid M<VAR>f : ℕ → ℕ → M<VAR>n : ℕ<GOAL>(∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i) * ∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i = (∏ x ∈ range n.succ, f x (n - x + 1) ^ n.choose x) * ∏ x ∈ range n.succ, f (x + 1) (n - x) ^ n.choose (n - x)
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommMonoid M✝<VAR>inst✝¹ : NonAssocSemiring R<VAR>M : Type u_4<VAR>inst✝ : CommMonoid M<VAR>f : ℕ → ℕ → M<VAR>n : ℕ<VAR>this : ∀ i ∈ range (n + 1), i ≤ n<GOAL>(∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i) * ∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i = (∏ x ∈ range n.succ, f x (n - x + 1) ^ n.choose x) * ∏ x ∈ range n.succ, f (x + 1) (n - x) ^ n.choose (n - x)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<GOAL>HasCompactSupport u
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<GOAL>IsCompact (closedBall 0 1)
<VAR>x✝ y x : ℝ<VAR>hx : 0 < x<GOAL>log x ≤ x - 1
<VAR>x✝ y x : ℝ<VAR>hx : 0 < x<GOAL>log x + 1 ≤ x
<VAR>x✝ y x : ℝ<VAR>hx : 0 < x<GOAL>x = rexp (log x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s t✝ : Set E<VAR>hs : Convex 𝕜 s<VAR>x : E<VAR>zero_mem : 0 ∈ s<VAR>hx : x ∈ s<VAR>t : 𝕜<VAR>ht : t ∈ Icc 0 1<GOAL>t • x ∈ s
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>f : LaurentSeries K<GOAL>Valued.v f ≤ 1 ↔ ∃ F, (ofPowerSeries ℤ K) F = f
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>f : LaurentSeries K<GOAL>(∀ n < 0, f.coeff n = 0) ↔ ∃ F, (ofPowerSeries ℤ K) F = f
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>f : LaurentSeries K<VAR>h : ∀ n < 0, f.coeff n = 0<VAR>n : ℕ<GOAL>((ofPowerSeries ℤ K) (PowerSeries.mk fun n => f.coeff ↑n)).coeff (Int.negSucc n) = f.coeff (Int.negSucc n)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>f : LaurentSeries K<GOAL>(∃ F, (ofPowerSeries ℤ K) F = f) → ∀ n < 0, f.coeff n = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>f : LaurentSeries K<VAR>h : ∀ n < 0, f.coeff n = 0<VAR>n : ℕ<GOAL>((ofPowerSeries ℤ K) (PowerSeries.mk fun n => f.coeff ↑n)).coeff (Int.negSucc n) = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>F : K⟦X⟧<VAR>n✝ : ℤ<VAR>a✝ : n✝ < 0<GOAL>((ofPowerSeries ℤ K) F).coeff n✝ = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>f : LaurentSeries K<VAR>h : ∀ n < 0, f.coeff n = 0<VAR>n x✝ : ℕ<GOAL>¬False
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>F : K⟦X⟧<VAR>n✝ : ℤ<VAR>a✝ : n✝ < 0<VAR>x✝ : ℕ<GOAL>¬↑x✝ = n✝
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S✝ : Type u_4<VAR>T : Type u_5<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : CommRing A<VAR>inst✝¹¹ : Ring B<VAR>inst✝¹⁰ : CommRing S✝<VAR>inst✝⁹ : CommRing T<VAR>inst✝⁸ : Algebra A B<VAR>inst✝⁷ : Algebra R✝ B<VAR>f : R✝ →+* S✝<VAR>g : S✝ →+* T<VAR>inst✝⁶ : Algebra R✝ A<VAR>inst✝⁵ : IsScalarTower R✝ A B<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra.IsIntegral R S<VAR>hR : IsField R<GOAL>IsField S
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S✝ : Type u_4<VAR>T : Type u_5<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : CommRing A<VAR>inst✝¹¹ : Ring B<VAR>inst✝¹⁰ : CommRing S✝<VAR>inst✝⁹ : CommRing T<VAR>inst✝⁸ : Algebra A B<VAR>inst✝⁷ : Algebra R✝ B<VAR>f : R✝ →+* S✝<VAR>g : S✝ →+* T<VAR>inst✝⁶ : Algebra R✝ A<VAR>inst✝⁵ : IsScalarTower R✝ A B<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra.IsIntegral R S<VAR>hR : IsField R<VAR>x : S<VAR>hx : x ≠ 0<GOAL>∃ b, x * b = 1
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S✝ : Type u_4<VAR>T : Type u_5<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : CommRing A<VAR>inst✝¹¹ : Ring B<VAR>inst✝¹⁰ : CommRing S✝<VAR>inst✝⁹ : CommRing T<VAR>inst✝⁸ : Algebra A B<VAR>inst✝⁷ : Algebra R✝ B<VAR>f : R✝ →+* S✝<VAR>g : S✝ →+* T<VAR>inst✝⁶ : Algebra R✝ A<VAR>inst✝⁵ : IsScalarTower R✝ A B<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra.IsIntegral R S<VAR>hR : IsField R<VAR>x : S<VAR>hx : x ≠ 0<VAR>this : Module.Finite R ↥(adjoin R {x})<GOAL>∃ b, x * b = 1
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S✝ : Type u_4<VAR>T : Type u_5<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : CommRing A<VAR>inst✝¹¹ : Ring B<VAR>inst✝¹⁰ : CommRing S✝<VAR>inst✝⁹ : CommRing T<VAR>inst✝⁸ : Algebra A B<VAR>inst✝⁷ : Algebra R✝ B<VAR>f : R✝ →+* S✝<VAR>g : S✝ →+* T<VAR>inst✝⁶ : Algebra R✝ A<VAR>inst✝⁵ : IsScalarTower R✝ A B<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra.IsIntegral R S<VAR>hR : IsField R<VAR>x : S<VAR>hx : x ≠ 0<VAR>this✝ : Module.Finite R ↥(adjoin R {x})<VAR>this : Field R := hR.toField<GOAL>∃ b, x * b = 1
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S✝ : Type u_4<VAR>T : Type u_5<VAR>inst✝¹³ : CommRing R✝<VAR>inst✝¹² : CommRing A<VAR>inst✝¹¹ : Ring B<VAR>inst✝¹⁰ : CommRing S✝<VAR>inst✝⁹ : CommRing T<VAR>inst✝⁸ : Algebra A B<VAR>inst✝⁷ : Algebra R✝ B<VAR>f : R✝ →+* S✝<VAR>g : S✝ →+* T<VAR>inst✝⁶ : Algebra R✝ A<VAR>inst✝⁵ : IsScalarTower R✝ A B<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra.IsIntegral R S<VAR>hR : IsField R<VAR>x : S<VAR>hx : x ≠ 0<VAR>this✝ : Module.Finite R ↥(adjoin R {x})<VAR>this : Field R := hR.toField<VAR>y : ↥(adjoin R {x})<VAR>hy : ⟨x, ⋯⟩ * y = 1<GOAL>∃ b, x * b = 1
<VAR>x y : ℝ<GOAL>↑(cos x ^ 2) = ↑(1 / 2 + cos (2 * x) / 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<GOAL>(fun i => if MeasurableSet i then μ i else 0) ∅ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>x✝ : ℕ → Set α<VAR>hf₁ : ∀ (i : ℕ), MeasurableSet (x✝ i)<VAR>hf₂ : Pairwise (Disjoint on x✝)<GOAL>HasSum (fun i => if MeasurableSet (x✝ i) then μ (x✝ i) else 0) (if MeasurableSet (⋃ i, x✝ i) then μ (⋃ i, x✝ i) else 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>x✝ : ℕ → Set α<VAR>hf₁ : ∀ (i : ℕ), MeasurableSet (x✝ i)<VAR>hf₂ : Pairwise (Disjoint on x✝)<GOAL>(∑' (b : ℕ), if MeasurableSet (x✝ b) then μ (x✝ b) else 0) = ∑' (i : ℕ), μ (x✝ i)
<VAR>z : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<GOAL>Continuous ⇑normSq
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>X₁ : ι → V<VAR>d₁ : (i j : ι) → X₁ i ⟶ X₁ j<VAR>s₁ : ∀ (i j : ι), ¬c.Rel i j → d₁ i j = 0<VAR>h₁ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₁ i j ≫ d₁ j k = 0<VAR>d₂ : (i j : ι) → X₁ i ⟶ X₁ j<VAR>s₂ : ∀ (i j : ι), ¬c.Rel i j → d₂ i j = 0<VAR>h₂ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₂ i j ≫ d₂ j k = 0<VAR>h_d : ∀ (i j : ι), c.Rel i j → { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ }.d i j ≫ eqToHom ⋯ = eqToHom ⋯ ≫ { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ }.d i j<GOAL>{ X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ } = { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ }
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>X₁ : ι → V<VAR>d₁ : (i j : ι) → X₁ i ⟶ X₁ j<VAR>s₁ : ∀ (i j : ι), ¬c.Rel i j → d₁ i j = 0<VAR>h₁ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₁ i j ≫ d₁ j k = 0<VAR>d₂ : (i j : ι) → X₁ i ⟶ X₁ j<VAR>s₂ : ∀ (i j : ι), ¬c.Rel i j → d₂ i j = 0<VAR>h₂ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₂ i j ≫ d₂ j k = 0<VAR>h_d : ∀ (i j : ι), c.Rel i j → { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ }.d i j ≫ eqToHom ⋯ = eqToHom ⋯ ≫ { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ }.d i j<GOAL>d₁ = d₂
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>i j : x.LeftMoves<VAR>k : y.LeftMoves<VAR>l : (-y).LeftMoves<GOAL>⟦x.mulOption y i k⟧ < -⟦x.mulOption (-y) j l⟧ ↔ P1 (x.moveLeft i) x (x.moveLeft j) y (y.moveLeft k) (-(-y).moveLeft l)
<VAR>x x₁ x₂ x₃ x' y y₁ y₂ y₃ y' : PGame<VAR>i j : x.LeftMoves<VAR>k : y.LeftMoves<VAR>l : (-y).LeftMoves<GOAL>⟦x.moveLeft i * y⟧ + ⟦x * y.moveLeft k⟧ - ⟦x.moveLeft i * y.moveLeft k⟧ < -(⟦x.moveLeft j * -y⟧ + ⟦x * (-y).moveLeft l⟧ - ⟦x.moveLeft j * (-y).moveLeft l⟧) ↔ ⟦x.moveLeft i * y⟧ + ⟦x * y.moveLeft k⟧ - ⟦x.moveLeft i * y.moveLeft k⟧ < ⟦x.moveLeft j * y⟧ + ⟦x * -(-y).moveLeft l⟧ - ⟦x.moveLeft j * -(-y).moveLeft l⟧
<VAR>m✝ n✝ m n : ℕ<VAR>nzm : NeZero m<VAR>a : ZMod m<VAR>h : a.val < n<VAR>nzn : NeZero n<GOAL>a.cast.val = a.val
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_7<VAR>inst✝ : SeminormedAddCommGroup β<VAR>T T' : Set α → β<VAR>C C' : ℝ<VAR>μ' : Measure α<VAR>h : μ ≤ μ'<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hC : 0 ≤ C<GOAL>DominatedFinMeasAdditive μ' T C
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_7<VAR>inst✝ : SeminormedAddCommGroup β<VAR>T T' : Set α → β<VAR>C C' : ℝ<VAR>μ' : Measure α<VAR>h : μ ≤ μ'<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hC : 0 ≤ C<VAR>h' : ∀ (s : Set α), μ s = ⊤ → μ' s = ⊤<GOAL>DominatedFinMeasAdditive μ' T C
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_7<VAR>inst✝ : SeminormedAddCommGroup β<VAR>T T' : Set α → β<VAR>C C' : ℝ<VAR>μ' : Measure α<VAR>h : μ ≤ μ'<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hC : 0 ≤ C<VAR>h' : ∀ (s : Set α), μ s = ⊤ → μ' s = ⊤<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμ's : μ' s < ⊤<GOAL>‖T s‖ ≤ C * (μ' s).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>β : Type u_7<VAR>inst✝ : SeminormedAddCommGroup β<VAR>T T' : Set α → β<VAR>C C' : ℝ<VAR>μ' : Measure α<VAR>h : μ ≤ μ'<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hC : 0 ≤ C<VAR>h' : ∀ (s : Set α), μ s = ⊤ → μ' s = ⊤<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμ's : μ' s < ⊤<VAR>hμs : μ s < ⊤<GOAL>‖T s‖ ≤ C * (μ' s).toReal
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>p : Type u_4<VAR>n' : m → Type u_5<VAR>𝔸 : Type u_6<VAR>inst✝⁹ : RCLike 𝕂<VAR>inst✝⁸ : Fintype m<VAR>inst✝⁷ : DecidableEq m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : (i : m) → Fintype (n' i)<VAR>inst✝³ : (i : m) → DecidableEq (n' i)<VAR>inst✝² : NormedRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕂 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>A B : Matrix m m 𝔸<VAR>h : Commute A B<VAR>this✝¹ : SeminormedRing (Matrix m m 𝔸) := Matrix.linftyOpSemiNormedRing<VAR>this✝ : NormedRing (Matrix m m 𝔸) := Matrix.linftyOpNormedRing<VAR>this : NormedAlgebra 𝕂 (Matrix m m 𝔸) := Matrix.linftyOpNormedAlgebra<GOAL>exp 𝕂 (A + B) = exp 𝕂 A * exp 𝕂 B
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>F : ι → Submodule 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>hK : CompleteSpace ↥K<VAR>this : ∀ (b : Bool), CompleteSpace ↥(bif b then K else Kᗮ)<GOAL>IsHilbertSum 𝕜 (fun b => ↥(bif b then K else Kᗮ)) fun b => (bif b then K else Kᗮ).subtypeₗᵢ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>F : ι → Submodule 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>hK : CompleteSpace ↥K<VAR>this : ∀ (b : Bool), CompleteSpace ↥(bif b then K else Kᗮ)<GOAL>⊤ ≤ (⨆ i, bif i then K else Kᗮ).topologicalClosure
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>F : ι → Submodule 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>hK : CompleteSpace ↥K<VAR>this : ∀ (b : Bool), CompleteSpace ↥(bif b then K else Kᗮ)<GOAL>⊤ ≤ ⨆ i, bif i then K else Kᗮ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>F : ι → Submodule 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>hK : CompleteSpace ↥K<VAR>this : ∀ (b : Bool), CompleteSpace ↥(bif b then K else Kᗮ)<GOAL>⊤ ≤ (match true with | true => K | false => Kᗮ) ⊔ match false with | true => K | false => Kᗮ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>F : ι → Submodule 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>hK : CompleteSpace ↥K<VAR>this : ∀ (b : Bool), CompleteSpace ↥(bif b then K else Kᗮ)<GOAL>Codisjoint (match true with | true => K | false => Kᗮ) (match false with | true => K | false => Kᗮ)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>F : J ⥤ CommRingCat<VAR>j j' : J<VAR>f : j ⟶ j'<VAR>x : ↑(F.obj j)<GOAL>(coconeMorphism F j') ((F.map f) x) = (coconeMorphism F j) x
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>f : J → C<VAR>inst✝¹ : HasBiproduct f<VAR>p : J → Prop<VAR>inst✝ : HasBiproduct (Subtype.restrict p f)<VAR>j j✝ : Subtype p<GOAL>(ι f ↑j ≫ toSubtype f p) ≫ π (Subtype.restrict p f) j✝ = ι (Subtype.restrict p f) j ≫ π (Subtype.restrict p f) j✝
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>f : J → C<VAR>inst✝¹ : HasBiproduct f<VAR>p : J → Prop<VAR>inst✝ : HasBiproduct (Subtype.restrict p f)<VAR>j j✝ : Subtype p<GOAL>(if h : ↑j = ↑j✝ then eqToHom ⋯ else 0) = if h : j = j✝ then eqToHom ⋯ else 0
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>f : J → C<VAR>inst✝¹ : HasBiproduct f<VAR>p : J → Prop<VAR>inst✝ : HasBiproduct (Subtype.restrict p f)<VAR>j j✝ : Subtype p<VAR>h₁ : ↑j = ↑j✝<VAR>h₂ : j = j✝<GOAL>eqToHom ⋯ = eqToHom ⋯
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>f : J → C<VAR>inst✝¹ : HasBiproduct f<VAR>p : J → Prop<VAR>inst✝ : HasBiproduct (Subtype.restrict p f)<VAR>j j✝ : Subtype p<VAR>h₁ : ↑j = ↑j✝<VAR>h₂ : ¬j = j✝<GOAL>eqToHom ⋯ = 0
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>f : J → C<VAR>inst✝¹ : HasBiproduct f<VAR>p : J → Prop<VAR>inst✝ : HasBiproduct (Subtype.restrict p f)<VAR>j j✝ : Subtype p<VAR>h₁ : ¬↑j = ↑j✝<VAR>h₂ : j = j✝<GOAL>0 = eqToHom ⋯
<VAR>J : Type w<VAR>K : Type u_1<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>f : J → C<VAR>inst✝¹ : HasBiproduct f<VAR>p : J → Prop<VAR>inst✝ : HasBiproduct (Subtype.restrict p f)<VAR>j j✝ : Subtype p<VAR>h₁ : ¬↑j = ↑j✝<VAR>h₂ : ¬j = j✝<GOAL>0 = 0
<VAR>this : 1 + √5 ≠ 0<GOAL>φ⁻¹ = -ψ
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>s : Set α<VAR>h : s.Countable<VAR>default x : α<VAR>hx : x ∈ s<VAR>this : Encodable ↑s := h.toEncodable<GOAL>enumerateCountable h default (encode ⟨x, hx⟩) = x
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : FunLike F G H<VAR>a : G<VAR>b : H<VAR>inst✝² : AddMonoidWithOne G<VAR>inst✝¹ : AddMonoid H<VAR>inst✝ : AddConstMapClass F G H 1 b<VAR>f : F<VAR>x : G<VAR>n : ℕ<GOAL>f (x + ↑n) = f x + n • b
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F✝ : C ⥤ Type w<VAR>F : Cᵒᵖ ⥤ Type v<GOAL>(toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F = 𝟭 F.Elements
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F✝ : C ⥤ Type w<VAR>F : Cᵒᵖ ⥤ Type v<GOAL>∀ (X : F.Elements), ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).obj X = (𝟭 F.Elements).obj X
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F✝ : C ⥤ Type w<VAR>F : Cᵒᵖ ⥤ Type v<GOAL>∀ (X Y : F.Elements) (f : X ⟶ Y), ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).map f = eqToHom ⋯ ≫ (𝟭 F.Elements).map f ≫ eqToHom ⋯
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Nontrivial α<GOAL>2 * card ↥(alternatingGroup α) = card (Perm α)
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Nontrivial α<VAR>this : Perm α ⧸ sign.ker ≃ ℤˣ := (QuotientGroup.quotientKerEquivOfSurjective sign ⋯).toEquiv<GOAL>2 * card ↥(alternatingGroup α) = card (Perm α)
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Nontrivial α<VAR>this : Perm α ⧸ sign.ker ≃ ℤˣ := (QuotientGroup.quotientKerEquivOfSurjective sign ⋯).toEquiv<GOAL>card (Perm α ⧸ sign.ker) * card ↥(alternatingGroup α) = card (Perm α)
<VAR>α : Type u_1<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Nontrivial α<VAR>this : Perm α ⧸ sign.ker ≃ ℤˣ := (QuotientGroup.quotientKerEquivOfSurjective sign ⋯).toEquiv<GOAL>Nat.card (Perm α ⧸ sign.ker) * Nat.card ↥(alternatingGroup α) = Nat.card (Perm α)
<VAR>m n✝ i n : ℕ<GOAL>i + (n + 1)! ≤ (i + (n + 1))!
<VAR>m n✝ i n : ℕ<VAR>h✝ : 2 ≤ i<GOAL>i + (n + 1)! ≤ (i + (n + 1))!
<VAR>m n✝ i n : ℕ<VAR>h✝ : i < 2<GOAL>i + (n + 1)! ≤ (i + (n + 1))!
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>c : CokernelCofork f<VAR>G : C ⥤ D<VAR>inst✝ : G.PreservesZeroMorphisms<GOAL>G.map f ≫ G.map (Cofork.π c) = 0
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ ψ : L.BoundedFormula α n<VAR>h : T.SemanticallyEquivalent φ ψ<GOAL>T.SemanticallyEquivalent (∼φ) ∼ψ
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ ψ : L.BoundedFormula α n<VAR>h : T.SemanticallyEquivalent φ ψ<GOAL>∀ (M : T.ModelType) (v : α → ↑M) (xs : Fin n → ↑M), ¬φ.Realize v xs ↔ ¬ψ.Realize v xs
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : Zero 𝕜<VAR>inst✝² : Zero β<VAR>inst✝¹ : SMulWithZero 𝕜 β<VAR>inst✝ : ContinuousConstSMul 𝕜 β<VAR>l : Filter α<VAR>f : α → β<VAR>c : 𝕜<VAR>hf : l.ZeroAtFilter f<GOAL>l.ZeroAtFilter (c • f)
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizedGCDMonoid α<VAR>inst✝ : DecidableEq α<VAR>s₁ s₂ : Multiset α<GOAL>(s₁.ndunion s₂).lcm = GCDMonoid.lcm s₁.lcm s₂.lcm