Theorem: Lean4Axiomatic.Rational.Impl.Fraction.recip_subst (Lean4Axiomatic/Rational/Impl/Fraction/Reciprocation.lean)

State before:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
p₁ p₂ : Fraction ℤ
inst✝¹ : AP (p₁ ≄ 0)
inst✝ : AP (p₂ ≄ 0)
⊢ p₁ ≃ p₂ → p₁⁻¹ ≃ p₂⁻¹
Tactic:
revert p₁
State after:
ℕ : Type
inst✝² : Natural ℕ
ℤ : Type
inst✝¹ : Integer ℤ
p₂ : Fraction ℤ
inst✝ : AP (p₂ ≄ 0)
⊢ ∀ {p₁ : Fraction ℤ} [inst : AP (p₁ ≄ 0)], p₁ ≃ p₂ → p₁⁻¹ ≃ p₂⁻¹

State before:
ℕ : Type
inst✝² : Natural ℕ
ℤ : Type
inst✝¹ : Integer ℤ
p₂ : Fraction ℤ
inst✝ : AP (p₂ ≄ 0)
⊢ ∀ {p₁ : Fraction ℤ} [inst : AP (p₁ ≄ 0)], p₁ ≃ p₂ → p₁⁻¹ ≃ p₂⁻¹
Tactic:
intro (a//b)
State after:
ℕ : Type
inst✝² : Natural ℕ
ℤ : Type
inst✝¹ : Integer ℤ
p₂ : Fraction ℤ
inst✝ : AP (p₂ ≄ 0)
a b : ℤ
denominator_positive✝ : AP (Positive b)
⊢ ∀ [inst : AP (a//b ≄ 0)], a//b ≃ p₂ → (a//b)⁻¹ ≃ p₂⁻¹

State before:
ℕ : Type
inst✝² : Natural ℕ
ℤ : Type
inst✝¹ : Integer ℤ
p₂ : Fraction ℤ
inst✝ : AP (p₂ ≄ 0)
a b : ℤ
denominator_positive✝ : AP (Positive b)
⊢ ∀ [inst : AP (a//b ≄ 0)], a//b ≃ p₂ → (a//b)⁻¹ ≃ p₂⁻¹
Tactic:
revert p₂
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
⊢ ∀ {p₂ : Fraction ℤ} [inst : AP (p₂ ≄ 0)] [inst_1 : AP (a//b ≄ 0)], a//b ≃ p₂ → (a//b)⁻¹ ≃ p₂⁻¹

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
⊢ ∀ {p₂ : Fraction ℤ} [inst : AP (p₂ ≄ 0)] [inst_1 : AP (a//b ≄ 0)], a//b ≃ p₂ → (a//b)⁻¹ ≃ p₂⁻¹
Tactic:
intro (c//d)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
⊢ ∀ [inst : AP (c//d ≄ 0)] [inst_1 : AP (a//b ≄ 0)], a//b ≃ c//d → (a//b)⁻¹ ≃ (c//d)⁻¹

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
⊢ ∀ [inst : AP (c//d ≄ 0)] [inst_1 : AP (a//b ≄ 0)], a//b ≃ c//d → (a//b)⁻¹ ≃ (c//d)⁻¹
Tactic:
intro _ _ (_ : a//b ≃ c//d)
State after:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
inst✝¹ : AP (c//d ≄ 0)
inst✝ : AP (a//b ≄ 0)
x✝ : a//b ≃ c//d
⊢ (a//b)⁻¹ ≃ (c//d)⁻¹

State before:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
inst✝¹ : AP (c//d ≄ 0)
inst✝ : AP (a//b ≄ 0)
x✝ : a//b ≃ c//d
⊢ (a//b)⁻¹ ≃ (c//d)⁻¹
Tactic:
have : Integer.Nonzero a := nonzero_numerator (a//b)
State after:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
inst✝¹ : AP (c//d ≄ 0)
inst✝ : AP (a//b ≄ 0)
x✝ : a//b ≃ c//d
this : Integer.Nonzero a
⊢ (a//b)⁻¹ ≃ (c//d)⁻¹

State before:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
inst✝¹ : AP (c//d ≄ 0)
inst✝ : AP (a//b ≄ 0)
x✝ : a//b ≃ c//d
this : Integer.Nonzero a
⊢ (a//b)⁻¹ ≃ (c//d)⁻¹
Tactic:
have : Integer.Nonzero c := nonzero_numerator (c//d)
State after:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
inst✝¹ : AP (c//d ≄ 0)
inst✝ : AP (a//b ≄ 0)
x✝ : a//b ≃ c//d
this✝ : Integer.Nonzero a
this : Integer.Nonzero c
⊢ (a//b)⁻¹ ≃ (c//d)⁻¹

State before:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
inst✝¹ : AP (c//d ≄ 0)
inst✝ : AP (a//b ≄ 0)
x✝ : a//b ≃ c//d
this✝ : Integer.Nonzero a
this : Integer.Nonzero c
⊢ (a//b)⁻¹ ≃ (c//d)⁻¹
Tactic:
show (b * sgn a)//(a * sgn a) ≃ (d * sgn c)//(c * sgn c)
State after:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
inst✝¹ : AP (c//d ≄ 0)
inst✝ : AP (a//b ≄ 0)
x✝ : a//b ≃ c//d
this✝ : Integer.Nonzero a
this : Integer.Nonzero c
⊢ (b * sgn a)//(a * sgn a) ≃ (d * sgn c)//(c * sgn c)

State before:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
inst✝¹ : AP (c//d ≄ 0)
inst✝ : AP (a//b ≄ 0)
x✝ : a//b ≃ c//d
this✝ : Integer.Nonzero a
this : Integer.Nonzero c
⊢ (b * sgn a)//(a * sgn a) ≃ (d * sgn c)//(c * sgn c)
Tactic:
show (b * sgn a) * (c * sgn c) ≃ (d * sgn c) * (a * sgn a)
State after:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
inst✝¹ : AP (c//d ≄ 0)
inst✝ : AP (a//b ≄ 0)
x✝ : a//b ≃ c//d
this✝ : Integer.Nonzero a
this : Integer.Nonzero c
⊢ b * sgn a * (c * sgn c) ≃ d * sgn c * (a * sgn a)

State before:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
inst✝¹ : AP (c//d ≄ 0)
inst✝ : AP (a//b ≄ 0)
x✝ : a//b ≃ c//d
this✝ : Integer.Nonzero a
this : Integer.Nonzero c
⊢ b * sgn a * (c * sgn c) ≃ d * sgn c * (a * sgn a)
Tactic:
have : a * d ≃ c * b := ‹a//b ≃ c//d›
State after:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
inst✝¹ : AP (c//d ≄ 0)
inst✝ : AP (a//b ≄ 0)
x✝ : a//b ≃ c//d
this✝¹ : Integer.Nonzero a
this✝ : Integer.Nonzero c
this : a * d ≃ c * b
⊢ b * sgn a * (c * sgn c) ≃ d * sgn c * (a * sgn a)

State before:
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
inst✝¹ : AP (c//d ≄ 0)
inst✝ : AP (a//b ≄ 0)
x✝ : a//b ≃ c//d
this✝¹ : Integer.Nonzero a
this✝ : Integer.Nonzero c
this : a * d ≃ c * b
⊢ b * sgn a * (c * sgn c) ≃ d * sgn c * (a * sgn a)
Tactic:
calc
  (b * sgn a) * (c * sgn c) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (b * c) * (sgn a * sgn c) ≃ _ := AA.substL AA.comm
  (c * b) * (sgn a * sgn c) ≃ _ := AA.substL (Rel.symm ‹a * d ≃ c * b›)
  (a * d) * (sgn a * sgn c) ≃ _ := AA.substL AA.comm
  (d * a) * (sgn a * sgn c) ≃ _ := AA.substR AA.comm
  (d * a) * (sgn c * sgn a) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (d * sgn c) * (a * sgn a) ≃ _ := Rel.refl
State after:
no goals