Theorem: Lean4Axiomatic.Natural.positive_subst (Lean4Axiomatic/Natural/Sign.lean)

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n₁ n₂ : ℕ
⊢ n₁ ≃ n₂ → Positive n₁ → Positive n₂
Tactic:
intro (_ : n₁ ≃ n₂) (_ : Positive n₁)
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n₁ n₂ : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : Positive n₁
⊢ Positive n₂

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n₁ n₂ : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : Positive n₁
⊢ Positive n₂
Tactic:
have : n₁ ≄ 0 := Signed.positive_defn.mp ‹Positive n₁›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n₁ n₂ : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : Positive n₁
this : n₁ ≄ 0
⊢ Positive n₂

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n₁ n₂ : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : Positive n₁
this : n₁ ≄ 0
⊢ Positive n₂
Tactic:
have : n₂ ≄ 0 := AA.neqv_substL ‹n₁ ≃ n₂› ‹n₁ ≄ 0›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n₁ n₂ : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : Positive n₁
this✝ : n₁ ≄ 0
this : n₂ ≄ 0
⊢ Positive n₂

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n₁ n₂ : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : Positive n₁
this✝ : n₁ ≄ 0
this : n₂ ≄ 0
⊢ Positive n₂
Tactic:
have : Positive n₂ := Signed.positive_defn.mpr ‹n₂ ≄ 0›
State after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n₁ n₂ : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : Positive n₁
this✝¹ : n₁ ≄ 0
this✝ : n₂ ≄ 0
this : Positive n₂
⊢ Positive n₂

State before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n₁ n₂ : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : Positive n₁
this✝¹ : n₁ ≄ 0
this✝ : n₂ ≄ 0
this : Positive n₂
⊢ Positive n₂
Tactic:
exact this
State after:
no goals