Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_symm (Lean4Axiomatic/Rational/Impl/Fraction/Naive.lean)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p q : Fraction ℤ
⊢ p ≃ q → q ≃ p
Tactic:
revert p
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, p ≃ q → q ≃ p

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, p ≃ q → q ≃ p
Tactic:
intro (a//b)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
a b : ℤ
⊢ a//b ≃ q → q ≃ a//b

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q : Fraction ℤ
a b : ℤ
⊢ a//b ≃ q → q ≃ a//b
Tactic:
revert q
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ ∀ {q : Fraction ℤ}, a//b ≃ q → q ≃ a//b

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ ∀ {q : Fraction ℤ}, a//b ≃ q → q ≃ a//b
Tactic:
intro (c//d)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b c d : ℤ
⊢ a//b ≃ c//d → c//d ≃ a//b

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b c d : ℤ
⊢ a//b ≃ c//d → c//d ≃ a//b
Tactic:
intro (_ : a//b ≃ c//d)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b c d : ℤ
x✝ : a//b ≃ c//d
⊢ c//d ≃ a//b

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b c d : ℤ
x✝ : a//b ≃ c//d
⊢ c//d ≃ a//b
Tactic:
have : a * d ≃ c * b := ‹a//b ≃ c//d›
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b c d : ℤ
x✝ : a//b ≃ c//d
this : a * d ≃ c * b
⊢ c//d ≃ a//b

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b c d : ℤ
x✝ : a//b ≃ c//d
this : a * d ≃ c * b
⊢ c//d ≃ a//b
Tactic:
show c * b ≃ a * d
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b c d : ℤ
x✝ : a//b ≃ c//d
this : a * d ≃ c * b
⊢ c * b ≃ a * d

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b c d : ℤ
x✝ : a//b ≃ c//d
this : a * d ≃ c * b
⊢ c * b ≃ a * d
Tactic:
exact Rel.symm ‹a * d ≃ c * b›
State after:
no goals