internlm/Lean-Github huggingface dataset:
Theorem: EStateM.SatisfiesM_EStateM_eq
Proof state before:
ε σ α : Type u
p : α → Prop
x : EStateM ε σ α
hx : SatisfiesM p x
s : σ
a : α
x✝ : σ
⊢ x s = Result.ok a x✝ → p a
Tactic:
cases hx with | intro w hw =>
cases hw
dsimp [Functor.map, EStateM.map]
cases w s <;> intro h
case ok a s' => exact (Result.ok.inj h).left ▸ a.property
case error e s' => cases h
Proof state after:
no goals
Theorem: EStateM.SatisfiesM_EStateM_eq
Proof state before:
case intro
ε σ α : Type u
p : α → Prop
x : EStateM ε σ α
s : σ
a : α
x✝ : σ
w : EStateM ε σ { a // p a }
hw : Subtype.val <$> w = x
⊢ x s = Result.ok a x✝ → p a
Tactic:
cases hw
Proof state after:
case intro.refl
ε σ α : Type u
p : α → Prop
s : σ
a : α
x✝ : σ
w : EStateM ε σ { a // p a }
⊢ (Subtype.val <$> w) s = Result.ok a x✝ → p a
Theorem: EStateM.SatisfiesM_EStateM_eq
Proof state before:
case intro.refl
ε σ α : Type u
p : α → Prop
s : σ
a : α
x✝ : σ
w : EStateM ε σ { a // p a }
⊢ (Subtype.val <$> w) s = Result.ok a x✝ → p a
Tactic:
dsimp [Functor.map, EStateM.map]
Proof state after:
case intro.refl
ε σ α : Type u
p : α → Prop
s : σ
a : α
x✝ : σ
w : EStateM ε σ { a // p a }
⊢ (match w s with
      | Result.ok a s => Result.ok a.val s
      | Result.error e s => Result.error e s) =
      Result.ok a x✝ →
    p a
Theorem: EStateM.SatisfiesM_EStateM_eq
Proof state before:
case intro.refl
ε σ α : Type u
p : α → Prop
s : σ
a : α
x✝ : σ
w : EStateM ε σ { a // p a }
⊢ (match w s with
      | Result.ok a s => Result.ok a.val s
      | Result.error e s => Result.error e s) =
      Result.ok a x✝ →
    p a
Tactic:
cases w s <;> intro h
Proof state after:
case intro.refl.ok
ε σ α : Type u
p : α → Prop
s : σ
a : α
x✝ : σ
w : EStateM ε σ { a // p a }
a✝¹ : { a // p a }
a✝ : σ
h :
  (match Result.ok a✝¹ a✝ with
    | Result.ok a s => Result.ok a.val s
    | Result.error e s => Result.error e s) =
    Result.ok a x✝
⊢ p a

case intro.refl.error
ε σ α : Type u
p : α → Prop
s : σ
a : α
x✝ : σ
w : EStateM ε σ { a // p a }
a✝¹ : ε
a✝ : σ
h :
  (match Result.error a✝¹ a✝ with
    | Result.ok a s => Result.ok a.val s
    | Result.error e s => Result.error e s) =
    Result.ok a x✝
⊢ p a
Theorem: EStateM.SatisfiesM_EStateM_eq
Proof state before:
ε σ α : Type u
p : α → Prop
s : σ
a✝ : α
x✝ : σ
w : EStateM ε σ { a // p a }
a : { a // p a }
s' : σ
h :
  (match Result.ok a s' with
    | Result.ok a s => Result.ok a.val s
    | Result.error e s => Result.error e s) =
    Result.ok a✝ x✝
⊢ p a✝
Tactic:
case ok a s' => exact (Result.ok.inj h).left ▸ a.property
Proof state after:
no goals
Theorem: EStateM.SatisfiesM_EStateM_eq
Proof state before:
ε σ α : Type u
p : α → Prop
s : σ
a : α
x✝ : σ
w : EStateM ε σ { a // p a }
e : ε
s' : σ
h :
  (match Result.error e s' with
    | Result.ok a s => Result.ok a.val s
    | Result.error e s => Result.error e s) =
    Result.ok a x✝
⊢ p a
Tactic:
case error e s' => cases h
Proof state after:
no goals
Theorem: EStateM.SatisfiesM_EStateM_eq
Proof state before:
ε σ α : Type u
p : α → Prop
s : σ
a✝ : α
x✝ : σ
w : EStateM ε σ { a // p a }
a : { a // p a }
s' : σ
h :
  (match Result.ok a s' with
    | Result.ok a s => Result.ok a.val s
    | Result.error e s => Result.error e s) =
    Result.ok a✝ x✝
⊢ p a✝
Tactic:
exact (Result.ok.inj h).left ▸ a.property
Proof state after:
no goals
Theorem: EStateM.SatisfiesM_EStateM_eq
Proof state before:
ε σ α : Type u
p : α → Prop
s : σ
a : α
x✝ : σ
w : EStateM ε σ { a // p a }
e : ε
s' : σ
h :
  (match Result.error e s' with
    | Result.ok a s => Result.ok a.val s
    | Result.error e s => Result.error e s) =
    Result.ok a x✝
⊢ p a
Tactic:
cases h
Proof state after:
no goals
Theorem: EStateM.SatisfiesM_EStateM_eq
Proof state before:
ε σ α : Type u
p : α → Prop
x : EStateM ε σ α
h : ∀ (s : σ) (a : α) (s' : σ), x s = Result.ok a s' → p a
⊢ SatisfiesM p x
Tactic:
exists λ s => (x s).zipProof (h s)
Proof state after:
ε σ α : Type u
p : α → Prop
x : EStateM ε σ α
h : ∀ (s : σ) (a : α) (s' : σ), x s = Result.ok a s' → p a
⊢ (Subtype.val <$> fun s => Result.zipProof (x s) (_ : ∀ (a : α) (s' : σ), x s = Result.ok a s' → p a)) = x
Theorem: EStateM.SatisfiesM_EStateM_eq
Proof state before:
ε σ α : Type u
p : α → Prop
x : EStateM ε σ α
h : ∀ (s : σ) (a : α) (s' : σ), x s = Result.ok a s' → p a
⊢ (Subtype.val <$> fun s => Result.zipProof (x s) (_ : ∀ (a : α) (s' : σ), x s = Result.ok a s' → p a)) = x
Tactic:
funext s
Proof state after:
case h
ε σ α : Type u
p : α → Prop
x : EStateM ε σ α
h : ∀ (s : σ) (a : α) (s' : σ), x s = Result.ok a s' → p a
s : σ
⊢ (Subtype.val <$> fun s => Result.zipProof (x s) (_ : ∀ (a : α) (s' : σ), x s = Result.ok a s' → p a)) s = x s
Theorem: EStateM.SatisfiesM_EStateM_eq
Proof state before:
case h
ε σ α : Type u
p : α → Prop
x : EStateM ε σ α
h : ∀ (s : σ) (a : α) (s' : σ), x s = Result.ok a s' → p a
s : σ
⊢ (Subtype.val <$> fun s => Result.zipProof (x s) (_ : ∀ (a : α) (s' : σ), x s = Result.ok a s' → p a)) s = x s
Tactic:
dsimp [Functor.map, EStateM.map]
Proof state after:
case h
ε σ α : Type u
p : α → Prop
x : EStateM ε σ α
h : ∀ (s : σ) (a : α) (s' : σ), x s = Result.ok a s' → p a
s : σ
⊢ (match Result.zipProof (x s) (_ : ∀ (a : α) (s' : σ), x s = Result.ok a s' → p a) with
    | Result.ok a s => Result.ok a.val s
    | Result.error e s => Result.error e s) =
    x s
Theorem: EStateM.SatisfiesM_EStateM_eq
Proof state before:
case h
ε σ α : Type u
p : α → Prop
x : EStateM ε σ α
h : ∀ (s : σ) (a : α) (s' : σ), x s = Result.ok a s' → p a
s : σ
⊢ (match Result.zipProof (x s) (_ : ∀ (a : α) (s' : σ), x s = Result.ok a s' → p a) with
    | Result.ok a s => Result.ok a.val s
    | Result.error e s => Result.error e s) =
    x s
Tactic:
conv =>
  lhs; change Result.map (Subtype.val (p:=p)) ((x s).zipProof (h s))
  rw [Result.map_val_zipProof]
Proof state after:
no goals
Theorem: SubtypeT.deq_of_iff
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
p q : Pred α
hpq : ∀ (a : α), p a ↔ q a
⊢ ∀ (x : SubtypeT m α p), DEq (SubtypeT m α) x (weaken (_ : ∀ (a : α), p a → q a) x)
Tactic:
have : p = q := funext (λ a => propext (hpq a))
Proof state after:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
p q : Pred α
hpq : ∀ (a : α), p a ↔ q a
this : p = q
⊢ ∀ (x : SubtypeT m α p), DEq (SubtypeT m α) x (weaken (_ : ∀ (a : α), p a → q a) x)
Theorem: SubtypeT.deq_of_iff
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
p q : Pred α
hpq : ∀ (a : α), p a ↔ q a
this : p = q
⊢ ∀ (x : SubtypeT m α p), DEq (SubtypeT m α) x (weaken (_ : ∀ (a : α), p a → q a) x)
Tactic:
cases this
Proof state after:
case refl
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
p : Pred α
hpq : ∀ (a : α), p a ↔ p a
⊢ ∀ (x : SubtypeT m α p), DEq (SubtypeT m α) x (weaken (_ : ∀ (a : α), p a → p a) x)
Theorem: SubtypeT.deq_of_iff
Proof state before:
case refl
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
p : Pred α
hpq : ∀ (a : α), p a ↔ p a
⊢ ∀ (x : SubtypeT m α p), DEq (SubtypeT m α) x (weaken (_ : ∀ (a : α), p a → p a) x)
Tactic:
intro x
Proof state after:
case refl
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
p : Pred α
hpq : ∀ (a : α), p a ↔ p a
x : SubtypeT m α p
⊢ DEq (SubtypeT m α) x (weaken (_ : ∀ (a : α), p a → p a) x)
Theorem: SubtypeT.deq_of_iff
Proof state before:
case refl
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
p : Pred α
hpq : ∀ (a : α), p a ↔ p a
x : SubtypeT m α p
⊢ DEq (SubtypeT m α) x (weaken (_ : ∀ (a : α), p a → p a) x)
Tactic:
apply DEq.deq_of_eq
Proof state after:
case refl.a
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
p : Pred α
hpq : ∀ (a : α), p a ↔ p a
x : SubtypeT m α p
⊢ x = weaken (_ : ∀ (a : α), p a → p a) x
Theorem: SubtypeT.deq_of_iff
Proof state before:
case refl.a
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
p : Pred α
hpq : ∀ (a : α), p a ↔ p a
x : SubtypeT m α p
⊢ x = weaken (_ : ∀ (a : α), p a → p a) x
Tactic:
conv =>
  rhs; dsimp [weaken]; congr
  . skip
  . ext a; change pure a
Proof state after:
case refl.a
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
p : Pred α
hpq : ∀ (a : α), p a ↔ p a
x : SubtypeT m α p
⊢ x = do
    let a ← x
    pure a
Theorem: SubtypeT.deq_of_iff
Proof state before:
case refl.a
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
p : Pred α
hpq : ∀ (a : α), p a ↔ p a
x : SubtypeT m α p
⊢ x = do
    let a ← x
    pure a
Tactic:
rw [bind_pure]
Proof state after:
no goals
Theorem: MonadHom.ext
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
n : Type u → Type w
inst✝ : Monad n
F G : MonadHom m n
h : ∀ {α : Type u} (x : m α), app F x = app G x
⊢ F = G
Tactic:
apply MonadHom.eq (m:=m)
Proof state after:
m : Type u → Type v
inst✝¹ : Monad m
n : Type u → Type w
inst✝ : Monad n
F G : MonadHom m n
h : ∀ {α : Type u} (x : m α), app F x = app G x
⊢ F.app = G.app
Theorem: MonadHom.ext
Proof state before:
m : Type u → Type v
inst✝¹ : Monad m
n : Type u → Type w
inst✝ : Monad n
F G : MonadHom m n
h : ∀ {α : Type u} (x : m α), app F x = app G x
⊢ F.app = G.app
Tactic:
funext _ x
Proof state after:
case h.h
m : Type u → Type v
inst✝¹ : Monad m
n : Type u → Type w
inst✝ : Monad n
F G : MonadHom m n
h : ∀ {α : Type u} (x : m α), app F x = app G x
x✝ : Type u
x : m x✝
⊢ app F x = app G x
Theorem: MonadHom.ext
Proof state before:
case h.h
m : Type u → Type v
inst✝¹ : Monad m
n : Type u → Type w
inst✝ : Monad n
F G : MonadHom m n
h : ∀ {α : Type u} (x : m α), app F x = app G x
x✝ : Type u
x : m x✝
⊢ app F x = app G x
Tactic:
exact h x
Proof state after:
no goals
Theorem: MonadHom.naturality
Proof state before:
m : Type u → Type v
inst✝³ : Monad m
inst✝² : LawfulMonad m
n : Type u → Type w
inst✝¹ : Monad n
inst✝ : LawfulMonad n
F : MonadHom m n
α β : Type u
f : α → β
⊢ app F ∘ Functor.map f = Functor.map f ∘ app F
Tactic:
funext x
Proof state after:
case h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : LawfulMonad m
n : Type u → Type w
inst✝¹ : Monad n
inst✝ : LawfulMonad n
F : MonadHom m n
α β : Type u
f : α → β
x : m α
⊢ (app F ∘ Functor.map f) x = (Functor.map f ∘ app F) x
Theorem: MonadHom.naturality
Proof state before:
case h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : LawfulMonad m
n : Type u → Type w
inst✝¹ : Monad n
inst✝ : LawfulMonad n
F : MonadHom m n
α β : Type u
f : α → β
x : m α
⊢ (app F ∘ Functor.map f) x = (Functor.map f ∘ app F) x
Tactic:
dsimp
Proof state after:
case h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : LawfulMonad m
n : Type u → Type w
inst✝¹ : Monad n
inst✝ : LawfulMonad n
F : MonadHom m n
α β : Type u
f : α → β
x : m α
⊢ app F (f <$> x) = f <$> app F x
Theorem: MonadHom.naturality
Proof state before:
case h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : LawfulMonad m
n : Type u → Type w
inst✝¹ : Monad n
inst✝ : LawfulMonad n
F : MonadHom m n
α β : Type u
f : α → β
x : m α
⊢ app F (f <$> x) = f <$> app F x
Tactic:
conv =>
  lhs; rw [map_eq_pure_bind, F.app_bind]; rhs; ext a; dsimp; rw [F.app_pure]
Proof state after:
case h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : LawfulMonad m
n : Type u → Type w
inst✝¹ : Monad n
inst✝ : LawfulMonad n
F : MonadHom m n
α β : Type u
f : α → β
x : m α
⊢ (do
      let a ← app F x
      pure (f a)) =
    f <$> app F x
Theorem: MonadHom.naturality
Proof state before:
case h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : LawfulMonad m
n : Type u → Type w
inst✝¹ : Monad n
inst✝ : LawfulMonad n
F : MonadHom m n
α β : Type u
f : α → β
x : m α
⊢ (do
      let a ← app F x
      pure (f a)) =
    f <$> app F x
Tactic:
rw [map_eq_pure_bind]
Proof state after:
no goals
Theorem: IMOSL.Extra.NatSeq_antitone_imp_const
Proof state before:
a : ℕ → ℕ
ha : Antitone a
⊢ ∃ C N, ∀ (n : ℕ), a (n + N) = C
Tactic:
by_contra h
Proof state after:
a : ℕ → ℕ
ha : Antitone a
h : ¬∃ C N, ∀ (n : ℕ), a (n + N) = C
⊢ False
Theorem: IMOSL.Extra.NatSeq_antitone_imp_const
Proof state before:
a : ℕ → ℕ
ha : Antitone a
h : ¬∃ C N, ∀ (n : ℕ), a (n + N) = C
⊢ False
Tactic:
simp only [not_exists, not_forall] at h
Proof state after:
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
⊢ False
Theorem: IMOSL.Extra.NatSeq_antitone_imp_const
Proof state before:
a : ℕ → ℕ
ha : Antitone a
h : ∀ (C : ℕ), ∃ N, ∀ (n : ℕ), a (n + N) + C ≤ a 0
⊢ False
Tactic:
rcases h (a 0).succ with ⟨N, h⟩
Proof state after:
case intro
a : ℕ → ℕ
ha : Antitone a
h✝ : ∀ (C : ℕ), ∃ N, ∀ (n : ℕ), a (n + N) + C ≤ a 0
N : ℕ
h : ∀ (n : ℕ), a (n + N) + (a 0).succ ≤ a 0
⊢ False
Theorem: IMOSL.Extra.NatSeq_antitone_imp_const
Proof state before:
case intro
a : ℕ → ℕ
ha : Antitone a
h✝ : ∀ (C : ℕ), ∃ N, ∀ (n : ℕ), a (n + N) + C ≤ a 0
N : ℕ
h : ∀ (n : ℕ), a (n + N) + (a 0).succ ≤ a 0
⊢ False
Tactic:
exact (h 0).not_lt (Nat.lt_add_left _ (a 0).lt_succ_self)
Proof state after:
no goals
Theorem: IMOSL.Extra.NatSeq_antitone_imp_const
Proof state before:
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C : ℕ
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + C ≤ a 0
Tactic:
induction' C with C hC
Proof state after:
case zero
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + 0 ≤ a 0

case succ
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C : ℕ
hC : ∃ N, ∀ (n : ℕ), a (n + N) + C ≤ a 0
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + (C + 1) ≤ a 0
Theorem: IMOSL.Extra.NatSeq_antitone_imp_const
Proof state before:
case zero
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + 0 ≤ a 0
Tactic:
exact ⟨0, λ n ↦ ha n.zero_le⟩
Proof state after:
no goals
Theorem: IMOSL.Extra.NatSeq_antitone_imp_const
Proof state before:
case succ
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C : ℕ
hC : ∃ N, ∀ (n : ℕ), a (n + N) + C ≤ a 0
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + (C + 1) ≤ a 0
Tactic:
rcases hC with ⟨N, hC⟩
Proof state after:
case succ.intro
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + (C + 1) ≤ a 0
Theorem: IMOSL.Extra.NatSeq_antitone_imp_const
Proof state before:
case succ.intro
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + (C + 1) ≤ a 0
Tactic:
rcases (hC 0).lt_or_eq with h0 | h0
Proof state after:
case succ.intro.inl
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C < a 0
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + (C + 1) ≤ a 0

case succ.intro.inr
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C = a 0
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + (C + 1) ≤ a 0
Theorem: IMOSL.Extra.NatSeq_antitone_imp_const
Proof state before:
case succ.intro.inl
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C < a 0
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + (C + 1) ≤ a 0
Tactic:
refine ⟨N, λ n ↦ h0.trans_le' (Nat.add_le_add_right (ha ?_) C)⟩
Proof state after:
case succ.intro.inl
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C < a 0
n : ℕ
⊢ 0 + N ≤ n + N
Theorem: IMOSL.Extra.NatSeq_antitone_imp_const
Proof state before:
case succ.intro.inl
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C < a 0
n : ℕ
⊢ 0 + N ≤ n + N
Tactic:
exact Nat.add_le_add_right n.zero_le N
Proof state after:
no goals
Theorem: IMOSL.Extra.NatSeq_antitone_imp_const
Proof state before:
case succ.intro.inr
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C = a 0
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + (C + 1) ≤ a 0
Tactic:
rcases h (a 0 - C) N with ⟨K, h1⟩
Proof state after:
case succ.intro.inr.intro
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C = a 0
K : ℕ
h1 : ¬a (K + N) = a 0 - C
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + (C + 1) ≤ a 0
Theorem: IMOSL.Extra.NatSeq_antitone_imp_const
Proof state before:
case succ.intro.inr.intro
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C = a 0
K : ℕ
h1 : ¬a (K + N) = a 0 - C
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + (C + 1) ≤ a 0
Tactic:
rw [← h0, Nat.add_sub_cancel, Nat.zero_add] at h1
Proof state after:
case succ.intro.inr.intro
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C = a 0
K : ℕ
h1 : ¬a (K + N) = a N
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + (C + 1) ≤ a 0
Theorem: IMOSL.Extra.NatSeq_antitone_imp_const
Proof state before:
case succ.intro.inr.intro
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C = a 0
K : ℕ
h1 : ¬a (K + N) = a N
⊢ ∃ N, ∀ (n : ℕ), a (n + N) + (C + 1) ≤ a 0
Tactic:
refine ⟨K + N, λ n ↦ Nat.add_one_le_iff.mpr ?_⟩
Proof state after:
case succ.intro.inr.intro
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C = a 0
K : ℕ
h1 : ¬a (K + N) = a N
n : ℕ
⊢ (a (n + (K + N))).add C < a 0
Theorem: IMOSL.Extra.NatSeq_antitone_imp_const
Proof state before:
case succ.intro.inr.intro
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C = a 0
K : ℕ
h1 : ¬a (K + N) = a N
n : ℕ
⊢ (a (n + (K + N))).add C < a 0
Tactic:
rw [← h0, Nat.zero_add]
Proof state after:
case succ.intro.inr.intro
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C = a 0
K : ℕ
h1 : ¬a (K + N) = a N
n : ℕ
⊢ (a (n + (K + N))).add C < a N + C
Theorem: IMOSL.Extra.NatSeq_antitone_imp_const
Proof state before:
case succ.intro.inr.intro
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C = a 0
K : ℕ
h1 : ¬a (K + N) = a N
n : ℕ
⊢ (a (n + (K + N))).add C < a N + C
Tactic:
refine Nat.add_lt_add_right ((ha <| (K + N).le_add_left n).trans_lt ?_) C
Proof state after:
case succ.intro.inr.intro
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C = a 0
K : ℕ
h1 : ¬a (K + N) = a N
n : ℕ
⊢ a (K + N) < a N
Theorem: IMOSL.Extra.NatSeq_antitone_imp_const
Proof state before:
case succ.intro.inr.intro
a : ℕ → ℕ
ha : Antitone a
h : ∀ (x x_1 : ℕ), ∃ x_2, ¬a (x_2 + x_1) = x
C N : ℕ
hC : ∀ (n : ℕ), a (n + N) + C ≤ a 0
h0 : a (0 + N) + C = a 0
K : ℕ
h1 : ¬a (K + N) = a N
n : ℕ
⊢ a (K + N) < a N
Tactic:
exact (ha (N.le_add_left K)).lt_of_ne h1
Proof state after:
no goals
Theorem: IMOSL.IMO2011A4.main_step
Proof state before:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
h0 : ∀ (n : ℕ), n ≤ f n
⊢ f = id
Tactic:
have h1 : ∀ t n, n ≤ f^[t] n :=
  Nat.rec Nat.le_refl λ t h1 n ↦ (h0 n).trans (h1 _)
Proof state after:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
h0 : ∀ (n : ℕ), n ≤ f n
h1 : ∀ (t n : ℕ), n ≤ f^[t] n
⊢ f = id
Theorem: IMOSL.IMO2011A4.main_step
Proof state before:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
h0 : ∀ (n : ℕ), n ≤ f n
h1 : ∀ (t n : ℕ), n ≤ f^[t] n
⊢ f = id
Tactic:
have h2 : StrictMono f :=
  strictMono_nat_of_lt_succ λ n ↦ (h1 _ (f n)).trans_lt (h n)
Proof state after:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
h0 : ∀ (n : ℕ), n ≤ f n
h1 : ∀ (t n : ℕ), n ≤ f^[t] n
h2 : StrictMono f
⊢ f = id
Theorem: IMOSL.IMO2011A4.main_step
Proof state before:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
h0 : ∀ (n : ℕ), n ≤ f n
h1 : ∀ (t n : ℕ), n ≤ f^[t] n
h2 : StrictMono f
⊢ f = id
Tactic:
refine funext λ n ↦ (h0 n).antisymm' ?_
Proof state after:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
h0 : ∀ (n : ℕ), n ≤ f n
h1 : ∀ (t n : ℕ), n ≤ f^[t] n
h2 : StrictMono f
n : ℕ
⊢ f n ≤ n
Theorem: IMOSL.IMO2011A4.main_step
Proof state before:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
h0 : ∀ (n : ℕ), n ≤ f n
h1 : ∀ (t n : ℕ), n ≤ f^[t] n
h2 : StrictMono f
n : ℕ
⊢ f n ≤ n
Tactic:
rw [← Nat.lt_succ_iff, ← h2.lt_iff_lt]
Proof state after:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
h0 : ∀ (n : ℕ), n ≤ f n
h1 : ∀ (t n : ℕ), n ≤ f^[t] n
h2 : StrictMono f
n : ℕ
⊢ f (f n) < f n.succ
Theorem: IMOSL.IMO2011A4.main_step
Proof state before:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
h0 : ∀ (n : ℕ), n ≤ f n
h1 : ∀ (t n : ℕ), n ≤ f^[t] n
h2 : StrictMono f
n : ℕ
⊢ f (f n) < f n.succ
Tactic:
exact (h1 _ _).trans_lt (h n)
Proof state after:
no goals
Theorem: IMOSL.IMO2011A4.main_step
Proof state before:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
⊢ ∀ (n : ℕ), n ≤ f n
Tactic:
suffices ∀ k n : ℕ, k ≤ n → k ≤ f n from λ n ↦ this n n n.le_refl
Proof state after:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
⊢ ∀ (k n : ℕ), k ≤ n → k ≤ f n
Theorem: IMOSL.IMO2011A4.main_step
Proof state before:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
⊢ ∀ (k n : ℕ), k ≤ n → k ≤ f n
Tactic:
refine Nat.rec (λ k _ ↦ (f k).zero_le) (λ k h0 n h1 ↦ ?_)
Proof state after:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
k : ℕ
h0 : ∀ (n : ℕ), k ≤ n → k ≤ f n
n : ℕ
h1 : k.succ ≤ n
⊢ k.succ ≤ f n
Theorem: IMOSL.IMO2011A4.main_step
Proof state before:
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
k : ℕ
h0 : ∀ (n : ℕ), k ≤ n → k ≤ f n
n : ℕ
h1 : k.succ ≤ n
⊢ k.succ ≤ f n
Tactic:
rcases n with _ | n
Proof state after:
case zero
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
k : ℕ
h0 : ∀ (n : ℕ), k ≤ n → k ≤ f n
h1 : k.succ ≤ 0
⊢ k.succ ≤ f 0

case succ
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
k : ℕ
h0 : ∀ (n : ℕ), k ≤ n → k ≤ f n
n : ℕ
h1 : k.succ ≤ n + 1
⊢ k.succ ≤ f (n + 1)
Theorem: IMOSL.IMO2011A4.main_step
Proof state before:
case zero
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
k : ℕ
h0 : ∀ (n : ℕ), k ≤ n → k ≤ f n
h1 : k.succ ≤ 0
⊢ k.succ ≤ f 0
Tactic:
exact absurd k.succ_pos h1.not_lt
Proof state after:
no goals
Theorem: IMOSL.IMO2011A4.main_step
Proof state before:
case succ
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
k : ℕ
h0 : ∀ (n : ℕ), k ≤ n → k ≤ f n
n : ℕ
h1 : k.succ ≤ n + 1
⊢ k.succ ≤ f (n + 1)
Tactic:
refine (h n).trans_le' ?_
Proof state after:
case succ
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
k : ℕ
h0 : ∀ (n : ℕ), k ≤ n → k ≤ f n
n : ℕ
h1 : k.succ ≤ n + 1
⊢ k ≤ f^[g n + 2] n
Theorem: IMOSL.IMO2011A4.main_step
Proof state before:
case succ
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
k : ℕ
h0 : ∀ (n : ℕ), k ≤ n → k ≤ f n
n : ℕ
h1 : k.succ ≤ n + 1
⊢ k ≤ f^[g n + 2] n
Tactic:
generalize g n + 2 = t
Proof state after:
case succ
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
k : ℕ
h0 : ∀ (n : ℕ), k ≤ n → k ≤ f n
n : ℕ
h1 : k.succ ≤ n + 1
t : ℕ
⊢ k ≤ f^[t] n
Theorem: IMOSL.IMO2011A4.main_step
Proof state before:
case succ
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k < f (k + 1)
k : ℕ
h0 : ∀ (n : ℕ), k ≤ n → k ≤ f n
n : ℕ
h1 : k.succ ≤ n + 1
t : ℕ
⊢ k ≤ f^[t] n
Tactic:
exact t.rec (Nat.succ_le_succ_iff.mp h1)
  (λ t h2 ↦ (h0 _ h2).trans_eq (f.iterate_succ_apply' _ _).symm)
Proof state after:
no goals
Theorem: IMOSL.IMO2011A4.final_solution
Proof state before:
f g : ℕ → ℕ
⊢ (∀ (k : ℕ), f^[g k + 2] k + (g^[f k + 1] k + g (k + 1)) + 1 = f (k + 1)) ↔ f = id ∧ g = fun x => 0
Tactic:
refine Iff.symm ⟨λ h k ↦ ?_, λ h ↦ ?_⟩
Proof state after:
case refine_1
f g : ℕ → ℕ
h : f = id ∧ g = fun x => 0
k : ℕ
⊢ f^[g k + 2] k + (g^[f k + 1] k + g (k + 1)) + 1 = f (k + 1)

case refine_2
f g : ℕ → ℕ
h : ∀ (k : ℕ), f^[g k + 2] k + (g^[f k + 1] k + g (k + 1)) + 1 = f (k + 1)
⊢ f = id ∧ g = fun x => 0
Theorem: IMOSL.IMO2011A4.final_solution
Proof state before:
case refine_1
f g : ℕ → ℕ
h : f = id ∧ g = fun x => 0
k : ℕ
⊢ f^[g k + 2] k + (g^[f k + 1] k + g (k + 1)) + 1 = f (k + 1)
Tactic:
rcases h with ⟨rfl, rfl⟩
Proof state after:
case refine_1.intro
k : ℕ
⊢ id^[(fun x => 0) k + 2] k + ((fun x => 0)^[id k + 1] k + (fun x => 0) (k + 1)) + 1 = id (k + 1)