internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Integer.as_diff
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
msubst : ∀ {x₁ x₂ : ℤ}, x₁ ≃ x₂ → motive x₁ → motive x₂ :=
  fun {x₁ x₂} h =>
    match h with
    | x => fun h =>
      match h with
      | x_1 =>
        let_fun this :=
          match x_1 with
          | Exists.intro n (Exists.intro m h) =>
            let_fun this := trans (trans rfl (Rel.symm x)) h;
            let_fun this := Exists.intro n (Exists.intro m this);
            let_fun this := this;
            this;
        this
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m
Tactic:
let idx_fam := Function.idx_fam_prop msubst
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
msubst : ∀ {x₁ x₂ : ℤ}, x₁ ≃ x₂ → motive x₁ → motive x₂ :=
  fun {x₁ x₂} h =>
    match h with
    | x => fun h =>
      match h with
      | x_1 =>
        let_fun this :=
          match x_1 with
          | Exists.intro n (Exists.intro m h) =>
            let_fun this := trans (trans rfl (Rel.symm x)) h;
            let_fun this := Exists.intro n (Exists.intro m this);
            let_fun this := this;
            this;
        this
idx_fam : IndexedFamily fun {x₁} => motive x₁ := Function.idx_fam_prop ⋯
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m
Theorem: Lean4Axiomatic.Integer.as_diff
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
msubst : ∀ {x₁ x₂ : ℤ}, x₁ ≃ x₂ → motive x₁ → motive x₂ :=
  fun {x₁ x₂} h =>
    match h with
    | x => fun h =>
      match h with
      | x_1 =>
        let_fun this :=
          match x_1 with
          | Exists.intro n (Exists.intro m h) =>
            let_fun this := trans (trans rfl (Rel.symm x)) h;
            let_fun this := Exists.intro n (Exists.intro m this);
            let_fun this := this;
            this;
        this
idx_fam : IndexedFamily fun {x₁} => motive x₁ := Function.idx_fam_prop ⋯
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m
Tactic:
let on_diff (k j : ℕ) : motive ((k:ℤ) - j) :=
  Exists.intro k (Exists.intro j Rel.refl)
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
msubst : ∀ {x₁ x₂ : ℤ}, x₁ ≃ x₂ → motive x₁ → motive x₂ :=
  fun {x₁ x₂} h =>
    match h with
    | x => fun h =>
      match h with
      | x_1 =>
        let_fun this :=
          match x_1 with
          | Exists.intro n (Exists.intro m h) =>
            let_fun this := trans (trans rfl (Rel.symm x)) h;
            let_fun this := Exists.intro n (Exists.intro m this);
            let_fun this := this;
            this;
        this
idx_fam : IndexedFamily fun {x₁} => motive x₁ := Function.idx_fam_prop ⋯
on_diff : ∀ (k j : ℕ), motive (Coe.coe k - Coe.coe j) := fun k j => Exists.intro k (Exists.intro j Rel.refl)
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m
Theorem: Lean4Axiomatic.Integer.as_diff
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
msubst : ∀ {x₁ x₂ : ℤ}, x₁ ≃ x₂ → motive x₁ → motive x₂ :=
  fun {x₁ x₂} h =>
    match h with
    | x => fun h =>
      match h with
      | x_1 =>
        let_fun this :=
          match x_1 with
          | Exists.intro n (Exists.intro m h) =>
            let_fun this := trans (trans rfl (Rel.symm x)) h;
            let_fun this := Exists.intro n (Exists.intro m this);
            let_fun this := this;
            this;
        this
idx_fam : IndexedFamily fun {x₁} => motive x₁ := Function.idx_fam_prop ⋯
on_diff : ∀ (k j : ℕ), motive (Coe.coe k - Coe.coe j) := fun k j => Exists.intro k (Exists.intro j Rel.refl)
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m
Tactic:
let ctx := ind_ctx_prop on_diff
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
msubst : ∀ {x₁ x₂ : ℤ}, x₁ ≃ x₂ → motive x₁ → motive x₂ :=
  fun {x₁ x₂} h =>
    match h with
    | x => fun h =>
      match h with
      | x_1 =>
        let_fun this :=
          match x_1 with
          | Exists.intro n (Exists.intro m h) =>
            let_fun this := trans (trans rfl (Rel.symm x)) h;
            let_fun this := Exists.intro n (Exists.intro m this);
            let_fun this := this;
            this;
        this
