-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem mod_lt (x : Nat) {y : Nat} : y > 0 → x % y < y

Proof state:
case ind
x y : Nat
h : 0 < y ∧ y ≤ x
h₂ : y > 0 → (x - y) % y < y
h₃ : y > 0
left✝ : 0 < y
h₁ : y ≤ x
⊢ x % y < y

Tactic:
rw [mod_eq_sub_mod h₁]

Result:
case ind
x y : Nat
h : 0 < y ∧ y ≤ x
h₂ : y > 0 → (x - y) % y < y
h₃ : y > 0
left✝ : 0 < y
h₁ : y ≤ x
⊢ (x - y) % y < y

Proof state:
x y : Nat
h₁✝¹ : ¬(0 < y ∧ y ≤ x)
h₂ : y > 0
h₁✝ : ¬0 < y ∨ ¬y ≤ x
h₁ : ¬0 < y
⊢ x % y < y

Tactic:
exact absurd h₂ h₁

Result:
no goals

Proof state:
case base
x y : Nat
h₁ : ¬(0 < y ∧ y ≤ x)
h₂ : y > 0
⊢ x % y < y

Tactic:
have h₁ : ¬ 0 < y ∨ ¬ y ≤ x := Decidable.not_and_iff_or_not.mp h₁

Result:
case base
x y : Nat
h₁✝ : ¬(0 < y ∧ y ≤ x)
h₂ : y > 0
h₁ : ¬0 < y ∨ ¬y ≤ x
⊢ x % y < y

Proof state:
case ind
x y : Nat
h : 0 < y ∧ y ≤ x
h₂ : y > 0 → (x - y) % y < y
h₃ : y > 0
left✝ : 0 < y
h₁ : y ≤ x
⊢ (x - y) % y < y

Tactic:
exact h₂ h₃

Result:
no goals

Proof state:
x y : Nat
h₁✝¹ : ¬(0 < y ∧ y ≤ x)
h₂ : y > 0
h₁✝ : ¬0 < y ∨ ¬y ≤ x
h₁ : ¬y ≤ x
hgt : y > x % y
heq : x % y = x
⊢ x % y < y

Tactic:
exact hgt

Result:
no goals

Proof state:
x y : Nat
h₁✝¹ : ¬(0 < y ∧ y ≤ x)
h₂ : y > 0
h₁✝ : ¬0 < y ∨ ¬y ≤ x
h₁ : ¬y ≤ x
hgt : y > x
⊢ x % y < y

Tactic:
have heq : x % y = x := mod_eq_of_lt hgt

Result:
x y : Nat
h₁✝¹ : ¬(0 < y ∧ y ≤ x)
h₂ : y > 0
h₁✝ : ¬0 < y ∨ ¬y ≤ x
h₁ : ¬y ≤ x
hgt : y > x
heq : x % y = x
⊢ x % y < y

Proof state:
case ind
x y : Nat
h : 0 < y ∧ y ≤ x
h₂ : y > 0 → (x - y) % y < y
⊢ y > 0 → x % y < y

Tactic:
intro h₃

Result:
case ind
x y : Nat
h : 0 < y ∧ y ≤ x
h₂ : y > 0 → (x - y) % y < y
h₃ : y > 0
⊢ x % y < y

Proof state:
case ind
x y : Nat
h : 0 < y ∧ y ≤ x
h₂ : y > 0 → (x - y) % y < y
h₃ : y > 0
⊢ x % y < y

Tactic:
have ⟨_, h₁⟩ := h

Result:
case ind
x y : Nat
h : 0 < y ∧ y ≤ x
h₂ : y > 0 → (x - y) % y < y
h₃ : y > 0
left✝ : 0 < y
h₁ : y ≤ x
⊢ x % y < y

Proof state:
x y : Nat
⊢ y > 0 → x % y < y

Tactic:
induction x, y using mod.inductionOn with
| base x y h₁ =>
  intro h₂
  have h₁ : ¬ 0 < y ∨ ¬ y ≤ x := Decidable.not_and_iff_or_not.mp h₁
  match h₁ with
  | Or.inl h₁ => exact absurd h₂ h₁
  | Or.inr h₁ =>
    have hgt : y > x := gt_of_not_le h₁
    have heq : x % y = x := mod_eq_of_lt hgt
    rw [← heq] at hgt
    exact hgt
| ind x y h h₂ =>
  intro h₃
  have ⟨_, h₁⟩ := h
  rw [mod_eq_sub_mod h₁]
  exact h₂ h₃

Result:
no goals

Proof state:
case base
x y : Nat
h₁✝ : ¬(0 < y ∧ y ≤ x)
h₂ : y > 0
h₁ : ¬0 < y ∨ ¬y ≤ x
⊢ x % y < y

Tactic:
match h₁ with
| Or.inl h₁ => exact absurd h₂ h₁
| Or.inr h₁ =>
  have hgt : y > x := gt_of_not_le h₁
  have heq : x % y = x := mod_eq_of_lt hgt
  rw [← heq] at hgt
  exact hgt

Result:
no goals

Proof state:
x y : Nat
h₁✝¹ : ¬(0 < y ∧ y ≤ x)
h₂ : y > 0
h₁✝ : ¬0 < y ∨ ¬y ≤ x
h₁ : ¬y ≤ x
⊢ x % y < y

Tactic:
have hgt : y > x := gt_of_not_le h₁

Result:
x y : Nat
h₁✝¹ : ¬(0 < y ∧ y ≤ x)
h₂ : y > 0
h₁✝ : ¬0 < y ∨ ¬y ≤ x
h₁ : ¬y ≤ x
hgt : y > x
⊢ x % y < y

Proof state:
case base
x y : Nat
h₁ : ¬(0 < y ∧ y ≤ x)
⊢ y > 0 → x % y < y

Tactic:
intro h₂

Result:
case base
x y : Nat
h₁ : ¬(0 < y ∧ y ≤ x)
h₂ : y > 0
⊢ x % y < y

Proof state:
x y : Nat
h₁✝¹ : ¬(0 < y ∧ y ≤ x)
h₂ : y > 0
h₁✝ : ¬0 < y ∨ ¬y ≤ x
h₁ : ¬y ≤ x
hgt : y > x
heq : x % y = x
⊢ x % y < y

Tactic:
rw [← heq] at hgt

Result:
x y : Nat
h₁✝¹ : ¬(0 < y ∧ y ≤ x)
h₂ : y > 0
h₁✝ : ¬0 < y ∨ ¬y ≤ x
h₁ : ¬y ≤ x
hgt : y > x % y
heq : x % y = x
⊢ x % y < y