internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.mul_right
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : ∀ (x : R), f (c * x + 1) = 0
d x : R
⊢ f (c * d * x + 1) = 0
Tactic:
rw [mul_assoc]
Proof state after:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : ∀ (x : R), f (c * x + 1) = 0
d x : R
⊢ f (c * (d * x) + 1) = 0
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.mul_right
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
c : R
h : ∀ (x : R), f (c * x + 1) = 0
d x : R
⊢ f (c * (d * x) + 1) = 0
Tactic:
exact h (d * x)
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.reduced_eq_zero_iff
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0✝ : c ≠ 0
h0 : f c = -1
x : R
⊢ f (x + c) = f (x + 0)
Tactic:
rw [add_zero, (iff_right hf.toNontrivialGood).mp h, h0, neg_neg, mul_one]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.reduced_QuasiPeriodic_eq
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : QuasiPeriodic f d
h2 : f d = 1
x : R
⊢ f (x + d) = f (x + c)
Tactic:
have h3 (c) := (iff_right hf.toNontrivialGood (c := c)).mp
Proof state after:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : QuasiPeriodic f d
h2 : f d = 1
x : R
h3 : ∀ (c : R), QuasiPeriodic f c → ∀ (x : R), f (x + c) = f x * -f c
⊢ f (x + d) = f (x + c)
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.reduced_QuasiPeriodic_eq
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : QuasiPeriodic f d
h2 : f d = 1
x : R
h3 : ∀ (c : R), QuasiPeriodic f c → ∀ (x : R), f (x + c) = f x * -f c
⊢ f (x + d) = f (x + c)
Tactic:
rw [h3 c h, h3 d h1, h2, reduced_map_eq_one hf h h0]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.reduced_mul_left_eq_zero_imp
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : d * c = 0
⊢ QuasiPeriodic f d
Tactic:
rw [iff_left2 hf.toNontrivialGood]
Proof state after:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : d * c = 0
⊢ ∀ (x : R), f (d * x + 1) = 0
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.reduced_mul_left_eq_zero_imp
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : d * c = 0
⊢ ∀ (x : R), f (d * x + 1) = 0
Tactic:
intro x
Proof state after:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : d * c = 0
x : R
⊢ f (d * x + 1) = 0
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.reduced_mul_left_eq_zero_imp
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : d * c = 0
x : R
⊢ f (d * x + 1) = 0
Tactic:
have h2 := reduced_map_eq_one hf h h0
Proof state after:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : d * c = 0
x : R
h2 : f c = 1
⊢ f (d * x + 1) = 0
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.reduced_mul_left_eq_zero_imp
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : d * c = 0
x : R
h2 : f c = 1
⊢ f (d * x + 1) = 0
Tactic:
have h3 : f (d * (c + x) + 1) = -f (d * x + 1) := by
  rw [iff_left hf.toNontrivialGood] at h
  rw [hf.is_good, h, add_left_comm, h, h2, neg_one_mul,
    neg_one_mul, mul_neg, ← neg_add, hf.is_good]