idx_fam : IndexedFamily fun {x₁} => motive x₁ := Function.idx_fam_prop ⋯
on_diff : ∀ (k j : ℕ), motive (Coe.coe k - Coe.coe j) := fun k j => Exists.intro k (Exists.intro j Rel.refl)
ctx : Induction.Context motive := ind_ctx_prop on_diff
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m
Theorem: Lean4Axiomatic.Integer.as_diff
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
msubst : ∀ {x₁ x₂ : ℤ}, x₁ ≃ x₂ → motive x₁ → motive x₂ :=
  fun {x₁ x₂} h =>
    match h with
    | x => fun h =>
      match h with
      | x_1 =>
        let_fun this :=
          match x_1 with
          | Exists.intro n (Exists.intro m h) =>
            let_fun this := trans (trans rfl (Rel.symm x)) h;
            let_fun this := Exists.intro n (Exists.intro m this);
            let_fun this := this;
            this;
        this
idx_fam : IndexedFamily fun {x₁} => motive x₁ := Function.idx_fam_prop ⋯
on_diff : ∀ (k j : ℕ), motive (Coe.coe k - Coe.coe j) := fun k j => Exists.intro k (Exists.intro j Rel.refl)
ctx : Induction.Context motive := ind_ctx_prop on_diff
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m
Tactic:
have : motive a := ctx.ind_diff a
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
msubst : ∀ {x₁ x₂ : ℤ}, x₁ ≃ x₂ → motive x₁ → motive x₂ :=
  fun {x₁ x₂} h =>
    match h with
    | x => fun h =>
      match h with
      | x_1 =>
        let_fun this :=
          match x_1 with
          | Exists.intro n (Exists.intro m h) =>
            let_fun this := trans (trans rfl (Rel.symm x)) h;
            let_fun this := Exists.intro n (Exists.intro m this);
            let_fun this := this;
            this;
        this
idx_fam : IndexedFamily fun {x₁} => motive x₁ := Function.idx_fam_prop ⋯
on_diff : ∀ (k j : ℕ), motive (Coe.coe k - Coe.coe j) := fun k j => Exists.intro k (Exists.intro j Rel.refl)
ctx : Induction.Context motive := ind_ctx_prop on_diff
this : motive a
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m
Theorem: Lean4Axiomatic.Integer.as_diff
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
msubst : ∀ {x₁ x₂ : ℤ}, x₁ ≃ x₂ → motive x₁ → motive x₂ :=
  fun {x₁ x₂} h =>
    match h with
    | x => fun h =>
      match h with
      | x_1 =>
        let_fun this :=
          match x_1 with
          | Exists.intro n (Exists.intro m h) =>
            let_fun this := trans (trans rfl (Rel.symm x)) h;
            let_fun this := Exists.intro n (Exists.intro m this);
            let_fun this := this;
            this;
        this
idx_fam : IndexedFamily fun {x₁} => motive x₁ := Function.idx_fam_prop ⋯
on_diff : ∀ (k j : ℕ), motive (Coe.coe k - Coe.coe j) := fun k j => Exists.intro k (Exists.intro j Rel.refl)
ctx : Induction.Context motive := ind_ctx_prop on_diff
this : motive a
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m
Tactic:
have : ∃ (n m : ℕ), a ≃ n - m := this
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
msubst : ∀ {x₁ x₂ : ℤ}, x₁ ≃ x₂ → motive x₁ → motive x₂ :=
  fun {x₁ x₂} h =>
    match h with
    | x => fun h =>
      match h with
      | x_1 =>
        let_fun this :=
          match x_1 with
          | Exists.intro n (Exists.intro m h) =>
            let_fun this := trans (trans rfl (Rel.symm x)) h;
            let_fun this := Exists.intro n (Exists.intro m this);
            let_fun this := this;
            this;
        this
