Theorem: Nat.Arith₁.if_pos (Logic/Vorspiel/Arith.lean)

State before:
n : ℕ
f g h : Vector ℕ n → ℕ
hf : Arith₁ f
hg : Arith₁ g
hh : Arith₁ h
⊢ Arith₁ fun v => if 0 < f v then g v else h v
Tactic:
have : Arith₁ (fun v => (f v).pos * (g v) + (f v).inv * (h v)) :=
  (add 0 1).comp₂ _
    ((mul 0 1).comp₂ _ ((pos 0).comp₁ _ hf) hg)
    ((mul 0 1).comp₂ _ ((inv 0).comp₁ _ hf) hh)
State after:
n : ℕ
f g h : Vector ℕ n → ℕ
hf : Arith₁ f
hg : Arith₁ g
hh : Arith₁ h
this : Arith₁ fun v => (f v).pos * g v + (f v).inv * h v
⊢ Arith₁ fun v => if 0 < f v then g v else h v

State before:
n : ℕ
f g h : Vector ℕ n → ℕ
hf : Arith₁ f
hg : Arith₁ g
hh : Arith₁ h
this : Arith₁ fun v => (f v).pos * g v + (f v).inv * h v
⊢ Arith₁ fun v => if 0 < f v then g v else h v
Tactic:
exact this.of_eq <| by
  intro i; by_cases hf : f i = 0 <;> simp[hf, zero_lt_iff]
State after:
no goals

State before:
n : ℕ
f g h : Vector ℕ n → ℕ
hf : Arith₁ f
hg : Arith₁ g
hh : Arith₁ h
this : Arith₁ fun v => (f v).pos * g v + (f v).inv * h v
⊢ ∀ (i : Vector ℕ n), (f i).pos * g i + (f i).inv * h i = if 0 < f i then g i else h i
Tactic:
intro i
State after:
n : ℕ
f g h : Vector ℕ n → ℕ
hf : Arith₁ f
hg : Arith₁ g
hh : Arith₁ h
this : Arith₁ fun v => (f v).pos * g v + (f v).inv * h v
i : Vector ℕ n
⊢ (f i).pos * g i + (f i).inv * h i = if 0 < f i then g i else h i

State before:
n : ℕ
f g h : Vector ℕ n → ℕ
hf : Arith₁ f
hg : Arith₁ g
hh : Arith₁ h
this : Arith₁ fun v => (f v).pos * g v + (f v).inv * h v
i : Vector ℕ n
⊢ (f i).pos * g i + (f i).inv * h i = if 0 < f i then g i else h i
Tactic:
by_cases hf : f i = 0 <;> simp[hf, zero_lt_iff]
State after:
no goals