internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2012A5.ℤφ.mul_assoc
Proof state before:
a b a' b' a'' b'' : ℤ
⊢ { re := a * a' + b * b', im := a * b' + a' * b + b * b' }.re * a'' +
        { re := a * a' + b * b', im := a * b' + a' * b + b * b' }.im * b'' =
      a * { re := a' * a'' + b' * b'', im := a' * b'' + a'' * b' + b' * b'' }.re +
        b * { re := a' * a'' + b' * b'', im := a' * b'' + a'' * b' + b' * b'' }.im ∧
    { re := a * a' + b * b', im := a * b' + a' * b + b * b' }.re * b'' +
          a'' * { re := a * a' + b * b', im := a * b' + a' * b + b * b' }.im +
        { re := a * a' + b * b', im := a * b' + a' * b + b * b' }.im * b'' =
      a * { re := a' * a'' + b' * b'', im := a' * b'' + a'' * b' + b' * b'' }.im +
          { re := a' * a'' + b' * b'', im := a' * b'' + a'' * b' + b' * b'' }.re * b +
        b * { re := a' * a'' + b' * b'', im := a' * b'' + a'' * b' + b' * b'' }.im
Tactic:
dsimp only
Proof state after:
a b a' b' a'' b'' : ℤ
⊢ (a * a' + b * b') * a'' + (a * b' + a' * b + b * b') * b'' =
      a * (a' * a'' + b' * b'') + b * (a' * b'' + a'' * b' + b' * b'') ∧
    (a * a' + b * b') * b'' + a'' * (a * b' + a' * b + b * b') + (a * b' + a' * b + b * b') * b'' =
      a * (a' * b'' + a'' * b' + b' * b'') + (a' * a'' + b' * b'') * b + b * (a' * b'' + a'' * b' + b' * b'')
Theorem: IMOSL.IMO2012A5.ℤφ.mul_assoc
Proof state before:
a b a' b' a'' b'' : ℤ
⊢ (a * a' + b * b') * a'' + (a * b' + a' * b + b * b') * b'' =
      a * (a' * a'' + b' * b'') + b * (a' * b'' + a'' * b' + b' * b'') ∧
    (a * a' + b * b') * b'' + a'' * (a * b' + a' * b + b * b') + (a * b' + a' * b + b * b') * b'' =
      a * (a' * b'' + a'' * b' + b' * b'') + (a' * a'' + b' * b'') * b + b * (a' * b'' + a'' * b' + b' * b'')
Tactic:
constructor <;> ring
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.ℤφ.zero_mul
Proof state before:
a b : ℤ
⊢ 0 * { re := a, im := b } = 0
Tactic:
rw [mul_def, zero_def, zero_mul,
zero_mul, mul_zero, add_zero, add_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.ℤφ.one_mul
Proof state before:
a b : ℤ
⊢ 1 * { re := a, im := b } = { re := a, im := b }
Tactic:
rw [mul_def, one_def, one_mul, one_mul,
zero_mul, mul_zero, add_zero, add_zero, add_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.ℤφ.mul_add
Proof state before:
a b a' b' a'' b'' : ℤ
⊢ { re := a, im := b } * ({ re := a', im := b' } + { re := a'', im := b'' }) =
    { re := a, im := b } * { re := a', im := b' } + { re := a, im := b } * { re := a'', im := b'' }
Tactic:
rw [mul_def, mul_def, mul_def, add_def, add_def, ℤφ.mk.injEq]
Proof state after:
a b a' b' a'' b'' : ℤ
⊢ a * { re := a' + a'', im := b' + b'' }.re + b * { re := a' + a'', im := b' + b'' }.im =
      a * a' + b * b' + (a * a'' + b * b'') ∧
    a * { re := a' + a'', im := b' + b'' }.im + { re := a' + a'', im := b' + b'' }.re * b +
        b * { re := a' + a'', im := b' + b'' }.im =
      a * b' + a' * b + b * b' + (a * b'' + a'' * b + b * b'')
Theorem: IMOSL.IMO2012A5.ℤφ.mul_add
Proof state before:
a b a' b' a'' b'' : ℤ
⊢ a * { re := a' + a'', im := b' + b'' }.re + b * { re := a' + a'', im := b' + b'' }.im =
      a * a' + b * b' + (a * a'' + b * b'') ∧
    a * { re := a' + a'', im := b' + b'' }.im + { re := a' + a'', im := b' + b'' }.re * b +
        b * { re := a' + a'', im := b' + b'' }.im =
      a * b' + a' * b + b * b' + (a * b'' + a'' * b + b * b'')
Tactic:
dsimp only
Proof state after:
a b a' b' a'' b'' : ℤ
⊢ a * (a' + a'') + b * (b' + b'') = a * a' + b * b' + (a * a'' + b * b'') ∧
    a * (b' + b'') + (a' + a'') * b + b * (b' + b'') = a * b' + a' * b + b * b' + (a * b'' + a'' * b + b * b'')
Theorem: IMOSL.IMO2012A5.ℤφ.mul_add
Proof state before:
a b a' b' a'' b'' : ℤ
⊢ a * (a' + a'') + b * (b' + b'') = a * a' + b * b' + (a * a'' + b * b'') ∧
    a * (b' + b'') + (a' + a'') * b + b * (b' + b'') = a * b' + a' * b + b * b' + (a * b'' + a'' * b + b * b'')
Tactic:
constructor
Proof state after:
case left
a b a' b' a'' b'' : ℤ
⊢ a * (a' + a'') + b * (b' + b'') = a * a' + b * b' + (a * a'' + b * b'')

case right
a b a' b' a'' b'' : ℤ
⊢ a * (b' + b'') + (a' + a'') * b + b * (b' + b'') = a * b' + a' * b + b * b' + (a * b'' + a'' * b + b * b'')
Theorem: IMOSL.IMO2012A5.ℤφ.mul_add
Proof state before:
case left
a b a' b' a'' b'' : ℤ
⊢ a * (a' + a'') + b * (b' + b'') = a * a' + b * b' + (a * a'' + b * b'')
Tactic:
rw [add_add_add_comm, ← mul_add, ← mul_add]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.ℤφ.mul_add
Proof state before:
case right
a b a' b' a'' b'' : ℤ
⊢ a * (b' + b'') + (a' + a'') * b + b * (b' + b'') = a * b' + a' * b + b * b' + (a * b'' + a'' * b + b * b'')
Tactic:
rw [add_add_add_comm, ← mul_add, add_add_add_comm, ← mul_add, ← add_mul]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.ℤφ.add_mul
Proof state before:
x y z : ℤφ
⊢ (x + y) * z = x * z + y * z
Tactic:
rw [ℤφ.mul_comm, ℤφ.mul_add, z.mul_comm, z.mul_comm]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.ℤφ.cast_zero
Proof state before:
R : Type u_1
inst✝ : AddGroupWithOne R
r : R
⊢ cast r 0 = 0
Tactic:
change ((0 : ℤ) : R) + 0 • r = 0
Proof state after:
R : Type u_1
inst✝ : AddGroupWithOne R
r : R
⊢ ↑0 + 0 • r = 0
Theorem: IMOSL.IMO2012A5.ℤφ.cast_zero
Proof state before:
R : Type u_1
inst✝ : AddGroupWithOne R
r : R
⊢ ↑0 + 0 • r = 0
Tactic:
rw [Int.cast_zero, zero_add, zero_zsmul]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.ℤφ.cast_one
Proof state before:
R : Type u_1
inst✝ : AddGroupWithOne R
r : R
⊢ cast r 1 = 1
Tactic:
change ((1 : ℤ) : R) + 0 • r = 1
Proof state after:
R : Type u_1
inst✝ : AddGroupWithOne R
r : R
⊢ ↑1 + 0 • r = 1
Theorem: IMOSL.IMO2012A5.ℤφ.cast_one
Proof state before:
R : Type u_1
inst✝ : AddGroupWithOne R
r : R
⊢ ↑1 + 0 • r = 1
Tactic:
rw [Int.cast_one, zero_zsmul, add_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.ℤφ.cast_φ
Proof state before:
R : Type u_1
inst✝ : AddGroupWithOne R
r : R
⊢ cast r φ = r
Tactic:
change ((0 : ℤ) : R) + 1 • r = r
Proof state after:
R : Type u_1
inst✝ : AddGroupWithOne R
r : R
⊢ ↑0 + 1 • r = r
Theorem: IMOSL.IMO2012A5.ℤφ.cast_φ
Proof state before:
R : Type u_1
inst✝ : AddGroupWithOne R
r : R
⊢ ↑0 + 1 • r = r
Tactic:
rw [Int.cast_zero, zero_add, one_zsmul]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.ℤφ.cast_add
Proof state before:
R : Type u_1
inst✝ : AddCommGroupWithOne R
r : R
a b a' b' : ℤ
⊢ cast r ({ re := a, im := b } + { re := a', im := b' }) = cast r { re := a, im := b } + cast r { re := a', im := b' }
Tactic:
change ((a + a' : ℤ) : R) + (b + b') • r = _
Proof state after:
R : Type u_1
inst✝ : AddCommGroupWithOne R
r : R
a b a' b' : ℤ
⊢ ↑(a + a') + (b + b') • r = cast r { re := a, im := b } + cast r { re := a', im := b' }
Theorem: IMOSL.IMO2012A5.ℤφ.cast_add
Proof state before:
R : Type u_1
inst✝ : AddCommGroupWithOne R
r : R
a b a' b' : ℤ
⊢ ↑(a + a') + (b + b') • r = cast r { re := a, im := b } + cast r { re := a', im := b' }
Tactic:
rw [Int.cast_add, add_zsmul, add_add_add_comm]
Proof state after:
R : Type u_1
inst✝ : AddCommGroupWithOne R
r : R
a b a' b' : ℤ
⊢ ↑a + b • r + (↑a' + b' • r) = cast r { re := a, im := b } + cast r { re := a', im := b' }
Theorem: IMOSL.IMO2012A5.ℤφ.cast_add
Proof state before:
R : Type u_1
inst✝ : AddCommGroupWithOne R
r : R
a b a' b' : ℤ
⊢ ↑a + b • r + (↑a' + b' • r) = cast r { re := a, im := b } + cast r { re := a', im := b' }
Tactic:
rfl
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.ℤφ.cast_mul
Proof state before:
R : Type u_1
inst✝ : Ring R
r : R
h : r * r = r + 1
a b a' b' : ℤ
⊢ cast r ({ re := a, im := b } * { re := a', im := b' }) = cast r { re := a, im := b } * cast r { re := a', im := b' }
Tactic:
change ↑(a * a' + b * b') + (a * b' + a' * b + b * b') • r
  = (↑a + b • r) * (↑a' + b' • r)
Proof state after:
R : Type u_1
inst✝ : Ring R
r : R
h : r * r = r + 1
a b a' b' : ℤ
⊢ ↑(a * a' + b * b') + (a * b' + a' * b + b * b') • r = (↑a + b • r) * (↑a' + b' • r)
Theorem: IMOSL.IMO2012A5.ℤφ.cast_mul
Proof state before:
R : Type u_1
inst✝ : Ring R
r : R
h : r * r = r + 1
a b a' b' : ℤ
⊢ ↑(a * a' + b * b') + (a * b' + a' * b + b * b') • r = (↑a + b • r) * (↑a' + b' • r)
Tactic:
rw [add_zsmul, Int.cast_add, add_add_add_comm, ← zsmul_one (b * b'),
  ← zsmul_add, add_comm 1 r, ← h, add_zsmul, ← add_assoc, mul_zsmul,
  zsmul_eq_mul, Int.cast_mul, ← mul_add, add_mul, add_assoc, add_right_inj,
  mul_add, ← zsmul_eq_mul', mul_zsmul, add_right_inj, mul_zsmul, zsmul_eq_mul,
  zsmul_eq_mul', zsmul_eq_mul, zsmul_eq_mul', mul_assoc, ← mul_assoc]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₂X.toList_inj
Proof state before:
P Q : 𝔽₂X
h : P.toList = Q.toList
⊢ P.toFinset = Q.toFinset
Tactic:
rw [← 𝔽₂X.toFinset_toList, h, 𝔽₂X.toFinset_toList]
Proof state after:
no goals
Theorem: IMOSL.IMO2012N1.admissible_mem_sq_mul
Proof state before:
R : Type u_1
z : R
inst✝ : CommRing R
A : Set R
h : admissible A
h0 : z ∈ A
k : R
⊢ k * z ^ 2 ∈ A
Tactic:
have h1 := h z z h0 h0 (k - 2)
Proof state after:
R : Type u_1
z : R
inst✝ : CommRing R
A : Set R
h : admissible A
h0 : z ∈ A
k : R
h1 : z ^ 2 + (k - 2) * z * z + z ^ 2 ∈ A
⊢ k * z ^ 2 ∈ A
Theorem: IMOSL.IMO2012N1.admissible_mem_sq_mul
Proof state before:
R : Type u_1
z : R
inst✝ : CommRing R
A : Set R
h : admissible A
h0 : z ∈ A
k : R
h1 : z ^ 2 + (k - 2) * z * z + z ^ 2 ∈ A
⊢ k * z ^ 2 ∈ A
Tactic:
rwa [mul_assoc, ← sq, ← one_add_mul (α := R), ← add_one_mul (α := R),
  add_right_comm, one_add_one_eq_two, add_sub_cancel] at h1
Proof state after:
no goals
Theorem: IMOSL.IMO2012N1.final_solution
Proof state before:
R : Type u_1
inst✝ : CommRing R
x y : R
h : ∀ (A : Set R), admissible A → x ∈ A → y ∈ A → ∀ (z : R), z ∈ A
⊢ IsCoprime x y
Tactic:
specialize h (Ideal.span {x, y}) (admissible_ideal _)
  (Ideal.subset_span (Set.mem_insert x _))
  (Ideal.subset_span (Set.mem_insert_of_mem x rfl)) 1
Proof state after:
R : Type u_1
inst✝ : CommRing R
x y : R
h : 1 ∈ ↑(Ideal.span {x, y})
⊢ IsCoprime x y
Theorem: IMOSL.IMO2012N1.final_solution
Proof state before:
R : Type u_1
inst✝ : CommRing R
x y : R
h : 1 ∈ ↑(Ideal.span {x, y})
⊢ IsCoprime x y
Tactic:
rwa [SetLike.mem_coe, Ideal.mem_span_pair] at h
Proof state after:
no goals
Theorem: IMOSL.IMO2012N1.final_solution
Proof state before:
R : Type u_1
inst✝ : CommRing R
x y : R
h : IsCoprime x y
A : Set R
h0 : admissible A
h1 : x ∈ A
h2 : y ∈ A
⊢ ∀ (z : R), z ∈ A
Tactic:
suffices 1 ∈ A from λ z ↦ mul_one z ▸
  one_pow (M := R) 2 ▸ admissible_mem_sq_mul h0 this z
Proof state after:
R : Type u_1
inst✝ : CommRing R
x y : R
h : IsCoprime x y
A : Set R
h0 : admissible A
h1 : x ∈ A
h2 : y ∈ A
⊢ 1 ∈ A
Theorem: IMOSL.IMO2012N1.final_solution
Proof state before:
R : Type u_1
inst✝ : CommRing R
x y : R
h : IsCoprime x y
A : Set R
h0 : admissible A
h1 : x ∈ A
h2 : y ∈ A
⊢ 1 ∈ A
Tactic:
obtain ⟨a, b, h⟩ : IsCoprime (x ^ 2) (y ^ 2) := IsCoprime.pow h
Proof state after:
case intro.intro
R : Type u_1
inst✝ : CommRing R
x y : R
h✝ : IsCoprime x y
A : Set R
h0 : admissible A
h1 : x ∈ A
h2 : y ∈ A
a b : R
h : a * x ^ 2 + b * y ^ 2 = 1
⊢ 1 ∈ A
Theorem: IMOSL.IMO2012N1.final_solution
Proof state before:
case intro.intro
R : Type u_1
inst✝ : CommRing R
x y : R
h✝ : IsCoprime x y
A : Set R
h0 : admissible A
h1 : x ∈ A
h2 : y ∈ A
a b : R
h : a * x ^ 2 + b * y ^ 2 = 1
⊢ 1 ∈ A
Tactic:
rw [← one_pow 2, ← h]
Proof state after:
case intro.intro
R : Type u_1
inst✝ : CommRing R
x y : R
h✝ : IsCoprime x y
A : Set R
h0 : admissible A
h1 : x ∈ A
h2 : y ∈ A
a b : R
h : a * x ^ 2 + b * y ^ 2 = 1
⊢ (a * x ^ 2 + b * y ^ 2) ^ 2 ∈ A
Theorem: IMOSL.IMO2012N1.final_solution
Proof state before:
case intro.intro
R : Type u_1
inst✝ : CommRing R
x y : R
h✝ : IsCoprime x y
A : Set R
h0 : admissible A
h1 : x ∈ A
h2 : y ∈ A
a b : R
h : a * x ^ 2 + b * y ^ 2 = 1
⊢ (a * x ^ 2 + b * y ^ 2) ^ 2 ∈ A
Tactic:
refine admissible_add_sq h0 (admissible_mem_sq_mul h0 h1 a)
  (admissible_mem_sq_mul h0 h2 b)
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.sub_one_is_good
Proof state before:
R : Type u_1
inst✝ : NonAssocRing R
x y : R
⊢ (fun x => x - 1) (x * y + 1) = (fun x => x - 1) x * (fun x => x - 1) y + (fun x => x - 1) (x + y)
Tactic:
rw [sub_one_mul, mul_sub_one, sub_sub, ← add_sub_assoc x, sub_add_cancel]
Proof state after:
R : Type u_1
inst✝ : NonAssocRing R
x y : R
⊢ (fun x => x - 1) (x * y + 1) = x * y
Theorem: IMOSL.IMO2012A5.sub_one_is_good
Proof state before:
R : Type u_1
inst✝ : NonAssocRing R
x y : R
⊢ (fun x => x - 1) (x * y + 1) = x * y
Tactic:
exact add_sub_cancel_right _ _
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.sub_one_solver
Proof state before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
⊢ ∃ φ, ∀ (x : R), f x = φ (x - 1)
Tactic:
suffices ∀ x y, f (x + y) = f x + f y + 1 by
  have h0 (x y) : f (x + y + 1) = f (x + 1) + f (y + 1) := by
    rw [h, h, h, this, add_assoc, add_add_add_comm]
  have h1 (x y) : f (x * y + 1) = f (x + 1) * f (y + 1) := by
    rw [hf.is_good, h, h, this, add_assoc, ← add_assoc,
      ← mul_add_one (f x), ← add_one_mul (f x)]
  exact ⟨⟨⟨⟨λ x ↦ f (x + 1), (h 1).trans <| by rw [hf.map_one, zero_add]⟩, h1⟩,
      ((h 0).trans hf.map_zero_add_one), h0⟩,
    λ x ↦ congrArg f (sub_add_cancel x 1).symm⟩
Proof state after:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
⊢ ∀ (x y : R), f (x + y) = f x + f y + 1
Theorem: IMOSL.IMO2012A5.sub_one_solver
Proof state before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
⊢ ∀ (x y : R), f (x + y) = f x + f y + 1
Tactic:
have h0 (x y) : f (x * y) + 1 = f x * f y + f (x + y) :=
  (h _).symm.trans (hf.is_good x y)
Proof state after:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
h0 : ∀ (x y : R), f (x * y) + 1 = f x * f y + f (x + y)
⊢ ∀ (x y : R), f (x + y) = f x + f y + 1
Theorem: IMOSL.IMO2012A5.sub_one_solver
Proof state before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
h0 : ∀ (x y : R), f (x * y) + 1 = f x * f y + f (x + y)
⊢ ∀ (x y : R), f (x + y) = f x + f y + 1
Tactic:
have h1 (x y) : f (x * y) = f x * f y + f (x + y) - 1 :=
  eq_sub_of_add_eq (h0 x y)
Proof state after:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
h0 : ∀ (x y : R), f (x * y) + 1 = f x * f y + f (x + y)
h1 : ∀ (x y : R), f (x * y) = f x * f y + f (x + y) - 1
⊢ ∀ (x y : R), f (x + y) = f x + f y + 1
Theorem: IMOSL.IMO2012A5.sub_one_solver
Proof state before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
h0 : ∀ (x y : R), f (x * y) + 1 = f x * f y + f (x + y)
h1 : ∀ (x y : R), f (x * y) = f x * f y + f (x + y) - 1
⊢ ∀ (x y : R), f (x + y) = f x + f y + 1
Tactic:
have h2 (x y) : f ((x + 1) * y) = f (x * y) + (f y + 1) := by
  rw [h1, h, add_right_comm, add_one_mul (f x), h, add_add_add_comm,
    ← h0, add_right_comm, add_sub_cancel_right]
Proof state after:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
h0 : ∀ (x y : R), f (x * y) + 1 = f x * f y + f (x + y)
h1 : ∀ (x y : R), f (x * y) = f x * f y + f (x + y) - 1
h2 : ∀ (x y : R), f ((x + 1) * y) = f (x * y) + (f y + 1)
⊢ ∀ (x y : R), f (x + y) = f x + f y + 1
Theorem: IMOSL.IMO2012A5.sub_one_solver
Proof state before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
h0 : ∀ (x y : R), f (x * y) + 1 = f x * f y + f (x + y)
h1 : ∀ (x y : R), f (x * y) = f x * f y + f (x + y) - 1
h2 : ∀ (x y : R), f ((x + 1) * y) = f (x * y) + (f y + 1)
⊢ ∀ (x y : R), f (x + y) = f x + f y + 1
Tactic:
intro x y
Proof state after:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
h0 : ∀ (x y : R), f (x * y) + 1 = f x * f y + f (x + y)
h1 : ∀ (x y : R), f (x * y) = f x * f y + f (x + y) - 1
h2 : ∀ (x y : R), f ((x + 1) * y) = f (x * y) + (f y + 1)
x y : R
⊢ f (x + y) = f x + f y + 1
Theorem: IMOSL.IMO2012A5.sub_one_solver
Proof state before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
h0 : ∀ (x y : R), f (x * y) + 1 = f x * f y + f (x + y)
h1 : ∀ (x y : R), f (x * y) = f x * f y + f (x + y) - 1
h2 : ∀ (x y : R), f ((x + 1) * y) = f (x * y) + (f y + 1)
x y : R
⊢ f (x + y) = f x + f y + 1
Tactic:
have h3 : f (x * ((x + 1) * y)) = f ((x + 1) * (x * y)) := by
  rw [add_one_mul x, add_one_mul x, mul_add]
Proof state after:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
h0 : ∀ (x y : R), f (x * y) + 1 = f x * f y + f (x + y)
h1 : ∀ (x y : R), f (x * y) = f x * f y + f (x + y) - 1
h2 : ∀ (x y : R), f ((x + 1) * y) = f (x * y) + (f y + 1)
x y : R
h3 : f (x * ((x + 1) * y)) = f ((x + 1) * (x * y))
⊢ f (x + y) = f x + f y + 1
Theorem: IMOSL.IMO2012A5.sub_one_solver
Proof state before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
h0 : ∀ (x y : R), f (x * y) + 1 = f x * f y + f (x + y)
h1 : ∀ (x y : R), f (x * y) = f x * f y + f (x + y) - 1
h2 : ∀ (x y : R), f ((x + 1) * y) = f (x * y) + (f y + 1)
x y : R
h3 : f (x * ((x + 1) * y)) = f ((x + 1) * (x * y))
⊢ f (x + y) = f x + f y + 1
Tactic:
rwa [h2, h1, h2, mul_add, ← add_assoc, add_right_comm _ _ 1, h0, ← h,
  sub_eq_iff_eq_add, add_assoc, add_assoc, add_assoc, add_right_inj,
  ← add_left_inj 1, add_assoc, ← h, add_right_comm, ← mul_one_add (x + 1),
  h2, add_left_comm, mul_one_add x, add_assoc, add_right_inj, add_comm 1,
  h, mul_add_one (f x), h0, add_assoc, add_assoc (_ * _), add_right_inj,
  ← add_assoc, add_left_inj, ← add_assoc, eq_comm] at h3
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.sub_one_solver
Proof state before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
this : ∀ (x y : R), f (x + y) = f x + f y + 1
⊢ ∃ φ, ∀ (x : R), f x = φ (x - 1)
Tactic:
have h0 (x y) : f (x + y + 1) = f (x + 1) + f (y + 1) := by
  rw [h, h, h, this, add_assoc, add_add_add_comm]
Proof state after:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
this : ∀ (x y : R), f (x + y) = f x + f y + 1
h0 : ∀ (x y : R), f (x + y + 1) = f (x + 1) + f (y + 1)
⊢ ∃ φ, ∀ (x : R), f x = φ (x - 1)
Theorem: IMOSL.IMO2012A5.sub_one_solver
Proof state before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
this : ∀ (x y : R), f (x + y) = f x + f y + 1
h0 : ∀ (x y : R), f (x + y + 1) = f (x + 1) + f (y + 1)
⊢ ∃ φ, ∀ (x : R), f x = φ (x - 1)
Tactic:
have h1 (x y) : f (x * y + 1) = f (x + 1) * f (y + 1) := by
  rw [hf.is_good, h, h, this, add_assoc, ← add_assoc,
    ← mul_add_one (f x), ← add_one_mul (f x)]
Proof state after:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
this : ∀ (x y : R), f (x + y) = f x + f y + 1
h0 : ∀ (x y : R), f (x + y + 1) = f (x + 1) + f (y + 1)
h1 : ∀ (x y : R), f (x * y + 1) = f (x + 1) * f (y + 1)
⊢ ∃ φ, ∀ (x : R), f x = φ (x - 1)
Theorem: IMOSL.IMO2012A5.sub_one_solver
Proof state before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
this : ∀ (x y : R), f (x + y) = f x + f y + 1
h0 : ∀ (x y : R), f (x + y + 1) = f (x + 1) + f (y + 1)
h1 : ∀ (x y : R), f (x * y + 1) = f (x + 1) * f (y + 1)
⊢ ∃ φ, ∀ (x : R), f x = φ (x - 1)
Tactic:
exact ⟨⟨⟨⟨λ x ↦ f (x + 1), (h 1).trans <| by rw [hf.map_one, zero_add]⟩, h1⟩,
    ((h 0).trans hf.map_zero_add_one), h0⟩,
  λ x ↦ congrArg f (sub_add_cancel x 1).symm⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.sub_one_solver
Proof state before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
this : ∀ (x y : R), f (x + y) = f x + f y + 1
x y : R
⊢ f (x + y + 1) = f (x + 1) + f (y + 1)
Tactic:
rw [h, h, h, this, add_assoc, add_add_add_comm]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.sub_one_solver
Proof state before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
this : ∀ (x y : R), f (x + y) = f x + f y + 1
h0 : ∀ (x y : R), f (x + y + 1) = f (x + 1) + f (y + 1)
x y : R
⊢ f (x * y + 1) = f (x + 1) * f (y + 1)
Tactic:
rw [hf.is_good, h, h, this, add_assoc, ← add_assoc,
  ← mul_add_one (f x), ← add_one_mul (f x)]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.sub_one_solver
Proof state before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
this : ∀ (x y : R), f (x + y) = f x + f y + 1
h0 : ∀ (x y : R), f (x + y + 1) = f (x + 1) + f (y + 1)
h1 : ∀ (x y : R), f (x * y + 1) = f (x + 1) * f (y + 1)
⊢ f 1 + 1 = 1
Tactic:
rw [hf.map_one, zero_add]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.sub_one_solver
Proof state before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
h0 : ∀ (x y : R), f (x * y) + 1 = f x * f y + f (x + y)
h1 : ∀ (x y : R), f (x * y) = f x * f y + f (x + y) - 1
x y : R
⊢ f ((x + 1) * y) = f (x * y) + (f y + 1)
Tactic:
rw [h1, h, add_right_comm, add_one_mul (f x), h, add_add_add_comm,
  ← h0, add_right_comm, add_sub_cancel_right]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.sub_one_solver
Proof state before:
R : Type u_2
inst✝¹ : NonAssocRing R
S : Type u_1
inst✝ : NonAssocRing S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (x + 1) = f x + 1
h0 : ∀ (x y : R), f (x * y) + 1 = f x * f y + f (x + y)
h1 : ∀ (x y : R), f (x * y) = f x * f y + f (x + y) - 1
h2 : ∀ (x y : R), f ((x + 1) * y) = f (x * y) + (f y + 1)
x y : R
⊢ f (x * ((x + 1) * y)) = f ((x + 1) * (x * y))
Tactic:
rw [add_one_mul x, add_one_mul x, mul_add]
Proof state after:
no goals
Theorem: IMOSL.Extra.symmDiff_singleton_eq_erase
Proof state before:
ι : Type u_1
inst✝ : DecidableEq ι
i : ι
S : Finset ι
h : i ∈ S
⊢ symmDiff {i} S = S.erase i
Tactic:
have h0 : {i} \ S = ∅ :=
  Finset.sdiff_eq_empty_iff_subset.mpr λ c h0 ↦ Finset.mem_singleton.mp h0 ▸ h
Proof state after:
ι : Type u_1
inst✝ : DecidableEq ι
i : ι
S : Finset ι
h : i ∈ S
h0 : {i} \ S = ∅
⊢ symmDiff {i} S = S.erase i
Theorem: IMOSL.Extra.symmDiff_singleton_eq_erase
Proof state before:
ι : Type u_1
inst✝ : DecidableEq ι
i : ι
S : Finset ι
h : i ∈ S
h0 : {i} \ S = ∅
⊢ symmDiff {i} S = S.erase i
Tactic:
rw [symmDiff, Finset.sdiff_singleton_eq_erase, h0]
Proof state after:
ι : Type u_1
inst✝ : DecidableEq ι
i : ι
S : Finset ι
h : i ∈ S
h0 : {i} \ S = ∅
⊢ ∅ ⊔ S.erase i = S.erase i
Theorem: IMOSL.Extra.symmDiff_singleton_eq_erase
Proof state before:
ι : Type u_1
inst✝ : DecidableEq ι
i : ι
S : Finset ι
h : i ∈ S
h0 : {i} \ S = ∅
⊢ ∅ ⊔ S.erase i = S.erase i
Tactic:
exact bot_sup_eq _
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.symmDiff_singleton_sum_eq
Proof state before:
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
i : ι
S : Finset ι
⊢ (symmDiff {i} S).sum f = f i + S.sum f
Tactic:
by_cases h : i ∈ S
Proof state after:
case pos
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
i : ι
S : Finset ι
h : i ∈ S
⊢ (symmDiff {i} S).sum f = f i + S.sum f

case neg
M : Type u_2
ι : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : CharTwo M
inst✝ : DecidableEq ι
f : ι → M
i : ι
S : Finset ι
h : i ∉ S
⊢ (symmDiff {i} S).sum f = f i + S.sum f