-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem forall_sum {γ : α ⊕ β → Sort _} {p : (∀ ab, γ ab) → Prop} :
    (∀ fab, p fab) ↔ (∀ fa fb, p (Sum.rec fa fb))

Proof state:
case h
α : Type u_1
β : Type u_2
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
h : ∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), p fun t => rec fa fb t
fab : (ab : α ⊕ β) → γ ab
⊢ ∀ (x : α ⊕ β), fab x = rec (fun a => fab (inl a)) (fun b => fab (inr b)) x

Tactic:
rintro (_ | _) <;> rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
h : ∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), p fun t => rec fa fb t
fab : (ab : α ⊕ β) → γ ab
h1 : fab = fun t => rec (fun a => fab (inl a)) (fun b => fab (inr b)) t
⊢ p fab

Tactic:
rw [h1]

Result:
α : Type u_1
β : Type u_2
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
h : ∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), p fun t => rec fa fb t
fab : (ab : α ⊕ β) → γ ab
h1 : fab = fun t => rec (fun a => fab (inl a)) (fun b => fab (inr b)) t
⊢ p fun t => rec (fun a => fab (inl a)) (fun b => fab (inr b)) t

Proof state:
α : Type u_1
β : Type u_2
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
h : ∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), p fun t => rec fa fb t
fab : (ab : α ⊕ β) → γ ab
⊢ p fab

Tactic:
have h1 : fab = Sum.rec (fun a => fab (Sum.inl a)) (fun b => fab (Sum.inr b)) := by
  apply funext
  rintro (_ | _) <;> rfl

Result:
α : Type u_1
β : Type u_2
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
h : ∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), p fun t => rec fa fb t
fab : (ab : α ⊕ β) → γ ab
h1 : fab = fun t => rec (fun a => fab (inl a)) (fun b => fab (inr b)) t
⊢ p fab

Proof state:
α : Type u_1
β : Type u_2
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
h : ∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), p fun t => rec fa fb t
fab : (ab : α ⊕ β) → γ ab
h1 : fab = fun t => rec (fun a => fab (inl a)) (fun b => fab (inr b)) t
⊢ p fun t => rec (fun a => fab (inl a)) (fun b => fab (inr b)) t

Tactic:
exact h _ _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
⊢ (∀ (fab : (ab : α ⊕ β) → γ ab), p fab) ↔
    ∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), p fun t => rec fa fb t

Tactic:
refine ⟨fun h fa fb => h _, fun h fab => ?_⟩

Result:
α : Type u_1
β : Type u_2
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
h : ∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), p fun t => rec fa fb t
fab : (ab : α ⊕ β) → γ ab
⊢ p fab

Proof state:
α : Type u_1
β : Type u_2
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
h : ∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), p fun t => rec fa fb t
fab : (ab : α ⊕ β) → γ ab
⊢ fab = fun t => rec (fun a => fab (inl a)) (fun b => fab (inr b)) t

Tactic:
apply funext

Result:
case h
α : Type u_1
β : Type u_2
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
h : ∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), p fun t => rec fa fb t
fab : (ab : α ⊕ β) → γ ab
⊢ ∀ (x : α ⊕ β), fab x = rec (fun a => fab (inl a)) (fun b => fab (inr b)) x