internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.Extra.CharTwo.ofRingHom
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : CharTwo R
inst✝ : NonAssocSemiring S
φ : R →+* S
⊢ 2 = 0
Tactic:
rw [← one_add_one_eq_two, ← φ.map_one,
← φ.map_add, add_self_eq_zero, φ.map_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.Int_good_iff_MonoidGood
Proof state before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
f : ℤ → R
m n : ℤ
⊢ f (⌊m⌋ • n) = f m * ↑⌊f n⌋ ↔ f (m * n) = f m * ↑⌊f n⌋
Tactic:
rw [Int.floor_int, smul_eq_mul, id_def]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₂X.XpowMul_nat_add
Proof state before:
m n : ℕ
P : 𝔽₂X
⊢ XpowMul (m + n) P = XpowMul n (XpowMul m P)
Tactic:
unfold XpowMul
Proof state after:
m n : ℕ
P : 𝔽₂X
⊢ { toFinset := Finset.image (fun k => k + (m + n)) P.toFinset } =
    { toFinset := Finset.image (fun k => k + n) { toFinset := Finset.image (fun k => k + m) P.toFinset }.toFinset }
Theorem: IMOSL.IMO2012A5.𝔽₂X.XpowMul_nat_add
Proof state before:
m n : ℕ
P : 𝔽₂X
⊢ { toFinset := Finset.image (fun k => k + (m + n)) P.toFinset } =
    { toFinset := Finset.image (fun k => k + n) { toFinset := Finset.image (fun k => k + m) P.toFinset }.toFinset }
Tactic:
rw [𝔽₂X.ext_iff, eq_comm, Finset.image_image, comp_add_right]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₂X.XpowMul_sum
Proof state before:
ι : Type u_1
n : ℕ
inst✝ : DecidableEq ι
f : ι → 𝔽₂X
S✝ : Finset ι
i : ι
S : Finset ι
h : i ∉ S
h0 : XpowMul n (S.sum f) = ∑ i ∈ S, XpowMul n (f i)
⊢ XpowMul n ((insert i S).sum f) = ∑ i ∈ insert i S, XpowMul n (f i)
Tactic:
rw [Finset.sum_insert h, Finset.sum_insert h, XpowMul_𝔽₂X_add, h0]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₂X.sum_Xpow_eq_ofFinset
Proof state before:
i : ℕ
S : Finset ℕ
h : i ∉ S
h0 : S.sum Xpow = ofFinset S
⊢ (insert i S).sum Xpow = ofFinset (insert i S)
Tactic:
rw [Finset.sum_insert h, h0]
Proof state after:
i : ℕ
S : Finset ℕ
h : i ∉ S
h0 : S.sum Xpow = ofFinset S
⊢ Xpow i + ofFinset S = ofFinset (insert i S)
Theorem: IMOSL.IMO2012A5.𝔽₂X.sum_Xpow_eq_ofFinset
Proof state before:
i : ℕ
S : Finset ℕ
h : i ∉ S
h0 : S.sum Xpow = ofFinset S
⊢ Xpow i + ofFinset S = ofFinset (insert i S)
Tactic:
exact 𝔽₂X.ext _ _ (symmDiff_singleton_eq_insert h)
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₂X.Xpow_add
Proof state before:
k m : ℕ
⊢ Xpow (k + m) = Xpow k * Xpow m
Tactic:
rw [← XpowMul_eq_Xpow_mul, XpowMul_Xpow, add_comm]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₂X.XpowMul_eq_mul_Xpow
Proof state before:
n k : ℕ
⊢ XpowMul n (Xpow k) = Xpow k * Xpow n
Tactic:
rw [XpowMul_Xpow, Xpow_add]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₂X.XpowMul_eq_mul_Xpow
Proof state before:
n : ℕ
P✝ Q✝ : 𝔽₂X
h : XpowMul n P✝ = P✝ * Xpow n
h0 : XpowMul n Q✝ = Q✝ * Xpow n
⊢ XpowMul n (P✝ + Q✝) = (P✝ + Q✝) * Xpow n
Tactic:
rw [XpowMul_𝔽₂X_add, 𝔽₂X.add_mul, h, h0]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₂X.mul_comm
Proof state before:
P : 𝔽₂X
n : ℕ
⊢ P * Xpow n = Xpow n * P
Tactic:
rw [← XpowMul_eq_Xpow_mul, XpowMul_eq_mul_Xpow]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₂X.mul_comm
Proof state before:
P P✝ Q✝ : 𝔽₂X
h : P * P✝ = P✝ * P
h0 : P * Q✝ = Q✝ * P
⊢ P * (P✝ + Q✝) = (P✝ + Q✝) * P
Tactic:
rw [𝔽₂X.add_mul, 𝔽₂X.mul_add, h, h0]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₂X.mul_XpowMul_left
Proof state before:
n : ℕ
P : 𝔽₂X
k : ℕ
⊢ XpowMul n P * Xpow k = XpowMul n (P * Xpow k)
Tactic:
rw [← XpowMul_eq_mul_Xpow, ← XpowMul_eq_mul_Xpow,
← XpowMul_nat_add, ← XpowMul_nat_add, Nat.add_comm]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₂X.mul_XpowMul_left
Proof state before:
n : ℕ
P P✝ Q✝ : 𝔽₂X
h : XpowMul n P * P✝ = XpowMul n (P * P✝)
h0 : XpowMul n P * Q✝ = XpowMul n (P * Q✝)
⊢ XpowMul n P * (P✝ + Q✝) = XpowMul n (P * (P✝ + Q✝))
Tactic:
rw [𝔽₂X.mul_add, 𝔽₂X.mul_add, h, h0, XpowMul_𝔽₂X_add]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₂X.mul_XpowMul_right
Proof state before:
n : ℕ
P Q : 𝔽₂X
⊢ P * XpowMul n Q = XpowMul n (P * Q)
Tactic:
rw [P.mul_comm, mul_XpowMul_left, Q.mul_comm]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₂X.mul_assoc
Proof state before:
P Q : 𝔽₂X
n : ℕ
⊢ P * Q * Xpow n = P * (Q * Xpow n)
Tactic:
rw [← XpowMul_eq_mul_Xpow, ← XpowMul_eq_mul_Xpow, mul_XpowMul_right]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₂X.mul_assoc
Proof state before:
P Q P✝ Q✝ : 𝔽₂X
h : P * Q * P✝ = P * (Q * P✝)
h0 : P * Q * Q✝ = P * (Q * Q✝)
⊢ P * Q * (P✝ + Q✝) = P * (Q * (P✝ + Q✝))
Tactic:
rw [𝔽₂X.mul_add, 𝔽₂X.mul_add, 𝔽₂X.mul_add, h, h0]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₂X.square_eq_mul_self
Proof state before:
n : ℕ
P : 𝔽₂X
h : P.square = P * P
⊢ (Xpow n + P).square = (Xpow n + P) * (Xpow n + P)
Tactic:
rw [square_add, square_Xpow, 𝔽₂X.add_mul, 𝔽₂X.mul_add, ← Xpow_add, Nat.two_mul,
  𝔽₂X.mul_add, ← h, ← P.mul_comm, CharTwo.add_add_add_cancel_middle]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₂X.square_XpowMul
Proof state before:
n : ℕ
P : 𝔽₂X
⊢ (XpowMul n P).square = XpowMul (2 * n) P.square
Tactic:
unfold square XpowMul
Proof state after:
n : ℕ
P : 𝔽₂X
⊢ { toFinset := Finset.image (fun n => 2 * n) { toFinset := Finset.image (fun k => k + n) P.toFinset }.toFinset } =
    { toFinset := Finset.image (fun k => k + 2 * n) { toFinset := Finset.image (fun n => 2 * n) P.toFinset }.toFinset }
Theorem: IMOSL.IMO2012A5.𝔽₂X.square_XpowMul
Proof state before:
n : ℕ
P : 𝔽₂X
⊢ { toFinset := Finset.image (fun n => 2 * n) { toFinset := Finset.image (fun k => k + n) P.toFinset }.toFinset } =
    { toFinset := Finset.image (fun k => k + 2 * n) { toFinset := Finset.image (fun n => 2 * n) P.toFinset }.toFinset }
Tactic:
rw [Finset.image_image, Finset.image_image]
Proof state after:
n : ℕ
P : 𝔽₂X
⊢ { toFinset := Finset.image ((fun n => 2 * n) ∘ fun k => k + n) P.toFinset } =
    { toFinset := Finset.image ((fun k => k + 2 * n) ∘ fun n => 2 * n) P.toFinset }
Theorem: IMOSL.IMO2012A5.𝔽₂X.square_XpowMul
Proof state before:
n : ℕ
P : 𝔽₂X
⊢ { toFinset := Finset.image ((fun n => 2 * n) ∘ fun k => k + n) P.toFinset } =
    { toFinset := Finset.image ((fun k => k + 2 * n) ∘ fun n => 2 * n) P.toFinset }
Tactic:
exact 𝔽₂X.ext _ _ (congrArg P.toFinset.image <| funext λ n ↦ Nat.mul_add 2 _ _)
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₂X.square_mul
Proof state before:
P : 𝔽₂X
n : ℕ
⊢ (P * Xpow n).square = P.square * (Xpow n).square
Tactic:
rw [← XpowMul_eq_mul_Xpow, square_XpowMul,
square_Xpow, XpowMul_eq_mul_Xpow]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₂X.square_mul
Proof state before:
P P✝ Q✝ : 𝔽₂X
h : (P * P✝).square = P.square * P✝.square
h0 : (P * Q✝).square = P.square * Q✝.square
⊢ (P * (P✝ + Q✝)).square = P.square * (P✝ + Q✝).square
Tactic:
rw [P.mul_add, square_add, h, h0, square_add, 𝔽₂X.mul_add]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₂X.natPow_of_ne_zero
Proof state before:
n : ℕ
P : 𝔽₂X
h : n ≠ 0
⊢ P.natPow n = if n % 2 = 0 then P.square.natPow (n / 2) else P.square.natPow (n / 2) * P
Tactic:
rw [𝔽₂X.natPow, if_neg h]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₂X.natPow_two_mul
Proof state before:
P : 𝔽₂X
n : ℕ
⊢ P.natPow (2 * n) = P.square.natPow n
Tactic:
rcases Decidable.eq_or_ne n 0 with rfl | h
Proof state after:
case inl
P : 𝔽₂X
⊢ P.natPow (2 * 0) = P.square.natPow 0

case inr
P : 𝔽₂X
n : ℕ
h : n ≠ 0
⊢ P.natPow (2 * n) = P.square.natPow n
Theorem: IMOSL.IMO2012A5.𝔽₂X.natPow_two_mul
Proof state before:
case inl
P : 𝔽₂X
⊢ P.natPow (2 * 0) = P.square.natPow 0
Tactic:
rw [Nat.mul_zero, 𝔽₂X.natPow_zero, 𝔽₂X.natPow_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₂X.natPow_two_mul
Proof state before:
case inr
P : 𝔽₂X
n : ℕ
h : n ≠ 0
⊢ P.natPow (2 * n) = P.square.natPow n
Tactic:
have h0 : 0 < 2 := Nat.two_pos
Proof state after:
case inr
P : 𝔽₂X
n : ℕ
h : n ≠ 0
h0 : 0 < 2
⊢ P.natPow (2 * n) = P.square.natPow n
Theorem: IMOSL.IMO2012A5.𝔽₂X.natPow_two_mul
Proof state before:
case inr
P : 𝔽₂X
n : ℕ
h : n ≠ 0
h0 : 0 < 2
⊢ P.natPow (2 * n) = P.square.natPow n
Tactic:
rw [P.natPow_of_ne_zero (Nat.mul_ne_zero h0.ne.symm h),
  if_pos (Nat.mul_mod_right _ _), Nat.mul_div_right _ h0]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₂X.natPow_two_mul_add_one
Proof state before:
P : 𝔽₂X
n : ℕ
⊢ P.natPow (2 * n + 1) = P.square.natPow n * P
Tactic:
rw [P.natPow_of_ne_zero (2 * n).add_one_ne_zero, Nat.mul_add_mod,
  Nat.mul_add_div Nat.two_pos, if_neg Nat.one_ne_zero,
  Nat.div_eq_of_lt Nat.one_lt_two, Nat.add_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₂X.natPow_succ
Proof state before:
P : 𝔽₂X
n : ℕ
⊢ P.natPow n.succ = P.natPow n * P
Tactic:
rw [← n.div_add_mod 2]
Proof state after:
P : 𝔽₂X
n : ℕ
⊢ P.natPow (2 * (n / 2) + n % 2).succ = P.natPow (2 * (n / 2) + n % 2) * P
Theorem: IMOSL.IMO2012A5.𝔽₂X.natPow_succ
Proof state before:
P : 𝔽₂X
n : ℕ
⊢ P.natPow (2 * (n / 2) + n % 2).succ = P.natPow (2 * (n / 2) + n % 2) * P
Tactic:
rcases n.mod_two_eq_zero_or_one with h0 | h0
Proof state after:
case inl
P : 𝔽₂X
n : ℕ
h0 : n % 2 = 0
⊢ P.natPow (2 * (n / 2) + n % 2).succ = P.natPow (2 * (n / 2) + n % 2) * P

case inr
P : 𝔽₂X
n : ℕ
h0 : n % 2 = 1
⊢ P.natPow (2 * (n / 2) + n % 2).succ = P.natPow (2 * (n / 2) + n % 2) * P
Theorem: IMOSL.IMO2012A5.𝔽₂X.natPow_succ
Proof state before:
case inl
P : 𝔽₂X
n : ℕ
h0 : n % 2 = 0
⊢ P.natPow (2 * (n / 2) + n % 2).succ = P.natPow (2 * (n / 2) + n % 2) * P
Tactic:
rw [h0, Nat.add_zero, 𝔽₂X.natPow_two_mul_add_one, 𝔽₂X.natPow_two_mul]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₂X.natPow_succ
Proof state before:
case inr
P : 𝔽₂X
n : ℕ
h0 : n % 2 = 1
⊢ P.natPow (2 * (n / 2) + n % 2).succ = P.natPow (2 * (n / 2) + n % 2) * P
Tactic:
rw [h0, Nat.succ_eq_add_one, ← Nat.mul_succ 2, 𝔽₂X.natPow_two_mul,
  𝔽₂X.natPow_two_mul_add_one, 𝔽₂X.mul_assoc, ← P.square_eq_mul_self]
Proof state after:
case inr
P : 𝔽₂X
n : ℕ
h0 : n % 2 = 1
⊢ P.square.natPow (n / 2).succ = P.square.natPow (n / 2) * P.square
Theorem: IMOSL.IMO2012A5.𝔽₂X.natPow_succ
Proof state before:
case inr
P : 𝔽₂X
n : ℕ
h0 : n % 2 = 1
⊢ P.square.natPow (n / 2).succ = P.square.natPow (n / 2) * P.square
Tactic:
exact (square P).natPow_succ (n / 2)
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₂X.natPow_succ
Proof state before:
P : 𝔽₂X
n : ℕ
a✝ :
  ∀ (y : (_ : 𝔽₂X) ×' ℕ),
    (invImage (fun x => PSigma.casesOn x fun P n => n) instWellFoundedRelationOfSizeOf).1 y ⟨P, n⟩ →
      y.1.natPow y.2.succ = y.1.natPow y.2 * y.1
h0 : n % 2 = 1
⊢ (invImage (fun x => PSigma.casesOn x fun P n => n) instWellFoundedRelationOfSizeOf).1 ⟨P.square, n / 2⟩ ⟨P, n⟩
Tactic:
apply Nat.bitwise_rec_lemma
Proof state after:
case hNe
P : 𝔽₂X
n : ℕ
a✝ :
  ∀ (y : (_ : 𝔽₂X) ×' ℕ),
    (invImage (fun x => PSigma.casesOn x fun P n => n) instWellFoundedRelationOfSizeOf).1 y ⟨P, n⟩ →
      y.1.natPow y.2.succ = y.1.natPow y.2 * y.1
h0 : n % 2 = 1
⊢ n ≠ 0
Theorem: IMOSL.IMO2012A5.𝔽₂X.natPow_succ
Proof state before:
case hNe
P : 𝔽₂X
n : ℕ
a✝ :
  ∀ (y : (_ : 𝔽₂X) ×' ℕ),
    (invImage (fun x => PSigma.casesOn x fun P n => n) instWellFoundedRelationOfSizeOf).1 y ⟨P, n⟩ →
      y.1.natPow y.2.succ = y.1.natPow y.2 * y.1
h0 : n % 2 = 1
⊢ n ≠ 0
Tactic:
rintro rfl
Proof state after:
case hNe
P : 𝔽₂X
a✝ :
  ∀ (y : (_ : 𝔽₂X) ×' ℕ),
    (invImage (fun x => PSigma.casesOn x fun P n => n) instWellFoundedRelationOfSizeOf).1 y ⟨P, 0⟩ →
      y.1.natPow y.2.succ = y.1.natPow y.2 * y.1
h0 : 0 % 2 = 1
⊢ False
Theorem: IMOSL.IMO2012A5.𝔽₂X.natPow_succ
Proof state before:
case hNe
P : 𝔽₂X
a✝ :
  ∀ (y : (_ : 𝔽₂X) ×' ℕ),
    (invImage (fun x => PSigma.casesOn x fun P n => n) instWellFoundedRelationOfSizeOf).1 y ⟨P, 0⟩ →
      y.1.natPow y.2.succ = y.1.natPow y.2 * y.1
h0 : 0 % 2 = 1
⊢ False
Tactic:
exact absurd h0.symm Nat.one_ne_zero
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.zero_is_good
Proof state before:
R : Type u_1
S : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
x✝¹ x✝ : R
⊢ (fun x => 0) (x✝¹ * x✝ + 1) = (fun x => 0) x✝¹ * (fun x => 0) x✝ + (fun x => 0) (x✝¹ + x✝)
Tactic:
rw [add_zero, zero_mul]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.good_Nontrivial_or_eq_zero
Proof state before:
R : Type u_2
S : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : NonAssocSemiring S
inst✝¹ : IsCancelAdd S
inst✝ : NoZeroDivisors S
f : R → S
h : good f
⊢ 0 + f (1 + 1) = f 1 * f 1 + f (1 + 1)
Tactic:
rw [zero_add, ← h, one_mul]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.good_Nontrivial_or_eq_zero
Proof state before:
R : Type u_2
S : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : NonAssocSemiring S
inst✝¹ : IsCancelAdd S
inst✝ : NoZeroDivisors S
f : R → S
h : good f
h0 : f 1 = 0
x : R
⊢ 0 = f x * (f 0 + 1)
Tactic:
have h1 := h x 0
Proof state after:
R : Type u_2
S : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : NonAssocSemiring S
inst✝¹ : IsCancelAdd S
inst✝ : NoZeroDivisors S
f : R → S
h : good f
h0 : f 1 = 0
x : R
h1 : f (x * 0 + 1) = f x * f 0 + f (x + 0)
⊢ 0 = f x * (f 0 + 1)
Theorem: IMOSL.IMO2012A5.good_Nontrivial_or_eq_zero
Proof state before:
R : Type u_2
S : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : NonAssocSemiring S
inst✝¹ : IsCancelAdd S
inst✝ : NoZeroDivisors S
f : R → S
h : good f
h0 : f 1 = 0
x : R
h1 : f (x * 0 + 1) = f x * f 0 + f (x + 0)
⊢ 0 = f x * (f 0 + 1)
Tactic:
rwa [mul_zero, zero_add, h0, add_zero, ← mul_add_one (f x)] at h1
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.good_Nontrivial_or_eq_zero
Proof state before:
R : Type u_2
S : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : NonAssocSemiring S
inst✝¹ : IsCancelAdd S
inst✝ : NoZeroDivisors S
f : R → S
h : good f
h0 : f 1 = 0
h1 : ∀ (x : R), 0 = f x * (f 0 + 1)
h2 : f 0 = 0
x : R
⊢ f x = 0
Tactic:
specialize h1 x
Proof state after:
R : Type u_2
S : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : NonAssocSemiring S
inst✝¹ : IsCancelAdd S
inst✝ : NoZeroDivisors S
f : R → S
h : good f
h0 : f 1 = 0
h2 : f 0 = 0
x : R
h1 : 0 = f x * (f 0 + 1)
⊢ f x = 0
Theorem: IMOSL.IMO2012A5.good_Nontrivial_or_eq_zero
Proof state before:
R : Type u_2
S : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : NonAssocSemiring S
inst✝¹ : IsCancelAdd S
inst✝ : NoZeroDivisors S
f : R → S
h : good f
h0 : f 1 = 0
h2 : f 0 = 0
x : R
h1 : 0 = f x * (f 0 + 1)
⊢ f x = 0
Tactic:
rwa [h2, zero_add, mul_one, eq_comm] at h1
Proof state after:
no goals
Theorem: IMOSL.IMO2015A2.final_solution
Proof state before:
f : ℤ → ℤ
⊢ (∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1) ↔ (f = fun x => -1) ∨ f = fun x => x + 1
Tactic:
refine Iff.symm ⟨λ h x y ↦ ?_, λ h ↦ ?_⟩
Proof state after:
case refine_1
f : ℤ → ℤ
h : (f = fun x => -1) ∨ f = fun x => x + 1
x y : ℤ
⊢ f (x - f y) = f (f x) - f y - 1

case refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
⊢ (f = fun x => -1) ∨ f = fun x => x + 1
Theorem: IMOSL.IMO2015A2.final_solution
Proof state before:
case refine_1
f : ℤ → ℤ
h : (f = fun x => -1) ∨ f = fun x => x + 1
x y : ℤ
⊢ f (x - f y) = f (f x) - f y - 1
Tactic:
rcases h with rfl | rfl
Proof state after:
case refine_1.inl
x y : ℤ
⊢ (fun x => -1) (x - (fun x => -1) y) = (fun x => -1) ((fun x => -1) x) - (fun x => -1) y - 1

case refine_1.inr
x y : ℤ
⊢ (fun x => x + 1) (x - (fun x => x + 1) y) = (fun x => x + 1) ((fun x => x + 1) x) - (fun x => x + 1) y - 1
Theorem: IMOSL.IMO2015A2.final_solution
Proof state before:
case refine_1.inl
x y : ℤ
⊢ (fun x => -1) (x - (fun x => -1) y) = (fun x => -1) ((fun x => -1) x) - (fun x => -1) y - 1
Tactic:
rw [sub_sub, neg_add_self, sub_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2015A2.final_solution
Proof state before:
case refine_1.inr
x y : ℤ
⊢ (fun x => x + 1) (x - (fun x => x + 1) y) = (fun x => x + 1) ((fun x => x + 1) x) - (fun x => x + 1) y - 1
Tactic:
rw [sub_sub, add_sub_add_right_eq_sub, add_sub_right_comm]
Proof state after:
no goals
Theorem: IMOSL.IMO2015A2.final_solution
Proof state before:
case refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
⊢ (f = fun x => -1) ∨ f = fun x => x + 1
Tactic:
have h0 := h 0 (f 0)
Proof state after:
case refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : f (0 - f (f 0)) = f (f 0) - f (f 0) - 1
⊢ (f = fun x => -1) ∨ f = fun x => x + 1
Theorem: IMOSL.IMO2015A2.final_solution
Proof state before:
case refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : f (0 - f (f 0)) = f (f 0) - f (f 0) - 1
⊢ (f = fun x => -1) ∨ f = fun x => x + 1
Tactic:
rw [sub_self, zero_sub 1] at h0
Proof state after:
case refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : f (0 - f (f 0)) = -1
⊢ (f = fun x => -1) ∨ f = fun x => x + 1
Theorem: IMOSL.IMO2015A2.final_solution
Proof state before:
case refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : f (0 - f (f 0)) = -1
⊢ (f = fun x => -1) ∨ f = fun x => x + 1
Tactic:
replace h0 x : f (x + 1) = f (f x) := by
  have h1 := h x (0 - f (f 0))
  rwa [h0, sub_neg_eq_add (f (f x)), add_sub_cancel_right] at h1
Proof state after:
case refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
⊢ (f = fun x => -1) ∨ f = fun x => x + 1
Theorem: IMOSL.IMO2015A2.final_solution
Proof state before:
case refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
⊢ (f = fun x => -1) ∨ f = fun x => x + 1
Tactic:
have h1 : ∀ n, f n = (f (-1) + 1) * n + f 0 := by
  refine Extra.IntIntLinearSolverAlt λ n ↦ ?_
  have h1 := h0 (n - f n - 1)
  rw [sub_add_cancel, sub_right_comm, h, ← h0, h (n - 1), ← h0,
    sub_add_cancel, sub_self, zero_sub, sub_eq_iff_eq_add] at h1
  exact eq_add_of_sub_eq h1
Proof state after:
case refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
h1 : ∀ (n : ℤ), f n = (f (-1) + 1) * n + f 0
⊢ (f = fun x => -1) ∨ f = fun x => x + 1
Theorem: IMOSL.IMO2015A2.final_solution
Proof state before:
case refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
h1 : ∀ (n : ℤ), f n = (f (-1) + 1) * n + f 0
⊢ (f = fun x => -1) ∨ f = fun x => x + 1
Tactic:
refine (eq_or_ne (f (-1) + 1) 0).imp
  (λ h2 ↦ funext λ x ↦ ?_) (λ h2 ↦ funext λ x ↦ ?_)
Proof state after:
case refine_2.refine_1
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
h1 : ∀ (n : ℤ), f n = (f (-1) + 1) * n + f 0
h2 : f (-1) + 1 = 0
x : ℤ
⊢ f x = -1

case refine_2.refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
h1 : ∀ (n : ℤ), f n = (f (-1) + 1) * n + f 0
h2 : f (-1) + 1 ≠ 0
x : ℤ
⊢ f x = x + 1
Theorem: IMOSL.IMO2015A2.final_solution
Proof state before:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : f (0 - f (f 0)) = -1
x : ℤ
⊢ f (x + 1) = f (f x)
Tactic:
have h1 := h x (0 - f (f 0))
Proof state after:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : f (0 - f (f 0)) = -1
x : ℤ
h1 : f (x - f (0 - f (f 0))) = f (f x) - f (0 - f (f 0)) - 1
⊢ f (x + 1) = f (f x)
Theorem: IMOSL.IMO2015A2.final_solution
Proof state before:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : f (0 - f (f 0)) = -1
x : ℤ
h1 : f (x - f (0 - f (f 0))) = f (f x) - f (0 - f (f 0)) - 1
⊢ f (x + 1) = f (f x)
Tactic:
rwa [h0, sub_neg_eq_add (f (f x)), add_sub_cancel_right] at h1
Proof state after:
no goals
Theorem: IMOSL.IMO2015A2.final_solution
Proof state before:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
⊢ ∀ (n : ℤ), f n = (f (-1) + 1) * n + f 0
Tactic:
refine Extra.IntIntLinearSolverAlt λ n ↦ ?_
Proof state after:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
n : ℤ
⊢ f (n + 1) = f (-1) + 1 + f n
Theorem: IMOSL.IMO2015A2.final_solution
Proof state before:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
n : ℤ
⊢ f (n + 1) = f (-1) + 1 + f n
Tactic:
have h1 := h0 (n - f n - 1)
Proof state after:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
n : ℤ
h1 : f (n - f n - 1 + 1) = f (f (n - f n - 1))
⊢ f (n + 1) = f (-1) + 1 + f n
Theorem: IMOSL.IMO2015A2.final_solution
Proof state before:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
n : ℤ
h1 : f (n - f n - 1 + 1) = f (f (n - f n - 1))
⊢ f (n + 1) = f (-1) + 1 + f n
Tactic:
rw [sub_add_cancel, sub_right_comm, h, ← h0, h (n - 1), ← h0,
  sub_add_cancel, sub_self, zero_sub, sub_eq_iff_eq_add] at h1
Proof state after:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
n : ℤ
h1 : f (n + 1) - f n = f (-1) + 1
⊢ f (n + 1) = f (-1) + 1 + f n
Theorem: IMOSL.IMO2015A2.final_solution
Proof state before:
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
n : ℤ
h1 : f (n + 1) - f n = f (-1) + 1
⊢ f (n + 1) = f (-1) + 1 + f n
Tactic:
exact eq_add_of_sub_eq h1
Proof state after:
no goals
Theorem: IMOSL.IMO2015A2.final_solution
Proof state before:
case refine_2.refine_1
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
h1 : ∀ (n : ℤ), f n = (f (-1) + 1) * n + f 0
h2 : f (-1) + 1 = 0
x : ℤ
⊢ f x = -1
Tactic:
rw [h1, h2, Int.zero_mul, zero_add, ← eq_neg_of_add_eq_zero_left h2]
Proof state after:
case refine_2.refine_1
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
h1 : ∀ (n : ℤ), f n = (f (-1) + 1) * n + f 0
h2 : f (-1) + 1 = 0
x : ℤ
⊢ f 0 = f (-1)
Theorem: IMOSL.IMO2015A2.final_solution
Proof state before:
case refine_2.refine_1
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
h1 : ∀ (n : ℤ), f n = (f (-1) + 1) * n + f 0
h2 : f (-1) + 1 = 0
x : ℤ
⊢ f 0 = f (-1)
Tactic:
specialize h1 (-1)
Proof state after:
case refine_2.refine_1
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
h2 : f (-1) + 1 = 0
x : ℤ
h1 : f (-1) = (f (-1) + 1) * -1 + f 0
⊢ f 0 = f (-1)
Theorem: IMOSL.IMO2015A2.final_solution
Proof state before:
case refine_2.refine_1
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
h2 : f (-1) + 1 = 0
x : ℤ
h1 : f (-1) = (f (-1) + 1) * -1 + f 0
⊢ f 0 = f (-1)
Tactic:
rw [h2, Int.zero_mul, zero_add] at h1
Proof state after:
case refine_2.refine_1
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
h2 : f (-1) + 1 = 0
x : ℤ
h1 : f (-1) = f 0
⊢ f 0 = f (-1)
Theorem: IMOSL.IMO2015A2.final_solution
Proof state before:
case refine_2.refine_1
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
h2 : f (-1) + 1 = 0
x : ℤ
h1 : f (-1) = f 0
⊢ f 0 = f (-1)
Tactic:
exact h1.symm
Proof state after:
no goals
Theorem: IMOSL.IMO2015A2.final_solution
Proof state before:
case refine_2.refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h0 : ∀ (x : ℤ), f (x + 1) = f (f x)
h1 : ∀ (n : ℤ), f n = (f (-1) + 1) * n + f 0
h2 : f (-1) + 1 ≠ 0
x : ℤ
⊢ f x = x + 1
Tactic:
specialize h0 x
Proof state after:
case refine_2.refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h1 : ∀ (n : ℤ), f n = (f (-1) + 1) * n + f 0
h2 : f (-1) + 1 ≠ 0
x : ℤ
h0 : f (x + 1) = f (f x)
⊢ f x = x + 1
Theorem: IMOSL.IMO2015A2.final_solution
Proof state before:
case refine_2.refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h1 : ∀ (n : ℤ), f n = (f (-1) + 1) * n + f 0
h2 : f (-1) + 1 ≠ 0
x : ℤ
h0 : f (x + 1) = f (f x)
⊢ f x = x + 1
Tactic:
rw [h1, h1 (f x), add_left_inj, Int.mul_eq_mul_left_iff h2] at h0
Proof state after:
case refine_2.refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h1 : ∀ (n : ℤ), f n = (f (-1) + 1) * n + f 0
h2 : f (-1) + 1 ≠ 0
x : ℤ
h0 : x + 1 = f x
⊢ f x = x + 1
Theorem: IMOSL.IMO2015A2.final_solution
Proof state before:
case refine_2.refine_2
f : ℤ → ℤ
h : ∀ (x y : ℤ), f (x - f y) = f (f x) - f y - 1
h1 : ∀ (n : ℤ), f n = (f (-1) + 1) * n + f 0
h2 : f (-1) + 1 ≠ 0
x : ℤ
h0 : x + 1 = f x
⊢ f x = x + 1
Tactic:
exact h0.symm
Proof state after:
no goals
Theorem: IMOSL.IMO2006N3.g_succ
Proof state before:
n : ℕ
⊢ g n.succ = g n + n.succ.divisors.card
Tactic:
rw [g, g, Nat.divisors]
Proof state after:
n : ℕ
⊢ ∑ k ∈ range n.succ, n.succ / (k + 1) =
    ∑ k ∈ range n, n / (k + 1) + (filter (fun x => x ∣ n.succ) (Ico 1 (n.succ + 1))).card