ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f g : PreTilt K v O hv p<VAR>hf : ¬f = 0<VAR>hg : ¬g = 0<GOAL>valAux K v O hv p (f * g) = valAux K v O hv p f * valAux K v O hv p g
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f g : PreTilt K v O hv p<VAR>hf : ¬f = 0<VAR>hg : ¬g = 0<VAR>m : ℕ<VAR>hm : (coeff (ModP K v O hv p) p m) f ≠ 0<GOAL>valAux K v O hv p (f * g) = valAux K v O hv p f * valAux K v O hv p g
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f g : PreTilt K v O hv p<VAR>hf : ¬f = 0<VAR>hg : ¬g = 0<VAR>m : ℕ<VAR>hm : (coeff (ModP K v O hv p) p m) f ≠ 0<VAR>n : ℕ<VAR>hn : (coeff (ModP K v O hv p) p n) g ≠ 0<GOAL>valAux K v O hv p (f * g) = valAux K v O hv p f * valAux K v O hv p g
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f g : PreTilt K v O hv p<VAR>hf : ¬f = 0<VAR>hg : ¬g = 0<VAR>m n : ℕ<VAR>hn : (coeff (ModP K v O hv p) p n) g ≠ 0<VAR>hm : (coeff (ModP K v O hv p) p (max m n)) f ≠ 0<GOAL>valAux K v O hv p (f * g) = valAux K v O hv p f * valAux K v O hv p g
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f g : PreTilt K v O hv p<VAR>hf : ¬f = 0<VAR>hg : ¬g = 0<VAR>m n : ℕ<VAR>hm : (coeff (ModP K v O hv p) p (max m n)) f ≠ 0<VAR>hn : (coeff (ModP K v O hv p) p (max m n)) g ≠ 0<GOAL>valAux K v O hv p (f * g) = valAux K v O hv p f * valAux K v O hv p g
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f g : PreTilt K v O hv p<VAR>hf : ¬f = 0<VAR>hg : ¬g = 0<VAR>m n : ℕ<VAR>hm : (coeff (ModP K v O hv p) p (max m n)) f ≠ 0<VAR>hn : (coeff (ModP K v O hv p) p (max m n)) g ≠ 0<VAR>hfg : (coeff (ModP K v O hv p) p (max m n + 1)) (f * g) ≠ 0<GOAL>valAux K v O hv p (f * g) = valAux K v O hv p f * valAux K v O hv p g
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f g : PreTilt K v O hv p<VAR>hf : ¬f = 0<VAR>hg : ¬g = 0<VAR>m n : ℕ<VAR>hm : (coeff (ModP K v O hv p) p (max m n)) f ≠ 0<VAR>hn : (coeff (ModP K v O hv p) p (max m n)) g ≠ 0<VAR>hfg : (coeff (ModP K v O hv p) p (max m n + 1)) (f * g) ≠ 0<GOAL>ModP.preVal K v O hv p ((coeff (ModP K v O hv p) p (max m n + 1)) (f * g)) ^ p ^ (max m n + 1) = ModP.preVal K v O hv p ((coeff (ModP K v O hv p) p (max m n + 1)) f) ^ p ^ (max m n + 1) * ModP.preVal K v O hv p ((coeff (ModP K v O hv p) p (max m n + 1)) g) ^ p ^ (max m n + 1)
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f g : PreTilt K v O hv p<VAR>hf : ¬f = 0<VAR>hg : ¬g = 0<VAR>m n : ℕ<VAR>hm : (coeff (ModP K v O hv p) p (max m n)) f ≠ 0<VAR>hn : (coeff (ModP K v O hv p) p (max m n)) g ≠ 0<VAR>hfg : (coeff (ModP K v O hv p) p (max m n + 1)) f * (coeff (ModP K v O hv p) p (max m n + 1)) g ≠ 0<GOAL>ModP.preVal K v O hv p ((coeff (ModP K v O hv p) p (max m n + 1)) f * (coeff (ModP K v O hv p) p (max m n + 1)) g) ^ p ^ (max m n + 1) = ModP.preVal K v O hv p ((coeff (ModP K v O hv p) p (max m n + 1)) f) ^ p ^ (max m n + 1) * ModP.preVal K v O hv p ((coeff (ModP K v O hv p) p (max m n + 1)) g) ^ p ^ (max m n + 1)
<VAR>d : ℤ<VAR>a b : ℤ√d<VAR>hcoprime : IsCoprime a.re a.im<VAR>hdvd : b ∣ a<GOAL>IsCoprime b.re b.im
<VAR>d : ℤ<VAR>a b : ℤ√d<VAR>hcoprime : IsCoprime a.re a.im<VAR>hdvd : b ∣ a<GOAL>¬(b.re = 0 ∧ b.im = 0)
<VAR>d : ℤ<VAR>a b : ℤ√d<VAR>hcoprime : IsCoprime a.re a.im<VAR>hdvd : b ∣ a<GOAL>∀ z ∈ nonunits ℤ, z ≠ 0 → z ∣ b.re → ¬z ∣ b.im
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a✝ a₁ a₂ b✝ b₁ b₂ : E<VAR>r✝ r₁ r₂ : ℝ<VAR>a b : E<VAR>r : ℝ<VAR>c : E<GOAL>c ∈ (fun x => b * x) ⁻¹' ball a r ↔ c ∈ ball (a / b) r
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>f : α × β → γ<VAR>s s' : Set α<VAR>t : Set β<VAR>hs' : s' ⊆ s<VAR>hss' : s ⊆ closure s'<VAR>K : ℝ≥0<VAR>ha : ∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t<VAR>hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s<VAR>x : α<VAR>y : β<VAR>hx : x ∈ s<VAR>hy : y ∈ t<GOAL>ContinuousWithinAt f (s ×ˢ t) (x, y)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>f : α × β → γ<VAR>s s' : Set α<VAR>t : Set β<VAR>hs' : s' ⊆ s<VAR>hss' : s ⊆ closure s'<VAR>K : ℝ≥0<VAR>ha : ∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t<VAR>hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s<VAR>x : α<VAR>y : β<VAR>hx : x ∈ s<VAR>hy : y ∈ t<VAR>ε : ℝ≥0∞<VAR>ε0 : 0 < ε<GOAL>∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ EMetric.closedBall (f (x, y)) ε
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>f : α × β → γ<VAR>s s' : Set α<VAR>t : Set β<VAR>hs' : s' ⊆ s<VAR>hss' : s ⊆ closure s'<VAR>K : ℝ≥0<VAR>ha : ∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t<VAR>hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s<VAR>x : α<VAR>y : β<VAR>hx : x ∈ s<VAR>hy : y ∈ t<VAR>ε : ℝ≥0∞<VAR>ε0 : 0 < ε / 2<GOAL>∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ EMetric.closedBall (f (x, y)) ε
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>f : α × β → γ<VAR>s s' : Set α<VAR>t : Set β<VAR>hs' : s' ⊆ s<VAR>hss' : s ⊆ closure s'<VAR>K : ℝ≥0<VAR>ha : ∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t<VAR>hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s<VAR>x : α<VAR>y : β<VAR>hx : x ∈ s<VAR>hy : y ∈ t<VAR>ε : ℝ≥0∞<VAR>ε0 : 0 < ε / 2<VAR>δ : ℝ≥0<VAR>δpos : 0 < δ<VAR>hδ : ↑δ * ↑(3 * K) < ε / 2<GOAL>∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ EMetric.closedBall (f (x, y)) ε
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>f : α × β → γ<VAR>s s' : Set α<VAR>t : Set β<VAR>hs' : s' ⊆ s<VAR>hss' : s ⊆ closure s'<VAR>K : ℝ≥0<VAR>ha : ∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t<VAR>hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s<VAR>x : α<VAR>y : β<VAR>hx : x ∈ s<VAR>hy : y ∈ t<VAR>ε : ℝ≥0∞<VAR>ε0 : 0 < ε / 2<VAR>δ : ℝ≥0<VAR>δpos : 0 < ↑δ<VAR>hδ : ↑δ * ↑(3 * K) < ε / 2<GOAL>∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ EMetric.closedBall (f (x, y)) ε
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>f : α × β → γ<VAR>s s' : Set α<VAR>t : Set β<VAR>hs' : s' ⊆ s<VAR>hss' : s ⊆ closure s'<VAR>K : ℝ≥0<VAR>ha : ∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t<VAR>hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s<VAR>x : α<VAR>y : β<VAR>hx : x ∈ s<VAR>hy : y ∈ t<VAR>ε : ℝ≥0∞<VAR>ε0 : 0 < ε / 2<VAR>δ : ℝ≥0<VAR>δpos : 0 < ↑δ<VAR>hδ : ↑δ * ↑(3 * K) < ε / 2<VAR>x' : α<VAR>hx' : x' ∈ s'<VAR>hxx' : edist x x' < ↑δ<GOAL>∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ EMetric.closedBall (f (x, y)) ε
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>f : α × β → γ<VAR>s s' : Set α<VAR>t : Set β<VAR>hs' : s' ⊆ s<VAR>hss' : s ⊆ closure s'<VAR>K : ℝ≥0<VAR>ha : ∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t<VAR>hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s<VAR>x : α<VAR>y : β<VAR>hx : x ∈ s<VAR>hy : y ∈ t<VAR>ε : ℝ≥0∞<VAR>ε0 : 0 < ε / 2<VAR>δ : ℝ≥0<VAR>δpos : 0 < ↑δ<VAR>hδ : ↑δ * ↑(3 * K) < ε / 2<VAR>x' : α<VAR>hx' : x' ∈ s'<VAR>hxx' : edist x x' < ↑δ<VAR>A : s ∩ EMetric.ball x ↑δ ∈ 𝓝[s] x<GOAL>∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ EMetric.closedBall (f (x, y)) ε
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>f : α × β → γ<VAR>s s' : Set α<VAR>t : Set β<VAR>hs' : s' ⊆ s<VAR>hss' : s ⊆ closure s'<VAR>K : ℝ≥0<VAR>ha : ∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t<VAR>hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s<VAR>x : α<VAR>y : β<VAR>hx : x ∈ s<VAR>hy : y ∈ t<VAR>ε : ℝ≥0∞<VAR>ε0 : 0 < ε / 2<VAR>δ : ℝ≥0<VAR>δpos : 0 < ↑δ<VAR>hδ : ↑δ * ↑(3 * K) < ε / 2<VAR>x' : α<VAR>hx' : x' ∈ s'<VAR>hxx' : edist x x' < ↑δ<VAR>A : s ∩ EMetric.ball x ↑δ ∈ 𝓝[s] x<VAR>B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y<GOAL>∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ EMetric.closedBall (f (x, y)) ε
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>f : α × β → γ<VAR>s s' : Set α<VAR>t : Set β<VAR>hs' : s' ⊆ s<VAR>hss' : s ⊆ closure s'<VAR>K : ℝ≥0<VAR>ha : ∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t<VAR>hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s<VAR>x : α<VAR>y : β<VAR>hx : x ∈ s<VAR>hy : y ∈ t<VAR>ε : ℝ≥0∞<VAR>ε0 : 0 < ε / 2<VAR>δ : ℝ≥0<VAR>δpos : 0 < ↑δ<VAR>hδ : ↑δ * ↑(3 * K) < ε / 2<VAR>x' : α<VAR>hx' : x' ∈ s'<VAR>hxx' : edist x x' < ↑δ<VAR>A : s ∩ EMetric.ball x ↑δ ∈ 𝓝[s] x<VAR>B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y<VAR>a : α<VAR>b : β<VAR>has : (a, b).1 ∈ s<VAR>hax : (a, b).1 ∈ EMetric.ball x ↑δ<VAR>hbt : (a, b).2 ∈ t<VAR>hby : (a, b).2 ∈ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2}<GOAL>f (a, b) ∈ EMetric.closedBall (f (x, y)) ε
<VAR>R : Type u_1<VAR>inst✝² : LinearOrderedField R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x y : M<VAR>hy : y ≠ 0<GOAL>(∃ r, 0 ≤ r ∧ x = r • y) ↔ SameRay R x y
<VAR>R : Type u_1<VAR>inst✝² : LinearOrderedField R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x y : M<VAR>hy : y ≠ 0<GOAL>(∃ r, 0 ≤ r ∧ x = r • y) ↔ SameRay R y x
<VAR>R : Type u_1<VAR>inst✝² : LinearOrderedField R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x y : M<VAR>hy : y ≠ 0<GOAL>(∃ r, 0 ≤ r ∧ r • y = x) ↔ SameRay R y x
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<VAR>p : α<VAR>hp : 0 < p<VAR>b : α<GOAL>toIcoDiv ⋯ 0 b = ⌊b⌋
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p q : α → Prop<VAR>h : Disjoint p q<VAR>inst✝² : Fintype { x // p x }<VAR>inst✝¹ : Fintype { x // q x }<VAR>inst✝ : Fintype { x // p x ∨ q x }<GOAL>card { x // p x ∨ q x } = card { x // p x } + card { x // q x }
<VAR>p : ℝ<VAR>x : ℝ≥0∞<VAR>hx_pos : 0 < x<VAR>hx_ne_top : x ≠ ⊤<GOAL>0 < x ^ p
<VAR>p : ℝ<VAR>x : ℝ≥0∞<VAR>hx_pos : 0 < x<VAR>hx_ne_top : x ≠ ⊤<VAR>hp_pos : 0 < p<GOAL>0 < x ^ p
<VAR>p : ℝ<VAR>x : ℝ≥0∞<VAR>hx_pos : 0 < x<VAR>hx_ne_top : x ≠ ⊤<VAR>hp_nonpos : p ≤ 0<GOAL>0 < x ^ p
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>c : ℝ<VAR>hc : c ≠ 0<VAR>x : ℝ<GOAL>gaussianPDFReal μ v (c * x) = |c⁻¹| * gaussianPDFReal (c⁻¹ * μ) (⟨(c ^ 2)⁻¹, ⋯⟩ * v) x
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>c : ℝ<VAR>hc : c ≠ 0<VAR>x : ℝ<GOAL>|c⁻¹| * gaussianPDFReal (c⁻¹ * μ) (⟨c⁻¹ ^ 2, ⋯⟩ * v) x = |c⁻¹| * gaussianPDFReal (c⁻¹ * μ) (⟨(c ^ 2)⁻¹, ⋯⟩ * v) x
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RespectsIso P<VAR>R S R' S' : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>f : R →+* S<VAR>r : R<VAR>inst✝¹ : IsLocalization.Away r R'<VAR>inst✝ : IsLocalization.Away (f r) S'<VAR>e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv<VAR>e₂ : Localization.Away (f r) ≃+* S' := (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv<GOAL>P (Localization.awayMap f r) ↔ P (IsLocalization.Away.map R' S' f r)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RespectsIso P<VAR>R S R' S' : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>f : R →+* S<VAR>r : R<VAR>inst✝¹ : IsLocalization.Away r R'<VAR>inst✝ : IsLocalization.Away (f r) S'<VAR>e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv<VAR>e₂ : Localization.Away (f r) ≃+* S' := (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv<GOAL>P (e₁.toCommRingCatIso.hom ≫ CommRingCat.ofHom (IsLocalization.map (Localization.Away (f r)) f ⋯)) ↔ P (IsLocalization.Away.map R' S' f r)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RespectsIso P<VAR>R S R' S' : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>f : R →+* S<VAR>r : R<VAR>inst✝¹ : IsLocalization.Away r R'<VAR>inst✝ : IsLocalization.Away (f r) S'<VAR>e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv<VAR>e₂ : Localization.Away (f r) ≃+* S' := (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv<GOAL>P (CommRingCat.ofHom (e₁.toCommRingCatIso.hom ≫ CommRingCat.ofHom (IsLocalization.map (Localization.Away (f r)) f ⋯)) ≫ e₂.toCommRingCatIso.hom) ↔ P (IsLocalization.Away.map R' S' f r)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RespectsIso P<VAR>R S R' S' : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>f : R →+* S<VAR>r : R<VAR>inst✝¹ : IsLocalization.Away r R'<VAR>inst✝ : IsLocalization.Away (f r) S'<VAR>e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv<VAR>e₂ : Localization.Away (f r) ≃+* S' := (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv<GOAL>P (CommRingCat.ofHom (e₁.toCommRingCatIso.hom ≫ CommRingCat.ofHom (IsLocalization.map (Localization.Away (f r)) f ⋯)) ≫ e₂.toCommRingCatIso.hom) = P (IsLocalization.Away.map R' S' f r)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RespectsIso P<VAR>R S R' S' : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>f : R →+* S<VAR>r : R<VAR>inst✝¹ : IsLocalization.Away r R'<VAR>inst✝ : IsLocalization.Away (f r) S'<VAR>e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv<VAR>e₂ : Localization.Away (f r) ≃+* S' := (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv<GOAL>CommRingCat.ofHom (e₁.toCommRingCatIso.hom ≫ CommRingCat.ofHom (IsLocalization.map (Localization.Away (f r)) f ⋯)) ≫ e₂.toCommRingCatIso.hom = IsLocalization.Away.map R' S' f r
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RespectsIso P<VAR>R S R' S' : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>f : R →+* S<VAR>r : R<VAR>inst✝¹ : IsLocalization.Away r R'<VAR>inst✝ : IsLocalization.Away (f r) S'<VAR>e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv<VAR>e₂ : Localization.Away (f r) ≃+* S' := (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv<VAR>e : R' →+* S' := (↑e₂).comp ((IsLocalization.map (Localization.Away (f r)) f ⋯).comp ↑e₁)<GOAL>CommRingCat.ofHom (e₁.toCommRingCatIso.hom ≫ CommRingCat.ofHom (IsLocalization.map (Localization.Away (f r)) f ⋯)) ≫ e₂.toCommRingCatIso.hom = IsLocalization.Away.map R' S' f r
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RespectsIso P<VAR>R S R' S' : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>f : R →+* S<VAR>r : R<VAR>inst✝¹ : IsLocalization.Away r R'<VAR>inst✝ : IsLocalization.Away (f r) S'<VAR>e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv<VAR>e₂ : Localization.Away (f r) ≃+* S' := (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv<VAR>e : R' →+* S' := (↑e₂).comp ((IsLocalization.map (Localization.Away (f r)) f ⋯).comp ↑e₁)<GOAL>e = IsLocalization.Away.map R' S' f r
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RespectsIso P<VAR>R S R' S' : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>f : R →+* S<VAR>r : R<VAR>inst✝¹ : IsLocalization.Away r R'<VAR>inst✝ : IsLocalization.Away (f r) S'<VAR>e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv<VAR>e₂ : Localization.Away (f r) ≃+* S' := (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv<VAR>e : R' →+* S' := (↑e₂).comp ((IsLocalization.map (Localization.Away (f r)) f ⋯).comp ↑e₁)<GOAL>e.comp (algebraMap R R') = (IsLocalization.Away.map R' S' f r).comp (algebraMap R R')
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RespectsIso P<VAR>R S R' S' : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>inst✝³ : Algebra R R'<VAR>inst✝² : Algebra S S'<VAR>f : R →+* S<VAR>r : R<VAR>inst✝¹ : IsLocalization.Away r R'<VAR>inst✝ : IsLocalization.Away (f r) S'<VAR>e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv<VAR>e₂ : Localization.Away (f r) ≃+* S' := (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv<VAR>e : R' →+* S' := (↑e₂).comp ((IsLocalization.map (Localization.Away (f r)) f ⋯).comp ↑e₁)<VAR>x : R<GOAL>(IsLocalization.map S' (id S) ⋯) ((IsLocalization.map (Localization.Away (f r)) f ⋯) ((IsLocalization.map (Localization.Away r) (id R) ⋯) ((algebraMap R R') x))) = (IsLocalization.map S' f ⋯) ((algebraMap R R') x)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>x : X<VAR>y : Y<VAR>s : Set (X × Y)<VAR>tx : Set X<VAR>ty : Set Y<GOAL>s ∈ 𝓝[tx ×ˢ ty] (x, y) ↔ ∃ u ∈ 𝓝[tx] x, ∃ v ∈ 𝓝[ty] y, u ×ˢ v ⊆ s
<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>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>f : α → β<VAR>hf : AEMeasurable f μ<GOAL>(map f μ).toOuterMeasure = ((OuterMeasure.map f) μ.toOuterMeasure).trim
<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>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>f : α → β<VAR>hf : AEMeasurable f μ<GOAL>∀ (s : Set β), MeasurableSet s → (map f μ).toOuterMeasure s = ((OuterMeasure.map f) μ.toOuterMeasure) s
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>n : ℕ<VAR>x : α<VAR>h : ¬p x = true<GOAL>rdropWhile p (l ++ [x]) = l ++ [x]
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : NoMaxOrder α<VAR>a : α<GOAL>Bounded (fun x x_1 => x < x_1) (Iic a)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : Ring S<VAR>M : Type u_4<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>m : Submodule R M<VAR>N : Type u_5<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p q : Submodule R M<VAR>x✝¹ : IsSemisimpleModule R ↥p<VAR>x✝ : IsSemisimpleModule R ↥q<VAR>f : Bool → Submodule R M := fun t => Bool.rec q p t<GOAL>IsSemisimpleModule R ↥(p ⊔ q)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : Ring S<VAR>M : Type u_4<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>m : Submodule R M<VAR>N : Type u_5<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p q : Submodule R M<VAR>x✝¹ : IsSemisimpleModule R ↥p<VAR>x✝ : IsSemisimpleModule R ↥q<VAR>f : Bool → Submodule R M := fun t => Bool.rec q p t<GOAL>IsSemisimpleModule R ↥(⨆ i ∈ Set.univ, f i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : CanonicallyOrderedAddCommMonoid α<VAR>f✝ g✝ : ι →₀ α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>f g : ι →₀ α<VAR>i : ι<VAR>a b : α<VAR>inst✝ : DecidableEq ι<VAR>f1 f2 : ι →₀ α<GOAL>f1.support \ f2.support ⊆ (f1 - f2).support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>f✝ g : β → α<VAR>a a₁ a₂ : α<VAR>inst✝ : Fintype β<VAR>f : β → α<GOAL>∏' (b : β), f b = ∏ b : β, f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>f✝ g : β → α<VAR>a a₁ a₂ : α<VAR>inst✝ : Fintype β<VAR>f : β → α<GOAL>∀ b ∉ univ, f b = 1
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M : Matrix n n R<VAR>j : n<VAR>s : R<VAR>u : n → R<GOAL>(M.updateColumn j (s • u)).det = s * (M.updateColumn j u).det
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M : Matrix n n R<VAR>j : n<VAR>s : R<VAR>u : n → R<GOAL>s * (Mᵀ.updateRow j u).det = s * (M.updateColumn j u).det
<VAR>x✝ y z x : ℝ<GOAL>1 ^ x = 1
<GOAL>UnivLE.{u, v} ↔ univ.{u, v + 1} ≤ univ.{v, u + 1}
<GOAL>(¬∀ (α : Type u), Small.{v, u} α) ↔ ¬univ.{u, v + 1} ≤ univ.{v, u + 1}
<GOAL>(¬∀ (α : Type u), lift.{v + 1, u} #α < univ.{v, max u (v + 1)}) ↔ ¬univ.{u, v + 1} ≤ univ.{v, u + 1}
<VAR>r : ℝ<VAR>hr : r < 0<VAR>x : ℝ<VAR>hx : x ∈ Set.Icc 0 1<GOAL>x ∈ {x | (fun x => (fun x => -|log x| ^ 1) x = log x) x}
<VAR>α : Type u_1<VAR>S : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSpace M<VAR>fst✝ : R<VAR>snd✝ : M<GOAL>𝓝 (fst✝, snd✝) = (𝓝 (fst (fst✝, snd✝))).prod (𝓝 (snd (fst✝, snd✝)))