ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>coequalizer.π ({ X := X.X, actLeft := X.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := X.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.actRight ▷ M.X) ((α_ { X := X.X, actLeft := X.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := X.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X X.X M.X).hom ≫ { X := X.X, actLeft := X.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := X.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X ◁ M.actLeft) ≫ ({ X := X.X, actLeft := X.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := X.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.whiskerLeft f).hom = coequalizer.π ({ X := X.X, actLeft := X.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := X.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.actRight ▷ M.X) ((α_ { X := X.X, actLeft := X.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := X.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X X.X M.X).hom ≫ { X := X.X, actLeft := X.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := X.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X ◁ M.actLeft) ≫ ((isoOfIso { hom := LeftUnitorBimod.hom M, inv := LeftUnitorBimod.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯ ⋯).hom ≫ f ≫ (isoOfIso { hom := LeftUnitorBimod.hom N, inv := LeftUnitorBimod.inv N, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯ ⋯).inv).hom
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>coequalizer.π (X.mul ▷ M.X) ((α_ X.X X.X M.X).hom ≫ X.X ◁ M.actLeft) ≫ colimMap (parallelPairHom (X.mul ▷ M.X) ((α_ X.X X.X M.X).hom ≫ X.X ◁ M.actLeft) (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft) ((X.X ⊗ X.X) ◁ f.hom) (X.X ◁ f.hom) ⋯ ⋯) = coequalizer.π (X.mul ▷ M.X) ((α_ X.X X.X M.X).hom ≫ X.X ◁ M.actLeft) ≫ LeftUnitorBimod.hom M ≫ f.hom ≫ LeftUnitorBimod.inv N
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>X.X ◁ f.hom ≫ colimit.ι (parallelPair (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one = coequalizer.π (X.mul ▷ M.X) ((α_ X.X X.X M.X).hom ≫ X.X ◁ M.actLeft) ≫ LeftUnitorBimod.hom M ≫ f.hom ≫ LeftUnitorBimod.inv N
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>X.X ◁ f.hom ≫ colimit.ι (parallelPair (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one = coequalizer.π (X.mul ▷ M.X) ((α_ X.X X.X M.X).hom ≫ X.X ◁ M.actLeft) ≫ coequalizer.desc M.actLeft ⋯ ≫ f.hom ≫ LeftUnitorBimod.inv N
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>X.X ◁ f.hom ≫ colimit.ι (parallelPair (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one = (M.actLeft ≫ f.hom) ≫ LeftUnitorBimod.inv N
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>X.X ◁ f.hom ≫ colimit.ι (parallelPair (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one = (M.actLeft ≫ f.hom) ≫ (λ_ N.X).inv ≫ X.one ▷ N.X ≫ coequalizer.π (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>X.X ◁ f.hom ≫ colimit.ι (parallelPair (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one = (((X.X ◁ f.hom ≫ N.actLeft) ≫ (λ_ N.X).inv) ≫ X.one ▷ N.X) ≫ coequalizer.π (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>X.X ◁ f.hom ≫ colimit.ι (parallelPair (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one = X.X ◁ f.hom ≫ (((λ_ (X.X ⊗ N.X)).inv ≫ 𝟙_ C ◁ N.actLeft) ≫ X.one ▷ N.X) ≫ coequalizer.π (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>X.X ◁ f.hom ≫ colimit.ι (parallelPair (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one = X.X ◁ f.hom ≫ (λ_ (X.X ⊗ N.X)).inv ≫ (X.one ▷ (X.X ⊗ N.X) ≫ X.X ◁ N.actLeft) ≫ coequalizer.π (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>X.X ◁ f.hom ≫ colimit.ι (parallelPair (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one = X.X ◁ f.hom ≫ (λ_ (X.X ⊗ N.X)).inv ≫ X.one ▷ (X.X ⊗ N.X) ≫ ((α_ X.X X.X N.X).inv ≫ (α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft) ≫ coequalizer.π (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>X.X ◁ f.hom ≫ colimit.ι (parallelPair (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one = X.X ◁ f.hom ≫ (λ_ (X.X ⊗ N.X)).inv ≫ X.one ▷ (X.X ⊗ N.X) ≫ (α_ X.X X.X N.X).inv ≫ X.mul ▷ N.X ≫ coequalizer.π (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>X.X ◁ f.hom ≫ colimit.ι (parallelPair (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one = X.X ◁ f.hom ≫ (λ_ (X.X ⊗ N.X)).inv ≫ (((α_ (𝟙_ C) X.X N.X).inv ≫ X.one ▷ X.X ▷ N.X) ≫ X.mul ▷ N.X) ≫ coequalizer.π (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<GOAL>X.X ◁ f.hom ≫ colimit.ι (parallelPair (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one = X.X ◁ f.hom ≫ (λ_ (X.X ⊗ N.X)).inv ≫ (α_ (𝟙_ C) X.X N.X).inv ≫ (λ_ X.X).hom ▷ N.X ≫ coequalizer.π (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<VAR>this : (λ_ (X.X ⊗ N.X)).inv ≫ (α_ (𝟙_ C) X.X N.X).inv ≫ (λ_ X.X).hom ▷ N.X = 𝟙 (X.X ⊗ N.X)<GOAL>X.X ◁ f.hom ≫ colimit.ι (parallelPair (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one = X.X ◁ f.hom ≫ (λ_ (X.X ⊗ N.X)).inv ≫ (α_ (𝟙_ C) X.X N.X).inv ≫ (λ_ X.X).hom ▷ N.X ≫ coequalizer.π (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>X Y : Mon_ C<VAR>M N : Bimod X Y<VAR>f : M ⟶ N<VAR>this : (λ_ (X.X ⊗ N.X)).inv ≫ (α_ (𝟙_ C) X.X N.X).inv ≫ (λ_ X.X).hom ▷ N.X = 𝟙 (X.X ⊗ N.X)<GOAL>X.X ◁ f.hom ≫ colimit.ι (parallelPair (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one = X.X ◁ f.hom ≫ 𝟙 (X.X ⊗ N.X) ≫ coequalizer.π (X.mul ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)
<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 R<GOAL>(Function.Surjective fun v => v ᵥ* A) ↔ IsUnit A
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>h : IsIdempotentComplete Cᵒᵖ<VAR>X : C<VAR>p : X ⟶ X<VAR>hp : p ≫ p = p<GOAL>∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>h : IsIdempotentComplete Cᵒᵖ<VAR>X : C<VAR>p : X ⟶ X<VAR>hp : p ≫ p = p<VAR>Y : Cᵒᵖ<VAR>i : Y ⟶ op X<VAR>e : op X ⟶ Y<VAR>h₁ : i ≫ e = 𝟙 Y<VAR>h₂ : e ≫ i = p.op<GOAL>∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>h : IsIdempotentComplete Cᵒᵖ<VAR>X : C<VAR>p : X ⟶ X<VAR>hp : p ≫ p = p<VAR>Y : Cᵒᵖ<VAR>i : Y ⟶ op X<VAR>e : op X ⟶ Y<VAR>h₁ : i ≫ e = 𝟙 Y<VAR>h₂ : e ≫ i = p.op<GOAL>e.unop ≫ i.unop = 𝟙 (unop Y) ∧ i.unop ≫ e.unop = p
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>p : Prop<GOAL>IsEmpty p ↔ ¬p
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>h : UniqueMul A B a0 b0<VAR>x1 y1 : G<VAR>hx : x1 ∈ A ∧ y1 ∈ B ∧ x1 * y1 = a0 * b0<VAR>x2 y2 : G<VAR>hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = a0 * b0<GOAL>(x1, y1) = (x2, y2)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>A B : Finset G<VAR>x1 y1 x2 y2 : G<VAR>h : UniqueMul A B x1 y1<VAR>hx : x1 ∈ A ∧ y1 ∈ B ∧ x1 * y1 = x1 * y1<VAR>hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = x1 * y1<GOAL>(x1, y1) = (x2, y2)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>A B : Finset G<VAR>x2 y2 : G<VAR>h : UniqueMul A B x2 y2<VAR>hx hy : x2 ∈ A ∧ y2 ∈ B ∧ x2 * y2 = x2 * y2<GOAL>(x2, y2) = (x2, y2)
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsIntegrallyClosed R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>hq : q.Monic<VAR>r : K[X]<VAR>hr : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) q * r<GOAL>q ∣ p
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsIntegrallyClosed R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>hq : q.Monic<VAR>r : K[X]<VAR>hr : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) q * r<VAR>d' : R[X]<VAR>hr' : Polynomial.map (algebraMap R K) d' * C r.leadingCoeff = r<GOAL>q ∣ p
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsIntegrallyClosed R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>hq : q.Monic<VAR>r : K[X]<VAR>hr : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) q * r<VAR>d' : R[X]<VAR>hr' : Polynomial.map (algebraMap R K) d' = r<GOAL>q ∣ p
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsIntegrallyClosed R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>hq : q.Monic<VAR>r : K[X]<VAR>hr : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) q * r<VAR>d' : R[X]<VAR>hr' : Polynomial.map (algebraMap R K) d' * C r.leadingCoeff = r<GOAL>r.Monic
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα✝ : α.IsNonZero<VAR>hα : ¬α.IsZero<GOAL>β (coroot α) = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα✝ : α.IsNonZero<VAR>hα : ¬α.IsZero<VAR>x : L<VAR>hx : x ∈ weightSpace L ⇑(chainTop (⇑α) β)<VAR>x_ne0 : x ≠ 0<GOAL>β (coroot α) = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα✝ : α.IsNonZero<VAR>hα : ¬α.IsZero<VAR>x : L<VAR>hx : x ∈ weightSpace L ⇑(chainTop (⇑α) β)<VAR>x_ne0 : x ≠ 0<VAR>this : ↑(chainLength α β) • x = ⁅coroot α, x⁆<GOAL>β (coroot α) = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα✝ : α.IsNonZero<VAR>hα : ¬α.IsZero<VAR>x : L<VAR>hx : x ∈ weightSpace L ⇑(chainTop (⇑α) β)<VAR>x_ne0 : x ≠ 0<VAR>this : ↑(chainLength α β) = ↑(chainTopCoeff (⇑α) β) * 2 + β (coroot α)<GOAL>β (coroot α) = ↑(↑(chainLength α β) - 2 * ↑(chainTopCoeff (⇑α) β))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hqr : q + r ≠ 0<VAR>hq : q ≠ 0<VAR>hr : r ≠ 0<VAR>hval : padicValRat p q ≠ padicValRat p r<GOAL>padicValRat p (q + r) = min (padicValRat p q) (padicValRat p r)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hqr : q + r ≠ 0<VAR>hq : q ≠ 0<VAR>hr : r ≠ 0<VAR>hval : padicValRat p q ≠ padicValRat p r<VAR>h1 : min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)<GOAL>padicValRat p (q + r) = min (padicValRat p q) (padicValRat p r)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hqr : q + r ≠ 0<VAR>hq : q ≠ 0<VAR>hr : r ≠ 0<VAR>hval : padicValRat p q ≠ padicValRat p r<VAR>h1 : min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)<VAR>h2 : min (padicValRat p (q + r)) (padicValRat p (-r)) ≤ padicValRat p (q + r + -r)<GOAL>padicValRat p (q + r) = min (padicValRat p q) (padicValRat p r)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hqr : q + r ≠ 0<VAR>hq : q ≠ 0<VAR>hr : r ≠ 0<VAR>hval : padicValRat p q ≠ padicValRat p r<VAR>h1 : min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)<VAR>h2 : min (padicValRat p (q + r)) (padicValRat p (-r)) ≤ padicValRat p (q + r + -r)<VAR>h3 : min (padicValRat p (r + q)) (padicValRat p (-q)) ≤ padicValRat p (r + q + -q)<GOAL>padicValRat p (q + r) = min (padicValRat p q) (padicValRat p r)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hqr : q + r ≠ 0<VAR>hq : q ≠ 0<VAR>hr : r ≠ 0<VAR>hval : padicValRat p q ≠ padicValRat p r<VAR>h1 : min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)<VAR>h2 : min (padicValRat p (q + r)) (padicValRat p r) ≤ padicValRat p q<VAR>h3 : min (padicValRat p (r + q)) (padicValRat p q) ≤ padicValRat p r<GOAL>padicValRat p (q + r) = min (padicValRat p q) (padicValRat p r)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hqr : q + r ≠ 0<VAR>hq : q ≠ 0<VAR>hr : r ≠ 0<VAR>hval : padicValRat p q ≠ padicValRat p r<VAR>h1 : min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)<VAR>h2 : min (padicValRat p (q + r)) (padicValRat p r) ≤ padicValRat p q<VAR>h3 : min (padicValRat p (q + r)) (padicValRat p q) ≤ padicValRat p r<GOAL>padicValRat p (q + r) = min (padicValRat p q) (padicValRat p r)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hqr : q + r ≠ 0<VAR>hq : q ≠ 0<VAR>hr : r ≠ 0<VAR>hval : padicValRat p q ≠ padicValRat p r<VAR>h1 : min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)<VAR>h2 : min (padicValRat p (q + r)) (padicValRat p r) ≤ padicValRat p q<VAR>h3 : min (padicValRat p (q + r)) (padicValRat p q) ≤ padicValRat p r<GOAL>padicValRat p (q + r) ≤ padicValRat p q
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hqr : q + r ≠ 0<VAR>hq : q ≠ 0<VAR>hr : r ≠ 0<VAR>hval : padicValRat p q ≠ padicValRat p r<VAR>h1 : min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)<VAR>h2 : min (padicValRat p (q + r)) (padicValRat p r) ≤ padicValRat p q<VAR>h3 : min (padicValRat p (q + r)) (padicValRat p q) ≤ padicValRat p r<GOAL>padicValRat p (q + r) ≤ padicValRat p r
<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✝⁷ : Semiring R₂<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>inst✝² : RingHomSurjective τ₁₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>f : F<VAR>p : Submodule R M<VAR>h : LinearMap.ker f ≤ p<GOAL>comap f (map f p) = p
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>f : 𝕜' → 𝕜'<VAR>g : 𝕜 → 𝕜'<VAR>x : 𝕜<VAR>hf : DifferentiableAt 𝕜' f (g x)<VAR>hg : DifferentiableAt 𝕜 g x<GOAL>logDeriv (f ∘ g) x = logDeriv f (g x) * deriv g x
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>f : 𝕜' → 𝕜'<VAR>g : 𝕜 → 𝕜'<VAR>x : 𝕜<VAR>hf : DifferentiableAt 𝕜' f (g x)<VAR>hg : DifferentiableAt 𝕜 g x<GOAL>deriv f (g x) * deriv g x / f (g x) = deriv f (g x) / f (g x) * deriv g x
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ z w : K<GOAL>im (z / w) = im z * re w / normSq w - re z * im w / normSq w
<VAR>𝕜 : Type u_1<VAR>inst✝³² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³¹ : NormedAddCommGroup E<VAR>inst✝³⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝²⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝²⁸ : TopologicalSpace M<VAR>inst✝²⁷ : ChartedSpace H M<VAR>inst✝²⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝²⁵ : NormedAddCommGroup E'<VAR>inst✝²⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²² : TopologicalSpace M'<VAR>inst✝²¹ : ChartedSpace H' M'<VAR>inst✝²⁰ : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_16<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_17<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>f✝ f₁ : M → M'<VAR>s t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>f : E → E'<GOAL>ContMDiff 𝓘(𝕜, E) 𝓘(𝕜, E') n f ↔ ContDiff 𝕜 n f
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>S : Type u_3<VAR>R : Type u_4<VAR>inst✝⁴ : Zero ι<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Algebra S R<VAR>A : ι → Submodule S R<VAR>inst✝ : GradedOne A<VAR>s : S<GOAL>(algebraMap S R) s ∈ A 0
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>S : Type u_3<VAR>R : Type u_4<VAR>inst✝⁴ : Zero ι<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Algebra S R<VAR>A : ι → Submodule S R<VAR>inst✝ : GradedOne A<VAR>s : S<GOAL>s • 1 ∈ A 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>ι : Sort u_2<VAR>inst✝ : Finite ι<VAR>l : Filter α<VAR>p : ι → α → Prop<GOAL>(∀ᶠ (x : α) in l, ∀ (i : ι), p i x) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p i x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝² : UniformSpace β<VAR>δ : ι → Type u_5<VAR>inst✝¹ : (i : ι) → UniformSpace (δ i)<VAR>inst✝ : TopologicalSpace α<GOAL>IsClosed {f | Continuous (toFun f)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝² : UniformSpace β<VAR>δ : ι → Type u_5<VAR>inst✝¹ : (i : ι) → UniformSpace (δ i)<VAR>inst✝ : TopologicalSpace α<VAR>f : α →ᵤ β<VAR>u : Filter (α →ᵤ β)<VAR>x✝ : u.NeBot<VAR>hu : u ≤ 𝓟 {f | Continuous (toFun f)}<VAR>huf : u ≤ 𝓝 f<GOAL>f ∈ {f | Continuous (toFun f)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝² : UniformSpace β<VAR>δ : ι → Type u_5<VAR>inst✝¹ : (i : ι) → UniformSpace (δ i)<VAR>inst✝ : TopologicalSpace α<VAR>f : α →ᵤ β<VAR>u : Filter (α →ᵤ β)<VAR>x✝ : u.NeBot<VAR>hu : u ≤ 𝓟 {f | Continuous (toFun f)}<VAR>huf : TendstoUniformly (⇑toFun ∘ id) (toFun f) u<GOAL>f ∈ {f | Continuous (toFun f)}