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

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

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

State before:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f : (x : α) → β x
x : α
⊢ f x ≃ f x
Tactic:
exact indexed_eqvOp.refl
State after:
no goals