ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<VAR>s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))<VAR>s₂ : ∀ (r : { x // x ∈ s }), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤<VAR>sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)<VAR>x : S<GOAL>x ∈ ⨆ x, Submodule.span R ↑(sf x)
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<VAR>s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))<VAR>s₂ : ∀ (r : { x // x ∈ s }), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤<VAR>sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)<VAR>x : S<GOAL>∀ (r : ↑↑s), ∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<VAR>s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))<VAR>s₂ : ∀ (r : { x // x ∈ s }), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤<VAR>sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)<VAR>x : S<VAR>r : ↑↑s<GOAL>∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<VAR>s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))<VAR>s₂ : ∀ (r : { x // x ∈ s }), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤<VAR>sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)<VAR>x : S<VAR>r : ↑↑s<VAR>n₁ : ℕ<VAR>hn₁ : ⟨(fun x => ↑r ^ x) n₁, ⋯⟩ • (algebraMap S (Localization.Away (f ↑r))) x ∈ Submodule.span R ↑(s₁ r)<GOAL>∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<VAR>s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))<VAR>s₂ : ∀ (r : { x // x ∈ s }), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤<VAR>sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)<VAR>x : S<VAR>r : ↑↑s<VAR>n₁ : ℕ<VAR>hn₁ : ⟨↑r ^ n₁, ⋯⟩ • (algebraMap S (Localization.Away (f ↑r))) x ∈ Submodule.span R ↑(s₁ r)<GOAL>∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<VAR>s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))<VAR>s₂ : ∀ (r : { x // x ∈ s }), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤<VAR>sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)<VAR>x : S<VAR>r : ↑↑s<VAR>n₁ : ℕ<VAR>hn₁ : (algebraMap S (Localization.Away (f ↑r))) ((algebraMap R S) ↑⟨↑r ^ n₁, ⋯⟩ * x) ∈ Submodule.span R ↑(s₁ r)<GOAL>∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<VAR>s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))<VAR>s₂ : ∀ (r : { x // x ∈ s }), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤<VAR>sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)<VAR>x : S<VAR>r : ↑↑s<VAR>n₁ : ℕ<VAR>hn₁ : (algebraMap S (Localization.Away (f ↑r))) ((algebraMap R S) ↑⟨↑r ^ n₁, ⋯⟩ * x) ∈ Submodule.span R ↑(s₁ r)<VAR>n₂ : ℕ<VAR>hn₂ : ⟨(fun x => ↑r ^ x) n₂, ⋯⟩ • ((algebraMap R S) ↑⟨↑r ^ n₁, ⋯⟩ * x) ∈ Submodule.span R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (s₁ r))<GOAL>∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<VAR>s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))<VAR>s₂ : ∀ (r : { x // x ∈ s }), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤<VAR>sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)<VAR>x : S<VAR>r : ↑↑s<VAR>n₁ : ℕ<VAR>hn₁ : (algebraMap S (Localization.Away (f ↑r))) ((algebraMap R S) ↑⟨↑r ^ n₁, ⋯⟩ * x) ∈ Submodule.span R ↑(s₁ r)<VAR>n₂ : ℕ<VAR>hn₂ : ↑r ^ (n₂ + n₁) • x ∈ Submodule.span R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (s₁ r))<GOAL>∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<VAR>s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))<VAR>s₂ : ∀ (r : { x // x ∈ s }), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤<VAR>sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)<VAR>x : S<VAR>r : ↑↑s<VAR>n₁ : ℕ<VAR>hn₁ : (algebraMap S (Localization.Away (f ↑r))) ((algebraMap R S) ↑⟨↑r ^ n₁, ⋯⟩ * x) ∈ Submodule.span R ↑(s₁ r)<VAR>n₂ : ℕ<VAR>hn₂ : ↑r ^ (n₂ + n₁) • x ∈ Submodule.span R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ((algebraMap R S) ↑r)) (s₁ r))<GOAL>∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)
<VAR>R✝ S✝ : Type u<VAR>inst✝⁷ : CommRing R✝<VAR>inst✝⁶ : CommRing S✝<VAR>M : Submonoid R✝<VAR>N : Submonoid S✝<VAR>R' S' : Type u<VAR>inst✝⁵ : CommRing R'<VAR>inst✝⁴ : CommRing S'<VAR>f✝ : R✝ →+* S✝<VAR>inst✝³ : Algebra R✝ R'<VAR>inst✝² : Algebra S✝ S'<VAR>R S : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>s : Finset R<VAR>hs : Ideal.span ↑s = ⊤<VAR>this✝² : Algebra R S := f.toAlgebra<VAR>this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) := fun r => (Localization.awayMap f ↑r).toAlgebra<VAR>this✝ : ∀ (r : { x // x ∈ s }), IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))<VAR>this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))<VAR>s₁ : (r : { x // x ∈ s }) → Finset (Localization.Away (f ↑r))<VAR>s₂ : ∀ (r : { x // x ∈ s }), Submodule.span (Localization.Away ↑r) ↑(s₁ r) = ⊤<VAR>sf : { x // x ∈ s } → Finset S := fun x => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f ↑x)) (s₁ x)<VAR>x : S<VAR>r : ↑↑s<VAR>n₁ : ℕ<VAR>hn₁ : (algebraMap S (Localization.Away (f ↑r))) ((algebraMap R S) ↑⟨↑r ^ n₁, ⋯⟩ * x) ∈ Submodule.span R ↑(s₁ r)<VAR>n₂ : ℕ<VAR>hn₂ : ↑r ^ (n₂ + n₁) • x ∈ Submodule.span R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.powers ((algebraMap R S) ↑r)) (s₁ r))<GOAL>↑r ^ (n₂ + n₁) • x ∈ ⨆ x, Submodule.span R ↑(sf x)
<VAR>m n✝ n : ℕ<VAR>a : ZMod n<GOAL>-a = a ↔ a = 0 ∨ 2 * a.val = n
<VAR>m n✝ n : ℕ<VAR>a : ZMod n<GOAL>2 * a = 0 ↔ a = 0 ∨ 2 * a.val = n
<VAR>m n n✝ : ℕ<VAR>a : ZMod (n✝ + 1)<GOAL>2 * a = 0 ↔ a = 0 ∨ 2 * a.val = n✝ + 1
<VAR>m n n✝ : ℕ<VAR>a : ZMod (n✝ + 1)<GOAL>n✝ + 1 ∣ 2 * a.val ↔ a = 0 ∨ 2 * a.val = n✝ + 1
<VAR>X✝ : LocallyRingedSpace<VAR>U : TopCat<VAR>X : LocallyRingedSpace<VAR>f : U ⟶ X.toTopCat<VAR>h : OpenEmbedding ⇑f<VAR>x : ↑↑(X.restrict h).toPresheafedSpace<GOAL>LocalRing ↑((X.restrict h).presheaf.stalk x)
<VAR>X✝ : LocallyRingedSpace<VAR>U : TopCat<VAR>X : LocallyRingedSpace<VAR>f : U ⟶ X.toTopCat<VAR>h : OpenEmbedding ⇑f<VAR>x : ↑↑(X.restrict h).toPresheafedSpace<GOAL>↑(X.presheaf.stalk (f x)) ≃+* ↑((X.restrict h).presheaf.stalk x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : OrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>v : 𝕜<VAR>q : E<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 < w i<VAR>h₁ : ∑ i ∈ t, w i = 1<VAR>hmem : ∀ i ∈ t, p i ∈ s<VAR>h_eq : f (∑ i ∈ t, w i • p i) ≤ ∑ i ∈ t, w i • f (p i)<GOAL>∀ ⦃j : ι⦄, j ∈ t → ∀ ⦃k : ι⦄, k ∈ t → p j = p k
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : OrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>v : 𝕜<VAR>q : E<VAR>hf : StrictConcaveOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 < w i<VAR>h₁ : ∑ i ∈ t, w i = 1<VAR>hmem : ∀ i ∈ t, p i ∈ s<VAR>h_eq : f (∑ i ∈ t, w i • p i) ≤ ∑ i ∈ t, w i • f (p i)<VAR>this : ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k<GOAL>False
<VAR>R : 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>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>q : Type u_12<VAR>r : Type u_13<VAR>l' : Type u_14<VAR>m' : Type u_15<VAR>n' : Type u_16<VAR>p' : Type u_17<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing α<VAR>inst✝⁶ : CommRing β<VAR>inst✝⁵ : Algebra R α<VAR>inst✝⁴ : Algebra R β<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : DecidableEq n<VAR>A : Matrix m m α<VAR>B : Matrix n n β<GOAL>(kroneckerMap (tmul R) A B).det = (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)
<VAR>R : 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>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>q : Type u_12<VAR>r : Type u_13<VAR>l' : Type u_14<VAR>m' : Type u_15<VAR>n' : Type u_16<VAR>p' : Type u_17<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing α<VAR>inst✝⁶ : CommRing β<VAR>inst✝⁵ : Algebra R α<VAR>inst✝⁴ : Algebra R β<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : DecidableEq n<VAR>A : Matrix m m α<VAR>B : Matrix n n β<GOAL>(A.map fun a => ((mk R α β) a) 1).det ^ Fintype.card n * (B.map fun b => ((mk R α β) 1) b).det ^ Fintype.card m = (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)
<VAR>R : 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>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>q : Type u_12<VAR>r : Type u_13<VAR>l' : Type u_14<VAR>m' : Type u_15<VAR>n' : Type u_16<VAR>p' : Type u_17<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing α<VAR>inst✝⁶ : CommRing β<VAR>inst✝⁵ : Algebra R α<VAR>inst✝⁴ : Algebra R β<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : DecidableEq n<VAR>A : Matrix m m α<VAR>B : Matrix n n β<GOAL>(A.map fun a => includeLeft a).det ^ Fintype.card n * (B.map fun b => includeRight b).det ^ Fintype.card m = (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)
<VAR>R : 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>l : Type u_8<VAR>m : Type u_9<VAR>n : Type u_10<VAR>p : Type u_11<VAR>q : Type u_12<VAR>r : Type u_13<VAR>l' : Type u_14<VAR>m' : Type u_15<VAR>n' : Type u_16<VAR>p' : Type u_17<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing α<VAR>inst✝⁶ : CommRing β<VAR>inst✝⁵ : Algebra R α<VAR>inst✝⁴ : Algebra R β<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : DecidableEq n<VAR>A : Matrix m m α<VAR>B : Matrix n n β<GOAL>includeLeft A.det ^ Fintype.card n * includeRight B.det ^ Fintype.card m = (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>a : ℝ<GOAL>ContinuousAt (fun p => p.1 + p.2) (⊥, ↑a)
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>a : ℝ<GOAL>∀ (x : ℝ), ∀ᶠ (a : EReal × EReal) in 𝓝 (⊥, ↑a), a.1 + a.2 < ↑x
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>a r : ℝ<VAR>x✝ : EReal × EReal<VAR>h : x✝.1 < ↑(r - (a + 1)) ∧ x✝.2 < ↑(a + 1)<GOAL>x✝.1 + x✝.2 < ↑r
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.100731, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>n : ℤ<GOAL>(mappingCone φ).d (n - 1) n ≫ (snd φ).v n n ⋯ = (↑(fst φ)).v (n - 1) n ⋯ ≫ φ.f n + (snd φ).v (n - 1) (n - 1) ⋯ ≫ G.d (n - 1) n
<VAR>u✝ : Lean.Level<VAR>arg : Q(Type u✝)<VAR>sα✝ : Q(CommSemiring «$arg»)<VAR>u : Lean.Level<VAR>α : Q(Type u)<VAR>sα : Q(CommSemiring «$α»)<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>a a' a₁✝ a₂✝ a₃ b b' b₁ b₂ b₃ c₁ c₂ a₁ : R<VAR>a₂ : ℕ<GOAL>a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * (a₃ * b)
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>z : N<GOAL>f.toMap (f.sec z).1 * ↑((IsUnit.liftRight (f.toMap.restrict S) ⋯) (f.sec z).2)⁻¹ = z
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>hQ : W'.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z = 0<GOAL>W'.add P Q = -(Q x * P z) • P
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f g : Perm α<VAR>h : f.cycleFactorsFinset = g.cycleFactorsFinset<GOAL>f = g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f g : Perm α<VAR>h : f.cycleFactorsFinset = g.cycleFactorsFinset<GOAL>f.cycleFactorsFinset.noncommProd id ⋯ = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>E : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>C : ℝ≥0∞<VAR>f : Set α → ℝ≥0∞<VAR>hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → f s ≤ C<VAR>h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ n, S n) ≤ ⨆ n, f (S n)<VAR>S : ℕ → Set α := spanningSets (μ.trim hm)<GOAL>f univ ≤ C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>E : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>C : ℝ≥0∞<VAR>f : Set α → ℝ≥0∞<VAR>hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → f s ≤ C<VAR>h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ n, S n) ≤ ⨆ n, f (S n)<VAR>S : ℕ → Set α := spanningSets (μ.trim hm)<VAR>hS_mono : Monotone S<GOAL>f univ ≤ C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>E : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>C : ℝ≥0∞<VAR>f : Set α → ℝ≥0∞<VAR>hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → f s ≤ C<VAR>h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ n, S n) ≤ ⨆ n, f (S n)<VAR>S : ℕ → Set α := spanningSets (μ.trim hm)<VAR>hS_mono : Monotone S<VAR>hS_meas : ∀ (n : ℕ), MeasurableSet (S n)<GOAL>f univ ≤ C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>E : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>C : ℝ≥0∞<VAR>f : Set α → ℝ≥0∞<VAR>hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → f s ≤ C<VAR>h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ n, S n) ≤ ⨆ n, f (S n)<VAR>S : ℕ → Set α := spanningSets (μ.trim hm)<VAR>hS_mono : Monotone S<VAR>hS_meas : ∀ (n : ℕ), MeasurableSet (S n)<GOAL>f (⋃ i, spanningSets (μ.trim hm) i) ≤ C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>E : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>C : ℝ≥0∞<VAR>f : Set α → ℝ≥0∞<VAR>hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → f s ≤ C<VAR>h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ n, S n) ≤ ⨆ n, f (S n)<VAR>S : ℕ → Set α := spanningSets (μ.trim hm)<VAR>hS_mono : Monotone S<VAR>hS_meas : ∀ (n : ℕ), MeasurableSet (S n)<GOAL>⨆ n, f (S n) ≤ C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>E : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>C : ℝ≥0∞<VAR>f : Set α → ℝ≥0∞<VAR>hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → f s ≤ C<VAR>h_F_lim : ∀ (S : ℕ → Set α), (∀ (n : ℕ), MeasurableSet (S n)) → Monotone S → f (⋃ n, S n) ≤ ⨆ n, f (S n)<VAR>S : ℕ → Set α := spanningSets (μ.trim hm)<VAR>hS_mono : Monotone S<VAR>hS_meas : ∀ (n : ℕ), MeasurableSet (S n)<VAR>n : ℕ<GOAL>μ (S n) ≠ ⊤
<VAR>α : Type u<VAR>M✝ : Type u_1<VAR>N : Type u_2<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>u : Mˣ<VAR>a : M<VAR>x✝ : IsUnit (↑u * a)<VAR>v : Mˣ<VAR>hv : ↑v = ↑u * a<GOAL>IsUnit a
<VAR>α : Type u<VAR>M✝ : Type u_1<VAR>N : Type u_2<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>u : Mˣ<VAR>a : M<VAR>x✝ : IsUnit (↑u * a)<VAR>v : Mˣ<VAR>hv : ↑v = ↑u * a<VAR>this : IsUnit (↑u⁻¹ * (↑u * a))<GOAL>IsUnit a
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : NormedSpace 𝕜 H<VAR>𝕝 : Type u_7<VAR>inst✝³ : NontriviallyNormedField 𝕝<VAR>inst✝² : NormedAlgebra 𝕜 𝕝<VAR>A : Type u_8<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>z : 𝕝<VAR>hz : z ≠ 0<VAR>f1 : 𝕝 → 𝕝 := fun a => 1 / z * a<VAR>f2 : 𝕝 → 𝕝 := fun b => (1 - b)⁻¹<VAR>f3 : 𝕝 → 𝕝 := fun c => 1 - c / z<GOAL>AnalyticAt 𝕜 Inv.inv z