Theorem: snd_le_max (UnitConjecture/FreeModule.lean)

State before:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
⊢ b ≤ max a b
Tactic:
exact if c: a ≤ b
then by
  unfold max
  unfold Nat.instMaxNat
  unfold maxOfLe 
  simp [if_pos c]
else by 
  unfold max
  unfold Nat.instMaxNat
  unfold maxOfLe
  simp [if_neg c]
  apply Nat.le_of_lt
  let c' := Nat.gt_of_not_le c
  assumption
State after:
no goals

State before:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ b ≤ max a b
Tactic:
unfold max
State after:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ b ≤ Nat.instMaxNat.1 a b

State before:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ b ≤ Nat.instMaxNat.1 a b
Tactic:
unfold Nat.instMaxNat
State after:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ b ≤ maxOfLe.1 a b

State before:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ b ≤ maxOfLe.1 a b
Tactic:
unfold maxOfLe
State after:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ b ≤ { max := fun x y => if x ≤ y then y else x }.1 a b

State before:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ b ≤ { max := fun x y => if x ≤ y then y else x }.1 a b
Tactic:
simp [if_pos c]
State after:
no goals

State before:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ b ≤ max a b
Tactic:
unfold max
State after:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ b ≤ Nat.instMaxNat.1 a b

State before:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ b ≤ Nat.instMaxNat.1 a b
Tactic:
unfold Nat.instMaxNat
State after:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ b ≤ maxOfLe.1 a b

State before:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ b ≤ maxOfLe.1 a b
Tactic:
unfold maxOfLe
State after:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ b ≤ { max := fun x y => if x ≤ y then y else x }.1 a b

State before:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ b ≤ { max := fun x y => if x ≤ y then y else x }.1 a b
Tactic:
simp [if_neg c]
State after:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ b ≤ a

State before:
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ b ≤ a
Tactic:
apply Nat.le_of_lt
State after:
case h
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ b < a

State before:
case h
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
⊢ b < a
Tactic:
let c' := Nat.gt_of_not_le c
State after:
case h
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
c' : a > b := Nat.gt_of_not_le c
⊢ b < a

State before:
case h
R : Type ?u.125823
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.125838
inst✝ : DecidableEq X
a b : ℕ
c : ¬a ≤ b
c' : a > b := Nat.gt_of_not_le c
⊢ b < a
Tactic:
assumption
State after:
no goals