Theorem: Lean4Axiomatic.Integer.sqrt1_factors_if_sqrt1_product (Lean4Axiomatic/Integer/Sign.lean)

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
⊢ Sqrt1 (a * b) → Sqrt1 a ∧ Sqrt1 b
Tactic:
intro (_ : Sqrt1 (a * b))
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
⊢ Sqrt1 a ∧ Sqrt1 b

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
⊢ Sqrt1 a ∧ Sqrt1 b
Tactic:
have : Nonzero (a * b) := nonzero_sqrt1
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
this : Nonzero (a * b)
⊢ Sqrt1 a ∧ Sqrt1 b

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
this : Nonzero (a * b)
⊢ Sqrt1 a ∧ Sqrt1 b
Tactic:
have (And.intro (_ : Nonzero a) (_ : Nonzero b)) :=
  nonzero_factors_if_nonzero_product this
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
this : Nonzero (a * b)
left✝ : Nonzero a
right✝ : Nonzero b
⊢ Sqrt1 a ∧ Sqrt1 b

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
this : Nonzero (a * b)
left✝ : Nonzero a
right✝ : Nonzero b
⊢ Sqrt1 a ∧ Sqrt1 b
Tactic:
have (Exists.intro (n : ℕ) (And.intro (_ : Positive n) a_eqv)) :=
  nonzero_squared_eqv_positive_nat_squared ‹Nonzero a›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
this : Nonzero (a * b)
left✝¹ : Nonzero a
right✝ : Nonzero b
n : ℕ
left✝ : Positive n
a_eqv : a * a ≃ coe (n * n)
⊢ Sqrt1 a ∧ Sqrt1 b

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
this : Nonzero (a * b)
left✝¹ : Nonzero a
right✝ : Nonzero b
n : ℕ
left✝ : Positive n
a_eqv : a * a ≃ coe (n * n)
⊢ Sqrt1 a ∧ Sqrt1 b
Tactic:
have : a * a ≃ (n * n : ℕ) := a_eqv
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
this✝ : Nonzero (a * b)
left✝¹ : Nonzero a
right✝ : Nonzero b
n : ℕ
left✝ : Positive n
a_eqv this : a * a ≃ coe (n * n)
⊢ Sqrt1 a ∧ Sqrt1 b

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
this✝ : Nonzero (a * b)
left✝¹ : Nonzero a
right✝ : Nonzero b
n : ℕ
left✝ : Positive n
a_eqv this : a * a ≃ coe (n * n)
⊢ Sqrt1 a ∧ Sqrt1 b
Tactic:
have (Exists.intro (m : ℕ) (And.intro (_ : Positive m) b_eqv)) :=
  nonzero_squared_eqv_positive_nat_squared ‹Nonzero b›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
