internlm/Lean-Github huggingface dataset:
Theorem: Category.NatTrans.id_comp
Proof state before:
case app.h
α : Type u_1
β : Type u_2
γ : Type ?u.76228
δ : Type ?u.76231
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F G : α ⥤ β
η : NatTrans F G
x✝ : α
⊢ app (comp (id G) η) x✝ = app η x✝
Tactic:
simp
Proof state after:
no goals
Theorem: Category.NatTrans.comp_id
Proof state before:
α : Type u_1
β : Type u_2
γ : Type ?u.76679
δ : Type ?u.76682
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F G : α ⥤ β
η : NatTrans F G
⊢ comp η (id F) = η
Tactic:
ext
Proof state after:
case app.h
α : Type u_1
β : Type u_2
γ : Type ?u.76679
δ : Type ?u.76682
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F G : α ⥤ β
η : NatTrans F G
x✝ : α
⊢ app (comp η (id F)) x✝ = app η x✝
Theorem: Category.NatTrans.comp_id
Proof state before:
case app.h
α : Type u_1
β : Type u_2
γ : Type ?u.76679
δ : Type ?u.76682
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F G : α ⥤ β
η : NatTrans F G
x✝ : α
⊢ app (comp η (id F)) x✝ = app η x✝
Tactic:
simp
Proof state after:
no goals
Theorem: Category.NatTrans.comp_assoc
Proof state before:
α : Type u_1
β : Type u_2
γ : Type ?u.77130
δ : Type ?u.77133
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F G H K : α ⥤ β
η₁ : NatTrans H K
η₂ : NatTrans G H
η₃ : NatTrans F G
⊢ comp (comp η₁ η₂) η₃ = comp η₁ (comp η₂ η₃)
Tactic:
ext
Proof state after:
case app.h
α : Type u_1
β : Type u_2
γ : Type ?u.77130
δ : Type ?u.77133
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F G H K : α ⥤ β
η₁ : NatTrans H K
η₂ : NatTrans G H
η₃ : NatTrans F G
x✝ : α
⊢ app (comp (comp η₁ η₂) η₃) x✝ = app (comp η₁ (comp η₂ η₃)) x✝
Theorem: Category.NatTrans.comp_assoc
Proof state before:
case app.h
α : Type u_1
β : Type u_2
γ : Type ?u.77130
δ : Type ?u.77133
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F G H K : α ⥤ β
η₁ : NatTrans H K
η₂ : NatTrans G H
η₃ : NatTrans F G
x✝ : α
⊢ app (comp (comp η₁ η₂) η₃) x✝ = app (comp η₁ (comp η₂ η₃)) x✝
Tactic:
simp
Proof state after:
no goals
Theorem: Category.HomQuotient.quotient_full
Proof state before:
α : Type u_1
β : Type ?u.92190
γ : Type ?u.92193
δ : Type ?u.92196
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
⊢ Full (quotient r)
Tactic:
intro A B g
Proof state after:
α : Type u_1
β : Type ?u.92190
γ : Type ?u.92193
δ : Type ?u.92196
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
g : Functor.obj (quotient r) A ⟶ Functor.obj (quotient r) B
⊢ ∃ f, Functor.map (quotient r) f = g
Theorem: Category.HomQuotient.quotient_full
Proof state before:
α : Type u_1
β : Type ?u.92190
γ : Type ?u.92193
δ : Type ?u.92196
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
g : Functor.obj (quotient r) A ⟶ Functor.obj (quotient r) B
⊢ ∃ f, Functor.map (quotient r) f = g
Tactic:
refine Quotient.inductionOn g ?_
Proof state after:
α : Type u_1
β : Type ?u.92190
γ : Type ?u.92193
δ : Type ?u.92196
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
g : Functor.obj (quotient r) A ⟶ Functor.obj (quotient r) B
⊢ ∀ (a : (Functor.obj (quotient r) A).unquot ⟶ (Functor.obj (quotient r) B).unquot),
    ∃ f,
      Functor.map (quotient r) f =
        Quotient.mk (Congruence.setoid r (Functor.obj (quotient r) A).unquot (Functor.obj (quotient r) B).unquot) a
