ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : CountableOrCountablyGenerated α β<VAR>κ : Kernel α (β × Ω)<VAR>inst✝² : IsFiniteKernel κ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>a : α<VAR>t : Set Ω<VAR>ht : MeasurableSet t<VAR>hf : IntegrableOn f (Set.univ ×ˢ t) (κ a)<GOAL>∫ (b : β), ∫ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (b : β) in Set.univ, ∫ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>inst✝² : One M<VAR>inst✝¹ : One N<VAR>inst✝ : One P<VAR>f : α → M<VAR>k : Set α<VAR>h : mulSupport f ⊆ k<GOAL>range f = f '' k ∨ range f = insert 1 (f '' k)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>inst✝² : One M<VAR>inst✝¹ : One N<VAR>inst✝ : One P<VAR>f : α → M<VAR>k : Set α<VAR>h : mulSupport f ⊆ k<GOAL>range f ≤ insert 1 (f '' k)
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>inst✝⁵ : CompleteSpace E'<VAR>inst✝⁴ : NormedSpace ℝ E'<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>hm : m ≤ m0<VAR>f g : ↥(Lp E' p μ)<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑f) s μ<VAR>hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑g) s μ<VAR>hfg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ<VAR>hf_meas : AEStronglyMeasurable' m (↑↑f) μ<VAR>hg_meas : AEStronglyMeasurable' m (↑↑g) μ<GOAL>↑↑f =ᶠ[ae μ] ↑↑g
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>inst✝⁵ : CompleteSpace E'<VAR>inst✝⁴ : NormedSpace ℝ E'<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>hm : m ≤ m0<VAR>f g : ↥(Lp E' p μ)<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑f) s μ<VAR>hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑g) s μ<VAR>hfg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ<VAR>hf_meas : AEStronglyMeasurable' m (↑↑f) μ<VAR>hg_meas : AEStronglyMeasurable' m (↑↑g) μ<GOAL>↑↑(f - g) =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>inst✝⁵ : CompleteSpace E'<VAR>inst✝⁴ : NormedSpace ℝ E'<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>hm : m ≤ m0<VAR>f g : ↥(Lp E' p μ)<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑f) s μ<VAR>hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑g) s μ<VAR>hfg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ<VAR>hf_meas : AEStronglyMeasurable' m (↑↑f) μ<VAR>hg_meas : AEStronglyMeasurable' m (↑↑g) μ<VAR>hfg' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑(f - g) x ∂μ = 0<GOAL>↑↑(f - g) =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>inst✝⁵ : CompleteSpace E'<VAR>inst✝⁴ : NormedSpace ℝ E'<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>hm : m ≤ m0<VAR>f g : ↥(Lp E' p μ)<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑f) s μ<VAR>hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑g) s μ<VAR>hfg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ<VAR>hf_meas : AEStronglyMeasurable' m (↑↑f) μ<VAR>hg_meas : AEStronglyMeasurable' m (↑↑g) μ<VAR>hfg' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑(f - g) x ∂μ = 0<VAR>hfg_int : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑(f - g)) s μ<GOAL>↑↑(f - g) =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>inst✝⁵ : CompleteSpace E'<VAR>inst✝⁴ : NormedSpace ℝ E'<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>hm : m ≤ m0<VAR>f g : ↥(Lp E' p μ)<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑f) s μ<VAR>hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑g) s μ<VAR>hfg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ<VAR>hf_meas : AEStronglyMeasurable' m (↑↑f) μ<VAR>hg_meas : AEStronglyMeasurable' m (↑↑g) μ<VAR>hfg' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑(f - g) x ∂μ = 0<VAR>hfg_int : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑(f - g)) s μ<VAR>hfg_meas : AEStronglyMeasurable' m (↑↑(f - g)) μ<GOAL>↑↑(f - g) =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n✝ : ℕ<VAR>s : Finset α<VAR>n : ℕ<GOAL>G.CliqueFree n ↔ IsEmpty (⊤ ↪g G)
<VAR>x : ℝ<GOAL>0 ≤ expNegInvGlue x
<VAR>m : Type u_1<VAR>n✝ : Type u_2<VAR>inst✝⁴ : DecidableEq n✝<VAR>inst✝³ : Fintype n✝<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>k✝ : Fin (n + 1)<VAR>k : Fin n<VAR>ih : ∀ (c : Fin n → R), (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) → ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R}, (∀ (j : Fin n.succ), M 0 j = N 0 j) → (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det<VAR>c : Fin n → R<VAR>hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0<VAR>M N : Matrix (Fin n.succ) (Fin n.succ) R<VAR>h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j<VAR>hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j<VAR>M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)<VAR>hM' : M' = M.updateRow k.succ (N k.succ)<VAR>hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)<GOAL>M.det = N.det
<VAR>m : Type u_1<VAR>n✝ : Type u_2<VAR>inst✝⁴ : DecidableEq n✝<VAR>inst✝³ : Fintype n✝<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>k✝ : Fin (n + 1)<VAR>k : Fin n<VAR>ih : ∀ (c : Fin n → R), (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) → ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R}, (∀ (j : Fin n.succ), M 0 j = N 0 j) → (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det<VAR>c : Fin n → R<VAR>hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0<VAR>M N : Matrix (Fin n.succ) (Fin n.succ) R<VAR>h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j<VAR>hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j<VAR>M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)<VAR>hM' : M' = M.updateRow k.succ (N k.succ)<VAR>hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)<VAR>k_ne_succ : k.castSucc ≠ k.succ<GOAL>M.det = N.det
<VAR>m : Type u_1<VAR>n✝ : Type u_2<VAR>inst✝⁴ : DecidableEq n✝<VAR>inst✝³ : Fintype n✝<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>k✝ : Fin (n + 1)<VAR>k : Fin n<VAR>ih : ∀ (c : Fin n → R), (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) → ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R}, (∀ (j : Fin n.succ), M 0 j = N 0 j) → (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det<VAR>c : Fin n → R<VAR>hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0<VAR>M N : Matrix (Fin n.succ) (Fin n.succ) R<VAR>h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j<VAR>hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j<VAR>M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)<VAR>hM' : M' = M.updateRow k.succ (N k.succ)<VAR>hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)<VAR>k_ne_succ : k.castSucc ≠ k.succ<VAR>M_k : M k.castSucc = M' k.castSucc<GOAL>M.det = N.det
<VAR>m : Type u_1<VAR>n✝ : Type u_2<VAR>inst✝⁴ : DecidableEq n✝<VAR>inst✝³ : Fintype n✝<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>k✝ : Fin (n + 1)<VAR>k : Fin n<VAR>ih : ∀ (c : Fin n → R), (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) → ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R}, (∀ (j : Fin n.succ), M 0 j = N 0 j) → (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det<VAR>c : Fin n → R<VAR>hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0<VAR>M N : Matrix (Fin n.succ) (Fin n.succ) R<VAR>h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j<VAR>hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j<VAR>M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)<VAR>hM' : M' = M.updateRow k.succ (N k.succ)<VAR>hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)<VAR>k_ne_succ : k.castSucc ≠ k.succ<VAR>M_k : M k.castSucc = M' k.castSucc<GOAL>∀ (i : Fin n), k.castSucc < i.succ → update c k 0 i = 0
<VAR>m : Type u_1<VAR>n✝ : Type u_2<VAR>inst✝⁴ : DecidableEq n✝<VAR>inst✝³ : Fintype n✝<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>k✝ : Fin (n + 1)<VAR>k : Fin n<VAR>ih : ∀ (c : Fin n → R), (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) → ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R}, (∀ (j : Fin n.succ), M 0 j = N 0 j) → (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det<VAR>c : Fin n → R<VAR>hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0<VAR>M N : Matrix (Fin n.succ) (Fin n.succ) R<VAR>h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j<VAR>hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j<VAR>M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)<VAR>hM' : M' = M.updateRow k.succ (N k.succ)<VAR>hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)<VAR>k_ne_succ : k.castSucc ≠ k.succ<VAR>M_k : M k.castSucc = M' k.castSucc<GOAL>∀ (j : Fin n.succ), M' 0 j = N 0 j
<VAR>m : Type u_1<VAR>n✝ : Type u_2<VAR>inst✝⁴ : DecidableEq n✝<VAR>inst✝³ : Fintype n✝<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>k✝ : Fin (n + 1)<VAR>k : Fin n<VAR>ih : ∀ (c : Fin n → R), (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) → ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R}, (∀ (j : Fin n.succ), M 0 j = N 0 j) → (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det<VAR>c : Fin n → R<VAR>hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0<VAR>M N : Matrix (Fin n.succ) (Fin n.succ) R<VAR>h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j<VAR>hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j<VAR>M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)<VAR>hM' : M' = M.updateRow k.succ (N k.succ)<VAR>hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)<VAR>k_ne_succ : k.castSucc ≠ k.succ<VAR>M_k : M k.castSucc = M' k.castSucc<GOAL>∀ (i : Fin n) (j : Fin n.succ), M' i.succ j = N i.succ j + update c k 0 i * M' i.castSucc j
<VAR>m : Type u_1<VAR>n✝ : Type u_2<VAR>inst✝⁴ : DecidableEq n✝<VAR>inst✝³ : Fintype n✝<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>k✝ : Fin (n + 1)<VAR>k : Fin n<VAR>ih : ∀ (c : Fin n → R), (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) → ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R}, (∀ (j : Fin n.succ), M 0 j = N 0 j) → (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det<VAR>c : Fin n → R<VAR>hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0<VAR>M N : Matrix (Fin n.succ) (Fin n.succ) R<VAR>h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j<VAR>hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j<VAR>M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)<VAR>hM' : M' = M.updateRow k.succ (N k.succ)<VAR>hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)<VAR>k_ne_succ : k.castSucc ≠ k.succ<VAR>M_k : M k.castSucc = M' k.castSucc<VAR>i : Fin n<VAR>j : Fin n.succ<GOAL>M' i.succ j = N i.succ j + update c k 0 i * M' i.castSucc j
<VAR>m : Type u_1<VAR>n✝ : Type u_2<VAR>inst✝⁴ : DecidableEq n✝<VAR>inst✝³ : Fintype n✝<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>k✝ : Fin (n + 1)<VAR>k : Fin n<VAR>ih : ∀ (c : Fin n → R), (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) → ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R}, (∀ (j : Fin n.succ), M 0 j = N 0 j) → (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det<VAR>c : Fin n → R<VAR>hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0<VAR>M N : Matrix (Fin n.succ) (Fin n.succ) R<VAR>h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j<VAR>hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j<VAR>M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)<VAR>hM' : M' = M.updateRow k.succ (N k.succ)<VAR>hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)<VAR>k_ne_succ : k.castSucc ≠ k.succ<VAR>M_k : M k.castSucc = M' k.castSucc<VAR>i : Fin n<VAR>j : Fin n.succ<GOAL>M' i.succ j = N i.succ j + (if i = k then 0 else c i) * M' i.castSucc j
<VAR>m : Type u_1<VAR>n✝ : Type u_2<VAR>inst✝⁴ : DecidableEq n✝<VAR>inst✝³ : Fintype n✝<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>k✝ : Fin (n + 1)<VAR>k : Fin n<VAR>ih : ∀ (c : Fin n → R), (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) → ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R}, (∀ (j : Fin n.succ), M 0 j = N 0 j) → (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det<VAR>c : Fin n → R<VAR>hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0<VAR>M N : Matrix (Fin n.succ) (Fin n.succ) R<VAR>h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j<VAR>hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j<VAR>M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)<VAR>hM' : M' = M.updateRow k.succ (N k.succ)<VAR>hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)<VAR>k_ne_succ : k.castSucc ≠ k.succ<VAR>M_k : M k.castSucc = M' k.castSucc<VAR>i : Fin n<VAR>j : Fin n.succ<VAR>hik : ¬i = k<GOAL>M' i.succ j = N i.succ j + c i * M' i.castSucc j
<VAR>m : Type u_1<VAR>n✝ : Type u_2<VAR>inst✝⁴ : DecidableEq n✝<VAR>inst✝³ : Fintype n✝<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>k✝ : Fin (n + 1)<VAR>k : Fin n<VAR>ih : ∀ (c : Fin n → R), (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) → ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R}, (∀ (j : Fin n.succ), M 0 j = N 0 j) → (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det<VAR>c : Fin n → R<VAR>hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0<VAR>M N : Matrix (Fin n.succ) (Fin n.succ) R<VAR>h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j<VAR>hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j<VAR>M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)<VAR>hM' : M' = M.updateRow k.succ (N k.succ)<VAR>hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)<VAR>k_ne_succ : k.castSucc ≠ k.succ<VAR>M_k : M k.castSucc = M' k.castSucc<VAR>i : Fin n<VAR>j : Fin n.succ<VAR>hik : ¬i = k<GOAL>N i.succ j + c i * M i.castSucc j = N i.succ j + c i * M.updateRow k.succ (N k.succ) i.castSucc j
<VAR>m : Type u_1<VAR>n✝ : Type u_2<VAR>inst✝⁴ : DecidableEq n✝<VAR>inst✝³ : Fintype n✝<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>k✝ : Fin (n + 1)<VAR>k : Fin n<VAR>ih : ∀ (c : Fin n → R), (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) → ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R}, (∀ (j : Fin n.succ), M 0 j = N 0 j) → (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det<VAR>c : Fin n → R<VAR>hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0<VAR>M N : Matrix (Fin n.succ) (Fin n.succ) R<VAR>h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j<VAR>hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j<VAR>M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)<VAR>hM' : M' = M.updateRow k.succ (N k.succ)<VAR>hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)<VAR>k_ne_succ : k.castSucc ≠ k.succ<VAR>M_k : M k.castSucc = M' k.castSucc<VAR>i : Fin n<VAR>j : Fin n.succ<VAR>hik : ¬i = k<VAR>hik2 : ¬k < i<GOAL>N i.succ j + c i * M i.castSucc j = N i.succ j + c i * M.updateRow k.succ (N k.succ) i.castSucc j
<VAR>m : Type u_1<VAR>n✝ : Type u_2<VAR>inst✝⁴ : DecidableEq n✝<VAR>inst✝³ : Fintype n✝<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>k✝ : Fin (n + 1)<VAR>k : Fin n<VAR>ih : ∀ (c : Fin n → R), (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) → ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R}, (∀ (j : Fin n.succ), M 0 j = N 0 j) → (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det<VAR>c : Fin n → R<VAR>hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0<VAR>M N : Matrix (Fin n.succ) (Fin n.succ) R<VAR>h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j<VAR>hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j<VAR>M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)<VAR>hM' : M' = M.updateRow k.succ (N k.succ)<VAR>hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)<VAR>k_ne_succ : k.castSucc ≠ k.succ<VAR>M_k : M k.castSucc = M' k.castSucc<VAR>i : Fin n<VAR>j : Fin n.succ<VAR>hik : ¬i = k<VAR>hik2 : ¬k < i<GOAL>i.castSucc ≠ k.succ
<VAR>m : Type u_1<VAR>n✝ : Type u_2<VAR>inst✝⁴ : DecidableEq n✝<VAR>inst✝³ : Fintype n✝<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>k✝ : Fin (n + 1)<VAR>k : Fin n<VAR>ih : ∀ (c : Fin n → R), (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) → ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R}, (∀ (j : Fin n.succ), M 0 j = N 0 j) → (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det<VAR>c : Fin n → R<VAR>hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0<VAR>M N : Matrix (Fin n.succ) (Fin n.succ) R<VAR>h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j<VAR>hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j<VAR>M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)<VAR>hM' : M' = M.updateRow k.succ (N k.succ)<VAR>hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)<VAR>k_ne_succ : k.castSucc ≠ k.succ<VAR>M_k : M k.castSucc = M' k.castSucc<VAR>i : Fin n<VAR>j : Fin n.succ<VAR>hik : ¬i = k<VAR>hik2 : ¬k < i<GOAL>i.castSucc < k.succ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁴ : CommSemiring R<VAR>inst✝¹³ : StarRing R<VAR>inst✝¹² : MetricSpace R<VAR>inst✝¹¹ : TopologicalSemiring R<VAR>inst✝¹⁰ : ContinuousStar R<VAR>inst✝⁹ : TopologicalSpace A<VAR>inst✝⁸ : Ring A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : ContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a✝ : A<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>hf : autoParam (ContinuousOn f (spectrum R a✝)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a✝)) _auto✝<VAR>S : Type u_3<VAR>inst✝⁴ : SMul S R<VAR>inst✝³ : ContinuousConstSMul S R<VAR>inst✝² : SMulZeroClass S A<VAR>inst✝¹ : IsScalarTower S R A<VAR>inst✝ : IsScalarTower S R (R → R)<VAR>s : S<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<GOAL>cfc (fun x => s • x) a = s • a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CommMonoid β<VAR>n : ℕ<VAR>f : Fin (n + 1) → β<GOAL>∏ i : Fin (n + 1), f i = (∏ i : Fin n, f i.castSucc) * f (last n)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.189232, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>K : CochainComplex C ℤ<VAR>n m : ℤ<VAR>α : Cochain K F m<VAR>β : Cochain K G n<VAR>h : n + 1 = m<VAR>m' : ℤ<VAR>hm' : m + 1 = m'<GOAL>δ n m (α.comp (inl φ) ⋯ + β.comp (Cochain.ofHom (inr φ)) ⋯) = -(δ m m' α).comp (inl φ) ⋯ + (δ n m β + α.comp (Cochain.ofHom φ) ⋯).comp (Cochain.ofHom (inr φ)) ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.189232, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>K : CochainComplex C ℤ<VAR>n m : ℤ<VAR>α : Cochain K F m<VAR>β : Cochain K G n<VAR>h : n + 1 = m<VAR>m' : ℤ<VAR>hm' : m + 1 = m'<GOAL>α.comp ((Cochain.ofHom φ).comp (Cochain.ofHom (inr φ)) ⋯) ⋯ + -(δ m m' α).comp (inl φ) ⋯ + (δ n m β).comp (Cochain.ofHom (inr φ)) ⋯ = -(δ m m' α).comp (inl φ) ⋯ + ((δ n m β).comp (Cochain.ofHom (inr φ)) ⋯ + α.comp ((Cochain.ofHom φ).comp (Cochain.ofHom (inr φ)) ⋯) ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁵ : Zero α<VAR>inst✝⁴ : Zero β<VAR>inst✝³ : SMulZeroClass α β<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : PosSMulStrictMono α β<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>0 < a • b
<VAR>α : Type u_1<GOAL>ofNat' 1 = 1
<VAR>α : Type u_1<GOAL>(match (motive := Bool → Num → Num) true with | true => Num.bit1 | false => Num.bit0) 0 = 1
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H : Subgroup G<VAR>A : Type u_2<VAR>inst✝¹ : CommGroup A<VAR>ϕ : ↥H →* A<VAR>T : ↑(leftTransversals ↑H)<VAR>inst✝ : H.FiniteIndex<VAR>g : G<GOAL>ϕ.transfer g = diff ϕ T (g • T)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<GOAL>Memℒp (fun x => ‖f x‖ ^ p.toReal) 1 μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → E<VAR>hf : Memℒp f p μ<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<GOAL>1 = p / p
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : Fintype α<VAR>s t : Finset α<GOAL>Eₘ[univ, t] = Fintype.card α * t.card ^ 2
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : Fintype α<VAR>s t : Finset α<GOAL>(filter (fun x => x.1.1 * x.2.1 = x.1.2 * x.2.2) (univ ×ˢ t ×ˢ t)).card = (univ ×ˢ t ×ˢ t).card
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : Fintype α<VAR>s t : Finset α<VAR>f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)<GOAL>(filter (fun x => x.1.1 * x.2.1 = x.1.2 * x.2.2) (univ ×ˢ t ×ˢ t)).card = (univ ×ˢ t ×ˢ t).card