Theorem: LoVe.RTC.lift (LoVe/LoVelib.lean)

State before:
α β : Type
R : α → α → Prop
S : β → β → Prop
a b : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
hab : RTC R a b
⊢ RTC S (f a) (f b)
Tactic:
induction hab with
| refl => apply refl
| tail b c hab hbc ih =>
  apply tail
  apply ih
  apply hf
  exact hbc
State after:
no goals

State before:
case refl
α β : Type
R : α → α → Prop
S : β → β → Prop
a b : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
⊢ RTC S (f a) (f a)
Tactic:
apply refl
State after:
no goals

State before:
case tail
α β : Type
R : α → α → Prop
S : β → β → Prop
a b✝ : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
b c : α
hab : RTC R a b
hbc : R b c
ih : RTC S (f a) (f b)
⊢ RTC S (f a) (f c)
Tactic:
apply tail
State after:
case tail.hab
α β : Type
R : α → α → Prop
S : β → β → Prop
a b✝ : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
b c : α
hab : RTC R a b
hbc : R b c
ih : RTC S (f a) (f b)
⊢ RTC S (f a) ?tail.b

case tail.hbc
α β : Type
R : α → α → Prop
S : β → β → Prop
a b✝ : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
b c : α
hab : RTC R a b
hbc : R b c
ih : RTC S (f a) (f b)
⊢ S ?tail.b (f c)

case tail.b
α β : Type
R : α → α → Prop
S : β → β → Prop
a b✝ : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
b c : α
hab : RTC R a b
hbc : R b c
ih : RTC S (f a) (f b)
⊢ β

State before:
case tail.hab
α β : Type
R : α → α → Prop
S : β → β → Prop
a b✝ : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
b c : α
hab : RTC R a b
hbc : R b c
ih : RTC S (f a) (f b)
⊢ RTC S (f a) ?tail.b

case tail.hbc
α β : Type
R : α → α → Prop
S : β → β → Prop
a b✝ : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
b c : α
hab : RTC R a b
hbc : R b c
ih : RTC S (f a) (f b)
⊢ S ?tail.b (f c)

case tail.b
α β : Type
R : α → α → Prop
S : β → β → Prop
a b✝ : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
b c : α
hab : RTC R a b
hbc : R b c
ih : RTC S (f a) (f b)
⊢ β
Tactic:
apply ih
State after:
case tail.hbc
α β : Type
R : α → α → Prop
S : β → β → Prop
a b✝ : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
b c : α
hab : RTC R a b
hbc : R b c
ih : RTC S (f a) (f b)
⊢ S (f b) (f c)

State before:
case tail.hbc
α β : Type
R : α → α → Prop
S : β → β → Prop
a b✝ : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
b c : α
hab : RTC R a b
hbc : R b c
ih : RTC S (f a) (f b)
⊢ S (f b) (f c)
Tactic:
apply hf
State after:
case tail.hbc.a
α β : Type
R : α → α → Prop
S : β → β → Prop
a b✝ : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
b c : α
hab : RTC R a b
hbc : R b c
ih : RTC S (f a) (f b)
⊢ R b c

State before:
case tail.hbc.a
α β : Type
R : α → α → Prop
S : β → β → Prop
a b✝ : α
f : α → β
hf : ∀ (a b : α), R a b → S (f a) (f b)
b c : α
hab : RTC R a b
hbc : R b c
ih : RTC S (f a) (f b)
⊢ R b c
Tactic:
exact hbc
State after:
no goals