Theorem: IMOSL.IMO2013N2.good_two_mul_add_one (IMOSLLean4/IMO2013/N2/N2.lean)

State before:
k c : ℕ
h : good k c
⊢ good (k + 1) (2 * c + 1)
Tactic:
intro n h0
State after:
k c : ℕ
h : good k c
n : ℕ
h0 : 0 < n
⊢ ∃ S, card S = k + 1 ∧ (∀ m ∈ S, 0 < m) ∧ ↑(n + (2 * c + 1)) / ↑n = (map (fun m => ↑(m + 1) / ↑m) S).prod

State before:
k c : ℕ
h : good k c
n : ℕ
h0 : 0 < n
⊢ ∃ S, card S = k + 1 ∧ (∀ m ∈ S, 0 < m) ∧ ↑(n + (2 * c + 1)) / ↑n = (map (fun m => ↑(m + 1) / ↑m) S).prod
Tactic:
rcases n.even_or_odd' with ⟨t, rfl | rfl⟩
State after:
case intro.inl
k c : ℕ
h : good k c
t : ℕ
h0 : 0 < 2 * t
⊢ ∃ S, card S = k + 1 ∧ (∀ m ∈ S, 0 < m) ∧ ↑(2 * t + (2 * c + 1)) / ↑(2 * t) = (map (fun m => ↑(m + 1) / ↑m) S).prod

case intro.inr
k c : ℕ
h : good k c
t : ℕ
h0 : 0 < 2 * t + 1
⊢ ∃ S,
    card S = k + 1 ∧
      (∀ m ∈ S, 0 < m) ∧ ↑(2 * t + 1 + (2 * c + 1)) / ↑(2 * t + 1) = (map (fun m => ↑(m + 1) / ↑m) S).prod

State before:
case intro.inl
k c : ℕ
h : good k c
t : ℕ
h0 : 0 < 2 * t
⊢ ∃ S, card S = k + 1 ∧ (∀ m ∈ S, 0 < m) ∧ ↑(2 * t + (2 * c + 1)) / ↑(2 * t) = (map (fun m => ↑(m + 1) / ↑m) S).prod
Tactic:
replace h0 := pos_of_mul_pos_right h0 (Nat.zero_le 2)
State after:
case intro.inl
k c : ℕ
h : good k c
t : ℕ
h0 : 0 < t
⊢ ∃ S, card S = k + 1 ∧ (∀ m ∈ S, 0 < m) ∧ ↑(2 * t + (2 * c + 1)) / ↑(2 * t) = (map (fun m => ↑(m + 1) / ↑m) S).prod

State before:
case intro.inl
k c : ℕ
h : good k c
t : ℕ
h0 : 0 < t
⊢ ∃ S, card S = k + 1 ∧ (∀ m ∈ S, 0 < m) ∧ ↑(2 * t + (2 * c + 1)) / ↑(2 * t) = (map (fun m => ↑(m + 1) / ↑m) S).prod
Tactic:
rcases h t h0 with ⟨T, rfl, h1, h2⟩
State after:
case intro.inl.intro.intro.intro
c t : ℕ
h0 : 0 < t
T : Multiset ℕ
h : good (card T) c
h1 : ∀ m ∈ T, 0 < m
h2 : ↑(t + c) / ↑t = (map (fun m => ↑(m + 1) / ↑m) T).prod
⊢ ∃ S,
    card S = card T + 1 ∧ (∀ m ∈ S, 0 < m) ∧ ↑(2 * t + (2 * c + 1)) / ↑(2 * t) = (map (fun m => ↑(m + 1) / ↑m) S).prod

State before:
case intro.inl.intro.intro.intro
c t : ℕ
h0 : 0 < t
T : Multiset ℕ
h : good (card T) c
h1 : ∀ m ∈ T, 0 < m
h2 : ↑(t + c) / ↑t = (map (fun m => ↑(m + 1) / ↑m) T).prod
⊢ ∃ S,
    card S = card T + 1 ∧ (∀ m ∈ S, 0 < m) ∧ ↑(2 * t + (2 * c + 1)) / ↑(2 * t) = (map (fun m => ↑(m + 1) / ↑m) S).prod
Tactic:
have X := t.add_pos_left h0 c
State after:
case intro.inl.intro.intro.intro
c t : ℕ
h0 : 0 < t
T : Multiset ℕ
h : good (card T) c
h1 : ∀ m ∈ T, 0 < m
h2 : ↑(t + c) / ↑t = (map (fun m => ↑(m + 1) / ↑m) T).prod
X : 0 < t + c
⊢ ∃ S,
    card S = card T + 1 ∧ (∀ m ∈ S, 0 < m) ∧ ↑(2 * t + (2 * c + 1)) / ↑(2 * t) = (map (fun m => ↑(m + 1) / ↑m) S).prod

