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

State before:
ℕ ℤ : Type
inst✝⁷ : Natural ℕ
inst✝⁶ : Integer ℤ
ℚ : Type
inst✝⁵ : Core ℚ
inst✝⁴ : Addition ℚ
inst✝³ : Multiplication ℚ
inst✝² : Negation ℚ
inst✝¹ : Reciprocation ℚ
inst✝ : Division ℚ
a b : ℚ
⊢ a ≃ b → AsRatio a → AsRatio b
Tactic:
intro (_ : a ≃ b) (_ : AsRatio a)
State after:
ℕ ℤ : Type
inst✝⁷ : Natural ℕ
inst✝⁶ : Integer ℤ
ℚ : Type
inst✝⁵ : Core ℚ
inst✝⁴ : Addition ℚ
inst✝³ : Multiplication ℚ
inst✝² : Negation ℚ
inst✝¹ : Reciprocation ℚ
inst✝ : Division ℚ
a b : ℚ
x✝¹ : a ≃ b
x✝ : AsRatio a
⊢ AsRatio b

State before:
ℕ ℤ : Type
inst✝⁷ : Natural ℕ
inst✝⁶ : Integer ℤ
ℚ : Type
inst✝⁵ : Core ℚ
inst✝⁴ : Addition ℚ
inst✝³ : Multiplication ℚ
inst✝² : Negation ℚ
inst✝¹ : Reciprocation ℚ
inst✝ : Division ℚ
a b : ℚ
x✝¹ : a ≃ b
x✝ : AsRatio a
⊢ AsRatio b
Tactic:
have (AsRatio.intro (n : ℤ) (d : ℤ) (_ : Integer.Nonzero d) eqv)
  := ‹AsRatio a›
State after:
ℕ ℤ : Type
inst✝⁷ : Natural ℕ
inst✝⁶ : Integer ℤ
ℚ : Type
inst✝⁵ : Core ℚ
inst✝⁴ : Addition ℚ
inst✝³ : Multiplication ℚ
inst✝² : Negation ℚ
inst✝¹ : Reciprocation ℚ
inst✝ : Division ℚ
a b : ℚ
x✝¹ : a ≃ b
x✝ : AsRatio a
n d : ℤ
b_nonzero✝ : Integer.Nonzero d
eqv : a ≃ from_integer n / from_integer d
⊢ AsRatio b

State before:
ℕ ℤ : Type
inst✝⁷ : Natural ℕ
inst✝⁶ : Integer ℤ
ℚ : Type
inst✝⁵ : Core ℚ
inst✝⁴ : Addition ℚ
inst✝³ : Multiplication ℚ
inst✝² : Negation ℚ
inst✝¹ : Reciprocation ℚ
inst✝ : Division ℚ
a b : ℚ
x✝¹ : a ≃ b
x✝ : AsRatio a
n d : ℤ
b_nonzero✝ : Integer.Nonzero d
eqv : a ≃ from_integer n / from_integer d
⊢ AsRatio b
Tactic:
have : a ≃ n / d := eqv
State after:
ℕ ℤ : Type
inst✝⁷ : Natural ℕ
inst✝⁶ : Integer ℤ
ℚ : Type
inst✝⁵ : Core ℚ
inst✝⁴ : Addition ℚ
inst✝³ : Multiplication ℚ
inst✝² : Negation ℚ
inst✝¹ : Reciprocation ℚ
inst✝ : Division ℚ
a b : ℚ
x✝¹ : a ≃ b
x✝ : AsRatio a
n d : ℤ
b_nonzero✝ : Integer.Nonzero d
eqv this : a ≃ from_integer n / from_integer d
⊢ AsRatio b

State before:
ℕ ℤ : Type
inst✝⁷ : Natural ℕ
inst✝⁶ : Integer ℤ
ℚ : Type
inst✝⁵ : Core ℚ
inst✝⁴ : Addition ℚ
inst✝³ : Multiplication ℚ
inst✝² : Negation ℚ
inst✝¹ : Reciprocation ℚ
inst✝ : Division ℚ
a b : ℚ
x✝¹ : a ≃ b
x✝ : AsRatio a
n d : ℤ
b_nonzero✝ : Integer.Nonzero d
eqv this : a ≃ from_integer n / from_integer d
⊢ AsRatio b
Tactic:
have : b ≃ n / d := calc
  _ ≃ b     := eqv_refl
  _ ≃ a     := eqv_symm ‹a ≃ b›
  _ ≃ n / d := ‹a ≃ n / d›
State after:
ℕ ℤ : Type
inst✝⁷ : Natural ℕ
inst✝⁶ : Integer ℤ
ℚ : Type
inst✝⁵ : Core ℚ
inst✝⁴ : Addition ℚ
inst✝³ : Multiplication ℚ
inst✝² : Negation ℚ
inst✝¹ : Reciprocation ℚ
inst✝ : Division ℚ
a b : ℚ
x✝¹ : a ≃ b
x✝ : AsRatio a
n d : ℤ
b_nonzero✝ : Integer.Nonzero d
eqv this✝ : a ≃ from_integer n / from_integer d
this : b ≃ from_integer n / from_integer d
⊢ AsRatio b

State before:
ℕ ℤ : Type
inst✝⁷ : Natural ℕ
inst✝⁶ : Integer ℤ
ℚ : Type
inst✝⁵ : Core ℚ
inst✝⁴ : Addition ℚ
inst✝³ : Multiplication ℚ
inst✝² : Negation ℚ
inst✝¹ : Reciprocation ℚ
inst✝ : Division ℚ
a b : ℚ
x✝¹ : a ≃ b
x✝ : AsRatio a
n d : ℤ
b_nonzero✝ : Integer.Nonzero d
eqv this✝ : a ≃ from_integer n / from_integer d
this : b ≃ from_integer n / from_integer d
⊢ AsRatio b
Tactic:
exact AsRatio.intro n d ‹Integer.Nonzero d› ‹b ≃ n / d›
State after:
no goals