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

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

State before:
ℕ ℤ : Type
inst✝⁴ : Natural ℕ
inst✝³ : Integer ℤ
ℚ : Type
inst✝² : Core ℚ
inst✝¹ : Addition ℚ
inst✝ : Multiplication ℚ
p₁ p₂ : ℚ
x✝¹ : p₁ ≃ p₂
x✝ : Sqrt1 p₁
⊢ Sqrt1 p₂
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₁ p₂ : ℚ
x✝¹ : p₁ ≃ p₂
x✝ : Sqrt1 p₁
a : ℤ
sqrt1✝ : Integer.Sqrt1 a
eqv : p₁ ≃ from_integer a
⊢ Sqrt1 p₂

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

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

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

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