idx_fam : IndexedFamily fun {x₁} => motive x₁ := Function.idx_fam_prop ⋯
on_diff : ∀ (k j : ℕ), motive (Coe.coe k - Coe.coe j) := fun k j => Exists.intro k (Exists.intro j Rel.refl)
ctx : Induction.Context motive := ind_ctx_prop on_diff
this✝ : motive a
this : ∃ n m, a ≃ Coe.coe n - Coe.coe m
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m
Theorem: Lean4Axiomatic.Integer.as_diff
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
msubst : ∀ {x₁ x₂ : ℤ}, x₁ ≃ x₂ → motive x₁ → motive x₂ :=
  fun {x₁ x₂} h =>
    match h with
    | x => fun h =>
      match h with
      | x_1 =>
        let_fun this :=
          match x_1 with
          | Exists.intro n (Exists.intro m h) =>
            let_fun this := trans (trans rfl (Rel.symm x)) h;
            let_fun this := Exists.intro n (Exists.intro m this);
            let_fun this := this;
            this;
        this
idx_fam : IndexedFamily fun {x₁} => motive x₁ := Function.idx_fam_prop ⋯
on_diff : ∀ (k j : ℕ), motive (Coe.coe k - Coe.coe j) := fun k j => Exists.intro k (Exists.intro j Rel.refl)
ctx : Induction.Context motive := ind_ctx_prop on_diff
this✝ : motive a
this : ∃ n m, a ≃ Coe.coe n - Coe.coe m
⊢ ∃ n m, a ≃ Coe.coe n - Coe.coe m
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.as_diff
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
x₁ x₂ : ℤ
⊢ x₁ ≃ x₂ → motive x₁ → motive x₂
Tactic:
intro (_ : x₁ ≃ x₂) (_ : motive x₁)
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
x₁ x₂ : ℤ
x✝¹ : x₁ ≃ x₂
x✝ : motive x₁
⊢ motive x₂
Theorem: Lean4Axiomatic.Integer.as_diff
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
x₁ x₂ : ℤ
x✝¹ : x₁ ≃ x₂
x✝ : motive x₁
⊢ motive x₂
Tactic:
have Exists.intro (n : ℕ) (Exists.intro (m : ℕ) (_ : x₁ ≃ n - m)) :=
  ‹motive x₁›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
