Theorem: Lean4Axiomatic.Rational.from_integer_preserves_sqrt1 (Lean4Axiomatic/Rational/Multiplication.lean)

State before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
⊢ Sqrt1 (from_integer a) ↔ Integer.Sqrt1 a
Tactic:
apply Iff.intro
State after:
case mp
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
⊢ Sqrt1 (from_integer a) → Integer.Sqrt1 a

case mpr
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
⊢ Integer.Sqrt1 a → Sqrt1 (from_integer a)

State before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
⊢ Sqrt1 (from_integer a) → Integer.Sqrt1 a
Tactic:
case mp =>
  intro (_ : Sqrt1 (a : ℚ))
  show Integer.Sqrt1 a
  have (Sqrt1.from_integer_intro (b : ℤ) (_ : Integer.Sqrt1 b) eqv) :=
    ‹Sqrt1 (a : ℚ)›
  have : (b : ℚ) ≃ (a : ℚ) := eqv_symm eqv
  have : b ≃ a := from_integer_inject this
  have : Integer.Sqrt1 a := Integer.sqrt1_subst this ‹Integer.Sqrt1 b›
  exact this
State after:
no goals

State before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
⊢ Integer.Sqrt1 a → Sqrt1 (from_integer a)
Tactic:
case mpr =>
  intro (_ : Integer.Sqrt1 a)
  show Sqrt1 (a : ℚ)
  exact Sqrt1.from_integer eqv_refl
State after:
no goals

State before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
⊢ Sqrt1 (from_integer a) → Integer.Sqrt1 a
Tactic:
intro (_ : Sqrt1 (a : ℚ))
State after:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
x✝ : Sqrt1 (from_integer a)
⊢ Integer.Sqrt1 a

State before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
x✝ : Sqrt1 (from_integer a)
⊢ Integer.Sqrt1 a
Tactic:
have (Sqrt1.from_integer_intro (b : ℤ) (_ : Integer.Sqrt1 b) eqv) :=
  ‹Sqrt1 (a : ℚ)›
State after:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
x✝ : Sqrt1 (from_integer a)
b : ℤ
sqrt1✝ : Integer.Sqrt1 b
eqv : from_integer a ≃ from_integer b
⊢ Integer.Sqrt1 a

State before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
x✝ : Sqrt1 (from_integer a)
b : ℤ
sqrt1✝ : Integer.Sqrt1 b
eqv : from_integer a ≃ from_integer b
⊢ Integer.Sqrt1 a
Tactic:
have : (b : ℚ) ≃ (a : ℚ) := eqv_symm eqv
State after:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
x✝ : Sqrt1 (from_integer a)
b : ℤ
sqrt1✝ : Integer.Sqrt1 b
eqv : from_integer a ≃ from_integer b
this : from_integer b ≃ from_integer a
⊢ Integer.Sqrt1 a

State before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
x✝ : Sqrt1 (from_integer a)
b : ℤ
sqrt1✝ : Integer.Sqrt1 b
eqv : from_integer a ≃ from_integer b
this : from_integer b ≃ from_integer a
⊢ Integer.Sqrt1 a
Tactic:
have : b ≃ a := from_integer_inject this
State after:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
x✝ : Sqrt1 (from_integer a)
b : ℤ
sqrt1✝ : Integer.Sqrt1 b
eqv : from_integer a ≃ from_integer b
this✝ : from_integer b ≃ from_integer a
this : b ≃ a
⊢ Integer.Sqrt1 a

State before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
x✝ : Sqrt1 (from_integer a)
b : ℤ
sqrt1✝ : Integer.Sqrt1 b
eqv : from_integer a ≃ from_integer b
this✝ : from_integer b ≃ from_integer a
this : b ≃ a
⊢ Integer.Sqrt1 a
Tactic:
have : Integer.Sqrt1 a := Integer.sqrt1_subst this ‹Integer.Sqrt1 b›
State after:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
x✝ : Sqrt1 (from_integer a)
b : ℤ
sqrt1✝ : Integer.Sqrt1 b
eqv : from_integer a ≃ from_integer b
this✝¹ : from_integer b ≃ from_integer a
this✝ : b ≃ a
this : Integer.Sqrt1 a
⊢ Integer.Sqrt1 a

State before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
x✝ : Sqrt1 (from_integer a)
b : ℤ
sqrt1✝ : Integer.Sqrt1 b
eqv : from_integer a ≃ from_integer b
this✝¹ : from_integer b ≃ from_integer a
this✝ : b ≃ a
this : Integer.Sqrt1 a
⊢ Integer.Sqrt1 a
Tactic:
exact this
State after:
no goals

State before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
⊢ Integer.Sqrt1 a → Sqrt1 (from_integer a)
Tactic:
intro (_ : Integer.Sqrt1 a)
State after:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
x✝ : Integer.Sqrt1 a
⊢ Sqrt1 (from_integer a)

State before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
a : ℤ
x✝ : Integer.Sqrt1 a
⊢ Sqrt1 (from_integer a)
Tactic:
exact Sqrt1.from_integer eqv_refl
State after:
no goals