ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x : ℤ_[p]<VAR>n : ℕ<GOAL>∀ (x : ℤ_[p]), x - ↑(x.appr n) ∈ Ideal.span {↑p ^ n}
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x : ℤ_[p]<VAR>n : ℕ<GOAL>∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ : ℤ_[p]<VAR>n : ℕ<VAR>ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)<VAR>x : ℤ_[p]<VAR>h : ¬x - ↑(x.appr n) = 0<GOAL>↑p ^ (n + 1) ∣ x - (↑(x.appr n) + ↑p ^ n * ↑(toZMod (↑(unitCoeff h) * ↑p ^ ((x - ↑(x.appr n)).valuation - ↑n).natAbs)).val)
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ : ℤ_[p]<VAR>n : ℕ<VAR>ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)<VAR>x : ℤ_[p]<VAR>h : ¬x - ↑(x.appr n) = 0<GOAL>↑p ^ (n + 1) ∣ x - ↑(x.appr n) - ↑p ^ n * ↑(toZMod (↑(unitCoeff h) * ↑p ^ ((x - ↑(x.appr n)).valuation - ↑n).natAbs)).val
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ : ℤ_[p]<VAR>n : ℕ<VAR>ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)<VAR>x : ℤ_[p]<VAR>h : ¬x - ↑(x.appr n) = 0<VAR>c : ℤ_[p]<VAR>hc : x - ↑(x.appr n) = ↑p ^ n * c<GOAL>↑p ^ (n + 1) ∣ x - ↑(x.appr n) - ↑p ^ n * ↑(toZMod (↑(unitCoeff h) * ↑p ^ ((x - ↑(x.appr n)).valuation - ↑n).natAbs)).val
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ : ℤ_[p]<VAR>n : ℕ<VAR>ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)<VAR>x : ℤ_[p]<VAR>h : ¬x - ↑(x.appr n) = 0<VAR>c : ℤ_[p]<VAR>hc : x - ↑(x.appr n) = ↑p ^ n * c<GOAL>↑p ^ (n + 1) ∣ x - ↑(x.appr n) - ↑p ^ n * (toZMod ↑(unitCoeff h) * 0 ^ ((x - ↑(x.appr n)).valuation - ↑n).natAbs).cast
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ : ℤ_[p]<VAR>n : ℕ<VAR>ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)<VAR>x : ℤ_[p]<VAR>h : ¬x - ↑(x.appr n) = 0<VAR>c : ℤ_[p]<VAR>hc : x - ↑(x.appr n) = ↑p ^ n * c<VAR>hc' : c ≠ 0<GOAL>↑p ^ (n + 1) ∣ x - ↑(x.appr n) - ↑p ^ n * (toZMod ↑(unitCoeff h) * 0 ^ ((x - ↑(x.appr n)).valuation - ↑n).natAbs).cast
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ : ℤ_[p]<VAR>n : ℕ<VAR>ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)<VAR>x : ℤ_[p]<VAR>h : ¬x - ↑(x.appr n) = 0<VAR>c : ℤ_[p]<VAR>hc : x - ↑(x.appr n) = ↑p ^ n * c<VAR>hc' : c ≠ 0<GOAL>↑p ^ (n + 1) ∣ ↑p ^ n * c - ↑p ^ n * (toZMod ↑(unitCoeff h) * 0 ^ ((↑p ^ n * c).valuation - ↑n).natAbs).cast
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ : ℤ_[p]<VAR>n : ℕ<VAR>ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)<VAR>x : ℤ_[p]<VAR>h : ¬x - ↑(x.appr n) = 0<VAR>c : ℤ_[p]<VAR>hc : x - ↑(x.appr n) = ↑p ^ n * c<VAR>hc' : c ≠ 0<GOAL>↑p ^ n * ↑p ∣ ↑p ^ n * (c - (toZMod ↑(unitCoeff h) * 0 ^ c.valuation.natAbs).cast)
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ : ℤ_[p]<VAR>n : ℕ<VAR>ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)<VAR>x : ℤ_[p]<VAR>h : ¬x - ↑(x.appr n) = 0<VAR>c : ℤ_[p]<VAR>hc : x - ↑(x.appr n) = ↑p ^ n * c<VAR>hc' : c ≠ 0<GOAL>↑p ∣ c - (toZMod ↑(unitCoeff h) * 0 ^ c.valuation.natAbs).cast
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ : ℤ_[p]<VAR>n : ℕ<VAR>ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)<VAR>x : ℤ_[p]<VAR>h : ¬x - ↑(x.appr n) = 0<VAR>c : ℤ_[p]<VAR>hc : x - ↑(x.appr n) = ↑p ^ n * c<VAR>hc' : c ≠ 0<VAR>hc0 : c.valuation.natAbs = 0<GOAL>↑p ∣ c - (toZMod ↑(unitCoeff h) * 0 ^ c.valuation.natAbs).cast
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ : ℤ_[p]<VAR>n : ℕ<VAR>ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)<VAR>x : ℤ_[p]<VAR>h : ¬x - ↑(x.appr n) = 0<VAR>c : ℤ_[p]<VAR>hc : x - ↑(x.appr n) = ↑p ^ n * c<VAR>hc' : c ≠ 0<VAR>hc0 : c.valuation.natAbs ≠ 0<GOAL>↑p ∣ c - (toZMod ↑(unitCoeff h) * 0 ^ c.valuation.natAbs).cast
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Nontrivial R<VAR>ι : Type u_1<VAR>f : ι → R<VAR>s : Finset ι<VAR>hfs : (∏ i ∈ s, (X - C (f i))).Separable<VAR>x y : ι<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hfxy : f x = f y<GOAL>x = y
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Nontrivial R<VAR>ι : Type u_1<VAR>f : ι → R<VAR>s : Finset ι<VAR>hfs : (∏ i ∈ s, (X - C (f i))).Separable<VAR>x y : ι<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hfxy : f x = f y<VAR>hxy : ¬x = y<GOAL>False
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Nontrivial R<VAR>ι : Type u_1<VAR>f : ι → R<VAR>s : Finset ι<VAR>x y : ι<VAR>hfs : ((X - C (f y)) ^ 2 * ∏ x ∈ (s.erase x).erase y, (X - C (f x))).Separable<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hfxy : f x = f y<VAR>hxy : ¬x = y<GOAL>False
<VAR>α : Type u_1<VAR>f : α → Char → α<VAR>l : List Char<VAR>c : Char<VAR>m r : List Char<VAR>a : α<GOAL>(if h : { byteIdx := utf8Len l } < { byteIdx := utf8Len l + utf8Len (c :: m) } then let_fun this := ⋯; foldlAux f { data := l ++ c :: m ++ r } { byteIdx := utf8Len l + utf8Len (c :: m) } ({ data := l ++ c :: m ++ r }.next { byteIdx := utf8Len l }) (f a ({ data := l ++ c :: m ++ r }.get { byteIdx := utf8Len l })) else a) = List.foldl f a (c :: m)
<VAR>α : Type u_1<VAR>f : α → Char → α<VAR>l : List Char<VAR>c : Char<VAR>m r : List Char<VAR>a : α<GOAL>(let_fun this := ⋯; foldlAux f { data := l ++ c :: m ++ r } { byteIdx := utf8Len l + utf8Len (c :: m) } ({ data := l ++ c :: m ++ r }.next { byteIdx := utf8Len l }) (f a ({ data := l ++ c :: m ++ r }.get { byteIdx := utf8Len l }))) = List.foldl f a (c :: m)
<VAR>α : Type u_1<VAR>f : α → Char → α<VAR>l : List Char<VAR>c : Char<VAR>m r : List Char<VAR>a : α<GOAL>foldlAux f { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l + (utf8Len m + c.utf8Size) } { byteIdx := utf8Len l + c.utf8Size } (f a c) = List.foldl f (f a c) m
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>x : ↥U<VAR>f : R<GOAL>((structureSheaf R).presheaf.germ x) ((toOpen R U) f) = (toStalk R ↑x) f
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>x : ↥U<VAR>f : R<GOAL>((structureSheaf R).presheaf.germ x) ((toOpen R U) f) = (toOpen R U ≫ (structureSheaf R).presheaf.germ x) f
<VAR>q a b c : ℚ<GOAL>-a + a = 0
<VAR>n : ℕ<GOAL>antidiagonal (n + 2) = (0, n + 2) :: map (Prod.map succ succ) (antidiagonal n) ++ [(n + 2, 0)]
<VAR>n : ℕ<GOAL>map (Prod.map id succ) (antidiagonal (n + 1)) ++ [(n + 1 + 1, 0)] = (0, n + 2) :: map (Prod.map succ succ) (antidiagonal n) ++ [(n + 2, 0)]
<VAR>n : ℕ<GOAL>map (Prod.map id succ ∘ Prod.map succ id) (antidiagonal n) = map (Prod.map succ succ) (antidiagonal n)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝¹ : Monoid β<VAR>inst✝ : Monoid γ<VAR>s : Finset α<VAR>a : α<VAR>f : α → β<VAR>ha : a ∉ s<VAR>comm : (↑(cons a s ha)).Pairwise fun a b => Commute (f a) (f b)<GOAL>(cons a s ha).noncommProd f comm = f a * s.noncommProd f ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>s t : Set α<GOAL>G.IsClique s ↔ induce s G = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>s t : Set α<GOAL>s.Pairwise G.Adj ↔ induce s G = ⊤
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>A : Type u_2<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S A<VAR>hS : S ≤ R⁰<VAR>hf : {I | I.IsMaximal}.Finite<VAR>I I' : FractionalIdeal S A<VAR>hinv hinv' : I * I' = 1<GOAL>(↑I).IsPrincipal
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>A : Type u_2<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S A<VAR>hS : S ≤ R⁰<VAR>hf : {I | I.IsMaximal}.Finite<VAR>I I' : FractionalIdeal S A<VAR>hinv : ↑I * ↑I' = ↑1<VAR>hinv' : I * I' = 1<GOAL>(↑I).IsPrincipal
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>A : Type u_2<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S A<VAR>hS : S ≤ R⁰<VAR>hf : {I | I.IsMaximal}.Finite<VAR>I I' : FractionalIdeal S A<VAR>hinv : ↑I * ↑I' = ↑1<VAR>hinv' : I * I' = 1<VAR>s : Finset (Ideal R) := hf.toFinset<VAR>this : DecidableEq (Ideal R)<GOAL>(↑I).IsPrincipal
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>A : Type u_2<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S A<VAR>hS : S ≤ R⁰<VAR>hf : {I | I.IsMaximal}.Finite<VAR>I I' : FractionalIdeal S A<VAR>hinv : ↑I * ↑I' = ↑1<VAR>hinv' : I * I' = 1<VAR>s : Finset (Ideal R) := hf.toFinset<VAR>this : DecidableEq (Ideal R)<VAR>coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤<GOAL>(↑I).IsPrincipal
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>A : Type u_2<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S A<VAR>hS : S ≤ R⁰<VAR>hf : {I | I.IsMaximal}.Finite<VAR>I I' : FractionalIdeal S A<VAR>hinv : ↑I * ↑I' = ↑1<VAR>hinv' : I * I' = 1<VAR>s : Finset (Ideal R) := hf.toFinset<VAR>this : DecidableEq (Ideal R)<VAR>coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤<VAR>nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M<GOAL>(↑I).IsPrincipal
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>A : Type u_2<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S A<VAR>hS : S ≤ R⁰<VAR>hf : {I | I.IsMaximal}.Finite<VAR>I I' : FractionalIdeal S A<VAR>hinv : ↑I * ↑I' = ↑1<VAR>hinv' : I * I' = 1<VAR>s : Finset (Ideal R) := hf.toFinset<VAR>this✝ : DecidableEq (Ideal R)<VAR>coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤<VAR>nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M<VAR>this : ∀ M ∈ s, ∃ a ∈ I, ∃ b ∈ I', a * b ∉ IsLocalization.coeSubmodule A M<GOAL>(↑I).IsPrincipal
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>A : Type u_2<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S A<VAR>hS : S ≤ R⁰<VAR>hf : {I | I.IsMaximal}.Finite<VAR>I I' : FractionalIdeal S A<VAR>hinv : ↑I * ↑I' = ↑1<VAR>hinv' : I * I' = 1<VAR>s : Finset (Ideal R) := hf.toFinset<VAR>this : DecidableEq (Ideal R)<VAR>coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤<VAR>nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M<VAR>a : Ideal R → A<VAR>ha : ∀ M ∈ s, a M ∈ I<VAR>b : Ideal R → A<VAR>hb : ∀ M ∈ s, b M ∈ I'<VAR>hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M<GOAL>(↑I).IsPrincipal
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>A : Type u_2<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S A<VAR>hS : S ≤ R⁰<VAR>hf : {I | I.IsMaximal}.Finite<VAR>I I' : FractionalIdeal S A<VAR>hinv : ↑I * ↑I' = ↑1<VAR>hinv' : I * I' = 1<VAR>s : Finset (Ideal R) := hf.toFinset<VAR>this : DecidableEq (Ideal R)<VAR>coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤<VAR>nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M<VAR>a : Ideal R → A<VAR>ha : ∀ M ∈ s, a M ∈ I<VAR>b : Ideal R → A<VAR>hb : ∀ M ∈ s, b M ∈ I'<VAR>hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M<VAR>u : Ideal R → R<VAR>hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'<VAR>hum : ∀ M ∈ s, u M ∉ M<GOAL>(↑I).IsPrincipal
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>A : Type u_2<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S A<VAR>hS : S ≤ R⁰<VAR>hf : {I | I.IsMaximal}.Finite<VAR>I I' : FractionalIdeal S A<VAR>hinv : ↑I * ↑I' = ↑1<VAR>hinv' : I * I' = 1<VAR>s : Finset (Ideal R) := hf.toFinset<VAR>this : DecidableEq (Ideal R)<VAR>coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤<VAR>nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M<VAR>a : Ideal R → A<VAR>ha : ∀ M ∈ s, a M ∈ I<VAR>b : Ideal R → A<VAR>hb : ∀ M ∈ s, b M ∈ I'<VAR>hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M<VAR>u : Ideal R → R<VAR>hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'<VAR>hum : ∀ M ∈ s, u M ∉ M<VAR>v : A := ∑ M ∈ s, u M • b M<GOAL>(↑I).IsPrincipal
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>A : Type u_2<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S A<VAR>hS : S ≤ R⁰<VAR>hf : {I | I.IsMaximal}.Finite<VAR>I I' : FractionalIdeal S A<VAR>hinv : ↑I * ↑I' = ↑1<VAR>hinv' : I * I' = 1<VAR>s : Finset (Ideal R) := hf.toFinset<VAR>this : DecidableEq (Ideal R)<VAR>coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤<VAR>nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M<VAR>a : Ideal R → A<VAR>ha : ∀ M ∈ s, a M ∈ I<VAR>b : Ideal R → A<VAR>hb : ∀ M ∈ s, b M ∈ I'<VAR>hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M<VAR>u : Ideal R → R<VAR>hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'<VAR>hum : ∀ M ∈ s, u M ∉ M<VAR>v : A := ∑ M ∈ s, u M • b M<VAR>hv : v ∈ I'<GOAL>(↑I).IsPrincipal
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>A : Type u_2<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S A<VAR>hS : S ≤ R⁰<VAR>hf : {I | I.IsMaximal}.Finite<VAR>I I' : FractionalIdeal S A<VAR>hinv : ↑I * ↑I' = ↑1<VAR>hinv' : I * I' = 1<VAR>s : Finset (Ideal R) := hf.toFinset<VAR>this : DecidableEq (Ideal R)<VAR>coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤<VAR>nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M<VAR>a : Ideal R → A<VAR>ha : ∀ M ∈ s, a M ∈ I<VAR>b : Ideal R → A<VAR>hb : ∀ M ∈ s, b M ∈ I'<VAR>hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M<VAR>u : Ideal R → R<VAR>hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'<VAR>hum : ∀ M ∈ s, u M ∉ M<VAR>v : A := ∑ M ∈ s, u M • b M<VAR>hv : v ∈ I'<VAR>h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>A : Type u_2<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S A<VAR>hS : S ≤ R⁰<VAR>hf : {I | I.IsMaximal}.Finite<VAR>I I' : FractionalIdeal S A<VAR>hinv : ↑I * ↑I' = ↑1<VAR>hinv' : I * I' = 1<VAR>s : Finset (Ideal R) := hf.toFinset<VAR>this : DecidableEq (Ideal R)<VAR>coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤<VAR>nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M<VAR>a : Ideal R → A<VAR>ha : ∀ M ∈ s, a M ∈ I<VAR>b : Ideal R → A<VAR>hb : ∀ M ∈ s, b M ∈ I'<VAR>hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M<VAR>u : Ideal R → R<VAR>hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'<VAR>hum : ∀ M ∈ s, u M ∉ M<VAR>v : A := ∑ M ∈ s, u M • b M<VAR>hv : v ∈ I'<VAR>h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤<VAR>M : Ideal R<VAR>hM : M.IsMaximal<VAR>hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>A : Type u_2<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S A<VAR>hS : S ≤ R⁰<VAR>hf : {I | I.IsMaximal}.Finite<VAR>I I' : FractionalIdeal S A<VAR>hinv : ↑I * ↑I' = ↑1<VAR>hinv' : I * I' = 1<VAR>s : Finset (Ideal R) := hf.toFinset<VAR>this : DecidableEq (Ideal R)<VAR>coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤<VAR>nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M<VAR>a : Ideal R → A<VAR>ha : ∀ M ∈ s, a M ∈ I<VAR>b : Ideal R → A<VAR>hb : ∀ M ∈ s, b M ∈ I'<VAR>hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M<VAR>u : Ideal R → R<VAR>hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'<VAR>hum : ∀ M ∈ s, u M ∉ M<VAR>v : A := ∑ M ∈ s, u M • b M<VAR>hv : v ∈ I'<VAR>h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤<VAR>M : Ideal R<VAR>hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M<VAR>hM : M ∈ hf.toFinset<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>A : Type u_2<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S A<VAR>hS : S ≤ R⁰<VAR>hf : {I | I.IsMaximal}.Finite<VAR>I I' : FractionalIdeal S A<VAR>hinv : ↑I * ↑I' = ↑1<VAR>hinv' : I * I' = 1<VAR>s : Finset (Ideal R) := hf.toFinset<VAR>this✝ : DecidableEq (Ideal R)<VAR>coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤<VAR>nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M<VAR>a : Ideal R → A<VAR>ha : ∀ M ∈ s, a M ∈ I<VAR>b : Ideal R → A<VAR>hb : ∀ M ∈ s, b M ∈ I'<VAR>hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M<VAR>u : Ideal R → R<VAR>hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'<VAR>hum : ∀ M ∈ s, u M ∉ M<VAR>v : A := ∑ M ∈ s, u M • b M<VAR>hv : v ∈ I'<VAR>h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤<VAR>M : Ideal R<VAR>hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M<VAR>hM : M ∈ hf.toFinset<VAR>this : ∀ a ∈ I, ∀ b ∈ I', ∃ c, (algebraMap R A) c = a * b<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>A : Type u_2<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S A<VAR>hS : S ≤ R⁰<VAR>hf : {I | I.IsMaximal}.Finite<VAR>I I' : FractionalIdeal S A<VAR>hinv : ↑I * ↑I' = ↑1<VAR>hinv' : I * I' = 1<VAR>s : Finset (Ideal R) := hf.toFinset<VAR>this✝ : DecidableEq (Ideal R)<VAR>coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤<VAR>nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M<VAR>a : Ideal R → A<VAR>ha : ∀ M ∈ s, a M ∈ I<VAR>b : Ideal R → A<VAR>hb : ∀ M ∈ s, b M ∈ I'<VAR>hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M<VAR>u : Ideal R → R<VAR>hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'<VAR>hum : ∀ M ∈ s, u M ∉ M<VAR>v : A := ∑ M ∈ s, u M • b M<VAR>hv : v ∈ I'<VAR>h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤<VAR>M : Ideal R<VAR>hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M<VAR>hM : M ∈ hf.toFinset<VAR>this : ∀ a ∈ I, ∀ b ∈ I', ∃ c, (algebraMap R A) c = a * b<VAR>hmem : a M * v ∈ IsLocalization.coeSubmodule A M<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>A : Type u_2<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S A<VAR>hS : S ≤ R⁰<VAR>hf : {I | I.IsMaximal}.Finite<VAR>I I' : FractionalIdeal S A<VAR>hinv : ↑I * ↑I' = ↑1<VAR>hinv' : I * I' = 1<VAR>s : Finset (Ideal R) := hf.toFinset<VAR>this✝ : DecidableEq (Ideal R)<VAR>coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤<VAR>nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M<VAR>a : Ideal R → A<VAR>ha : ∀ M ∈ s, a M ∈ I<VAR>b : Ideal R → A<VAR>hb : ∀ M ∈ s, b M ∈ I'<VAR>hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M<VAR>u : Ideal R → R<VAR>hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'<VAR>hum : ∀ M ∈ s, u M ∉ M<VAR>v : A := ∑ M ∈ s, u M • b M<VAR>hv : v ∈ I'<VAR>h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤<VAR>M : Ideal R<VAR>hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M<VAR>hM : M ∈ hf.toFinset<VAR>this : ∀ a ∈ I, ∀ b ∈ I', ∃ c, (algebraMap R A) c = a * b<VAR>hmem : ∑ x ∈ s, u x • (a M * b x) ∈ IsLocalization.coeSubmodule A M<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>A : Type u_2<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S A<VAR>hS : S ≤ R⁰<VAR>hf : {I | I.IsMaximal}.Finite<VAR>I I' : FractionalIdeal S A<VAR>hinv : ↑I * ↑I' = ↑1<VAR>hinv' : I * I' = 1<VAR>s : Finset (Ideal R) := hf.toFinset<VAR>this✝ : DecidableEq (Ideal R)<VAR>coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤<VAR>nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M<VAR>a : Ideal R → A<VAR>ha : ∀ M ∈ s, a M ∈ I<VAR>b : Ideal R → A<VAR>hb : ∀ M ∈ s, b M ∈ I'<VAR>hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M<VAR>u : Ideal R → R<VAR>hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'<VAR>hum : ∀ M ∈ s, u M ∉ M<VAR>v : A := ∑ M ∈ s, u M • b M<VAR>hv : v ∈ I'<VAR>h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤<VAR>M : Ideal R<VAR>hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M<VAR>hM : M ∈ hf.toFinset<VAR>this : ∀ a ∈ I, ∀ b ∈ I', ∃ c, (algebraMap R A) c = a * b<VAR>hmem : u M • (a M * b M) ∈ IsLocalization.coeSubmodule A M<GOAL>False
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>A : Type u_2<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S A<VAR>hS : S ≤ R⁰<VAR>hf : {I | I.IsMaximal}.Finite<VAR>I I' : FractionalIdeal S A<VAR>hinv : ↑I * ↑I' = ↑1<VAR>hinv' : I * I' = 1<VAR>s : Finset (Ideal R) := hf.toFinset<VAR>this✝ : DecidableEq (Ideal R)<VAR>coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤<VAR>nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M<VAR>a : Ideal R → A<VAR>ha : ∀ M ∈ s, a M ∈ I<VAR>b : Ideal R → A<VAR>hb : ∀ M ∈ s, b M ∈ I'<VAR>hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M<VAR>u : Ideal R → R<VAR>hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'<VAR>hum : ∀ M ∈ s, u M ∉ M<VAR>v : A := ∑ M ∈ s, u M • b M<VAR>hv : v ∈ I'<VAR>h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) = ⊤<VAR>M : Ideal R<VAR>hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * Submodule.span R {v}) ≤ M<VAR>hM : M ∈ hf.toFinset<VAR>this : ∀ a ∈ I, ∀ b ∈ I', ∃ c, (algebraMap R A) c = a * b<VAR>hmem : u M • (a M * b M) + ∑ x ∈ s.erase M, u x • (a M * b x) ∈ IsLocalization.coeSubmodule A M<GOAL>∑ x ∈ s.erase M, u x • (a M * b x) ∈ IsLocalization.coeSubmodule A M
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : ContinuousMul M<VAR>f : ι → X → M<VAR>p : ι → Prop<VAR>hc : ∀ (i : ι), p i → Continuous (f i)<VAR>hf : LocallyFinite fun i => mulSupport (f i)<GOAL>Continuous fun x => ∏ᶠ (i : ι) (_ : p i), f i x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : ContinuousMul M<VAR>f : ι → X → M<VAR>p : ι → Prop<VAR>hc : ∀ (i : ι), p i → Continuous (f i)<VAR>hf : LocallyFinite fun i => mulSupport (f i)<GOAL>Continuous fun x => ∏ᶠ (j : Subtype p), f (↑j) x
<VAR>R : Type u<VAR>inst✝³ : Field R<VAR>inst✝² : Fintype R<VAR>R' : Type v<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : IsDomain R'<VAR>χ : MulChar R R'<VAR>hχ : χ ≠ 1<VAR>ψ : AddChar R R'<VAR>b : R<GOAL>∑ a : R, χ (a * b⁻¹) * ψ (a - b) = ∑ c : R, χ c * ψ (b * (c - 1))
<VAR>R : Type u<VAR>inst✝³ : Field R<VAR>inst✝² : Fintype R<VAR>R' : Type v<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : IsDomain R'<VAR>χ : MulChar R R'<VAR>hχ : χ ≠ 1<VAR>ψ : AddChar R R'<VAR>b : R<VAR>hb : b = 0<GOAL>∑ a : R, χ (a * b⁻¹) * ψ (a - b) = ∑ c : R, χ c * ψ (b * (c - 1))
<VAR>R : Type u<VAR>inst✝³ : Field R<VAR>inst✝² : Fintype R<VAR>R' : Type v<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : IsDomain R'<VAR>χ : MulChar R R'<VAR>hχ : χ ≠ 1<VAR>ψ : AddChar R R'<VAR>b : R<VAR>hb : b ≠ 0<GOAL>∑ a : R, χ (a * b⁻¹) * ψ (a - b) = ∑ c : R, χ c * ψ (b * (c - 1))
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c✝ d✝ : ℝ<VAR>f : ℝ → E<VAR>c d : ℝ<GOAL>c⁻¹ • ∫ (x : ℝ) in a..b, f (d - x / c) = ∫ (x : ℝ) in d - b / c..d - a / c, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝ : DivisionSemiring α<VAR>a✝ b✝ c✝ d a b c : α<VAR>hc : c ≠ 0<GOAL>a / c + b = (a + b * c) / c
<VAR>f : Ordinal.{u} → Ordinal.{u}<VAR>H : IsNormal f<GOAL>Set.Unbounded (fun x x_1 => x < x_1) (fixedPoints f)
<VAR>f : Ordinal.{u} → Ordinal.{u}<VAR>H : IsNormal f<GOAL>fixedPoints f = ⋂ i, fixedPoints f
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>m✝ : OuterMeasure α<VAR>β : Type u_3<VAR>f : α → β<VAR>hf : Surjective f<VAR>m : OuterMeasure β<VAR>s : Set β<GOAL>((map f) ((comap f) m)) s = m s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b c : Ordinal.{u_4}<VAR>a0 : a = 0<GOAL>a * (b - c) = a * b - a * c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b c : Ordinal.{u_4}<VAR>a0 : ¬a = 0<VAR>d : Ordinal.{u_4}<GOAL>a * (b - c) ≤ d ↔ a * b - a * c ≤ d
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α✝<VAR>μ✝ μ₁ μ₂ : Measure α✝<VAR>s s₁ s₂ t : Set α✝<VAR>α : Type u_8<VAR>ι : Type u_9<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : Countable ι<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>f : ι → Set α<GOAL>Tendsto (fun i => μ (Accumulate f i)) atTop (𝓝 (μ (⋃ i, f i)))