Theorem: Lean4Axiomatic.Rational.as_ratio (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 : ℚ
⊢ AsRatio p
Tactic:
apply ind_fraction_on p
State after:
ℕ ℤ : Type
inst✝⁷ : Natural ℕ
inst✝⁶ : Integer ℤ
ℚ : Type
inst✝⁵ : Core ℚ
inst✝⁴ : Addition ℚ
inst✝³ : Multiplication ℚ
inst✝² : Negation ℚ
inst✝¹ : Reciprocation ℚ
inst✝ : Division ℚ
p : ℚ
⊢ ∀ (a b : ℤ) [inst : Integer.Nonzero b], AsRatio (from_integer a / from_integer b)

State before:
ℕ ℤ : Type
inst✝⁷ : Natural ℕ
inst✝⁶ : Integer ℤ
ℚ : Type
inst✝⁵ : Core ℚ
inst✝⁴ : Addition ℚ
inst✝³ : Multiplication ℚ
inst✝² : Negation ℚ
inst✝¹ : Reciprocation ℚ
inst✝ : Division ℚ
p : ℚ
⊢ ∀ (a b : ℤ) [inst : Integer.Nonzero b], AsRatio (from_integer a / from_integer b)
Tactic:
intro (a : ℤ) (b : ℤ) (_ : Integer.Nonzero b)
State after:
ℕ ℤ : Type
inst✝⁷ : Natural ℕ
inst✝⁶ : Integer ℤ
ℚ : Type
inst✝⁵ : Core ℚ
inst✝⁴ : Addition ℚ
inst✝³ : Multiplication ℚ
inst✝² : Negation ℚ
inst✝¹ : Reciprocation ℚ
inst✝ : Division ℚ
p : ℚ
a b : ℤ
x✝ : Integer.Nonzero b
⊢ AsRatio (from_integer a / from_integer b)

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