ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f g : α →. σ<VAR>hf : Partrec f<VAR>hg : Partrec g<VAR>k : ℕ →. ℕ<VAR>hk : Nat.Partrec k<VAR>H : ∀ (a : ℕ), (∀ x ∈ k a, (x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (f a)) ∨ x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (g a)) ∧ ((k a).Dom ↔ ((↑(decode₂ α a)).bind fun a => Part.map encode (f a)).Dom ∨ ((↑(decode₂ α a)).bind fun a => Part.map encode (g a)).Dom)<VAR>k' : α → Part σ := fun a => (k (encode a)).bind fun n => ↑(decode n)<VAR>a : α<VAR>this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a<VAR>h : (f a).Dom ∨ (g a).Dom<GOAL>∃ (h : (k (encode a)).Dom), (↑(decode ((k (encode a)).get h))).Dom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f g : α →. σ<VAR>hf : Partrec f<VAR>hg : Partrec g<VAR>k : ℕ →. ℕ<VAR>hk✝ : Nat.Partrec k<VAR>H : ∀ (a : ℕ), (∀ x ∈ k a, (x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (f a)) ∨ x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (g a)) ∧ ((k a).Dom ↔ ((↑(decode₂ α a)).bind fun a => Part.map encode (f a)).Dom ∨ ((↑(decode₂ α a)).bind fun a => Part.map encode (g a)).Dom)<VAR>k' : α → Part σ := fun a => (k (encode a)).bind fun n => ↑(decode n)<VAR>a : α<VAR>this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a<VAR>h : (f a).Dom ∨ (g a).Dom<VAR>hk : (k (encode a)).Dom<GOAL>∃ (h : (k (encode a)).Dom), (↑(decode ((k (encode a)).get h))).Dom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f g : α →. σ<VAR>hf : Partrec f<VAR>hg : Partrec g<VAR>k : ℕ →. ℕ<VAR>hk✝ : Nat.Partrec k<VAR>H : ∀ (a : ℕ), (∀ x ∈ k a, (x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (f a)) ∨ x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (g a)) ∧ ((k a).Dom ↔ ((↑(decode₂ α a)).bind fun a => Part.map encode (f a)).Dom ∨ ((↑(decode₂ α a)).bind fun a => Part.map encode (g a)).Dom)<VAR>k' : α → Part σ := fun a => (k (encode a)).bind fun n => ↑(decode n)<VAR>a : α<VAR>this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a<VAR>h : (f a).Dom ∨ (g a).Dom<VAR>hk : (k (encode a)).Dom<GOAL>(↑(decode ((k (encode a)).get hk))).Dom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f g : α →. σ<VAR>hf : Partrec f<VAR>hg : Partrec g<VAR>k : ℕ →. ℕ<VAR>hk✝ : Nat.Partrec k<VAR>k' : α → Part σ := fun a => (k (encode a)).bind fun n => ↑(decode n)<VAR>a : α<VAR>this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a<VAR>h : (f a).Dom ∨ (g a).Dom<VAR>hk : (k (encode a)).Dom<VAR>H : ∀ (a : ℕ), (∀ x ∈ k a, (∃ a_2, decode₂ α a = Option.some a_2 ∧ ∃ a ∈ f a_2, encode a = x) ∨ ∃ a_2, decode₂ α a = Option.some a_2 ∧ ∃ a ∈ g a_2, encode a = x) ∧ ((k a).Dom ↔ ((↑(decode₂ α a)).bind fun a => Part.map encode (f a)).Dom ∨ ((↑(decode₂ α a)).bind fun a => Part.map encode (g a)).Dom)<GOAL>(↑(decode ((k (encode a)).get hk))).Dom
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℝ<VAR>ha : a < 0<VAR>b s : ℝ<GOAL>(fun x => rexp (a * x ^ 2 + b * x)) =o[atTop] fun x => x ^ s
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℝ<VAR>ha : a < 0<VAR>b s : ℝ<GOAL>(fun x => rexp (a * x ^ 2 + b * x)) =o[atTop] fun x => rexp (-x)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℝ<VAR>ha : a < 0<VAR>b s : ℝ<GOAL>Tendsto (fun x => -x - (a * x ^ 2 + b * x)) atTop atTop
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℝ<VAR>ha : a < 0<VAR>b s : ℝ<VAR>this : (fun x => -x - (a * x ^ 2 + b * x)) = fun x => x * (-a * x - (b + 1))<GOAL>Tendsto (fun x => x * (-a * x - (b + 1))) atTop atTop
<VAR>a : ℤ<GOAL>∃ u, ∃ (_ : IsUnit u), ↑a.natAbs = u * a
<VAR>a : ℤ<VAR>h : a = ↑a.natAbs<GOAL>∃ u, ∃ (_ : IsUnit u), ↑a.natAbs = u * a
<VAR>a : ℤ<VAR>h : a = -↑a.natAbs<GOAL>∃ u, ∃ (_ : IsUnit u), ↑a.natAbs = u * a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>1 / a ≤ b ↔ 1 / b ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hfg : f ≤ᶠ[ae μ] g<VAR>hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>hg : AEMeasurable g μ<VAR>hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ<GOAL>f =ᶠ[ae μ] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hfg : f ≤ᶠ[ae μ] g<VAR>hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>hg : AEMeasurable g μ<VAR>hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ<VAR>this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, g x < f x + (↑n)⁻¹<GOAL>f =ᶠ[ae μ] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hfg : f ≤ᶠ[ae μ] g<VAR>hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>hg : AEMeasurable g μ<VAR>hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ<VAR>this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, g x < f x + (↑n)⁻¹<VAR>x : α<VAR>hlt : ∀ (i : ℕ), g x < f x + (↑i)⁻¹<VAR>hle : f x ≤ g x<GOAL>g x ≤ f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hfg : f ≤ᶠ[ae μ] g<VAR>hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>hg : AEMeasurable g μ<VAR>hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ<VAR>this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, g x < f x + (↑n)⁻¹<VAR>x : α<VAR>hlt : ∀ (i : ℕ), g x < f x + (↑i)⁻¹<VAR>hle : f x ≤ g x<GOAL>Tendsto (fun n => f x + (↑n)⁻¹) atTop (𝓝 (f x))
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B✝ B' I J D X : Set α<VAR>e f : α<VAR>B : Set α<GOAL>B ∈ {B | M.Base B} ↔ B ∈ maximals (fun x x_1 => x ⊆ x_1) {I | M.Indep I}
<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>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>f : α × β → E<VAR>h1f : AEStronglyMeasurable f (μ.prod ν)<GOAL>HasFiniteIntegral f (μ.prod ν) ↔ (∀ᵐ (x : α) ∂μ, HasFiniteIntegral (fun y => f (x, y)) ν) ∧ HasFiniteIntegral (fun x => ∫ (y : β), ‖f (x, y)‖ ∂ν) μ
<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>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>f : α × β → E<VAR>h1f : AEStronglyMeasurable f (μ.prod ν)<GOAL>(∀ᵐ (x : α) ∂μ, HasFiniteIntegral (fun y => AEStronglyMeasurable.mk f h1f (x, y)) ν) ∧ HasFiniteIntegral (fun x => ∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂ν) μ ↔ (∀ᵐ (x : α) ∂μ, HasFiniteIntegral (fun y => f (x, y)) ν) ∧ HasFiniteIntegral (fun x => ∫ (y : β), ‖f (x, y)‖ ∂ν) μ
<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>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>f : α × β → E<VAR>h1f : AEStronglyMeasurable f (μ.prod ν)<GOAL>(∀ᵐ (x : α) ∂μ, HasFiniteIntegral (fun y => AEStronglyMeasurable.mk f h1f (x, y)) ν) ↔ ∀ᵐ (x : α) ∂μ, HasFiniteIntegral (fun y => f (x, y)) ν
<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>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>f : α × β → E<VAR>h1f : AEStronglyMeasurable f (μ.prod ν)<GOAL>HasFiniteIntegral (fun x => ∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂ν) μ ↔ HasFiniteIntegral (fun x => ∫ (y : β), ‖f (x, y)‖ ∂ν) μ
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : FiniteDimensional K V<VAR>b : ι → V<VAR>lin_ind : LinearIndependent K b<VAR>card_eq : Fintype.card ι = finrank K V<GOAL>span K (Set.range b) = ⊤
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : FiniteDimensional K V<VAR>b : ι → V<VAR>lin_ind : LinearIndependent K b<VAR>card_eq : Fintype.card ι = finrank K V<VAR>ne_top : ¬span K (Set.range b) = ⊤<GOAL>False
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : FiniteDimensional K V<VAR>b : ι → V<VAR>lin_ind : LinearIndependent K b<VAR>card_eq : finrank K ↥(span K (Set.range b)) = finrank K V<VAR>ne_top : ¬span K (Set.range b) = ⊤<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Fintype α<VAR>s t : Finset α<GOAL>univ.Nontrivial ↔ Nontrivial α
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>h : I = 0<VAR>z : K<GOAL>‖{ toFun := __spread✝⁻⁰.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread✝⁻⁰.invFun, left_inv := ⋯, right_inv := ⋯ } z‖ = ‖z‖
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>h : I = 0<VAR>z : K<GOAL>‖{ toFun := __spread✝⁻⁰.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread✝⁻⁰.invFun, left_inv := ⋯, right_inv := ⋯ } (↑(re z) + ↑(im z) * I)‖ = ‖↑(re z) + ↑(im z) * I‖
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_3, u_1} C<VAR>B B' : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>i : B ⟶ B'<VAR>W : C<VAR>e : (a : α) → X a ⟶ W<VAR>h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ ≫ i = g₂ ≫ π a₂ ≫ i → g₁ ≫ e a₁ = g₂ ≫ e a₂<VAR>Z : C<VAR>a₁ a₂ : α<VAR>g₁ : Z ⟶ X a₁<VAR>g₂ : Z ⟶ X a₂<VAR>hg : g₁ ≫ π a₁ = g₂ ≫ π a₂<GOAL>g₁ ≫ π a₁ ≫ i = g₂ ≫ π a₂ ≫ i
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_3, u_1} C<VAR>B B' : C<VAR>α : Type u_2<VAR>X : α → C<VAR>π : (a : α) → X a ⟶ B<VAR>i : B ⟶ B'<VAR>W : C<VAR>e : (a : α) → X a ⟶ W<VAR>h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), g₁ ≫ π a₁ ≫ i = g₂ ≫ π a₂ ≫ i → g₁ ≫ e a₁ = g₂ ≫ e a₂<VAR>Z : C<VAR>a₁ a₂ : α<VAR>g₁ : Z ⟶ X a₁<VAR>g₂ : Z ⟶ X a₂<VAR>hg : g₁ ≫ π a₁ = g₂ ≫ π a₂<GOAL>(g₂ ≫ π a₂) ≫ i = g₂ ≫ π a₂ ≫ i
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>r : R<VAR>n : ℕ<GOAL>(ghostComponent n) (teichmullerFun p r) = r ^ p ^ n
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>r : R<VAR>n : ℕ<GOAL>(teichmullerFun p r).coeff 0 ^ p ^ n = r ^ p ^ n
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>r : R<VAR>n : ℕ<GOAL>∀ b ∈ Finset.range (n + 1), b ≠ 0 → ↑p ^ b * (teichmullerFun p r).coeff b ^ p ^ (n - b) = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>r : R<VAR>n : ℕ<GOAL>0 ∉ Finset.range (n + 1) → ↑p ^ 0 * (teichmullerFun p r).coeff 0 ^ p ^ (n - 0) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(μ.restrict s).singularPart ν = (μ.singularPart ν).restrict s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>Measurable (s.indicator (μ.rnDeriv ν))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(μ.singularPart ν).restrict s ⟂ₘ ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>μ.restrict s = (μ.singularPart ν).restrict s + ν.withDensity (s.indicator (μ.rnDeriv ν))
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v w x y : V<VAR>p : G.Walk x y<VAR>hp : ¬p.Nil<GOAL>(p.tail hp).length + 1 = p.length
<VAR>𝕜 : Type u_1<VAR>M : Type u_2<VAR>α : Type u_3<VAR>G : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>μ : Measure G<VAR>f✝ : G → E<VAR>g✝ : G<VAR>inst✝² : Group G<VAR>inst✝¹ : MeasurableMul G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>f : G → E<VAR>g : G<GOAL>∫ (x : G), f (g * x) ∂μ = ∫ (x : G), f x ∂μ
<VAR>𝕜 : Type u_1<VAR>M : Type u_2<VAR>α : Type u_3<VAR>G : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>μ : Measure G<VAR>f✝ : G → E<VAR>g✝ : G<VAR>inst✝² : Group G<VAR>inst✝¹ : MeasurableMul G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>f : G → E<VAR>g : G<VAR>h_mul : MeasurableEmbedding fun x => g * x<GOAL>∫ (x : G), f (g * x) ∂μ = ∫ (x : G), f x ∂μ
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : NormedSpace 𝕜 E'<VAR>F : Type u_4<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>inst✝¹¹ : TopologicalSpace H<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>G : Type u_7<VAR>inst✝⁹ : TopologicalSpace G<VAR>G' : Type u_8<VAR>inst✝⁸ : TopologicalSpace G'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>J : ModelWithCorners 𝕜 F G<VAR>J' : ModelWithCorners 𝕜 F G'<VAR>M : Type u_9<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>M' : Type u_10<VAR>inst✝⁵ : TopologicalSpace M'<VAR>inst✝⁴ : ChartedSpace H' M'<VAR>N : Type u_11<VAR>inst✝³ : TopologicalSpace N<VAR>inst✝² : ChartedSpace G N<VAR>N' : Type u_12<VAR>inst✝¹ : TopologicalSpace N'<VAR>inst✝ : ChartedSpace G' N'<VAR>n : ℕ∞<VAR>e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, E')⟯ E'<VAR>x : M<GOAL>(extChartAt (I.transDiffeomorph e) x).target = ⇑e.symm ⁻¹' (extChartAt I x).target
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : NormedSpace 𝕜 E'<VAR>F : Type u_4<VAR>inst✝¹³ : NormedAddCommGroup F<VAR>inst✝¹² : NormedSpace 𝕜 F<VAR>H : Type u_5<VAR>inst✝¹¹ : TopologicalSpace H<VAR>H' : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace H'<VAR>G : Type u_7<VAR>inst✝⁹ : TopologicalSpace G<VAR>G' : Type u_8<VAR>inst✝⁸ : TopologicalSpace G'<VAR>I : ModelWithCorners 𝕜 E H<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>J : ModelWithCorners 𝕜 F G<VAR>J' : ModelWithCorners 𝕜 F G'<VAR>M : Type u_9<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>M' : Type u_10<VAR>inst✝⁵ : TopologicalSpace M'<VAR>inst✝⁴ : ChartedSpace H' M'<VAR>N : Type u_11<VAR>inst✝³ : TopologicalSpace N<VAR>inst✝² : ChartedSpace G N<VAR>N' : Type u_12<VAR>inst✝¹ : TopologicalSpace N'<VAR>inst✝ : ChartedSpace G' N'<VAR>n : ℕ∞<VAR>e : E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, E')⟯ E'<VAR>x : M<GOAL>⇑e.symm ⁻¹' range ↑I ∩ ↑I.symm ∘ ⇑e.symm ⁻¹' (chartAt H x).target = ⇑e.symm ⁻¹' range ↑I ∩ (fun x => ↑I.symm (e.symm x)) ⁻¹' (chartAt H x).target
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : DecidableEq n<VAR>R : Type u_2<VAR>K : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Field K<VAR>inst✝ : Fintype m<VAR>A : Matrix m m K<GOAL>(LinearIndependent K fun i => Aᵀ i) ↔ IsUnit A
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>f : α →₀ ℕ<VAR>g : α → β<GOAL>Multiset.map g (toMultiset f) = toMultiset (mapDomain g f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>f : α →₀ ℕ<VAR>g : α → β<GOAL>Multiset.map g (toMultiset 0) = toMultiset (mapDomain g 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>f : α →₀ ℕ<VAR>g : α → β<GOAL>∀ (a : α) (b : ℕ) (f : α →₀ ℕ), a ∉ f.support → b ≠ 0 → Multiset.map g (toMultiset f) = toMultiset (mapDomain g f) → Multiset.map g (toMultiset (single a b + f)) = toMultiset (mapDomain g (single a b + f))
<VAR>α : Type u_1<VAR>G : SimpleGraph α<VAR>c : G.Coloring Bool<VAR>u v : α<VAR>p : G.Walk u v<GOAL>Even p.length ↔ (c u = true ↔ c v = true)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>s : Set (Set A)<VAR>hsn : s.Nonempty<VAR>hs : DirectedOn (fun x x_1 => x ⊆ x_1) s<VAR>h : ∀ a ∈ s, AlgebraicIndependent R Subtype.val<GOAL>AlgebraicIndependent R Subtype.val
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>s : Set (Set A)<VAR>hsn : s.Nonempty<VAR>hs : DirectedOn (fun x x_1 => x ⊆ x_1) s<VAR>h : ∀ a ∈ s, AlgebraicIndependent R Subtype.val<VAR>this : Nonempty ↑s := Nonempty.to_subtype hsn<GOAL>AlgebraicIndependent R Subtype.val
<VAR>b c d : ℝ≥0∞<VAR>r p q a : ℝ≥0<VAR>hz : ↑a ≠ 0<GOAL>↑a / 2 < ↑a
<VAR>b c d : ℝ≥0∞<VAR>r p q a : ℝ≥0<VAR>hz : a ≠ 0<GOAL>↑a / 2 < ↑a
<VAR>b c d : ℝ≥0∞<VAR>r p q a : ℝ≥0<VAR>hz : a ≠ 0<GOAL>a / 2 < a
<VAR>b c d : ℝ≥0∞<VAR>r p q a : ℝ≥0<VAR>hz : a ≠ 0<GOAL>2 ≠ 0
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>r : Finset (α × γ)<VAR>s : Finset γ<VAR>t : γ → Finset α<VAR>h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2<VAR>f : α × γ → β<GOAL>∏ p ∈ r, f p = ∏ c ∈ s, ∏ a ∈ t c, f (a, c)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>r : Finset (α × γ)<VAR>s : Finset γ<VAR>t : γ → Finset α<VAR>h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2<VAR>f : α × γ → β<GOAL>∏ p ∈ r, f p = ∏ x ∈ s.sigma t, f (x.snd, x.fst)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝²³ : CommRing R<VAR>inst✝²² : CommRing S<VAR>inst✝²¹ : CommRing T<VAR>inst✝²⁰ : Algebra R S<VAR>inst✝¹⁹ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝¹⁸ : Field K<VAR>inst✝¹⁷ : Field L<VAR>inst✝¹⁶ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝¹⁵ : Fintype ι<VAR>F : Type u_6<VAR>inst✝¹⁴ : Field F<VAR>inst✝¹³ : Algebra R L<VAR>inst✝¹² : Algebra L F<VAR>inst✝¹¹ : Algebra R F<VAR>inst✝¹⁰ : IsScalarTower R L F<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : CommRing B<VAR>inst✝⁷ : Algebra A B<VAR>inst✝⁶ : CommRing C<VAR>inst✝⁵ : Algebra A C<VAR>E : Type z<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra K E<VAR>inst✝² : Module.Finite K L<VAR>inst✝¹ : Algebra.IsSeparable K L<VAR>inst✝ : IsAlgClosed E<VAR>b : κ → L<VAR>pb : PowerBasis K L<VAR>i j : κ<GOAL>(traceMatrix K b).map (⇑(algebraMap K E)) i j = (embeddingsMatrix K E b * (embeddingsMatrix K E b)ᵀ) i j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a✝ b c d : G<VAR>n✝ : ℤ<VAR>a : G<VAR>m n : ℤ<GOAL>a ^ (m - n) = a ^ m * (a ^ n)⁻¹
<VAR>a : Bool<VAR>m : ℤ<VAR>b : Bool<VAR>n : ℤ<GOAL>(bit a m).lor (bit b n) = bit (a || b) (m.lor n)
<VAR>𝕜 : Type u_1<VAR>M : Type u_2<VAR>α : Type u_3<VAR>G : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>μ : Measure G<VAR>f✝ : G → E<VAR>g✝ : G<VAR>inst✝² : Group G<VAR>inst✝¹ : MeasurableMul G<VAR>inst✝ : μ.IsMulRightInvariant<VAR>f : G → E<VAR>g : G<GOAL>∫ (x : G), f (x / g) ∂μ = ∫ (x : G), f x ∂μ
<VAR>𝕜 : Type u_1<VAR>M : Type u_2<VAR>α : Type u_3<VAR>G : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>μ : Measure G<VAR>f✝ : G → E<VAR>g✝ : G<VAR>inst✝² : Group G<VAR>inst✝¹ : MeasurableMul G<VAR>inst✝ : μ.IsMulRightInvariant<VAR>f : G → E<VAR>g : G<GOAL>∫ (x : G), f (x * g⁻¹) ∂μ = ∫ (x : G), f x ∂μ
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type w<VAR>ι' : Type w'<VAR>inst✝ : StrongRankCondition R<VAR>v : ι → M<VAR>hv : LinearIndependent R v<GOAL>Module.rank R ↥(span R (range v)) = #↑(range v)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type w<VAR>ι' : Type w'<VAR>inst✝ : StrongRankCondition R<VAR>v : ι → M<VAR>hv : LinearIndependent R v<VAR>this : Nontrivial R<GOAL>Module.rank R ↥(span R (range v)) = #↑(range v)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ✝ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ✝<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f✝ f' : α → β → γ✝<VAR>g✝ g'✝ : α → β → γ✝ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u✝ u' : Finset γ✝<VAR>a a' : α<VAR>b b' : β<VAR>c : γ✝<VAR>γ : Type u_14<VAR>u : Finset γ<VAR>f : α → δ → ε<VAR>g : β → γ → δ<VAR>f₁ : α → β → β'<VAR>f₂ : α → γ → γ'<VAR>g' : β' → γ' → ε<VAR>h_distrib : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)<GOAL>image2 f (↑s) (image2 g ↑t ↑u) ⊆ image2 g' (image2 f₁ ↑s ↑t) (image2 f₂ ↑s ↑u)
<VAR>R : Type u<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<VAR>toFinsupp✝ : R[ℕ]<GOAL>(erase n { toFinsupp := toFinsupp✝ }).toFinsupp = Finsupp.erase n { toFinsupp := toFinsupp✝ }.toFinsupp
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝¹ : CanonicallyOrderedCommSemiring α<VAR>b c d : α<VAR>inst✝ : Nontrivial α<VAR>k : α<GOAL>0 < 2 * k + 1
<VAR>i : (nim 1).RightMoves<GOAL>toRightMovesNim.symm i = ⟨0, ⋯⟩
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.4862, u_2} D<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>inst✝¹ : S.HasHomology<VAR>inst✝ : HasZeroObject C<GOAL>S.Exact ↔ Nonempty (S.homology ≅ 0)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.4862, u_2} D<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>inst✝¹ : S.HasHomology<VAR>inst✝ : HasZeroObject C<GOAL>IsZero S.homology ↔ Nonempty (S.homology ≅ 0)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>N : Type u_5<VAR>P : Type u_6<VAR>inst✝¹ : Group N<VAR>inst✝ : Group P<VAR>K : Subgroup G<VAR>f : G →* N<VAR>s : Set N<VAR>x : G<VAR>hx : x ∈ ⇑f ⁻¹' s<GOAL>x ∈ ↑(comap f (closure s))