ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>v✝ : ι → M<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : CommRing R₂<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M'<VAR>inst✝⁸ : AddCommGroup M''<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R₂ M<VAR>inst✝⁵ : Module R M'<VAR>inst✝⁴ : Module R M''<VAR>c d : R<VAR>x y : M<VAR>b : Basis ι R M<VAR>G : Type u_10<VAR>inst✝³ : Group G<VAR>inst✝² : DistribMulAction G R<VAR>inst✝¹ : DistribMulAction G M<VAR>inst✝ : IsScalarTower G R M<VAR>v : ι → M<VAR>hv : span R (Set.range v) = ⊤<VAR>w : ι → G<VAR>j : M<VAR>hj : ∀ (p : Submodule R M), Set.range v ⊆ ↑p → j ∈ p<VAR>p : Submodule R M<VAR>hp : Set.range (w • v) ⊆ ↑p<VAR>i : ι<GOAL>v i ∈ ↑p
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>v✝ : ι → M<VAR>inst✝¹² : Ring R<VAR>inst✝¹¹ : CommRing R₂<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : AddCommGroup M'<VAR>inst✝⁸ : AddCommGroup M''<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R₂ M<VAR>inst✝⁵ : Module R M'<VAR>inst✝⁴ : Module R M''<VAR>c d : R<VAR>x y : M<VAR>b : Basis ι R M<VAR>G : Type u_10<VAR>inst✝³ : Group G<VAR>inst✝² : DistribMulAction G R<VAR>inst✝¹ : DistribMulAction G M<VAR>inst✝ : IsScalarTower G R M<VAR>v : ι → M<VAR>hv : span R (Set.range v) = ⊤<VAR>w : ι → G<VAR>j : M<VAR>hj : ∀ (p : Submodule R M), Set.range v ⊆ ↑p → j ∈ p<VAR>p : Submodule R M<VAR>hp : Set.range (w • v) ⊆ ↑p<VAR>i : ι<VAR>this : ((w i)⁻¹ • 1) • w i • v i ∈ p<GOAL>v i ∈ ↑p
<GOAL>IsGδ (⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b})
<VAR>n : ℕ<GOAL>IsOpen (⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b})
<VAR>n : ℕ<VAR>a b : ℤ<VAR>_hb : 1 < b<GOAL>IsOpen (ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b})
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>l₁ l₂ : List α<GOAL>Pairwise R (l₁ ++ l₂) ↔ Pairwise R l₁ ∧ Pairwise R l₂ ∧ ∀ (a : α), a ∈ l₁ → ∀ (b : α), b ∈ l₂ → R a b
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : PartialOrder β<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : OrderBot β<VAR>f : β ↪o α<VAR>hbot : f ⊥ = ⊥<VAR>b : β<VAR>hb : IsAtom (f b)<GOAL>IsAtom b
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : PartialOrder β<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : OrderBot β<VAR>f : β ↪o α<VAR>hbot : f ⊥ = ⊥<VAR>b : β<VAR>hb : ⊥ ⋖ f b<GOAL>⊥ ⋖ b
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>r : ℝ<VAR>s : Set E<GOAL>μ (r • s) = ENNReal.ofReal |r ^ finrank ℝ E| * μ s
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>r : ℝ<VAR>s : Set E<VAR>h : r ≠ 0<GOAL>μ (r • s) = ENNReal.ofReal |r ^ finrank ℝ E| * μ s
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s : Set E<GOAL>μ (0 • s) = ENNReal.ofReal |0 ^ finrank ℝ E| * μ s
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<GOAL>μ (0 • ∅) = ENNReal.ofReal |0 ^ finrank ℝ E| * μ ∅
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s : Set E<VAR>hs : s.Nonempty<GOAL>μ (0 • s) = ENNReal.ofReal |0 ^ finrank ℝ E| * μ s
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>s : Set E<VAR>hs : s.Nonempty<GOAL>μ {0} = ENNReal.ofReal |0 ^ finrank ℝ E| * μ s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : Preorder α<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : Preorder β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : Preorder γ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : Preorder δ<VAR>g : β →Co γ<VAR>f₁ f₂ : α →Co β<VAR>hg : Injective ⇑g<VAR>h : g.comp f₁ = g.comp f₂<VAR>a : α<GOAL>g (f₁ a) = g (f₂ a)
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>r : R<VAR>p : R[X]<VAR>S : Type u_2<VAR>inst✝² : AddCommMonoid S<VAR>inst✝¹ : Pow S ℕ<VAR>inst✝ : MulActionWithZero R S<VAR>x : S<GOAL>p.smeval x = p.sum (smul_pow x)
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>S : L.Substructure M<VAR>s : Set M<GOAL>↑((closure L).toFun s) = range (Term.realize Subtype.val)
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>S✝ : L.Substructure M<VAR>s : Set M<VAR>S : L.Substructure M := { carrier := range (Term.realize Subtype.val), fun_mem := ⋯ }<GOAL>↑((closure L).toFun s) = range (Term.realize Subtype.val)
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>S✝ : L.Substructure M<VAR>s : Set M<VAR>S : L.Substructure M := { carrier := range (Term.realize Subtype.val), fun_mem := ⋯ }<GOAL>↑((closure L).toFun s) = ↑S
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>S✝ : L.Substructure M<VAR>s : Set M<VAR>S : L.Substructure M := { carrier := range (Term.realize Subtype.val), fun_mem := ⋯ }<GOAL>(closure L).toFun s = S
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>S✝ : L.Substructure M<VAR>s : Set M<VAR>S : L.Substructure M := { carrier := range (Term.realize Subtype.val), fun_mem := ⋯ }<VAR>S' : L.Substructure M<VAR>hS' : S' ∈ {S | s ⊆ ↑S}<GOAL>S ≤ S'
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>S✝ : L.Substructure M<VAR>s : Set M<VAR>S : L.Substructure M := { carrier := range (Term.realize Subtype.val), fun_mem := ⋯ }<VAR>S' : L.Substructure M<VAR>hS' : S' ∈ {S | s ⊆ ↑S}<VAR>t : L.Term { x // x ∈ s }<GOAL>Term.realize Subtype.val t ∈ S'
<VAR>M₀ : Type u_1<VAR>M₀' : Type u_2<VAR>inst✝³ : MulZeroOneClass M₀<VAR>inst✝² : Nontrivial M₀<VAR>inst✝¹ : Zero M₀'<VAR>inst✝ : One M₀'<VAR>f : M₀' → M₀<VAR>zero : f 0 = 0<VAR>one : f 1 = 1<GOAL>¬0 = 1
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableEq V<VAR>x u v : V<VAR>p : G.Walk u v<VAR>ht : p.IsEulerian<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<GOAL>Even (G.degree x) ↔ u ≠ v → x ≠ u ∧ x ≠ v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableEq V<VAR>x u v : V<VAR>p : G.Walk u v<VAR>ht : p.IsEulerian<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<GOAL>G.degree x = List.countP (fun e => decide (x ∈ e)) p.edges
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableEq V<VAR>x u v : V<VAR>p : G.Walk u v<VAR>ht : p.IsEulerian<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<GOAL>(G.incidenceFinset x).card = Multiset.card (Multiset.filter (Membership.mem x) ↑p.edges)
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableEq V<VAR>x u v : V<VAR>p : G.Walk u v<VAR>ht : p.IsEulerian<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<GOAL>(G.incidenceFinset x).val = Multiset.filter (Membership.mem x) ↑p.edges
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableEq V<VAR>x u v : V<VAR>p : G.Walk u v<VAR>ht : p.IsEulerian<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<GOAL>(G.incidenceFinset x).val = (Finset.filter (Membership.mem x) ⋯.edgesFinset).val
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableEq V<VAR>x u v : V<VAR>p : G.Walk u v<VAR>ht : p.IsEulerian<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>this : Fintype ↑G.edgeSet<GOAL>(G.incidenceFinset x).val = (Finset.filter (Membership.mem x) ⋯.edgesFinset).val
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>c : ℂ<VAR>R θ : ℝ<GOAL>circleMap c R (θ + 2 * π) = circleMap c R θ
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>α : Type w<VAR>inst✝¹ : HasFiniteCoproducts C<VAR>inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C<VAR>F : Discrete α ⥤ C<VAR>s : Cocone F<VAR>m : { pt := colimit (liftToFinset F), ι := Discrete.natTrans fun j => Sigma.ι (fun x => F.obj ↑x) ⟨j, ⋯⟩ ≫ colimit.ι (liftToFinset F) {j} }.pt ⟶ s.pt<VAR>h : ∀ (j : Discrete α), { pt := colimit (liftToFinset F), ι := Discrete.natTrans fun j => Sigma.ι (fun x => F.obj ↑x) ⟨j, ⋯⟩ ≫ colimit.ι (liftToFinset F) {j} }.ι.app j ≫ m = s.ι.app j<GOAL>m = (fun s => colimit.desc (liftToFinset F) { pt := s.pt, ι := { app := fun t => Sigma.desc fun x => s.ι.app ↑x, naturality := ⋯ } }) s
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>α : Type w<VAR>inst✝¹ : HasFiniteCoproducts C<VAR>inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C<VAR>F : Discrete α ⥤ C<VAR>s : Cocone F<VAR>m : { pt := colimit (liftToFinset F), ι := Discrete.natTrans fun j => Sigma.ι (fun x => F.obj ↑x) ⟨j, ⋯⟩ ≫ colimit.ι (liftToFinset F) {j} }.pt ⟶ s.pt<VAR>h : ∀ (j : Discrete α), { pt := colimit (liftToFinset F), ι := Discrete.natTrans fun j => Sigma.ι (fun x => F.obj ↑x) ⟨j, ⋯⟩ ≫ colimit.ι (liftToFinset F) {j} }.ι.app j ≫ m = s.ι.app j<GOAL>∀ (j : Finset (Discrete α)), colimit.ι (liftToFinset F) j ≫ m = colimit.ι (liftToFinset F) j ≫ (fun s => colimit.desc (liftToFinset F) { pt := s.pt, ι := { app := fun t => Sigma.desc fun x => s.ι.app ↑x, naturality := ⋯ } }) s
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>α : Type w<VAR>inst✝¹ : HasFiniteCoproducts C<VAR>inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C<VAR>F : Discrete α ⥤ C<VAR>s : Cocone F<VAR>m : { pt := colimit (liftToFinset F), ι := Discrete.natTrans fun j => Sigma.ι (fun x => F.obj ↑x) ⟨j, ⋯⟩ ≫ colimit.ι (liftToFinset F) {j} }.pt ⟶ s.pt<VAR>h : ∀ (j : Discrete α), { pt := colimit (liftToFinset F), ι := Discrete.natTrans fun j => Sigma.ι (fun x => F.obj ↑x) ⟨j, ⋯⟩ ≫ colimit.ι (liftToFinset F) {j} }.ι.app j ≫ m = s.ι.app j<VAR>t : Finset (Discrete α)<GOAL>colimit.ι { obj := fun s => ∐ fun x => F.obj ↑x, map := fun {x Y} h => Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) ⟨↑y, ⋯⟩, map_id := ⋯, map_comp := ⋯ } t ≫ m = colimit.ι { obj := fun s => ∐ fun x => F.obj ↑x, map := fun {x Y} h => Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) ⟨↑y, ⋯⟩, map_id := ⋯, map_comp := ⋯ } t ≫ colimit.desc { obj := fun s => ∐ fun x => F.obj ↑x, map := fun {x Y} h => Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) ⟨↑y, ⋯⟩, map_id := ⋯, map_comp := ⋯ } { pt := s.pt, ι := { app := fun t => Sigma.desc fun x => s.ι.app ↑x, naturality := ⋯ } }
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>α : Type w<VAR>inst✝¹ : HasFiniteCoproducts C<VAR>inst✝ : HasFilteredColimitsOfSize.{w, w, v, u} C<VAR>F : Discrete α ⥤ C<VAR>s : Cocone F<VAR>m : { pt := colimit (liftToFinset F), ι := Discrete.natTrans fun j => Sigma.ι (fun x => F.obj ↑x) ⟨j, ⋯⟩ ≫ colimit.ι (liftToFinset F) {j} }.pt ⟶ s.pt<VAR>h : ∀ (j : Discrete α), { pt := colimit (liftToFinset F), ι := Discrete.natTrans fun j => Sigma.ι (fun x => F.obj ↑x) ⟨j, ⋯⟩ ≫ colimit.ι (liftToFinset F) {j} }.ι.app j ≫ m = s.ι.app j<VAR>t : Finset (Discrete α)<GOAL>∀ (j : Discrete { x // x ∈ t }), colimit.ι (Discrete.functor fun x => F.obj ↑x) j ≫ colimit.ι { obj := fun s => ∐ fun x => F.obj ↑x, map := fun {x Y} h => Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) ⟨↑y, ⋯⟩, map_id := ⋯, map_comp := ⋯ } t ≫ m = colimit.ι (Discrete.functor fun x => F.obj ↑x) j ≫ colimit.ι { obj := fun s => ∐ fun x => F.obj ↑x, map := fun {x Y} h => Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) ⟨↑y, ⋯⟩, map_id := ⋯, map_comp := ⋯ } t ≫ colimit.desc { obj := fun s => ∐ fun x => F.obj ↑x, map := fun {x Y} h => Sigma.desc fun y => Sigma.ι (fun x => F.obj ↑x) ⟨↑y, ⋯⟩, map_id := ⋯, map_comp := ⋯ } { pt := s.pt, ι := { app := fun t => Sigma.desc fun x => s.ι.app ↑x, naturality := ⋯ } }
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>rι : ι → ι → Prop<VAR>rπ : (i : ι) → π i → π i → Prop<VAR>f : γ → ι<VAR>g : (i : ι) → γ → π i<VAR>s : Set γ<VAR>hι : s.WellFoundedOn (rι on f)<VAR>hπ : ∀ (i : ι), (s ∩ f ⁻¹' {i}).WellFoundedOn (rπ i on g i)<GOAL>WellFounded (Sigma.Lex rι rπ on fun c => ⟨f ↑c, g (f ↑c) ↑c⟩)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>a : R<GOAL>(coeff R 0) ((C R) a) = a
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>p₁ q₁ p₂ q₂ : F[X]<VAR>hq₁ : q₁ ≠ 0<VAR>hq₂ : q₂ ≠ 0<VAR>h₁ : Splits (algebraMap F q₁.SplittingField) p₁<VAR>h₂ : Splits (algebraMap F q₂.SplittingField) p₂<GOAL>Splits (algebraMap F (q₁ * q₂).SplittingField) (p₁ * p₂)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>p₁ q₁ p₂ q₂ : F[X]<VAR>hq₁ : q₁ ≠ 0<VAR>hq₂ : q₂ ≠ 0<VAR>h₁ : Splits (algebraMap F q₁.SplittingField) p₁<VAR>h₂ : Splits (algebraMap F q₂.SplittingField) p₂<GOAL>Splits (algebraMap F (q₁ * q₂).SplittingField) p₁
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>p₁ q₁ p₂ q₂ : F[X]<VAR>hq₁ : q₁ ≠ 0<VAR>hq₂ : q₂ ≠ 0<VAR>h₁ : Splits (algebraMap F q₁.SplittingField) p₁<VAR>h₂ : Splits (algebraMap F q₂.SplittingField) p₂<GOAL>Splits (algebraMap F (q₁ * q₂).SplittingField) p₂
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>x y L : R<GOAL>span {(mk W) (C (X - C x)), (mk W) (Y - C (C y))} = span {(mk W) (C (X - C x)), (mk W) (Y - C (C L * (X - C x) + C y))}
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>x y L : R<GOAL>span {(mk W) (C (X - C x)), (mk W) (Y - C (C y) + C (X - C x) * C (C (-L)))} = span {(mk W) (C (X - C x)), (mk W) (Y - C (C L * (X - C x) + C y))}
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>x y L : R<GOAL>Y - C (C y) + C (X - C x) * C (C (-L)) = Y - C (C L * (X - C x) + C y)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>x y L : R<GOAL>Y - C (C y) + (C X - C (C x)) * -C (C L) = Y - (C (C L) * (C X - C (C x)) + C (C y))
<VAR>a b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n : ℕ<VAR>motive : (m : ℕ) → m ≤ n → Sort u_1<VAR>of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯<VAR>self : motive n ⋯<GOAL>leRec (motive := fun {n_1} mn => {motive : (m : ℕ) → m ≤ n_1 → Sort u_1} → ((k : ℕ) → (h : k < n_1) → motive (k + 1) h → motive k ⋯) → motive n_1 ⋯ → motive n mn) (fun {motive} of_succ self => self) (fun ⦃k⦄ h ih {motive} of_succ self => ih (fun i hi => of_succ i ⋯) (of_succ k ⋯ self)) ⋯ of_succ self = self
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N : LieSubmodule R L M<VAR>N' : LieSubmodule R L ↥↑N<GOAL>map N.incl N' < N ↔ N' < ⊤
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N : LieSubmodule R L M<VAR>N' : LieSubmodule R L ↥↑N<GOAL>N = (mapOrderEmbedding ⋯) ⊤
<VAR>α : Type u<VAR>c : Cardinal.{u_1}<VAR>c' : ℕ<GOAL>toPartENat c ≤ toPartENat ↑c' ↔ c ≤ ↑c'
<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 : α<GOAL>toIcoDiv hp a (b + p) = toIcoDiv hp a b + 1
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>f : R[X]<VAR>S : Type u_2<VAR>F : Type u_3<VAR>inst✝² : Semiring S<VAR>inst✝¹ : FunLike F R[X] S[X]<VAR>inst✝ : AddMonoidHomClass F R[X] S[X]<VAR>φ : F<VAR>p : R[X]<VAR>k : ℕ<VAR>fu : ℕ → ℕ<VAR>fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0<VAR>fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m<VAR>φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0<VAR>φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n<GOAL>(φ p).natDegree = fu p.natDegree
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>f : R[X]<VAR>S : Type u_2<VAR>F : Type u_3<VAR>inst✝² : Semiring S<VAR>inst✝¹ : FunLike F R[X] S[X]<VAR>inst✝ : AddMonoidHomClass F R[X] S[X]<VAR>φ : F<VAR>p : R[X]<VAR>k : ℕ<VAR>fu : ℕ → ℕ<VAR>fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0<VAR>fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m<VAR>φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0<VAR>φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n<GOAL>∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ p.natDegree → (fun p => (φ p).natDegree = fu p.natDegree) (C r * X ^ n)
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>f : R[X]<VAR>S : Type u_2<VAR>F : Type u_3<VAR>inst✝² : Semiring S<VAR>inst✝¹ : FunLike F R[X] S[X]<VAR>inst✝ : AddMonoidHomClass F R[X] S[X]<VAR>φ : F<VAR>p : R[X]<VAR>k : ℕ<VAR>fu : ℕ → ℕ<VAR>fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0<VAR>fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m<VAR>φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0<VAR>φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n<GOAL>∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ p.natDegree → (fun p => (φ p).natDegree = fu p.natDegree) f → (fun p => (φ p).natDegree = fu p.natDegree) g → (fun p => (φ p).natDegree = fu p.natDegree) (f + g)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>A : C<VAR>hg : S.g = 0<VAR>inst✝ : S.HasHomology<GOAL>IsIso S.homologyι
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>A : C<VAR>hg : S.g = 0<VAR>inst✝ : S.HasHomology<VAR>this : IsIso S.rightHomologyι<GOAL>IsIso S.homologyι
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>G : C<VAR>inst✝ : ∀ (A : C), HasCoproduct fun x => G<GOAL>IsSeparator G ↔ ∀ (A : C), Epi (Sigma.desc fun f => f)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>G : C<VAR>inst✝ : ∀ (A : C), HasCoproduct fun x => G<GOAL>(∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g) ↔ ∀ (A : C), Epi (Sigma.desc fun f => f)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>r • closedBall 0 1 = closedBall 0 r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁵ : MeasurableSpace δ<VAR>inst✝⁴ : NormedAddCommGroup β<VAR>inst✝³ : NormedAddCommGroup γ<VAR>𝕜 : Type u_5<VAR>inst✝² : NormedAddCommGroup 𝕜<VAR>inst✝¹ : SMulZeroClass 𝕜 β<VAR>inst✝ : BoundedSMul 𝕜 β<VAR>c : 𝕜<VAR>f : α → β<VAR>hfi : ∫⁻ (a : α), ↑‖f a‖₊ ∂μ < ⊤<GOAL>∫⁻ (a : α), ↑‖(c • f) a‖₊ ∂μ < ⊤
<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>({a} ∩ s).Nonempty ↔ a ∈ s
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m n₁ n₂ n₁₂ : ℤ<VAR>k : R<VAR>z₁ : Cochain F G n₁<VAR>z₂ : Cochain G K n₂<VAR>h : n₁ + n₂ = n₁₂<VAR>p q : ℤ<VAR>hpq : p + n₁₂ = q<GOAL>((k • z₁).comp z₂ h).v p q hpq = (k • z₁.comp z₂ h).v p q hpq
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>u : δ → δ → Prop<VAR>F : Type u_5<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : RelHomClass F r s<VAR>f : F<VAR>b : β<VAR>a : α<VAR>H : ∀ (y : β), s y (f a) → Acc s y<VAR>IH : ∀ (y : β), s y (f a) → ∀ (a : α), f a = y → Acc r a<GOAL>Acc r a
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g✝ : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>f g : ι → Ω → ℝ<VAR>hf : Submartingale f ℱ μ<VAR>hg : Submartingale g ℱ μ<GOAL>Submartingale (f ⊔ g) ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g✝ : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>f g : ι → Ω → ℝ<VAR>hf : Submartingale f ℱ μ<VAR>hg : Submartingale g ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>(f ⊔ g) i ≤ᶠ[ae μ] μ[(f ⊔ g) j|↑ℱ i]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g✝ : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>f g : ι → Ω → ℝ<VAR>hf : Submartingale f ℱ μ<VAR>hg : Submartingale g ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>f i ≤ᶠ[ae μ] μ[(f ⊔ g) j|↑ℱ i]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g✝ : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>f g : ι → Ω → ℝ<VAR>hf : Submartingale f ℱ μ<VAR>hg : Submartingale g ℱ μ<VAR>i j : ι<VAR>hij : i ≤ j<GOAL>g i ≤ᶠ[ae μ] μ[(f ⊔ g) j|↑ℱ i]
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x y : RatFunc K<GOAL>x + y = (algebraMap K[X] (RatFunc K)) (x.num * y.denom + x.denom * y.num) / (algebraMap K[X] (RatFunc K)) (x.denom * y.denom)
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x y : RatFunc K<GOAL>(algebraMap K[X] (RatFunc K)) x.num / (algebraMap K[X] (RatFunc K)) x.denom + (algebraMap K[X] (RatFunc K)) y.num / (algebraMap K[X] (RatFunc K)) y.denom = (algebraMap K[X] (RatFunc K)) (x.num * y.denom + x.denom * y.num) / (algebraMap K[X] (RatFunc K)) (x.denom * y.denom)
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x y : RatFunc K<GOAL>(algebraMap K[X] (RatFunc K)) x.denom ≠ 0
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x y : RatFunc K<GOAL>(algebraMap K[X] (RatFunc K)) y.denom ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : ι → α<VAR>s✝ t : Set α<VAR>f : α → β<VAR>s : Set β<GOAL>f ⁻¹' s = univ ↔ range f ⊆ s
<VAR>n m : ℕ<GOAL>(range' n (m - n)).length = m - n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Fintype n<VAR>M₁₁ : Matrix m m R<VAR>M₁₂ : Matrix m n R<VAR>M₂₁ : Matrix n m R<VAR>M₂₂ M✝ : Matrix n n R<VAR>i j : n<VAR>e : n ≃ m<VAR>M : Matrix n n R<GOAL>((reindex e e) M).charmatrix.det = M.charmatrix.det