ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p : ℕ<VAR>R S : Type u<VAR>σ : Type u_1<VAR>idx : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R<VAR>h : ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ), (ghostComponent n) (f x) = (ghostComponent n) (g x)<VAR>φ : ℕ → MvPolynomial ℕ ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => (aeval x.coeff) (φ n)<VAR>ψ : ℕ → MvPolynomial ℕ ℤ<VAR>hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => (aeval x.coeff) (ψ n)<VAR>R✝ : Type u<VAR>_Rcr✝ : CommRing R✝<VAR>x✝ : 𝕎 R✝<VAR>n k : ℕ<VAR>x : ℕ → ℤ<GOAL>(MvPolynomial.eval x) ((bind₁ φ) (wittPolynomial p ℤ k)) = (MvPolynomial.eval x) ((bind₁ ψ) (wittPolynomial p ℤ k))
<VAR>p : ℕ<VAR>R S : Type u<VAR>σ : Type u_1<VAR>idx : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R<VAR>h : ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ), (ghostComponent n) (f x) = (ghostComponent n) (g x)<VAR>φ : ℕ → MvPolynomial ℕ ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => (aeval x.coeff) (φ n)<VAR>ψ : ℕ → MvPolynomial ℕ ℤ<VAR>hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => (aeval x.coeff) (ψ n)<VAR>R✝ : Type u<VAR>_Rcr✝ : CommRing R✝<VAR>x✝ : 𝕎 R✝<VAR>n k : ℕ<VAR>x : ℕ → ℤ<GOAL>(eval₂Hom ((MvPolynomial.eval x).comp C) fun i => (MvPolynomial.eval x) (φ i)) (wittPolynomial p ℤ k) = (eval₂Hom ((MvPolynomial.eval x).comp C) fun i => (MvPolynomial.eval x) (ψ i)) (wittPolynomial p ℤ k)
<VAR>p : ℕ<VAR>R S : Type u<VAR>σ : Type u_1<VAR>idx : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R<VAR>φ : ℕ → MvPolynomial ℕ ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => (aeval x.coeff) (φ n)<VAR>ψ : ℕ → MvPolynomial ℕ ℤ<VAR>hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => (aeval x.coeff) (ψ n)<VAR>R✝ : Type u<VAR>_Rcr✝ : CommRing R✝<VAR>x✝ : 𝕎 R✝<VAR>n k : ℕ<VAR>x : ℕ → ℤ<VAR>h : (ghostComponent k) (f (mk p fun i => { down := x i })) = (ghostComponent k) (g (mk p fun i => { down := x i }))<GOAL>(eval₂Hom ((MvPolynomial.eval x).comp C) fun i => (MvPolynomial.eval x) (φ i)) (wittPolynomial p ℤ k) = (eval₂Hom ((MvPolynomial.eval x).comp C) fun i => (MvPolynomial.eval x) (ψ i)) (wittPolynomial p ℤ k)
<VAR>p : ℕ<VAR>R S : Type u<VAR>σ : Type u_1<VAR>idx : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R<VAR>φ : ℕ → MvPolynomial ℕ ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => (aeval x.coeff) (φ n)<VAR>ψ : ℕ → MvPolynomial ℕ ℤ<VAR>hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => (aeval x.coeff) (ψ n)<VAR>R✝ : Type u<VAR>_Rcr✝ : CommRing R✝<VAR>x✝ : 𝕎 R✝<VAR>n k : ℕ<VAR>x : ℕ → ℤ<VAR>h : (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (f (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k) = (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (g (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k)<GOAL>(eval₂Hom ((MvPolynomial.eval x).comp C) fun i => (MvPolynomial.eval x) (φ i)) (wittPolynomial p ℤ k) = (eval₂Hom ((MvPolynomial.eval x).comp C) fun i => (MvPolynomial.eval x) (ψ i)) (wittPolynomial p ℤ k)
<VAR>p : ℕ<VAR>R S : Type u<VAR>σ : Type u_1<VAR>idx : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R<VAR>φ : ℕ → MvPolynomial ℕ ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => (aeval x.coeff) (φ n)<VAR>ψ : ℕ → MvPolynomial ℕ ℤ<VAR>hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => (aeval x.coeff) (ψ n)<VAR>R✝ : Type u<VAR>_Rcr✝ : CommRing R✝<VAR>x✝ : 𝕎 R✝<VAR>n k : ℕ<VAR>x : ℕ → ℤ<VAR>h : (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (f (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k) = (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (g (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k)<GOAL>ULift.ringEquiv.symm ((eval₂Hom ((MvPolynomial.eval x).comp C) fun i => (MvPolynomial.eval x) (φ i)) (wittPolynomial p ℤ k)) = ULift.ringEquiv.symm ((eval₂Hom ((MvPolynomial.eval x).comp C) fun i => (MvPolynomial.eval x) (ψ i)) (wittPolynomial p ℤ k))
<VAR>p : ℕ<VAR>R S : Type u<VAR>σ : Type u_1<VAR>idx : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R<VAR>φ : ℕ → MvPolynomial ℕ ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => (aeval x.coeff) (φ n)<VAR>ψ : ℕ → MvPolynomial ℕ ℤ<VAR>hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => (aeval x.coeff) (ψ n)<VAR>R✝ : Type u<VAR>_Rcr✝ : CommRing R✝<VAR>x✝ : 𝕎 R✝<VAR>n k : ℕ<VAR>x : ℕ → ℤ<VAR>h : (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (f (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k) = (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (g (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k)<GOAL>(eval₂Hom ((↑ULift.ringEquiv.symm).comp ((MvPolynomial.eval x).comp C)) fun i => ↑ULift.ringEquiv.symm ((MvPolynomial.eval x) (φ i))) (wittPolynomial p ℤ k) = (eval₂Hom ((↑ULift.ringEquiv.symm).comp ((MvPolynomial.eval x).comp C)) fun i => ↑ULift.ringEquiv.symm ((MvPolynomial.eval x) (ψ i))) (wittPolynomial p ℤ k)
<VAR>p : ℕ<VAR>R S : Type u<VAR>σ : Type u_1<VAR>idx : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R<VAR>φ : ℕ → MvPolynomial ℕ ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => (aeval x.coeff) (φ n)<VAR>ψ : ℕ → MvPolynomial ℕ ℤ<VAR>hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => (aeval x.coeff) (ψ n)<VAR>R✝ : Type u<VAR>_Rcr✝ : CommRing R✝<VAR>x✝ : 𝕎 R✝<VAR>n k : ℕ<VAR>x : ℕ → ℤ<VAR>h : (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (f (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k) = (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (g (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k)<GOAL>(eval₂Hom ((↑ULift.ringEquiv.symm).comp ((MvPolynomial.eval x).comp C)) fun i => ↑ULift.ringEquiv.symm ((MvPolynomial.eval x) (φ i))) (wittPolynomial p ℤ k) = (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (f (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k)
<VAR>p : ℕ<VAR>R S : Type u<VAR>σ : Type u_1<VAR>idx : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f g : ⦃R : Type u⦄ → [inst : CommRing R] → 𝕎 R → 𝕎 R<VAR>φ : ℕ → MvPolynomial ℕ ℤ<VAR>hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n => (aeval x.coeff) (φ n)<VAR>ψ : ℕ → MvPolynomial ℕ ℤ<VAR>hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n => (aeval x.coeff) (ψ n)<VAR>R✝ : Type u<VAR>_Rcr✝ : CommRing R✝<VAR>x✝ : 𝕎 R✝<VAR>n k : ℕ<VAR>x : ℕ → ℤ<VAR>h : (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (f (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k) = (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (g (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k)<GOAL>(eval₂Hom ((↑ULift.ringEquiv.symm).comp ((MvPolynomial.eval x).comp C)) fun i => ↑ULift.ringEquiv.symm ((MvPolynomial.eval x) (ψ i))) (wittPolynomial p ℤ k) = (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (g (mk p fun i => { down := x i })).coeff) (wittPolynomial p ℤ k)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x = 0 ∨ y ≠ 0<GOAL>‖y‖ / Real.tan (angle x (x - y)) = ‖x‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, -y⟫_ℝ = 0<VAR>h0 : x = 0 ∨ y ≠ 0<GOAL>‖y‖ / Real.tan (angle x (x - y)) = ‖x‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, -y⟫_ℝ = 0<VAR>h0 : x = 0 ∨ -y ≠ 0<GOAL>‖y‖ / Real.tan (angle x (x - y)) = ‖x‖
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>U : UniqueMDiffWithinAt I s x<VAR>h : HasMFDerivWithinAt I I' f s x f'<VAR>h₁ : HasMFDerivWithinAt I I' f s x f₁'<GOAL>f' = f₁'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝ : DivisionSemiring α<VAR>a b c d : α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>1 / a * (a + b) * (1 / b) = 1 / a + 1 / b
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A✝ B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε✝ ε : ℝ<VAR>hε : 0 < ε<VAR>hG : cornersTheoremBound ε ≤ Fintype.card G<VAR>A : Finset G<VAR>hAε : ε * ↑(Fintype.card G) ≤ ↑A.card<VAR>hA : ThreeAPFree ↑A<GOAL>False
<VAR>F : Type u_1<VAR>R✝ : Type u_2<VAR>S : Type u_3<VAR>x y : R✝<VAR>r : ℝ<VAR>inst✝⁴ : NonAssocRing R✝<VAR>inst✝³ : DecidableEq R✝<VAR>inst✝² : NoZeroDivisors R✝<VAR>inst✝¹ : Nontrivial R✝<VAR>R : Type u_4<VAR>inst✝ : Ring R<VAR>f g : MulRingNorm R<VAR>c : ℝ<VAR>hcpos : 0 < c<VAR>h : (fun x => f x ^ c) = ⇑g<GOAL>g.equiv f
<VAR>F : Type u_1<VAR>R✝ : Type u_2<VAR>S : Type u_3<VAR>x y : R✝<VAR>r : ℝ<VAR>inst✝⁴ : NonAssocRing R✝<VAR>inst✝³ : DecidableEq R✝<VAR>inst✝² : NoZeroDivisors R✝<VAR>inst✝¹ : Nontrivial R✝<VAR>R : Type u_4<VAR>inst✝ : Ring R<VAR>f g : MulRingNorm R<VAR>c : ℝ<VAR>hcpos : 0 < c<VAR>h : (fun x => f x ^ c) = ⇑g<GOAL>0 < 1 / c ∧ (fun x => g x ^ (1 / c)) = ⇑f
<VAR>F : Type u_1<VAR>R✝ : Type u_2<VAR>S : Type u_3<VAR>x✝ y : R✝<VAR>r : ℝ<VAR>inst✝⁴ : NonAssocRing R✝<VAR>inst✝³ : DecidableEq R✝<VAR>inst✝² : NoZeroDivisors R✝<VAR>inst✝¹ : Nontrivial R✝<VAR>R : Type u_4<VAR>inst✝ : Ring R<VAR>f g : MulRingNorm R<VAR>c : ℝ<VAR>hcpos : 0 < c<VAR>h : (fun x => f x ^ c) = ⇑g<VAR>x : R<GOAL>g x ^ (1 / c) = f x
<VAR>α : Type u<VAR>l : List α<VAR>n m : ℕ<VAR>hml : m < l.length<GOAL>(l.rotate n).get? m = l.get? ((m + n) % l.length)
<VAR>α : Type u<VAR>l : List α<VAR>n m : ℕ<VAR>hml : m < l.length<GOAL>some l[(m + n) % l.length] = l[(m + n) % l.length]?
<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'<VAR>S' : Type v'<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>T : Type uT<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>f g : P.Hom P'<VAR>x : P.Cotangent<GOAL>((map f - map g) x).val = ((f.sub g ∘ₗ P.cotangentComplex) x).val
<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'<VAR>S' : Type v'<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>T : Type uT<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>f g : P.Hom P'<VAR>x : ↥P.ker<GOAL>((map f - map g) (mk x)).val = ((f.sub g ∘ₗ P.cotangentComplex) (mk x)).val
<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'<VAR>S' : Type v'<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>T : Type uT<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>f g : P.Hom P'<VAR>x : ↥P.ker<GOAL>(mk ⟨f.toAlgHom ↑x, ⋯⟩ - mk ⟨g.toAlgHom ↑x, ⋯⟩).val = P'.ker.toCotangent ((f.subToKer g) ↑x)
<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'<VAR>S' : Type v'<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>T : Type uT<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>f g : P.Hom P'<VAR>x : ↥P.ker<GOAL>P'.ker.cotangentEquivIdeal (mk ⟨f.toAlgHom ↑x, ⋯⟩ - mk ⟨g.toAlgHom ↑x, ⋯⟩).val = P'.ker.cotangentEquivIdeal (P'.ker.toCotangent ((f.subToKer g) ↑x))
<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'<VAR>S' : Type v'<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>T : Type uT<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>f g : P.Hom P'<VAR>x : ↥P.ker<GOAL>↑(P'.ker.cotangentEquivIdeal (mk ⟨f.toAlgHom ↑x, ⋯⟩ - mk ⟨g.toAlgHom ↑x, ⋯⟩).val) = ↑(P'.ker.cotangentEquivIdeal (P'.ker.toCotangent ((f.subToKer g) ↑x)))
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>inst✝³ : Zero R<VAR>inst✝² : Zero M<VAR>inst✝¹ : SMulWithZero R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>c : R<VAR>x : M<GOAL>c • x ≠ 0 ↔ c ≠ 0 ∧ x ≠ 0
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>d d' : Module.Dual R M<VAR>a : CliffordAlgebra Q<VAR>r : R<GOAL>(contractRight (a * (algebraMap R (CliffordAlgebra Q)) r)) d = (contractRight a) d * (algebraMap R (CliffordAlgebra Q)) r
<VAR>E : Type u_1<VAR>PE : Type u_2<VAR>F : Type u_3<VAR>PF : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : MetricSpace PE<VAR>inst✝⁴ : NormedAddTorsor E PE<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : MetricSpace PF<VAR>inst✝ : NormedAddTorsor F PF<VAR>f : PE ≃ᵢ PF<VAR>x y : PE<VAR>e : PE ≃ᵢ PE := ((f.trans (pointReflection ℝ (midpoint ℝ (f x) (f y))).toIsometryEquiv).trans f.symm).trans (pointReflection ℝ (midpoint ℝ x y)).toIsometryEquiv<VAR>hx : e x = x<VAR>hy : e y = y<GOAL>f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
<VAR>E : Type u_1<VAR>PE : Type u_2<VAR>F : Type u_3<VAR>PF : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : MetricSpace PE<VAR>inst✝⁴ : NormedAddTorsor E PE<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : MetricSpace PF<VAR>inst✝ : NormedAddTorsor F PF<VAR>f : PE ≃ᵢ PF<VAR>x y : PE<VAR>e : PE ≃ᵢ PE := ((f.trans (pointReflection ℝ (midpoint ℝ (f x) (f y))).toIsometryEquiv).trans f.symm).trans (pointReflection ℝ (midpoint ℝ x y)).toIsometryEquiv<VAR>hx : e x = x<VAR>hy : e y = y<VAR>hm : e (midpoint ℝ x y) = midpoint ℝ x y<GOAL>f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
<VAR>E : Type u_1<VAR>PE : Type u_2<VAR>F : Type u_3<VAR>PF : Type u_4<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : MetricSpace PE<VAR>inst✝⁴ : NormedAddTorsor E PE<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : MetricSpace PF<VAR>inst✝ : NormedAddTorsor F PF<VAR>f : PE ≃ᵢ PF<VAR>x y : PE<VAR>e : PE ≃ᵢ PE := ((f.trans (pointReflection ℝ (midpoint ℝ (f x) (f y))).toIsometryEquiv).trans f.symm).trans (pointReflection ℝ (midpoint ℝ x y)).toIsometryEquiv<VAR>hx : e x = x<VAR>hy : e y = y<VAR>hm : (pointReflection ℝ (midpoint ℝ x y)).toIsometryEquiv (f.symm ((pointReflection ℝ (midpoint ℝ (f x) (f y))).toIsometryEquiv (f (midpoint ℝ x y)))) = midpoint ℝ x y<GOAL>f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
<VAR>ι : Sort uι<VAR>R✝ : Type u<VAR>inst✝⁶ : CommSemiring R✝<VAR>A✝ : Type v<VAR>inst✝⁵ : Semiring A✝<VAR>inst✝⁴ : Algebra R✝ A✝<VAR>S✝ T : Set A✝<VAR>M N P Q : Submodule R✝ A✝<VAR>m n : A✝<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : Semiring R<VAR>inst✝² : AddCommMonoid A<VAR>inst✝¹ : Mul A<VAR>inst✝ : Module R A<VAR>S S' : Set A<VAR>x : A<VAR>hx : x ∈ span R (S * S')<GOAL>∃ T T', ↑T ⊆ S ∧ ↑T' ⊆ S' ∧ x ∈ span R (↑T * ↑T')
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<GOAL>(∃ m, m < n + 1 ∧ p m) ↔ (∃ m, m < n ∧ p m) ∨ p n
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<GOAL>(¬∃ m, m < n + 1 ∧ p m) ↔ ¬((∃ m, m < n ∧ p m) ∨ p n)
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<GOAL>(∀ (m : ℕ), m < n + 1 → ¬p m) ↔ (∀ (m : ℕ), m < n → ¬p m) ∧ ¬p n
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.RightHomologyData<VAR>A : C<VAR>k : S.X₂ ⟶ A<VAR>hk : S.f ≫ k = 0<VAR>inst✝ : S.HasRightHomology<GOAL>h.opcyclesIso.inv ≫ S.descOpcycles k hk = h.descQ k hk
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁ p₂ p1 p2 p3 p4 : P<VAR>h : InnerProductGeometry.angle (p2 -ᵥ p3) (p4 -ᵥ p3) = π<GOAL>∠ p1 p3 p2 + ∠ p1 p3 p4 = π
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁ p₂ p1 p2 p3 p4 : P<VAR>h : InnerProductGeometry.angle (p2 -ᵥ p3) (p4 -ᵥ p3) = π<GOAL>∠ p2 p3 p1 + ∠ p4 p3 p1 = π
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p p₀ p₁ p₂ p1 p2 p3 p4 : P<VAR>h : InnerProductGeometry.angle (p2 -ᵥ p3) (p4 -ᵥ p3) = π<GOAL>InnerProductGeometry.angle (p2 -ᵥ p3) (p1 -ᵥ p3) + InnerProductGeometry.angle (p4 -ᵥ p3) (p1 -ᵥ p3) = π
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>x : E<GOAL>(𝓝 x).HasBasis (fun sr => 0 < sr.2) fun sr => (sr.1.sup p).ball x sr.2
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>x : E<VAR>this : TopologicalAddGroup E<GOAL>(𝓝 x).HasBasis (fun sr => 0 < sr.2) fun sr => (sr.1.sup p).ball x sr.2
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>x : E<VAR>this : TopologicalAddGroup E<GOAL>(Filter.map (fun x_1 => x + x_1) (𝓝 0)).HasBasis (fun sr => 0 < sr.2) fun sr => (sr.1.sup p).ball x sr.2
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>x : E<VAR>this : TopologicalAddGroup E<VAR>sr : Finset ι × ℝ<GOAL>(sr.1.sup p).ball x sr.2 = (fun x_1 => x + x_1) '' (sr.1.sup p).ball 0 sr.2
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>x : E<VAR>this✝ : TopologicalAddGroup E<VAR>sr : Finset ι × ℝ<VAR>this : (sr.1.sup p).ball (x +ᵥ 0) sr.2 = x +ᵥ (sr.1.sup p).ball 0 sr.2<GOAL>(sr.1.sup p).ball x sr.2 = (fun x_1 => x + x_1) '' (sr.1.sup p).ball 0 sr.2
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>n : ℕ<VAR>a : K<VAR>hn : 0 < n<VAR>ha : a ≠ 0<GOAL>root (X ^ n - C a) ≠ 0
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>a : K<VAR>ha : a ≠ 0<VAR>hn : 0 < Nat.succ 0<GOAL>root (X ^ Nat.succ 0 - C a) ≠ 0
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>n : ℕ<VAR>a : K<VAR>hn✝ : 0 < n<VAR>ha : a ≠ 0<VAR>hn : Nat.succ 0 < n<GOAL>root (X ^ n - C a) ≠ 0
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>inst✝¹³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹² : (x : B) → TopologicalSpace (E x)<VAR>EB : Type u_7<VAR>inst✝¹¹ : NormedAddCommGroup EB<VAR>inst✝¹⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>E' : B → Type u_9<VAR>inst✝⁸ : (x : B) → Zero (E' x)<VAR>EM : Type u_10<VAR>inst✝⁷ : NormedAddCommGroup EM<VAR>inst✝⁶ : NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>inst✝⁵ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : ChartedSpace HB B<VAR>inst✝ : FiberBundle F E<VAR>f : M → TotalSpace F E<VAR>s : Set M<VAR>x₀ : M<GOAL>ContMDiffWithinAt IM (IB.prod 𝓘(𝕜, F)) n f s x₀ ↔ ContMDiffWithinAt IM IB n (fun x => (f x).proj) s x₀ ∧ ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun x => (↑(trivializationAt F E (f x₀).proj) (f x)).2) s x₀