Theorem: IMOSL.IMO2021A3.lowerBoundMk_perm_iota (IMOSLLean4/IMO2021/A3/A3.lean)

State before:
b : Bool
n k : ℕ
h : lowerBoundMk (k + 1) ~ iota (k + 1)
⊢ lowerBoundMk (Nat.bit false (k + 1)) ~ iota (Nat.bit false (k + 1))
Tactic:
rw [lowerBoundMk_bit0_succ, Nat.bit_false, Nat.bit0_val]
State after:
b : Bool
n k : ℕ
h : lowerBoundMk (k + 1) ~ iota (k + 1)
⊢ map (k + 1).add (iota k) ++ (2 * k + 2) :: lowerBoundMk (k + 1) ~ iota (2 * (k + 1))

State before:
b : Bool
n k : ℕ
h : lowerBoundMk (k + 1) ~ iota (k + 1)
⊢ map (k + 1).add (iota k) ++ (2 * k + 2) :: lowerBoundMk (k + 1) ~ iota (2 * (k + 1))
Tactic:
refine perm_middle.trans (((h.append_left _).trans ?_).cons _)
State after:
b : Bool
n k : ℕ
h : lowerBoundMk (k + 1) ~ iota (k + 1)
⊢ map (k + 1).add (iota k) ++ iota (k + 1) ~ iota (Nat.mul 2 k + 1)

State before:
b : Bool
n k : ℕ
h : lowerBoundMk (k + 1) ~ iota (k + 1)
⊢ map (k + 1).add (iota k) ++ iota (k + 1) ~ iota (Nat.mul 2 k + 1)
Tactic:
rw [iota_map_add_append_iota_eq_iota, add_right_comm, ← two_mul]
State after:
b : Bool
n k : ℕ
h : lowerBoundMk (k + 1) ~ iota (k + 1)
⊢ iota (2 * k + 1) ~ iota (Nat.mul 2 k + 1)

State before:
b : Bool
n k : ℕ
h : lowerBoundMk (k + 1) ~ iota (k + 1)
⊢ iota (2 * k + 1) ~ iota (Nat.mul 2 k + 1)
Tactic:
exact Perm.refl _
State after:
no goals

State before:
b : Bool
n✝ n : ℕ
h : lowerBoundMk n ~ iota n
⊢ lowerBoundMk (Nat.bit true n) ~ iota (Nat.bit true n)
Tactic:
rw [lowerBoundMk_bit1, Nat.bit_true, Nat.bit1_val]
State after:
b : Bool
n✝ n : ℕ
h : lowerBoundMk n ~ iota n
⊢ map n.add (iota n) ++ (2 * n + 1) :: lowerBoundMk n ~ iota (2 * n + 1)

State before:
b : Bool
n✝ n : ℕ
h : lowerBoundMk n ~ iota n
⊢ map n.add (iota n) ++ (2 * n + 1) :: lowerBoundMk n ~ iota (2 * n + 1)
Tactic:
refine perm_middle.trans (((h.append_left _).trans ?_).cons _)
State after:
b : Bool
n✝ n : ℕ
h : lowerBoundMk n ~ iota n
⊢ map n.add (iota n) ++ iota n ~ iota (2 * n)

State before:
b : Bool
n✝ n : ℕ
h : lowerBoundMk n ~ iota n
⊢ map n.add (iota n) ++ iota n ~ iota (2 * n)
Tactic:
rw [iota_map_add_append_iota_eq_iota, ← two_mul]
State after:
no goals