Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.shift_mk_iff (IMOSLLean4/IMO2012/A5/A5Cases/Case2.lean)

State before:
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R → S
⊢ ShiftGood23 (f + 1) ↔ GoodCase2 f ∧ f 2 = 3
Tactic:
rw [mk_iff, add_sub_cancel_right, ← three_add_one_eq_four]
State after:
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R → S
⊢ GoodCase2 f ∧ (f + 1) 2 = 3 + 1 ↔ GoodCase2 f ∧ f 2 = 3

State before:
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R → S
⊢ GoodCase2 f ∧ (f + 1) 2 = 3 + 1 ↔ GoodCase2 f ∧ f 2 = 3
Tactic:
exact and_congr_right' (add_left_inj _)
State after:
no goals