internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Natural.sqrt1
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
x✝ : n * n ≃ 1
⊢ n ≃ 1
Tactic:
have (And.intro (_ : n ≃ 1) _) := factors_eqv_1.mp ‹n * n ≃ 1›
Proof state after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
x✝ : n * n ≃ 1
left✝ right✝ : n ≃ 1
⊢ n ≃ 1
Theorem: Lean4Axiomatic.Natural.sqrt1
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
x✝ : n * n ≃ 1
left✝ right✝ : n ≃ 1
⊢ n ≃ 1
Tactic:
exact ‹n ≃ 1›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.sqrt1
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
⊢ n ≃ 1 → n * n ≃ 1
Tactic:
intro (_ : n ≃ 1)
Proof state after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
x✝ : n ≃ 1
⊢ n * n ≃ 1
Theorem: Lean4Axiomatic.Natural.sqrt1
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
x✝ : n ≃ 1
⊢ n * n ≃ 1
Tactic:
have : n * n ≃ 1 := factors_eqv_1.mpr (And.intro ‹n ≃ 1› ‹n ≃ 1›)
Proof state after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
x✝ : n ≃ 1
this : n * n ≃ 1
⊢ n * n ≃ 1
Theorem: Lean4Axiomatic.Natural.sqrt1
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
x✝ : n ≃ 1
this : n * n ≃ 1
⊢ n * n ≃ 1
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.ind_diff_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
a₁ a₂ : Difference ℕ
a_eqv : a₁ ≃ a₂
⊢ fsubst a_eqv (Induction.Context.ind_diff ctx a₁) ≃ Induction.Context.ind_diff ctx a₂
Tactic:
revert a₁ a₂
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
⊢ ∀ {a₁ a₂ : Difference ℕ} {a_eqv : a₁ ≃ a₂},
    fsubst a_eqv (Induction.Context.ind_diff ctx a₁) ≃ Induction.Context.ind_diff ctx a₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.ind_diff_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
⊢ ∀ {a₁ a₂ : Difference ℕ} {a_eqv : a₁ ≃ a₂},
    fsubst a_eqv (Induction.Context.ind_diff ctx a₁) ≃ Induction.Context.ind_diff ctx a₂
Tactic:
intro (n₁——m₁) (n₂——m₂)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
⊢ ∀ {a_eqv : n₁——m₁ ≃ n₂——m₂},
    fsubst a_eqv (Induction.Context.ind_diff ctx (n₁——m₁)) ≃ Induction.Context.ind_diff ctx (n₂——m₂)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.ind_diff_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
⊢ ∀ {a_eqv : n₁——m₁ ≃ n₂——m₂},
    fsubst a_eqv (Induction.Context.ind_diff ctx (n₁——m₁)) ≃ Induction.Context.ind_diff ctx (n₂——m₂)
Tactic:
let a₁ := n₁——m₁
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
a₁ : Difference ℕ := n₁——m₁
⊢ ∀ {a_eqv : n₁——m₁ ≃ n₂——m₂},
    fsubst a_eqv (Induction.Context.ind_diff ctx (n₁——m₁)) ≃ Induction.Context.ind_diff ctx (n₂——m₂)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.ind_diff_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
a₁ : Difference ℕ := n₁——m₁
⊢ ∀ {a_eqv : n₁——m₁ ≃ n₂——m₂},
    fsubst a_eqv (Induction.Context.ind_diff ctx (n₁——m₁)) ≃ Induction.Context.ind_diff ctx (n₂——m₂)
Tactic:
let a₂ := n₂——m₂
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
a₁ : Difference ℕ := n₁——m₁
a₂ : Difference ℕ := n₂——m₂
⊢ ∀ {a_eqv : n₁——m₁ ≃ n₂——m₂},
    fsubst a_eqv (Induction.Context.ind_diff ctx (n₁——m₁)) ≃ Induction.Context.ind_diff ctx (n₂——m₂)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.ind_diff_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
