ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(MaxProducts C ho)<VAR>h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))<VAR>this✝ : Inhabited I<VAR>m : Products I →₀ ℤ<VAR>hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}<VAR>hmsum : (m.sum fun i a => a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)<VAR>this : (Products.eval C ↑l - m.sum fun i a => a • (List.map (e C) (term I ho :: ↑i)).prod) ∈ LinearMap.range (πs C o)<VAR>hse : LinearMap.range (πs C o) = LinearMap.ker (Linear_CC' C hsC ho)<GOAL>False
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(MaxProducts C ho)<VAR>h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))<VAR>this : Inhabited I<VAR>m : Products I →₀ ℤ<VAR>hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}<VAR>hmsum : (m.sum fun i a => a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)<VAR>hse : LinearMap.range (πs C o) = LinearMap.ker (Linear_CC' C hsC ho)<VAR>n : LocallyConstant ↑(π C fun x => ord I x < o) ℤ<VAR>hn : (πs C o) n = Products.eval C ↑l - m.sum fun i a => a • (List.map (e C) (term I ho :: ↑i)).prod<GOAL>False
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(MaxProducts C ho)<VAR>h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))<VAR>this : Inhabited I<VAR>m : Products I →₀ ℤ<VAR>hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}<VAR>hmsum : (m.sum fun i a => a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)<VAR>hse : LinearMap.range (πs C o) = LinearMap.ker (Linear_CC' C hsC ho)<VAR>n : LocallyConstant ↑(π C fun x => ord I x < o) ℤ<VAR>hn : ((πs C o) n + m.sum fun i a => a • (List.map (e C) (term I ho :: ↑i)).prod) = Products.eval C ↑l<GOAL>False
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(MaxProducts C ho)<VAR>h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))<VAR>this : Inhabited I<VAR>m : Products I →₀ ℤ<VAR>hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}<VAR>hmsum : (m.sum fun i a => a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)<VAR>hse : LinearMap.range (πs C o) = LinearMap.ker (Linear_CC' C hsC ho)<VAR>n : LocallyConstant ↑(π C fun x => ord I x < o) ℤ<VAR>hn : ((πs C o) n + m.sum fun i a => a • (List.map (e C) (term I ho :: ↑i)).prod) = Products.eval C ↑l<VAR>hn' : n ∈ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))<GOAL>False
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(MaxProducts C ho)<VAR>h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))<VAR>this : Inhabited I<VAR>m : Products I →₀ ℤ<VAR>hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}<VAR>hmsum : (m.sum fun i a => a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)<VAR>hse : LinearMap.range (πs C o) = LinearMap.ker (Linear_CC' C hsC ho)<VAR>n : LocallyConstant ↑(π C fun x => ord I x < o) ℤ<VAR>hn : ((πs C o) n + m.sum fun i a => a • (List.map (e C) (term I ho :: ↑i)).prod) = Products.eval C ↑l<VAR>hn' : ∃ c, (c.sum fun i a => a • eval (π C fun x => ord I x < o) i) = n<GOAL>False
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(MaxProducts C ho)<VAR>h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))<VAR>this : Inhabited I<VAR>m : Products I →₀ ℤ<VAR>hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}<VAR>hmsum : (m.sum fun i a => a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)<VAR>hse : LinearMap.range (πs C o) = LinearMap.ker (Linear_CC' C hsC ho)<VAR>n : LocallyConstant ↑(π C fun x => ord I x < o) ℤ<VAR>hn : ((πs C o) n + m.sum fun i a => a • (List.map (e C) (term I ho :: ↑i)).prod) = Products.eval C ↑l<VAR>w : { l // Products.isGood (π C fun x => ord I x < o) l } →₀ ℤ<VAR>hc : (w.sum fun i a => a • eval (π C fun x => ord I x < o) i) = n<GOAL>False
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(MaxProducts C ho)<VAR>h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))<VAR>this : Inhabited I<VAR>m : Products I →₀ ℤ<VAR>hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}<VAR>hmsum : (m.sum fun i a => a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)<VAR>hse : LinearMap.range (πs C o) = LinearMap.ker (Linear_CC' C hsC ho)<VAR>n : LocallyConstant ↑(π C fun x => ord I x < o) ℤ<VAR>w : { l // Products.isGood (π C fun x => ord I x < o) l } →₀ ℤ<VAR>hn : ((w.sum fun a b => (πs C o) (b • eval (π C fun x => ord I x < o) a)) + m.sum fun i a => a • (List.map (e C) (term I ho :: ↑i)).prod) = Products.eval C ↑l<VAR>hc : (w.sum fun i a => a • eval (π C fun x => ord I x < o) i) = n<GOAL>False
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(MaxProducts C ho)<VAR>h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))<VAR>this : Inhabited I<VAR>m : Products I →₀ ℤ<VAR>hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}<VAR>hmsum : (m.sum fun i a => a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)<VAR>hse : LinearMap.range (πs C o) = LinearMap.ker (Linear_CC' C hsC ho)<VAR>n : LocallyConstant ↑(π C fun x => ord I x < o) ℤ<VAR>w : { l // Products.isGood (π C fun x => ord I x < o) l } →₀ ℤ<VAR>hn : ((w.sum fun a b => (πs C o) (b • eval (π C fun x => ord I x < o) a)) + m.sum fun i a => a • (List.map (e C) (term I ho :: ↑i)).prod) = Products.eval C ↑l<VAR>hc : (w.sum fun i a => a • eval (π C fun x => ord I x < o) i) = n<GOAL>Products.eval C ↑l ∈ Submodule.span ℤ (Products.eval C '' {m | m < ↑l})
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(MaxProducts C ho)<VAR>h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))<VAR>this : Inhabited I<VAR>m : Products I →₀ ℤ<VAR>hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}<VAR>hmsum : (m.sum fun i a => a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)<VAR>hse : LinearMap.range (πs C o) = LinearMap.ker (Linear_CC' C hsC ho)<VAR>n : LocallyConstant ↑(π C fun x => ord I x < o) ℤ<VAR>w : { l // Products.isGood (π C fun x => ord I x < o) l } →₀ ℤ<VAR>hn : ((w.sum fun a b => (πs C o) (b • eval (π C fun x => ord I x < o) a)) + m.sum fun i a => a • (List.map (e C) (term I ho :: ↑i)).prod) = Products.eval C ↑l<VAR>hc : (w.sum fun i a => a • eval (π C fun x => ord I x < o) i) = n<GOAL>((w.sum fun a b => (πs C o) (b • eval (π C fun x => ord I x < o) a)) + m.sum fun i a => a • (List.map (e C) (term I ho :: ↑i)).prod) ∈ Submodule.span ℤ (Products.eval C '' {m | m < ↑l})
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(MaxProducts C ho)<VAR>h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))<VAR>this : Inhabited I<VAR>m : Products I →₀ ℤ<VAR>hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}<VAR>hmsum : (m.sum fun i a => a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)<VAR>hse : LinearMap.range (πs C o) = LinearMap.ker (Linear_CC' C hsC ho)<VAR>n : LocallyConstant ↑(π C fun x => ord I x < o) ℤ<VAR>w : { l // Products.isGood (π C fun x => ord I x < o) l } →₀ ℤ<VAR>hn : ((w.sum fun a b => (πs C o) (b • eval (π C fun x => ord I x < o) a)) + m.sum fun i a => a • (List.map (e C) (term I ho :: ↑i)).prod) = Products.eval C ↑l<VAR>hc : (w.sum fun i a => a • eval (π C fun x => ord I x < o) i) = n<GOAL>(w.sum fun a b => (πs C o) (b • eval (π C fun x => ord I x < o) a)) ∈ Submodule.span ℤ (Products.eval C '' {m | m < ↑l})
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>o : Ordinal.{u}<VAR>hC : IsClosed C<VAR>hsC : contained C (Order.succ o)<VAR>ho : o < Ordinal.type fun x x_1 => x < x_1<VAR>l : ↑(MaxProducts C ho)<VAR>h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))<VAR>this : Inhabited I<VAR>m : Products I →₀ ℤ<VAR>hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}<VAR>hmsum : (m.sum fun i a => a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)<VAR>hse : LinearMap.range (πs C o) = LinearMap.ker (Linear_CC' C hsC ho)<VAR>n : LocallyConstant ↑(π C fun x => ord I x < o) ℤ<VAR>w : { l // Products.isGood (π C fun x => ord I x < o) l } →₀ ℤ<VAR>hn : ((w.sum fun a b => (πs C o) (b • eval (π C fun x => ord I x < o) a)) + m.sum fun i a => a • (List.map (e C) (term I ho :: ↑i)).prod) = Products.eval C ↑l<VAR>hc : (w.sum fun i a => a • eval (π C fun x => ord I x < o) i) = n<GOAL>(m.sum fun i a => a • (List.map (e C) (term I ho :: ↑i)).prod) ∈ Submodule.span ℤ (Products.eval C '' {m | m < ↑l})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>κ' : Kernel α (γ × β)<VAR>hκκ' : κ ≤ κ'<VAR>hκ'ν : κ'.fst ≤ ν<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>s : Set β<VAR>h0 : ¬(ν a) (countablePartitionSet n x) = 0<GOAL>((κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)).toReal ≤ ((κ' a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>κ' : Kernel α (γ × β)<VAR>hκκ' : κ ≤ κ'<VAR>hκ'ν : κ'.fst ≤ ν<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>s : Set β<VAR>h0 : ¬(ν a) (countablePartitionSet n x) = 0<VAR>h_le : (κ' a) (countablePartitionSet n x ×ˢ s) ≤ (ν a) (countablePartitionSet n x)<GOAL>((κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)).toReal ≤ ((κ' a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>κ' : Kernel α (γ × β)<VAR>hκκ' : κ ≤ κ'<VAR>hκ'ν : κ'.fst ≤ ν<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>s : Set β<VAR>h0 : ¬(ν a) (countablePartitionSet n x) = 0<VAR>h_le : (κ' a) (countablePartitionSet n x ×ˢ s) ≤ (ν a) (countablePartitionSet n x)<GOAL>(κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) ≤ (κ' a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>κ' : Kernel α (γ × β)<VAR>hκκ' : κ ≤ κ'<VAR>hκ'ν : κ'.fst ≤ ν<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>s : Set β<VAR>h0 : ¬(ν a) (countablePartitionSet n x) = 0<VAR>h_le : (κ' a) (countablePartitionSet n x ×ˢ s) ≤ (ν a) (countablePartitionSet n x)<GOAL>(κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>κ' : Kernel α (γ × β)<VAR>hκκ' : κ ≤ κ'<VAR>hκ'ν : κ'.fst ≤ ν<VAR>n : ℕ<VAR>a : α<VAR>x : γ<VAR>s : Set β<VAR>h0 : ¬(ν a) (countablePartitionSet n x) = 0<VAR>h_le : (κ' a) (countablePartitionSet n x ×ˢ s) ≤ (ν a) (countablePartitionSet n x)<GOAL>(κ' a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) ≠ ⊤
<VAR>x : ℂ<GOAL>sin x = 1 ↔ ∃ k, ↑π / 2 + ↑k * (2 * ↑π) = x
<VAR>x : ℂ<GOAL>(∃ k, ↑k * (2 * ↑π) = x - ↑π / 2) ↔ ∃ k, ↑π / 2 + ↑k * (2 * ↑π) = x
<VAR>a : ℂ<VAR>r : ℝ<VAR>ha : 0 < a.re<VAR>hr : 0 < r<GOAL>∫ (t : ℝ) in Ioi 0, ↑t ^ (a - 1) * cexp (-(↑r * ↑t)) = (1 / ↑r) ^ a * Gamma a
<VAR>a : ℂ<VAR>r : ℝ<VAR>ha : 0 < a.re<VAR>hr : 0 < r<VAR>aux : (1 / ↑r) ^ a = 1 / ↑r * (1 / ↑r) ^ (a - 1)<GOAL>∫ (t : ℝ) in Ioi 0, ↑t ^ (a - 1) * cexp (-(↑r * ↑t)) = (1 / ↑r) ^ a * Gamma a
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x : α✝ 0<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.succ<VAR>i : Fin n<VAR>y : α✝ i.succ<VAR>z : α✝ 0<VAR>α : Type u_1<VAR>a : Fin n → α<VAR>h : 1 * n = n<GOAL>repeat 1 a = a ∘ cast h
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x : α✝ 0<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.succ<VAR>i : Fin n<VAR>y : α✝ i.succ<VAR>z : α✝ 0<VAR>α : Type u_1<VAR>a : Fin n → α<VAR>h : 1 * n = n<GOAL>∀ (x : Fin (1 * n)), repeat 1 a x = (a ∘ cast h) x
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x : α✝ 0<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.succ<VAR>i : Fin n<VAR>y : α✝ i.succ<VAR>z : α✝ 0<VAR>α : Type u_1<VAR>a : Fin n → α<VAR>h : 1 * n = n<GOAL>∀ (x : Fin n), repeat 1 a (cast ⋯ x) = (a ∘ cast h) (cast ⋯ x)
<VAR>m n : ℕ<VAR>α✝ : Fin (n + 1) → Type u<VAR>x : α✝ 0<VAR>q : (i : Fin (n + 1)) → α✝ i<VAR>p : (i : Fin n) → α✝ i.succ<VAR>i✝ : Fin n<VAR>y : α✝ i✝.succ<VAR>z : α✝ 0<VAR>α : Type u_1<VAR>a : Fin n → α<VAR>h : 1 * n = n<VAR>i : Fin n<GOAL>repeat 1 a (cast ⋯ i) = (a ∘ cast h) (cast ⋯ i)
<VAR>n : ℕ<VAR>hn : 0 < n<VAR>s : ℂ<GOAL>‖↑n ^ s‖ = ↑n ^ s.re
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>r s : R<VAR>x y : M<GOAL>2 • x = x + 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✝¹ : NormedSpace ℝ E<VAR>f✝ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f f' : ℝ → E<VAR>hcont : ContinuousOn g [[a, b]]<VAR>hderiv : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt g (g' x) x<VAR>hpos : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ g' x<GOAL>IntervalIntegrable g' volume a b
<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✝¹ : NormedSpace ℝ E<VAR>f✝ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f f' : ℝ → E<VAR>hcont : ContinuousOn g [[a, b]]<VAR>hderiv : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt g (g' x) x<VAR>hpos : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ g' x<VAR>hab : a ≤ b<GOAL>IntervalIntegrable g' volume a b
<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✝¹ : NormedSpace ℝ E<VAR>f✝ : ℝ → E<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f f' : ℝ → E<VAR>hcont : ContinuousOn g [[a, b]]<VAR>hderiv : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt g (g' x) x<VAR>hpos : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ g' x<VAR>hab : b ≤ a<GOAL>IntervalIntegrable g' volume a b
<VAR>α : Type u_1<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>ι : Sort u_2<VAR>f : ι → ℝ≥0<VAR>s : Set ℝ≥0<GOAL>↑r ∈ upperBounds (ofNNReal '' s) ↔ r ∈ upperBounds s
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>n : ℕ<VAR>hn : ∀ (hf : (setOf p).Finite), n < hf.toFinset.card<GOAL>count p (nth p n + 1) = n + 1
<VAR>x y : ℝ<VAR>hy : 0 < y<GOAL>x < log y ↔ rexp x < y
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝ : CommSemiring R<GOAL>zeroLocus ∘ SetLike.coe '' minimalPrimes R = irreducibleComponents (PrimeSpectrum R)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝ : CommSemiring R<GOAL>Set.EqOn ((zeroLocus ∘ SetLike.coe) ∘ vanishingIdeal) id (irreducibleComponents (PrimeSpectrum R))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝ : CommSemiring R<VAR>s : Set (PrimeSpectrum R)<VAR>hs : s ∈ irreducibleComponents (PrimeSpectrum R)<GOAL>((zeroLocus ∘ SetLike.coe) ∘ vanishingIdeal) s = id s
<VAR>R : Type u_1<VAR>n : ℕ<GOAL>∑ m ∈ range (n + 1), (-1) ^ m * ↑(n.choose m) = if n = 0 then 1 else 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s✝ t✝ : WSeq α<VAR>h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n<VAR>s t : WSeq α<VAR>h : (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) s t<GOAL>Computation.LiftRel (LiftRelO (fun x x_1 => x = x_1) fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) s.destruct t.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s✝ t✝ : WSeq α<VAR>h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n<VAR>s t : WSeq α<VAR>h : (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) s t<GOAL>s.destruct.Terminates ↔ t.destruct.Terminates
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s✝ t✝ : WSeq α<VAR>h✝ : ∀ (n : ℕ), s✝.get? n ~ t✝.get? n<VAR>s t : WSeq α<VAR>h : (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) s t<GOAL>∀ {a b : Option (α × WSeq α)}, a ∈ s.destruct → b ∈ t.destruct → LiftRelO (fun x x_1 => x = x_1) (fun s t => ∀ (n : ℕ), s.get? n ~ t.get? n) a b
<VAR>p : ℕ<VAR>R S : Type u<VAR>σ : Type u_1<VAR>idx : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R<VAR>g : R →+* S<VAR>x : 𝕎 R<VAR>φ : ℕ → MvPolynomial ℕ ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => (aeval x.coeff) (φ n)<VAR>n : ℕ<GOAL>((WittVector.map g) (f x)).coeff n = (f ((WittVector.map g) x)).coeff n
<VAR>p : ℕ<VAR>R S : Type u<VAR>σ : Type u_1<VAR>idx : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R<VAR>g : R →+* S<VAR>x : 𝕎 R<VAR>φ : ℕ → MvPolynomial ℕ ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => (aeval x.coeff) (φ n)<VAR>n : ℕ<GOAL>(eval₂Hom (g.comp (algebraMap ℤ R)) fun i => g (x.coeff i)) (φ n) = (aeval ((WittVector.map g) x).coeff) (φ n)
<VAR>p : ℕ<VAR>R S : Type u<VAR>σ : Type u_1<VAR>idx : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R<VAR>g : R →+* S<VAR>x : 𝕎 R<VAR>φ : ℕ → MvPolynomial ℕ ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => (aeval x.coeff) (φ n)<VAR>n : ℕ<GOAL>(fun i => g (x.coeff i)) = ((WittVector.map g) x).coeff
<VAR>p : ℕ<VAR>R S : Type u<VAR>σ : Type u_1<VAR>idx : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R<VAR>g : R →+* S<VAR>x : 𝕎 R<VAR>φ : ℕ → MvPolynomial ℕ ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => (aeval x.coeff) (φ n)<VAR>n x✝ : ℕ<GOAL>g (x.coeff x✝) = ((WittVector.map g) x).coeff x✝
<VAR>N : ℕ<VAR>x✝ : SL(2, ℤ)<GOAL>x✝ ∈ Gamma 1 ↔ x✝ ∈ ⊤
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y✝ : α<VAR>Φ : α → β<VAR>y : α<VAR>hy : y ∈ s<GOAL>infEdist x s ≠ ⊤
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>l : List α<VAR>a : α<GOAL>(l.all fun a => decide (p a)) = true ↔ ∀ (a : α), a ∈ l → p a
<VAR>m n k : ℕ<VAR>h₁ : m ≤ k<VAR>h₂ : k < m + n<GOAL>finAddFlip ⟨k, h₂⟩ = ⟨k - m, ⋯⟩
<VAR>m n k : ℕ<VAR>h₁ : m ≤ k<VAR>h₂ : k < m + n<GOAL>k = ↑(Fin.natAdd m ⟨k - m, ⋯⟩)
<VAR>ι : Sort uι<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>q : Submodule R N<VAR>m : M<VAR>hm : m ∈ ⊥<VAR>n : N<VAR>hn : n ∈ q<GOAL>(f m) n ∈ ⊥
<VAR>ι : Sort uι<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>q : Submodule R N<VAR>m : M<VAR>hm : m = 0<VAR>n : N<VAR>hn : n ∈ q<GOAL>(f m) n = 0
<VAR>α : Type u<VAR>g : Ordinal.{u} → α<VAR>h_inj : InjOn g (Iio (succ #α).ord)<GOAL>False
<VAR>α : Type u<VAR>g : Ordinal.{u} → α<VAR>h_inj : InjOn g (Iio (succ #α).ord)<VAR>h : lift.{u, u + 1} #↑(Iio (succ #α).ord) ≤ lift.{u + 1, u} #α<GOAL>False
<VAR>α : Type u<VAR>g : Ordinal.{u} → α<VAR>h_inj : InjOn g (Iio (succ #α).ord)<VAR>h : lift.{u, u + 1} #↑(Iio (succ #α).ord) ≤ lift.{u + 1, u} #α<VAR>mk_initialSeg_subtype : #↑(Iio (succ #α).ord) = lift.{u + 1, u} (succ #α)<GOAL>False
<VAR>α : Type u<VAR>g : Ordinal.{u} → α<VAR>h_inj : InjOn g (Iio (succ #α).ord)<VAR>h : succ #α ≤ #α<VAR>mk_initialSeg_subtype : #↑(Iio (succ #α).ord) = lift.{u + 1, u} (succ #α)<GOAL>False
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<GOAL>closure s ∩ coborder s = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>inst✝ : UniformSpace γ<VAR>f : γ → β<VAR>hf : UniformContinuous f<GOAL>UniformContinuous (⇑(ofFun 𝔖) ∘ (fun x => f ∘ x) ∘ ⇑(toFun 𝔖))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝¹ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>inst✝ : UniformSpace γ<VAR>f : γ → β<VAR>hf : UniformContinuous f<GOAL>uniformSpace α γ 𝔖 ≤ UniformSpace.comap (⇑(ofFun 𝔖) ∘ (fun x => f ∘ x) ∘ ⇑(toFun 𝔖)) (uniformSpace α β 𝔖)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>x : R<VAR>hx : IsUnit x<VAR>hfx : f x ≠ 0<VAR>n : ℕ<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<GOAL>f (x ^ n) ≠ 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>x : R<VAR>hx : IsUnit x<VAR>hfx : f x ≠ 0<VAR>n : ℕ<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>h1 : f 1 ≠ 0<GOAL>f (x ^ n) ≠ 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>x : R<VAR>hx : IsUnit x<VAR>hfx : f x ≠ 0<VAR>n : ℕ<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>h1 : f 1 ≠ 0<VAR>hxn : f (x ^ n) = 0<GOAL>False
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>x : R<VAR>hx : IsUnit x<VAR>hfx : f x ≠ 0<VAR>n : ℕ<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>h1 : f 1 ≠ 0<VAR>hxn : f (x ^ n) = 0<VAR>this : f 1 ≤ 0<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ e.source<GOAL>x ∈ ↑e ⁻¹' (↑e.symm ⁻¹' s) ↔ x ∈ s
<VAR>α : Type u_1<VAR>inst✝¹ : Div α<VAR>inst✝ : Small.{u_2, u_1} α<VAR>x y : Shrink.{u_2, u_1} α<GOAL>(equivShrink α).symm (x / y) = (equivShrink α).symm x / (equivShrink α).symm y