Theorem: Lean4Axiomatic.Rational.div_eqv_1 (Lean4Axiomatic/Rational/Reciprocation.lean)

State before:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
⊢ p / q ≃ 1 ↔ p ≃ q
Tactic:
apply Iff.intro
State after:
case mp
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
⊢ p / q ≃ 1 → p ≃ q

case mpr
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
⊢ p ≃ q → p / q ≃ 1

State before:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
⊢ p / q ≃ 1 → p ≃ q
Tactic:
case mp =>
  intro (_ : p/q ≃ 1)
  show p ≃ q
  calc
    _ ≃ p             := eqv_refl
    _ ≃ p * 1         := eqv_symm mul_identR
    _ ≃ p * (q⁻¹ * q) := mul_substR (eqv_symm mul_inverseL)
    _ ≃ (p * q⁻¹) * q := eqv_symm mul_assoc
    _ ≃ (p/q) * q     := mul_substL (eqv_symm div_mul_recip)
    _ ≃ 1 * q         := mul_substL ‹p/q ≃ 1›
    _ ≃ q             := mul_identL
State after:
no goals

State before:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
⊢ p ≃ q → p / q ≃ 1
Tactic:
case mpr =>
  intro (_ : p ≃ q)
  show p/q ≃ 1
  calc
    _ ≃ p/q := eqv_refl
    _ ≃ q/q := div_substL ‹p ≃ q›
    _ ≃ 1   := div_same
State after:
no goals

State before:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
⊢ p / q ≃ 1 → p ≃ q
Tactic:
intro (_ : p/q ≃ 1)
State after:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
x✝ : p / q ≃ 1
⊢ p ≃ q

State before:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
x✝ : p / q ≃ 1
⊢ p ≃ q
Tactic:
calc
  _ ≃ p             := eqv_refl
  _ ≃ p * 1         := eqv_symm mul_identR
  _ ≃ p * (q⁻¹ * q) := mul_substR (eqv_symm mul_inverseL)
  _ ≃ (p * q⁻¹) * q := eqv_symm mul_assoc
  _ ≃ (p/q) * q     := mul_substL (eqv_symm div_mul_recip)
  _ ≃ 1 * q         := mul_substL ‹p/q ≃ 1›
  _ ≃ q             := mul_identL
State after:
no goals

State before:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
⊢ p ≃ q → p / q ≃ 1
Tactic:
intro (_ : p ≃ q)
State after:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
x✝ : p ≃ q
⊢ p / q ≃ 1

State before:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
x✝ : p ≃ q
⊢ p / q ≃ 1
Tactic:
calc
  _ ≃ p/q := eqv_refl
  _ ≃ q/q := div_substL ‹p ≃ q›
  _ ≃ 1   := div_same
State after:
no goals