a₁ : Difference ℕ := n₁——m₁
a₂ : Difference ℕ := n₂——m₂
⊢ ∀ {a_eqv : n₁——m₁ ≃ n₂——m₂},
    fsubst a_eqv (Induction.Context.ind_diff ctx (n₁——m₁)) ≃ Induction.Context.ind_diff ctx (n₂——m₂)
Tactic:
intro (_ : a₁ ≃ a₂)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
a₁ : Difference ℕ := n₁——m₁
a₂ : Difference ℕ := n₂——m₂
x✝ : a₁ ≃ a₂
⊢ fsubst x✝ (Induction.Context.ind_diff ctx (n₁——m₁)) ≃ Induction.Context.ind_diff ctx (n₂——m₂)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.ind_diff_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
a₁ : Difference ℕ := n₁——m₁
a₂ : Difference ℕ := n₂——m₂
x✝ : a₁ ≃ a₂
⊢ fsubst x✝ (Induction.Context.ind_diff ctx (n₁——m₁)) ≃ Induction.Context.ind_diff ctx (n₂——m₂)
Tactic:
show fsubst ‹a₁ ≃ a₂› (ctx.ind_diff a₁) ≃ ctx.ind_diff a₂
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
a₁ : Difference ℕ := n₁——m₁
a₂ : Difference ℕ := n₂——m₂
x✝ : a₁ ≃ a₂
⊢ fsubst x✝ (Induction.Context.ind_diff ctx a₁) ≃ Induction.Context.ind_diff ctx a₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.ind_diff_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
a₁ : Difference ℕ := n₁——m₁
a₂ : Difference ℕ := n₂——m₂
x✝ : a₁ ≃ a₂
⊢ fsubst x✝ (Induction.Context.ind_diff ctx a₁) ≃ Induction.Context.ind_diff ctx a₂
Tactic:
let d₁ := (n₁:Difference ℕ) - m₁
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
a₁ : Difference ℕ := n₁——m₁
a₂ : Difference ℕ := n₂——m₂
x✝ : a₁ ≃ a₂
d₁ : Difference ℕ := n₁——0 - m₁——0
⊢ fsubst x✝ (Induction.Context.ind_diff ctx a₁) ≃ Induction.Context.ind_diff ctx a₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.ind_diff_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
a₁ : Difference ℕ := n₁——m₁
a₂ : Difference ℕ := n₂——m₂
x✝ : a₁ ≃ a₂
d₁ : Difference ℕ := n₁——0 - m₁——0
⊢ fsubst x✝ (Induction.Context.ind_diff ctx a₁) ≃ Induction.Context.ind_diff ctx a₂
Tactic:
let d₂ := (n₂:Difference ℕ) - m₂
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
a₁ : Difference ℕ := n₁——m₁
a₂ : Difference ℕ := n₂——m₂
x✝ : a₁ ≃ a₂
d₁ : Difference ℕ := n₁——0 - m₁——0
d₂ : Difference ℕ := n₂——0 - m₂——0
⊢ fsubst x✝ (Induction.Context.ind_diff ctx a₁) ≃ Induction.Context.ind_diff ctx a₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.ind_diff_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
a₁ : Difference ℕ := n₁——m₁
a₂ : Difference ℕ := n₂——m₂
x✝ : a₁ ≃ a₂
d₁ : Difference ℕ := n₁——0 - m₁——0
d₂ : Difference ℕ := n₂——0 - m₂——0
⊢ fsubst x✝ (Induction.Context.ind_diff ctx a₁) ≃ Induction.Context.ind_diff ctx a₂
Tactic:
have : d₁ ≃ a₁ := sub_eqv_diff
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
a₁ : Difference ℕ := n₁——m₁
a₂ : Difference ℕ := n₂——m₂
x✝ : a₁ ≃ a₂
d₁ : Difference ℕ := n₁——0 - m₁——0
d₂ : Difference ℕ := n₂——0 - m₂——0
this : d₁ ≃ a₁
⊢ fsubst x✝ (Induction.Context.ind_diff ctx a₁) ≃ Induction.Context.ind_diff ctx a₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.ind_diff_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
a₁ : Difference ℕ := n₁——m₁
a₂ : Difference ℕ := n₂——m₂
x✝ : a₁ ≃ a₂
d₁ : Difference ℕ := n₁——0 - m₁——0
d₂ : Difference ℕ := n₂——0 - m₂——0
this : d₁ ≃ a₁
⊢ fsubst x✝ (Induction.Context.ind_diff ctx a₁) ≃ Induction.Context.ind_diff ctx a₂
Tactic:
have : d₂ ≃ a₂ := sub_eqv_diff
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
a₁ : Difference ℕ := n₁——m₁
a₂ : Difference ℕ := n₂——m₂
x✝ : a₁ ≃ a₂
d₁ : Difference ℕ := n₁——0 - m₁——0
d₂ : Difference ℕ := n₂——0 - m₂——0
this✝ : d₁ ≃ a₁
this : d₂ ≃ a₂
⊢ fsubst x✝ (Induction.Context.ind_diff ctx a₁) ≃ Induction.Context.ind_diff ctx a₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.ind_diff_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
a₁ : Difference ℕ := n₁——m₁
a₂ : Difference ℕ := n₂——m₂
x✝ : a₁ ≃ a₂
d₁ : Difference ℕ := n₁——0 - m₁——0
d₂ : Difference ℕ := n₂——0 - m₂——0
this✝ : d₁ ≃ a₁
this : d₂ ≃ a₂
⊢ fsubst x✝ (Induction.Context.ind_diff ctx a₁) ≃ Induction.Context.ind_diff ctx a₂
Tactic:
have : d₁ ≃ a₂ := Rel.trans ‹d₁ ≃ a₁› ‹a₁ ≃ a₂›
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
a₁ : Difference ℕ := n₁——m₁
a₂ : Difference ℕ := n₂——m₂
x✝ : a₁ ≃ a₂
d₁ : Difference ℕ := n₁——0 - m₁——0
d₂ : Difference ℕ := n₂——0 - m₂——0
this✝¹ : d₁ ≃ a₁
this✝ : d₂ ≃ a₂
this : d₁ ≃ a₂
⊢ fsubst x✝ (Induction.Context.ind_diff ctx a₁) ≃ Induction.Context.ind_diff ctx a₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.ind_diff_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
a₁ : Difference ℕ := n₁——m₁
a₂ : Difference ℕ := n₂——m₂
x✝ : a₁ ≃ a₂
d₁ : Difference ℕ := n₁——0 - m₁——0
d₂ : Difference ℕ := n₂——0 - m₂——0
this✝¹ : d₁ ≃ a₁
this✝ : d₂ ≃ a₂
this : d₁ ≃ a₂
⊢ fsubst x✝ (Induction.Context.ind_diff ctx a₁) ≃ Induction.Context.ind_diff ctx a₂
Tactic:
have : d₂ ≃ d₁ := Rel.trans ‹d₂ ≃ a₂› (Rel.symm ‹d₁ ≃ a₂›)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
a₁ : Difference ℕ := n₁——m₁
a₂ : Difference ℕ := n₂——m₂
x✝ : a₁ ≃ a₂
d₁ : Difference ℕ := n₁——0 - m₁——0
d₂ : Difference ℕ := n₂——0 - m₂——0
this✝² : d₁ ≃ a₁
this✝¹ : d₂ ≃ a₂
this✝ : d₁ ≃ a₂
this : d₂ ≃ d₁
⊢ fsubst x✝ (Induction.Context.ind_diff ctx a₁) ≃ Induction.Context.ind_diff ctx a₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.ind_diff_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
a₁ : Difference ℕ := n₁——m₁
a₂ : Difference ℕ := n₂——m₂
x✝ : a₁ ≃ a₂
d₁ : Difference ℕ := n₁——0 - m₁——0
d₂ : Difference ℕ := n₂——0 - m₂——0
this✝² : d₁ ≃ a₁
this✝¹ : d₂ ≃ a₂
this✝ : d₁ ≃ a₂
this : d₂ ≃ d₁
⊢ fsubst x✝ (Induction.Context.ind_diff ctx a₁) ≃ Induction.Context.ind_diff ctx a₂
Tactic:
let od₁ := ctx.on_diff n₁ m₁
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
a₁ : Difference ℕ := n₁——m₁
a₂ : Difference ℕ := n₂——m₂
x✝ : a₁ ≃ a₂
d₁ : Difference ℕ := n₁——0 - m₁——0
d₂ : Difference ℕ := n₂——0 - m₂——0
this✝² : d₁ ≃ a₁
this✝¹ : d₂ ≃ a₂
this✝ : d₁ ≃ a₂
this : d₂ ≃ d₁
od₁ : motive (Coe.coe n₁ - Coe.coe m₁) := Induction.Context.on_diff n₁ m₁
⊢ fsubst x✝ (Induction.Context.ind_diff ctx a₁) ≃ Induction.Context.ind_diff ctx a₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.ind_diff_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
a₁ : Difference ℕ := n₁——m₁
a₂ : Difference ℕ := n₂——m₂
x✝ : a₁ ≃ a₂
d₁ : Difference ℕ := n₁——0 - m₁——0
d₂ : Difference ℕ := n₂——0 - m₂——0
this✝² : d₁ ≃ a₁
this✝¹ : d₂ ≃ a₂
this✝ : d₁ ≃ a₂
this : d₂ ≃ d₁
od₁ : motive (Coe.coe n₁ - Coe.coe m₁) := Induction.Context.on_diff n₁ m₁
⊢ fsubst x✝ (Induction.Context.ind_diff ctx a₁) ≃ Induction.Context.ind_diff ctx a₂
Tactic:
let od₂ := ctx.on_diff n₂ m₂
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
a₁ : Difference ℕ := n₁——m₁
a₂ : Difference ℕ := n₂——m₂
x✝ : a₁ ≃ a₂
d₁ : Difference ℕ := n₁——0 - m₁——0
d₂ : Difference ℕ := n₂——0 - m₂——0
this✝² : d₁ ≃ a₁
this✝¹ : d₂ ≃ a₂
this✝ : d₁ ≃ a₂
this : d₂ ≃ d₁
od₁ : motive (Coe.coe n₁ - Coe.coe m₁) := Induction.Context.on_diff n₁ m₁
od₂ : motive (Coe.coe n₂ - Coe.coe m₂) := Induction.Context.on_diff n₂ m₂
⊢ fsubst x✝ (Induction.Context.ind_diff ctx a₁) ≃ Induction.Context.ind_diff ctx a₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.ind_diff_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
a₁ : Difference ℕ := n₁——m₁
a₂ : Difference ℕ := n₂——m₂
x✝ : a₁ ≃ a₂
d₁ : Difference ℕ := n₁——0 - m₁——0
d₂ : Difference ℕ := n₂——0 - m₂——0
this✝² : d₁ ≃ a₁
this✝¹ : d₂ ≃ a₂
this✝ : d₁ ≃ a₂
this : d₂ ≃ d₁
od₁ : motive (Coe.coe n₁ - Coe.coe m₁) := Induction.Context.on_diff n₁ m₁
od₂ : motive (Coe.coe n₂ - Coe.coe m₂) := Induction.Context.on_diff n₂ m₂
⊢ fsubst x✝ (Induction.Context.ind_diff ctx a₁) ≃ Induction.Context.ind_diff ctx a₂
Tactic:
have od_subst : od₁ ≃ fsubst ‹d₂ ≃ d₁› od₂ := Rel.symm ctx.on_diff_subst
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
a₁ : Difference ℕ := n₁——m₁
a₂ : Difference ℕ := n₂——m₂
x✝ : a₁ ≃ a₂
d₁ : Difference ℕ := n₁——0 - m₁——0
d₂ : Difference ℕ := n₂——0 - m₂——0
this✝² : d₁ ≃ a₁
this✝¹ : d₂ ≃ a₂
this✝ : d₁ ≃ a₂
this : d₂ ≃ d₁
od₁ : motive (Coe.coe n₁ - Coe.coe m₁) := Induction.Context.on_diff n₁ m₁
od₂ : motive (Coe.coe n₂ - Coe.coe m₂) := Induction.Context.on_diff n₂ m₂
od_subst : od₁ ≃ fsubst this od₂
⊢ fsubst x✝ (Induction.Context.ind_diff ctx a₁) ≃ Induction.Context.ind_diff ctx a₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.ind_diff_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n₁ m₁ n₂ m₂ : ℕ
a₁ : Difference ℕ := n₁——m₁
a₂ : Difference ℕ := n₂——m₂
x✝ : a₁ ≃ a₂
d₁ : Difference ℕ := n₁——0 - m₁——0
d₂ : Difference ℕ := n₂——0 - m₂——0
this✝² : d₁ ≃ a₁
this✝¹ : d₂ ≃ a₂
this✝ : d₁ ≃ a₂
this : d₂ ≃ d₁
od₁ : motive (Coe.coe n₁ - Coe.coe m₁) := Induction.Context.on_diff n₁ m₁
od₂ : motive (Coe.coe n₂ - Coe.coe m₂) := Induction.Context.on_diff n₂ m₂
od_subst : od₁ ≃ fsubst this od₂
⊢ fsubst x✝ (Induction.Context.ind_diff ctx a₁) ≃ Induction.Context.ind_diff ctx a₂
Tactic:
calc
  _ = fsubst ‹a₁ ≃ a₂› (ctx.ind_diff a₁)         := rfl
  _ = fsubst ‹a₁ ≃ a₂› (fsubst ‹d₁ ≃ a₁› od₁)    := rfl
  _ ≃ fsubst (Rel.trans ‹d₁ ≃ a₁› ‹a₁ ≃ a₂›) od₁ := fsubst_trans
  _ = fsubst ‹d₁ ≃ a₂› od₁                       := rfl
  _ ≃ fsubst ‹d₁ ≃ a₂› (fsubst ‹d₂ ≃ d₁› od₂)    := fsubst_substR od_subst
  _ ≃ fsubst (Rel.trans ‹d₂ ≃ d₁› ‹d₁ ≃ a₂›) od₂ := fsubst_trans
  _ = fsubst ‹d₂ ≃ a₂› od₂                       := rfl
  _ = ctx.ind_diff a₂                            := rfl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.ind_diff_eval
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n m : ℕ
⊢ Induction.Context.ind_diff ctx (n——0 - m——0) ≃ Induction.Context.on_diff n m
Tactic:
have sed : (n:Difference ℕ) - m ≃ n——m := sub_eqv_diff
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n m : ℕ
sed : n——0 - m——0 ≃ n——m
⊢ Induction.Context.ind_diff ctx (n——0 - m——0) ≃ Induction.Context.on_diff n m
Theorem: Lean4Axiomatic.Integer.Impl.Difference.ind_diff_eval
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n m : ℕ
sed : n——0 - m——0 ≃ n——m
⊢ Induction.Context.ind_diff ctx (n——0 - m——0) ≃ Induction.Context.on_diff n m
Tactic:
have des : n——m ≃ n - m := Rel.symm sed
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n m : ℕ
sed : n——0 - m——0 ≃ n——m
des : n——m ≃ n——0 - m——0
⊢ Induction.Context.ind_diff ctx (n——0 - m——0) ≃ Induction.Context.on_diff n m
Theorem: Lean4Axiomatic.Integer.Impl.Difference.ind_diff_eval
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
motive : Difference ℕ → Sort u
inst✝ : IndexedFamily motive
ctx : Induction.Context motive
n m : ℕ
sed : n——0 - m——0 ≃ n——m
des : n——m ≃ n——0 - m——0
⊢ Induction.Context.ind_diff ctx (n——0 - m——0) ≃ Induction.Context.on_diff n m
Tactic:
calc
  _ = ctx.ind_diff (n - m)                         := rfl
  _ ≃ fsubst des (ctx.ind_diff (n——m))             := Rel.symm ind_diff_subst
  _ = fsubst des (fsubst sed (ctx.on_diff n m))    := rfl
  _ ≃ fsubst (Rel.trans sed des) (ctx.on_diff n m) := fsubst_trans
  _ = fsubst Rel.refl (ctx.on_diff n m)            := rfl
  _ ≃ ctx.on_diff n m                              := fsubst_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Generic.min_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ Ordered.min p q ≃ p ∨ Ordered.min p q ≃ q
