awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this_1 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H_1 : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
this : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
m : Subtype p → Set δ :=
  fun (j : Subtype p) ↦ {x : δ | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun (x : δ) ↦ liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (i : ι) ↦ f i x) s p
F0 : Subtype p → δ → α := fun (j : Subtype p) (x : δ) ↦ ⨅ (i : (↑(s (↑j : ι')) : Type u_5)), f (↑i : ι) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x
hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose (p := Function.Surjective) ⋯
x : δ
H : ∃ (k : Subtype p), x ∈ m k
pos : ∀ (k : Subtype p) (hk : x ∈ m k), ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
⊢ ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k

Tactic:
rcases H with ⟨k, hk⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this_1 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
this : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
m : Subtype p → Set δ :=
  fun (j : Subtype p) ↦ {x : δ | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun (x : δ) ↦ liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (i : ι) ↦ f i x) s p
F0 : Subtype p → δ → α := fun (j : Subtype p) (x : δ) ↦ ⨅ (i : (↑(s (↑j : ι')) : Type u_5)), f (↑i : ι) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x
hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose (p := Function.Surjective) ⋯
x : δ
k : Subtype p
hk : x ∈ m k
pos :
  ∀ (n : ℕ) (hk : x ∈ m (Classical.choose (p := Function.Surjective) ⋯ n)),
    ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
⊢ ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k

Tactic:
rcases Classical.choose_spec (exists_surjective_nat (Subtype p)) k with ⟨n, rfl⟩

Premises used: Subtype, Classical.choose_spec, exists_surjective_nat, rfl
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this_1 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
this : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
m : Subtype p → Set δ :=
  fun (j : Subtype p) ↦ {x : δ | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun (x : δ) ↦ liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (i : ι) ↦ f i x) s p
F0 : Subtype p → δ → α := fun (j : Subtype p) (x : δ) ↦ ⨅ (i : (↑(s (↑j : ι')) : Type u_5)), f (↑i : ι) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x
hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose (p := Function.Surjective) ⋯
x : δ
n : ℕ
hk : x ∈ m (Classical.choose (p := Function.Surjective) ⋯ n)
⊢ ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k

Tactic:
⟨n, Or.inl hk⟩

Premises used: Exists.intro, Or.inl
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this_1 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
this : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
m : Subtype p → Set δ :=
  fun (j : Subtype p) ↦ {x : δ | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun (x : δ) ↦ liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (i : ι) ↦ f i x) s p
F0 : Subtype p → δ → α := fun (j : Subtype p) (x : δ) ↦ ⨅ (i : (↑(s (↑j : ι')) : Type u_5)), f (↑i : ι) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x
hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose (p := Function.Surjective) ⋯
x : δ
n : ℕ
hk : x ∈ m (Classical.choose (p := Function.Surjective) ⋯ n)
⊢ ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k

Tactic:
exact ⟨n, Or.inl hk⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this_1 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H_1 : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
this : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
m : Subtype p → Set δ :=
  fun (j : Subtype p) ↦ {x : δ | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun (x : δ) ↦ liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (i : ι) ↦ f i x) s p
F0 : Subtype p → δ → α := fun (j : Subtype p) (x : δ) ↦ ⨅ (i : (↑(s (↑j : ι')) : Type u_5)), f (↑i : ι) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x
hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose (p := Function.Surjective) ⋯
x : δ
H : ∀ (k : Subtype p), x ∉ m k
⊢ ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k

Tactic:
⟨0, Or.inr H⟩

Premises used: Exists.intro, OfNat.ofNat, Or.inr
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this_1 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H_1 : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
this : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
m : Subtype p → Set δ :=
  fun (j : Subtype p) ↦ {x : δ | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun (x : δ) ↦ liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (i : ι) ↦ f i x) s p
F0 : Subtype p → δ → α := fun (j : Subtype p) (x : δ) ↦ ⨅ (i : (↑(s (↑j : ι')) : Type u_5)), f (↑i : ι) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x
hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose (p := Function.Surjective) ⋯
x : δ
H : ∀ (k : Subtype p), x ∉ m k
⊢ ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k

Tactic:
exact ⟨0, Or.inr H⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this_1 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
this : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
m : Subtype p → Set δ :=
  fun (j : Subtype p) ↦ {x : δ | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun (x : δ) ↦ liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (i : ι) ↦ f i x) s p
F0 : Subtype p → δ → α := fun (j : Subtype p) (x : δ) ↦ ⨅ (i : (↑(s (↑j : ι')) : Type u_5)), f (↑i : ι) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x
hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose (p := Function.Surjective) ⋯
⊢ ∀ (x : δ), ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k

Tactic:
have Z : ∀ x, ∃ n, x ∈ m (g n) ∨ ∀ k, x ∉ m k := by
    intro x
    by_cases! H : ∃ k, x ∈ m k
    · rcases H with ⟨k, hk⟩
      rcases Classical.choose_spec (exists_surjective_nat (Subtype p)) k with ⟨n, rfl⟩
      exact ⟨n, Or.inl hk⟩
    · exact ⟨0, Or.inr H⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this_1 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
this : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
m : Subtype p → Set δ :=
  fun (j : Subtype p) ↦ {x : δ | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun (x : δ) ↦ liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (i : ι) ↦ f i x) s p
F0 : Subtype p → δ → α := fun (j : Subtype p) (x : δ) ↦ ⨅ (i : (↑(s (↑j : ι')) : Type u_5)), f (↑i : ι) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x
hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose (p := Function.Surjective) ⋯
Z : ∀ (x : δ), ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
h :
  ∀ (x : δ),
    F1 x =
      if x ∈ m j then F0 j x else F0 (g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)) x
⊢ F1 = fun (x : δ) ↦
    if x ∈ m j then F0 j x else F0 (g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)) x

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this_1 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
this : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
m : Subtype p → Set δ :=
  fun (j : Subtype p) ↦ {x : δ | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun (x : δ) ↦ liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (i : ι) ↦ f i x) s p
F0 : Subtype p → δ → α := fun (j : Subtype p) (x : δ) ↦ ⨅ (i : (↑(s (↑j : ι')) : Type u_5)), f (↑i : ι) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x
hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose (p := Function.Surjective) ⋯
Z : ∀ (x : δ), ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
x : δ
⊢ reparam x j = if x ∈ m j then j else g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)

Tactic:
have A : reparam x j = if x ∈ m j then j else g (Nat.find (Z x)) := rfl
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this_1 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
this : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
m : Subtype p → Set δ :=
  fun (j : Subtype p) ↦ {x : δ | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun (x : δ) ↦ liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (i : ι) ↦ f i x) s p
F0 : Subtype p → δ → α := fun (j : Subtype p) (x : δ) ↦ ⨅ (i : (↑(s (↑j : ι')) : Type u_5)), f (↑i : ι) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x
hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose (p := Function.Surjective) ⋯
Z : ∀ (x : δ), ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
x : δ
A : reparam x j = if x ∈ m j then j else g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)
pos : ∀ (hjx : x ∈ m j), F1 x = F0 j x
neg : ∀ (hjx : x ∉ m j), F1 x = F0 (g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)) x
⊢ F1 x = if x ∈ m j then F0 j x else F0 (g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)) x

Tactic:
split_ifs with hjx
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this_1 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
this : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
m : Subtype p → Set δ :=
  fun (j : Subtype p) ↦ {x : δ | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun (x : δ) ↦ liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (i : ι) ↦ f i x) s p
F0 : Subtype p → δ → α := fun (j : Subtype p) (x : δ) ↦ ⨅ (i : (↑(s (↑j : ι')) : Type u_5)), f (↑i : ι) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x
hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose (p := Function.Surjective) ⋯
Z : ∀ (x : δ), ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
x : δ
A : reparam x j = if x ∈ m j then j else g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)
hjx : x ∈ m j
rw : (if x ∈ m j then j else g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)) = j
rw₁ rw₂ : j = j
⊢ reparam x j = j

Tactic:
rw [A, if_pos hjx]

Premises used: if_pos
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this_1 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
this : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
m : Subtype p → Set δ :=
  fun (j : Subtype p) ↦ {x : δ | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun (x : δ) ↦ liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (i : ι) ↦ f i x) s p
F0 : Subtype p → δ → α := fun (j : Subtype p) (x : δ) ↦ ⨅ (i : (↑(s (↑j : ι')) : Type u_5)), f (↑i : ι) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x
hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose (p := Function.Surjective) ⋯
Z : ∀ (x : δ), ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
x : δ
A : reparam x j = if x ∈ m j then j else g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)
hjx : x ∈ m j
⊢ reparam x j = j

Tactic:
have : reparam x j = j := by rw [A, if_pos hjx]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this_1 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
this_2 : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
m : Subtype p → Set δ :=
  fun (j : Subtype p) ↦ {x : δ | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun (x : δ) ↦ liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (i : ι) ↦ f i x) s p
F0 : Subtype p → δ → α := fun (j : Subtype p) (x : δ) ↦ ⨅ (i : (↑(s (↑j : ι')) : Type u_5)), f (↑i : ι) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x
hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose (p := Function.Surjective) ⋯
Z : ∀ (x : δ), ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
x : δ
A : reparam x j = if x ∈ m j then j else g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)
hjx : x ∈ m j
this : reparam x j = j
⊢ F1 x = F0 j x

Tactic:
simp only [hF1, this]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order
Goal:
α : Type u_1
δ : Type u_4
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mδ : MeasurableSpace δ
inst_2 : ConditionallyCompleteLinearOrder α
inst_3 : OrderTopology α
inst_4 : SecondCountableTopology α
ι : Type u_5
ι' : Type u_6
f : ι → δ → α
v : Filter ι
hf : ∀ (i : ι), Measurable (f i)
p : ι' → Prop
s : ι' → Set ι
hv : v.HasCountableBasis p s
hs : ∀ (j : ι'), (s j).Countable
this_1 : Countable.{max 1 (u_6 + 1)} (Subtype p)
hp : Nonempty.{max 1 (u_6 + 1)} (Subtype p)
H : ¬∃ (j : Subtype p), s (↑j : ι') = ∅
this : ∀ (i : ι'), Countable.{u_5 + 1} (↑(s i) : Type u_5)
m : Subtype p → Set δ :=
  fun (j : Subtype p) ↦ {x : δ | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_5)) ↦ f (↑i : ι) x)}
m_meas : ∀ (j : Subtype p), MeasurableSet (m j)
mc_meas : MeasurableSet.{u_4} (α := δ) {x : δ | ∀ (j : Subtype p), x ∉ m j}
j : Subtype p
reparam : δ → Subtype p → Subtype p := fun (x : δ) ↦ liminf_reparam.{u_1, u_5, u_6} (α := α) (fun (i : ι) ↦ f i x) s p
F0 : Subtype p → δ → α := fun (j : Subtype p) (x : δ) ↦ ⨅ (i : (↑(s (↑j : ι')) : Type u_5)), f (↑i : ι) x
F0_meas : ∀ (j : Subtype p), Measurable (F0 j)
F1 : δ → α := fun (x : δ) ↦ F0 (reparam x j) x
hF1 : F1 = fun (x : δ) ↦ F0 (reparam x j) x
g : ℕ → Subtype p := Classical.choose (p := Function.Surjective) ⋯
Z : ∀ (x : δ), ∃ (n : ℕ), x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k
x : δ
A : reparam x j = if x ∈ m j then j else g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)
hjx : x ∉ m j
rw :
  (if x ∈ m j then j else g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)) =
    g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)
rw₁ rw₂ :
  g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯) =
    g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)
⊢ reparam x j = g (Nat.find (p := fun (n : ℕ) ↦ x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k) ⋯)

Tactic:
rw [A, if_neg hjx]

Premises used: if_neg