ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m<VAR>c : idx × ℕ →₀ ℕ<VAR>sum_induction_steps : (map (Int.castRingHom ℚ)) (∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) = ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)<GOAL>(fun x => ↑x) (coeff c ((bind₁ fun b => (rename fun i => (b, i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ) - ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)) / ↑p ^ n).num = coeff c ((bind₁ fun b => (rename fun i => (b, i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ) - ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)) / ↑p ^ n
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m<VAR>c : idx × ℕ →₀ ℕ<VAR>sum_induction_steps : (map (Int.castRingHom ℚ)) (∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) = ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)<GOAL>↑((Int.castRingHom ℚ) (coeff c ((bind₁ fun i => (rename fun i_1 => (i, i_1)) (W_ ℤ n)) Φ - ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i))) / ↑p ^ n).num = (Int.castRingHom ℚ) (coeff c ((bind₁ fun i => (rename fun i_1 => (i, i_1)) (W_ ℤ n)) Φ - ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i))) / ↑p ^ n
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m<VAR>c : idx × ℕ →₀ ℕ<VAR>sum_induction_steps : (map (Int.castRingHom ℚ)) (∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) = ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)<GOAL>↑((Int.castRingHom ℚ) (coeff c ((bind₁ fun i => (rename fun i_1 => (i, i_1)) (W_ ℤ n)) Φ - ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i))) / ↑↑(p ^ n)).num = (Int.castRingHom ℚ) (coeff c ((bind₁ fun i => (rename fun i_1 => (i, i_1)) (W_ ℤ n)) Φ - ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i))) / ↑↑(p ^ n)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m<VAR>c : idx × ℕ →₀ ℕ<VAR>sum_induction_steps : (map (Int.castRingHom ℚ)) (∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) = ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)<GOAL>↑(p ^ n) ∣ coeff c ((bind₁ fun i => (rename fun i_1 => (i, i_1)) (W_ ℤ n)) Φ - ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m<VAR>c : idx × ℕ →₀ ℕ<VAR>sum_induction_steps : (map (Int.castRingHom ℚ)) (∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) = ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)<GOAL>↑(p ^ n) ≠ 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m<VAR>sum_induction_steps : (map (Int.castRingHom ℚ)) (∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) = ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)<GOAL>∀ (c : idx × ℕ →₀ ℕ), ↑(p ^ n) ∣ coeff c ((bind₁ fun i => (rename fun i_1 => (i, i_1)) (W_ ℤ n)) Φ - ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m<VAR>sum_induction_steps : (map (Int.castRingHom ℚ)) (∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) = ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) i ^ p ^ (n - i)<GOAL>C ↑(p ^ n) ∣ (bind₁ fun i => (rename fun i_1 => (i, i_1)) (W_ ℤ n)) Φ - ∑ i ∈ Finset.range n, C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)
<VAR>M : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero M<VAR>q : Associates M<VAR>hq : q ≠ 0<VAR>n : ℕ<VAR>hn : n + 1 ≠ 0<VAR>c : Fin (n + 1 + 1) → Associates M<VAR>h₁ : StrictMono c<VAR>h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i<GOAL>Irreducible (c 1)
<VAR>M : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero M<VAR>q : Associates M<VAR>hq : q ≠ 0<VAR>n : ℕ<VAR>hn : n + 1 ≠ 0<VAR>c : Fin (n + 1 + 1) → Associates M<VAR>h₁ : StrictMono c<VAR>h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i<GOAL>c 1 ≠ ⊥
<VAR>M : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero M<VAR>q : Associates M<VAR>hq : q ≠ 0<VAR>n : ℕ<VAR>hn : n + 1 ≠ 0<VAR>c : Fin (n + 1 + 1) → Associates M<VAR>h₁ : StrictMono c<VAR>h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i<VAR>b : Associates M<VAR>hb : b < c 1<GOAL>b = ⊥
<VAR>M : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero M<VAR>q : Associates M<VAR>hq : q ≠ 0<VAR>n : ℕ<VAR>hn : n + 1 ≠ 0<VAR>c : Fin (n + 1 + 1) → Associates M<VAR>h₁ : StrictMono c<VAR>h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i<VAR>i : ℕ<VAR>hi : i < n + 1 + 1<VAR>hb : c ⟨i, hi⟩ < c 1<GOAL>c ⟨i, hi⟩ = ⊥
<VAR>z : ℍ<VAR>A B : ℝ<VAR>h : 0 < B<VAR>hz : z ∈ verticalStrip A B<GOAL>r ⟨{ re := A, im := B }, h⟩ ≤ r z
<VAR>z : ℍ<VAR>A B : ℝ<VAR>h : 0 < B<VAR>hz : z ∈ verticalStrip A B<GOAL>√(r1 ⟨{ re := A, im := B }, h⟩) ≤ √(r1 z)
<VAR>z : ℍ<VAR>A B : ℝ<VAR>h : 0 < B<VAR>hz : z ∈ verticalStrip A B<GOAL>r1 ⟨{ re := A, im := B }, h⟩ ≤ r1 z
<VAR>z : ℍ<VAR>A B : ℝ<VAR>h : 0 < B<VAR>hz : z ∈ verticalStrip A B<GOAL>(UpperHalfPlane.re ⟨{ re := A, im := B }, h⟩ ^ 2 / UpperHalfPlane.im ⟨{ re := A, im := B }, h⟩ ^ 2 + 1)⁻¹ ≤ (z.re ^ 2 / z.im ^ 2 + 1)⁻¹
<VAR>z : ℍ<VAR>A B : ℝ<VAR>h : 0 < B<VAR>hz : z ∈ verticalStrip A B<GOAL>z.re ^ 2 / z.im ^ 2 ≤ UpperHalfPlane.re ⟨{ re := A, im := B }, h⟩ ^ 2 / UpperHalfPlane.im ⟨{ re := A, im := B }, h⟩ ^ 2
<VAR>z : ℍ<VAR>A B : ℝ<VAR>h : 0 < B<VAR>hz : z ∈ verticalStrip A B<GOAL>z.re ^ 2 ≤ UpperHalfPlane.re ⟨{ re := A, im := B }, h⟩ ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : PredOrder α<VAR>inst✝ : IsPredArchimedean α<VAR>a b : α<GOAL>(hasse α).Reachable a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : PredOrder α<VAR>inst✝ : IsPredArchimedean α<VAR>a b : α<GOAL>ReflTransGen (Function.swap (hasse α).Adj) b a
<VAR>S : Type u_1<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>inst✝⁵ : Nontrivial S<VAR>inst✝⁴ : IsDedekindDomain S<VAR>inst✝³ : Module.Free ℤ S<VAR>inst✝² : Module.Finite ℤ S<VAR>I : Ideal S<VAR>E : Type u_2<VAR>inst✝¹ : EquivLike E S ↥I<VAR>inst✝ : AddEquivClass E S ↥I<VAR>e : E<VAR>hI : ¬I = ⊥<VAR>ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S<VAR>b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S<GOAL>(LinearMap.det (↑ℤ (Submodule.subtype I) ∘ₗ (↑e).toIntLinearMap)).natAbs = absNorm I
<VAR>S : Type u_1<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>inst✝⁵ : Nontrivial S<VAR>inst✝⁴ : IsDedekindDomain S<VAR>inst✝³ : Module.Free ℤ S<VAR>inst✝² : Module.Finite ℤ S<VAR>I : Ideal S<VAR>E : Type u_2<VAR>inst✝¹ : EquivLike E S ↥I<VAR>inst✝ : AddEquivClass E S ↥I<VAR>e : E<VAR>hI : ¬I = ⊥<VAR>ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S<VAR>b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S<VAR>h✝ : IsEmpty ι<GOAL>(LinearMap.det (↑ℤ (Submodule.subtype I) ∘ₗ (↑e).toIntLinearMap)).natAbs = absNorm I
<VAR>S : Type u_1<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>inst✝⁵ : Nontrivial S<VAR>inst✝⁴ : IsDedekindDomain S<VAR>inst✝³ : Module.Free ℤ S<VAR>inst✝² : Module.Finite ℤ S<VAR>I : Ideal S<VAR>E : Type u_2<VAR>inst✝¹ : EquivLike E S ↥I<VAR>inst✝ : AddEquivClass E S ↥I<VAR>e : E<VAR>hI : ¬I = ⊥<VAR>ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S<VAR>b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S<VAR>h✝ : Nonempty ι<GOAL>(LinearMap.det (↑ℤ (Submodule.subtype I) ∘ₗ (↑e).toIntLinearMap)).natAbs = absNorm I
<VAR>S : Type u_1<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>inst✝⁵ : Nontrivial S<VAR>inst✝⁴ : IsDedekindDomain S<VAR>inst✝³ : Module.Free ℤ S<VAR>inst✝² : Module.Finite ℤ S<VAR>I : Ideal S<VAR>E : Type u_2<VAR>inst✝¹ : EquivLike E S ↥I<VAR>inst✝ : AddEquivClass E S ↥I<VAR>e : E<VAR>hI : ¬I = ⊥<VAR>ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S<VAR>b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S<VAR>h✝ : Nonempty ι<VAR>this✝ : Fintype (S ⧸ I) := I.fintypeQuotientOfFreeOfNeBot hI<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI<VAR>b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI<VAR>ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ ↥I := selfBasis b I hI<GOAL>(LinearMap.det (↑ℤ (Submodule.subtype I) ∘ₗ (↑e).toIntLinearMap)).natAbs = absNorm I
<VAR>S : Type u_1<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>inst✝⁵ : Nontrivial S<VAR>inst✝⁴ : IsDedekindDomain S<VAR>inst✝³ : Module.Free ℤ S<VAR>inst✝² : Module.Finite ℤ S<VAR>I : Ideal S<VAR>E : Type u_2<VAR>inst✝¹ : EquivLike E S ↥I<VAR>inst✝ : AddEquivClass E S ↥I<VAR>e : E<VAR>hI : ¬I = ⊥<VAR>ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S<VAR>b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S<VAR>h✝ : Nonempty ι<VAR>this✝ : Fintype (S ⧸ I) := I.fintypeQuotientOfFreeOfNeBot hI<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI<VAR>b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI<VAR>ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ ↥I := selfBasis b I hI<VAR>ab_eq : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑((selfBasis b I hI) i) = smithCoeffs b I hI i • (ringBasis b I hI) i<GOAL>(LinearMap.det (↑ℤ (Submodule.subtype I) ∘ₗ (↑e).toIntLinearMap)).natAbs = absNorm I
<VAR>S : Type u_1<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>inst✝⁵ : Nontrivial S<VAR>inst✝⁴ : IsDedekindDomain S<VAR>inst✝³ : Module.Free ℤ S<VAR>inst✝² : Module.Finite ℤ S<VAR>I : Ideal S<VAR>E : Type u_2<VAR>inst✝¹ : EquivLike E S ↥I<VAR>inst✝ : AddEquivClass E S ↥I<VAR>e : E<VAR>hI : ¬I = ⊥<VAR>ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S<VAR>b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S<VAR>h✝ : Nonempty ι<VAR>this✝ : Fintype (S ⧸ I) := I.fintypeQuotientOfFreeOfNeBot hI<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI<VAR>b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI<VAR>ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ ↥I := selfBasis b I hI<VAR>ab_eq : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑((selfBasis b I hI) i) = smithCoeffs b I hI i • (ringBasis b I hI) i<VAR>e' : S ≃ₗ[ℤ] ↥I := b'.equiv ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))<VAR>f : S →ₗ[ℤ] S := ↑ℤ (Submodule.subtype I) ∘ₗ ↑e'<VAR>f_apply : ∀ (x : S), f x = ↑((b'.equiv ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))) x) := fun x => rfl<GOAL>(LinearMap.det (↑ℤ (Submodule.subtype I) ∘ₗ (↑e).toIntLinearMap)).natAbs = absNorm I
<VAR>S : Type u_1<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>inst✝⁵ : Nontrivial S<VAR>inst✝⁴ : IsDedekindDomain S<VAR>inst✝³ : Module.Free ℤ S<VAR>inst✝² : Module.Finite ℤ S<VAR>I : Ideal S<VAR>E : Type u_2<VAR>inst✝¹ : EquivLike E S ↥I<VAR>inst✝ : AddEquivClass E S ↥I<VAR>e : E<VAR>hI : ¬I = ⊥<VAR>ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S<VAR>b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S<VAR>h✝ : Nonempty ι<VAR>this✝ : Fintype (S ⧸ I) := I.fintypeQuotientOfFreeOfNeBot hI<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI<VAR>b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI<VAR>ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ ↥I := selfBasis b I hI<VAR>ab_eq : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑((selfBasis b I hI) i) = smithCoeffs b I hI i • (ringBasis b I hI) i<VAR>e' : S ≃ₗ[ℤ] ↥I := b'.equiv ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))<VAR>f : S →ₗ[ℤ] S := ↑ℤ (Submodule.subtype I) ∘ₗ ↑e'<VAR>f_apply : ∀ (x : S), f x = ↑((b'.equiv ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))) x) := fun x => rfl<GOAL>(LinearMap.det f).natAbs = absNorm I
<VAR>S : Type u_1<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>inst✝⁵ : Nontrivial S<VAR>inst✝⁴ : IsDedekindDomain S<VAR>inst✝³ : Module.Free ℤ S<VAR>inst✝² : Module.Finite ℤ S<VAR>I : Ideal S<VAR>E : Type u_2<VAR>inst✝¹ : EquivLike E S ↥I<VAR>inst✝ : AddEquivClass E S ↥I<VAR>e : E<VAR>hI : ¬I = ⊥<VAR>ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S<VAR>b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S<VAR>h✝ : Nonempty ι<VAR>this✝ : Fintype (S ⧸ I) := I.fintypeQuotientOfFreeOfNeBot hI<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI<VAR>b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI<VAR>ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ ↥I := selfBasis b I hI<VAR>ab_eq : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑((selfBasis b I hI) i) = smithCoeffs b I hI i • (ringBasis b I hI) i<VAR>e' : S ≃ₗ[ℤ] ↥I := b'.equiv ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))<VAR>f : S →ₗ[ℤ] S := ↑ℤ (Submodule.subtype I) ∘ₗ ↑e'<VAR>f_apply : ∀ (x : S), f x = ↑((b'.equiv ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))) x) := fun x => rfl<VAR>ha : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), f (b' i) = a i • b' i<GOAL>(LinearMap.det f).natAbs = absNorm I
<VAR>S : Type u_1<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>inst✝⁵ : Nontrivial S<VAR>inst✝⁴ : IsDedekindDomain S<VAR>inst✝³ : Module.Free ℤ S<VAR>inst✝² : Module.Finite ℤ S<VAR>I : Ideal S<VAR>E : Type u_2<VAR>inst✝¹ : EquivLike E S ↥I<VAR>inst✝ : AddEquivClass E S ↥I<VAR>e : E<VAR>hI : ¬I = ⊥<VAR>ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S<VAR>b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S<VAR>h✝ : Nonempty ι<VAR>this✝¹ : Fintype (S ⧸ I) := I.fintypeQuotientOfFreeOfNeBot hI<VAR>this✝ : DecidableEq ι := Classical.decEq ι<VAR>a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI<VAR>b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI<VAR>ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ ↥I := selfBasis b I hI<VAR>ab_eq : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑((selfBasis b I hI) i) = smithCoeffs b I hI i • (ringBasis b I hI) i<VAR>e' : S ≃ₗ[ℤ] ↥I := b'.equiv ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))<VAR>f : S →ₗ[ℤ] S := ↑ℤ (Submodule.subtype I) ∘ₗ ↑e'<VAR>f_apply : ∀ (x : S), f x = ↑((b'.equiv ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))) x) := fun x => rfl<VAR>ha : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), f (b' i) = a i • b' i<VAR>this : DecidableEq ι := Classical.decEq ι<GOAL>(LinearMap.det f).natAbs = absNorm I
<VAR>S : Type u_1<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>inst✝⁵ : Nontrivial S<VAR>inst✝⁴ : IsDedekindDomain S<VAR>inst✝³ : Module.Free ℤ S<VAR>inst✝² : Module.Finite ℤ S<VAR>I : Ideal S<VAR>E : Type u_2<VAR>inst✝¹ : EquivLike E S ↥I<VAR>inst✝ : AddEquivClass E S ↥I<VAR>e : E<VAR>hI : ¬I = ⊥<VAR>ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S<VAR>b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S<VAR>h✝ : Nonempty ι<VAR>this✝¹ : Fintype (S ⧸ I) := I.fintypeQuotientOfFreeOfNeBot hI<VAR>this✝ : DecidableEq ι := Classical.decEq ι<VAR>a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI<VAR>b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI<VAR>ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ ↥I := selfBasis b I hI<VAR>ab_eq : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑((selfBasis b I hI) i) = smithCoeffs b I hI i • (ringBasis b I hI) i<VAR>e' : S ≃ₗ[ℤ] ↥I := b'.equiv ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))<VAR>f : S →ₗ[ℤ] S := ↑ℤ (Submodule.subtype I) ∘ₗ ↑e'<VAR>f_apply : ∀ (x : S), f x = ↑((b'.equiv ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))) x) := fun x => rfl<VAR>ha : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), f (b' i) = a i • b' i<VAR>this : DecidableEq ι := Classical.decEq ι<GOAL>((LinearMap.toMatrix b' b') f).det.natAbs = (Matrix.diagonal a).det.natAbs
<VAR>S : Type u_1<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>inst✝⁵ : Nontrivial S<VAR>inst✝⁴ : IsDedekindDomain S<VAR>inst✝³ : Module.Free ℤ S<VAR>inst✝² : Module.Finite ℤ S<VAR>I : Ideal S<VAR>E : Type u_2<VAR>inst✝¹ : EquivLike E S ↥I<VAR>inst✝ : AddEquivClass E S ↥I<VAR>e : E<VAR>hI : ¬I = ⊥<VAR>ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S<VAR>b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S<VAR>h✝ : Nonempty ι<VAR>this✝¹ : Fintype (S ⧸ I) := I.fintypeQuotientOfFreeOfNeBot hI<VAR>this✝ : DecidableEq ι := Classical.decEq ι<VAR>a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI<VAR>b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI<VAR>ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ ↥I := selfBasis b I hI<VAR>ab_eq : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑((selfBasis b I hI) i) = smithCoeffs b I hI i • (ringBasis b I hI) i<VAR>e' : S ≃ₗ[ℤ] ↥I := b'.equiv ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))<VAR>f : S →ₗ[ℤ] S := ↑ℤ (Submodule.subtype I) ∘ₗ ↑e'<VAR>f_apply : ∀ (x : S), f x = ↑((b'.equiv ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))) x) := fun x => rfl<VAR>ha : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), f (b' i) = a i • b' i<VAR>this : DecidableEq ι := Classical.decEq ι<GOAL>∏ i : Module.Free.ChooseBasisIndex ℤ S, (a i).natAbs = Nat.card (S ⧸ I)
<VAR>S : Type u_1<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>inst✝⁵ : Nontrivial S<VAR>inst✝⁴ : IsDedekindDomain S<VAR>inst✝³ : Module.Free ℤ S<VAR>inst✝² : Module.Finite ℤ S<VAR>I : Ideal S<VAR>E : Type u_2<VAR>inst✝¹ : EquivLike E S ↥I<VAR>inst✝ : AddEquivClass E S ↥I<VAR>e : E<VAR>hI : ¬I = ⊥<VAR>ι : Type u_1 := Module.Free.ChooseBasisIndex ℤ S<VAR>b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S<VAR>h✝ : Nonempty ι<VAR>this✝² : Fintype (S ⧸ I) := I.fintypeQuotientOfFreeOfNeBot hI<VAR>this✝¹ : DecidableEq ι := Classical.decEq ι<VAR>a : Module.Free.ChooseBasisIndex ℤ S → ℤ := smithCoeffs b I hI<VAR>b' : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := ringBasis b I hI<VAR>ab : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ ↥I := selfBasis b I hI<VAR>ab_eq : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), ↑((selfBasis b I hI) i) = smithCoeffs b I hI i • (ringBasis b I hI) i<VAR>e' : S ≃ₗ[ℤ] ↥I := b'.equiv ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))<VAR>f : S →ₗ[ℤ] S := ↑ℤ (Submodule.subtype I) ∘ₗ ↑e'<VAR>f_apply : ∀ (x : S), f x = ↑((b'.equiv ab (Equiv.refl (Module.Free.ChooseBasisIndex ℤ S))) x) := fun x => rfl<VAR>ha : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), f (b' i) = a i • b' i<VAR>this✝ : DecidableEq ι := Classical.decEq ι<VAR>this : ∀ (i : Module.Free.ChooseBasisIndex ℤ S), NeZero (a i).natAbs<GOAL>∏ i : Module.Free.ChooseBasisIndex ℤ S, (a i).natAbs = Nat.card (S ⧸ I)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>p : α → Prop<VAR>x y z : α<VAR>n : ℕ<VAR>x✝ : (f ^ n).SameCycle x y<VAR>m : ℤ<VAR>h : ((f ^ n) ^ m) x = y<GOAL>(f ^ (↑n * m)) x = y
<VAR>n m : ℕ<GOAL>nim ↑n + nim ↑m ≈ nim ↑(n ^^^ m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>s t : Set β<VAR>a : α<GOAL>(κ.restrict ⋯) a = κ a
<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>s t : Set M<VAR>x : M<VAR>hs : UniqueMDiffWithinAt I s x<VAR>ht : 𝓝[s] x ≤ 𝓝[t] x<GOAL>𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x ≤ 𝓝[↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I] ↑(extChartAt I x) x
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>X : C<GOAL>e.counit.app (e.functor.obj X) = e.functor.map (e.unitInv.app X)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : C ≌ D<VAR>X : C<GOAL>𝟙 (e.functor.obj X) = 𝟙 (e.functor.obj ((𝟭 C).obj X))
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>s t : Set α<VAR>hs : IsComplete s<VAR>ht : IsComplete t<GOAL>IsComplete (s ∪ t)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>s t : Set α<VAR>hs : ∀ (l : Ultrafilter α), Cauchy ↑l → s ∈ l → ∃ x ∈ s, ↑l ≤ 𝓝 x<VAR>ht : ∀ (l : Ultrafilter α), Cauchy ↑l → t ∈ l → ∃ x ∈ t, ↑l ≤ 𝓝 x<GOAL>∀ (l : Ultrafilter α), Cauchy ↑l → (s ∈ l → ∃ x ∈ s ∪ t, ↑l ≤ 𝓝 x) ∧ (t ∈ l → ∃ x ∈ s ∪ t, ↑l ≤ 𝓝 x)
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>a : ℍ[R]<GOAL>normSq a = 0 ↔ a = 0
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>a : ℍ[R]<VAR>h : normSq a = 0<GOAL>a = 0
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>a : ℍ[R]<VAR>h : ((a.re ^ 2 = 0 ∧ a.imI ^ 2 = 0) ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0<GOAL>a = 0
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>a : ℍ[R]<VAR>h : (a.re ^ 2 + a.imI ^ 2 = 0 ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0<GOAL>0 ≤ a.re ^ 2
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>a : ℍ[R]<VAR>h : (a.re ^ 2 + a.imI ^ 2 = 0 ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0<GOAL>0 ≤ a.imI ^ 2
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>a : ℍ[R]<VAR>h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 = 0 ∧ a.imK ^ 2 = 0<GOAL>0 ≤ a.re ^ 2 + a.imI ^ 2
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>a : ℍ[R]<VAR>h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 = 0 ∧ a.imK ^ 2 = 0<GOAL>0 ≤ a.imJ ^ 2
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>a : ℍ[R]<VAR>h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2 = 0<GOAL>0 ≤ a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>a : ℍ[R]<VAR>h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2 = 0<GOAL>0 ≤ a.imK ^ 2
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>n : ℕ<GOAL>Tendsto (fun x => rexp x / x ^ n) atTop atTop
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>n : ℕ<VAR>C : ℝ<VAR>hC₁ : 1 ≤ C<GOAL>∃ ia, True ∧ ∀ x ∈ Set.Ioi ia, rexp x / x ^ n ∈ Set.Ici C
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>n : ℕ<VAR>C : ℝ<VAR>hC₁ : 1 ≤ C<VAR>hC₀ : 0 < C<GOAL>∃ ia, True ∧ ∀ x ∈ Set.Ioi ia, rexp x / x ^ n ∈ Set.Ici C