x₁ x₂ : ℤ
x✝¹ : x₁ ≃ x₂
x✝ : motive x₁
n m : ℕ
h✝ : x₁ ≃ Coe.coe n - Coe.coe m
⊢ motive x₂
Theorem: Lean4Axiomatic.Integer.as_diff
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
x₁ x₂ : ℤ
x✝¹ : x₁ ≃ x₂
x✝ : motive x₁
n m : ℕ
h✝ : x₁ ≃ Coe.coe n - Coe.coe m
⊢ motive x₂
Tactic:
have : x₂ ≃ n - m := calc
  _ = x₂    := rfl
  _ ≃ x₁    := Rel.symm ‹x₁ ≃ x₂›
  _ ≃ n - m := ‹x₁ ≃ n - m›
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
x₁ x₂ : ℤ
x✝¹ : x₁ ≃ x₂
x✝ : motive x₁
n m : ℕ
h✝ : x₁ ≃ Coe.coe n - Coe.coe m
this : x₂ ≃ Coe.coe n - Coe.coe m
⊢ motive x₂
Theorem: Lean4Axiomatic.Integer.as_diff
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
x₁ x₂ : ℤ
x✝¹ : x₁ ≃ x₂
x✝ : motive x₁
n m : ℕ
h✝ : x₁ ≃ Coe.coe n - Coe.coe m
this : x₂ ≃ Coe.coe n - Coe.coe m
⊢ motive x₂
Tactic:
have : ∃ (n m : ℕ), x₂ ≃ n - m := Exists.intro n (Exists.intro m this)
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
x₁ x₂ : ℤ
x✝¹ : x₁ ≃ x₂
x✝ : motive x₁
n m : ℕ
h✝ : x₁ ≃ Coe.coe n - Coe.coe m
this✝ : x₂ ≃ Coe.coe n - Coe.coe m
this : ∃ n m, x₂ ≃ Coe.coe n - Coe.coe m
⊢ motive x₂
Theorem: Lean4Axiomatic.Integer.as_diff
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
x₁ x₂ : ℤ
x✝¹ : x₁ ≃ x₂
x✝ : motive x₁
n m : ℕ
h✝ : x₁ ≃ Coe.coe n - Coe.coe m
this✝ : x₂ ≃ Coe.coe n - Coe.coe m
this : ∃ n m, x₂ ≃ Coe.coe n - Coe.coe m
⊢ motive x₂
Tactic:
have : motive x₂ := this
Proof state after:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
x₁ x₂ : ℤ
x✝¹ : x₁ ≃ x₂
x✝ : motive x₁
n m : ℕ
h✝ : x₁ ≃ Coe.coe n - Coe.coe m
this✝¹ : x₂ ≃ Coe.coe n - Coe.coe m
this✝ : ∃ n m, x₂ ≃ Coe.coe n - Coe.coe m
this : motive x₂
⊢ motive x₂
Theorem: Lean4Axiomatic.Integer.as_diff
Proof state before:
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Negation ℤ
inst✝¹ : Subtraction ℤ
inst✝ : Induction ℤ
a : ℤ
motive : ℤ → Prop := fun z => ∃ n m, z ≃ Coe.coe n - Coe.coe m
x₁ x₂ : ℤ
x✝¹ : x₁ ≃ x₂
x✝ : motive x₁
n m : ℕ
h✝ : x₁ ≃ Coe.coe n - Coe.coe m
this✝¹ : x₂ ≃ Coe.coe n - Coe.coe m
this✝ : ∃ n m, x₂ ≃ Coe.coe n - Coe.coe m
this : motive x₂
⊢ motive x₂
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.one_neqv_zero
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Core ℤ
⊢ 1 ≄ 0
Tactic:
intro (_ : (1 : ℤ) ≃ 0)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Core ℤ
x✝ : 1 ≃ 0
⊢ False
Theorem: Lean4Axiomatic.Integer.one_neqv_zero
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Core ℤ
x✝ : 1 ≃ 0
⊢ False
Tactic:
have : coe (1 : ℕ) ≃ coe (0 : ℕ) := ‹(1 : ℤ) ≃ 0›
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Core ℤ
x✝ : 1 ≃ 0
this : coe 1 ≃ coe 0
⊢ False
Theorem: Lean4Axiomatic.Integer.one_neqv_zero
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Core ℤ
x✝ : 1 ≃ 0
this : coe 1 ≃ coe 0
⊢ False
Tactic:
have : (1 : ℕ) ≃ 0 := AA.inject ‹coe (1 : ℕ) ≃ coe (0 : ℕ)›
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Core ℤ
x✝ : 1 ≃ 0
this✝ : coe 1 ≃ coe 0
this : 1 ≃ 0
⊢ False
Theorem: Lean4Axiomatic.Integer.one_neqv_zero
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Core ℤ
x✝ : 1 ≃ 0
this✝ : coe 1 ≃ coe 0
this : 1 ≃ 0
⊢ False
Tactic:
have : Natural.step (0 : ℕ) ≃ 0 :=
  Rel.trans (Rel.symm Natural.literal_step) ‹(1 : ℕ) ≃ 0›
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Core ℤ
x✝ : 1 ≃ 0
this✝¹ : coe 1 ≃ coe 0
this✝ : 1 ≃ 0
this : Natural.step 0 ≃ 0
⊢ False
Theorem: Lean4Axiomatic.Integer.one_neqv_zero
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Core ℤ
x✝ : 1 ≃ 0
this✝¹ : coe 1 ≃ coe 0
this✝ : 1 ≃ 0
this : Natural.step 0 ≃ 0
⊢ False
Tactic:
exact absurd ‹Natural.step (0 : ℕ) ≃ 0› Natural.step_neqv_zero
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.min_le
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
inst✝ : MinMax ℚ
p q : ℚ
⊢ Ordered.min p q ≃ p ↔ p ≤ q
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
inst✝ : MinMax ℚ
p q : ℚ
⊢ Ordered.min p q ≃ p → p ≤ q

