-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem coeFn_const_eq [NeZero μ] (b : β) (x : α) : (const α b : α →ₘ[μ] β) x = b

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : NeZero μ
b : β
x : α
h : ∃ b_1, const α b = mk (Function.const α b_1) ⋯
this : const α b = mk (Function.const α (Classical.choose h)) ⋯
⊢ Function.const α (Classical.choose h) x = b

Tactic:
set b' := Classical.choose h

Result:
case pos
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : NeZero μ
b : β
x : α
h : ∃ b_1, const α b = mk (Function.const α b_1) ⋯
b' : β := Classical.choose h
this : const α b = mk (Function.const α b') ⋯
⊢ Function.const α b' x = b

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : NeZero μ
b : β
x : α
h : ∃ b_1, const α b = mk (Function.const α b_1) ⋯
b' : β := Classical.choose h
this : const α b = mk (Function.const α b') ⋯
⊢ Function.const α b' x = b

Tactic:
simp_rw [const, mk_eq_mk, EventuallyEq, ← const_def, eventually_const] at this

Result:
case pos
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : NeZero μ
b : β
x : α
h : ∃ b_1, const α b = mk (Function.const α b_1) ⋯
b' : β := Classical.choose h
this : b = b'
⊢ Function.const α b' x = b

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : NeZero μ
b : β
x : α
h : ∃ b_1, const α b = mk (Function.const α b_1) ⋯
b' : β := Classical.choose h
this : b = b'
⊢ Function.const α b' x = b

Tactic:
rw [Function.const, this]

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : NeZero μ
b : β
x : α
h : ∃ b_1, const α b = mk (Function.const α b_1) ⋯
⊢ Function.const α (Classical.choose h) x = b

Tactic:
have := Classical.choose_spec h

Result:
case pos
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : NeZero μ
b : β
x : α
h : ∃ b_1, const α b = mk (Function.const α b_1) ⋯
this : const α b = mk (Function.const α (Classical.choose h)) ⋯
⊢ Function.const α (Classical.choose h) x = b

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : NeZero μ
b : β
x : α
h : ¬∃ b_1, const α b = mk (Function.const α b_1) ⋯
⊢ AEStronglyMeasurable.mk ↑(Quotient.out (const α b)) ⋯ x = b

Tactic:
exact h.elim ⟨b, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : NeZero μ
b : β
x : α
⊢ ↑(const α b) x = b

Tactic:
simp only [cast]

Result:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : NeZero μ
b : β
x : α
⊢ (if h : ∃ b_1, const α b = mk (Function.const α b_1) ⋯ then Function.const α (Classical.choose h)
      else AEStronglyMeasurable.mk ↑(Quotient.out (const α b)) ⋯)
      x =
    b

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : NeZero μ
b : β
x : α
h : ∃ b_1, const α b = mk (Function.const α b_1) ⋯
⊢ Function.const α (Classical.choose h) x = b

case neg
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : NeZero μ
b : β
x : α
h : ¬∃ b_1, const α b = mk (Function.const α b_1) ⋯
⊢ AEStronglyMeasurable.mk ↑(Quotient.out (const α b)) ⋯ x = b

Tactic:
swap

Result:
case neg
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : NeZero μ
b : β
x : α
h : ¬∃ b_1, const α b = mk (Function.const α b_1) ⋯
⊢ AEStronglyMeasurable.mk ↑(Quotient.out (const α b)) ⋯ x = b

case pos
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : NeZero μ
b : β
x : α
h : ∃ b_1, const α b = mk (Function.const α b_1) ⋯
⊢ Function.const α (Classical.choose h) x = b

Proof state:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : NeZero μ
b : β
x : α
⊢ (if h : ∃ b_1, const α b = mk (Function.const α b_1) ⋯ then Function.const α (Classical.choose h)
      else AEStronglyMeasurable.mk ↑(Quotient.out (const α b)) ⋯)
      x =
    b

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : NeZero μ
b : β
x : α
h : ∃ b_1, const α b = mk (Function.const α b_1) ⋯
⊢ Function.const α (Classical.choose h) x = b

case neg
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : NeZero μ
b : β
x : α
h : ¬∃ b_1, const α b = mk (Function.const α b_1) ⋯
⊢ AEStronglyMeasurable.mk ↑(Quotient.out (const α b)) ⋯ x = b