ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹⁸ : CommSemiring R<VAR>inst✝¹⁷ : AddCommMonoid M₁<VAR>inst✝¹⁶ : Module R M₁<VAR>inst✝¹⁵ : AddCommMonoid M₂<VAR>inst✝¹⁴ : Module R M₂<VAR>inst✝¹³ : AddCommMonoid N₂<VAR>inst✝¹² : Module R N₂<VAR>inst✝¹¹ : DecidableEq n<VAR>inst✝¹⁰ : Fintype n<VAR>inst✝⁹ : DecidableEq m<VAR>inst✝⁸ : Fintype m<VAR>b₁✝ : Basis n R M₁<VAR>b₂✝ : Basis m R M₂<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>inst✝⁷ : AddCommMonoid M₁'<VAR>inst✝⁶ : Module R M₁'<VAR>inst✝⁵ : AddCommMonoid M₂'<VAR>inst✝⁴ : Module R M₂'<VAR>b₁' : Basis n' R M₁'<VAR>b₂' : Basis m' R M₂'<VAR>inst✝³ : Fintype n'<VAR>inst✝² : Fintype m'<VAR>inst✝¹ : DecidableEq n'<VAR>inst✝ : DecidableEq m'<VAR>B : M₁ →ₗ[R] M₂ →ₗ[R] R<VAR>l : M₁' →ₗ[R] M₁<VAR>r : M₂' →ₗ[R] M₂<VAR>i : n'<VAR>j : m'<GOAL>(B (l (b₁' i))) (r (b₂' j)) = ∑ y : n, ∑ x : m, (b₁.repr (l (b₁' i))) y * (B (b₁ y)) (b₂ x) * (b₂.repr (r (b₂' j))) x
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹⁸ : CommSemiring R<VAR>inst✝¹⁷ : AddCommMonoid M₁<VAR>inst✝¹⁶ : Module R M₁<VAR>inst✝¹⁵ : AddCommMonoid M₂<VAR>inst✝¹⁴ : Module R M₂<VAR>inst✝¹³ : AddCommMonoid N₂<VAR>inst✝¹² : Module R N₂<VAR>inst✝¹¹ : DecidableEq n<VAR>inst✝¹⁰ : Fintype n<VAR>inst✝⁹ : DecidableEq m<VAR>inst✝⁸ : Fintype m<VAR>b₁✝ : Basis n R M₁<VAR>b₂✝ : Basis m R M₂<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>inst✝⁷ : AddCommMonoid M₁'<VAR>inst✝⁶ : Module R M₁'<VAR>inst✝⁵ : AddCommMonoid M₂'<VAR>inst✝⁴ : Module R M₂'<VAR>b₁' : Basis n' R M₁'<VAR>b₂' : Basis m' R M₂'<VAR>inst✝³ : Fintype n'<VAR>inst✝² : Fintype m'<VAR>inst✝¹ : DecidableEq n'<VAR>inst✝ : DecidableEq m'<VAR>B : M₁ →ₗ[R] M₂ →ₗ[R] R<VAR>l : M₁' →ₗ[R] M₁<VAR>r : M₂' →ₗ[R] M₂<VAR>i : n'<VAR>j : m'<GOAL>((b₁.repr (l (b₁' i))).sum fun i xi => (b₂.repr (r (b₂' j))).sum fun j yj => xi •> yj •> (B (b₁ i)) (b₂ j)) = ∑ y : n, ∑ x : m, (b₁.repr (l (b₁' i))) y * (B (b₁ y)) (b₂ x) * (b₂.repr (r (b₂' j))) x
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹⁸ : CommSemiring R<VAR>inst✝¹⁷ : AddCommMonoid M₁<VAR>inst✝¹⁶ : Module R M₁<VAR>inst✝¹⁵ : AddCommMonoid M₂<VAR>inst✝¹⁴ : Module R M₂<VAR>inst✝¹³ : AddCommMonoid N₂<VAR>inst✝¹² : Module R N₂<VAR>inst✝¹¹ : DecidableEq n<VAR>inst✝¹⁰ : Fintype n<VAR>inst✝⁹ : DecidableEq m<VAR>inst✝⁸ : Fintype m<VAR>b₁✝ : Basis n R M₁<VAR>b₂✝ : Basis m R M₂<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>inst✝⁷ : AddCommMonoid M₁'<VAR>inst✝⁶ : Module R M₁'<VAR>inst✝⁵ : AddCommMonoid M₂'<VAR>inst✝⁴ : Module R M₂'<VAR>b₁' : Basis n' R M₁'<VAR>b₂' : Basis m' R M₂'<VAR>inst✝³ : Fintype n'<VAR>inst✝² : Fintype m'<VAR>inst✝¹ : DecidableEq n'<VAR>inst✝ : DecidableEq m'<VAR>B : M₁ →ₗ[R] M₂ →ₗ[R] R<VAR>l : M₁' →ₗ[R] M₁<VAR>r : M₂' →ₗ[R] M₂<VAR>i : n'<VAR>j : m'<GOAL>(∑ i_1 : n, (b₂.repr (r (b₂' j))).sum fun j yj => (b₁.repr (l (b₁' i))) i_1 •> yj •> (B (b₁ i_1)) (b₂ j)) = ∑ y : n, ∑ x : m, (b₁.repr (l (b₁' i))) y * (B (b₁ y)) (b₂ x) * (b₂.repr (r (b₂' j))) x
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹⁸ : CommSemiring R<VAR>inst✝¹⁷ : AddCommMonoid M₁<VAR>inst✝¹⁶ : Module R M₁<VAR>inst✝¹⁵ : AddCommMonoid M₂<VAR>inst✝¹⁴ : Module R M₂<VAR>inst✝¹³ : AddCommMonoid N₂<VAR>inst✝¹² : Module R N₂<VAR>inst✝¹¹ : DecidableEq n<VAR>inst✝¹⁰ : Fintype n<VAR>inst✝⁹ : DecidableEq m<VAR>inst✝⁸ : Fintype m<VAR>b₁✝ : Basis n R M₁<VAR>b₂✝ : Basis m R M₂<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>inst✝⁷ : AddCommMonoid M₁'<VAR>inst✝⁶ : Module R M₁'<VAR>inst✝⁵ : AddCommMonoid M₂'<VAR>inst✝⁴ : Module R M₂'<VAR>b₁' : Basis n' R M₁'<VAR>b₂' : Basis m' R M₂'<VAR>inst✝³ : Fintype n'<VAR>inst✝² : Fintype m'<VAR>inst✝¹ : DecidableEq n'<VAR>inst✝ : DecidableEq m'<VAR>B : M₁ →ₗ[R] M₂ →ₗ[R] R<VAR>l : M₁' →ₗ[R] M₁<VAR>r : M₂' →ₗ[R] M₂<VAR>i : n'<VAR>j : m'<GOAL>∀ (i : n), ((b₂.repr (r (b₂' j))).sum fun j yj => 0 •> yj •> (B (b₁ i)) (b₂ j)) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α<VAR>a✝ b : α<VAR>x y s t : Finset α<VAR>h : x ⊆ y<VAR>h' : s ⊆ t<VAR>a : α<VAR>a_in : a ∈ x ∩ s<GOAL>a ∈ y ∩ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α<VAR>a✝ b : α<VAR>x y s t : Finset α<VAR>h : x ⊆ y<VAR>h' : s ⊆ t<VAR>a : α<VAR>a_in : a ∈ x ∧ a ∈ s<GOAL>a ∈ y ∧ a ∈ t
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : BooleanAlgebra α<VAR>h : yᶜ ≤ x<GOAL>xᶜ ≤ y
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>inst✝ : Invertible 2<GOAL>dickson 1 1 0 = 2 * (Chebyshev.T R ↑0).comp (C ⅟2 * X)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>inst✝ : Invertible 2<GOAL>3 - ↑1 = 2 * (Chebyshev.T R ↑0).comp (C ⅟2 * X)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>inst✝ : Invertible 2<GOAL>dickson 1 1 1 = 2 * (Chebyshev.T R ↑1).comp (C ⅟2 * X)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>inst✝ : Invertible 2<VAR>n : ℕ<GOAL>dickson 1 1 (n + 2) = 2 * (Chebyshev.T R ↑(n + 2)).comp (C ⅟2 * X)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>inst✝ : Invertible 2<VAR>n : ℕ<GOAL>X * (2 * (Chebyshev.T R ↑(n + 1)).comp (C ⅟2 * X)) - 1 * (2 * (Chebyshev.T R ↑n).comp (C ⅟2 * X)) = 2 * (↑2 * (C ⅟2 * X) * (Chebyshev.T R (↑n + 1)).comp (C ⅟2 * X) - (Chebyshev.T R ↑n).comp (C ⅟2 * X))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>inst✝ : Invertible 2<VAR>n : ℕ<GOAL>X * 2 * (Chebyshev.T R (↑n + 1)).comp (C ⅟2 * X) - 1 * 2 * (Chebyshev.T R ↑n).comp (C ⅟2 * X) = 2 * (1 * X * (Chebyshev.T R (↑n + 1)).comp (C ⅟2 * X) - (Chebyshev.T R ↑n).comp (C ⅟2 * X))
<VAR>n m : ℕ<VAR>a b : Fin (n + 1)<VAR>ha : a ≠ 0<GOAL>b ≤ (a.pred ha).castSucc ↔ b < a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>Ioo a b ⊆ Ioc a b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>Set.Ioo a b ⊆ Set.Ioc a b
<VAR>α : Type u<VAR>β : Type v<VAR>S : WSeq (Computation α)<VAR>a : α<VAR>h : a ∈ parallel S<GOAL>∃ c, c ∈ S ∧ a ∈ c
<VAR>α : Type u<VAR>β : Type v<VAR>S : WSeq (Computation α)<VAR>a : α<VAR>h : a ∈ parallel S<GOAL>∀ (C : Computation α), a ∈ C → ∀ (l : List (Computation α)) (S : WSeq (Computation α)), corec parallel.aux1 (l, S) = C → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
<VAR>α : Type u<VAR>β : Type v<VAR>S : WSeq (Computation α)<VAR>a : α<VAR>h : a ∈ parallel S<VAR>F : List (Computation α) → α ⊕ List (Computation α) → Prop := fun l a => Sum.casesOn (motive := fun t => a = t → Prop) a (fun a_1 h => ∃ c, c ∈ l ∧ a_1 ∈ c) (fun l' h => ∀ (a' : α), (∃ c, c ∈ l' ∧ a' ∈ c) → ∃ c, c ∈ l ∧ a' ∈ c) ⋯<VAR>lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)<VAR>C : Computation α<VAR>aC : a ∈ C<GOAL>∀ (l : List (Computation α)) (S : WSeq (Computation α)), corec parallel.aux1 (l, S) = C → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
<VAR>α : Type u<VAR>β : Type v<VAR>S✝ : WSeq (Computation α)<VAR>a : α<VAR>h : a ∈ parallel S✝<VAR>F : List (Computation α) → α ⊕ List (Computation α) → Prop := fun l a => Sum.casesOn (motive := fun t => a = t → Prop) a (fun a_1 h => ∃ c, c ∈ l ∧ a_1 ∈ c) (fun l' h => ∀ (a' : α), (∃ c, c ∈ l' ∧ a' ∈ c) → ∃ c, c ∈ l ∧ a' ∈ c) ⋯<VAR>lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)<VAR>C : Computation α<VAR>aC : a ∈ C<VAR>l : List (Computation α)<VAR>S : WSeq (Computation α)<VAR>e : corec parallel.aux1 (l, S) = pure a<VAR>a' : α<VAR>this : F l (Sum.inl a')<VAR>h' : a' = a<GOAL>∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
<VAR>α : Type u<VAR>β : Type v<VAR>S✝ : WSeq (Computation α)<VAR>a : α<VAR>h : a ∈ parallel S✝<VAR>F : List (Computation α) → α ⊕ List (Computation α) → Prop := fun l a => Sum.casesOn (motive := fun t => a = t → Prop) a (fun a_1 h => ∃ c, c ∈ l ∧ a_1 ∈ c) (fun l' h => ∀ (a' : α), (∃ c, c ∈ l' ∧ a' ∈ c) → ∃ c, c ∈ l ∧ a' ∈ c) ⋯<VAR>lem1 : ∀ (l : List (Computation α)), F l (parallel.aux2 l)<VAR>C : Computation α<VAR>aC : a ∈ C<VAR>C' : Computation α<VAR>IH : ∀ (l : List (Computation α)) (S : WSeq (Computation α)), corec parallel.aux1 (l, S) = C' → ∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c<VAR>l : List (Computation α)<VAR>S : WSeq (Computation α)<VAR>e : corec parallel.aux1 (l, S) = C'.think<VAR>l' : List (Computation α)<VAR>this : F l (Sum.inr l')<VAR>h' : corec parallel.aux1 ((fun l' => match Seq.destruct S with | none => (l', Seq.nil) | some (none, S') => (l', S') | some (some c, S') => (c :: l', S')) l') = C'<GOAL>∃ c, (c ∈ l ∨ c ∈ S) ∧ a ∈ c
<VAR>θ : Angle<GOAL>-θ = θ ↔ θ = 0 ∨ θ = ↑π
<VAR>x : Cardinal.{v}<VAR>m : ℕ∞<GOAL>lift.{u, v} x = ↑m ↔ x = ↑m
<VAR>x : ℝ<GOAL>cos (arctan x) = 1 / √(1 + x ^ 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝ : DivisionRing K<VAR>a b c d : K<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>1 / a * (b - a) * (1 / b) = 1 / a - 1 / b
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>P : Fin 3 → R<GOAL>W.Nonsingular P ↔ W.Equation P ∧ (W.a₁ * P 1 * P 2 ≠ 3 * P 0 ^ 2 + 2 * W.a₂ * P 0 * P 2 + W.a₄ * P 2 ^ 2 ∨ P 1 * P 2 ≠ -P 1 * P 2 - W.a₁ * P 0 * P 2 - W.a₃ * P 2 ^ 2 ∨ P 1 ^ 2 + W.a₁ * P 0 * P 1 + 2 * W.a₃ * P 1 * P 2 ≠ W.a₂ * P 0 ^ 2 + 2 * W.a₄ * P 0 * P 2 + 3 * W.a₆ * P 2 ^ 2)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>P : Fin 3 → R<GOAL>W.Equation P ∧ (W.a₁ * P 1 * P 2 ≠ 3 * P 0 ^ 2 + 2 * W.a₂ * P 0 * P 2 + W.a₄ * P 2 ^ 2 ∨ 2 * P 1 * P 2 + W.a₁ * P 0 * P 2 + W.a₃ * P 2 ^ 2 ≠ 0 ∨ P 1 ^ 2 + W.a₁ * P 0 * P 1 + 2 * W.a₃ * P 1 * P 2 ≠ W.a₂ * P 0 ^ 2 + 2 * W.a₄ * P 0 * P 2 + 3 * W.a₆ * P 2 ^ 2) ↔ W.Equation P ∧ (W.a₁ * P 1 * P 2 ≠ 3 * P 0 ^ 2 + 2 * W.a₂ * P 0 * P 2 + W.a₄ * P 2 ^ 2 ∨ P 1 * P 2 - (-P 1 * P 2 - W.a₁ * P 0 * P 2 - W.a₃ * P 2 ^ 2) ≠ 0 ∨ P 1 ^ 2 + W.a₁ * P 0 * P 1 + 2 * W.a₃ * P 1 * P 2 ≠ W.a₂ * P 0 ^ 2 + 2 * W.a₄ * P 0 * P 2 + 3 * W.a₆ * P 2 ^ 2)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u_1<VAR>S' : Type u_2<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type ?u.236825<VAR>S'' : Type ?u.236828<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<VAR>f : P.Hom P'<VAR>v : P.vars →₀ ℕ<VAR>r : R<GOAL>f.toAlgHom ((monomial v) r) = r • v.prod fun x x_1 => f.val x ^ x_1
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddCommGroup (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+ G j<VAR>P : Type u₁<VAR>inst✝¹ : AddCommGroup P<VAR>g : (i : ι) → G i →+ P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>F : DirectLimit G f →+ P<VAR>x : DirectLimit G f<GOAL>F x = (lift G f P (fun i => F.comp (of G f i)) ⋯) x
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddCommGroup (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+ G j<VAR>P : Type u₁<VAR>inst✝¹ : AddCommGroup P<VAR>g : (i : ι) → G i →+ P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>F : DirectLimit G f →+ P<VAR>x : DirectLimit G f<VAR>h✝ : IsEmpty ι<GOAL>F x = (lift G f P (fun i => F.comp (of G f i)) ⋯) x
<VAR>R : Type u<VAR>inst✝⁵ : Ring R<VAR>ι : Type v<VAR>inst✝⁴ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddCommGroup (G i)<VAR>f : (i j : ι) → i ≤ j → G i →+ G j<VAR>P : Type u₁<VAR>inst✝¹ : AddCommGroup P<VAR>g : (i : ι) → G i →+ P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>F : DirectLimit G f →+ P<VAR>x : DirectLimit G f<VAR>h✝ : Nonempty ι<GOAL>F x = (lift G f P (fun i => F.comp (of G f i)) ⋯) x
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<GOAL>(W.map f).preΨ₄ = Polynomial.map f W.preΨ₄
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<GOAL>2 * X ^ 6 + C (f W.b₂) * X ^ 5 + 5 * C (f W.b₄) * X ^ 4 + 10 * C (f W.b₆) * X ^ 3 + 10 * C (f W.b₈) * X ^ 2 + C (f W.b₂ * f W.b₈ - f W.b₄ * f W.b₆) * X + C (f W.b₄ * f W.b₈ - f W.b₆ ^ 2) = Polynomial.map f (2 * X ^ 6 + C W.b₂ * X ^ 5 + 5 * C W.b₄ * X ^ 4 + 10 * C W.b₆ * X ^ 3 + 10 * C W.b₈ * X ^ 2 + C (W.b₂ * W.b₈ - W.b₄ * W.b₆) * X + C (W.b₄ * W.b₈ - W.b₆ ^ 2))
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁶ : CommRing P<VAR>inst✝⁵ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝⁴ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝¹ : IsDomain R₁<VAR>inst✝ : IsNoetherianRing R₁<VAR>I : FractionalIdeal R₁⁰ K<GOAL>IsNoetherian R₁ ↥↑I
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁶ : CommRing P<VAR>inst✝⁵ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝⁴ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝¹ : IsDomain R₁<VAR>inst✝ : IsNoetherianRing R₁<VAR>d : R₁<VAR>J : Ideal R₁<VAR>left✝ : d ≠ 0<GOAL>IsNoetherian R₁ ↥↑(spanSingleton R₁⁰ ((algebraMap R₁ K) d)⁻¹ * ↑J)
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁶ : CommRing P<VAR>inst✝⁵ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝⁴ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝¹ : IsDomain R₁<VAR>inst✝ : IsNoetherianRing R₁<VAR>d : R₁<VAR>J : Ideal R₁<VAR>left✝ : d ≠ 0<GOAL>IsNoetherian R₁ ↥↑↑J
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>M₀ : Type u_6<VAR>inst✝⁴ : MulZeroOneClass α<VAR>inst✝³ : MulZeroOneClass β<VAR>inst✝² : MulZeroOneClass γ<VAR>inst✝¹ : MulZeroOneClass δ<VAR>inst✝ : FunLike F α β<VAR>g : β →*₀ γ<VAR>f₁ f₂ : α →*₀ β<VAR>hg : Injective ⇑g<VAR>h : g.comp f₁ = g.comp f₂<VAR>x : α<GOAL>g (f₁ x) = g (f₂ x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>μ✝ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NoAtoms μ✝<VAR>h : s.Countable<VAR>μ : Measure α<VAR>inst✝ : NoAtoms μ<GOAL>∀ᵐ (x : α) ∂μ, x ∉ s
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁰ : Category.{u_4, u_1} C<VAR>inst✝⁹ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝⁸ : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝⁷ : G.IsCocontinuous J K<VAR>inst✝⁶ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>inst✝⁵ : G.IsCocontinuous J K<VAR>inst✝⁴ : G.IsContinuous J K<VAR>inst✝³ : HasWeakSheafify J A<VAR>inst✝² : HasWeakSheafify K A<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : G.IsContinuous J K<VAR>F : Dᵒᵖ ⥤ A<VAR>adj₁ : (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⊣ G.op.ran := G.op.ranAdjunction A<VAR>adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := sheafificationAdjunction J A<VAR>adj₃ : presheafToSheaf K A ⊣ sheafToPresheaf K A := sheafificationAdjunction K A<VAR>adj₄ : G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K := G.sheafAdjunctionCocontinuous A J K<GOAL>adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F) ≫ (sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F) = ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₃.unit.app F)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁰ : Category.{u_4, u_1} C<VAR>inst✝⁹ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝⁸ : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝⁷ : G.IsCocontinuous J K<VAR>inst✝⁶ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>inst✝⁵ : G.IsCocontinuous J K<VAR>inst✝⁴ : G.IsContinuous J K<VAR>inst✝³ : HasWeakSheafify J A<VAR>inst✝² : HasWeakSheafify K A<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : G.IsContinuous J K<VAR>F : Dᵒᵖ ⥤ A<VAR>adj₁ : (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⊣ G.op.ran := G.op.ranAdjunction A<VAR>adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := sheafificationAdjunction J A<VAR>adj₃ : presheafToSheaf K A ⊣ sheafToPresheaf K A := sheafificationAdjunction K A<VAR>adj₄ : G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K := G.sheafAdjunctionCocontinuous A J K<GOAL>(adj₁.homEquiv F ((sheafToPresheaf J A).obj ((presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K).obj F))) (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F) ≫ (sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F)) = (adj₁.homEquiv F ((sheafToPresheaf J A).obj ((presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K).obj F))) (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₃.unit.app F))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁰ : Category.{u_4, u_1} C<VAR>inst✝⁹ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝⁸ : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝⁷ : G.IsCocontinuous J K<VAR>inst✝⁶ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>inst✝⁵ : G.IsCocontinuous J K<VAR>inst✝⁴ : G.IsContinuous J K<VAR>inst✝³ : HasWeakSheafify J A<VAR>inst✝² : HasWeakSheafify K A<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : G.IsContinuous J K<VAR>F : Dᵒᵖ ⥤ A<VAR>adj₁ : (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⊣ G.op.ran := G.op.ranAdjunction A<VAR>adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := sheafificationAdjunction J A<VAR>adj₃ : presheafToSheaf K A ⊣ sheafToPresheaf K A := sheafificationAdjunction K A<VAR>adj₄ : G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K := G.sheafAdjunctionCocontinuous A J K<VAR>eq : (adj₁.comp adj₂).unit.app F ≫ (sheafToPresheaf J A ⋙ G.op.ran).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F) = (adj₃.comp adj₄).unit.app F<GOAL>(adj₁.homEquiv F ((sheafToPresheaf J A).obj ((presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K).obj F))) (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F) ≫ (sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F)) = (adj₁.homEquiv F ((sheafToPresheaf J A).obj ((presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K).obj F))) (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₃.unit.app F))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁰ : Category.{u_4, u_1} C<VAR>inst✝⁹ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝⁸ : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝⁷ : G.IsCocontinuous J K<VAR>inst✝⁶ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>inst✝⁵ : G.IsCocontinuous J K<VAR>inst✝⁴ : G.IsContinuous J K<VAR>inst✝³ : HasWeakSheafify J A<VAR>inst✝² : HasWeakSheafify K A<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : G.IsContinuous J K<VAR>F : Dᵒᵖ ⥤ A<VAR>adj₁ : (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⊣ G.op.ran := G.op.ranAdjunction A<VAR>adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := sheafificationAdjunction J A<VAR>adj₃ : presheafToSheaf K A ⊣ sheafToPresheaf K A := sheafificationAdjunction K A<VAR>adj₄ : G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K := G.sheafAdjunctionCocontinuous A J K<VAR>eq : adj₁.unit.app F ≫ G.op.ran.map (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F)) ≫ G.op.ran.map ((sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F)) = adj₃.unit.app F ≫ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F))<GOAL>(adj₁.homEquiv F ((sheafToPresheaf J A).obj ((presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K).obj F))) (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F) ≫ (sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F)) = (adj₁.homEquiv F ((sheafToPresheaf J A).obj ((presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K).obj F))) (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₃.unit.app F))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁰ : Category.{u_4, u_1} C<VAR>inst✝⁹ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝⁸ : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝⁷ : G.IsCocontinuous J K<VAR>inst✝⁶ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>inst✝⁵ : G.IsCocontinuous J K<VAR>inst✝⁴ : G.IsContinuous J K<VAR>inst✝³ : HasWeakSheafify J A<VAR>inst✝² : HasWeakSheafify K A<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : G.IsContinuous J K<VAR>F : Dᵒᵖ ⥤ A<VAR>adj₁ : (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⊣ G.op.ran := G.op.ranAdjunction A<VAR>adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := sheafificationAdjunction J A<VAR>adj₃ : presheafToSheaf K A ⊣ sheafToPresheaf K A := sheafificationAdjunction K A<VAR>adj₄ : G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K := G.sheafAdjunctionCocontinuous A J K<VAR>eq : adj₁.unit.app F ≫ G.op.ran.map (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F)) ≫ G.op.ran.map ((sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F)) = adj₃.unit.app F ≫ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F))<GOAL>adj₃.unit.app F ≫ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F)) = (adj₁.homEquiv F ((sheafToPresheaf J A).obj ((presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K).obj F))) (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₃.unit.app F))