Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.DepFn.trans (Lean4Axiomatic/Relation/Equivalence/Impl.lean)

State before:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g h : (x : α) → β x
⊢ f ≃ g → g ≃ h → f ≃ h
Tactic:
intro (_ : ∀ (x : α), f x ≃ g x) (_ : ∀ (x : α), g x ≃ h x)
State after:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g h : (x : α) → β x
x✝¹ : ∀ (x : α), f x ≃ g x
x✝ : ∀ (x : α), g x ≃ h x
⊢ f ≃ h

State before:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g h : (x : α) → β x
x✝¹ : ∀ (x : α), f x ≃ g x
x✝ : ∀ (x : α), g x ≃ h x
⊢ f ≃ h
Tactic:
show ∀ (x : α), f x ≃ h x
State after:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g h : (x : α) → β x
x✝¹ : ∀ (x : α), f x ≃ g x
x✝ : ∀ (x : α), g x ≃ h x
⊢ ∀ (x : α), f x ≃ h x

State before:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g h : (x : α) → β x
x✝¹ : ∀ (x : α), f x ≃ g x
x✝ : ∀ (x : α), g x ≃ h x
⊢ ∀ (x : α), f x ≃ h x
Tactic:
intro x
State after:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g h : (x : α) → β x
x✝¹ : ∀ (x : α), f x ≃ g x
x✝ : ∀ (x : α), g x ≃ h x
x : α
⊢ f x ≃ h x

State before:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g h : (x : α) → β x
x✝¹ : ∀ (x : α), f x ≃ g x
x✝ : ∀ (x : α), g x ≃ h x
x : α
⊢ f x ≃ h x
Tactic:
have : f x ≃ g x := ‹∀ (x : α), f x ≃ g x› x
State after:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g h : (x : α) → β x
x✝¹ : ∀ (x : α), f x ≃ g x
x✝ : ∀ (x : α), g x ≃ h x
x : α
this : f x ≃ g x
⊢ f x ≃ h x

State before:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g h : (x : α) → β x
x✝¹ : ∀ (x : α), f x ≃ g x
x✝ : ∀ (x : α), g x ≃ h x
x : α
this : f x ≃ g x
⊢ f x ≃ h x
Tactic:
have : g x ≃ h x := ‹∀ (x : α), g x ≃ h x› x
State after:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g h : (x : α) → β x
x✝¹ : ∀ (x : α), f x ≃ g x
x✝ : ∀ (x : α), g x ≃ h x
x : α
this✝ : f x ≃ g x
this : g x ≃ h x
⊢ f x ≃ h x

State before:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g h : (x : α) → β x
x✝¹ : ∀ (x : α), f x ≃ g x
x✝ : ∀ (x : α), g x ≃ h x
x : α
this✝ : f x ≃ g x
this : g x ≃ h x
⊢ f x ≃ h x
Tactic:
exact indexed_eqvOp.trans ‹f x ≃ g x› ‹g x ≃ h x›
State after:
no goals