Theorem: Category.HomQuotient.quotient_full
Proof state before:
α : Type u_1
β : Type ?u.92190
γ : Type ?u.92193
δ : Type ?u.92196
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
g : Functor.obj (quotient r) A ⟶ Functor.obj (quotient r) B
⊢ ∀ (a : (Functor.obj (quotient r) A).unquot ⟶ (Functor.obj (quotient r) B).unquot),
    ∃ f,
      Functor.map (quotient r) f =
        Quotient.mk (Congruence.setoid r (Functor.obj (quotient r) A).unquot (Functor.obj (quotient r) B).unquot) a
Tactic:
intro g
Proof state after:
α : Type u_1
β : Type ?u.92190
γ : Type ?u.92193
δ : Type ?u.92196
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
g✝ : Functor.obj (quotient r) A ⟶ Functor.obj (quotient r) B
g : (Functor.obj (quotient r) A).unquot ⟶ (Functor.obj (quotient r) B).unquot
⊢ ∃ f,
    Functor.map (quotient r) f =
      Quotient.mk (Congruence.setoid r (Functor.obj (quotient r) A).unquot (Functor.obj (quotient r) B).unquot) g
Theorem: Category.HomQuotient.quotient_full
Proof state before:
α : Type u_1
β : Type ?u.92190
γ : Type ?u.92193
δ : Type ?u.92196
A✝ B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
A B : α
g✝ : Functor.obj (quotient r) A ⟶ Functor.obj (quotient r) B
g : (Functor.obj (quotient r) A).unquot ⟶ (Functor.obj (quotient r) B).unquot
⊢ ∃ f,
    Functor.map (quotient r) f =
      Quotient.mk (Congruence.setoid r (Functor.obj (quotient r) A).unquot (Functor.obj (quotient r) B).unquot) g
