Theorem: Nat.dfold_congr (Fifteen/Data/Nat/Basic.lean)

State before:
α β : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
g : (n : Nat) → β n → β (n + 1)
hfg : ∀ (n : Nat) (a : α n) (b : β n), HEq a b → HEq (f n a) (g n b)
n : Nat
a : α 0
b : β 0
hab : HEq a b
⊢ HEq (dfold f n a) (dfold g n b)
Tactic:
have : α = β := funext fun n => by
  suffices ∃ (a : α n) (b : β n), HEq a b
  from let ⟨_,_,hab⟩ := this; type_eq_of_heq hab
  induction n with
  | zero => exact ⟨a,b,hab⟩
  | succ n IH =>
    let ⟨a,b,hab⟩ := IH
    exact ⟨f n a, g n b, hfg n a b hab⟩
State after:
α β : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
g : (n : Nat) → β n → β (n + 1)
hfg : ∀ (n : Nat) (a : α n) (b : β n), HEq a b → HEq (f n a) (g n b)
n : Nat
a : α 0
b : β 0
hab : HEq a b
this : α = β
⊢ HEq (dfold f n a) (dfold g n b)

State before:
α β : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
g : (n : Nat) → β n → β (n + 1)
hfg : ∀ (n : Nat) (a : α n) (b : β n), HEq a b → HEq (f n a) (g n b)
n : Nat
a : α 0
b : β 0
hab : HEq a b
this : α = β
⊢ HEq (dfold f n a) (dfold g n b)
Tactic:
cases this
State after:
case refl
α : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
n : Nat
a : α 0
g : (n : Nat) → α n → α (n + 1)
hfg : ∀ (n : Nat) (a b : α n), HEq a b → HEq (f n a) (g n b)
b : α 0
hab : HEq a b
⊢ HEq (dfold f n a) (dfold g n b)

State before:
case refl
α : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
n : Nat
a : α 0
g : (n : Nat) → α n → α (n + 1)
hfg : ∀ (n : Nat) (a b : α n), HEq a b → HEq (f n a) (g n b)
b : α 0
hab : HEq a b
⊢ HEq (dfold f n a) (dfold g n b)
Tactic:
cases hab
State after:
case refl.refl
α : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
n : Nat
a : α 0
g : (n : Nat) → α n → α (n + 1)
hfg : ∀ (n : Nat) (a b : α n), HEq a b → HEq (f n a) (g n b)
⊢ HEq (dfold f n a) (dfold g n a)

State before:
case refl.refl
α : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
n : Nat
a : α 0
g : (n : Nat) → α n → α (n + 1)
hfg : ∀ (n : Nat) (a b : α n), HEq a b → HEq (f n a) (g n b)
⊢ HEq (dfold f n a) (dfold g n a)
Tactic:
simp only [heq_iff_eq] at hfg ⊢
State after:
case refl.refl
α : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
n : Nat
a : α 0
g : (n : Nat) → α n → α (n + 1)
hfg : ∀ (n : Nat) (a b : α n), a = b → f n a = g n b
⊢ dfold f n a = dfold g n a

State before:
case refl.refl
α : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
n : Nat
a : α 0
g : (n : Nat) → α n → α (n + 1)
hfg : ∀ (n : Nat) (a b : α n), a = b → f n a = g n b
⊢ dfold f n a = dfold g n a
Tactic:
induction n with
| zero => rfl
| succ n IH => dsimp [dfold]; exact hfg n _ _ IH
State after:
no goals

State before:
α β : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
g : (n : Nat) → β n → β (n + 1)
hfg : ∀ (n : Nat) (a : α n) (b : β n), HEq a b → HEq (f n a) (g n b)
n✝ : Nat
a : α 0
b : β 0
hab : HEq a b
n : Nat
⊢ α n = β n
Tactic:
suffices ∃ (a : α n) (b : β n), HEq a b
from let ⟨_,_,hab⟩ := this; type_eq_of_heq hab
State after:
α β : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
g : (n : Nat) → β n → β (n + 1)
hfg : ∀ (n : Nat) (a : α n) (b : β n), HEq a b → HEq (f n a) (g n b)
n✝ : Nat
a : α 0
b : β 0
hab : HEq a b
n : Nat
⊢ ∃ a b, HEq a b

