ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>inst✝ : IsFiltered J<VAR>j₁ : J<VAR>y : ↑(F.obj j₁)<VAR>j₂ : J<VAR>x : ↑(F.obj j₂)<VAR>j₃ : J<VAR>y' : ↑(F.obj j₃)<VAR>l : J<VAR>f : ⟨j₁, y⟩.fst ⟶ l<VAR>g : ⟨j₃, y'⟩.fst ⟶ l<VAR>hfg : (F.map f) y = (F.map g) y'<VAR>s : J<VAR>α : IsFiltered.max j₂ j₁ ⟶ s<VAR>β : l ⟶ s<VAR>γ : IsFiltered.max j₂ j₃ ⟶ s<VAR>h₁ : IsFiltered.rightToMax j₂ j₁ ≫ α = f ≫ β<VAR>h₂ : IsFiltered.leftToMax j₂ j₁ ≫ α = IsFiltered.leftToMax j₂ j₃ ≫ γ<VAR>h₃ : IsFiltered.rightToMax j₂ j₃ ≫ γ = g ≫ β<GOAL>∃ k f g, (F.map f) ⟨IsFiltered.max ⟨j₂, x⟩.fst ⟨j₁, y⟩.fst, (F.map (IsFiltered.leftToMax ⟨j₂, x⟩.fst ⟨j₁, y⟩.fst)) ⟨j₂, x⟩.snd * (F.map (IsFiltered.rightToMax ⟨j₂, x⟩.fst ⟨j₁, y⟩.fst)) ⟨j₁, y⟩.snd⟩.snd = (F.map g) ⟨IsFiltered.max ⟨j₂, x⟩.fst ⟨j₃, y'⟩.fst, (F.map (IsFiltered.leftToMax ⟨j₂, x⟩.fst ⟨j₃, y'⟩.fst)) ⟨j₂, x⟩.snd * (F.map (IsFiltered.rightToMax ⟨j₂, x⟩.fst ⟨j₃, y'⟩.fst)) ⟨j₃, y'⟩.snd⟩.snd
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>inst✝ : IsFiltered J<VAR>j₁ : J<VAR>y : ↑(F.obj j₁)<VAR>j₂ : J<VAR>x : ↑(F.obj j₂)<VAR>j₃ : J<VAR>y' : ↑(F.obj j₃)<VAR>l : J<VAR>f : ⟨j₁, y⟩.fst ⟶ l<VAR>g : ⟨j₃, y'⟩.fst ⟶ l<VAR>hfg : (F.map f) y = (F.map g) y'<VAR>s : J<VAR>α : IsFiltered.max j₂ j₁ ⟶ s<VAR>β : l ⟶ s<VAR>γ : IsFiltered.max j₂ j₃ ⟶ s<VAR>h₁ : IsFiltered.rightToMax j₂ j₁ ≫ α = f ≫ β<VAR>h₂ : IsFiltered.leftToMax j₂ j₁ ≫ α = IsFiltered.leftToMax j₂ j₃ ≫ γ<VAR>h₃ : IsFiltered.rightToMax j₂ j₃ ≫ γ = g ≫ β<GOAL>(F.map α) ⟨IsFiltered.max ⟨j₂, x⟩.fst ⟨j₁, y⟩.fst, (F.map (IsFiltered.leftToMax ⟨j₂, x⟩.fst ⟨j₁, y⟩.fst)) ⟨j₂, x⟩.snd * (F.map (IsFiltered.rightToMax ⟨j₂, x⟩.fst ⟨j₁, y⟩.fst)) ⟨j₁, y⟩.snd⟩.snd = (F.map γ) ⟨IsFiltered.max ⟨j₂, x⟩.fst ⟨j₃, y'⟩.fst, (F.map (IsFiltered.leftToMax ⟨j₂, x⟩.fst ⟨j₃, y'⟩.fst)) ⟨j₂, x⟩.snd * (F.map (IsFiltered.rightToMax ⟨j₂, x⟩.fst ⟨j₃, y'⟩.fst)) ⟨j₃, y'⟩.snd⟩.snd
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>inst✝ : IsFiltered J<VAR>j₁ : J<VAR>y : ↑(F.obj j₁)<VAR>j₂ : J<VAR>x : ↑(F.obj j₂)<VAR>j₃ : J<VAR>y' : ↑(F.obj j₃)<VAR>l : J<VAR>f : ⟨j₁, y⟩.fst ⟶ l<VAR>g : ⟨j₃, y'⟩.fst ⟶ l<VAR>hfg : (F.map f) y = (F.map g) y'<VAR>s : J<VAR>α : IsFiltered.max j₂ j₁ ⟶ s<VAR>β : l ⟶ s<VAR>γ : IsFiltered.max j₂ j₃ ⟶ s<VAR>h₁ : IsFiltered.rightToMax j₂ j₁ ≫ α = f ≫ β<VAR>h₂ : IsFiltered.leftToMax j₂ j₁ ≫ α = IsFiltered.leftToMax j₂ j₃ ≫ γ<VAR>h₃ : IsFiltered.rightToMax j₂ j₃ ≫ γ = g ≫ β<GOAL>(F.map α) ((F.map (IsFiltered.leftToMax j₂ j₁)) x * (F.map (IsFiltered.rightToMax j₂ j₁)) y) = (F.map γ) ((F.map (IsFiltered.leftToMax j₂ j₃)) x * (F.map (IsFiltered.rightToMax j₂ j₃)) y')
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>inst✝ : IsFiltered J<VAR>j₁ : J<VAR>y : ↑(F.obj j₁)<VAR>j₂ : J<VAR>x : ↑(F.obj j₂)<VAR>j₃ : J<VAR>y' : ↑(F.obj j₃)<VAR>l : J<VAR>f : ⟨j₁, y⟩.fst ⟶ l<VAR>g : ⟨j₃, y'⟩.fst ⟶ l<VAR>hfg : (F.map f) y = (F.map g) y'<VAR>s : J<VAR>α : IsFiltered.max j₂ j₁ ⟶ s<VAR>β : l ⟶ s<VAR>γ : IsFiltered.max j₂ j₃ ⟶ s<VAR>h₁ : IsFiltered.rightToMax j₂ j₁ ≫ α = f ≫ β<VAR>h₂ : IsFiltered.leftToMax j₂ j₁ ≫ α = IsFiltered.leftToMax j₂ j₃ ≫ γ<VAR>h₃ : IsFiltered.rightToMax j₂ j₃ ≫ γ = g ≫ β<GOAL>(F.map α) ((F.map (IsFiltered.leftToMax j₂ j₁)) x) * (F.map α) ((F.map (IsFiltered.rightToMax j₂ j₁)) y) = (F.map γ) ((F.map (IsFiltered.leftToMax j₂ j₃)) x) * (F.map γ) ((F.map (IsFiltered.rightToMax j₂ j₃)) y')
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>inst✝ : IsFiltered J<VAR>j₁ : J<VAR>y : ↑(F.obj j₁)<VAR>j₂ : J<VAR>x : ↑(F.obj j₂)<VAR>j₃ : J<VAR>y' : ↑(F.obj j₃)<VAR>l : J<VAR>f : ⟨j₁, y⟩.fst ⟶ l<VAR>g : ⟨j₃, y'⟩.fst ⟶ l<VAR>hfg : (F.map f) y = (F.map g) y'<VAR>s : J<VAR>α : IsFiltered.max j₂ j₁ ⟶ s<VAR>β : l ⟶ s<VAR>γ : IsFiltered.max j₂ j₃ ⟶ s<VAR>h₁ : IsFiltered.rightToMax j₂ j₁ ≫ α = f ≫ β<VAR>h₂ : IsFiltered.leftToMax j₂ j₁ ≫ α = IsFiltered.leftToMax j₂ j₃ ≫ γ<VAR>h₃ : IsFiltered.rightToMax j₂ j₃ ≫ γ = g ≫ β<GOAL>(F.map (IsFiltered.leftToMax j₂ j₁) ≫ F.map α) x * (F.map (IsFiltered.rightToMax j₂ j₁) ≫ F.map α) y = (F.map (IsFiltered.leftToMax j₂ j₃) ≫ F.map γ) x * (F.map (IsFiltered.rightToMax j₂ j₃) ≫ F.map γ) y'
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>inst✝ : IsFiltered J<VAR>j₁ : J<VAR>y : ↑(F.obj j₁)<VAR>j₂ : J<VAR>x : ↑(F.obj j₂)<VAR>j₃ : J<VAR>y' : ↑(F.obj j₃)<VAR>l : J<VAR>f : ⟨j₁, y⟩.fst ⟶ l<VAR>g : ⟨j₃, y'⟩.fst ⟶ l<VAR>hfg : (F.map f) y = (F.map g) y'<VAR>s : J<VAR>α : IsFiltered.max j₂ j₁ ⟶ s<VAR>β : l ⟶ s<VAR>γ : IsFiltered.max j₂ j₃ ⟶ s<VAR>h₁ : IsFiltered.rightToMax j₂ j₁ ≫ α = f ≫ β<VAR>h₂ : IsFiltered.leftToMax j₂ j₁ ≫ α = IsFiltered.leftToMax j₂ j₃ ≫ γ<VAR>h₃ : IsFiltered.rightToMax j₂ j₃ ≫ γ = g ≫ β<GOAL>(F.map (IsFiltered.leftToMax j₂ j₃) ≫ F.map γ) x * (F.map f ≫ F.map β) y = (F.map (IsFiltered.leftToMax j₂ j₃) ≫ F.map γ) x * (F.map g ≫ F.map β) y'
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra R L<VAR>inst✝ : IsLieAbelian L<VAR>ψ : Module.Dual R L<VAR>x y : L<GOAL>ψ.toFun ⁅x, y⁆ = ⁅ψ.toFun x, ψ.toFun y⁆
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>k r : ℕ<GOAL>t ∈ ∂ 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s ∧ s.card = t.card + 1
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 : Finset (Finset α)<VAR>s t✝ : Finset α<VAR>a : α<VAR>k r : ℕ<VAR>t : Finset α<VAR>x✝ : t ∈ 𝒜<VAR>hst : t✝ ⊆ t<GOAL>(t \ t✝).card = 1 ↔ t.card = t✝.card + 1
<VAR>R✝ : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>R : Type u_17<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : Fintype n<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype n'<VAR>inst✝² : Fintype m'<VAR>inst✝¹ : DecidableEq n'<VAR>inst✝ : DecidableEq m'<VAR>B : (n → R) →ₗ[R] (m → R) →ₗ[R] R<VAR>l : (n' → R) →ₗ[R] n → R<VAR>r : (m' → R) →ₗ[R] m → R<VAR>i : n'<VAR>j : m'<GOAL>(toMatrix₂' R) (B.compl₁₂ l r) i j = ((toMatrix' l)ᵀ * (toMatrix₂' R) B * toMatrix' r) i j
<VAR>R✝ : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>R : Type u_17<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : Fintype n<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype n'<VAR>inst✝² : Fintype m'<VAR>inst✝¹ : DecidableEq n'<VAR>inst✝ : DecidableEq m'<VAR>B : (n → R) →ₗ[R] (m → R) →ₗ[R] R<VAR>l : (n' → R) →ₗ[R] n → R<VAR>r : (m' → R) →ₗ[R] m → R<VAR>i : n'<VAR>j : m'<GOAL>(B (l ((stdBasis R (fun x => R) i) 1))) (r ((stdBasis R (fun x => R) j) 1)) = ∑ x : m, ∑ i_1 : n, of (fun i j => l ((stdBasis R (fun x => R) j) 1) i) i_1 i * (B ((stdBasis R (fun x => R) i_1) 1)) ((stdBasis R (fun x => R) x) 1) * of (fun i j => r ((stdBasis R (fun x => R) j) 1) i) x j
<VAR>R✝ : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>R : Type u_17<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : Fintype n<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype n'<VAR>inst✝² : Fintype m'<VAR>inst✝¹ : DecidableEq n'<VAR>inst✝ : DecidableEq m'<VAR>B : (n → R) →ₗ[R] (m → R) →ₗ[R] R<VAR>l : (n' → R) →ₗ[R] n → R<VAR>r : (m' → R) →ₗ[R] m → R<VAR>i : n'<VAR>j : m'<GOAL>(B (l ((stdBasis R (fun x => R) i) 1))) (r ((stdBasis R (fun x => R) j) 1)) = ∑ y : n, ∑ x : m, of (fun i j => l ((stdBasis R (fun x => R) j) 1) i) y i * (B ((stdBasis R (fun x => R) y) 1)) ((stdBasis R (fun x => R) x) 1) * of (fun i j => r ((stdBasis R (fun x => R) j) 1) i) x j
<VAR>R✝ : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>R : Type u_17<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : Fintype n<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype n'<VAR>inst✝² : Fintype m'<VAR>inst✝¹ : DecidableEq n'<VAR>inst✝ : DecidableEq m'<VAR>B : (n → R) →ₗ[R] (m → R) →ₗ[R] R<VAR>l : (n' → R) →ₗ[R] n → R<VAR>r : (m' → R) →ₗ[R] m → R<VAR>i : n'<VAR>j : m'<GOAL>(((Pi.basisFun R n).repr (l ((stdBasis R (fun x => R) i) 1))).sum fun i xi => ((Pi.basisFun R m).repr (r ((stdBasis R (fun x => R) j) 1))).sum fun j yj => xi •> yj •> (B ((Pi.basisFun R n) i)) ((Pi.basisFun R m) j)) = ∑ y : n, ∑ x : m, of (fun i j => l ((stdBasis R (fun x => R) j) 1) i) y i * (B ((stdBasis R (fun x => R) y) 1)) ((stdBasis R (fun x => R) x) 1) * of (fun i j => r ((stdBasis R (fun x => R) j) 1) i) x j
<VAR>R✝ : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>R : Type u_17<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : Fintype n<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype n'<VAR>inst✝² : Fintype m'<VAR>inst✝¹ : DecidableEq n'<VAR>inst✝ : DecidableEq m'<VAR>B : (n → R) →ₗ[R] (m → R) →ₗ[R] R<VAR>l : (n' → R) →ₗ[R] n → R<VAR>r : (m' → R) →ₗ[R] m → R<VAR>i : n'<VAR>j : m'<GOAL>(∑ i_1 : n, ((Pi.basisFun R m).repr (r ((stdBasis R (fun x => R) j) 1))).sum fun j yj => ((Pi.basisFun R n).repr (l ((stdBasis R (fun x => R) i) 1))) i_1 •> yj •> (B ((Pi.basisFun R n) i_1)) ((Pi.basisFun R m) j)) = ∑ y : n, ∑ x : m, of (fun i j => l ((stdBasis R (fun x => R) j) 1) i) y i * (B ((stdBasis R (fun x => R) y) 1)) ((stdBasis R (fun x => R) x) 1) * of (fun i j => r ((stdBasis R (fun x => R) j) 1) i) x j
<VAR>R✝ : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>R : Type u_17<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : Fintype n<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype n'<VAR>inst✝² : Fintype m'<VAR>inst✝¹ : DecidableEq n'<VAR>inst✝ : DecidableEq m'<VAR>B : (n → R) →ₗ[R] (m → R) →ₗ[R] R<VAR>l : (n' → R) →ₗ[R] n → R<VAR>r : (m' → R) →ₗ[R] m → R<VAR>i : n'<VAR>j : m'<GOAL>∀ (i : n), (((Pi.basisFun R m).repr (r ((stdBasis R (fun x => R) j) 1))).sum fun j yj => 0 •> yj •> (B ((Pi.basisFun R n) i)) ((Pi.basisFun R m) j)) = 0
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ z : K<GOAL>|im z / ‖z‖| ≤ 1
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ z : K<GOAL>|im z| / ‖z‖ ≤ 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<GOAL>(s ∩ {a}).Nonempty ↔ a ∈ s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x✝ : ∃ k, orderOf x = p ^ k<VAR>k : ℕ<VAR>hk : orderOf x = p ^ k<GOAL>x ^ p ^ k = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x✝ : ∃ m, x ^ p ^ m = 1<VAR>w✝ : ℕ<VAR>hm : x ^ p ^ w✝ = 1<GOAL>∃ k, orderOf x = p ^ k
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x✝ : ∃ m, x ^ p ^ m = 1<VAR>w✝ : ℕ<VAR>hm : x ^ p ^ w✝ = 1<VAR>k : ℕ<VAR>left✝ : k ≤ w✝<VAR>hk : orderOf x = p ^ k<GOAL>∃ k, orderOf x = p ^ k
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<GOAL>IsIso (toSpec 𝒜 f).val.base
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<GOAL>(toSpec 𝒜 f).val.base = (projIsoSpecTopComponent f_deg hm).hom
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasExt C<VAR>n : ℕ<VAR>X₁ X₂ : Cᵒᵖ<VAR>f : X₁ ⟶ X₂<VAR>Y₁ Y₂ : C<VAR>g : Y₁ ⟶ Y₂<VAR>α : ↑(((fun X => extFunctorObj (Opposite.unop X) n) X₁).obj Y₁)<GOAL>(AddCommGrp.ofHom (AddMonoidHom.mk' (fun α => (Ext.mk₀ f.unop).comp α ⋯) ⋯) ≫ AddCommGrp.ofHom ((Ext.mk₀ g).postcomp (Opposite.unop X₂) ⋯)) α = (AddCommGrp.ofHom ((Ext.mk₀ g).postcomp (Opposite.unop X₁) ⋯) ≫ AddCommGrp.ofHom (AddMonoidHom.mk' (fun α => (Ext.mk₀ f.unop).comp α ⋯) ⋯)) α
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasExt C<VAR>n : ℕ<VAR>X₁ X₂ : Cᵒᵖ<VAR>f : X₁ ⟶ X₂<VAR>Y₁ Y₂ : C<VAR>g : Y₁ ⟶ Y₂<VAR>α : ↑(((fun X => extFunctorObj (Opposite.unop X) n) X₁).obj Y₁)<GOAL>0 + n = n
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasExt C<VAR>n : ℕ<VAR>X₁ X₂ : Cᵒᵖ<VAR>f : X₁ ⟶ X₂<VAR>Y₁ Y₂ : C<VAR>g : Y₁ ⟶ Y₂<VAR>α : ↑(((fun X => extFunctorObj (Opposite.unop X) n) X₁).obj Y₁)<GOAL>n + 0 = n
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasExt C<VAR>n : ℕ<VAR>X₁ X₂ : Cᵒᵖ<VAR>f : X₁ ⟶ X₂<VAR>Y₁ Y₂ : C<VAR>g : Y₁ ⟶ Y₂<VAR>α : ↑(((fun X => extFunctorObj (Opposite.unop X) n) X₁).obj Y₁)<GOAL>0 + n + 0 = n
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasExt C<VAR>n : ℕ<VAR>X₁ X₂ X₃ : Cᵒᵖ<VAR>f : X₁ ⟶ X₂<VAR>f' : X₂ ⟶ X₃<VAR>Y : C<VAR>α : ↑(({ obj := fun X => extFunctorObj (Opposite.unop X) n, map := fun {X₁ X₂} f => { app := fun Y => AddCommGrp.ofHom (AddMonoidHom.mk' (fun α => (Ext.mk₀ f.unop).comp α ⋯) ⋯), naturality := ⋯ } }.obj X₁).obj Y)<GOAL>(Ext.mk₀ (f'.unop ≫ f.unop)).comp α ⋯ = (AddCommGrp.ofHom (AddMonoidHom.mk' (fun α => (Ext.mk₀ f.unop).comp α ⋯) ⋯) ≫ AddCommGrp.ofHom (AddMonoidHom.mk' (fun α => (Ext.mk₀ f'.unop).comp α ⋯) ⋯)) α
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasExt C<VAR>n : ℕ<VAR>X₁ X₂ X₃ : Cᵒᵖ<VAR>f : X₁ ⟶ X₂<VAR>f' : X₂ ⟶ X₃<VAR>Y : C<VAR>α : ↑(({ obj := fun X => extFunctorObj (Opposite.unop X) n, map := fun {X₁ X₂} f => { app := fun Y => AddCommGrp.ofHom (AddMonoidHom.mk' (fun α => (Ext.mk₀ f.unop).comp α ⋯) ⋯), naturality := ⋯ } }.obj X₁).obj Y)<GOAL>((Ext.mk₀ f'.unop).comp (Ext.mk₀ f.unop) ⋯).comp α ⋯ = (AddCommGrp.ofHom (AddMonoidHom.mk' (fun α => (Ext.mk₀ f.unop).comp α ⋯) ⋯) ≫ AddCommGrp.ofHom (AddMonoidHom.mk' (fun α => (Ext.mk₀ f'.unop).comp α ⋯) ⋯)) α
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasExt C<VAR>n : ℕ<VAR>X₁ X₂ X₃ : Cᵒᵖ<VAR>f : X₁ ⟶ X₂<VAR>f' : X₂ ⟶ X₃<VAR>Y : C<VAR>α : ↑(({ obj := fun X => extFunctorObj (Opposite.unop X) n, map := fun {X₁ X₂} f => { app := fun Y => AddCommGrp.ofHom (AddMonoidHom.mk' (fun α => (Ext.mk₀ f.unop).comp α ⋯) ⋯), naturality := ⋯ } }.obj X₁).obj Y)<GOAL>0 + n = n
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasExt C<VAR>n : ℕ<VAR>X₁ X₂ X₃ : Cᵒᵖ<VAR>f : X₁ ⟶ X₂<VAR>f' : X₂ ⟶ X₃<VAR>Y : C<VAR>α : ↑(({ obj := fun X => extFunctorObj (Opposite.unop X) n, map := fun {X₁ X₂} f => { app := fun Y => AddCommGrp.ofHom (AddMonoidHom.mk' (fun α => (Ext.mk₀ f.unop).comp α ⋯) ⋯), naturality := ⋯ } }.obj X₁).obj Y)<GOAL>0 + 0 + n = n
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>r : R<GOAL>log b r⁻¹ = -clog b r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>f : α →ₛ β<VAR>g : β → γ<VAR>s : Set γ<GOAL>↑(map g f) ⁻¹' s = ↑f ⁻¹' ↑(Finset.filter (fun b => g b ∈ s) f.range)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>f : α →ₛ β<VAR>g : β → γ<VAR>s : Set γ<GOAL>g ∘ ↑f ⁻¹' s = ↑f ⁻¹' (g ⁻¹' s)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>x : M<GOAL>x ∈ (p ⊔ p').toAddSubmonoid ↔ x ∈ p.toAddSubmonoid ⊔ p'.toAddSubmonoid
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>x : M<GOAL>(∃ y ∈ p, ∃ z ∈ p', y + z = x) ↔ ∃ y ∈ p.toAddSubmonoid, ∃ z ∈ p'.toAddSubmonoid, y + z = x
<VAR>s : Set Ordinal.{u}<VAR>a : Ordinal.{u}<GOAL>IsClosed s ↔ ∀ {o : Ordinal.{u}}, o ≠ 0 → ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s
<VAR>s : Set Ordinal.{u}<VAR>a : Ordinal.{u}<GOAL>(∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → sup f ∈ s) ↔ ∀ {o : Ordinal.{u}}, o ≠ 0 → ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s
<VAR>s : Set Ordinal.{u}<VAR>a : Ordinal.{u}<VAR>H : ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → sup f ∈ s<VAR>o : Ordinal.{u}<VAR>ho : o ≠ 0<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{u}<VAR>hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s<GOAL>∀ (i : (Quotient.out o).α), o.familyOfBFamily f i ∈ s
<VAR>s : Set Ordinal.{u}<VAR>a : Ordinal.{u}<VAR>H : ∀ {o : Ordinal.{u}}, o ≠ 0 → ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s<VAR>ι : Type u<VAR>hι : Nonempty ι<VAR>f : ι → Ordinal.{u}<VAR>hf : ∀ (i : ι), f i ∈ s<GOAL>sup f ∈ s
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c✝ : α<VAR>n : ℤ<VAR>a b c : α<GOAL>toIocDiv hp (a - c) b = toIocDiv hp a (b + c)
<VAR>M : Type u_1<VAR>inst✝³ : Mul M<VAR>inst✝² : Finite M<VAR>G : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>H : Subgroup G<GOAL>commProb ↥H ≤ commProb G * ↑H.index ^ 2
<VAR>M : Type u_1<VAR>inst✝³ : Mul M<VAR>inst✝² : Finite M<VAR>G : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>H : Subgroup G<GOAL>Nat.card { p // Commute p.1 p.2 } ≤ Nat.card { p // Commute p.1 p.2 }
<VAR>M : Type u_1<VAR>inst✝³ : Mul M<VAR>inst✝² : Finite M<VAR>G : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>H : Subgroup G<GOAL>↑(Nat.card G) ^ 2 ≠ 0
<VAR>M : Type u_1<VAR>inst✝³ : Mul M<VAR>inst✝² : Finite M<VAR>G : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>H : Subgroup G<GOAL>0 < ↑(Nat.card ↥H) ^ 2
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<VAR>hf : Inducing f<GOAL>IsCompact s ↔ IsCompact (f '' s)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<VAR>hf : Inducing f<VAR>hs : IsCompact (f '' s)<VAR>F : Filter X<VAR>F_ne_bot : F.NeBot<VAR>F_le : F ≤ 𝓟 s<GOAL>∃ x ∈ s, ClusterPt x F
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<VAR>hf : Inducing f<VAR>hs : IsCompact (f '' s)<VAR>F : Filter X<VAR>F_ne_bot : F.NeBot<VAR>F_le : F ≤ 𝓟 s<VAR>x : X<VAR>x_in : x ∈ s<VAR>hx : ClusterPt (f x) (map f F)<GOAL>∃ x ∈ s, ClusterPt x F
<VAR>a b p q : ℝ<VAR>h : p.IsConjExponent q<GOAL>p * q = p + q
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>n : ℕ<GOAL>invariants f ≤ invariants f^[n]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s✝ t s : SignedMeasure α<VAR>μ : Measure α<GOAL>(-s).singularPart μ = -s.singularPart μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s✝ t s : SignedMeasure α<VAR>μ : Measure α<VAR>h₁ : ((-s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure = (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure<GOAL>(-s).singularPart μ = -s.singularPart μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s✝ t s : SignedMeasure α<VAR>μ : Measure α<VAR>h₁ : ((-s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure = (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure<VAR>h₂ : ((-s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure = (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure<GOAL>(-s).singularPart μ = -s.singularPart μ
<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>x y z : α<VAR>hu : IsUnit x<GOAL>IsRelPrime y (x * z) ↔ IsRelPrime y z
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Monoid α<VAR>s t : Finset α<VAR>a : α<VAR>m n : ℕ<VAR>hn : n ≠ 0<GOAL>∅ ^ n = ∅
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝³ : Semiring R₁<VAR>inst✝² : Semiring R₂<VAR>inst✝¹ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>σ : R₁ →+* R₂<VAR>σ' : R₂ →+* R₁<VAR>inst✝ : RingHomInvPair σ σ'<VAR>x : R₁<GOAL>σ' (σ x) = x
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝³ : Semiring R₁<VAR>inst✝² : Semiring R₂<VAR>inst✝¹ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>σ : R₁ →+* R₂<VAR>σ' : R₂ →+* R₁<VAR>inst✝ : RingHomInvPair σ σ'<VAR>x : R₁<GOAL>(RingHom.id R₁) x = x
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : E × F → G<GOAL>IsBoundedBilinearMap 𝕜 fun p => p.1 * p.2
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : E × F → G<GOAL>IsBoundedBilinearMap 𝕜 fun p => p.1 • p.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableRel G.Adj<VAR>n : ℕ<VAR>a b c : α<VAR>s : Finset α<GOAL>(G.cliqueFinset n).card ≤ (Fintype.card α).choose n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableRel G.Adj<VAR>n : ℕ<VAR>a b c : α<VAR>s : Finset α<GOAL>(G.cliqueFinset n).card ≤ (powersetCard n univ).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableRel G.Adj<VAR>n : ℕ<VAR>a b c : α<VAR>s✝ s : Finset α<GOAL>s ∈ G.cliqueFinset n → s ∈ powersetCard n univ
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>p : Type u_4<VAR>n' : m → Type u_5<VAR>𝔸 : Type u_6<VAR>inst✝⁹ : RCLike 𝕂<VAR>inst✝⁸ : Fintype m<VAR>inst✝⁷ : DecidableEq m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : (i : m) → Fintype (n' i)<VAR>inst✝³ : (i : m) → DecidableEq (n' i)<VAR>inst✝² : NormedCommRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕂 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>U A : Matrix m m 𝔸<VAR>hy : IsUnit U<VAR>u : (Matrix m m 𝔸)ˣ<VAR>hu : ↑u = U<GOAL>exp 𝕂 ((↑u)⁻¹ * A * ↑u) = (↑u)⁻¹ * exp 𝕂 A * ↑u