ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>x : ℝ<GOAL>Real.toEReal ⁻¹' Set.Ici ↑x = Set.Ici x
<VAR>x : ℝ<GOAL>Real.toEReal ⁻¹' Set.Ioi ↑x = Set.Ioi x
<GOAL>Real.toEReal ⁻¹' Set.Ioi ⊥ = Set.univ
<VAR>y : ℝ<GOAL>Real.toEReal ⁻¹' Set.Iic ↑y = Set.Iic y
<VAR>y : ℝ<GOAL>Real.toEReal ⁻¹' Set.Iio ↑y = Set.Iio y
<GOAL>Real.toEReal ⁻¹' Set.Iio ⊤ = Set.univ
<VAR>x y : ℝ<GOAL>Real.toEReal ⁻¹' Set.Icc ↑x ↑y = Set.Icc x y
<VAR>x y : ℝ<GOAL>Real.toEReal ⁻¹' Set.Ico ↑x ↑y = Set.Ico x y
<VAR>x y : ℝ<GOAL>Real.toEReal ⁻¹' Set.Ioc ↑x ↑y = Set.Ioc x y
<VAR>x y : ℝ<GOAL>Real.toEReal ⁻¹' Set.Ioo ↑x ↑y = Set.Ioo x y
<VAR>x : ℝ<GOAL>Real.toEReal ⁻¹' Set.Ico ↑x ⊤ = Set.Ici x
<VAR>x : ℝ<GOAL>Real.toEReal ⁻¹' Set.Ioo ↑x ⊤ = Set.Ioi x
<VAR>y : ℝ<GOAL>Real.toEReal ⁻¹' Set.Ioc ⊥ ↑y = Set.Iic y
<VAR>y : ℝ<GOAL>Real.toEReal ⁻¹' Set.Ioo ⊥ ↑y = Set.Iio y
<GOAL>Real.toEReal ⁻¹' Set.Ioo ⊥ ⊤ = Set.univ
<VAR>x : ℝ≥0∞<GOAL>(↑x).toReal = x.toReal
<VAR>x : ℝ<GOAL>↑(ENNReal.ofReal x) = ↑(max x 0)
<VAR>x : ℝ≥0<GOAL>↑↑x = ↑↑x
<VAR>x : ℝ≥0∞<GOAL>↑x = ⊤ ↔ x = ⊤
<VAR>x : ℝ≥0<GOAL>↑↑x ≠ ⊤
<VAR>x : ℝ≥0<GOAL>↑↑x < ⊤
<VAR>x y : ℝ≥0∞<GOAL>↑x ≤ ↑y ↔ x ≤ y
<VAR>x y : ℝ≥0∞<GOAL>↑x < ↑y ↔ x < y
<VAR>x y : ℝ≥0∞<GOAL>↑x = ↑y ↔ x = y
<VAR>x y : ℝ≥0∞<GOAL>↑x ≠ ↑y ↔ x ≠ y
<VAR>x : ℝ≥0∞<GOAL>↑x ≠ 0 ↔ x ≠ 0
<VAR>x : ℝ≥0∞<GOAL>↑x ≠ 1 ↔ x ≠ 1
<VAR>x : ℝ≥0∞<GOAL>0 ≤ ↑x
<GOAL>Set.range ENNReal.toEReal = Set.Ici 0
<VAR>x : ℝ≥0∞<GOAL>⊥ < ↑x
<VAR>x : ℝ≥0∞<GOAL>↑x ≠ ⊥
<VAR>x y : ℝ≥0∞<GOAL>↑(x + y) = ↑x + ↑y
<VAR>x y : ℝ≥0∞<GOAL>↑(x * y) = ↑x * ↑y
<VAR>n : ℕ<VAR>x : ℝ≥0∞<GOAL>↑(n • x) = n • ↑x
<VAR>n : ℕ<GOAL>↑n ≠ ⊥
<VAR>m n : ℕ<GOAL>↑m ≠ ↑n ↔ m ≠ n
<VAR>a b : EReal<GOAL>a < b → ∃ x, a < ↑↑x ∧ ↑↑x < b
<VAR>a b : EReal<GOAL>a < b ↔ ∃ x, a < ↑↑x ∧ ↑↑x < b
<VAR>a b : EReal<GOAL>a < b ↔ ∃ x, a < ↑x ∧ ↑x < b
<VAR>x : EReal<GOAL>x + ⊥ = ⊥
<VAR>x : EReal<GOAL>⊥ + x = ⊥
<VAR>x y : EReal<GOAL>x + y = ⊥ ↔ x = ⊥ ∨ y = ⊥
<VAR>x : ℝ<GOAL>⊤ + ↑x = ⊤
<VAR>x : EReal<VAR>h : x ≠ ⊥<GOAL>⊤ + x = ⊤
<VAR>x : EReal<GOAL>⊤ + x = ⊤ ↔ x ≠ ⊥
<VAR>a b : EReal<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>0 < a + b
<VAR>x : ℝ<GOAL>↑x + ⊤ = ⊤
<VAR>x y : EReal<VAR>hx : x ≠ ⊤<VAR>h'x : x ≠ ⊥<VAR>hy : y ≠ ⊤<VAR>h'y : y ≠ ⊥<GOAL>(x + y).toReal = x.toReal + y.toReal
<VAR>x : ℝ<GOAL>AddLECancellable ↑x
<VAR>x y : EReal<VAR>h : x < y<VAR>z : ℝ<GOAL>x + ↑z < y + ↑z
<VAR>x y z t : EReal<VAR>h : x < y<VAR>h' : z ≤ t<VAR>hbot : t ≠ ⊥<VAR>htop : t = ⊤ → z = ⊤ → x = ⊥<GOAL>x + z < y + t
<VAR>x y z t : EReal<VAR>h : x < y<VAR>h' : z ≤ t<VAR>hz : z ≠ ⊥<VAR>ht : t ≠ ⊤<GOAL>x + z < y + t
<VAR>n : ℤ<VAR>x : ℝ<GOAL>↑(n • x) = n • ↑x
<VAR>a : EReal<GOAL>(-a).toReal = -a.toReal
<VAR>x : EReal<GOAL>-x = ⊤ ↔ x = ⊥
<VAR>x : EReal<GOAL>-x = ⊥ ↔ x = ⊤
<VAR>x : EReal<GOAL>-x = 0 ↔ x = 0
<VAR>a b : EReal<GOAL>-a ≤ -b ↔ b ≤ a
<VAR>a b : EReal<GOAL>-a < -b ↔ b < a
<VAR>a b : EReal<VAR>h : -a ≤ b<GOAL>-b ≤ a
<VAR>a b : EReal<GOAL>-a < b ↔ -b < a
<VAR>a b : EReal<VAR>h : -a < b<GOAL>-b < a
<VAR>x : EReal<GOAL>⊥ - x = ⊥
<VAR>x : EReal<GOAL>x - ⊤ = ⊥
<VAR>x : ℝ<GOAL>⊤ - ↑x = ⊤
<VAR>x : ℝ<GOAL>↑x - ⊥ = ⊤
<VAR>x y z t : EReal<VAR>h : x ≤ y<VAR>h' : t ≤ z<GOAL>x - z ≤ y - t
<VAR>x y z t : EReal<VAR>h : x < y<VAR>h' : z ≤ t<VAR>hz : z ≠ ⊥<VAR>ht : t ≠ ⊤<GOAL>x - t < y - z
<VAR>x y : EReal<VAR>hx : x ≠ ⊤<VAR>h'x : x ≠ ⊥<VAR>hy : y ≠ ⊤<VAR>h'y : y ≠ ⊥<GOAL>(x - y).toReal = x.toReal - y.toReal
<VAR>a : EReal<VAR>b : ℝ<GOAL>a + ↑b - ↑b = a
<VAR>x : ℝ<VAR>h : 0 < x<GOAL>↑x * ⊤ = ⊤
<VAR>x : ℝ<VAR>h : x < 0<GOAL>↑x * ⊤ = ⊥
<VAR>x : ℝ<VAR>h : 0 < x<GOAL>⊤ * ↑x = ⊤
<VAR>x : ℝ<VAR>h : x < 0<GOAL>⊤ * ↑x = ⊥
<VAR>x : EReal<GOAL>0 < x → x * ⊤ = ⊤
<VAR>x : EReal<GOAL>x < 0 → x * ⊤ = ⊥
<VAR>a b : EReal<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>0 < a * b
<VAR>x : EReal<VAR>h : x < 0<GOAL>⊤ * x = ⊥
<VAR>x : ℝ<VAR>h : 0 < x<GOAL>↑x * ⊥ = ⊥
<VAR>x : ℝ<VAR>h : x < 0<GOAL>↑x * ⊥ = ⊤
<VAR>x : ℝ<VAR>h : 0 < x<GOAL>⊥ * ↑x = ⊥
<VAR>x : ℝ<VAR>h : x < 0<GOAL>⊥ * ↑x = ⊤
<VAR>x : EReal<GOAL>0 < x → x * ⊥ = ⊥
<VAR>x : EReal<GOAL>x < 0 → x * ⊥ = ⊤
<VAR>P : EReal → EReal → Prop<VAR>neg_left : ∀ {x y : EReal}, P x y → P (-x) y<VAR>top_top : P ⊤ ⊤<VAR>top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x<VAR>top_zero : P ⊤ 0<VAR>top_neg : ∀ x < 0, P ⊤ ↑x<VAR>top_bot : P ⊤ ⊥<VAR>zero_top : P 0 ⊤<VAR>zero_bot : P 0 ⊥<VAR>pos_top : ∀ (x : ℝ), 0 < x → P ↑x ⊤<VAR>pos_bot : ∀ (x : ℝ), 0 < x → P ↑x ⊥<VAR>coe_coe : ∀ (x y : ℝ), P ↑x ↑y<VAR>x y : EReal<GOAL>P x y
<VAR>P : EReal → EReal → Prop<VAR>symm : ∀ {x y : EReal}, P x y → P y x<VAR>neg_left : ∀ {x y : EReal}, P x y → P (-x) y<VAR>top_top : P ⊤ ⊤<VAR>top_pos : ∀ (x : ℝ), 0 < x → P ⊤ ↑x<VAR>top_zero : P ⊤ 0<VAR>coe_coe : ∀ (x y : ℝ), P ↑x ↑y<VAR>x y : EReal<GOAL>P x y
<VAR>x y : EReal<GOAL>(∀ (z : ℝ), x < ↑z → y ≤ ↑z) ↔ y ≤ x
<VAR>x : ℝ<GOAL>(↑x).abs = ENNReal.ofReal |x|
<VAR>x : ℝ<GOAL>(↑x).abs < ⊤
<VAR>x : EReal<GOAL>x.abs = 0 ↔ x = 0
<VAR>x : ℝ<GOAL>SignType.sign ↑x = SignType.sign x
<VAR>x : SignType<GOAL>↑↑x = ↑x
<VAR>x : EReal<GOAL>SignType.sign (-x) = -SignType.sign x
<VAR>x y : EReal<GOAL>SignType.sign (x * y) = SignType.sign x * SignType.sign y
<VAR>x : EReal<GOAL>↑(SignType.sign x) * ↑x.abs = x
<VAR>x : EReal<GOAL>↑x.abs * ↑(SignType.sign x) = x
<VAR>x y : EReal<GOAL>x.abs = y.abs ∧ SignType.sign x = SignType.sign y ↔ x = y
<VAR>x y : EReal<GOAL>x ≤ y ↔ SignType.sign x < SignType.sign y ∨ SignType.sign x = SignType.neg ∧ SignType.sign y = SignType.neg ∧ y.abs ≤ x.abs ∨ SignType.sign x = SignType.zero ∧ SignType.sign y = SignType.zero ∨ SignType.sign x = SignType.pos ∧ SignType.sign y = SignType.pos ∧ x.abs ≤ y.abs
<VAR>x : ℝ<VAR>n : ℕ<GOAL>↑(x ^ n) = ↑x ^ n
<VAR>x : ℝ≥0∞<VAR>n : ℕ<GOAL>↑(x ^ n) = ↑x ^ n
<VAR>a : EReal<GOAL>(-a)⁻¹ = -a⁻¹
<VAR>a : EReal<VAR>h : a ≠ ⊥<VAR>h' : a ≠ ⊤<GOAL>a⁻¹⁻¹ = a
<VAR>a : EReal<GOAL>↑(SignType.sign a) * (↑a.abs)⁻¹ = a⁻¹
<VAR>a : EReal<GOAL>↑(SignType.sign a) * ↑a.abs⁻¹ = a⁻¹
<VAR>a b : EReal<GOAL>a / b = b⁻¹ * a
<VAR>a b : ℝ<GOAL>↑(a / b) = ↑a / ↑b
<VAR>a : EReal<GOAL>a / ⊥ = 0
<VAR>a : EReal<GOAL>a / ⊤ = 0
<VAR>a : EReal<VAR>h : 0 < a<VAR>h' : a ≠ ⊤<GOAL>⊤ / a = ⊤
<VAR>a : EReal<VAR>h : a < 0<VAR>h' : a ≠ ⊥<GOAL>⊤ / a = ⊥
<VAR>a : EReal<VAR>h : 0 < a<VAR>h' : a ≠ ⊤<GOAL>⊥ / a = ⊥
<VAR>a : EReal<VAR>h : a < 0<VAR>h' : a ≠ ⊥<GOAL>⊥ / a = ⊤
<VAR>a b c : EReal<GOAL>a * (b / c) = a * b / c
<VAR>a b c : EReal<GOAL>a / b / c = a / (b * c)
<VAR>a b : EReal<VAR>h₁ : b ≠ ⊥<VAR>h₂ : b ≠ ⊤<VAR>h₃ : b ≠ 0<GOAL>a / b * b = a
<VAR>a b c : EReal<VAR>h₁ : c ≠ ⊥<VAR>h₂ : c ≠ ⊤<VAR>h₃ : c ≠ 0<GOAL>a * c / (b * c) = a / b
<VAR>a b c : EReal<VAR>h : 0 ≤ a<VAR>h' : 0 ≤ b<GOAL>(a + b) / c = a / c + b / c
<VAR>b : EReal<VAR>h : 0 ≤ b<GOAL>Monotone fun a => a / b
<VAR>a a' b : EReal<VAR>h : 0 ≤ b<VAR>h' : a ≤ a'<GOAL>a / b ≤ a' / b
<VAR>b : EReal<VAR>h : 0 < b<VAR>h' : b ≠ ⊤<GOAL>StrictMono fun a => a / b
<VAR>a a' b : EReal<VAR>h₁ : 0 < b<VAR>h₂ : b ≠ ⊤<VAR>h₃ : a < a'<GOAL>a / b < a' / b
<VAR>b : EReal<VAR>h : b ≤ 0<GOAL>Antitone fun a => a / b
<VAR>a a' b : EReal<VAR>h : b ≤ 0<VAR>h' : a ≤ a'<GOAL>a' / b ≤ a / b
<VAR>b : EReal<VAR>h : b < 0<VAR>h' : b ≠ ⊥<GOAL>StrictAnti fun a => a / b
<VAR>a a' b : EReal<VAR>h₁ : b < 0<VAR>h₂ : b ≠ ⊥<VAR>h₃ : a < a'<GOAL>a' / b < a / b
<VAR>a b c : EReal<VAR>h : 0 < b<VAR>h' : b ≠ ⊤<GOAL>a / b ≤ c ↔ a ≤ b * c
<VAR>a b : EReal<VAR>h : 0 ≤ a<VAR>h' : 0 ≤ b<GOAL>0 ≤ a / b
<VAR>a b : EReal<VAR>h : a ≤ 0<VAR>h' : 0 ≤ b<GOAL>a / b ≤ 0
<VAR>a b : EReal<VAR>h : 0 ≤ a<VAR>h' : b ≤ 0<GOAL>a / b ≤ 0
<VAR>a b : EReal<VAR>h : a ≤ 0<VAR>h' : b ≤ 0<GOAL>0 ≤ a / b
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>(i : ι) → (s : Set ι) → Decidable (i ∈ s)<GOAL>Relation.Fibration (InvImage (Prod.GameAdd (DFinsupp.Lex r s) (DFinsupp.Lex r s)) Prod.snd) (DFinsupp.Lex r s) fun x => x.2.1.piecewise x.2.2 x.1
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>DecidableEq ι<VAR>x : Π₀ (i : ι), α i<VAR>i : ι<VAR>hs : Acc (DFinsupp.Lex r s) (DFinsupp.single i (x i))<VAR>hu : Acc (DFinsupp.Lex r s) (DFinsupp.erase i x)<GOAL>Acc (DFinsupp.Lex r s) x
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0<GOAL>Acc (DFinsupp.Lex r s) 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0<VAR>DecidableEq ι<VAR>(i : ι) → (x : α i) → Decidable (x ≠ 0)<VAR>x : Π₀ (i : ι), α i<GOAL>(∀ i ∈ x.support, Acc (DFinsupp.Lex r s) (DFinsupp.single i (x i))) → Acc (DFinsupp.Lex r s) x
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0<VAR>hs : ∀ (i : ι), WellFounded (s i)<VAR>DecidableEq ι<VAR>i : ι<VAR>hi : Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) i<VAR>a : α i<GOAL>Acc (DFinsupp.Lex r s) (DFinsupp.single i a)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0<VAR>hs : ∀ (i : ι), WellFounded (s i)<VAR>DecidableEq ι<VAR>(i : ι) → (x : α i) → Decidable (x ≠ 0)<VAR>x : Π₀ (i : ι), α i<VAR>h : ∀ i ∈ x.support, Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) i<GOAL>Acc (DFinsupp.Lex r s) x
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0<VAR>hs : ∀ (i : ι), WellFounded (s i)<VAR>hr : WellFounded (rᶜ ⊓ fun x x_1 => x ≠ x_1)<GOAL>WellFounded (DFinsupp.Lex r s)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0<VAR>hs : ∀ (i : ι), WellFounded (s i)<VAR>IsTrichotomous ι r<VAR>hr : WellFounded (Function.swap r)<GOAL>WellFounded (DFinsupp.Lex r s)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>IsStrictTotalOrder ι r<VAR>Finite ι<VAR>hs : ∀ (i : ι), WellFounded (s i)<GOAL>WellFounded (Pi.Lex r fun {i} => s i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>IsStrictTotalOrder ι r<VAR>Finite ι<VAR>(i : ι) → Zero (α i)<VAR>hs : ∀ (i : ι), WellFounded (s i)<GOAL>WellFounded (DFinsupp.Lex r s)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>(i : ι) → Zero (α i)<VAR>(i : ι) → Preorder (α i)<VAR>∀ (i : ι), WellFoundedLT (α i)<VAR>hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0<GOAL>WellFoundedLT (Π₀ (i : ι), α i)
<VAR>ds₁ ds₂ : List ℕ<VAR>is : List ℕ<VAR>eq : ds₁ = ds₂<VAR>h : List.Forall₂ (fun x x_1 => x < x_1) is ds₁<GOAL>↑(cast ⋯ ⟨is, h⟩) = is
<VAR>ds₁ ds₂ ds₃ : List ℕ<VAR>t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)<GOAL>t.assocRight.take = t.take.take
<VAR>ds₁ ds₂ ds₃ : List ℕ<VAR>t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)<GOAL>t.assocRight.drop.take = t.take.drop
<VAR>ds₁ ds₂ ds₃ : List ℕ<VAR>t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)<GOAL>t.assocRight.drop.drop = t.drop
<VAR>α : Type<VAR>ds₁ ds₂ : List ℕ<VAR>eq : ds₁ = ds₂<VAR>a : Holor α ds₁<GOAL>cast ⋯ a = fun t => a (cast ⋯ t)
<VAR>α : Type<VAR>ds₁ ds₂ ds₃ : List ℕ<VAR>Semigroup α<VAR>x : Holor α ds₁<VAR>y : Holor α ds₂<VAR>z : Holor α ds₃<GOAL>(x.mul y).mul z = (x.mul (y.mul z)).assocLeft
<VAR>α : Type<VAR>ds₁ ds₂ ds₃ : List ℕ<VAR>Semigroup α<VAR>x : Holor α ds₁<VAR>y : Holor α ds₂<VAR>z : Holor α ds₃<GOAL>HEq ((x.mul y).mul z) (x.mul (y.mul z))
<VAR>α : Type<VAR>ds₁ ds₂ : List ℕ<VAR>Distrib α<VAR>x : Holor α ds₁<VAR>y z : Holor α ds₂<GOAL>x.mul (y + z) = x.mul y + x.mul z
<VAR>α : Type<VAR>ds₁ ds₂ : List ℕ<VAR>Distrib α<VAR>x y : Holor α ds₁<VAR>z : Holor α ds₂<GOAL>(x + y).mul z = x.mul z + y.mul z
<VAR>ds₁ ds₂ : List ℕ<VAR>α : Type<VAR>Ring α<VAR>x : Holor α ds₂<GOAL>Holor.mul 0 x = 0
<VAR>ds₁ ds₂ : List ℕ<VAR>α : Type<VAR>Ring α<VAR>x : Holor α ds₁<GOAL>x.mul 0 = 0
<VAR>α : Type<VAR>ds : List ℕ<VAR>Monoid α<VAR>x : Holor α []<VAR>y : Holor α ds<GOAL>x.mul y = x ⟨[], ⋯⟩ • y
<VAR>d : ℕ<VAR>ds : List ℕ<VAR>p : HolorIndex (d :: ds) → Prop<VAR>t : HolorIndex (d :: ds)<GOAL>(∀ (i : ℕ) (is : List ℕ) (h : ↑t = i :: is), p ⟨i :: is, ⋯⟩) → p t
<VAR>α : Type<VAR>d : ℕ<VAR>ds : List ℕ<VAR>x y : Holor α (d :: ds)<VAR>h : x.slice = y.slice<GOAL>x = y
<VAR>α : Type<VAR>d : ℕ<VAR>ds : List ℕ<VAR>Ring α<VAR>i j : ℕ<VAR>hid : i < d<VAR>x : Holor α ds<GOAL>((Holor.unitVec d j).mul x).slice i hid = if i = j then x else 0
<VAR>α : Type<VAR>d : ℕ<VAR>ds : List ℕ<VAR>Add α<VAR>i : ℕ<VAR>hid : i < d<VAR>x y : Holor α (d :: ds)<GOAL>x.slice i hid + y.slice i hid = (x + y).slice i hid
<VAR>α : Type<VAR>d : ℕ<VAR>ds : List ℕ<VAR>Zero α<VAR>i : ℕ<VAR>hid : i < d<GOAL>Holor.slice 0 i hid = 0
<VAR>α : Type<VAR>d : ℕ<VAR>ds : List ℕ<VAR>AddCommMonoid α<VAR>β : Type<VAR>i : ℕ<VAR>hid : i < d<VAR>s : Finset β<VAR>f : β → Holor α (d :: ds)<GOAL>∑ x ∈ s, (f x).slice i hid = (∑ x ∈ s, f x).slice i hid
<VAR>α : Type<VAR>d : ℕ<VAR>ds : List ℕ<VAR>Ring α<VAR>x : Holor α (d :: ds)<GOAL>∑ i ∈ (Finset.range d).attach, (Holor.unitVec d ↑i).mul (x.slice ↑i ⋯) = x
<VAR>α : Type<VAR>Monoid α<VAR>AddMonoid α<VAR>x : Holor α []<GOAL>Holor.CPRankMax 1 x
<VAR>α : Type<VAR>ds : List ℕ<VAR>Monoid α<VAR>AddMonoid α<VAR>x : Holor α ds<VAR>h : x.CPRankMax1<GOAL>Holor.CPRankMax 1 x
<VAR>α : Type<VAR>ds : List ℕ<VAR>Monoid α<VAR>AddMonoid α<VAR>m n : ℕ<VAR>x y : Holor α ds<GOAL>Holor.CPRankMax m x → Holor.CPRankMax n y → Holor.CPRankMax (m + n) (x + y)
<VAR>α : Type<VAR>d : ℕ<VAR>ds : List ℕ<VAR>Ring α<VAR>n : ℕ<VAR>x : Holor α [d]<VAR>y : Holor α ds<GOAL>Holor.CPRankMax n y → Holor.CPRankMax n (x.mul y)
<VAR>α : Type<VAR>ds : List ℕ<VAR>Ring α<VAR>β : Type u_1<VAR>n : ℕ<VAR>s : Finset β<VAR>f : β → Holor α ds<GOAL>(∀ x ∈ s, Holor.CPRankMax n (f x)) → Holor.CPRankMax (s.card * n) (∑ x ∈ s, f x)
<VAR>α : Type<VAR>Ring α<VAR>ds : List ℕ<VAR>x : Holor α ds<GOAL>Holor.CPRankMax ds.prod x
<VAR>α : Type<VAR>Ring α<VAR>ds : List ℕ<VAR>x : Holor α ds<GOAL>x.cprank ≤ ds.prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>f : ι →₀ α<GOAL>f.rangeSingleton.support = f.support
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>f : ι →₀ α<VAR>i : ι<GOAL>f.rangeSingleton i = {f i}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>f : ι →₀ α<VAR>i : ι<VAR>a : α<GOAL>a ∈ f.rangeSingleton i ↔ a = f i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>f g : ι →₀ α<VAR>i : ι<GOAL>(f.rangeIcc g) i = Finset.Icc (f i) (g i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>i : ι<VAR>f g : ι →₀ α<GOAL>(f.rangeIcc g) i = Finset.Icc (f i) (g i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>f g : ι →₀ α<GOAL>(f.rangeIcc g).support = f.support ∪ g.support
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>PartialOrder α<VAR>LocallyFiniteOrder α<VAR>f g : ι →₀ α<VAR>i : ι<VAR>a : α<GOAL>a ∈ (f.rangeIcc g) i ↔ f i ≤ a ∧ a ≤ g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>PartialOrder α<VAR>Zero α<VAR>LocallyFiniteOrder α<VAR>f g : ι →₀ α<GOAL>Finset.Icc f g = (f.support ∪ g.support).finsupp ⇑(f.rangeIcc g)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>PartialOrder α<VAR>Zero α<VAR>LocallyFiniteOrder α<VAR>f g : ι →₀ α<GOAL>(Finset.Icc f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.Icc (f i) (g i)).card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>PartialOrder α<VAR>Zero α<VAR>LocallyFiniteOrder α<VAR>f g : ι →₀ α<GOAL>(Finset.Ico f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.Icc (f i) (g i)).card - 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>PartialOrder α<VAR>Zero α<VAR>LocallyFiniteOrder α<VAR>f g : ι →₀ α<GOAL>(Finset.Ioc f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.Icc (f i) (g i)).card - 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>PartialOrder α<VAR>Zero α<VAR>LocallyFiniteOrder α<VAR>f g : ι →₀ α<GOAL>(Finset.Ioo f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.Icc (f i) (g i)).card - 2
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Lattice α<VAR>Zero α<VAR>LocallyFiniteOrder α<VAR>f g : ι →₀ α<GOAL>(Finset.uIcc f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.uIcc (f i) (g i)).card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CanonicallyOrderedAddCommMonoid α<VAR>LocallyFiniteOrder α<VAR>f : ι →₀ α<GOAL>(Finset.Iic f).card = ∏ i ∈ f.support, (Finset.Iic (f i)).card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CanonicallyOrderedAddCommMonoid α<VAR>LocallyFiniteOrder α<VAR>f : ι →₀ α<GOAL>(Finset.Iio f).card = ∏ i ∈ f.support, (Finset.Iic (f i)).card - 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>s : Finset ι<VAR>i : ι<VAR>hi : i ∈ s<VAR>f : (i : ι) → i ∈ s → α<GOAL>(Finsupp.indicator s f) i = f i hi
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>s : Finset ι<VAR>i : ι<VAR>hi : i ∉ s<VAR>f : (i : ι) → i ∈ s → α<GOAL>(Finsupp.indicator s f) i = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>s : Finset ι<VAR>f : (i : ι) → i ∈ s → α<VAR>i : ι<VAR>DecidableEq ι<GOAL>(Finsupp.indicator s f) i = if hi : i ∈ s then f i hi else 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>s : Finset ι<GOAL>Function.Injective fun f => Finsupp.indicator s f
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>s : Finset ι<VAR>f : (i : ι) → i ∈ s → α<GOAL>↑(Finsupp.indicator s f).support ⊆ ↑s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>i : ι<VAR>b : α<GOAL>Finsupp.single i b = Finsupp.indicator {i} fun x x => b
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>Zero M<VAR>f : ι →₀ M<GOAL>⇑f.toDFinsupp = ⇑f
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>Zero M<VAR>i : ι<VAR>m : M<GOAL>(Finsupp.single i m).toDFinsupp = DFinsupp.single i m
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>Zero M<VAR>(m : M) → Decidable (m ≠ 0)<VAR>f : ι →₀ M<GOAL>f.toDFinsupp.support = f.support
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>Zero M<VAR>(m : M) → Decidable (m ≠ 0)<VAR>f : Π₀ (x : ι), M<GOAL>⇑f.toFinsupp = ⇑f
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>Zero M<VAR>(m : M) → Decidable (m ≠ 0)<VAR>f : Π₀ (x : ι), M<GOAL>f.toFinsupp.support = f.support
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>Zero M<VAR>(m : M) → Decidable (m ≠ 0)<VAR>i : ι<VAR>m : M<GOAL>(DFinsupp.single i m).toFinsupp = Finsupp.single i m
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>Zero M<VAR>(m : M) → Decidable (m ≠ 0)<VAR>f : ι →₀ M<GOAL>f.toDFinsupp.toFinsupp = f
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>Zero M<VAR>(m : M) → Decidable (m ≠ 0)<VAR>f : Π₀ (x : ι), M<GOAL>f.toFinsupp.toDFinsupp = f
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>Zero M<GOAL>Finsupp.toDFinsupp 0 = 0
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>AddZeroClass M<VAR>f g : ι →₀ M<GOAL>(f + g).toDFinsupp = f.toDFinsupp + g.toDFinsupp
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>AddGroup M<VAR>f : ι →₀ M<GOAL>(-f).toDFinsupp = -f.toDFinsupp
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>AddGroup M<VAR>f g : ι →₀ M<GOAL>(f - g).toDFinsupp = f.toDFinsupp - g.toDFinsupp
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>Monoid R<VAR>AddMonoid M<VAR>DistribMulAction R M<VAR>r : R<VAR>f : ι →₀ M<GOAL>(r • f).toDFinsupp = r • f.toDFinsupp
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>Zero M<VAR>(m : M) → Decidable (m ≠ 0)<GOAL>DFinsupp.toFinsupp 0 = 0
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>AddZeroClass M<VAR>(m : M) → Decidable (m ≠ 0)<VAR>f g : Π₀ (x : ι), M<GOAL>(f + g).toFinsupp = f.toFinsupp + g.toFinsupp
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>AddGroup M<VAR>(m : M) → Decidable (m ≠ 0)<VAR>f : Π₀ (x : ι), M<GOAL>(-f).toFinsupp = -f.toFinsupp
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>AddGroup M<VAR>(m : M) → Decidable (m ≠ 0)<VAR>f g : Π₀ (x : ι), M<GOAL>(f - g).toFinsupp = f.toFinsupp - g.toFinsupp
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>Monoid R<VAR>AddMonoid M<VAR>DistribMulAction R M<VAR>(m : M) → Decidable (m ≠ 0)<VAR>r : R<VAR>f : Π₀ (x : ι), M<GOAL>(r • f).toFinsupp = r • f.toFinsupp
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>Zero M<VAR>(m : M) → Decidable (m ≠ 0)<GOAL>⇑finsuppEquivDFinsupp.symm = DFinsupp.toFinsupp
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>Zero M<VAR>(m : M) → Decidable (m ≠ 0)<GOAL>⇑finsuppEquivDFinsupp = Finsupp.toDFinsupp
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>AddZeroClass M<VAR>(m : M) → Decidable (m ≠ 0)<GOAL>⇑finsuppAddEquivDFinsupp = Finsupp.toDFinsupp
<VAR>ι : Type u_1<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>AddZeroClass M<VAR>(m : M) → Decidable (m ≠ 0)<GOAL>⇑finsuppAddEquivDFinsupp.symm = DFinsupp.toFinsupp
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>Semiring R<VAR>AddCommMonoid M<VAR>(m : M) → Decidable (m ≠ 0)<VAR>Module R M<GOAL>⇑(finsuppLequivDFinsupp R) = Finsupp.toDFinsupp
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>DecidableEq ι<VAR>Semiring R<VAR>AddCommMonoid M<VAR>(m : M) → Decidable (m ≠ 0)<VAR>Module R M<GOAL>⇑(finsuppLequivDFinsupp R).symm = DFinsupp.toFinsupp
<VAR>ι : Type u_1<VAR>η : ι → Type u_4<VAR>N : Type u_5<VAR>Zero N<VAR>f : (i : ι) × η i →₀ N<GOAL>⇑(sigmaFinsuppEquivDFinsupp f) = f.split
<VAR>ι : Type u_1<VAR>η : ι → Type u_4<VAR>N : Type u_5<VAR>Zero N<VAR>f : Π₀ (i : ι), η i →₀ N<VAR>s : (i : ι) × η i<GOAL>(sigmaFinsuppEquivDFinsupp.symm f) s = (f s.fst) s.snd
<VAR>ι : Type u_1<VAR>η : ι → Type u_4<VAR>N : Type u_5<VAR>DecidableEq ι<VAR>Zero N<VAR>(i : ι) → (x : η i →₀ N) → Decidable (x ≠ 0)<VAR>f : (i : ι) × η i →₀ N<GOAL>(sigmaFinsuppEquivDFinsupp f).support = f.splitSupport
<VAR>ι : Type u_1<VAR>η : ι → Type u_4<VAR>N : Type u_5<VAR>DecidableEq ι<VAR>Zero N<VAR>a : (i : ι) × η i<VAR>n : N<GOAL>sigmaFinsuppEquivDFinsupp (Finsupp.single a n) = DFinsupp.single a.fst (Finsupp.single a.snd n)
<VAR>ι : Type u_1<VAR>η : ι → Type u_4<VAR>N : Type u_5<VAR>AddZeroClass N<VAR>f g : (i : ι) × η i →₀ N<GOAL>sigmaFinsuppEquivDFinsupp (f + g) = sigmaFinsuppEquivDFinsupp f + sigmaFinsuppEquivDFinsupp g
<VAR>ι : Type u_1<VAR>η : ι → Type u_4<VAR>N : Type u_5<VAR>AddZeroClass N<VAR>a : (i : ι) × η i →₀ N<GOAL>sigmaFinsuppAddEquivDFinsupp a = sigmaFinsuppEquivDFinsupp a
<VAR>ι : Type u_1<VAR>η : ι → Type u_4<VAR>N : Type u_5<VAR>AddZeroClass N<VAR>a : Π₀ (i : ι), η i →₀ N<GOAL>sigmaFinsuppAddEquivDFinsupp.symm a = sigmaFinsuppEquivDFinsupp.symm a
<VAR>ι : Type u_1<VAR>η : ι → Type u_4<VAR>N : Type u_5<VAR>R : Type u_6<VAR>Monoid R<VAR>AddMonoid N<VAR>DistribMulAction R N<VAR>r : R<VAR>f : (i : ι) × η i →₀ N<GOAL>sigmaFinsuppEquivDFinsupp (r • f) = r • sigmaFinsuppEquivDFinsupp f
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>η : ι → Type u_4<VAR>N : Type u_5<VAR>Semiring R<VAR>AddCommMonoid N<VAR>Module R N<VAR>a : Π₀ (i : ι), η i →₀ N<GOAL>(sigmaFinsuppLequivDFinsupp R).symm a = sigmaFinsuppEquivDFinsupp.symm a
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>η : ι → Type u_4<VAR>N : Type u_5<VAR>Semiring R<VAR>AddCommMonoid N<VAR>Module R N<VAR>a : (i : ι) × η i →₀ N<GOAL>(sigmaFinsuppLequivDFinsupp R) a = sigmaFinsuppEquivDFinsupp a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>LE α<VAR>f g : ι →₀ α<GOAL>f ≤ g ↔ ∀ (i : ι), f i ≤ g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>LE α<VAR>f g : ι →₀ α<GOAL>⇑f ≤ ⇑g ↔ f ≤ g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>LE α<VAR>f : ι →₀ α<VAR>i : ι<GOAL>Finsupp.orderEmbeddingToFun f i = f i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>Preorder α<VAR>f g : ι →₀ α<GOAL>f < g ↔ f ≤ g ∧ ∃ i, f i < g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>Preorder α<VAR>f g : ι →₀ α<GOAL>⇑f < ⇑g ↔ f < g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>Preorder α<GOAL>Monotone Finsupp.toFun
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>SemilatticeInf α<VAR>i : ι<VAR>f g : ι →₀ α<GOAL>(f ⊓ g) i = f i ⊓ g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>SemilatticeSup α<VAR>i : ι<VAR>f g : ι →₀ α<GOAL>(f ⊔ g) i = f i ⊔ g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>DecidableEq ι<VAR>Lattice α<VAR>f g : ι →₀ α<GOAL>(f ⊓ g).support ∪ (f ⊔ g).support = f.support ∪ g.support
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>DecidableEq ι<VAR>Lattice α<VAR>f g : ι →₀ α<GOAL>(f ⊔ g).support ∪ (f ⊓ g).support = f.support ∪ g.support
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CanonicallyOrderedAddCommMonoid α<GOAL>⊥ = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CanonicallyOrderedAddCommMonoid α<VAR>f g : ι →₀ α<GOAL>f + g = 0 ↔ f = 0 ∧ g = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CanonicallyOrderedAddCommMonoid α<VAR>f g : ι →₀ α<VAR>s : Finset ι<VAR>hf : f.support ⊆ s<GOAL>f ≤ g ↔ ∀ i ∈ s, f i ≤ g i