ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>v w : V<VAR>s : Set (Sym2 V)<VAR>p : G.Walk v w<VAR>hp : ∀ e ∈ p.edges, e ∉ s<GOAL>∀ e ∈ (p.transfer (G.deleteEdges s) ⋯).edges, e ∈ G.edgeSet
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>v w : V<VAR>s : Set (Sym2 V)<VAR>p : G.Walk v w<VAR>hp : ∀ e ∈ p.edges, e ∉ s<VAR>e : Sym2 V<GOAL>e ∈ (p.transfer (G.deleteEdges s) ⋯).edges → e ∈ G.edgeSet
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>v w : V<VAR>s : Set (Sym2 V)<VAR>p : G.Walk v w<VAR>hp : ∀ e ∈ p.edges, e ∉ s<VAR>e : Sym2 V<GOAL>e ∈ p.edges → e ∈ G.edgeSet
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : LinearOrderedCommGroupWithZero Γ₀<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ'₀<VAR>v : Valuation K Γ₀<VAR>v' : Valuation K Γ'₀<VAR>h : ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1<VAR>x y : K<VAR>hy : ¬y = 0<GOAL>v x ≤ v y ↔ v' x ≤ v' y
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : LinearOrderedCommGroupWithZero Γ₀<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ'₀<VAR>v : Valuation K Γ₀<VAR>v' : Valuation K Γ'₀<VAR>h : ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1<VAR>x y : K<VAR>hy : ¬y = 0<GOAL>v x ≤ v (1 * y) ↔ v' x ≤ v' (1 * y)
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : LinearOrderedCommGroupWithZero Γ₀<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ'₀<VAR>v : Valuation K Γ₀<VAR>v' : Valuation K Γ'₀<VAR>h : ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1<VAR>x y : K<VAR>hy : ¬y = 0<GOAL>v (x * y⁻¹ * y) ≤ v (1 * y) ↔ v' (x * y⁻¹ * y) ≤ v' (1 * y)
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : LinearOrderedCommGroupWithZero Γ₀<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ'₀<VAR>v : Valuation K Γ₀<VAR>v' : Valuation K Γ'₀<VAR>h : ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1<VAR>x y : K<VAR>hy : ¬y = 0<GOAL>v (x * y⁻¹) * v y ≤ v 1 * v y ↔ v' (x * y⁻¹) * v' y ≤ v' 1 * v' y
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : LinearOrderedCommGroupWithZero Γ₀<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ'₀<VAR>v : Valuation K Γ₀<VAR>v' : Valuation K Γ'₀<VAR>h : ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1<VAR>x y : K<VAR>hy : ¬y = 0<GOAL>v (x * y⁻¹) * v y ≤ 1 * v y ↔ v' (x * y⁻¹) * v' y ≤ 1 * v' y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<GOAL>Exact ⇑(rTensor Q f) ⇑(rTensor Q g)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<GOAL>ker (rTensor Q g) = ker (rTensor.inverse Q hfg hg ∘ₗ rTensor Q g)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<GOAL>ker (rTensor.inverse Q hfg hg ∘ₗ rTensor Q g) = ker (rTensor Q g)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<GOAL>ker (rTensor.inverse Q hfg hg) = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : AddCommGroup P<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<GOAL>Injective ⇑(rTensor.inverse Q hfg hg)
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommRing R<VAR>M✝ : Type u_2<VAR>inst✝¹⁰ : AddCommGroup M✝<VAR>inst✝⁹ : Module R M✝<VAR>M'✝ : Type u_3<VAR>inst✝⁸ : AddCommGroup M'✝<VAR>inst✝⁷ : Module R M'✝<VAR>ι : Type u_4<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : Fintype ι<VAR>e : Basis ι R M✝<VAR>A : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>m : Type u_6<VAR>n : Type u_7<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : DecidableEq n<VAR>M : Matrix m n A<VAR>M' : Matrix n m A<VAR>N : Matrix n n A<VAR>hMM' : M * M' = 1<VAR>hM'M : M' * M = 1<GOAL>(M * N * M').det = N.det
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIocDiv hp (p + a) b = toIocDiv hp a b - 1
<VAR>c : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ c<GOAL>c + c ≤ c
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>α : Type u_5<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : Nontrivial E<GOAL>(cobounded E).NeBot
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>α : Type u_5<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : Nontrivial E<GOAL>¬Bornology.IsBounded univ
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>p : α × Bool<VAR>LL₁ : List (α × Bool)<VAR>eq₁ : p :: L₁ = LL₁<VAR>LL₂ : List (α × Bool)<VAR>eq₂ : p :: L₂ = LL₂<VAR>h : Red LL₁ LL₂<GOAL>Red L₁ L₂
<VAR>α : Type u<VAR>L L₃ L₄ : List (α × Bool)<VAR>p : α × Bool<VAR>LL₁ LL₂ L₁ L₂ : List (α × Bool)<VAR>eq₁ : p :: L₁ = LL₂<VAR>eq₂ : p :: L₂ = LL₂<GOAL>Red L₁ L₂
<VAR>α : Type u<VAR>L L₃ L₄ : List (α × Bool)<VAR>p : α × Bool<VAR>LL₁ LL₂ L₁✝ L₂✝ : List (α × Bool)<VAR>h₁₂ : Step L₁✝ L₂✝<VAR>h : ReflTransGen Step L₂✝ LL₂<VAR>ih : ∀ {L₁ L₂ : List (α × Bool)}, p :: L₁ = L₂✝ → p :: L₂ = LL₂ → Red L₁ L₂<VAR>L₁ L₂ : List (α × Bool)<VAR>eq₁ : p :: L₁ = L₁✝<VAR>eq₂ : p :: L₂ = LL₂<GOAL>Red L₁ L₂
<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>ι : Sort u_5<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>hf : f.HasBasis p s<VAR>hh : Monotone h<VAR>t : Set β<GOAL>(∃ i, p i ∧ ∃ x, True ∧ h (s i) ⊆ t) ↔ ∃ i, p i ∧ (h ∘ s) i ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>ε K₁ K₂ : α<VAR>ε0 : 0 < ε<GOAL>∃ δ > 0, ∀ {a₁ a₂ b₁ b₂ : β}, abv a₁ < K₁ → abv b₂ < K₂ → abv (a₁ - b₁) < δ → abv (a₂ - b₂) < δ → abv (a₁ * a₂ - b₁ * b₂) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>ε K₁ K₂ : α<VAR>ε0 : 0 < ε<VAR>K0 : 0 < max 1 (max K₁ K₂)<GOAL>∃ δ > 0, ∀ {a₁ a₂ b₁ b₂ : β}, abv a₁ < K₁ → abv b₂ < K₂ → abv (a₁ - b₁) < δ → abv (a₂ - b₂) < δ → abv (a₁ * a₂ - b₁ * b₂) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>ε K₁ K₂ : α<VAR>ε0 : 0 < ε<VAR>K0 : 0 < max 1 (max K₁ K₂)<VAR>εK : 0 < ε / 2 / max 1 (max K₁ K₂)<GOAL>∃ δ > 0, ∀ {a₁ a₂ b₁ b₂ : β}, abv a₁ < K₁ → abv b₂ < K₂ → abv (a₁ - b₁) < δ → abv (a₂ - b₂) < δ → abv (a₁ * a₂ - b₁ * b₂) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>ε K₁ K₂ : α<VAR>ε0 : 0 < ε<VAR>K0 : 0 < max 1 (max K₁ K₂)<VAR>εK : 0 < ε / 2 / max 1 (max K₁ K₂)<VAR>a₁ a₂ b₁ b₂ : β<VAR>ha₁ : abv a₁ < K₁<VAR>hb₂ : abv b₂ < K₂<VAR>h₁ : abv (a₁ - b₁) < ε / 2 / max 1 (max K₁ K₂)<VAR>h₂ : abv (a₂ - b₂) < ε / 2 / max 1 (max K₁ K₂)<GOAL>abv (a₁ * a₂ - b₁ * b₂) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>ε K₁ K₂ : α<VAR>ε0 : 0 < ε<VAR>K0 : 0 < max 1 (max K₁ K₂)<VAR>εK : 0 < ε / 2 / max 1 (max K₁ K₂)<VAR>a₁ a₂ b₁ b₂ : β<VAR>hb₂ : abv b₂ < K₂<VAR>h₁ : abv (a₁ - b₁) < ε / 2 / max 1 (max K₁ K₂)<VAR>h₂ : abv (a₂ - b₂) < ε / 2 / max 1 (max K₁ K₂)<VAR>ha₁ : abv a₁ < max 1 (max K₁ K₂)<GOAL>abv (a₁ * a₂ - b₁ * b₂) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>ε K₁ K₂ : α<VAR>ε0 : 0 < ε<VAR>K0 : 0 < max 1 (max K₁ K₂)<VAR>εK : 0 < ε / 2 / max 1 (max K₁ K₂)<VAR>a₁ a₂ b₁ b₂ : β<VAR>h₁ : abv (a₁ - b₁) < ε / 2 / max 1 (max K₁ K₂)<VAR>h₂ : abv (a₂ - b₂) < ε / 2 / max 1 (max K₁ K₂)<VAR>ha₁ : abv a₁ < max 1 (max K₁ K₂)<VAR>hb₂ : abv b₂ < max 1 (max K₁ K₂)<GOAL>abv (a₁ * a₂ - b₁ * b₂) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>ε K₁ K₂ : α<VAR>ε0 : 0 < ε<VAR>a₁ a₂ b₁ b₂ : β<VAR>M : α := max 1 (max K₁ K₂)<VAR>K0 : 0 < M<VAR>εK : 0 < ε / 2 / M<VAR>h₁ : abv (a₁ - b₁) < ε / 2 / M<VAR>h₂ : abv (a₂ - b₂) < ε / 2 / M<VAR>ha₁ : abv a₁ < M<VAR>hb₂ : abv b₂ < M<VAR>this : abv (a₁ - b₁) * abv b₂ + abv (a₂ - b₂) * abv a₁ < ε / 2 / M * M + ε / 2 / M * M<GOAL>abv (a₁ * a₂ - b₁ * b₂) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>ε K₁ K₂ : α<VAR>ε0 : 0 < ε<VAR>a₁ a₂ b₁ b₂ : β<VAR>M : α := max 1 (max K₁ K₂)<VAR>K0 : 0 < M<VAR>εK : 0 < ε / 2 / M<VAR>h₁ : abv (a₁ - b₁) < ε / 2 / M<VAR>h₂ : abv (a₂ - b₂) < ε / 2 / M<VAR>ha₁ : abv a₁ < M<VAR>hb₂ : abv b₂ < M<VAR>this : abv ((a₁ - b₁) * b₂) + abv (a₁ * (a₂ - b₂)) < ε<GOAL>abv (a₁ * a₂ - b₁ * b₂) < ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : LinearOrderedCommRing 𝕜<VAR>inst✝⁹ : LinearOrderedCommRing E<VAR>inst✝⁸ : LinearOrderedAddCommGroup F<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜 F<VAR>inst✝⁵ : Module E F<VAR>inst✝⁴ : IsScalarTower 𝕜 E F<VAR>inst✝³ : SMulCommClass 𝕜 E F<VAR>inst✝² : OrderedSMul 𝕜 E<VAR>inst✝¹ : OrderedSMul 𝕜 F<VAR>inst✝ : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConcaveOn 𝕜 s f<VAR>hg : ConvexOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g x ≤ 0<VAR>hfg : MonovaryOn f g s<GOAL>ConvexOn 𝕜 s (f • g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : LinearOrderedCommRing 𝕜<VAR>inst✝⁹ : LinearOrderedCommRing E<VAR>inst✝⁸ : LinearOrderedAddCommGroup F<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜 F<VAR>inst✝⁵ : Module E F<VAR>inst✝⁴ : IsScalarTower 𝕜 E F<VAR>inst✝³ : SMulCommClass 𝕜 E F<VAR>inst✝² : OrderedSMul 𝕜 E<VAR>inst✝¹ : OrderedSMul 𝕜 F<VAR>inst✝ : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConcaveOn 𝕜 s f<VAR>hg : ConvexOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g x ≤ 0<VAR>hfg : MonovaryOn f g s<GOAL>ConcaveOn 𝕜 s (f • -g)
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<VAR>inst✝ : Finite γ<VAR>f : α → β ⊕ γ<VAR>φ : L.Formula α<VAR>v : β → M<GOAL>(Formula.iAlls f φ).Realize v ↔ ∀ (i : γ → M), φ.Realize fun a => Sum.elim v i (f a)
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<VAR>inst✝ : Finite γ<VAR>f : α → β ⊕ γ<VAR>φ : L.Formula α<VAR>v : β → M<VAR>e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯<GOAL>(Formula.iAlls f φ).Realize v ↔ ∀ (i : γ → M), φ.Realize fun a => Sum.elim v i (f a)
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<VAR>inst✝ : Finite γ<VAR>f : α → β ⊕ γ<VAR>φ : L.Formula α<VAR>v : β → M<VAR>e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯<GOAL>(let e := Classical.choice ⋯; (relabel (fun a => Sum.map id (⇑e) (f a)) φ).alls).Realize v ↔ ∀ (i : γ → M), φ.Realize fun a => Sum.elim v i (f a)
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<VAR>inst✝ : Finite γ<VAR>f : α → β ⊕ γ<VAR>φ : L.Formula α<VAR>v : β → M<VAR>e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯<GOAL>(∀ (xs : Fin (Classical.choose ⋯) → M), Realize φ (fun x => Sum.elim (fun x => v x) (fun x => xs (Fin.cast ⋯ ((Classical.choice ⋯) x))) (f x)) fun x => xs (natAdd (Classical.choose ⋯) x)) ↔ ∀ (i : γ → M), φ.Realize fun a => Sum.elim v i (f a)
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<VAR>inst✝ : Finite γ<VAR>f : α → β ⊕ γ<VAR>φ : L.Formula α<VAR>v : β → M<VAR>e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯<GOAL>(Fin (Classical.choose ⋯) → M) ≃ (γ → M)
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<VAR>inst✝ : Finite γ<VAR>f : α → β ⊕ γ<VAR>φ : L.Formula α<VAR>v : β → M<VAR>e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯<GOAL>∀ (a : Fin (Classical.choose ⋯) → M), (Realize φ (fun x => Sum.elim (fun x => v x) (fun x => a (Fin.cast ⋯ ((Classical.choice ⋯) x))) (f x)) fun x => a (natAdd (Classical.choose ⋯) x)) ↔ φ.Realize fun a_1 => Sum.elim v (?refine_1 a) (f a_1)
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝⁴ : Category.{v, u} V<VAR>inst✝³ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g✝ : C ⟶ D<VAR>h✝ k : D ⟶ E<VAR>i✝ : ι<VAR>W : Type u_2<VAR>inst✝² : Category.{?u.284404, u_2} W<VAR>inst✝¹ : Preadditive W<VAR>F : V ⥤ W<VAR>inst✝ : F.Additive<VAR>f g : C ⟶ D<VAR>h : Homotopy f g<VAR>i j : ι<VAR>w : ¬c.Rel j i<GOAL>F.map (h.hom i j) = 0
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝⁴ : Category.{v, u} V<VAR>inst✝³ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g✝ : C ⟶ D<VAR>h✝ k : D ⟶ E<VAR>i✝ : ι<VAR>W : Type u_2<VAR>inst✝² : Category.{?u.284404, u_2} W<VAR>inst✝¹ : Preadditive W<VAR>F : V ⥤ W<VAR>inst✝ : F.Additive<VAR>f g : C ⟶ D<VAR>h : Homotopy f g<VAR>i : ι<GOAL>((F.mapHomologicalComplex c).map f).f i = (((dNext i) fun i j => F.map (h.hom i j)) + (prevD i) fun i j => F.map (h.hom i j)) + ((F.mapHomologicalComplex c).map g).f i
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝⁴ : Category.{v, u} V<VAR>inst✝³ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f✝ g✝ : C ⟶ D<VAR>h✝ k : D ⟶ E<VAR>i✝ : ι<VAR>W : Type u_2<VAR>inst✝² : Category.{?u.284404, u_2} W<VAR>inst✝¹ : Preadditive W<VAR>F : V ⥤ W<VAR>inst✝ : F.Additive<VAR>f g : C ⟶ D<VAR>h : Homotopy f g<VAR>i : ι<VAR>H : f.f i = (dNext i) h.hom + (prevD i) h.hom + g.f i<GOAL>((F.mapHomologicalComplex c).map f).f i = (((dNext i) fun i j => F.map (h.hom i j)) + (prevD i) fun i j => F.map (h.hom i j)) + ((F.mapHomologicalComplex c).map g).f i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * re ⟪x, y⟫_𝕜 + ‖y‖ ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<GOAL>Disjoint (s₁ ×ˢ t₁) (s₂ ×ˢ t₂) ↔ Disjoint s₁ s₂ ∨ Disjoint t₁ t₂
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>inst✝ : Monoid M<VAR>a✝ b c : M<VAR>m✝ n : ℕ<VAR>a : M<VAR>m : ℕ<GOAL>a ^ (m + 0) = a ^ m * a ^ 0
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>inst✝ : Monoid M<VAR>a✝ b c : M<VAR>m✝ n✝ : ℕ<VAR>a : M<VAR>m n : ℕ<GOAL>a ^ (m + (n + 1)) = a ^ m * a ^ (n + 1)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasProjectiveResolutions C<VAR>inst✝ : EnoughProjectives C<VAR>Z : C<GOAL>(ofComplex Z).d 1 0 ≫ Projective.π Z = 0
<VAR>K : Type ?u.601713<VAR>L : Type ?u.601716<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>p q : K[X]<VAR>hp : p ≠ 0<VAR>h_eq : p = q<GOAL>(aeval (root q)) p = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s t : WSeq α<VAR>h : s ~ʷ t<GOAL>s.tail ~ʷ t.tail
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s t : WSeq α<VAR>h : s ~ʷ t<GOAL>Computation.LiftRel Equiv ((fun o => Option.recOn o nil Prod.snd) <$> s.destruct) ((fun o => Option.recOn o nil Prod.snd) <$> t.destruct)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s t : WSeq α<VAR>h : s ~ʷ t<GOAL>Computation.LiftRel Equiv (Computation.map (fun o => Option.rec nil Prod.snd o) s.destruct) (Computation.map (fun o => Option.rec nil Prod.snd o) t.destruct)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s t : WSeq α<VAR>h : s ~ʷ t<GOAL>Computation.LiftRel Equiv (s.destruct.bind (Computation.pure ∘ fun o => Option.rec nil Prod.snd o)) (t.destruct.bind (Computation.pure ∘ fun o => Option.rec nil Prod.snd o))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s t : WSeq α<VAR>h : s ~ʷ t<GOAL>∀ {a b : Option (α × WSeq α)}, BisimO (fun x x_1 => x ~ʷ x_1) a b → Computation.LiftRel Equiv ((Computation.pure ∘ fun o => Option.rec nil Prod.snd o) a) ((Computation.pure ∘ fun o => Option.rec nil Prod.snd o) b)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s t : WSeq α<VAR>h✝ : s ~ʷ t<VAR>a b : Option (α × WSeq α)<VAR>h : BisimO (fun x x_1 => x ~ʷ x_1) a b<GOAL>Computation.LiftRel Equiv ((Computation.pure ∘ fun o => Option.rec nil Prod.snd o) a) ((Computation.pure ∘ fun o => Option.rec nil Prod.snd o) b)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s t : WSeq α<VAR>h✝ : s ~ʷ t<VAR>a b : Option (α × WSeq α)<VAR>h : BisimO (fun x x_1 => x ~ʷ x_1) a b<GOAL>Option.rec nil Prod.snd a ~ʷ Option.rec nil Prod.snd b
<VAR>a b : ℝ<VAR>n k : ℕ<VAR>ih : ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) = π * ∏ i ∈ Finset.range k, (2 * ↑i + 1) / (2 * ↑i + 2)<GOAL>∫ (x : ℝ) in 0 ..π, sin x ^ (2 * (k + 1)) = π * ∏ i ∈ Finset.range (k + 1), (2 * ↑i + 1) / (2 * ↑i + 2)
<VAR>a b : ℝ<VAR>n k : ℕ<VAR>ih : ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) = π * ∏ i ∈ Finset.range k, (2 * ↑i + 1) / (2 * ↑i + 2)<GOAL>(sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / (↑(2 * k) + 2) + (↑(2 * k) + 1) / (↑(2 * k) + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) = (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
<VAR>a b : ℝ<VAR>n k : ℕ<VAR>ih : ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) = π * ∏ i ∈ Finset.range k, (2 * ↑i + 1) / (2 * ↑i + 2)<GOAL>(sin 0 ^ (2 * k + 1) * cos 0 - sin π ^ (2 * k + 1) * cos π) / ↑(2 * k + 2) + ↑(2 * k + 1) / ↑(2 * k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k) = ↑(2 * k + 1) / ↑(2 * k + 2) * ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>s t : Finset α<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>ha : a ∉ s<GOAL>insert a (insert a s)ᶜ = sᶜ
<VAR>X Y S : Type v<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>c : PullbackCone f g<VAR>hc : IsLimit c<VAR>x : Types.PullbackObj f g<GOAL>c.fst ((equivPullbackObj hc).symm x) = (↑x).1
<VAR>X Y S : Type v<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>c : PullbackCone f g<VAR>hc : IsLimit c<VAR>x : c.pt<GOAL>c.fst ((equivPullbackObj hc).symm ((equivPullbackObj hc) x)) = (↑((equivPullbackObj hc) x)).1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>ga : α → α → α<VAR>gb : β → β → β<VAR>f' : β → γ<VAR>gc : γ → γ → γ<VAR>hf' : Semiconj₂ f' gb gc<VAR>hf : Semiconj₂ f ga gb<VAR>x y : α<GOAL>(f' ∘ f) (ga x y) = gc ((f' ∘ f) x) ((f' ∘ f) y)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : σ → τ<VAR>p : ℕ<VAR>φ : σ<GOAL>((rename f).comp (expand p)) (X φ) = ((expand p).comp (rename f)) (X φ)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<GOAL>GaloisConnection (fun s => zeroLocus s) fun t => ↑(vanishingIdeal t)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>ideal_gc : GaloisConnection Ideal.span SetLike.coe<GOAL>GaloisConnection (fun s => zeroLocus s) fun t => ↑(vanishingIdeal t)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>κ : ι → Sort u_3<VAR>inst✝ : PartialOrder α<VAR>c : ClosureOperator α<VAR>x y : α<VAR>hy : c.IsClosed y<GOAL>c x ≤ y ↔ x ≤ y
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>f : α → β<VAR>inst✝ : Zero β<VAR>hs : MeasurableSet s<GOAL>s.indicator f =ᶠ[ae (μ.restrict s)] f
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>inst✝⁶ : Preadditive C<VAR>R : Type u_1<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive D<VAR>z z' : Cochain K L n<VAR>f : K ⟶ L<VAR>Φ✝ : C ⥤ D<VAR>inst✝¹ : Φ✝.Additive<VAR>n₁ n₂ n₁₂ : ℤ<VAR>z₁ : Cochain F G n₁<VAR>z₂ : Cochain G K n₂<VAR>h : n₁ + n₂ = n₁₂<VAR>Φ : C ⥤ D<VAR>inst✝ : Φ.Additive<VAR>p q : ℤ<VAR>hpq : p + n₁₂ = q<GOAL>Φ.map ((z₁.comp z₂ h).v p q hpq) = ((z₁.map Φ).comp (z₂.map Φ) h).v p q hpq
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : Group G'<VAR>inst✝⁴ : Group G''<VAR>A : Type u_4<VAR>inst✝³ : AddGroup A<VAR>G₁ : Type u_5<VAR>G₂ : Type u_6<VAR>G₃ : Type u_7<VAR>inst✝² : Group G₁<VAR>inst✝¹ : Group G₂<VAR>inst✝ : Group G₃<VAR>f : G₁ →* G₂<VAR>f_inv : G₂ → G₁<VAR>hf : Function.RightInverse f_inv ⇑f<VAR>g : G₁ →* G₃<VAR>hg : f.ker ≤ g.ker<VAR>x : G₁<GOAL>g (f_inv (f x)) = g x
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : Group G'<VAR>inst✝⁴ : Group G''<VAR>A : Type u_4<VAR>inst✝³ : AddGroup A<VAR>G₁ : Type u_5<VAR>G₂ : Type u_6<VAR>G₃ : Type u_7<VAR>inst✝² : Group G₁<VAR>inst✝¹ : Group G₂<VAR>inst✝ : Group G₃<VAR>f : G₁ →* G₂<VAR>f_inv : G₂ → G₁<VAR>hf : Function.RightInverse f_inv ⇑f<VAR>g : G₁ →* G₃<VAR>hg : f.ker ≤ g.ker<VAR>x : G₁<GOAL>f_inv (f x) * x⁻¹ ∈ g.ker
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : Group G'<VAR>inst✝⁴ : Group G''<VAR>A : Type u_4<VAR>inst✝³ : AddGroup A<VAR>G₁ : Type u_5<VAR>G₂ : Type u_6<VAR>G₃ : Type u_7<VAR>inst✝² : Group G₁<VAR>inst✝¹ : Group G₂<VAR>inst✝ : Group G₃<VAR>f : G₁ →* G₂<VAR>f_inv : G₂ → G₁<VAR>hf : Function.RightInverse f_inv ⇑f<VAR>g : G₁ →* G₃<VAR>hg : f.ker ≤ g.ker<VAR>x : G₁<GOAL>f_inv (f x) * x⁻¹ ∈ f.ker