Theorem: Lean4Axiomatic.Rational.Sqrt1.elim (Lean4Axiomatic/Rational/Multiplication.lean)

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

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

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

State before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
p : ℚ
x✝ : Sqrt1 p
a : ℤ
sqrt1✝ : Integer.Sqrt1 a
eqv this : p ≃ Rational.from_integer a
⊢ p * p ≃ 1
Tactic:
have : p * p ≃ 1 := calc
  p * p             ≃ _ := mul_substL ‹p ≃ (a : ℚ)›
  (a : ℚ) * p       ≃ _ := mul_substR ‹p ≃ (a : ℚ)›
  (a : ℚ) * (a : ℚ) ≃ _ := eqv_symm mul_compat_from_integer
  ((a * a : ℤ) : ℚ) ≃ _ := from_integer_subst ‹Integer.Sqrt1 a›.elim
  (1 : ℚ)           ≃ _ := eqv_refl
  1                 ≃ _ := eqv_refl
State after:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
p : ℚ
x✝ : Sqrt1 p
a : ℤ
sqrt1✝ : Integer.Sqrt1 a
eqv this✝ : p ≃ Rational.from_integer a
this : p * p ≃ 1
⊢ p * p ≃ 1

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