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

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

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

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

State before:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g : (x : α) → β x
x✝ : ∀ (x : α), f x ≃ g x
x : α
⊢ g x ≃ f 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 : (x : α) → β x
x✝ : ∀ (x : α), f x ≃ g x
x : α
this : f x ≃ g x
⊢ g x ≃ f x

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