Proof state after:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : d * c = 0
x : R
h2 : f c = 1
h3 : f (d * (c + x) + 1) = -f (d * x + 1)
⊢ f (d * x + 1) = 0
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.reduced_mul_left_eq_zero_imp
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : d * c = 0
x : R
h2 : f c = 1
h3 : f (d * (c + x) + 1) = -f (d * x + 1)
⊢ f (d * x + 1) = 0
Tactic:
rw [mul_add, h1, zero_add, eq_neg_iff_add_eq_zero, ← two_mul, mul_eq_zero] at h3
Proof state after:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : d * c = 0
x : R
h2 : f c = 1
h3 : 2 = 0 ∨ f (d * x + 1) = 0
⊢ f (d * x + 1) = 0
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.reduced_mul_left_eq_zero_imp
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : d * c = 0
x : R
h2 : f c = 1
h3 : 2 = 0 ∨ f (d * x + 1) = 0
⊢ f (d * x + 1) = 0
Tactic:
refine h3.resolve_left λ h3 ↦ h0 ?_
Proof state after:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : d * c = 0
x : R
h2 : f c = 1
h3✝ : 2 = 0 ∨ f (d * x + 1) = 0
h3 : 2 = 0
⊢ c = 0
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.reduced_mul_left_eq_zero_imp
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : d * c = 0
x : R
h2 : f c = 1
h3✝ : 2 = 0 ∨ f (d * x + 1) = 0
h3 : 2 = 0
⊢ c = 0
Tactic:
rw [reduced_eq_zero_iff hf h, h2, eq_neg_iff_add_eq_zero, one_add_one_eq_two, h3]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.reduced_mul_left_eq_zero_imp
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : d * c = 0
x : R
h2 : f c = 1
⊢ f (d * (c + x) + 1) = -f (d * x + 1)
Tactic:
rw [iff_left hf.toNontrivialGood] at h
Proof state after:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : ∀ (x : R), f (c + x) = -f c * f x
h0 : c ≠ 0
d : R
h1 : d * c = 0
x : R
h2 : f c = 1
⊢ f (d * (c + x) + 1) = -f (d * x + 1)
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.reduced_mul_left_eq_zero_imp
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : ∀ (x : R), f (c + x) = -f c * f x
h0 : c ≠ 0
d : R
h1 : d * c = 0
x : R
h2 : f c = 1
⊢ f (d * (c + x) + 1) = -f (d * x + 1)
Tactic:
rw [hf.is_good, h, add_left_comm, h, h2, neg_one_mul,
  neg_one_mul, mul_neg, ← neg_add, hf.is_good]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.QuasiPeriodic.reduced_QuasiPeriod_equiv_cases