case mpr
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
inst✝ : MinMax ℚ
p q : ℚ
⊢ p ≤ q → Ordered.min p q ≃ p
Theorem: Lean4Axiomatic.Rational.min_le
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
inst✝ : MinMax ℚ
p q : ℚ
⊢ Ordered.min p q ≃ p → p ≤ q
Tactic:
case mp =>
  intro (_ : min p q ≃ p)
  show p ≤ q
  have : min p q ≤ q := min_leR
  have : p ≤ q := le_substL_eqv ‹min p q ≃ p› ‹min p q ≤ q›
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.min_le
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
inst✝ : MinMax ℚ
p q : ℚ
⊢ p ≤ q → Ordered.min p q ≃ p
Tactic:
case mpr =>
  intro (_ : p ≤ q)
  show min p q ≃ p
  have : min p q ≃ p ∨ min p q ≃ q := min_cases
  match this with
  | Or.inl (_ : min p q ≃ p) =>
    have := ‹min p q ≃ p›
    exact this
  | Or.inr (_ : min p q ≃ q) =>
    have : min p q ≤ p := min_leL
    have : q ≤ p := le_substL_eqv ‹min p q ≃ q› ‹min p q ≤ p›
    have : q ≃ p := le_antisymm ‹q ≤ p› ‹p ≤ q›
    have : min p q ≃ p := eqv_trans ‹min p q ≃ q› ‹q ≃ p›
    exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.min_le
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
inst✝ : MinMax ℚ
p q : ℚ
⊢ Ordered.min p q ≃ p → p ≤ q
Tactic:
intro (_ : min p q ≃ p)
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
inst✝ : MinMax ℚ
p q : ℚ
x✝ : Ordered.min p q ≃ p
⊢ p ≤ q
Theorem: Lean4Axiomatic.Rational.min_le
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
inst✝ : MinMax ℚ
p q : ℚ
x✝ : Ordered.min p q ≃ p
⊢ p ≤ q
Tactic:
have : min p q ≤ q := min_leR
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
inst✝ : MinMax ℚ
p q : ℚ
x✝ : Ordered.min p q ≃ p
this : Ordered.min p q ≤ q
⊢ p ≤ q
Theorem: Lean4Axiomatic.Rational.min_le
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
inst✝ : MinMax ℚ
p q : ℚ
x✝ : Ordered.min p q ≃ p
this : Ordered.min p q ≤ q
⊢ p ≤ q
Tactic:
have : p ≤ q := le_substL_eqv ‹min p q ≃ p› ‹min p q ≤ q›
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
inst✝ : MinMax ℚ
p q : ℚ
x✝ : Ordered.min p q ≃ p
this✝ : Ordered.min p q ≤ q
this : p ≤ q
⊢ p ≤ q
Theorem: Lean4Axiomatic.Rational.min_le
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
inst✝ : MinMax ℚ
p q : ℚ
x✝ : Ordered.min p q ≃ p
this✝ : Ordered.min p q ≤ q
this : p ≤ q
⊢ p ≤ q
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.min_le
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
inst✝ : MinMax ℚ
p q : ℚ
⊢ p ≤ q → Ordered.min p q ≃ p
Tactic:
intro (_ : p ≤ q)
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
inst✝ : MinMax ℚ
p q : ℚ
x✝ : p ≤ q
⊢ Ordered.min p q ≃ p
Theorem: Lean4Axiomatic.Rational.min_le
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
inst✝ : MinMax ℚ
p q : ℚ
x✝ : p ≤ q
⊢ Ordered.min p q ≃ p
Tactic:
have : min p q ≃ p ∨ min p q ≃ q := min_cases
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
inst✝ : MinMax ℚ
p q : ℚ
x✝ : p ≤ q
this : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
⊢ Ordered.min p q ≃ p
Theorem: Lean4Axiomatic.Rational.min_le
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
inst✝ : MinMax ℚ
p q : ℚ
x✝ : p ≤ q
this : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
⊢ Ordered.min p q ≃ p
Tactic:
match this with
| Or.inl (_ : min p q ≃ p) =>
  have := ‹min p q ≃ p›
  exact this
| Or.inr (_ : min p q ≃ q) =>
  have : min p q ≤ p := min_leL
  have : q ≤ p := le_substL_eqv ‹min p q ≃ q› ‹min p q ≤ p›
  have : q ≃ p := le_antisymm ‹q ≤ p› ‹p ≤ q›
  have : min p q ≃ p := eqv_trans ‹min p q ≃ q› ‹q ≃ p›
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.min_le
Proof state before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
inst✝ : MinMax ℚ
p q : ℚ
x✝ : p ≤ q
this : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
h✝ : Ordered.min p q ≃ p
⊢ Ordered.min p q ≃ p
Tactic:
have := ‹min p q ≃ p›
Proof state after:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
inst✝ : MinMax ℚ
p q : ℚ
x✝ : p ≤ q
this✝ : Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
h✝ this : Ordered.min p q ≃ p
⊢ Ordered.min p q ≃ p