internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Integer.mul_split_zero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a ≃ 0 ∨ b ≃ 0
⊢ a * b ≃ 0
Tactic:
match ‹a ≃ 0 ∨ b ≃ 0› with
| Or.inl (_ : a ≃ 0) => calc
  a * b ≃ _ := AA.substL ‹a ≃ 0›
  0 * b ≃ _ := AA.absorbL
  0     ≃ _ := Rel.refl
| Or.inr (_ : b ≃ 0) => calc
  a * b ≃ _ := AA.substR ‹b ≃ 0›
  a * 0 ≃ _ := AA.absorbR
  0     ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.mul_split_zero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a ≃ 0 ∨ b ≃ 0
h✝ : a ≃ 0
⊢ a * b ≃ 0
Tactic:
calc
a * b ≃ _ := AA.substL ‹a ≃ 0›
0 * b ≃ _ := AA.absorbL
0     ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.mul_split_zero
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : a ≃ 0 ∨ b ≃ 0
h✝ : b ≃ 0
⊢ a * b ≃ 0
Tactic:
calc
a * b ≃ _ := AA.substR ‹b ≃ 0›
a * 0 ≃ _ := AA.absorbR
0     ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzero_factors_if_nonzero_product
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
⊢ Nonzero (a * b) → Nonzero a ∧ Nonzero b
Tactic:
intro (_ : Nonzero (a * b))
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Nonzero (a * b)
⊢ Nonzero a ∧ Nonzero b
Theorem: Lean4Axiomatic.Integer.nonzero_factors_if_nonzero_product
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Nonzero (a * b)
⊢ Nonzero a ∧ Nonzero b
Tactic:
have : a * b ≄ 0 := nonzero_iff_neqv_zero.mp ‹Nonzero (a * b)›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Nonzero (a * b)
this : a * b ≄ 0
⊢ Nonzero a ∧ Nonzero b
Theorem: Lean4Axiomatic.Integer.nonzero_factors_if_nonzero_product
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Nonzero (a * b)
this : a * b ≄ 0
⊢ Nonzero a ∧ Nonzero b
Tactic:
have : ¬(a ≃ 0 ∨ b ≃ 0) := mt mul_split_zero.mpr ‹a * b ≄ 0›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Nonzero (a * b)
this✝ : a * b ≄ 0
this : ¬(a ≃ 0 ∨ b ≃ 0)
⊢ Nonzero a ∧ Nonzero b
Theorem: Lean4Axiomatic.Integer.nonzero_factors_if_nonzero_product
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Nonzero (a * b)
this✝ : a * b ≄ 0
this : ¬(a ≃ 0 ∨ b ≃ 0)
⊢ Nonzero a ∧ Nonzero b
Tactic:
have (And.intro (_ : a ≄ 0) (_ : b ≄ 0)) :=
  Logic.not_or_iff_and_not.mp ‹¬(a ≃ 0 ∨ b ≃ 0)›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Nonzero (a * b)