Proof state before:
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : ReducedGood f
c : R
h : QuasiPeriodic f c
h0 : c ≠ 0
d : R
h1 : ∀ (d : R), d * c = 0 → QuasiPeriodic f d := fun d => reduced_mul_left_eq_zero_imp hf h h0
h2 : d * c = c
⊢ (d - 1) * c = 0
Tactic:
rwa [sub_one_mul, sub_eq_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A7.MetaClosure.add_mem
Proof state before:
G : Type u_1
inst✝³ : Lattice G
inst✝² : AddGroup G
inst✝¹ : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
S : AddSubgroup G
a b : G
ha✝ : MetaClosure (fun x => x ∈ S) a
hb : MetaClosure (fun x => x ∈ S) b
a✝¹ : G
ha : a✝¹ ∈ S
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (a✝¹ + a✝) →
    MetaClosure (fun x => x ∈ S) (a✝¹ + b✝) → MetaClosure (fun x => x ∈ S) (a✝¹ + a✝ ⊓ b✝)
Tactic:
rw [add_inf]
Proof state after:
G : Type u_1
inst✝³ : Lattice G
inst✝² : AddGroup G
inst✝¹ : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
S : AddSubgroup G
a b : G
ha✝ : MetaClosure (fun x => x ∈ S) a
hb : MetaClosure (fun x => x ∈ S) b
a✝¹ : G
ha : a✝¹ ∈ S
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (a✝¹ + a✝) →
    MetaClosure (fun x => x ∈ S) (a✝¹ + b✝) → MetaClosure (fun x => x ∈ S) ((a✝¹ + a✝) ⊓ (a✝¹ + b✝))
Theorem: IMOSL.IMO2012A7.MetaClosure.add_mem
Proof state before:
G : Type u_1
inst✝³ : Lattice G
inst✝² : AddGroup G
inst✝¹ : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
S : AddSubgroup G
a b : G
ha✝ : MetaClosure (fun x => x ∈ S) a
hb : MetaClosure (fun x => x ∈ S) b
a✝¹ : G
ha : a✝¹ ∈ S
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (a✝¹ + a✝) →
    MetaClosure (fun x => x ∈ S) (a✝¹ + b✝) → MetaClosure (fun x => x ∈ S) ((a✝¹ + a✝) ⊓ (a✝¹ + b✝))
Tactic:
exact ofInf
Proof state after:
no goals
Theorem: IMOSL.IMO2012A7.MetaClosure.add_mem
Proof state before:
G : Type u_1
inst✝³ : Lattice G
inst✝² : AddGroup G
inst✝¹ : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
S : AddSubgroup G
a b : G
ha✝ : MetaClosure (fun x => x ∈ S) a
hb : MetaClosure (fun x => x ∈ S) b
a✝¹ : G
ha : a✝¹ ∈ S
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (a✝¹ + a✝) →
    MetaClosure (fun x => x ∈ S) (a✝¹ + b✝) → MetaClosure (fun x => x ∈ S) (a✝¹ + a✝ ⊔ b✝)
Tactic:
rw [add_sup]
Proof state after:
G : Type u_1
inst✝³ : Lattice G
inst✝² : AddGroup G
inst✝¹ : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
S : AddSubgroup G
a b : G
ha✝ : MetaClosure (fun x => x ∈ S) a
hb : MetaClosure (fun x => x ∈ S) b
a✝¹ : G
ha : a✝¹ ∈ S
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (a✝¹ + a✝) →
    MetaClosure (fun x => x ∈ S) (a✝¹ + b✝) → MetaClosure (fun x => x ∈ S) ((a✝¹ + a✝) ⊔ (a✝¹ + b✝))
Theorem: IMOSL.IMO2012A7.MetaClosure.add_mem
Proof state before:
G : Type u_1
inst✝³ : Lattice G
inst✝² : AddGroup G
inst✝¹ : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
S : AddSubgroup G
a b : G
ha✝ : MetaClosure (fun x => x ∈ S) a
hb : MetaClosure (fun x => x ∈ S) b
a✝¹ : G
ha : a✝¹ ∈ S
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (a✝¹ + a✝) →
    MetaClosure (fun x => x ∈ S) (a✝¹ + b✝) → MetaClosure (fun x => x ∈ S) ((a✝¹ + a✝) ⊔ (a✝¹ + b✝))
Tactic:
exact ofSup
Proof state after:
no goals
Theorem: IMOSL.IMO2012A7.MetaClosure.add_mem
Proof state before:
G : Type u_1
inst✝³ : Lattice G
inst✝² : AddGroup G
inst✝¹ : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
S : AddSubgroup G
a b : G
ha : MetaClosure (fun x => x ∈ S) a
hb : MetaClosure (fun x => x ∈ S) b
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (a✝ + b) →
    MetaClosure (fun x => x ∈ S) (b✝ + b) → MetaClosure (fun x => x ∈ S) (a✝ ⊓ b✝ + b)
Tactic:
rw [inf_add]
Proof state after:
G : Type u_1
inst✝³ : Lattice G
inst✝² : AddGroup G
inst✝¹ : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
S : AddSubgroup G
a b : G
ha : MetaClosure (fun x => x ∈ S) a
hb : MetaClosure (fun x => x ∈ S) b
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (a✝ + b) →
    MetaClosure (fun x => x ∈ S) (b✝ + b) → MetaClosure (fun x => x ∈ S) ((a✝ + b) ⊓ (b✝ + b))
Theorem: IMOSL.IMO2012A7.MetaClosure.add_mem
Proof state before:
G : Type u_1
inst✝³ : Lattice G
inst✝² : AddGroup G
inst✝¹ : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
S : AddSubgroup G
a b : G
ha : MetaClosure (fun x => x ∈ S) a
hb : MetaClosure (fun x => x ∈ S) b
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (a✝ + b) →
    MetaClosure (fun x => x ∈ S) (b✝ + b) → MetaClosure (fun x => x ∈ S) ((a✝ + b) ⊓ (b✝ + b))
Tactic:
exact ofInf
Proof state after:
no goals
Theorem: IMOSL.IMO2012A7.MetaClosure.add_mem
Proof state before:
G : Type u_1
inst✝³ : Lattice G
inst✝² : AddGroup G
inst✝¹ : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
S : AddSubgroup G
a b : G
ha : MetaClosure (fun x => x ∈ S) a
hb : MetaClosure (fun x => x ∈ S) b
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (a✝ + b) →
    MetaClosure (fun x => x ∈ S) (b✝ + b) → MetaClosure (fun x => x ∈ S) (a✝ ⊔ b✝ + b)
Tactic:
rw [sup_add]
Proof state after:
G : Type u_1
inst✝³ : Lattice G
inst✝² : AddGroup G
inst✝¹ : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
S : AddSubgroup G
a b : G
ha : MetaClosure (fun x => x ∈ S) a
hb : MetaClosure (fun x => x ∈ S) b
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (a✝ + b) →
    MetaClosure (fun x => x ∈ S) (b✝ + b) → MetaClosure (fun x => x ∈ S) ((a✝ + b) ⊔ (b✝ + b))
Theorem: IMOSL.IMO2012A7.MetaClosure.add_mem
Proof state before:
G : Type u_1
inst✝³ : Lattice G
inst✝² : AddGroup G
inst✝¹ : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
S : AddSubgroup G
a b : G
ha : MetaClosure (fun x => x ∈ S) a
hb : MetaClosure (fun x => x ∈ S) b
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (a✝ + b) →
    MetaClosure (fun x => x ∈ S) (b✝ + b) → MetaClosure (fun x => x ∈ S) ((a✝ + b) ⊔ (b✝ + b))
Tactic:
exact ofSup
Proof state after:
no goals
Theorem: IMOSL.IMO2012A7.MetaClosure.neg_mem
Proof state before:
G : Type u_1
inst✝³ : Lattice G
inst✝² : AddGroup G
inst✝¹ : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
S : AddSubgroup G
a : G
ha : MetaClosure (fun x => x ∈ S) a
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (-a✝) → MetaClosure (fun x => x ∈ S) (-b✝) → MetaClosure (fun x => x ∈ S) (-(a✝ ⊓ b✝))
Tactic:
rw [neg_inf]
Proof state after:
G : Type u_1
inst✝³ : Lattice G
inst✝² : AddGroup G
inst✝¹ : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
S : AddSubgroup G
a : G
ha : MetaClosure (fun x => x ∈ S) a
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (-a✝) → MetaClosure (fun x => x ∈ S) (-b✝) → MetaClosure (fun x => x ∈ S) (-a✝ ⊔ -b✝)
Theorem: IMOSL.IMO2012A7.MetaClosure.neg_mem
Proof state before:
G : Type u_1
inst✝³ : Lattice G
inst✝² : AddGroup G
inst✝¹ : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
S : AddSubgroup G
a : G
ha : MetaClosure (fun x => x ∈ S) a
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (-a✝) → MetaClosure (fun x => x ∈ S) (-b✝) → MetaClosure (fun x => x ∈ S) (-a✝ ⊔ -b✝)
Tactic:
exact ofSup
Proof state after:
no goals
Theorem: IMOSL.IMO2012A7.MetaClosure.neg_mem
Proof state before:
G : Type u_1
inst✝³ : Lattice G
inst✝² : AddGroup G
inst✝¹ : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
S : AddSubgroup G
a : G
ha : MetaClosure (fun x => x ∈ S) a
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (-a✝) → MetaClosure (fun x => x ∈ S) (-b✝) → MetaClosure (fun x => x ∈ S) (-(a✝ ⊔ b✝))
Tactic:
rw [neg_sup]
Proof state after:
G : Type u_1
inst✝³ : Lattice G
inst✝² : AddGroup G
inst✝¹ : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
S : AddSubgroup G
a : G
ha : MetaClosure (fun x => x ∈ S) a
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (-a✝) → MetaClosure (fun x => x ∈ S) (-b✝) → MetaClosure (fun x => x ∈ S) (-a✝ ⊓ -b✝)
Theorem: IMOSL.IMO2012A7.MetaClosure.neg_mem
Proof state before:
G : Type u_1
inst✝³ : Lattice G
inst✝² : AddGroup G
inst✝¹ : CovariantClass G G (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass G G (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
S : AddSubgroup G
a : G
ha : MetaClosure (fun x => x ∈ S) a
a✝ b✝ : G
x✝¹ : MetaClosure (fun x => x ∈ S) a✝
x✝ : MetaClosure (fun x => x ∈ S) b✝
⊢ MetaClosure (fun x => x ∈ S) (-a✝) → MetaClosure (fun x => x ∈ S) (-b✝) → MetaClosure (fun x => x ∈ S) (-a✝ ⊓ -b✝)
Tactic:
exact ofInf
Proof state after:
no goals
Theorem: IMOSL.IMO2010A6.lem1
Proof state before:
f g : ℕ → ℕ
h : good f g
⊢ ∃ a, ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
Tactic:
have h0 : ∃ n, ∃ x, f x = n := ⟨f 0, 0, rfl⟩
Proof state after:
f g : ℕ → ℕ
h : good f g
h0 : ∃ n x, f x = n
⊢ ∃ a, ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
Theorem: IMOSL.IMO2010A6.lem1
Proof state before:
f g : ℕ → ℕ
h : good f g
h0 : ∃ n x, f x = n
⊢ ∃ a, ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
Tactic:
refine ⟨Nat.find h0, λ k ↦
  ⟨Nat.find_min' h0, Nat.le_induction (Nat.find_spec h0) ?_ k⟩⟩
Proof state after:
f g : ℕ → ℕ
h : good f g
h0 : ∃ n x, f x = n
k : ℕ
⊢ ∀ (n : ℕ), Nat.find h0 ≤ n → (∃ x, f x = n) → ∃ x, f x = n + 1
Theorem: IMOSL.IMO2010A6.lem1
Proof state before:
f g : ℕ → ℕ
h : good f g
h0 : ∃ n x, f x = n
k : ℕ
⊢ ∀ (n : ℕ), Nat.find h0 ≤ n → (∃ x, f x = n) → ∃ x, f x = n + 1
Tactic:
rintro n h1 ⟨x, rfl⟩
Proof state after:
case intro
f g : ℕ → ℕ
h : good f g
h0 : ∃ n x, f x = n
k x : ℕ
h1 : Nat.find h0 ≤ f x
⊢ ∃ x_1, f x_1 = f x + 1
Theorem: IMOSL.IMO2010A6.lem1
Proof state before:
case intro
f g : ℕ → ℕ
h : good f g
h0 : ∃ n x, f x = n
k x : ℕ
h1 : Nat.find h0 ≤ f x
⊢ ∃ x_1, f x_1 = f x + 1
Tactic:
exact ⟨g x, h x⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2010A6.lem4
Proof state before:
f g : ℕ → ℕ
h : good f g
h0 : good g f
k m : ℕ
h1 : ∃ x, f x = k
h2 : ∃ y, f y = m
h3 : f k = f m
⊢ k = m
Tactic:
rcases h1 with ⟨x, rfl⟩
Proof state after:
case intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
m : ℕ
h2 : ∃ y, f y = m
x : ℕ
h3 : f (f x) = f m
⊢ f x = m
Theorem: IMOSL.IMO2010A6.lem4
Proof state before:
case intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
m : ℕ
h2 : ∃ y, f y = m
x : ℕ
h3 : f (f x) = f m
⊢ f x = m
Tactic:
rcases h2 with ⟨y, rfl⟩
Proof state after:
case intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
x y : ℕ
h3 : f (f x) = f (f y)
⊢ f x = f y
Theorem: IMOSL.IMO2010A6.lem4
Proof state before:
case intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
x y : ℕ
h3 : f (f x) = f (f y)
⊢ f x = f y
Tactic:
replace h3 := lem2 h0 h3
Proof state after:
case intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
x y : ℕ
h3 : g (f x) = g (f y)
⊢ f x = f y
Theorem: IMOSL.IMO2010A6.lem4
Proof state before:
case intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
x y : ℕ
h3 : g (f x) = g (f y)
⊢ f x = f y
Tactic:
rw [h0, h0, Nat.succ_inj'] at h3
Proof state after:
case intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
x y : ℕ
h3 : g x = g y
⊢ f x = f y
Theorem: IMOSL.IMO2010A6.lem4
Proof state before:
case intro.intro
f g : ℕ → ℕ
h : good f g
h0 : good g f
x y : ℕ
h3 : g x = g y
⊢ f x = f y
Tactic:
exact lem2 h h3
Proof state after:
no goals
Theorem: IMOSL.IMO2010A6.lem5
Proof state before:
f g : ℕ → ℕ
h : good f g
h0 : good g f
a b : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ b ≤ k
⊢ a = b
Tactic:
wlog h3 : a ≤ b
Proof state after:
case inr
f g : ℕ → ℕ
h : good f g
h0 : good g f
a b : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ b ≤ k
this :
  ∀ {f g : ℕ → ℕ},
    good f g →
      good g f → ∀ {a b : ℕ}, (∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k) → (∀ (k : ℕ), (∃ x, g x = k) ↔ b ≤ k) → a ≤ b → a = b
h3 : ¬a ≤ b
⊢ a = b

f✝ g✝ f g : ℕ → ℕ
h : good f g
h0 : good g f
a b : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ b ≤ k
h3 : a ≤ b
⊢ a = b
Theorem: IMOSL.IMO2010A6.lem5
Proof state before:
f✝ g✝ f g : ℕ → ℕ
h : good f g
h0 : good g f
a b : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ b ≤ k
h3 : a ≤ b
⊢ a = b
Tactic:
refine h3.antisymm ((h2 _).mp ?_)
Proof state after:
f✝ g✝ f g : ℕ → ℕ
h : good f g
h0 : good g f
a b : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ b ≤ k
h3 : a ≤ b
⊢ ∃ x, g x = a
Theorem: IMOSL.IMO2010A6.lem5
Proof state before:
f✝ g✝ f g : ℕ → ℕ
h : good f g
h0 : good g f
a b : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ b ≤ k
h3 : a ≤ b
⊢ ∃ x, g x = a
Tactic:
obtain ⟨k, h4⟩ := Nat.exists_eq_add_of_le (lem3 h0 h1)
Proof state after:
case intro
f✝ g✝ f g : ℕ → ℕ
h : good f g
h0 : good g f
a b : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ b ≤ k
h3 : a ≤ b
k : ℕ
h4 : f a = a.succ + k
⊢ ∃ x, g x = a
Theorem: IMOSL.IMO2010A6.lem5
Proof state before:
case intro
f✝ g✝ f g : ℕ → ℕ
h : good f g
h0 : good g f
a b : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ b ≤ k
h3 : a ≤ b
k : ℕ
h4 : f a = a.succ + k
⊢ ∃ x, g x = a
Tactic:
obtain ⟨d, h5⟩ := (h1 (a + k)).mpr (a.le_add_right k)
Proof state after:
case intro.intro
f✝ g✝ f g : ℕ → ℕ
h : good f g
h0 : good g f
a b : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ b ≤ k
h3 : a ≤ b
k : ℕ
h4 : f a = a.succ + k
d : ℕ
h5 : f d = a + k
⊢ ∃ x, g x = a
Theorem: IMOSL.IMO2010A6.lem5
Proof state before:
case intro.intro
f✝ g✝ f g : ℕ → ℕ
h : good f g
h0 : good g f
a b : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ b ≤ k
h3 : a ≤ b
k : ℕ
h4 : f a = a.succ + k
d : ℕ
h5 : f d = a + k
⊢ ∃ x, g x = a
Tactic:
rw [Nat.succ_add, ← h5, ← h, eq_comm] at h4
Proof state after:
case intro.intro
f✝ g✝ f g : ℕ → ℕ
h : good f g
h0 : good g f
a b : ℕ
h1 : ∀ (k : ℕ), (∃ x, f x = k) ↔ a ≤ k
h2 : ∀ (k : ℕ), (∃ x, g x = k) ↔ b ≤ k
h3 : a ≤ b
k d : ℕ
h4 : f (g d) = f a
h5 : f d = a + k
⊢ ∃ x, g x = a