-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem dite_congr {_ : Decidable b} [Decidable c]
    {x : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
    (h₁ : b = c)
    (h₂ : (h : c)  → x (h₁.mpr_prop h) = u h)
    (h₃ : (h : ¬c) → y (h₁.mpr_not h)  = v h) :
    dite b x y = dite c u v

Proof state:
case inl
c : Prop
α : Sort u_1
inst✝ : Decidable c
u : c → α
v : ¬c → α
h : c
x✝ : Decidable c
x : c → α
y : ¬c → α
h₂ : ∀ (h : c), x ⋯ = u h
h₃ : ∀ (h : ¬c), y ⋯ = v h
⊢ x h = u h

Tactic:
exact h₂ h

Result:
no goals

Proof state:
case inr
b c : Prop
α : Sort u_1
x✝ : Decidable b
inst✝ : Decidable c
x : b → α
u : c → α
y : ¬b → α
v : ¬c → α
h₁ : b = c
h₂ : ∀ (h : c), x ⋯ = u h
h₃ : ∀ (h : ¬c), y ⋯ = v h
h : ¬c
⊢ dite b x y = v h

Tactic:
subst b

Result:
case inr
c : Prop
α : Sort u_1
inst✝ : Decidable c
u : c → α
v : ¬c → α
h : ¬c
x✝ : Decidable c
x : c → α
y : ¬c → α
h₂ : ∀ (h : c), x ⋯ = u h
h₃ : ∀ (h : ¬c), y ⋯ = v h
⊢ dite c x y = v h

Proof state:
case inr
c : Prop
α : Sort u_1
inst✝ : Decidable c
u : c → α
v : ¬c → α
h : ¬c
x✝ : Decidable c
x : c → α
y : ¬c → α
h₂ : ∀ (h : c), x ⋯ = u h
h₃ : ∀ (h : ¬c), y ⋯ = v h
⊢ y h = v h

Tactic:
exact h₃ h

Result:
no goals

Proof state:
case inl
b c : Prop
α : Sort u_1
x✝ : Decidable b
inst✝ : Decidable c
x : b → α
u : c → α
y : ¬b → α
v : ¬c → α
h₁ : b = c
h₂ : ∀ (h : c), x ⋯ = u h
h₃ : ∀ (h : ¬c), y ⋯ = v h
h : c
⊢ dite b x y = dite c u v

Tactic:
rw [dif_pos h]

Result:
case inl
b c : Prop
α : Sort u_1
x✝ : Decidable b
inst✝ : Decidable c
x : b → α
u : c → α
y : ¬b → α
v : ¬c → α
h₁ : b = c
h₂ : ∀ (h : c), x ⋯ = u h
h₃ : ∀ (h : ¬c), y ⋯ = v h
h : c
⊢ dite b x y = u h

Proof state:
b c : Prop
α : Sort u_1
x✝ : Decidable b
inst✝ : Decidable c
x : b → α
u : c → α
y : ¬b → α
v : ¬c → α
h₁ : b = c
h₂ : ∀ (h : c), x ⋯ = u h
h₃ : ∀ (h : ¬c), y ⋯ = v h
⊢ dite b x y = dite c u v

Tactic:
cases Decidable.em c with
| inl h => rw [dif_pos h]; subst b; rw [dif_pos h]; exact h₂ h
| inr h => rw [dif_neg h]; subst b; rw [dif_neg h]; exact h₃ h

Result:
no goals

Proof state:
case inl
b c : Prop
α : Sort u_1
x✝ : Decidable b
inst✝ : Decidable c
x : b → α
u : c → α
y : ¬b → α
v : ¬c → α
h₁ : b = c
h₂ : ∀ (h : c), x ⋯ = u h
h₃ : ∀ (h : ¬c), y ⋯ = v h
h : c
⊢ dite b x y = u h

Tactic:
subst b

Result:
case inl
c : Prop
α : Sort u_1
inst✝ : Decidable c
u : c → α
v : ¬c → α
h : c
x✝ : Decidable c
x : c → α
y : ¬c → α
h₂ : ∀ (h : c), x ⋯ = u h
h₃ : ∀ (h : ¬c), y ⋯ = v h
⊢ dite c x y = u h

Proof state:
case inr
c : Prop
α : Sort u_1
inst✝ : Decidable c
u : c → α
v : ¬c → α
h : ¬c
x✝ : Decidable c
x : c → α
y : ¬c → α
h₂ : ∀ (h : c), x ⋯ = u h
h₃ : ∀ (h : ¬c), y ⋯ = v h
⊢ dite c x y = v h

Tactic:
rw [dif_neg h]

Result:
case inr
c : Prop
α : Sort u_1
inst✝ : Decidable c
u : c → α
v : ¬c → α
h : ¬c
x✝ : Decidable c
x : c → α
y : ¬c → α
h₂ : ∀ (h : c), x ⋯ = u h
h₃ : ∀ (h : ¬c), y ⋯ = v h
⊢ y h = v h

Proof state:
case inl
c : Prop
α : Sort u_1
inst✝ : Decidable c
u : c → α
v : ¬c → α
h : c
x✝ : Decidable c
x : c → α
y : ¬c → α
h₂ : ∀ (h : c), x ⋯ = u h
h₃ : ∀ (h : ¬c), y ⋯ = v h
⊢ dite c x y = u h

Tactic:
rw [dif_pos h]

Result:
case inl
c : Prop
α : Sort u_1
inst✝ : Decidable c
u : c → α
v : ¬c → α
h : c
x✝ : Decidable c
x : c → α
y : ¬c → α
h₂ : ∀ (h : c), x ⋯ = u h
h₃ : ∀ (h : ¬c), y ⋯ = v h
⊢ x h = u h

Proof state:
case inr
b c : Prop
α : Sort u_1
x✝ : Decidable b
inst✝ : Decidable c
x : b → α
u : c → α
y : ¬b → α
v : ¬c → α
h₁ : b = c
h₂ : ∀ (h : c), x ⋯ = u h
h₃ : ∀ (h : ¬c), y ⋯ = v h
h : ¬c
⊢ dite b x y = dite c u v

Tactic:
rw [dif_neg h]

Result:
case inr
b c : Prop
α : Sort u_1
x✝ : Decidable b
inst✝ : Decidable c
x : b → α
u : c → α
y : ¬b → α
v : ¬c → α
h₁ : b = c
h₂ : ∀ (h : c), x ⋯ = u h
h₃ : ∀ (h : ¬c), y ⋯ = v h
h : ¬c
⊢ dite b x y = v h