this✝ : Nonzero (a * b)
left✝² : Nonzero a
right✝ : Nonzero b
n : ℕ
left✝¹ : Positive n
a_eqv this : a * a ≃ coe (n * n)
m : ℕ
left✝ : Positive m
b_eqv : b * b ≃ coe (m * m)
⊢ Sqrt1 a ∧ Sqrt1 b

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
this✝ : Nonzero (a * b)
left✝² : Nonzero a
right✝ : Nonzero b
n : ℕ
left✝¹ : Positive n
a_eqv this : a * a ≃ coe (n * n)
m : ℕ
left✝ : Positive m
b_eqv : b * b ≃ coe (m * m)
⊢ Sqrt1 a ∧ Sqrt1 b
Tactic:
have : b * b ≃ (m * m : ℕ) := b_eqv
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
this✝¹ : Nonzero (a * b)
left✝² : Nonzero a
right✝ : Nonzero b
n : ℕ
left✝¹ : Positive n
a_eqv this✝ : a * a ≃ coe (n * n)
m : ℕ
left✝ : Positive m
b_eqv this : b * b ≃ coe (m * m)
⊢ Sqrt1 a ∧ Sqrt1 b

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
this✝¹ : Nonzero (a * b)
left✝² : Nonzero a
right✝ : Nonzero b
n : ℕ
left✝¹ : Positive n
a_eqv this✝ : a * a ≃ coe (n * n)
m : ℕ
left✝ : Positive m
b_eqv this : b * b ≃ coe (m * m)
⊢ Sqrt1 a ∧ Sqrt1 b
Tactic:
have : (((n * n) * (m * m) : ℕ) : ℤ) ≃ ((1 : ℕ) : ℤ) := calc
  (((n * n) * (m * m) : ℕ) : ℤ)
    ≃ _ := AA.compat₂
  ((n * n : ℕ) : ℤ) * ((m * m : ℕ) : ℤ)
    ≃ _ := AA.substL (Rel.symm ‹a * a ≃ (n * n : ℕ)›)
  (a * a) * ((m * m : ℕ) : ℤ)
    ≃ _ := AA.substR (Rel.symm ‹b * b ≃ (m * m : ℕ)›)
  (a * a) * (b * b)
    ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (a * b) * (a * b)
    ≃ _ := ‹Sqrt1 (a * b)›.elim
  1
    ≃ _ := Rel.refl
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
this✝² : Nonzero (a * b)
left✝² : Nonzero a
right✝ : Nonzero b
n : ℕ
left✝¹ : Positive n
a_eqv this✝¹ : a * a ≃ coe (n * n)
m : ℕ
left✝ : Positive m
b_eqv this✝ : b * b ≃ coe (m * m)
this : coe (n * n * (m * m)) ≃ coe 1
⊢ Sqrt1 a ∧ Sqrt1 b

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
this✝² : Nonzero (a * b)
left✝² : Nonzero a
right✝ : Nonzero b
n : ℕ
left✝¹ : Positive n
a_eqv this✝¹ : a * a ≃ coe (n * n)
m : ℕ
left✝ : Positive m
b_eqv this✝ : b * b ≃ coe (m * m)
this : coe (n * n * (m * m)) ≃ coe 1
⊢ Sqrt1 a ∧ Sqrt1 b
Tactic:
have : (n * n) * (m * m) ≃ 1 := AA.inject this
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
this✝³ : Nonzero (a * b)
left✝² : Nonzero a
right✝ : Nonzero b
n : ℕ
left✝¹ : Positive n
a_eqv this✝² : a * a ≃ coe (n * n)
m : ℕ
left✝ : Positive m
b_eqv this✝¹ : b * b ≃ coe (m * m)
this✝ : coe (n * n * (m * m)) ≃ coe 1
this : n * n * (m * m) ≃ 1
⊢ Sqrt1 a ∧ Sqrt1 b

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
this✝³ : Nonzero (a * b)
left✝² : Nonzero a
right✝ : Nonzero b
n : ℕ
left✝¹ : Positive n
a_eqv this✝² : a * a ≃ coe (n * n)
m : ℕ
left✝ : Positive m
b_eqv this✝¹ : b * b ≃ coe (m * m)
this✝ : coe (n * n * (m * m)) ≃ coe 1
this : n * n * (m * m) ≃ 1
⊢ Sqrt1 a ∧ Sqrt1 b
Tactic:
have (And.intro (_ : n * n ≃ 1) (_ : m * m ≃ 1)) :=
  Natural.factors_eqv_1.mp this
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
this✝³ : Nonzero (a * b)
left✝³ : Nonzero a
right✝¹ : Nonzero b
n : ℕ
left✝² : Positive n
a_eqv this✝² : a * a ≃ coe (n * n)
m : ℕ
left✝¹ : Positive m
b_eqv this✝¹ : b * b ≃ coe (m * m)
this✝ : coe (n * n * (m * m)) ≃ coe 1
this : n * n * (m * m) ≃ 1
left✝ : n * n ≃ 1
right✝ : m * m ≃ 1
⊢ Sqrt1 a ∧ Sqrt1 b

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
this✝³ : Nonzero (a * b)
left✝³ : Nonzero a
right✝¹ : Nonzero b
n : ℕ
left✝² : Positive n
a_eqv this✝² : a * a ≃ coe (n * n)
m : ℕ
left✝¹ : Positive m
b_eqv this✝¹ : b * b ≃ coe (m * m)
this✝ : coe (n * n * (m * m)) ≃ coe 1
this : n * n * (m * m) ≃ 1
left✝ : n * n ≃ 1
right✝ : m * m ≃ 1
⊢ Sqrt1 a ∧ Sqrt1 b
Tactic:
have : a * a ≃ 1 := calc
  a * a             ≃ _ := ‹a * a ≃ (n * n : ℕ)›
  ((n * n : ℕ) : ℤ) ≃ _ := AA.subst₁ ‹n * n ≃ 1›
  (1 : ℤ)           ≃ _ := Rel.refl
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
this✝⁴ : Nonzero (a * b)
left✝³ : Nonzero a
right✝¹ : Nonzero b
n : ℕ
left✝² : Positive n
a_eqv this✝³ : a * a ≃ coe (n * n)
m : ℕ
left✝¹ : Positive m
b_eqv this✝² : b * b ≃ coe (m * m)
this✝¹ : coe (n * n * (m * m)) ≃ coe 1
this✝ : n * n * (m * m) ≃ 1
left✝ : n * n ≃ 1
right✝ : m * m ≃ 1
this : a * a ≃ 1
⊢ Sqrt1 a ∧ Sqrt1 b

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
this✝⁴ : Nonzero (a * b)
left✝³ : Nonzero a
right✝¹ : Nonzero b
n : ℕ
left✝² : Positive n
a_eqv this✝³ : a * a ≃ coe (n * n)
m : ℕ
left✝¹ : Positive m
b_eqv this✝² : b * b ≃ coe (m * m)
this✝¹ : coe (n * n * (m * m)) ≃ coe 1
this✝ : n * n * (m * m) ≃ 1
left✝ : n * n ≃ 1
right✝ : m * m ≃ 1
this : a * a ≃ 1
⊢ Sqrt1 a ∧ Sqrt1 b
Tactic:
have : b * b ≃ 1 := calc
  b * b             ≃ _ := ‹b * b ≃ (m * m : ℕ)›
  ((m * m : ℕ) : ℤ) ≃ _ := AA.subst₁ ‹m * m ≃ 1›
  (1 : ℤ)           ≃ _ := Rel.refl
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
this✝⁵ : Nonzero (a * b)
left✝³ : Nonzero a
right✝¹ : Nonzero b
n : ℕ
left✝² : Positive n
a_eqv this✝⁴ : a * a ≃ coe (n * n)
m : ℕ
left✝¹ : Positive m
b_eqv this✝³ : b * b ≃ coe (m * m)
this✝² : coe (n * n * (m * m)) ≃ coe 1
this✝¹ : n * n * (m * m) ≃ 1
left✝ : n * n ≃ 1
right✝ : m * m ≃ 1
this✝ : a * a ≃ 1
this : b * b ≃ 1
⊢ Sqrt1 a ∧ Sqrt1 b

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
this✝⁵ : Nonzero (a * b)
left✝³ : Nonzero a
right✝¹ : Nonzero b
n : ℕ
left✝² : Positive n
a_eqv this✝⁴ : a * a ≃ coe (n * n)
m : ℕ
left✝¹ : Positive m
b_eqv this✝³ : b * b ≃ coe (m * m)
this✝² : coe (n * n * (m * m)) ≃ coe 1
this✝¹ : n * n * (m * m) ≃ 1
left✝ : n * n ≃ 1
right✝ : m * m ≃ 1
this✝ : a * a ≃ 1
this : b * b ≃ 1
⊢ Sqrt1 a ∧ Sqrt1 b
Tactic:
have : Sqrt1 a := Sqrt1.mk ‹a * a ≃ 1›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
this✝⁶ : Nonzero (a * b)
left✝³ : Nonzero a
right✝¹ : Nonzero b
n : ℕ
left✝² : Positive n
a_eqv this✝⁵ : a * a ≃ coe (n * n)
m : ℕ
left✝¹ : Positive m
b_eqv this✝⁴ : b * b ≃ coe (m * m)
this✝³ : coe (n * n * (m * m)) ≃ coe 1
this✝² : n * n * (m * m) ≃ 1
left✝ : n * n ≃ 1
right✝ : m * m ≃ 1
this✝¹ : a * a ≃ 1
this✝ : b * b ≃ 1
this : Sqrt1 a
⊢ Sqrt1 a ∧ Sqrt1 b

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
this✝⁶ : Nonzero (a * b)
left✝³ : Nonzero a
right✝¹ : Nonzero b
n : ℕ
left✝² : Positive n
a_eqv this✝⁵ : a * a ≃ coe (n * n)
m : ℕ
left✝¹ : Positive m
b_eqv this✝⁴ : b * b ≃ coe (m * m)
this✝³ : coe (n * n * (m * m)) ≃ coe 1
this✝² : n * n * (m * m) ≃ 1
left✝ : n * n ≃ 1
right✝ : m * m ≃ 1
this✝¹ : a * a ≃ 1
this✝ : b * b ≃ 1
this : Sqrt1 a
⊢ Sqrt1 a ∧ Sqrt1 b
Tactic:
have : Sqrt1 b := Sqrt1.mk ‹b * b ≃ 1›
State after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
this✝⁷ : Nonzero (a * b)
left✝³ : Nonzero a
right✝¹ : Nonzero b
n : ℕ
left✝² : Positive n
a_eqv this✝⁶ : a * a ≃ coe (n * n)
m : ℕ
left✝¹ : Positive m
b_eqv this✝⁵ : b * b ≃ coe (m * m)
this✝⁴ : coe (n * n * (m * m)) ≃ coe 1
this✝³ : n * n * (m * m) ≃ 1
left✝ : n * n ≃ 1
right✝ : m * m ≃ 1
this✝² : a * a ≃ 1
this✝¹ : b * b ≃ 1
this✝ : Sqrt1 a
this : Sqrt1 b
⊢ Sqrt1 a ∧ Sqrt1 b

State before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Sqrt1 (a * b)
this✝⁷ : Nonzero (a * b)
left✝³ : Nonzero a
right✝¹ : Nonzero b
n : ℕ
left✝² : Positive n
a_eqv this✝⁶ : a * a ≃ coe (n * n)
m : ℕ
left✝¹ : Positive m
b_eqv this✝⁵ : b * b ≃ coe (m * m)
this✝⁴ : coe (n * n * (m * m)) ≃ coe 1
this✝³ : n * n * (m * m) ≃ 1
left✝ : n * n ≃ 1
right✝ : m * m ≃ 1
this✝² : a * a ≃ 1
this✝¹ : b * b ≃ 1
this✝ : Sqrt1 a
this : Sqrt1 b
⊢ Sqrt1 a ∧ Sqrt1 b
Tactic:
exact And.intro ‹Sqrt1 a› ‹Sqrt1 b›
State after:
no goals