Theorem: Lean4Axiomatic.Natural.sqrt1 (Lean4Axiomatic/Natural/Multiplication.lean)

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
⊢ n * n ≃ 1 ↔ n ≃ 1
Tactic:
apply Iff.intro
State after:
case mp
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
⊢ n * n ≃ 1 → n ≃ 1

case mpr
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
⊢ n ≃ 1 → n * n ≃ 1

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
⊢ n * n ≃ 1 → n ≃ 1
Tactic:
case mp =>
  intro (_ : n * n ≃ 1)
  show n ≃ 1
  have (And.intro (_ : n ≃ 1) _) := factors_eqv_1.mp ‹n * n ≃ 1›
  exact ‹n ≃ 1›
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
⊢ n ≃ 1 → n * n ≃ 1
Tactic:
case mpr =>
  intro (_ : n ≃ 1)
  show n * n ≃ 1
  have : n * n ≃ 1 := factors_eqv_1.mpr (And.intro ‹n ≃ 1› ‹n ≃ 1›)
  exact this
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
⊢ n * n ≃ 1 → n ≃ 1
Tactic:
intro (_ : n * n ≃ 1)
State after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
x✝ : n * n ≃ 1
⊢ n ≃ 1

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
x✝ : n * n ≃ 1
⊢ n ≃ 1
Tactic:
have (And.intro (_ : n ≃ 1) _) := factors_eqv_1.mp ‹n * n ≃ 1›
State after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
x✝ : n * n ≃ 1
left✝ right✝ : n ≃ 1
⊢ n ≃ 1

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
x✝ : n * n ≃ 1
left✝ right✝ : n ≃ 1
⊢ n ≃ 1
Tactic:
exact ‹n ≃ 1›
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
⊢ n ≃ 1 → n * n ≃ 1
Tactic:
intro (_ : n ≃ 1)
State after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
x✝ : n ≃ 1
⊢ n * n ≃ 1

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
x✝ : n ≃ 1
⊢ n * n ≃ 1
Tactic:
have : n * n ≃ 1 := factors_eqv_1.mpr (And.intro ‹n ≃ 1› ‹n ≃ 1›)
State after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
x✝ : n ≃ 1
this : n * n ≃ 1
⊢ n * n ≃ 1

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
x✝ : n ≃ 1
this : n * n ≃ 1
⊢ n * n ≃ 1
Tactic:
exact this
State after:
no goals