State before:
case intro.inl.intro.intro.intro
c t : ℕ
h0 : 0 < t
T : Multiset ℕ
h : good (card T) c
h1 : ∀ m ∈ T, 0 < m
h2 : ↑(t + c) / ↑t = (map (fun m => ↑(m + 1) / ↑m) T).prod
X : 0 < t + c
⊢ ∃ S,
    card S = card T + 1 ∧ (∀ m ∈ S, 0 < m) ∧ ↑(2 * t + (2 * c + 1)) / ↑(2 * t) = (map (fun m => ↑(m + 1) / ↑m) S).prod
Tactic:
refine ⟨(2 * (t + c)) ::ₘ T, card_cons _ T,
  forall_mem_cons.mpr ⟨mul_pos (Nat.succ_pos 1) X, h1⟩, ?_⟩
State after:
case intro.inl.intro.intro.intro
c t : ℕ
h0 : 0 < t
T : Multiset ℕ
h : good (card T) c
h1 : ∀ m ∈ T, 0 < m
h2 : ↑(t + c) / ↑t = (map (fun m => ↑(m + 1) / ↑m) T).prod
X : 0 < t + c
⊢ ↑(2 * t + (2 * c + 1)) / ↑(2 * t) = (map (fun m => ↑(m + 1) / ↑m) (2 * (t + c) ::ₘ T)).prod

State before:
case intro.inl.intro.intro.intro
c t : ℕ
h0 : 0 < t
T : Multiset ℕ
h : good (card T) c
h1 : ∀ m ∈ T, 0 < m
h2 : ↑(t + c) / ↑t = (map (fun m => ↑(m + 1) / ↑m) T).prod
X : 0 < t + c
⊢ ↑(2 * t + (2 * c + 1)) / ↑(2 * t) = (map (fun m => ↑(m + 1) / ↑m) (2 * (t + c) ::ₘ T)).prod
Tactic:
rw [map_cons, prod_cons, ← h2, ← add_assoc, ← mul_add,
  div_mul_div_comm, Nat.cast_mul, Nat.cast_mul, mul_right_comm]
State after:
case intro.inl.intro.intro.intro
c t : ℕ
h0 : 0 < t
T : Multiset ℕ
h : good (card T) c
h1 : ∀ m ∈ T, 0 < m
h2 : ↑(t + c) / ↑t = (map (fun m => ↑(m + 1) / ↑m) T).prod
X : 0 < t + c
⊢ ↑(2 * (t + c) + 1) / (↑2 * ↑t) = ↑(2 * (t + c) + 1) * ↑(t + c) / (↑2 * ↑t * ↑(t + c))

State before:
case intro.inl.intro.intro.intro
c t : ℕ
h0 : 0 < t
T : Multiset ℕ
h : good (card T) c
h1 : ∀ m ∈ T, 0 < m
h2 : ↑(t + c) / ↑t = (map (fun m => ↑(m + 1) / ↑m) T).prod
X : 0 < t + c
⊢ ↑(2 * (t + c) + 1) / (↑2 * ↑t) = ↑(2 * (t + c) + 1) * ↑(t + c) / (↑2 * ↑t * ↑(t + c))
Tactic:
exact (mul_div_mul_right _ _ <| Nat.cast_ne_zero.mpr X.ne.symm).symm
State after:
no goals

State before:
case intro.inr
k c : ℕ
h : good k c
t : ℕ
h0 : 0 < 2 * t + 1
⊢ ∃ S,
    card S = k + 1 ∧
      (∀ m ∈ S, 0 < m) ∧ ↑(2 * t + 1 + (2 * c + 1)) / ↑(2 * t + 1) = (map (fun m => ↑(m + 1) / ↑m) S).prod
Tactic:
have X := t.succ_pos
State after:
case intro.inr
k c : ℕ
h : good k c
t : ℕ
h0 : 0 < 2 * t + 1
X : 0 < t.succ
⊢ ∃ S,
    card S = k + 1 ∧
      (∀ m ∈ S, 0 < m) ∧ ↑(2 * t + 1 + (2 * c + 1)) / ↑(2 * t + 1) = (map (fun m => ↑(m + 1) / ↑m) S).prod

State before:
case intro.inr
k c : ℕ
h : good k c
t : ℕ
h0 : 0 < 2 * t + 1
X : 0 < t.succ
⊢ ∃ S,
    card S = k + 1 ∧
      (∀ m ∈ S, 0 < m) ∧ ↑(2 * t + 1 + (2 * c + 1)) / ↑(2 * t + 1) = (map (fun m => ↑(m + 1) / ↑m) S).prod
