[GOAL]
a b c d : Prop
p : ?m.25026
h : Decidable True
⊢ decide True = true
[PROOFSTEP]
simp
[GOAL]
a b c d : Prop
p : ?m.25099
h : Decidable False
⊢ decide False = false
[PROOFSTEP]
simp
[GOAL]
a b c d p : Prop
h : Decidable p
h₁ : p → Sort u
h₂ : ¬p → Sort u
h₃ : p
h₄ : h₁ h₃
⊢ h₁ h₃ = Decidable.recOn h h₂ h₁
[PROOFSTEP]
match h with
| .isTrue _ => rfl
[GOAL]
a b c d p : Prop
h : Decidable p
h₁ : p → Sort u
h₂ : ¬p → Sort u
h₃ : p
h₄ : h₁ h₃
h✝ : p
⊢ h₁ h₃ = Decidable.recOn (isTrue h✝) h₂ h₁
[PROOFSTEP]
rfl
[GOAL]
a b c d p : Prop
h : Decidable p
h₁ : p → Sort u
h₂ : ¬p → Sort u
h₃ : ¬p
h₄ : h₂ h₃
⊢ h₂ h₃ = Decidable.recOn h h₂ h₁
[PROOFSTEP]
match h with
| .isFalse _ => rfl
[GOAL]
a b c d p : Prop
h : Decidable p
h₁ : p → Sort u
h₂ : ¬p → Sort u
h₃ : ¬p
h₄ : h₂ h₃
h✝ : ¬p
⊢ h₂ h₃ = Decidable.recOn (isFalse h✝) h₂ h₁
[PROOFSTEP]
rfl
[GOAL]
a b c d : Prop
p✝ : ?m.26639
α : Sort u
p : α → α → Bool
h₁ : IsDecEq p
h₂ : IsDecRefl p
x y : α
hp : ¬p x y = true
hxy : x = y
⊢ ¬p y y = true
[PROOFSTEP]
rwa [hxy] at hp 
[GOAL]
a b c✝ d : Prop
p : ?m.27547
c t e : Prop
inst✝ : Decidable c
h : if c then t else e
hc : c
⊢ t
[PROOFSTEP]
have := if_pos hc ▸ h
[GOAL]
a b c✝ d : Prop
p : ?m.27547
c t e : Prop
inst✝ : Decidable c
h : if c then t else e
hc : c
this : t
⊢ t
[PROOFSTEP]
exact this
[GOAL]
a b c✝ d : Prop
p : ?m.27609
c t e : Prop
inst✝ : Decidable c
h : if c then t else e
hnc : ¬c
⊢ e
[PROOFSTEP]
have := if_neg hnc ▸ h
[GOAL]
a b c✝ d : Prop
p : ?m.27609
c t e : Prop
inst✝ : Decidable c
h : if c then t else e
hnc : ¬c
this : e
⊢ e
[PROOFSTEP]
exact this
[GOAL]
a b✝ c d : Prop
p : ?m.29900
α : Sort v
β : α → Sort u
a₁ a₂ : α
b : (x : α) → β x
h : a₁ = a₂
⊢ HEq
    (let x := a₁;
    b x)
    (let x := a₂;
    b x)
[PROOFSTEP]
cases h
[GOAL]
case refl
a b✝ c d : Prop
p : ?m.29900
α : Sort v
β : α → Sort u
a₁ : α
b : (x : α) → β x
⊢ HEq
    (let x := a₁;
    b x)
    (let x := a₁;
    b x)
[PROOFSTEP]
rfl
[GOAL]
a✝ b c d : Prop
p : ?m.30034
α : Sort v
β : α → Sort u
a : α
b₁ b₂ : (x : α) → β x
h : ∀ (x : α), b₁ x = b₂ x
⊢ (let x := a;
    b₁ x) =
    let x := a;
    b₂ x
[PROOFSTEP]
exact h _ ▸ rfl
[GOAL]
a b c d : Prop
p : ?m.30108
α : Sort v
β : Sort u
a₁ a₂ : α
b₁ b₂ : α → β
h₁ : a₁ = a₂
h₂ : ∀ (x : α), b₁ x = b₂ x
⊢ (let x := a₁;
    b₁ x) =
    let x := a₂;
    b₂ x
[PROOFSTEP]
simp [h₁, h₂]