State before:
α β : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
g : (n : Nat) → β n → β (n + 1)
hfg : ∀ (n : Nat) (a : α n) (b : β n), HEq a b → HEq (f n a) (g n b)
n✝ : Nat
a : α 0
b : β 0
hab : HEq a b
n : Nat
⊢ ∃ a b, HEq a b
Tactic:
induction n with
| zero => exact ⟨a,b,hab⟩
| succ n IH =>
  let ⟨a,b,hab⟩ := IH
  exact ⟨f n a, g n b, hfg n a b hab⟩
State after:
no goals

State before:
case zero
α β : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
g : (n : Nat) → β n → β (n + 1)
hfg : ∀ (n : Nat) (a : α n) (b : β n), HEq a b → HEq (f n a) (g n b)
n : Nat
a : α 0
b : β 0
hab : HEq a b
⊢ ∃ a b, HEq a b
Tactic:
exact ⟨a,b,hab⟩
State after:
no goals

State before:
case succ
α β : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
g : (n : Nat) → β n → β (n + 1)
hfg : ∀ (n : Nat) (a : α n) (b : β n), HEq a b → HEq (f n a) (g n b)
n✝ : Nat
a : α 0
b : β 0
hab : HEq a b
n : Nat
IH : ∃ a b, HEq a b
⊢ ∃ a b, HEq a b
Tactic:
let ⟨a,b,hab⟩ := IH
State after:
case succ
α β : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
g : (n : Nat) → β n → β (n + 1)
hfg : ∀ (n : Nat) (a : α n) (b : β n), HEq a b → HEq (f n a) (g n b)
n✝ : Nat
a✝ : α 0
b✝ : β 0
hab✝ : HEq a✝ b✝
n : Nat
IH : ∃ a b, HEq a b
a : α n
b : β n
hab : HEq a b
⊢ ∃ a b, HEq a b

State before:
case succ
α β : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
g : (n : Nat) → β n → β (n + 1)
hfg : ∀ (n : Nat) (a : α n) (b : β n), HEq a b → HEq (f n a) (g n b)
n✝ : Nat
a✝ : α 0
b✝ : β 0
hab✝ : HEq a✝ b✝
n : Nat
IH : ∃ a b, HEq a b
a : α n
b : β n
hab : HEq a b
⊢ ∃ a b, HEq a b
Tactic:
exact ⟨f n a, g n b, hfg n a b hab⟩
State after:
no goals

State before:
case refl.refl.zero
α : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
a : α 0
g : (n : Nat) → α n → α (n + 1)
hfg : ∀ (n : Nat) (a b : α n), a = b → f n a = g n b
⊢ dfold f zero a = dfold g zero a
Tactic:
rfl
State after:
no goals

State before:
case refl.refl.succ
α : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
a : α 0
g : (n : Nat) → α n → α (n + 1)
hfg : ∀ (n : Nat) (a b : α n), a = b → f n a = g n b
n : Nat
IH : dfold f n a = dfold g n a
⊢ dfold f (succ n) a = dfold g (succ n) a
Tactic:
dsimp [dfold]
State after:
case refl.refl.succ
α : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
a : α 0
g : (n : Nat) → α n → α (n + 1)
hfg : ∀ (n : Nat) (a b : α n), a = b → f n a = g n b
n : Nat
IH : dfold f n a = dfold g n a
⊢ f n (dfold f n a) = g n (dfold g n a)

State before:
case refl.refl.succ
α : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
a : α 0
g : (n : Nat) → α n → α (n + 1)
hfg : ∀ (n : Nat) (a b : α n), a = b → f n a = g n b
n : Nat
IH : dfold f n a = dfold g n a
⊢ f n (dfold f n a) = g n (dfold g n a)
Tactic:
exact hfg n _ _ IH
State after:
no goals