Tactic:
rcases h (t + 1) X with ⟨T, rfl, h1, h2⟩
State after:
case intro.inr.intro.intro.intro
c t : ℕ
h0 : 0 < 2 * t + 1
X : 0 < t.succ
T : Multiset ℕ
h : good (card T) c
h1 : ∀ m ∈ T, 0 < m
h2 : ↑(t + 1 + c) / ↑(t + 1) = (map (fun m => ↑(m + 1) / ↑m) T).prod
⊢ ∃ S,
    card S = card T + 1 ∧
      (∀ m ∈ S, 0 < m) ∧ ↑(2 * t + 1 + (2 * c + 1)) / ↑(2 * t + 1) = (map (fun m => ↑(m + 1) / ↑m) S).prod

State before:
case intro.inr.intro.intro.intro
c t : ℕ
h0 : 0 < 2 * t + 1
X : 0 < t.succ
T : Multiset ℕ
h : good (card T) c
h1 : ∀ m ∈ T, 0 < m
h2 : ↑(t + 1 + c) / ↑(t + 1) = (map (fun m => ↑(m + 1) / ↑m) T).prod
⊢ ∃ S,
    card S = card T + 1 ∧
      (∀ m ∈ S, 0 < m) ∧ ↑(2 * t + 1 + (2 * c + 1)) / ↑(2 * t + 1) = (map (fun m => ↑(m + 1) / ↑m) S).prod
Tactic:
refine ⟨(2 * t + 1) ::ₘ T, card_cons _ T,
  forall_mem_cons.mpr ⟨(2 * t).succ_pos, h1⟩, ?_⟩
State after:
case intro.inr.intro.intro.intro
c t : ℕ
h0 : 0 < 2 * t + 1
X : 0 < t.succ
T : Multiset ℕ
h : good (card T) c
h1 : ∀ m ∈ T, 0 < m
h2 : ↑(t + 1 + c) / ↑(t + 1) = (map (fun m => ↑(m + 1) / ↑m) T).prod
⊢ ↑(2 * t + 1 + (2 * c + 1)) / ↑(2 * t + 1) = (map (fun m => ↑(m + 1) / ↑m) ((2 * t + 1) ::ₘ T)).prod

State before:
case intro.inr.intro.intro.intro
c t : ℕ
h0 : 0 < 2 * t + 1
X : 0 < t.succ
T : Multiset ℕ
h : good (card T) c
h1 : ∀ m ∈ T, 0 < m
h2 : ↑(t + 1 + c) / ↑(t + 1) = (map (fun m => ↑(m + 1) / ↑m) T).prod
⊢ ↑(2 * t + 1 + (2 * c + 1)) / ↑(2 * t + 1) = (map (fun m => ↑(m + 1) / ↑m) ((2 * t + 1) ::ₘ T)).prod
Tactic:
rw [map_cons, prod_cons, ← h2, add_add_add_comm, add_right_comm,
  add_assoc (2 * t) 1, ← mul_add_one (α := ℕ), ← mul_add, div_mul_div_comm,
  Nat.cast_mul, Nat.cast_mul, mul_right_comm]
State after:
case intro.inr.intro.intro.intro
c t : ℕ
h0 : 0 < 2 * t + 1
X : 0 < t.succ
T : Multiset ℕ
h : good (card T) c
h1 : ∀ m ∈ T, 0 < m
h2 : ↑(t + 1 + c) / ↑(t + 1) = (map (fun m => ↑(m + 1) / ↑m) T).prod
⊢ ↑2 * ↑(t + 1 + c) / ↑(2 * t + 1) = ↑2 * ↑(t + 1 + c) * ↑(t + 1) / (↑(2 * t + 1) * ↑(t + 1))

State before:
case intro.inr.intro.intro.intro
c t : ℕ
h0 : 0 < 2 * t + 1
X : 0 < t.succ
T : Multiset ℕ
h : good (card T) c
h1 : ∀ m ∈ T, 0 < m
h2 : ↑(t + 1 + c) / ↑(t + 1) = (map (fun m => ↑(m + 1) / ↑m) T).prod
⊢ ↑2 * ↑(t + 1 + c) / ↑(2 * t + 1) = ↑2 * ↑(t + 1 + c) * ↑(t + 1) / (↑(2 * t + 1) * ↑(t + 1))
Tactic:
exact (mul_div_mul_right _ _ <| Nat.cast_ne_zero.mpr X.ne.symm).symm
State after:
no goals