this✝ : a * b ≄ 0
this : ¬(a ≃ 0 ∨ b ≃ 0)
left✝ : a ≄ 0
right✝ : b ≄ 0
⊢ Nonzero a ∧ Nonzero b
Theorem: Lean4Axiomatic.Integer.nonzero_factors_if_nonzero_product
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Nonzero (a * b)
this✝ : a * b ≄ 0
this : ¬(a ≃ 0 ∨ b ≃ 0)
left✝ : a ≄ 0
right✝ : b ≄ 0
⊢ Nonzero a ∧ Nonzero b
Tactic:
have : Nonzero a := nonzero_iff_neqv_zero.mpr ‹a ≄ 0›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Nonzero (a * b)
this✝¹ : a * b ≄ 0
this✝ : ¬(a ≃ 0 ∨ b ≃ 0)
left✝ : a ≄ 0
right✝ : b ≄ 0
this : Nonzero a
⊢ Nonzero a ∧ Nonzero b
Theorem: Lean4Axiomatic.Integer.nonzero_factors_if_nonzero_product
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Nonzero (a * b)
this✝¹ : a * b ≄ 0
this✝ : ¬(a ≃ 0 ∨ b ≃ 0)
left✝ : a ≄ 0
right✝ : b ≄ 0
this : Nonzero a
⊢ Nonzero a ∧ Nonzero b
Tactic:
have : Nonzero b := nonzero_iff_neqv_zero.mpr ‹b ≄ 0›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Nonzero (a * b)
this✝² : a * b ≄ 0
this✝¹ : ¬(a ≃ 0 ∨ b ≃ 0)
left✝ : a ≄ 0
right✝ : b ≄ 0
this✝ : Nonzero a
this : Nonzero b
⊢ Nonzero a ∧ Nonzero b
Theorem: Lean4Axiomatic.Integer.nonzero_factors_if_nonzero_product
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
x✝ : Nonzero (a * b)
this✝² : a * b ≄ 0
this✝¹ : ¬(a ≃ 0 ∨ b ≃ 0)
left✝ : a ≄ 0
right✝ : b ≄ 0
this✝ : Nonzero a
this : Nonzero b
⊢ Nonzero a ∧ Nonzero b
Tactic:
exact And.intro ‹Nonzero a› ‹Nonzero b›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.nonzero_squared_eqv_positive_nat_squared
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Nonzero a → ∃ n, Positive n ∧ a * a ≃ coe (n * n)
Tactic:
intro (_ : Nonzero a)
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
⊢ ∃ n, Positive n ∧ a * a ≃ coe (n * n)
Theorem: Lean4Axiomatic.Integer.nonzero_squared_eqv_positive_nat_squared
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
⊢ ∃ n, Positive n ∧ a * a ≃ coe (n * n)
Tactic:
have (Nonzero.intro (sa : ℤ) (_ : Sqrt1 sa) nws) := ‹Nonzero a›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
sa : ℤ
sqrt1✝ : Sqrt1 sa
nws : NonzeroWithSign a sa
⊢ ∃ n, Positive n ∧ a * a ≃ coe (n * n)
Theorem: Lean4Axiomatic.Integer.nonzero_squared_eqv_positive_nat_squared
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
sa : ℤ
sqrt1✝ : Sqrt1 sa
nws : NonzeroWithSign a sa
⊢ ∃ n, Positive n ∧ a * a ≃ coe (n * n)
Tactic:
have (NonzeroWithSign.intro (n : ℕ) (_ : Positive n) (_ : a ≃ sa * n)) := nws
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
sa : ℤ
sqrt1✝ : Sqrt1 sa
nws : NonzeroWithSign a sa
n : ℕ
pos✝ : Positive n
eqv✝ : a ≃ sa * coe n
⊢ ∃ n, Positive n ∧ a * a ≃ coe (n * n)
Theorem: Lean4Axiomatic.Integer.nonzero_squared_eqv_positive_nat_squared
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
sa : ℤ
sqrt1✝ : Sqrt1 sa
nws : NonzeroWithSign a sa
n : ℕ
pos✝ : Positive n
eqv✝ : a ≃ sa * coe n
⊢ ∃ n, Positive n ∧ a * a ≃ coe (n * n)
Tactic:
have : a * a ≃ (n * n : ℕ) := calc
  a * a               ≃ _ := AA.substL ‹a ≃ sa * n›
  (sa * n) * a        ≃ _ := AA.substR ‹a ≃ sa * n›
  (sa * n) * (sa * n) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (sa * sa) * (n * n) ≃ _ := AA.substL ‹Sqrt1 sa›.elim
  (1 : ℤ) * (n * n)   ≃ _ := AA.identL
  (n : ℤ) * n         ≃ _ := Rel.symm AA.compat₂
  ((n * n : ℕ) : ℤ)   ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
sa : ℤ
sqrt1✝ : Sqrt1 sa
nws : NonzeroWithSign a sa
n : ℕ
pos✝ : Positive n
eqv✝ : a ≃ sa * coe n
this : a * a ≃ coe (n * n)
⊢ ∃ n, Positive n ∧ a * a ≃ coe (n * n)
Theorem: Lean4Axiomatic.Integer.nonzero_squared_eqv_positive_nat_squared
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Nonzero a
sa : ℤ
sqrt1✝ : Sqrt1 sa
nws : NonzeroWithSign a sa
n : ℕ
pos✝ : Positive n
eqv✝ : a ≃ sa * coe n
this : a * a ≃ coe (n * n)
⊢ ∃ n, Positive n ∧ a * a ≃ coe (n * n)
Tactic:
exact Exists.intro n (And.intro ‹Positive n› ‹a * a ≃ (n * n : ℕ)›)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.sqrt1_factors_if_sqrt1_product
Proof 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))
Proof 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
Theorem: Lean4Axiomatic.Integer.sqrt1_factors_if_sqrt1_product
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Integer.sqrt1_factors_if_sqrt1_product
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Integer.sqrt1_factors_if_sqrt1_product
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Integer.sqrt1_factors_if_sqrt1_product
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Integer.sqrt1_factors_if_sqrt1_product
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Integer.sqrt1_factors_if_sqrt1_product
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Integer.sqrt1_factors_if_sqrt1_product
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Integer.sqrt1_factors_if_sqrt1_product
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Integer.sqrt1_factors_if_sqrt1_product
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Integer.sqrt1_factors_if_sqrt1_product
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Integer.sqrt1_factors_if_sqrt1_product
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Integer.sqrt1_factors_if_sqrt1_product
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Integer.sqrt1_factors_if_sqrt1_product
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Integer.sqrt1_factors_if_sqrt1_product
Proof 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›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.mul_sqrt1_eqv
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
⊢ a * b ≃ 1 ↔ Sqrt1 b ∧ a ≃ b
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
⊢ a * b ≃ 1 → Sqrt1 b ∧ a ≃ b

case mpr
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
⊢ Sqrt1 b ∧ a ≃ b → a * b ≃ 1