Theorem: fst_le_max (UnitConjecture/FreeModule.lean)

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

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

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

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

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

State before:
R : Type ?u.124898
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.124913
inst✝ : DecidableEq X
a b : ℕ
c : a ≤ b
⊢ a ≤ b
Tactic:
assumption
State after:
no goals

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

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

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

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