α : Type ?u.26
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
a : ℚ
⊢ (if a.den = 1 then a.num else a.num / ↑a.den) = a.num / ↑a.den
α : Type ?u.26
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
a : ℚ
⊢ Rat.floor a = a.num / ↑a.den
rw [Rat.floor]
case inl
α : Type ?u.26
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
a : ℚ
h✝ : a.den = 1
⊢ a.num = a.num / ↑a.den

case inr
α : Type ?u.26
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
a : ℚ
h✝ : ¬a.den = 1
⊢ a.num / ↑a.den = a.num / ↑a.den
α : Type ?u.26
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
a : ℚ
⊢ (if a.den = 1 then a.num else a.num / ↑a.den) = a.num / ↑a.den
split
case inr
α : Type ?u.26
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
a : ℚ
h✝ : ¬a.den = 1
⊢ a.num / ↑a.den = a.num / ↑a.den
case inl
α : Type ?u.26
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
a : ℚ
h✝ : a.den = 1
⊢ a.num = a.num / ↑a.den

case inr
α : Type ?u.26
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
a : ℚ
h✝ : ¬a.den = 1
⊢ a.num / ↑a.den = a.num / ↑a.den
. next h => simp [h]
no goals
case inr
α : Type ?u.26
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
a : ℚ
h✝ : ¬a.den = 1
⊢ a.num / ↑a.den = a.num / ↑a.den
. next => rfl
no goals
case inl
α : Type ?u.26
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
a : ℚ
h✝ : a.den = 1
⊢ a.num = a.num / ↑a.den
next h => simp [h]
no goals
α : Type ?u.26
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
a : ℚ
h : a.den = 1
⊢ a.num = a.num / ↑a.den
simp [h]
no goals
case inr
α : Type ?u.26
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
a : ℚ
h✝ : ¬a.den = 1
⊢ a.num / ↑a.den = a.num / ↑a.den
next => rfl
no goals
α : Type ?u.26
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
a : ℚ
h✝ : ¬a.den = 1
⊢ a.num / ↑a.den = a.num / ↑a.den
rfl