Theorem: Nat.find_ext (GMLInit/Data/Nat/Find.lean)

State before:
p₁ p₂ : Nat → Prop
inst✝¹ : DecidablePred p₁
inst✝ : DecidablePred p₂
h : ∀ (n : Nat), p₁ n ↔ p₂ n
x✝¹ : ∃ n, p₁ n
x✝ : ∃ n, p₂ n
⊢ p₁ = p₂
Tactic:
funext n
State after:
case h
p₁ p₂ : Nat → Prop
inst✝¹ : DecidablePred p₁
inst✝ : DecidablePred p₂
h : ∀ (n : Nat), p₁ n ↔ p₂ n
x✝¹ : ∃ n, p₁ n
x✝ : ∃ n, p₂ n
n : Nat
⊢ p₁ n = p₂ n

State before:
case h
p₁ p₂ : Nat → Prop
inst✝¹ : DecidablePred p₁
inst✝ : DecidablePred p₂
h : ∀ (n : Nat), p₁ n ↔ p₂ n
x✝¹ : ∃ n, p₁ n
x✝ : ∃ n, p₂ n
n : Nat
⊢ p₁ n = p₂ n
Tactic:
apply propext
State after:
case h.a
p₁ p₂ : Nat → Prop
inst✝¹ : DecidablePred p₁
inst✝ : DecidablePred p₂
h : ∀ (n : Nat), p₁ n ↔ p₂ n
x✝¹ : ∃ n, p₁ n
x✝ : ∃ n, p₂ n
n : Nat
⊢ p₁ n ↔ p₂ n

State before:
case h.a
p₁ p₂ : Nat → Prop
inst✝¹ : DecidablePred p₁
inst✝ : DecidablePred p₂
h : ∀ (n : Nat), p₁ n ↔ p₂ n
x✝¹ : ∃ n, p₁ n
x✝ : ∃ n, p₂ n
n : Nat
⊢ p₁ n ↔ p₂ n
Tactic:
exact h n
State after:
no goals