Tactic:
exact ⟨g, rfl⟩
Proof state after:
no goals
Theorem: Category.HomQuotient.quotient_essSurjective
Proof state before:
α : Type u_1
β : Type ?u.92381
γ : Type ?u.92384
δ : Type ?u.92387
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
⊢ EssSurjective (quotient r)
Tactic:
intro B
Proof state after:
α : Type u_1
β : Type ?u.92381
γ : Type ?u.92384
δ : Type ?u.92387
A B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
B : HomQuotient r
⊢ Nonempty ((A : α) ×' (Functor.obj (quotient r) A ≃ B))
Theorem: Category.HomQuotient.quotient_essSurjective
Proof state before:
α : Type u_1
β : Type ?u.92381
γ : Type ?u.92384
δ : Type ?u.92387
A B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
r : Congruence α
B : HomQuotient r
⊢ Nonempty ((A : α) ×' (Functor.obj (quotient r) A ≃ B))
Tactic:
exact ⟨⟨B.unquot, Iso.refl _⟩⟩
Proof state after:
no goals
Theorem: Set.ext
Proof state before:
α : Type u_1
a b : Set α
h : ∀ (x : α), x ∈ a ↔ x ∈ b
⊢ a = b
Tactic:
rw [mk.injEq]
Proof state after:
α : Type u_1
a b : Set α
h : ∀ (x : α), x ∈ a ↔ x ∈ b
⊢ a.mem = b.mem
Theorem: Set.ext
Proof state before:
α : Type u_1
a b : Set α
h : ∀ (x : α), x ∈ a ↔ x ∈ b
⊢ a.mem = b.mem
Tactic:
funext x
Proof state after:
case h
α : Type u_1
a b : Set α
h : ∀ (x : α), x ∈ a ↔ x ∈ b
x : α
⊢ mem a x = mem b x
Theorem: Set.ext
Proof state before:
case h
α : Type u_1
a b : Set α
h : ∀ (x : α), x ∈ a ↔ x ∈ b
x : α
⊢ mem a x = mem b x
Tactic:
exact propext (h x)
Proof state after:
no goals
Theorem: Set.image_id
Proof state before:
α : Type u_1
s : Set α
⊢ image id s = s
Tactic:
ext
Proof state after:
case h
α : Type u_1
s : Set α
x✝ : α
⊢ x✝ ∈ image id s ↔ x✝ ∈ s
Theorem: Set.image_id
Proof state before:
case h
α : Type u_1
s : Set α
x✝ : α
⊢ x✝ ∈ image id s ↔ x✝ ∈ s
Tactic:
rw [image]
Proof state after:
case h
α : Type u_1
s : Set α
x✝ : α
⊢ x✝ ∈ {x | ∃ a, a ∈ s ∧ id a = x} ↔ x✝ ∈ s
Theorem: Set.image_id
Proof state before:
case h
α : Type u_1
s : Set α
x✝ : α
⊢ x✝ ∈ {x | ∃ a, a ∈ s ∧ id a = x} ↔ x✝ ∈ s
Tactic:
simp
Proof state after:
no goals
Theorem: Set.image_comp
Proof state before:
β : Type u_1
γ : Type u_2
α : Type u_3
g : β → γ
f : α → β
s : Set α
⊢ image (g ∘ f) s = image g (image f s)
Tactic:
ext
Proof state after:
case h
β : Type u_1
γ : Type u_2
α : Type u_3
g : β → γ
f : α → β
s : Set α
x✝ : γ
⊢ x✝ ∈ image (g ∘ f) s ↔ x✝ ∈ image g (image f s)
Theorem: Set.image_comp
Proof state before:
case h
β : Type u_1
γ : Type u_2
α : Type u_3
g : β → γ
f : α → β
s : Set α
x✝ : γ
⊢ x✝ ∈ image (g ∘ f) s ↔ x✝ ∈ image g (image f s)
Tactic:
unfold image
Proof state after:
case h
β : Type u_1
γ : Type u_2
α : Type u_3
g : β → γ
f : α → β
s : Set α
x✝ : γ
⊢ x✝ ∈ {x | ∃ a, a ∈ s ∧ (g ∘ f) a = x} ↔ x✝ ∈ {x | ∃ a, a ∈ {x | ∃ a, a ∈ s ∧ f a = x} ∧ g a = x}
Theorem: Set.image_comp
Proof state before:
case h
β : Type u_1
γ : Type u_2
α : Type u_3
g : β → γ
f : α → β
s : Set α
x✝ : γ
⊢ x✝ ∈ {x | ∃ a, a ∈ s ∧ (g ∘ f) a = x} ↔ x✝ ∈ {x | ∃ a, a ∈ {x | ∃ a, a ∈ s ∧ f a = x} ∧ g a = x}
Tactic:
aesop
Proof state after:
no goals
Theorem: Set.image_singleton
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
x : α
⊢ image f {x} = {f x}
Tactic:
ext x
Proof state after:
case h
α : Type u_1
β : Type u_2
f : α → β
x✝ : α
x : β
⊢ x ∈ image f {x✝} ↔ x ∈ {f x✝}
Theorem: Set.image_singleton
Proof state before:
case h
α : Type u_1
β : Type u_2
f : α → β
x✝ : α
x : β
⊢ x ∈ image f {x✝} ↔ x ∈ {f x✝}
Tactic:
constructor
Proof state after:
case h.mp
α : Type u_1
β : Type u_2
f : α → β
x✝ : α
x : β
⊢ x ∈ image f {x✝} → x ∈ {f x✝}

case h.mpr
α : Type u_1
β : Type u_2
f : α → β
x✝ : α
x : β
⊢ x ∈ {f x✝} → x ∈ image f {x✝}
Theorem: Set.image_singleton
Proof state before:
case h.mp
α : Type u_1
β : Type u_2
f : α → β
x✝ : α
x : β
⊢ x ∈ image f {x✝} → x ∈ {f x✝}
Tactic:
rintro ⟨_, rfl, rfl⟩
Proof state after:
case h.mp.intro.intro
α : Type u_1
β : Type u_2
f : α → β
w✝ : α
⊢ f w✝ ∈ {f w✝}
Theorem: Set.image_singleton
Proof state before:
case h.mp.intro.intro
α : Type u_1
β : Type u_2
f : α → β
w✝ : α
⊢ f w✝ ∈ {f w✝}
Tactic:
rfl
Proof state after:
no goals
Theorem: Set.image_singleton
Proof state before:
case h.mpr
α : Type u_1
β : Type u_2
f : α → β
x✝ : α
x : β
⊢ x ∈ {f x✝} → x ∈ image f {x✝}
Tactic:
rintro rfl
Proof state after:
case h.mpr
α : Type u_1
β : Type u_2
f : α → β
x : α
⊢ f x ∈ image f {x}
Theorem: Set.image_singleton
Proof state before:
case h.mpr
α : Type u_1
β : Type u_2
f : α → β
x : α
⊢ f x ∈ image f {x}
Tactic:
exact ⟨x, rfl, rfl⟩
Proof state after:
no goals
Theorem: Category.ΦΨ
Proof state before:
α : Type u_1
β : Type ?u.4710
γ : Type ?u.4713
δ : Type ?u.4716
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ Type u_2
x : Functor.obj F A
⊢ Φ (Ψ x) = x
Tactic:
unfold Φ Ψ
Proof state after:
α : Type u_1
β : Type ?u.4710
γ : Type ?u.4713
δ : Type ?u.4716
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ Type u_2
x : Functor.obj F A
⊢ NatTrans.app
      { app := fun B f => Functor.map F f x,
        naturality :=
          (_ :
            ∀ {B C : α} (f : B ⟶ C),
              (fun B f => Functor.map F f x) C ∘ Functor.map (CoHom A) f =
                Functor.map F f ∘ (fun B f => Functor.map F f x) B) }
      A (𝟙 A) =
    x
Theorem: Category.ΦΨ
Proof state before:
α : Type u_1
β : Type ?u.4710
γ : Type ?u.4713
δ : Type ?u.4716
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ Type u_2
x : Functor.obj F A
⊢ NatTrans.app
      { app := fun B f => Functor.map F f x,
        naturality :=
          (_ :
            ∀ {B C : α} (f : B ⟶ C),
              (fun B f => Functor.map F f x) C ∘ Functor.map (CoHom A) f =
                Functor.map F f ∘ (fun B f => Functor.map F f x) B) }
      A (𝟙 A) =
    x
Tactic:
simp
Proof state after:
no goals
Theorem: Category.ΨΦ
Proof state before:
α : Type u_1
β : Type ?u.4979
γ : Type ?u.4982
δ : Type ?u.4985
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ Type u_2
η : NatTrans (CoHom A) F
⊢ Ψ (Φ η) = η
Tactic:
ext B
Proof state after:
case app.h
α : Type u_1
β : Type ?u.4979
γ : Type ?u.4982
δ : Type ?u.4985
A B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ Type u_2
η : NatTrans (CoHom A) F
B : α
⊢ NatTrans.app (Ψ (Φ η)) B = NatTrans.app η B
Theorem: Category.ΨΦ
Proof state before:
case app.h
α : Type u_1
β : Type ?u.4979
γ : Type ?u.4982
δ : Type ?u.4985
A B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ Type u_2
η : NatTrans (CoHom A) F
B : α
⊢ NatTrans.app (Ψ (Φ η)) B = NatTrans.app η B
Tactic:
funext f
Proof state after:
case app.h.h
α : Type u_1
β : Type ?u.4979
γ : Type ?u.4982
δ : Type ?u.4985
A B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ Type u_2
η : NatTrans (CoHom A) F
B : α
f : Functor.obj (CoHom A) B
⊢ NatTrans.app (Ψ (Φ η)) B f = NatTrans.app η B f
Theorem: Category.ΨΦ
Proof state before:
case app.h.h
α : Type u_1
β : Type ?u.4979
γ : Type ?u.4982
δ : Type ?u.4985
A B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ Type u_2
η : NatTrans (CoHom A) F
B : α
f : Functor.obj (CoHom A) B
⊢ NatTrans.app (Ψ (Φ η)) B f = NatTrans.app η B f
Tactic:
have := congrFun (η.naturality f) (𝟙 A)
Proof state after:
case app.h.h
α : Type u_1
β : Type ?u.4979
γ : Type ?u.4982
δ : Type ?u.4985
A B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ Type u_2
η : NatTrans (CoHom A) F
B : α
f : Functor.obj (CoHom A) B
this : (NatTrans.app η B ∘ Functor.map (CoHom A) f) (𝟙 A) = (Functor.map F f ∘ NatTrans.app η A) (𝟙 A)
⊢ NatTrans.app (Ψ (Φ η)) B f = NatTrans.app η B f
Theorem: Category.ΨΦ
Proof state before:
case app.h.h
α : Type u_1
β : Type ?u.4979
γ : Type ?u.4982
δ : Type ?u.4985
A B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ Type u_2
η : NatTrans (CoHom A) F
B : α
f : Functor.obj (CoHom A) B
this : (NatTrans.app η B ∘ Functor.map (CoHom A) f) (𝟙 A) = (Functor.map F f ∘ NatTrans.app η A) (𝟙 A)
⊢ NatTrans.app (Ψ (Φ η)) B f = NatTrans.app η B f
Tactic:
simp at this
Proof state after:
case app.h.h
α : Type u_1
β : Type ?u.4979
γ : Type ?u.4982
δ : Type ?u.4985
A B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ Type u_2
η : NatTrans (CoHom A) F
B : α
f : Functor.obj (CoHom A) B
this : NatTrans.app η B f = Functor.map F f (NatTrans.app η A (𝟙 A))
⊢ NatTrans.app (Ψ (Φ η)) B f = NatTrans.app η B f
Theorem: Category.ΨΦ
Proof state before:
case app.h.h
α : Type u_1
β : Type ?u.4979
γ : Type ?u.4982
δ : Type ?u.4985
A B✝ C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F : α ⥤ Type u_2
η : NatTrans (CoHom A) F
B : α
f : Functor.obj (CoHom A) B
this : NatTrans.app η B f = Functor.map F f (NatTrans.app η A (𝟙 A))
⊢ NatTrans.app (Ψ (Φ η)) B f = NatTrans.app η B f
Tactic:
exact this.symm
Proof state after:
no goals
Theorem: verus_lemma_mul_strictly_positive
Proof state before:
x y : ℤ
⊢ 0 < x ∧ 0 < y → 0 < x * y
Tactic:
aesop
Proof state after:
no goals
Theorem: verus_lemma_mul_nonzero
Proof state before:
x y : ℤ
⊢ x * y ≠ 0 ↔ x ≠ 0 ∧ y ≠ 0
Tactic:
aesop
Proof state after:
no goals
Theorem: verus_lemma_mul_is_associative
Proof state before:
x y z : ℤ
⊢ x * (y * z) = x * y * z
Tactic:
rw [Int.mul_assoc]
Proof state after:
no goals
Theorem: verus_lemma_mul_ordering
Proof state before:
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
⊢ x * y ≥ x ∧ x * y ≥ y
Tactic:
have h' : ∀ x y : Int, x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x := by
  intros x y h1 h2 h3
  by_cases h4 : x > 0
  . apply le_mul_of_one_le_right (Int.nonneg_of_pos h4)
    have h5 : y < 0 ∨ 1 ≤ y := by
      rw [← Int.zero_add 1, Int.add_one_le_iff]
      exact Int.lt_or_gt_of_ne h2
    rcases h5 with h5 | h5
    . have := Int.mul_neg_of_pos_of_neg h4 h5
      linarith
    . exact h5
  . have h5 : x < 0 := by
      simp only [gt_iff_lt, not_lt] at h4
      exact lt_of_le_of_ne h4 h1
    linarith
Proof state after:
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h' : ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
⊢ x * y ≥ x ∧ x * y ≥ y
Theorem: verus_lemma_mul_ordering
Proof state before:
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h' : ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
⊢ x * y ≥ x ∧ x * y ≥ y
Tactic:
constructor
Proof state after:
case left
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h' : ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
⊢ x * y ≥ x

case right
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h' : ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
⊢ x * y ≥ y
Theorem: verus_lemma_mul_ordering
Proof state before:
case left
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h' : ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
⊢ x * y ≥ x

case right
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h' : ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
⊢ x * y ≥ y
Tactic:
. exact h' x y h1 h2 h3
Proof state after:
case right
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h' : ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
⊢ x * y ≥ y
Theorem: verus_lemma_mul_ordering
Proof state before:
case right
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h' : ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
⊢ x * y ≥ y
Tactic:
. rw [mul_comm] at h3
  rw [mul_comm]
  exact h' y x h2 h1 h3
Proof state after:
no goals
Theorem: verus_lemma_mul_ordering
Proof state before:
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
⊢ ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
Tactic:
intros x y h1 h2 h3
Proof state after:
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
⊢ x * y ≥ x
Theorem: verus_lemma_mul_ordering
Proof state before:
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
⊢ x * y ≥ x
Tactic:
by_cases h4 : x > 0
Proof state after:
case pos
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
⊢ x * y ≥ x

case neg
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : ¬x > 0
⊢ x * y ≥ x
Theorem: verus_lemma_mul_ordering
Proof state before:
case pos
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
⊢ x * y ≥ x

case neg
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : ¬x > 0
⊢ x * y ≥ x
Tactic:
. apply le_mul_of_one_le_right (Int.nonneg_of_pos h4)
  have h5 : y < 0 ∨ 1 ≤ y := by
    rw [← Int.zero_add 1, Int.add_one_le_iff]
    exact Int.lt_or_gt_of_ne h2
  rcases h5 with h5 | h5
  . have := Int.mul_neg_of_pos_of_neg h4 h5
    linarith
  . exact h5
Proof state after:
case neg
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : ¬x > 0
⊢ x * y ≥ x
Theorem: verus_lemma_mul_ordering
Proof state before:
case neg
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : ¬x > 0
⊢ x * y ≥ x
Tactic:
. have h5 : x < 0 := by
    simp only [gt_iff_lt, not_lt] at h4
    exact lt_of_le_of_ne h4 h1
  linarith
Proof state after:
no goals
Theorem: verus_lemma_mul_ordering
Proof state before:
case pos
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
⊢ x * y ≥ x
Tactic:
apply le_mul_of_one_le_right (Int.nonneg_of_pos h4)
Proof state after:
case pos
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
⊢ 1 ≤ y
Theorem: verus_lemma_mul_ordering
Proof state before:
case pos
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
⊢ 1 ≤ y
Tactic:
have h5 : y < 0 ∨ 1 ≤ y := by
  rw [← Int.zero_add 1, Int.add_one_le_iff]
  exact Int.lt_or_gt_of_ne h2
Proof state after:
case pos
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
h5 : y < 0 ∨ 1 ≤ y
⊢ 1 ≤ y
Theorem: verus_lemma_mul_ordering
Proof state before:
case pos
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
h5 : y < 0 ∨ 1 ≤ y
⊢ 1 ≤ y
Tactic:
rcases h5 with h5 | h5
Proof state after:
case pos.inl
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
h5 : y < 0
⊢ 1 ≤ y

case pos.inr
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
h5 : 1 ≤ y
⊢ 1 ≤ y
Theorem: verus_lemma_mul_ordering
Proof state before:
case pos.inl
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
h5 : y < 0
⊢ 1 ≤ y

case pos.inr
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
h5 : 1 ≤ y
⊢ 1 ≤ y
Tactic:
. have := Int.mul_neg_of_pos_of_neg h4 h5
  linarith
Proof state after:
case pos.inr
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
h5 : 1 ≤ y
⊢ 1 ≤ y
Theorem: verus_lemma_mul_ordering
Proof state before:
case pos.inr
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
h5 : 1 ≤ y
⊢ 1 ≤ y
Tactic:
. exact h5
Proof state after:
no goals
Theorem: verus_lemma_mul_ordering
Proof state before:
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
⊢ y < 0 ∨ 1 ≤ y
Tactic:
rw [← Int.zero_add 1, Int.add_one_le_iff]
Proof state after:
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
⊢ y < 0 ∨ 0 < y
Theorem: verus_lemma_mul_ordering
Proof state before:
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
⊢ y < 0 ∨ 0 < y
Tactic:
exact Int.lt_or_gt_of_ne h2
Proof state after:
no goals
Theorem: verus_lemma_mul_ordering
Proof state before:
case pos.inl
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
h5 : y < 0
⊢ 1 ≤ y
Tactic:
have := Int.mul_neg_of_pos_of_neg h4 h5
Proof state after:
case pos.inl
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
h5 : y < 0
this : x * y < 0
⊢ 1 ≤ y
Theorem: verus_lemma_mul_ordering
Proof state before:
case pos.inl
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
h5 : y < 0
this : x * y < 0
⊢ 1 ≤ y
Tactic:
linarith
Proof state after:
no goals
Theorem: verus_lemma_mul_ordering
Proof state before:
case pos.inr
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x > 0
h5 : 1 ≤ y
⊢ 1 ≤ y
Tactic:
exact h5
Proof state after:
no goals
Theorem: verus_lemma_mul_ordering
Proof state before:
case neg
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : ¬x > 0
⊢ x * y ≥ x
Tactic:
have h5 : x < 0 := by
  simp only [gt_iff_lt, not_lt] at h4
  exact lt_of_le_of_ne h4 h1
Proof state after:
case neg
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : ¬x > 0
h5 : x < 0
⊢ x * y ≥ x
Theorem: verus_lemma_mul_ordering
Proof state before:
case neg
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : ¬x > 0
h5 : x < 0
⊢ x * y ≥ x
Tactic:
linarith
Proof state after:
no goals
Theorem: verus_lemma_mul_ordering
Proof state before:
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : ¬x > 0
⊢ x < 0
Tactic:
simp only [gt_iff_lt, not_lt] at h4
Proof state after:
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x ≤ 0
⊢ x < 0
Theorem: verus_lemma_mul_ordering
Proof state before:
x✝ y✝ : ℤ
h1✝ : x✝ ≠ 0
h2✝ : y✝ ≠ 0
h3✝ : 0 ≤ x✝ * y✝
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h4 : x ≤ 0
⊢ x < 0
Tactic:
exact lt_of_le_of_ne h4 h1
Proof state after:
no goals
Theorem: verus_lemma_mul_ordering
Proof state before:
case left
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h' : ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
⊢ x * y ≥ x
Tactic:
exact h' x y h1 h2 h3
Proof state after:
no goals
Theorem: verus_lemma_mul_ordering
Proof state before:
case right
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ x * y
h' : ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
⊢ x * y ≥ y
Tactic:
rw [mul_comm] at h3
Proof state after:
case right
x y : ℤ
h1 : x ≠ 0
h2 : y ≠ 0
h3 : 0 ≤ y * x
h' : ∀ (x y : ℤ), x ≠ 0 → y ≠ 0 → 0 ≤ x * y → x * y ≥ x
⊢ x * y ≥ y