Theorem: eq_fst_or_snd_of_max (UnitConjecture/FreeModule.lean)

State before:
R : Type ?u.126771
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type ?u.126786
inst✝ : DecidableEq X
a b : ℕ
⊢ max a b = a ∨ max a b = 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]
State after:
no goals

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

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

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

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

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

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

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

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