✖ [7030/7059] Building Mathlib.Probability.Independence.Kernel
trace: .> LEAN_PATH=/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/packages/Cli/.lake/build/lib/lean:/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/packages/batteries/.lake/build/lib/lean:/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/packages/Qq/.lake/build/lib/lean:/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/packages/aesop/.lake/build/lib/lean:/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/packages/importGraph/.lake/build/lib/lean:/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/packages/plausible/.lake/build/lib/lean:/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/build/lib/lean /home/lean/.elan/toolchains/leanprover--lean4---v4.22.0-rc4/bin/lean /home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/Mathlib/Probability/Independence/Kernel.lean -o /home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/build/lib/lean/Mathlib/Probability/Independence/Kernel.olean -i /home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/build/lib/lean/Mathlib/Probability/Independence/Kernel.ilean -c /home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/build/ir/Mathlib/Probability/Independence/Kernel.c --setup /home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/build/ir/Mathlib/Probability/Independence/Kernel.setup.json --json
Error: error: Mathlib/Probability/Independence/Kernel.lean:1074:6: `grind` failed
case grind.1.1.1.1.1.1
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
S T : Finset ι
hST : Disjoint S T
hf_Indep : iIndepFun f κ μ
hf_meas : ∀ (i : ι), Measurable (f i)
hμ : ¬μ = 0
η : Kernel α Ω
η_eq : ⇑κ =ᶠ[ae μ] ⇑η
hη : IsMarkovKernel η
hπS_pi : IsPiSystem {s | ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπS_gen :
  MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi =
    generateFrom {s | ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπT_pi : IsPiSystem {s | ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
hπT_gen :
  MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi =
    generateFrom {s | ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
s : Set ((i : ↥S) → β i.1)
sets_s : (i : ↥S) → Set (β i.1)
hs2 : univ.pi sets_s = s
t : Set ((i : ↥T) → β i.1)
sets_t : (i : ↥T) → Set (β i.1)
ht2 : univ.pi sets_t = t
hs1 : ∀ (i : ↥S), MeasurableSet (sets_s i)
ht1 : ∀ (i : ↥T), MeasurableSet (sets_t i)
h_sets_s'_eq : ∀ {i : ι} (hi : i ∈ S), (if hi : i ∈ S then sets_s ⟨i, hi⟩ else univ) = sets_s ⟨i, hi⟩
h_sets_s'_univ : ∀ {i : ι}, i ∈ T → (if hi : i ∈ S then sets_s ⟨i, hi⟩ else univ) = univ
h_sets_t'_univ : ∀ {i : ι}, i ∈ S → (if hi : i ∈ T then sets_t ⟨i, hi⟩ else univ) = univ
h_meas_s' : ∀ i ∈ S, MeasurableSet (if hi : i ∈ S then sets_s ⟨i, hi⟩ else univ)
h_meas_t' : ∀ i ∈ T, MeasurableSet (if hi : i ∈ T then sets_t ⟨i, hi⟩ else univ)
h_eq_inter_S : (fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_s = ⋂ i ∈ S, f i ⁻¹' if hi : i ∈ S then sets_s ⟨i, hi⟩ else univ
x : Ω
h : ∀ i ∈ T, f i x ∈ if hi : i ∈ T then sets_t ⟨i, hi⟩ else univ
val : ι
property : val ∈ T
h_1 : f val x ∉ sets_t ⟨val, ⋯⟩
h_2 :
  (fun s ↦ ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s) = fun s ↦
    ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s
h_3 : {_a | False} = fun s ↦ ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s
h_4 : {_a | False} = univ
h_5 : univ = fun s ↦ ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s
h_6 : univ = fun s ↦ ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s
h_7 : {_a | False} = fun s ↦ ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s
⊢ False
[grind] Goal diagnostics
  [facts] Asserted facts
    [prop] Disjoint S T
    [prop] iIndepFun f κ μ
    [prop] ∀ (i : ι), Measurable (f i)
    [prop] ¬μ = 0
    [prop] ⇑κ =ᶠ[ae μ] ⇑η
    [prop] IsMarkovKernel η
    [prop] IsPiSystem {s | ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
    [prop] MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi =
          generateFrom {s | ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
    [prop] IsPiSystem {s | ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
    [prop] MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi =
          generateFrom {s | ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
    [prop] univ.pi sets_s = s
    [prop] univ.pi sets_t = t
    [prop] ∀ (i : ↥S), MeasurableSet (sets_s i)
    [prop] ∀ (i : ↥T), MeasurableSet (sets_t i)
    [prop] ∀ {i : ι} (hi : i ∈ S), (if hi : i ∈ S then sets_s ⟨i, hi⟩ else univ) = sets_s ⟨i, hi⟩
    [prop] ∀ {i : ι}, i ∈ T → (if hi : i ∈ S then sets_s ⟨i, hi⟩ else univ) = univ
    [prop] ∀ {i : ι}, i ∈ S → (if hi : i ∈ T then sets_t ⟨i, hi⟩ else univ) = univ
    [prop] ∀ i ∈ S, MeasurableSet (if hi : i ∈ S then sets_s ⟨i, hi⟩ else univ)
    [prop] ∀ i ∈ T, MeasurableSet (if hi : i ∈ T then sets_t ⟨i, hi⟩ else univ)
    [prop] (fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_s = ⋂ i ∈ S, f i ⁻¹' if hi : i ∈ S then sets_s ⟨i, hi⟩ else univ
    [prop] ∀ i ∈ T, f i x ∈ if hi : i ∈ T then sets_t ⟨i, hi⟩ else univ
    [prop] val ∈ T
    [prop] f val x ∉ sets_t ⟨val, ⋯⟩
    [prop] Measurable (f val)
    [prop] {_x | True} = univ
    [prop] {_a | False} = ∅
    [prop] MeasurableSet (sets_t ⟨val, ⋯⟩)
    [prop] (fun s ↦ ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s) = fun s ↦
          ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s
    [prop] {_a | False} = fun s ↦ ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s
    [prop] {_a | False} = univ
    [prop] univ = fun s ↦ ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s
    [prop] univ = fun s ↦ ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s
    [prop] {_a | False} = fun s ↦ ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s
  [eqc] True propositions
    [prop] IsPiSystem {s | ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
    [prop] IsPiSystem {s | ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
    [prop] (fun s ↦ ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s) = fun s ↦
          ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s
    [prop] OuterMeasureClass (Measure α) α
    [prop] Disjoint S T
    [prop] ⇑κ =ᶠ[ae μ] ⇑η
    [prop] val ∈ T
    [prop] IsMarkovKernel η
    [prop] iIndepFun f κ μ
    [prop] ∀ (i : ι), Measurable (f i)
    [prop] ∀ {i : ι} (hi : i ∈ S), (if hi : i ∈ S then sets_s ⟨i, hi⟩ else univ) = sets_s ⟨i, hi⟩
    [prop] ∀ {i : ι}, i ∈ S → (if hi : i ∈ T then sets_t ⟨i, hi⟩ else univ) = univ
    [prop] ∀ i ∈ S, MeasurableSet (if hi : i ∈ S then sets_s ⟨i, hi⟩ else univ)
    [prop] ∀ {i : ι}, i ∈ T → (if hi : i ∈ S then sets_s ⟨i, hi⟩ else univ) = univ
    [prop] ∀ i ∈ T, MeasurableSet (if hi : i ∈ T then sets_t ⟨i, hi⟩ else univ)
    [prop] ∀ i ∈ T, f i x ∈ if hi : i ∈ T then sets_t ⟨i, hi⟩ else univ
    [prop] ∀ (i : ↥S), MeasurableSet (sets_s i)
    [prop] ∀ (i : ↥T), MeasurableSet (sets_t i)
    [prop] MeasurableSet (sets_t ⟨val, ⋯⟩)
    [prop] Measurable (f val)
  [eqc] False propositions
    [prop] μ = 0
    [prop] f val x ∈ sets_t ⟨val, ⋯⟩
  [eqc] Equivalence classes
    [eqc] {s, univ.pi sets_s}
    [eqc] {t, univ.pi sets_t}
    [eqc] {generateFrom {s | ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s},
        generateFrom {s | ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s},
        MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi,
        MeasurableSpace.comap (fun a i ↦ f (↑i) a) MeasurableSpace.pi}
    [eqc] {{s | ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s},
        {s | ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s}}
    [eqc] {⋂ i ∈ S, f i ⁻¹' if hi : i ∈ S then sets_s ⟨i, hi⟩ else univ, (fun a i ↦ f (↑i) a) ⁻¹' univ.pi sets_s}
    [eqc] {Membership.mem S, fun x ↦ x ∈ S}
    [eqc] {Membership.mem T, fun x ↦ x ∈ T}
    [eqc] {fun s ↦ ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s,
        fun s ↦ ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s,
        univ,
        ∅,
        {_a | False},
        {_x | True}}
    [eqc] {(fun _a ↦ False) = fun s ↦
          ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s,
        (fun _a ↦ False) = fun s ↦
          ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
    [eqc] {(fun _x ↦ True) = fun s ↦
          ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s,
        (fun _x ↦ True) = fun s ↦
          ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s}
  [cases] Case analyses
    [cases] [1/2]: (fun s ↦ ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s) =
          fun s ↦ ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s
      [cases] source: Initial goal
    [cases] [1/2]: (fun _a ↦ False) = fun s ↦
          ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s
      [cases] source: E-matching setOf_false
    [cases] [1/2]: (fun _a ↦ False) = fun _x ↦ True
      [cases] source: E-matching setOf_false
    [cases] [1/2]: (fun _x ↦ True) = fun s ↦
          ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s
      [cases] source: E-matching setOf_true
    [cases] [1/2]: (fun _x ↦ True) = fun s ↦
          ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s
      [cases] source: E-matching setOf_true
    [cases] [1/2]: (fun _a ↦ False) = fun s ↦
          ∃ t ∈ univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s}, (fun a i ↦ f (↑i) a) ⁻¹' t = s
      [cases] source: E-matching setOf_false
  [ematch] E-matching patterns
    [thm] hf_meas: [f #0]
    [thm] hf_meas: [f #0]
    [thm] setOf_true: [@setOf #0 _]
    [thm] setOf_false: [@setOf #0 _]
    [thm] Multiset.notMem_zero: [@Membership.mem #1 _ _ (@OfNat.ofNat _ `[0] _) #0]
    [thm] mem_pi: [@Membership.mem _ _ _ (@Set.pi #4 #3 #2 #1) #0]
    [thm] mem_univ: [@Membership.mem #1 _ _ (@univ _) #0]
    [thm] hs1: [sets_s #0]
    [thm] hs1: [sets_s #0]
    [thm] ht1: [sets_t #0]
    [thm] ht1: [sets_t #0]
    [thm] h_sets_s'_eq: [@Membership.mem `[ι] `[Finset ι] `[Finset.instMembership] `[S] #1]
    [thm] h_sets_s'_eq: [@Membership.mem `[ι] `[Finset ι] `[Finset.instMembership] `[S] #1]
    [thm] h_sets_s'_univ: [@Membership.mem `[ι] `[Finset ι] `[Finset.instMembership] `[T] #1]
    [thm] h_sets_s'_univ: [@Membership.mem `[ι] `[Finset ι] `[Finset.instMembership] `[S] #1]
    [thm] h_sets_t'_univ: [@Membership.mem `[ι] `[Finset ι] `[Finset.instMembership] `[S] #1]
    [thm] h_sets_t'_univ: [@Membership.mem `[ι] `[Finset ι] `[Finset.instMembership] `[T] #1]
    [thm] h_meas_s': [@Membership.mem `[ι] `[Finset ι] `[Finset.instMembership] `[S] #1]
    [thm] h_meas_s': [@Membership.mem `[ι] `[Finset ι] `[Finset.instMembership] `[S] #1]
    [thm] h_meas_t': [@Membership.mem `[ι] `[Finset ι] `[Finset.instMembership] `[T] #1]
    [thm] h_meas_t': [@Membership.mem `[ι] `[Finset ι] `[Finset.instMembership] `[T] #1]
    [thm] mem_preimage: [@Membership.mem #4 _ _ (@preimage _ #3 #2 #1) #0]
    [thm] h: [@Membership.mem `[ι] `[Finset ι] `[Finset.instMembership] `[T] #1]
    [thm] h: [@Membership.mem `[ι] `[Finset ι] `[Finset.instMembership] `[T] #1]
    [thm] mem_empty_iff_false: [@Membership.mem #1 _ _ (@EmptyCollection.emptyCollection _ _) #0]
    [thm] Finset.notMem_empty: [@Membership.mem #1 (Finset _) _ (@EmptyCollection.emptyCollection (Finset _) _) #0]
[grind] Diagnostics
  [thm] E-Matching instances
    [thm] setOf_false ↦ 1
    [thm] setOf_true ↦ 1
  [cases] Cases instances
    [cases] Subtype ↦ 1