ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>a : Primrec fun a => ofNat (ℕ × Code) a.length<VAR>k✝ : Primrec fun a => (ofNat (ℕ × Code) a.1.length).1<VAR>n✝ : Primrec Prod.snd<VAR>k : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).1<VAR>n : Primrec fun a => a.1.2<VAR>k' : Primrec Prod.snd<VAR>c : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).2<GOAL>Primrec fun p => (fun p k' => Code.recOn (ofNat (ℕ × Code) p.1.length).2 (some 0) (some p.2.succ) (some (unpair p.2).1) (some (unpair p.2).2) (fun cf cg x x => do let x ← Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) p.2 let y ← Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2 some (Nat.pair x y)) (fun cf cg x x => do let x ← Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2 Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) x) (fun cf cg x x => let z := (unpair p.2).1; Nat.casesOn (unpair p.2).2 (Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) z) fun y => do let i ← Nat.Partrec.Code.lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z y) Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) (Nat.pair z (Nat.pair y i))) fun cf x => let z := (unpair p.2).1; let m := (unpair p.2).2; do let x ← Nat.Partrec.Code.lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) (Nat.pair z m) Nat.casesOn x (some m) fun x => Nat.Partrec.Code.lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z (m + 1))) p.1 p.2
<VAR>a : Primrec fun a => ofNat (ℕ × Code) a.length<VAR>k✝ : Primrec fun a => (ofNat (ℕ × Code) a.1.length).1<VAR>n✝ : Primrec Prod.snd<VAR>k : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).1<VAR>n : Primrec fun a => a.1.2<VAR>k' : Primrec Prod.snd<VAR>c : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).2<GOAL>Primrec fun a => do let x ← Nat.Partrec.Code.lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) a.1.1.2 let y ← Nat.Partrec.Code.lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) a.1.1.2 some (Nat.pair x y)
<VAR>a : Primrec fun a => ofNat (ℕ × Code) a.length<VAR>k✝ : Primrec fun a => (ofNat (ℕ × Code) a.1.length).1<VAR>n✝ : Primrec Prod.snd<VAR>k : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).1<VAR>n : Primrec fun a => a.1.2<VAR>k' : Primrec Prod.snd<VAR>c : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).2<GOAL>Primrec fun a => do let x ← Nat.Partrec.Code.lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) a.1.1.2 Nat.Partrec.Code.lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) x
<VAR>a : Primrec fun a => ofNat (ℕ × Code) a.length<VAR>k✝ : Primrec fun a => (ofNat (ℕ × Code) a.1.length).1<VAR>n✝ : Primrec Prod.snd<VAR>k : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).1<VAR>n : Primrec fun a => a.1.2<VAR>k' : Primrec Prod.snd<VAR>c : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).2<GOAL>Primrec fun a => let z := (unpair a.1.1.2).1; Nat.casesOn (unpair a.1.1.2).2 (Nat.Partrec.Code.lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) z) fun y => do let i ← Nat.Partrec.Code.lup a.1.1.1 (a.1.2, (ofNat (ℕ × Code) a.1.1.1.length).2) (Nat.pair z y) Nat.Partrec.Code.lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) (Nat.pair z (Nat.pair y i))
<VAR>a : Primrec fun a => ofNat (ℕ × Code) a.length<VAR>k✝ : Primrec fun a => (ofNat (ℕ × Code) a.1.length).1<VAR>n✝ : Primrec Prod.snd<VAR>k : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).1<VAR>n : Primrec fun a => a.1.2<VAR>k' : Primrec Prod.snd<VAR>c : Primrec fun a => (ofNat (ℕ × Code) a.1.1.length).2<GOAL>Primrec fun a => let z := (unpair a.1.1.2).1; let m := (unpair a.1.1.2).2; do let x ← Nat.Partrec.Code.lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) (Nat.pair z m) Nat.casesOn x (some m) fun x => Nat.Partrec.Code.lup a.1.1.1 (a.1.2, (ofNat (ℕ × Code) a.1.1.1.length).2) (Nat.pair z (m + 1))
<VAR>a✝ b✝ : ℤ<VAR>n : ℕ<VAR>a b : ℤ<GOAL>a.natAbs < b.natAbs ↔ a * a < b * b
<VAR>a✝ b✝ : ℤ<VAR>n : ℕ<VAR>a b : ℤ<GOAL>a.natAbs < b.natAbs ↔ ↑a.natAbs < ↑b.natAbs
<VAR>f : ℕ → ℂ<GOAL>abscissaOfAbsConv (logMul f) = abscissaOfAbsConv f
<VAR>f : ℕ → ℂ<VAR>s : ℝ<VAR>hs : abscissaOfAbsConv f < ↑s<GOAL>LSeriesSummable (logMul f) ↑s
<VAR>f : ℕ → ℂ<VAR>s : ℝ<VAR>hs : abscissaOfAbsConv (logMul f) < ↑s<GOAL>LSeriesSummable f ↑s
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>completedCosZeta₀ (-a) s = completedCosZeta₀ a s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹⁵ : CommRing 𝕜<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : AddCommGroup F<VAR>inst✝¹² : AddCommGroup G<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : Module 𝕜 F<VAR>inst✝⁹ : Module 𝕜 G<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : ContinuousConstSMul 𝕜 E<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : ContinuousConstSMul 𝕜 F<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : ContinuousConstSMul 𝕜 G<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : 0 < n<VAR>v : Fin n → E<GOAL>(q.removeZero.comp p n) v = (q.comp p n) v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹⁵ : CommRing 𝕜<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : AddCommGroup F<VAR>inst✝¹² : AddCommGroup G<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : Module 𝕜 F<VAR>inst✝⁹ : Module 𝕜 G<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : ContinuousConstSMul 𝕜 E<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : ContinuousConstSMul 𝕜 F<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : ContinuousConstSMul 𝕜 G<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : 0 < n<VAR>v : Fin n → E<GOAL>∑ x : Composition n, (q.removeZero x.length) (p.applyComposition x v) = ∑ x : Composition n, (q x.length) (p.applyComposition x v)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹⁵ : CommRing 𝕜<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : AddCommGroup F<VAR>inst✝¹² : AddCommGroup G<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : Module 𝕜 F<VAR>inst✝⁹ : Module 𝕜 G<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : ContinuousConstSMul 𝕜 E<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : ContinuousConstSMul 𝕜 F<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : ContinuousConstSMul 𝕜 G<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : 0 < n<VAR>v : Fin n → E<VAR>c : Composition n<VAR>_hc : c ∈ Finset.univ<GOAL>(q.removeZero c.length) (p.applyComposition c v) = (q c.length) (p.applyComposition c v)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>R : Type u_5<GOAL>∀ (v : Fin 0 → α), (circulant v)ᵀ = circulant fun i => v (-i)
<VAR>G : Type u''<VAR>S : Type u'<VAR>R : Type u<VAR>M : Type v<VAR>ι : Type w<VAR>inst✝¹ : Ring R<VAR>inst✝ : AddCommGroup M<VAR>module_M : Module R M<VAR>p p' : Submodule R M<VAR>r : R<VAR>x y : M<VAR>hx : x ∈ p<GOAL>x - y ∈ p ↔ y ∈ p
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F✝ F : Pseudofunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>whiskerLeftIso (F.map f) (F.mapId b) = (F.mapComp f (𝟙 b)).symm ≪≫ F.map₂Iso (ρ_ f) ≪≫ (ρ_ (F.map f)).symm
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>M : Λ → Stmt₂<VAR>k : K<VAR>o : StAct k<VAR>q : Stmt₂<VAR>v : σ<VAR>S : List (Γ k)<VAR>L : ListBlank ((k : K) → Option (Γ k))<VAR>hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse<VAR>n : ℕ<VAR>IH : n ≤ S.length → Reaches₀ (TM1.step (tr M)) { l := some (go k o q), var := v, Tape := Tape.mk' ∅ (addBottom L) } { l := some (go k o q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }<VAR>H : n + 1 ≤ S.length<GOAL>Reaches₀ (TM1.step (tr M)) { l := some (go k o q), var := v, Tape := Tape.mk' ∅ (addBottom L) } { l := some (go k o q), var := v, Tape := (Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom L)) }
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>M : Λ → Stmt₂<VAR>k : K<VAR>o : StAct k<VAR>q : Stmt₂<VAR>v : σ<VAR>S : List (Γ k)<VAR>L : ListBlank ((k : K) → Option (Γ k))<VAR>hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse<VAR>n : ℕ<VAR>IH : n ≤ S.length → Reaches₀ (TM1.step (tr M)) { l := some (go k o q), var := v, Tape := Tape.mk' ∅ (addBottom L) } { l := some (go k o q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }<VAR>H : n + 1 ≤ S.length<GOAL>{ l := some (go k o q), var := v, Tape := (Tape.move Dir.right)^[n + 1] (Tape.mk' ∅ (addBottom L)) } ∈ TM1.step (tr M) { l := some (go k o q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>M : Λ → Stmt₂<VAR>k : K<VAR>o : StAct k<VAR>q : Stmt₂<VAR>v : σ<VAR>S : List (Γ k)<VAR>L : ListBlank ((k : K) → Option (Γ k))<VAR>hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse<VAR>n : ℕ<VAR>IH : n ≤ S.length → Reaches₀ (TM1.step (tr M)) { l := some (go k o q), var := v, Tape := Tape.mk' ∅ (addBottom L) } { l := some (go k o q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }<VAR>H : n + 1 ≤ S.length<GOAL>{ l := some (go k o q), var := v, Tape := Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L))) } ∈ TM1.step (tr M) { l := some (go k o q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>M : Λ → Stmt₂<VAR>k : K<VAR>o : StAct k<VAR>q : Stmt₂<VAR>v : σ<VAR>S : List (Γ k)<VAR>L : ListBlank ((k : K) → Option (Γ k))<VAR>hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse<VAR>n : ℕ<VAR>IH : n ≤ S.length → Reaches₀ (TM1.step (tr M)) { l := some (go k o q), var := v, Tape := Tape.mk' ∅ (addBottom L) } { l := some (go k o q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }<VAR>H : n + 1 ≤ S.length<GOAL>some (bif (L.nth n k).isNone then TM1.stepAux (trStAct (goto fun x x => ret q) o) v ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L))) else { l := some (go k o q), var := v, Tape := Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L))) }) = some { l := some (go k o q), var := v, Tape := Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L))) }
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>M : Λ → Stmt₂<VAR>k : K<VAR>o : StAct k<VAR>q : Stmt₂<VAR>v : σ<VAR>S : List (Γ k)<VAR>L : ListBlank ((k : K) → Option (Γ k))<VAR>hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse<VAR>n : ℕ<VAR>IH : n ≤ S.length → Reaches₀ (TM1.step (tr M)) { l := some (go k o q), var := v, Tape := Tape.mk' ∅ (addBottom L) } { l := some (go k o q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }<VAR>H : n + 1 ≤ S.length<GOAL>some (bif (some (S.reverse.get ⟨n, ?succ⟩)).isNone then TM1.stepAux (trStAct (goto fun x x => ret q) o) v ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L))) else { l := some (go k o q), var := v, Tape := Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L))) }) = some { l := some (go k o q), var := v, Tape := Tape.move Dir.right ((Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L))) }
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>M : Λ → Stmt₂<VAR>k : K<VAR>o : StAct k<VAR>q : Stmt₂<VAR>v : σ<VAR>S : List (Γ k)<VAR>L : ListBlank ((k : K) → Option (Γ k))<VAR>hL : ListBlank.map (proj k) L = ListBlank.mk (List.map some S).reverse<VAR>n : ℕ<VAR>IH : n ≤ S.length → Reaches₀ (TM1.step (tr M)) { l := some (go k o q), var := v, Tape := Tape.mk' ∅ (addBottom L) } { l := some (go k o q), var := v, Tape := (Tape.move Dir.right)^[n] (Tape.mk' ∅ (addBottom L)) }<VAR>H : n + 1 ≤ S.length<GOAL>n < S.reverse.length
<VAR>m₂ m₁ : List Char<VAR>x✝ : Substring<VAR>h : x✝.Valid<VAR>e : x✝.toString.data = m₁.reverse ++ m₂<GOAL>∀ (n : Nat), x✝.prevn n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len (List.drop n m₁) }
<VAR>m₂ m₁ : List Char<VAR>x✝ : Substring<VAR>h✝ : x✝.Valid<VAR>e : x✝.toString.data = m₁.reverse ++ m₂<VAR>l m r : List Char<VAR>h : ValidFor l m r x✝<GOAL>∀ (n : Nat), x✝.prevn n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len (List.drop n m₁) }
<VAR>m₂ m₁ : List Char<VAR>x✝ : Substring<VAR>h✝ : x✝.Valid<VAR>l m r : List Char<VAR>h : ValidFor l m r x✝<VAR>e : m = m₁.reverse ++ m₂<GOAL>∀ (n : Nat), x✝.prevn n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len (List.drop n m₁) }
<VAR>m₂ m₁ : List Char<VAR>x✝ : Substring<VAR>h✝ : x✝.Valid<VAR>l r : List Char<VAR>h : ValidFor l (m₁.reverse ++ m₂) r x✝<GOAL>∀ (n : Nat), x✝.prevn n { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len (List.drop n m₁) }
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Opens X<VAR>hs : Nonempty ↥s<VAR>U V : Opens X<VAR>hU : Nonempty ↥U<VAR>hV : Nonempty ↥V<VAR>hUV : U ≤ V<VAR>i : ↑↑U → ↑↑V := inclusion hUV<VAR>y : Y<VAR>hy : y ∈ (e.subtypeRestr hU).target<GOAL>↑(e.subtypeRestr hV).symm y = (i ∘ ↑(e.subtypeRestr hU).symm) y
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Opens X<VAR>hs : Nonempty ↥s<VAR>U V : Opens X<VAR>hU : Nonempty ↥U<VAR>hV : Nonempty ↥V<VAR>hUV : U ≤ V<VAR>i : ↑↑U → ↑↑V := inclusion hUV<VAR>y : Y<VAR>hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (U.partialHomeomorphSubtypeCoe hU).target<GOAL>↑(V.partialHomeomorphSubtypeCoe hV).symm (↑e.symm y) = i (↑(U.partialHomeomorphSubtypeCoe hU).symm (↑e.symm y))
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Opens X<VAR>hs : Nonempty ↥s<VAR>U V : Opens X<VAR>hU : Nonempty ↥U<VAR>hV : Nonempty ↥V<VAR>hUV : U ≤ V<VAR>i : ↑↑U → ↑↑V := inclusion hUV<VAR>y : Y<VAR>hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (U.partialHomeomorphSubtypeCoe hU).target<VAR>hyV : ↑e.symm y ∈ (V.partialHomeomorphSubtypeCoe hV).target<GOAL>↑(V.partialHomeomorphSubtypeCoe hV).symm (↑e.symm y) = i (↑(U.partialHomeomorphSubtypeCoe hU).symm (↑e.symm y))
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Opens X<VAR>hs : Nonempty ↥s<VAR>U V : Opens X<VAR>hU : Nonempty ↥U<VAR>hV : Nonempty ↥V<VAR>hUV : U ≤ V<VAR>i : ↑↑U → ↑↑V := inclusion hUV<VAR>y : Y<VAR>hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (U.partialHomeomorphSubtypeCoe hU).target<VAR>hyV : ↑e.symm y ∈ (V.partialHomeomorphSubtypeCoe hV).target<GOAL>↑(V.partialHomeomorphSubtypeCoe hV).symm (↑e.symm y) ∈ (V.partialHomeomorphSubtypeCoe hV).source
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Opens X<VAR>hs : Nonempty ↥s<VAR>U V : Opens X<VAR>hU : Nonempty ↥U<VAR>hV : Nonempty ↥V<VAR>hUV : U ≤ V<VAR>i : ↑↑U → ↑↑V := inclusion hUV<VAR>y : Y<VAR>hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (U.partialHomeomorphSubtypeCoe hU).target<VAR>hyV : ↑e.symm y ∈ (V.partialHomeomorphSubtypeCoe hV).target<GOAL>↑(V.partialHomeomorphSubtypeCoe hV) (↑(V.partialHomeomorphSubtypeCoe hV).symm (↑e.symm y)) = ↑(V.partialHomeomorphSubtypeCoe hV) (i (↑(U.partialHomeomorphSubtypeCoe hU).symm (↑e.symm y)))
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>i j k : n<GOAL>A i k * A.adjugate k j = Aᵀ.cramer (Pi.single k (A i k)) j
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>f : R[X]<VAR>n : WithBot ℕ<GOAL>f.degree ≤ n ↔ ∀ (m : ℕ), n < ↑m → f.coeff m = 0
<VAR>x y : EReal<GOAL>-x * y = -(x * y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : ι → Set (Set α)<GOAL>⋂₀ ⋃ i, s i = ⋂ i, ⋂₀ s i
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>a : R<VAR>ha : a ∈ nonZeroDivisors R<VAR>b : S<VAR>e : b * (algebraMap R S) a = 0<GOAL>b = 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>a : R<VAR>ha : a ∈ nonZeroDivisors R<VAR>x : R<VAR>s : ↥M<VAR>e : mk' S x s * (algebraMap R S) a = 0<GOAL>mk' S x s = 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>a : R<VAR>ha : a ∈ nonZeroDivisors R<VAR>x : R<VAR>s : ↥M<VAR>e : ∃ c, ↑c * (↑1 * (x * a)) = ↑c * (↑(s * 1) * 0)<GOAL>mk' S x s = 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>a : R<VAR>ha : a ∈ nonZeroDivisors R<VAR>x : R<VAR>s c : ↥M<VAR>e : ↑c * (↑1 * (x * a)) = ↑c * (↑(s * 1) * 0)<GOAL>mk' S x s = 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>a : R<VAR>ha : a ∈ nonZeroDivisors R<VAR>x : R<VAR>s c : ↥M<VAR>e : ↑c * x * a = 0<GOAL>mk' S x s = 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>a : R<VAR>ha : a ∈ nonZeroDivisors R<VAR>x : R<VAR>s c : ↥M<VAR>e : ↑c * x * a = 0<GOAL>∃ m, ↑m * x = 0
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>φ : MultilinearMap R s E<VAR>f : (i : ι) → s i<GOAL>(liftAux φ) ((tprod R) f) = φ f
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>φ : MultilinearMap R s E<VAR>f : (i : ι) → s i<GOAL>((addConGen (Eqv R s)).lift (FreeAddMonoid.lift fun p => p.1 • φ p.2) ⋯) ↑(FreeAddMonoid.of (1, f)) = φ f
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>φ : MultilinearMap R s E<VAR>f : (i : ι) → s i<GOAL>(FreeAddMonoid.lift fun p => p.1 • φ p.2) (FreeAddMonoid.of (1, f)) = φ f
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>φ : MultilinearMap R s E<VAR>f : (i : ι) → s i<GOAL>(FreeAddMonoid.lift fun p => p.1 • φ p.2) ((Equiv.refl (List (R × ((i : ι) → s i)))) [(1, f)]) = φ f
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>φ : MultilinearMap R s E<VAR>f : (i : ι) → s i<GOAL>(FreeAddMonoid.lift fun p => p.1 • φ p.2) ((Equiv.refl (List (R × ((i : ι) → s i)))) [(1, f)]) = 1 • φ f
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>φ : MultilinearMap R s E<VAR>f : (i : ι) → s i<GOAL>(FreeAddMonoid.sumAux.match_1 (fun x => E) (List.map (fun p => p.1 • φ p.2) (FreeAddMonoid.toList ((Equiv.refl (List (R × ((i : ι) → s i)))) [(1, f)]))) (fun _ => 0) fun x xs => List.foldl (fun x x_1 => x + x_1) x xs) = 1 • φ f
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>φ : MultilinearMap R s E<VAR>f : (i : ι) → s i<GOAL>1 • φ f = φ f
<VAR>p a b : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>padicValNat p (p ^ n) = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>f g : ι → α<VAR>s t u : Set α<VAR>a b : α<VAR>hr : Symmetric r<VAR>ha : a ∉ s<GOAL>(insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, r a b