Theorem: add_le_of_dvd_of_dvd_of_lt (Fl/Lemmas.lean)

State before:
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ m + k ≤ n
Tactic:
apply Nat.le_of_lt_add_of_dvd
State after:
case h
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ m + k < n + ?n

case a
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ ?n ∣ m + k

case a
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ ?n ∣ n

case n
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ ℕ

State before:
case h
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ m + k < n + ?n

case a
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ ?n ∣ m + k

case a
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ ?n ∣ n

case n
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ ℕ
Tactic:
. exact Nat.add_lt_add_right h₃ k
State after:
case a
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ k ∣ m + k

case a
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ k ∣ n

State before:
case a
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ k ∣ m + k

case a
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ k ∣ n
Tactic:
. exact Nat.dvd_add h₂ (Nat.dvd_refl _)
State after:
case a
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ k ∣ n

State before:
case a
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ k ∣ n
Tactic:
. exact h₁
State after:
no goals

State before:
case h
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ m + k < n + ?n
Tactic:
exact Nat.add_lt_add_right h₃ k
State after:
no goals

State before:
case a
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ k ∣ m + k
Tactic:
exact Nat.dvd_add h₂ (Nat.dvd_refl _)
State after:
no goals

State before:
case a
n m k : ℕ
h₁ : k ∣ n
h₂ : k ∣ m
h₃ : m < n
⊢ k ∣ n
Tactic:
exact h₁
State after:
no goals