ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>c : Computation (WSeq α)<GOAL>Computation.IsBisimulation fun c1 c2 => c1 = c2 ∨ ∃ c, c1 = (flatten c).destruct ∧ c2 = c.bind destruct
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝ : LinearOrderedRing R<VAR>a b : R<VAR>n : ℕ<VAR>hb : b ≠ 0<VAR>he : Even n<VAR>this : a ^ n > -b ^ n<GOAL>a ^ n = -b ^ n ↔ a = -b ∧ Odd n
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝ : LinearOrderedRing R<VAR>a b : R<VAR>n : ℕ<VAR>hb : b ≠ 0<VAR>he : Even n<GOAL>-b ^ n < 0
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝ : LinearOrderedRing R<VAR>a b : R<VAR>n : ℕ<VAR>hb : b ≠ 0<VAR>ho : Odd n<GOAL>a ^ n = -b ^ n ↔ a = -b ∧ Odd n
<VAR>n : ℕ<GOAL>powHalf (n + 1) + powHalf (n + 1) ≈ powHalf n
<VAR>n : ℕ<VAR>hn : ∀ m < n, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m<GOAL>powHalf (n + 1) + powHalf (n + 1) ≈ powHalf n
<VAR>n : ℕ<VAR>hn : ∀ m < n, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m<GOAL>∀ (i : (powHalf (n + 1) + powHalf (n + 1)).LeftMoves), (powHalf (n + 1) + powHalf (n + 1)).moveLeft i ⧏ powHalf n
<VAR>n : ℕ<VAR>hn : ∀ m < n, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m<GOAL>∀ (j : (powHalf n).RightMoves), powHalf (n + 1) + powHalf (n + 1) ⧏ (powHalf n).moveRight j
<VAR>n : ℕ<VAR>hn : ∀ m < n, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m<GOAL>∀ (i : (powHalf n).LeftMoves), (powHalf n).moveLeft i ⧏ powHalf (n + 1) + powHalf (n + 1)
<VAR>n : ℕ<VAR>hn : ∀ m < n, powHalf (m + 1) + powHalf (m + 1) ≈ powHalf m<GOAL>∀ (j : (powHalf (n + 1) + powHalf (n + 1)).RightMoves), powHalf n ⧏ (powHalf (n + 1) + powHalf (n + 1)).moveRight j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>a a₁ a₂ b b₁ b₂ c d x : α<GOAL>MonotoneOn f s ∨ AntitoneOn f s ↔ ∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, c ∈ [[a, b]] → f c ∈ [[f a, f b]]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>r : ℝ≥0∞<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<GOAL>∫⁻ (a : α), f a * r ∂μ = (∫⁻ (a : α), f a ∂μ) * r
<VAR>n : ℕ<GOAL>orderOf (a 1) = 2 * n
<VAR>n : ℕ<VAR>hn : n = 0<GOAL>orderOf (a 1) = 2 * n
<VAR>n : ℕ<VAR>hn : NeZero n<GOAL>orderOf (a 1) = 2 * n
<VAR>n : ℕ<VAR>hn : NeZero n<GOAL>¬orderOf (a 1) < 2 * n
<VAR>n : ℕ<VAR>hn : NeZero n<VAR>h : orderOf (a 1) < 2 * n<GOAL>False
<VAR>n : ℕ<VAR>hn : NeZero n<VAR>h : orderOf (a 1) < 2 * n<VAR>h1 : a 1 ^ orderOf (a 1) = 1<GOAL>False
<VAR>n : ℕ<VAR>hn : NeZero n<VAR>h : orderOf (a 1) < 2 * n<VAR>h1 : a ↑(orderOf (a 1)) = 1<GOAL>False
<VAR>n : ℕ<VAR>hn : NeZero n<VAR>h : orderOf (a 1) < 2 * n<VAR>h2 : ↑(orderOf (a 1)) = 0<GOAL>False
<VAR>n : ℕ<VAR>hn : NeZero n<VAR>h : orderOf (a 1) < 2 * n<VAR>h2 : orderOf (a 1) = 0<GOAL>False
<VAR>α : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : NoZeroDivisors α<VAR>m n✝ n : ℕ<VAR>R : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n<VAR>a b c : R<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>hc : c ≠ 0<VAR>habc : a ^ n + b ^ n = c ^ n<VAR>s : Finset R := {a, b, c}<VAR>d : R := s.gcd id<GOAL>False
<VAR>α : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : NoZeroDivisors α<VAR>m n✝ n : ℕ<VAR>R : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n<VAR>a b c : R<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>hc : c ≠ 0<VAR>habc : a ^ n + b ^ n = c ^ n<VAR>s : Finset R := {a, b, c}<VAR>d : R := s.gcd id<VAR>A : R<VAR>hA : a = d * A<GOAL>False
<VAR>α : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : NoZeroDivisors α<VAR>m n✝ n : ℕ<VAR>R : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n<VAR>a b c : R<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>hc : c ≠ 0<VAR>habc : a ^ n + b ^ n = c ^ n<VAR>s : Finset R := {a, b, c}<VAR>d : R := s.gcd id<VAR>A : R<VAR>hA : a = d * A<VAR>B : R<VAR>hB : b = d * B<GOAL>False
<VAR>α : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : NoZeroDivisors α<VAR>m n✝ n : ℕ<VAR>R : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n<VAR>a b c : R<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>hc : c ≠ 0<VAR>habc : a ^ n + b ^ n = c ^ n<VAR>s : Finset R := {a, b, c}<VAR>d : R := s.gcd id<VAR>A : R<VAR>hA : a = d * A<VAR>B : R<VAR>hB : b = d * B<VAR>C : R<VAR>hC : c = d * C<GOAL>False
<VAR>α : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : NoZeroDivisors α<VAR>m n✝ n : ℕ<VAR>R : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n<VAR>a b c : R<VAR>s : Finset R := {a, b, c}<VAR>d : R := s.gcd id<VAR>A : R<VAR>hA : a = d * A<VAR>B : R<VAR>hB : b = d * B<VAR>C : R<VAR>hC : c = d * C<VAR>ha : d ≠ 0 ∧ A ≠ 0<VAR>hb : d ≠ 0 ∧ B ≠ 0<VAR>hc : d ≠ 0 ∧ C ≠ 0<VAR>habc : d ^ n * A ^ n + d ^ n * B ^ n = d ^ n * C ^ n<GOAL>False
<VAR>α : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : NoZeroDivisors α<VAR>m n✝ n : ℕ<VAR>R : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n<VAR>a b c : R<VAR>s : Finset R := {a, b, c}<VAR>d : R := s.gcd id<VAR>A : R<VAR>hA : a = d * A<VAR>B : R<VAR>hB : b = d * B<VAR>C : R<VAR>hC : c = d * C<VAR>ha : d ≠ 0 ∧ A ≠ 0<VAR>hb : d ≠ 0 ∧ B ≠ 0<VAR>hc : d ≠ 0 ∧ C ≠ 0<VAR>habc : A ^ n + B ^ n = C ^ n<GOAL>False
<VAR>α : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : NoZeroDivisors α<VAR>m n✝ n : ℕ<VAR>R : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n<VAR>a b c : R<VAR>s : Finset R := {a, b, c}<VAR>d : R := s.gcd id<VAR>A : R<VAR>hA : a = d * A<VAR>B : R<VAR>hB : b = d * B<VAR>C : R<VAR>hC : c = d * C<VAR>ha : d ≠ 0 ∧ A ≠ 0<VAR>hb : d ≠ 0 ∧ B ≠ 0<VAR>hc : d ≠ 0 ∧ C ≠ 0<VAR>habc : A ^ n + B ^ n = C ^ n<GOAL>{A, B, C}.gcd id = 1
<VAR>α : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : NoZeroDivisors α<VAR>m n✝ n : ℕ<VAR>R : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n<VAR>a b c : R<VAR>s : Finset R := {a, b, c}<VAR>d : R := s.gcd id<VAR>A : R<VAR>hA : a = d * A<VAR>B : R<VAR>hB : b = d * B<VAR>C : R<VAR>hC : c = d * C<VAR>ha : d ≠ 0 ∧ A ≠ 0<VAR>hb : d ≠ 0 ∧ B ≠ 0<VAR>hc : d ≠ 0 ∧ C ≠ 0<VAR>habc : A ^ n + B ^ n = C ^ n<GOAL>IsUnit ({A, B, C}.gcd id)
<VAR>α : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : NoZeroDivisors α<VAR>m n✝ n : ℕ<VAR>R : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n<VAR>a b c : R<VAR>s : Finset R := {a, b, c}<VAR>d : R := s.gcd id<VAR>A : R<VAR>hA : a = d * A<VAR>B : R<VAR>hB : b = d * B<VAR>C : R<VAR>hC : c = d * C<VAR>ha : d ≠ 0 ∧ A ≠ 0<VAR>hb : d ≠ 0 ∧ B ≠ 0<VAR>hc : d ≠ 0 ∧ C ≠ 0<VAR>habc : A ^ n + B ^ n = C ^ n<VAR>u : Rˣ<VAR>hu : normalize d * ↑u = d<GOAL>IsUnit ({A, B, C}.gcd id)
<VAR>α : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : NoZeroDivisors α<VAR>m n✝ n : ℕ<VAR>R : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n<VAR>a b c : R<VAR>s : Finset R := {a, b, c}<VAR>d : R := s.gcd id<VAR>A : R<VAR>hA : a = d * A<VAR>B : R<VAR>hB : b = d * B<VAR>C : R<VAR>hC : c = d * C<VAR>ha : d ≠ 0 ∧ A ≠ 0<VAR>hb : d ≠ 0 ∧ B ≠ 0<VAR>hc : d ≠ 0 ∧ C ≠ 0<VAR>habc : A ^ n + B ^ n = C ^ n<VAR>u : Rˣ<VAR>hu : normalize d * ↑u = d<GOAL>d = normalize d * {A, B, C}.gcd id
<VAR>ι : Type u_1<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → Setoid (α i)<VAR>f : (i : ι) → α i<GOAL>(Quotient.recOn Finset.univ.val (fun l => finChoiceAux l fun i x => ⟦f i⟧) ⋯).liftOn (fun f => ⟦fun i => f i ⋯⟧) ⋯ = ⟦f⟧
<VAR>ι : Type u_1<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ι<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → Setoid (α i)<VAR>f : (i : ι) → α i<GOAL>⟦fun i x => f i⟧.liftOn (fun f => ⟦fun i => f i ⋯⟧) ⋯ = ⟦f⟧
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>r k : ℕ<VAR>ih : ∀ {t : Finset α}, t ∈ ∂ ^[k] 𝒜 ↔ ∃ u, u.card = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜<VAR>t : Finset α<GOAL>t ∈ ∂ ^[k + 1] 𝒜 ↔ ∃ u, u.card = k + 1 ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>W : WeierstrassCurve R<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<GOAL>(W.baseChange B).ψ₂ = Polynomial.map (mapRingHom ↑f) (W.baseChange A).ψ₂
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>inst✝² : (i : ι) → Zero (α i)<VAR>inst✝¹ : (i : ι) → Preorder (α i)<VAR>inst✝ : ∀ (i : ι), WellFoundedLT (α i)<VAR>hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0<VAR>β : ι → Type u_2 := fun i => Antisymmetrization (α i) fun x x_1 => x ≤ x_1<VAR>e : (i : ι) → α i → β i := fun i => toAntisymmetrization fun x x_1 => x ≤ x_1<VAR>x✝ : (i : ι) → Zero (β i) := fun i => { zero := e i 0 }<VAR>this : WellFounded (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x_1 x_2 => x_1 < x_2)<GOAL>WellFounded fun x x_1 => x < x_1
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>inst✝² : (i : ι) → Zero (α i)<VAR>inst✝¹ : (i : ι) → Preorder (α i)<VAR>inst✝ : ∀ (i : ι), WellFoundedLT (α i)<VAR>hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0<VAR>β : ι → Type u_2 := fun i => Antisymmetrization (α i) fun x x_1 => x ≤ x_1<VAR>e : (i : ι) → α i → β i := fun i => toAntisymmetrization fun x x_1 => x ≤ x_1<VAR>x✝¹ : (i : ι) → Zero (β i) := fun i => { zero := e i 0 }<VAR>this : WellFounded (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x_1 x_2 => x_1 < x_2)<VAR>x✝ y✝ : Π₀ (i : ι), α i<VAR>h : x✝ < y✝<GOAL>InvImage (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x_1 x_2 => x_1 < x_2) (mapRange (fun i => e i) ⋯) x✝ y✝
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>inst✝² : (i : ι) → Zero (α i)<VAR>inst✝¹ : (i : ι) → Preorder (α i)<VAR>inst✝ : ∀ (i : ι), WellFoundedLT (α i)<VAR>hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0<VAR>β : ι → Type u_2 := fun i => Antisymmetrization (α i) fun x x_1 => x ≤ x_1<VAR>e : (i : ι) → α i → β i := fun i => toAntisymmetrization fun x x_1 => x ≤ x_1<VAR>x✝¹ : (i : ι) → Zero (β i) := fun i => { zero := e i 0 }<VAR>this✝ : WellFounded (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x_1 x_2 => x_1 < x_2)<VAR>x✝ y✝ : Π₀ (i : ι), α i<VAR>h : x✝ < y✝<VAR>this : IsStrictOrder ι (Function.swap WellOrderingRel)<GOAL>InvImage (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x_1 x_2 => x_1 < x_2) (mapRange (fun i => e i) ⋯) x✝ y✝
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>inst✝² : (i : ι) → Zero (α i)<VAR>inst✝¹ : (i : ι) → Preorder (α i)<VAR>inst✝ : ∀ (i : ι), WellFoundedLT (α i)<VAR>hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0<VAR>β : ι → Type u_2 := fun i => Antisymmetrization (α i) fun x x_1 => x ≤ x_1<VAR>e : (i : ι) → α i → β i := fun i => toAntisymmetrization fun x x_1 => x ≤ x_1<VAR>x✝¹ : (i : ι) → Zero (β i) := fun i => { zero := e i 0 }<VAR>this✝ : WellFounded (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x_1 x_2 => x_1 < x_2)<VAR>x✝ y✝ : Π₀ (i : ι), α i<VAR>h : x✝ < y✝<VAR>this : IsStrictOrder ι (Function.swap WellOrderingRel)<VAR>i : ι<VAR>he : ∀ (j : ι), Function.swap WellOrderingRel j i → x✝ j ≤ y✝ j ∧ y✝ j ≤ x✝ j<VAR>hl : x✝ i < y✝ i<GOAL>InvImage (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x_1 x_2 => x_1 < x_2) (mapRange (fun i => e i) ⋯) x✝ y✝
<VAR>α : Type u_1<VAR>inst✝³ : Ring α<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : TopologicalRing α<VAR>inst✝ : UniformAddGroup α<VAR>m : α →+ α →+ Completion α := AddMonoidHom.mul.compr₂ toCompl<GOAL>Continuous fun p => p.1 * p.2
<VAR>α : Type u_1<VAR>inst✝³ : Ring α<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : TopologicalRing α<VAR>inst✝ : UniformAddGroup α<VAR>m : α →+ α →+ Completion α := AddMonoidHom.mul.compr₂ toCompl<VAR>this : Continuous fun p => (m p.1) p.2<GOAL>Continuous fun p => p.1 * p.2
<VAR>α : Type u_1<VAR>inst✝³ : Ring α<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : TopologicalRing α<VAR>inst✝ : UniformAddGroup α<VAR>m : α →+ α →+ Completion α := AddMonoidHom.mul.compr₂ toCompl<VAR>this : Continuous fun p => (m p.1) p.2<VAR>di : DenseInducing ⇑toCompl<GOAL>Continuous fun p => p.1 * p.2
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝¹ : Preorder E<VAR>inst✝ : CovariantClass E E (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Submartingale f ℱ μ<VAR>hg : Submartingale g ℱ μ<GOAL>Submartingale (f + g) ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝¹ : Preorder E<VAR>inst✝ : CovariantClass E E (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Submartingale f ℱ μ<VAR>hg : Submartingale g ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>(f + g) i ≤ᶠ[ae μ] μ[(f + g) j|↑ℱ i]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝¹ : Preorder E<VAR>inst✝ : CovariantClass E E (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Submartingale f ℱ μ<VAR>hg : Submartingale g ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>(f + g) i ≤ᶠ[ae μ] μ[f j|↑ℱ i] + μ[g j|↑ℱ i]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝¹ : Preorder E<VAR>inst✝ : CovariantClass E E (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Submartingale f ℱ μ<VAR>hg : Submartingale g ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>∀ (a : Ω), f i a ≤ (μ[f j|↑ℱ i]) a → g i a ≤ (μ[g j|↑ℱ i]) a → (f + g) i a ≤ (μ[f j|↑ℱ i] + μ[g j|↑ℱ i]) a
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝¹ : Preorder E<VAR>inst✝ : CovariantClass E E (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Submartingale f ℱ μ<VAR>hg : Submartingale g ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<VAR>a✝² : Ω<VAR>a✝¹ : f i a✝² ≤ (μ[f j|↑ℱ i]) a✝²<VAR>a✝ : g i a✝² ≤ (μ[g j|↑ℱ i]) a✝²<GOAL>(f + g) i a✝² ≤ (μ[f j|↑ℱ i] + μ[g j|↑ℱ i]) a✝²
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<GOAL>IsClosed {∞}
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<GOAL>IsOpen (range some)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝² : (a : α) → DecidablePred (r a)<VAR>s✝ s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>s : Finset ι<VAR>t : Finset κ<VAR>f : ι → Finset α<VAR>g : κ → Finset β<GOAL>interedges r (s.biUnion f) (t.biUnion g) = (s ×ˢ t).biUnion fun ab => interedges r (f ab.1) (g ab.2)
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : BorelSpace E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>g : ℝ → F<VAR>a : ℝ<GOAL>∫ (x : ℝ), g (a⁻¹ * x) = |a| • ∫ (y : ℝ), g y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>f✝ : α → β<VAR>f : β → γ<VAR>g : α → β<VAR>hf : LocallyLipschitz f<VAR>hg : LocallyLipschitz g<VAR>x : α<VAR>Kg : ℝ≥0<VAR>t : Set α<VAR>ht : t ∈ 𝓝 x<VAR>hgL : LipschitzOnWith Kg g t<VAR>Kf : ℝ≥0<VAR>u : Set β<VAR>hu : u ∈ 𝓝 (g x)<VAR>hfL : LipschitzOnWith Kf f u<GOAL>∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (f ∘ g) t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>f✝ : α → β<VAR>f : β → γ<VAR>g : α → β<VAR>hf : LocallyLipschitz f<VAR>hg : LocallyLipschitz g<VAR>x : α<VAR>Kg : ℝ≥0<VAR>t : Set α<VAR>ht : t ∈ 𝓝 x<VAR>hgL : LipschitzOnWith Kg g t<VAR>Kf : ℝ≥0<VAR>u : Set β<VAR>hu : u ∈ 𝓝 (g x)<VAR>hfL : LipschitzOnWith Kf f u<GOAL>LipschitzOnWith (Kf * Kg) (f ∘ g) (t ∩ g ⁻¹' u)
<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<GOAL>Wbtw R x y z ∧ Wbtw R z x y ↔ x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>f : ι → Compacts α<GOAL>↑(s.sup f) = s.sup fun i => ↑(f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>f : ι → Compacts α<VAR>a : ι<VAR>s : Finset ι<VAR>x✝ : a ∉ s<VAR>h : ↑(s.sup f) = s.sup fun i => ↑(f i)<GOAL>↑((Finset.cons a s x✝).sup f) = (Finset.cons a s x✝).sup fun i => ↑(f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>f : ι → Compacts α<VAR>a : ι<VAR>s : Finset ι<VAR>x✝ : a ∉ s<VAR>h : ↑(s.sup f) = s.sup fun i => ↑(f i)<GOAL>↑(f a) ∪ ↑(s.sup f) = ↑(f a) ∪ s.sup fun i => ↑(f i)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>h : HasFDerivWithinAt f f' s x<VAR>v : E<VAR>c : ℕ → 𝕜<VAR>d : ℕ → E<VAR>dtop : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s<VAR>clim : Tendsto (fun n => ‖c n‖) atTop atTop<VAR>cdlim : Tendsto (fun n => c n • d n) atTop (𝓝 v)<GOAL>f' v ∈ tangentConeAt 𝕜 (f '' s) (f x)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>h : HasFDerivWithinAt f f' s x<VAR>v : E<VAR>c : ℕ → 𝕜<VAR>d : ℕ → E<VAR>dtop : ∀ᶠ (n : ℕ) in atTop, x + d n ∈ s<VAR>clim : Tendsto (fun n => ‖c n‖) atTop atTop<VAR>cdlim : Tendsto (fun n => c n • d n) atTop (𝓝 v)<GOAL>{x_1 | (fun n => x + d n ∈ s) x_1} ⊆ {x_1 | (fun n => f x + (fun n => f (x + d n) - f x) n ∈ f '' s) x_1}
<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>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hf : Integrable f μ<GOAL>‖setToFun μ T hT f‖ ≤ max C 0 * ‖Integrable.toL1 f hf‖
<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>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f g : α → E<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hf : Integrable f μ<GOAL>‖(L1.setToL1 hT) (Integrable.toL1 f hf)‖ ≤ max C 0 * ‖Integrable.toL1 f hf‖
<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>update v i (v j) i = update v i (v j) j
<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>w✝ : M<VAR>α : Type u_7<VAR>t : Finset α<VAR>B : α → BilinForm R M<VAR>v w : M<GOAL>((∑ i ∈ t, B i) v) w = ∑ i ∈ t, ((B i) v) w
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup M'<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M'<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : StrongRankCondition R<VAR>inst✝² : Module.Finite R M<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>p : ι → Submodule R M<VAR>hp : Independent p<VAR>inst✝ : Fintype { i // p i ≠ ⊥ }<GOAL>Fintype.card { i // p i ≠ ⊥ } ≤ finrank R M
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f✝ f₁ f₂ : Filter α<VAR>h h₁ h₂ : Set α → Set β<VAR>f : ι → Filter α<VAR>g : Set α → Set β<VAR>hg : ∀ {s t : Set α}, g (s ∩ t) = g s ∩ g t<VAR>hg' : g univ = univ<VAR>s t : Set α<GOAL>(𝓟 ∘ g) (s ∩ t) = (𝓟 ∘ g) s ⊓ (𝓟 ∘ g) t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f✝ f₁ f₂ : Filter α<VAR>h h₁ h₂ : Set α → Set β<VAR>f : ι → Filter α<VAR>g : Set α → Set β<VAR>hg : ∀ {s t : Set α}, g (s ∩ t) = g s ∩ g t<VAR>hg' : g univ = univ<GOAL>(𝓟 ∘ g) univ = ⊤