Tactic:
show
  (if decide (p < q) then p else q) ≃ p ∨
  (if decide (p < q) then p else q) ≃ q
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ (if decide (p < q) = true then p else q) ≃ p ∨ (if decide (p < q) = true then p else q) ≃ q
Theorem: Lean4Axiomatic.Rational.Impl.Generic.min_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ (if decide (p < q) = true then p else q) ≃ p ∨ (if decide (p < q) = true then p else q) ≃ q
Tactic:
match decide (p < q) with
| true =>
  apply Or.inl
  show (if true then p else q) ≃ p
  show p ≃ p
  exact eqv_refl
| false =>
  apply Or.inr
  show (if false then p else q) ≃ q
  show q ≃ q
  exact eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Generic.min_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ (if true = true then p else q) ≃ p ∨ (if true = true then p else q) ≃ q
Tactic:
apply Or.inl
Proof state after:
case h
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ (if true = true then p else q) ≃ p
Theorem: Lean4Axiomatic.Rational.Impl.Generic.min_cases
Proof state before:
case h
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ (if true = true then p else q) ≃ p
Tactic:
show p ≃ p
Proof state after:
case h
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ p ≃ p
Theorem: Lean4Axiomatic.Rational.Impl.Generic.min_cases
Proof state before:
case h
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ p ≃ p
Tactic:
exact eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Generic.min_cases
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ (if false = true then p else q) ≃ p ∨ (if false = true then p else q) ≃ q
Tactic:
apply Or.inr
Proof state after:
case h
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ (if false = true then p else q) ≃ q
Theorem: Lean4Axiomatic.Rational.Impl.Generic.min_cases
Proof state before:
case h
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ (if false = true then p else q) ≃ q
Tactic:
show q ≃ q
Proof state after:
case h
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ q ≃ q
Theorem: Lean4Axiomatic.Rational.Impl.Generic.min_cases
Proof state before:
case h
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ q ≃ q
Tactic:
exact eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Generic.min_leL
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ Ordered.min p q ≤ p
Tactic:
show (if decide (p < q) then p else q) ≤ p
Proof state after:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ (if decide (p < q) = true then p else q) ≤ p
Theorem: Lean4Axiomatic.Rational.Impl.Generic.min_leL
Proof state before:
ℕ ℤ ℚ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Sign ℚ
inst✝¹ : Subtraction ℚ
inst✝ : Order ℚ
p q : ℚ
⊢ (if decide (p < q) = true then p else q) ≤ p
Tactic:
match eq : decide (p < q) with
| true =>
  show (if true then p else q) ≤ p
  show p ≤ p
  exact le_refl
| false =>
  show (if false then p else q) ≤ p
  show q ≤ p
  have : ¬(p < q) := ofBoolUsing_eq_false eq
  have : sgn (p - q) ≄ -1 := mt lt_sgn.mpr this
  have : q ≤ p := ge_sgn.mpr this
  exact this
Proof state after:
no goals