ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>NontriviallyNormedField K<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace K F<VAR>m : ℕ<VAR>f : K → F<VAR>hf : ContDiff K (↑m + 1) f<GOAL>Differentiable K (iteratedDeriv m f)
<VAR>ι : Type u_1<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>s : Finset ι<VAR>a : ι → ZMod p<GOAL>(f₁ s a).totalDegree + (f₂ s a).totalDegree < 2 * p - 1
<VAR>ι : Type u_1<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>s : Finset ι<VAR>a : ι → ZMod p<VAR>hs : s.card = 2 * p - 1<GOAL>∃ t ⊆ s, t.card = p ∧ ∑ i ∈ t, a i = 0
<VAR>ι : Type u_1<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>s : Finset ι<VAR>a : ι → ℤ<VAR>hs : s.card = 2 * p - 1<GOAL>∃ t ⊆ s, t.card = p ∧ ↑p ∣ ∑ i ∈ t, a i
<VAR>ι : Type u_1<VAR>n : ℕ<VAR>s : Finset ι<VAR>a : ι → ℤ<VAR>hs : 2 * n - 1 ≤ s.card<GOAL>∃ t ⊆ s, t.card = n ∧ ↑n ∣ ∑ i ∈ t, a i
<VAR>n : ℕ<VAR>s : Multiset ℤ<VAR>hs : 2 * n - 1 ≤ Multiset.card s<GOAL>∃ t ≤ s, Multiset.card t = n ∧ ↑n ∣ t.sum
<VAR>n : ℕ<VAR>s : Multiset (ZMod n)<VAR>hs : 2 * n - 1 ≤ Multiset.card s<GOAL>∃ t ≤ s, Multiset.card t = n ∧ t.sum = 0
<VAR>G : Type u_1<VAR>AddCommGroup G<VAR>A : Finset (G × G)<VAR>a b c : G<GOAL>(a, b, c) ∈ Corners.triangleIndices A ↔ (a, b) ∈ A ∧ c = a + b
<VAR>G : Type u_1<VAR>AddCommGroup G<VAR>A : Finset (G × G)<GOAL>(Corners.triangleIndices A).card = A.card
<VAR>G : Type u_1<VAR>AddCommGroup G<VAR>A : Finset (G × G)<VAR>hs : IsCornerFree ↑A<GOAL>SimpleGraph.TripartiteFromTriangles.NoAccidental (Corners.triangleIndices A)
<VAR>G : Type u_1<VAR>AddCommGroup G<VAR>Fintype G<VAR>A : Finset (G × G)<VAR>ε : ℝ<VAR>DecidableEq G<VAR>hε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑A.card<GOAL>(SimpleGraph.TripartiteFromTriangles.graph (Corners.triangleIndices A)).FarFromTriangleFree (ε / 9)
<VAR>G : Type u_1<VAR>AddCommGroup G<VAR>Fintype G<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hG : cornersTheoremBound ε ≤ Fintype.card G<VAR>A : Finset (G × G)<VAR>hAε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑A.card<GOAL>¬IsCornerFree ↑A
<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hn : cornersTheoremBound (ε / 9) ≤ n<VAR>A : Finset (ℕ × ℕ)<VAR>hAn : A ⊆ Finset.range n ×ˢ Finset.range n<VAR>hAε : ε * ↑n ^ 2 ≤ ↑A.card<GOAL>¬IsCornerFree ↑A
<VAR>G : Type u_1<VAR>AddCommGroup G<VAR>Fintype G<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hG : cornersTheoremBound ε ≤ Fintype.card G<VAR>A : Finset G<VAR>hAε : ε * ↑(Fintype.card G) ≤ ↑A.card<GOAL>¬ThreeAPFree ↑A
<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hG : cornersTheoremBound (ε / 3) ≤ n<VAR>A : Finset ℕ<VAR>hAn : A ⊆ Finset.range n<VAR>hAε : ε * ↑n ≤ ↑A.card<GOAL>¬ThreeAPFree ↑A
<GOAL>(fun N => ↑(rothNumberNat N)) =o[Filter.atTop] fun N => ↑N
<VAR>R : Type u_1<VAR>Ring R<VAR>p : ℕ<VAR>CharP R p<VAR>k : ℤ<GOAL>↑k = ↑(k % ↑p)
<VAR>e' r : ℤ<VAR>α : Type u_1<VAR>Ring α<VAR>n n' : ℕ<VAR>inst : CharP α n<VAR>e : α<VAR>he : Mathlib.Meta.NormNum.IsInt e e'<VAR>hn : Mathlib.Meta.NormNum.IsNat n n'<VAR>h₂ : Mathlib.Meta.NormNum.IsInt (e' % ↑n') r<GOAL>Mathlib.Meta.NormNum.IsInt e r
<VAR>α : Type u_1<VAR>Ring α<VAR>n : ℕ<VAR>inst : CharP α n<VAR>b : α<VAR>a : ℕ<VAR>a' : α<VAR>p : Mathlib.Meta.NormNum.IsNat (↑n - 1) a<VAR>pa : ↑a = a'<GOAL>-b = a' * b
<VAR>α : Type u_1<VAR>Ring α<VAR>n : ℕ<VAR>inst : CharP α n<VAR>a b : α<VAR>na : ℕ<VAR>na' : α<VAR>p : Mathlib.Meta.NormNum.IsNat ((↑n - 1) * a) na<VAR>pa : ↑na = na'<GOAL>-(a * b) = na' * b
<VAR>K : Type u_1<VAR>NontriviallyNormedField K<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>s : Set E<GOAL>DifferentiableOn K (fun x => x) s
<VAR>K : Type u_1<VAR>NontriviallyNormedField K<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace K F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace K G<VAR>f : E → F<VAR>g : F → G<VAR>hg : Differentiable K g<VAR>hf : Differentiable K f<GOAL>Differentiable K fun x => g (f x)
<VAR>K : Type u_1<VAR>NontriviallyNormedField K<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace K F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace K G<VAR>x : E<VAR>f : E → F<VAR>g : F → G<VAR>hg : DifferentiableAt K g (f x)<VAR>hf : DifferentiableAt K f x<GOAL>DifferentiableAt K (fun x => g (f x)) x
<VAR>K : Type u_1<VAR>NontriviallyNormedField K<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace K E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace K F<VAR>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace K G<VAR>f : E → F<VAR>s : Set E<VAR>g : F → G<VAR>t : Set F<VAR>hg : DifferentiableOn K g t<VAR>hf : DifferentiableOn K f s<VAR>st : Set.MapsTo f s t<GOAL>DifferentiableOn K (fun x => g (f x)) s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>n : ℕ<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>self : IsAddFreimanHom n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : Multiset.card s = n<VAR>ht : Multiset.card t = n<VAR>h : s.sum = t.sum<GOAL>(Multiset.map f s).sum = (Multiset.map f t).sum
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>n : ℕ<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>self : IsAddFreimanHom n A B f<GOAL>Set.MapsTo f A B
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommMonoid α<VAR>CommMonoid β<VAR>n : ℕ<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>self : IsMulFreimanHom n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : Multiset.card s = n<VAR>ht : Multiset.card t = n<VAR>h : s.prod = t.prod<GOAL>(Multiset.map f s).prod = (Multiset.map f t).prod
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommMonoid α<VAR>CommMonoid β<VAR>n : ℕ<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>self : IsMulFreimanHom n A B f<GOAL>Set.MapsTo f A B
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>n : ℕ<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>self : IsAddFreimanIso n A B f<GOAL>Set.BijOn f A B
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>n : ℕ<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>self : IsAddFreimanIso n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : Multiset.card s = n<VAR>ht : Multiset.card t = n<GOAL>(Multiset.map f s).sum = (Multiset.map f t).sum ↔ s.sum = t.sum
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommMonoid α<VAR>CommMonoid β<VAR>n : ℕ<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>self : IsMulFreimanIso n A B f<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : Multiset.card s = n<VAR>ht : Multiset.card t = n<GOAL>(Multiset.map f s).prod = (Multiset.map f t).prod ↔ s.prod = t.prod
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommMonoid α<VAR>CommMonoid β<VAR>n : ℕ<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>self : IsMulFreimanIso n A B f<GOAL>Set.BijOn f A B
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>n : ℕ<VAR>hf : IsAddFreimanIso n A B f<GOAL>IsAddFreimanHom n A B f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommMonoid α<VAR>CommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>n : ℕ<VAR>hf : IsMulFreimanIso n A B f<GOAL>IsMulFreimanHom n A B f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>hf : IsAddFreimanHom 2 A B f<VAR>a b c d : α<VAR>ha : a ∈ A<VAR>hb : b ∈ A<VAR>hc : c ∈ A<VAR>hd : d ∈ A<VAR>h : a + b = c + d<GOAL>f a + f b = f c + f d
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommMonoid α<VAR>CommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>hf : IsMulFreimanHom 2 A B f<VAR>a b c d : α<VAR>ha : a ∈ A<VAR>hb : b ∈ A<VAR>hc : c ∈ A<VAR>hd : d ∈ A<VAR>h : a * b = c * d<GOAL>f a * f b = f c * f d
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommMonoid α<VAR>CommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>hf : IsMulFreimanIso 2 A B f<VAR>a b c d : α<VAR>ha : a ∈ A<VAR>hb : b ∈ A<VAR>hc : c ∈ A<VAR>hd : d ∈ A<GOAL>f a * f b = f c * f d ↔ a * b = c * d
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>hf : IsAddFreimanIso 2 A B f<VAR>a b c d : α<VAR>ha : a ∈ A<VAR>hb : b ∈ A<VAR>hc : c ∈ A<VAR>hd : d ∈ A<GOAL>f a + f b = f c + f d ↔ a + b = c + d
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommMonoid α<VAR>CommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<GOAL>IsMulFreimanHom 2 A B f ↔ Set.MapsTo f A B ∧ ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A, a * b = c * d → f a * f b = f c * f d
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<GOAL>IsAddFreimanHom 2 A B f ↔ Set.MapsTo f A B ∧ ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A, a + b = c + d → f a + f b = f c + f d
<VAR>α : Type u_2<VAR>CommMonoid α<VAR>A₁ A₂ : Set α<VAR>n : ℕ<VAR>hA : A₁ ⊆ A₂<GOAL>IsMulFreimanHom n A₁ A₂ id
<VAR>α : Type u_2<VAR>AddCommMonoid α<VAR>A₁ A₂ : Set α<VAR>n : ℕ<VAR>hA : A₁ ⊆ A₂<GOAL>IsAddFreimanHom n A₁ A₂ id
<VAR>α : Type u_2<VAR>CommMonoid α<VAR>A : Set α<VAR>n : ℕ<GOAL>IsMulFreimanIso n A A id
<VAR>α : Type u_2<VAR>AddCommMonoid α<VAR>A : Set α<VAR>n : ℕ<GOAL>IsAddFreimanIso n A A id
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>AddCommMonoid γ<VAR>A : Set α<VAR>B : Set β<VAR>C : Set γ<VAR>f : α → β<VAR>g : β → γ<VAR>n : ℕ<VAR>hg : IsAddFreimanHom n B C g<VAR>hf : IsAddFreimanHom n A B f<GOAL>IsAddFreimanHom n A C (g ∘ f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>CommMonoid α<VAR>CommMonoid β<VAR>CommMonoid γ<VAR>A : Set α<VAR>B : Set β<VAR>C : Set γ<VAR>f : α → β<VAR>g : β → γ<VAR>n : ℕ<VAR>hg : IsMulFreimanHom n B C g<VAR>hf : IsMulFreimanHom n A B f<GOAL>IsMulFreimanHom n A C (g ∘ f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>AddCommMonoid γ<VAR>A : Set α<VAR>B : Set β<VAR>C : Set γ<VAR>f : α → β<VAR>g : β → γ<VAR>n : ℕ<VAR>hg : IsAddFreimanIso n B C g<VAR>hf : IsAddFreimanIso n A B f<GOAL>IsAddFreimanIso n A C (g ∘ f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>CommMonoid α<VAR>CommMonoid β<VAR>CommMonoid γ<VAR>A : Set α<VAR>B : Set β<VAR>C : Set γ<VAR>f : α → β<VAR>g : β → γ<VAR>n : ℕ<VAR>hg : IsMulFreimanIso n B C g<VAR>hf : IsMulFreimanIso n A B f<GOAL>IsMulFreimanIso n A C (g ∘ f)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommMonoid α<VAR>CommMonoid β<VAR>A₁ A₂ : Set α<VAR>B₁ B₂ : Set β<VAR>f : α → β<VAR>n : ℕ<VAR>hA : A₁ ⊆ A₂<VAR>hf : IsMulFreimanHom n A₂ B₂ f<VAR>hf' : Set.MapsTo f A₁ B₁<GOAL>IsMulFreimanHom n A₁ B₁ f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>A₁ A₂ : Set α<VAR>B₁ B₂ : Set β<VAR>f : α → β<VAR>n : ℕ<VAR>hA : A₁ ⊆ A₂<VAR>hf : IsAddFreimanHom n A₂ B₂ f<VAR>hf' : Set.MapsTo f A₁ B₁<GOAL>IsAddFreimanHom n A₁ B₁ f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommMonoid α<VAR>CommMonoid β<VAR>A : Set α<VAR>B₁ B₂ : Set β<VAR>f : α → β<VAR>n : ℕ<VAR>hB : B₁ ⊆ B₂<VAR>hf : IsMulFreimanHom n A B₁ f<GOAL>IsMulFreimanHom n A B₂ f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>A : Set α<VAR>B₁ B₂ : Set β<VAR>f : α → β<VAR>n : ℕ<VAR>hB : B₁ ⊆ B₂<VAR>hf : IsAddFreimanHom n A B₁ f<GOAL>IsAddFreimanHom n A B₂ f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>A₁ A₂ : Set α<VAR>B₁ B₂ : Set β<VAR>f : α → β<VAR>n : ℕ<VAR>hA : A₁ ⊆ A₂<VAR>hf : IsAddFreimanIso n A₂ B₂ f<VAR>hf' : Set.BijOn f A₁ B₁<GOAL>IsAddFreimanIso n A₁ B₁ f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommMonoid α<VAR>CommMonoid β<VAR>A₁ A₂ : Set α<VAR>B₁ B₂ : Set β<VAR>f : α → β<VAR>n : ℕ<VAR>hA : A₁ ⊆ A₂<VAR>hf : IsMulFreimanIso n A₂ B₂ f<VAR>hf' : Set.BijOn f A₁ B₁<GOAL>IsMulFreimanIso n A₁ B₁ f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommMonoid α<VAR>CommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>n : ℕ<VAR>b : β<VAR>hb : b ∈ B<GOAL>IsMulFreimanHom n A B fun x => b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>n : ℕ<VAR>b : β<VAR>hb : b ∈ B<GOAL>IsAddFreimanHom n A B fun x => b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>f : α → β<VAR>n : ℕ<GOAL>IsAddFreimanIso n ∅ ∅ f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommMonoid α<VAR>CommMonoid β<VAR>f : α → β<VAR>n : ℕ<GOAL>IsMulFreimanIso n ∅ ∅ f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommMonoid α<VAR>CommMonoid β<VAR>A : Set α<VAR>B₁ B₂ : Set β<VAR>f₁ f₂ : α → β<VAR>n : ℕ<VAR>h₁ : IsMulFreimanHom n A B₁ f₁<VAR>h₂ : IsMulFreimanHom n A B₂ f₂<GOAL>IsMulFreimanHom n A (B₁ * B₂) (f₁ * f₂)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>A : Set α<VAR>B₁ B₂ : Set β<VAR>f₁ f₂ : α → β<VAR>n : ℕ<VAR>h₁ : IsAddFreimanHom n A B₁ f₁<VAR>h₂ : IsAddFreimanHom n A B₂ f₂<GOAL>IsAddFreimanHom n A (B₁ + B₂) (f₁ + f₂)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>n : ℕ<VAR>FunLike F α β<VAR>AddMonoidHomClass F α β<VAR>f : F<VAR>hfAB : Set.MapsTo (⇑f) A B<GOAL>IsAddFreimanHom n A B ⇑f
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommMonoid α<VAR>CommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>n : ℕ<VAR>FunLike F α β<VAR>MonoidHomClass F α β<VAR>f : F<VAR>hfAB : Set.MapsTo (⇑f) A B<GOAL>IsMulFreimanHom n A B ⇑f
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommMonoid α<VAR>CommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>n : ℕ<VAR>EquivLike F α β<VAR>MulEquivClass F α β<VAR>f : F<VAR>hfAB : Set.BijOn (⇑f) A B<GOAL>IsMulFreimanIso n A B ⇑f
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>n : ℕ<VAR>EquivLike F α β<VAR>AddEquivClass F α β<VAR>f : F<VAR>hfAB : Set.BijOn (⇑f) A B<GOAL>IsAddFreimanIso n A B ⇑f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoid α<VAR>AddCancelCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hf : IsAddFreimanHom n A B f<GOAL>IsAddFreimanHom m A B f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommMonoid α<VAR>CancelCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hf : IsMulFreimanHom n A B f<GOAL>IsMulFreimanHom m A B f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCancelCommMonoid α<VAR>AddCancelCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hf : IsAddFreimanIso n A B f<GOAL>IsAddFreimanIso m A B f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CancelCommMonoid α<VAR>CancelCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hf : IsMulFreimanIso n A B f<GOAL>IsMulFreimanIso m A B f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommMonoid α<VAR>DivisionCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>n : ℕ<VAR>hf : IsMulFreimanHom n A B f<GOAL>IsMulFreimanHom n A B⁻¹ f⁻¹
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoid α<VAR>SubtractionCommMonoid β<VAR>A : Set α<VAR>B : Set β<VAR>f : α → β<VAR>n : ℕ<VAR>hf : IsAddFreimanHom n A B f<GOAL>IsAddFreimanHom n A (-B) (-f)
<VAR>α : Type u_2<VAR>CommMonoid α<VAR>A : Set α<VAR>n : ℕ<VAR>β : Type u_5<VAR>DivisionCommMonoid β<VAR>B₁ B₂ : Set β<VAR>f₁ f₂ : α → β<VAR>h₁ : IsMulFreimanHom n A B₁ f₁<VAR>h₂ : IsMulFreimanHom n A B₂ f₂<GOAL>IsMulFreimanHom n A (B₁ / B₂) (f₁ / f₂)
<VAR>α : Type u_2<VAR>AddCommMonoid α<VAR>A : Set α<VAR>n : ℕ<VAR>β : Type u_5<VAR>SubtractionCommMonoid β<VAR>B₁ B₂ : Set β<VAR>f₁ f₂ : α → β<VAR>h₁ : IsAddFreimanHom n A B₁ f₁<VAR>h₂ : IsAddFreimanHom n A B₂ f₂<GOAL>IsAddFreimanHom n A (B₁ - B₂) (f₁ - f₂)
<VAR>α₁ : Type u_5<VAR>α₂ : Type u_6<VAR>β₁ : Type u_7<VAR>β₂ : Type u_8<VAR>AddCommMonoid α₁<VAR>AddCommMonoid α₂<VAR>AddCommMonoid β₁<VAR>AddCommMonoid β₂<VAR>A₁ : Set α₁<VAR>A₂ : Set α₂<VAR>B₁ : Set β₁<VAR>B₂ : Set β₂<VAR>f₁ : α₁ → β₁<VAR>f₂ : α₂ → β₂<VAR>n : ℕ<VAR>h₁ : IsAddFreimanHom n A₁ B₁ f₁<VAR>h₂ : IsAddFreimanHom n A₂ B₂ f₂<GOAL>IsAddFreimanHom n (A₁ ×ˢ A₂) (B₁ ×ˢ B₂) (Prod.map f₁ f₂)
<VAR>α₁ : Type u_5<VAR>α₂ : Type u_6<VAR>β₁ : Type u_7<VAR>β₂ : Type u_8<VAR>CommMonoid α₁<VAR>CommMonoid α₂<VAR>CommMonoid β₁<VAR>CommMonoid β₂<VAR>A₁ : Set α₁<VAR>A₂ : Set α₂<VAR>B₁ : Set β₁<VAR>B₂ : Set β₂<VAR>f₁ : α₁ → β₁<VAR>f₂ : α₂ → β₂<VAR>n : ℕ<VAR>h₁ : IsMulFreimanHom n A₁ B₁ f₁<VAR>h₂ : IsMulFreimanHom n A₂ B₂ f₂<GOAL>IsMulFreimanHom n (A₁ ×ˢ A₂) (B₁ ×ˢ B₂) (Prod.map f₁ f₂)
<VAR>α₁ : Type u_5<VAR>α₂ : Type u_6<VAR>β₁ : Type u_7<VAR>β₂ : Type u_8<VAR>AddCommMonoid α₁<VAR>AddCommMonoid α₂<VAR>AddCommMonoid β₁<VAR>AddCommMonoid β₂<VAR>A₁ : Set α₁<VAR>A₂ : Set α₂<VAR>B₁ : Set β₁<VAR>B₂ : Set β₂<VAR>f₁ : α₁ → β₁<VAR>f₂ : α₂ → β₂<VAR>n : ℕ<VAR>h₁ : IsAddFreimanIso n A₁ B₁ f₁<VAR>h₂ : IsAddFreimanIso n A₂ B₂ f₂<GOAL>IsAddFreimanIso n (A₁ ×ˢ A₂) (B₁ ×ˢ B₂) (Prod.map f₁ f₂)
<VAR>α₁ : Type u_5<VAR>α₂ : Type u_6<VAR>β₁ : Type u_7<VAR>β₂ : Type u_8<VAR>CommMonoid α₁<VAR>CommMonoid α₂<VAR>CommMonoid β₁<VAR>CommMonoid β₂<VAR>A₁ : Set α₁<VAR>A₂ : Set α₂<VAR>B₁ : Set β₁<VAR>B₂ : Set β₂<VAR>f₁ : α₁ → β₁<VAR>f₂ : α₂ → β₂<VAR>n : ℕ<VAR>h₁ : IsMulFreimanIso n A₁ B₁ f₁<VAR>h₂ : IsMulFreimanIso n A₂ B₂ f₂<GOAL>IsMulFreimanIso n (A₁ ×ˢ A₂) (B₁ ×ˢ B₂) (Prod.map f₁ f₂)
<VAR>k m n : ℕ<VAR>hm : m ≠ 0<VAR>hkmn : m * k ≤ n<GOAL>k < n + 1
<VAR>k m n : ℕ<VAR>hm : m ≠ 0<VAR>hkmn : m * k ≤ n<GOAL>IsAddFreimanIso m (Set.Iic ↑k) (Set.Iic k) Fin.val
<VAR>k m n : ℕ<VAR>hm : m ≠ 0<VAR>hkmn : m * k ≤ n<GOAL>IsAddFreimanIso m (Set.Iio ↑k) (Set.Iio k) Fin.val
<VAR>a b : Prop<VAR>h : a = True<GOAL>(a ↔ b) = b
<VAR>a b : Prop<VAR>h : b = True<GOAL>(a ↔ b) = a
<VAR>a b : Prop<VAR>h : a = b<GOAL>(a ↔ b) = True
<VAR>a b : Prop<VAR>h : a = True<GOAL>(a ∧ b) = b
<VAR>a b : Prop<VAR>h : b = True<GOAL>(a ∧ b) = a
<VAR>a b : Prop<VAR>h : a = False<GOAL>(a ∧ b) = False
<VAR>a b : Prop<VAR>h : b = False<GOAL>(a ∧ b) = False
<VAR>a b : Prop<VAR>h : a = b<GOAL>(a ∧ b) = a
<VAR>a b : Prop<VAR>h : a = True<GOAL>(a ∨ b) = True
<VAR>a b : Prop<VAR>h : b = True<GOAL>(a ∨ b) = True
<VAR>a b : Prop<VAR>h : a = False<GOAL>(a ∨ b) = b
<VAR>a b : Prop<VAR>h : b = False<GOAL>(a ∨ b) = a
<VAR>a b : Prop<VAR>h : a = b<GOAL>(a ∨ b) = a
<VAR>a b : Prop<VAR>h : a = True<GOAL>(a → b) = b
<VAR>a b : Prop<VAR>h : b = True<GOAL>(a → b) = True
<VAR>a b : Prop<VAR>h : a = False<GOAL>(a → b) = True
<VAR>a b : Prop<VAR>h : b = False<GOAL>(a → b) = ¬a
<VAR>a b : Prop<VAR>h : b = False<GOAL>(¬a → b) = a
<VAR>a b : Prop<VAR>h : a = b<GOAL>(a → b) = True
<VAR>a : Prop<VAR>h : a = True<GOAL>(¬a) = False
<VAR>a : Prop<VAR>h : a = False<GOAL>(¬a) = True
<VAR>a : Prop<VAR>h : a = ¬a<GOAL>False
<VAR>c : Prop<VAR>d : Decidable c<VAR>α : Sort u<VAR>t e : α<VAR>h : c = True<GOAL>(if c then t else e) = t
<VAR>c : Prop<VAR>d : Decidable c<VAR>α : Sort u<VAR>t e : α<VAR>h : c = False<GOAL>(if c then t else e) = e
<VAR>c : Prop<VAR>d : Decidable c<VAR>α : Sort u<VAR>t e : α<VAR>h : t = e<GOAL>(if c then t else e) = t
<VAR>a b : Prop<VAR>h : (a ∧ b) = True<GOAL>a = True
<VAR>a b : Prop<VAR>h : (a ∧ b) = True<GOAL>b = True
<VAR>a b : Prop<VAR>h : (a ∨ b) = False<GOAL>a = False
<VAR>a b : Prop<VAR>h : (a ∨ b) = False<GOAL>b = False
<VAR>a : Prop<VAR>h : (¬a) = True<GOAL>a = False
<VAR>a : Prop<VAR>h : (¬a) = False<GOAL>a = True
<VAR>α : Type u_1<VAR>a b a' : α<VAR>LinearOrder α<VAR>h : ¬a < b<VAR>eq : a = a'<GOAL>b ≤ a'
<VAR>α : Type u_1<VAR>a b b' : α<VAR>LinearOrder α<VAR>h : ¬a < b<VAR>eq : b = b'<GOAL>b' ≤ a
<VAR>α : Type u_1<VAR>a b a' : α<VAR>LE α<VAR>h : ¬a ≤ b<VAR>eq : a = a'<GOAL>¬a' ≤ b
<VAR>α : Type u_1<VAR>a b b' : α<VAR>LE α<VAR>h : ¬a ≤ b<VAR>eq : b = b'<GOAL>¬a ≤ b'
<VAR>α : Type u_1<VAR>a b a' : α<VAR>LinearOrder α<VAR>h : a < b<VAR>eq : a = a'<GOAL>¬b ≤ a'
<VAR>α : Type u_1<VAR>a b b' : α<VAR>LinearOrder α<VAR>h : a < b<VAR>eq : b = b'<GOAL>¬b' ≤ a
<VAR>α : Type u_1<VAR>a b a' : α<VAR>LE α<VAR>h : a ≤ b<VAR>eq : a = a'<GOAL>a' ≤ b
<VAR>α : Type u_1<VAR>a b b' : α<VAR>LE α<VAR>h : a ≤ b<VAR>eq : b = b'<GOAL>a ≤ b'
<VAR>α : Type u_1<VAR>hi n lo : α<VAR>LinearOrder α<VAR>h1 : ¬hi ≤ n<VAR>h2 : hi ≤ lo<GOAL>n ≤ lo
<VAR>a b : ℤ<VAR>h : ¬b ≤ a<GOAL>a + 1 ≤ b
<VAR>a b : ℤ<VAR>h : ¬b ≤ a<GOAL>a ≤ b - 1
<VAR>α : Type u_1<VAR>CommRing α<VAR>n1 n2 k e1 e2 t1 t2 : α<VAR>h1 : n1 * e1 = t1<VAR>h2 : n2 * e2 = t2<VAR>h3 : n1 * n2 = k<GOAL>k * (e1 * e2) = t1 * t2
<VAR>α : Type u_1<VAR>Field α<VAR>n1 n2 k e1 e2 t1 : α<VAR>h1 : n1 * e1 = t1<VAR>h2 : n2 / e2 = 1<VAR>h3 : n1 * n2 = k<GOAL>k * (e1 / e2) = t1
<VAR>α : Type u_1<VAR>Field α<VAR>n e e' : α<VAR>h : n * e = e'<VAR>h2 : n ≠ 0<GOAL>e = e' / n
<VAR>α : Type u_1<VAR>Ring α<VAR>n e1 e2 t1 t2 : α<VAR>h1 : n * e1 = t1<VAR>h2 : n * e2 = t2<GOAL>n * (e1 + e2) = t1 + t2
<VAR>α : Type u_1<VAR>Ring α<VAR>n e1 e2 t1 t2 : α<VAR>h1 : n * e1 = t1<VAR>h2 : n * e2 = t2<GOAL>n * (e1 - e2) = t1 - t2
<VAR>α : Type u_1<VAR>Ring α<VAR>n e t : α<VAR>h1 : n * e = t<GOAL>n * -e = -t
<VAR>α : Type u_1<VAR>CommRing α<VAR>n e1 t1 k l : α<VAR>e2 : ℕ<VAR>h1 : n * e1 = t1<VAR>h2 : l * n ^ e2 = k<GOAL>k * e1 ^ e2 = l * t1 ^ e2
<VAR>α : Type u_1<VAR>Field α<VAR>n k e : α<VAR>h2 : e ≠ 0<VAR>h3 : n * e = k<GOAL>k * e⁻¹ = n
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b ad bd a' b' gcd : α<VAR>ha : ad * a = a'<VAR>hb : bd * b = b'<VAR>had : 0 < ad<VAR>hbd : 0 < bd<VAR>hgcd : 0 < gcd<GOAL>(a < b) = (1 / gcd * (bd * a') < 1 / gcd * (ad * b'))
<VAR>α : Type u_1<VAR>LinearOrderedField α<VAR>a b ad bd a' b' gcd : α<VAR>ha : ad * a = a'<VAR>hb : bd * b = b'<VAR>had : 0 < ad<VAR>hbd : 0 < bd<VAR>hgcd : 0 < gcd<GOAL>(a ≤ b) = (1 / gcd * (bd * a') ≤ 1 / gcd * (ad * b'))
<VAR>α : Type u_1<VAR>Field α<VAR>a b ad bd a' b' gcd : α<VAR>ha : ad * a = a'<VAR>hb : bd * b = b'<VAR>had : ad ≠ 0<VAR>hbd : bd ≠ 0<VAR>hgcd : gcd ≠ 0<GOAL>(a = b) = (1 / gcd * (bd * a') = 1 / gcd * (ad * b'))
<VAR>α : Type u_1<VAR>Field α<VAR>a b ad bd a' b' gcd : α<VAR>ha : ad * a = a'<VAR>hb : bd * b = b'<VAR>had : ad ≠ 0<VAR>hbd : bd ≠ 0<VAR>hgcd : gcd ≠ 0<GOAL>(a ≠ b) = (1 / gcd * (bd * a') ≠ 1 / gcd * (ad * b'))
<VAR>α : Type u_1<VAR>Mul α<VAR>a b c d : α<VAR>h : a = b<VAR>h' : c * b = d<GOAL>c * a = d
<VAR>p q : Prop<GOAL>(¬(p ∧ q)) = (p → ¬q)
<VAR>p q : Prop<GOAL>(¬(p ∨ q)) = (¬p ∧ ¬q)
<VAR>α : Sort u_1<VAR>s : α → Prop<GOAL>(¬∀ (x : α), s x) = ∃ x, ¬s x
<VAR>α : Sort u_1<VAR>s : α → Prop<GOAL>(¬∃ x, s x) = ∀ (x : α), ¬s x
<VAR>p q : Prop<GOAL>(¬(p → q)) = (p ∧ ¬q)
<VAR>α : Sort u_1<VAR>x y : α<GOAL>(¬x ≠ y) = (x = y)
<VAR>p q : Prop<GOAL>(¬(p ↔ q)) = (p ∧ ¬q ∨ ¬p ∧ q)
<VAR>β : Type u_2<VAR>LinearOrder β<VAR>a b : β<GOAL>(¬a ≤ b) = (b < a)
<VAR>β : Type u_2<VAR>LinearOrder β<VAR>a b : β<GOAL>(¬a < b) = (b ≤ a)
<VAR>β : Type u_2<VAR>LinearOrder β<VAR>a b : β<GOAL>(¬a ≥ b) = (a < b)
<VAR>β : Type u_2<VAR>LinearOrder β<VAR>a b : β<GOAL>(¬a > b) = (a ≤ b)
<VAR>β : Type u_2<VAR>s : Set β<GOAL>(¬s.Nonempty) = (s = ∅)
<VAR>β : Type u_2<VAR>s : Set β<GOAL>(s ≠ ∅) = s.Nonempty
<VAR>β : Type u_2<VAR>s : Set β<GOAL>(∅ ≠ s) = s.Nonempty
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>LinearOrderedField 𝕜<VAR>TopologicalSpace E<VAR>AddCommMonoid E<VAR>Module 𝕜 E<VAR>s : Set E<VAR>hs₀ : IsClosed s<VAR>hs₁ : StrictConvex 𝕜 s<GOAL>ThreeAPFree (frontier s)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>StrictConvexSpace ℝ E<VAR>x : E<VAR>r : ℝ<GOAL>ThreeAPFree (Metric.sphere x r)
<VAR>n d : ℕ<VAR>x : Fin n → ℕ<GOAL>x ∈ Behrend.box n d ↔ ∀ (i : Fin n), x i < d
<VAR>n d : ℕ<GOAL>(Behrend.box n d).card = d ^ n
<VAR>n : ℕ<GOAL>Behrend.box (n + 1) 0 = ∅
<VAR>n d : ℕ<GOAL>Behrend.sphere n d 0 ⊆ 0
<VAR>n k : ℕ<GOAL>Behrend.sphere (n + 1) 0 k = ∅
<VAR>n d k : ℕ<GOAL>Behrend.sphere n d k ⊆ Behrend.box n d
<VAR>n d k : ℕ<VAR>x : Fin n → ℕ<VAR>hx : x ∈ Behrend.sphere n d k<GOAL>‖(WithLp.equiv 2 (Fin n → ℝ)).symm (Nat.cast ∘ x)‖ = √↑k
<VAR>n d k : ℕ<GOAL>↑(Behrend.sphere n d k) ⊆ (fun x => (WithLp.equiv 2 (Fin n → ℝ)).symm (Nat.cast ∘ x)) ⁻¹' Metric.sphere 0 √↑k
<VAR>n : ℕ<VAR>d : ℕ<VAR>a : Fin n → ℕ<GOAL>(Behrend.map d) a = ∑ i : Fin n, a i * d ^ ↑i
<VAR>d : ℕ<VAR>a : Fin 0 → ℕ<GOAL>(Behrend.map d) a = 0
<VAR>n d : ℕ<VAR>a : Fin (n + 1) → ℕ<GOAL>(Behrend.map d) a = a 0 + (∑ x : Fin n, a x.succ * d ^ ↑x) * d
<VAR>n d : ℕ<VAR>a : Fin (n + 1) → ℕ<GOAL>(Behrend.map d) a = a 0 + (Behrend.map d) (a ∘ Fin.succ) * d
<VAR>n : ℕ<VAR>d : ℕ<GOAL>Monotone ⇑(Behrend.map d)
<VAR>n d : ℕ<VAR>a : Fin n.succ → ℕ<GOAL>(Behrend.map d) a % d = a 0 % d
<VAR>n d : ℕ<VAR>x₁ x₂ : Fin n.succ → ℕ<VAR>hx₁ : ∀ (i : Fin n.succ), x₁ i < d<VAR>hx₂ : ∀ (i : Fin n.succ), x₂ i < d<GOAL>(Behrend.map d) x₁ = (Behrend.map d) x₂ ↔ x₁ 0 = x₂ 0 ∧ (Behrend.map d) (x₁ ∘ Fin.succ) = (Behrend.map d) (x₂ ∘ Fin.succ)