internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_trichotomy
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
this : AA.OneOfThree (p.numerator ≃ 0) (Positive p.numerator) (Negative p.numerator)
b✝ : Positive p.numerator
⊢ AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
Tactic:
have : sgn p ≃ 1 := calc
  sgn p           ≃ _ := Rel.refl
  sgn p.numerator ≃ _ := Integer.sgn_positive.mp ‹Positive p.numerator›
  1               ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
this✝ : AA.OneOfThree (p.numerator ≃ 0) (Positive p.numerator) (Negative p.numerator)
b✝ : Positive p.numerator
this : sgn p ≃ 1
⊢ AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_trichotomy
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
this✝ : AA.OneOfThree (p.numerator ≃ 0) (Positive p.numerator) (Negative p.numerator)
b✝ : Positive p.numerator
this : sgn p ≃ 1
⊢ AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
Tactic:
exact AA.OneOfThree.second this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_trichotomy
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
this : AA.OneOfThree (p.numerator ≃ 0) (Positive p.numerator) (Negative p.numerator)
c✝ : Negative p.numerator
⊢ AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
Tactic:
have : sgn p ≃ -1 := calc
  sgn p           ≃ _ := Rel.refl
  sgn p.numerator ≃ _ := Integer.sgn_negative.mp ‹Negative p.numerator›
  (-1)            ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
this✝ : AA.OneOfThree (p.numerator ≃ 0) (Positive p.numerator) (Negative p.numerator)
c✝ : Negative p.numerator
this : sgn p ≃ -1
⊢ AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.sgn_trichotomy
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
this✝ : AA.OneOfThree (p.numerator ≃ 0) (Positive p.numerator) (Negative p.numerator)
c✝ : Negative p.numerator
this : sgn p ≃ -1
⊢ AA.OneOfThree (sgn p ≃ 0) (sgn p ≃ 1) (sgn p ≃ -1)
Tactic:
exact AA.OneOfThree.third this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.positive_subst
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n₁ n₂ : ℕ
⊢ n₁ ≃ n₂ → Positive n₁ → Positive n₂
Tactic:
intro (_ : n₁ ≃ n₂) (_ : Positive n₁)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n₁ n₂ : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : Positive n₁
⊢ Positive n₂
Theorem: Lean4Axiomatic.Natural.positive_subst
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n₁ n₂ : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : Positive n₁
⊢ Positive n₂
Tactic:
have : n₁ ≄ 0 := Signed.positive_defn.mp ‹Positive n₁›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n₁ n₂ : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : Positive n₁
this : n₁ ≄ 0
⊢ Positive n₂
Theorem: Lean4Axiomatic.Natural.positive_subst
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n₁ n₂ : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : Positive n₁
this : n₁ ≄ 0
⊢ Positive n₂
Tactic:
have : n₂ ≄ 0 := AA.neqv_substL ‹n₁ ≃ n₂› ‹n₁ ≄ 0›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n₁ n₂ : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : Positive n₁
this✝ : n₁ ≄ 0
this : n₂ ≄ 0
⊢ Positive n₂
Theorem: Lean4Axiomatic.Natural.positive_subst
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n₁ n₂ : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : Positive n₁
this✝ : n₁ ≄ 0
this : n₂ ≄ 0
⊢ Positive n₂
Tactic:
have : Positive n₂ := Signed.positive_defn.mpr ‹n₂ ≄ 0›
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n₁ n₂ : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : Positive n₁
this✝¹ : n₁ ≄ 0
this✝ : n₂ ≄ 0
this : Positive n₂
⊢ Positive n₂
Theorem: Lean4Axiomatic.Natural.positive_subst
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n₁ n₂ : ℕ
x✝¹ : n₁ ≃ n₂
x✝ : Positive n₁
this✝¹ : n₁ ≄ 0
this✝ : n₂ ≄ 0
this : Positive n₂
⊢ Positive n₂
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.positive_step
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
⊢ Positive n → ∃ m, step m ≃ n
Tactic:
apply cases_on (motive := λ n => Positive n → ∃ m, step m ≃ n) n
Proof state after:
case zero
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
⊢ Positive 0 → ∃ m, step m ≃ 0

case step
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
⊢ ∀ (m : ℕ), Positive (step m) → ∃ m_1, step m_1 ≃ step m
Theorem: Lean4Axiomatic.Natural.positive_step
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
⊢ Positive 0 → ∃ m, step m ≃ 0
Tactic:
case zero =>
  intro (_ : Positive (0:ℕ))
  apply False.elim
  show False
  have : (0:ℕ) ≄ 0 := Signed.positive_defn.mp ‹Positive (0:ℕ)›
  apply this
  show 0 ≃ 0
  exact Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.positive_step
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
⊢ ∀ (m : ℕ), Positive (step m) → ∃ m_1, step m_1 ≃ step m
Tactic:
case step =>
  intro n (_ : Positive (step n))
  exists n
  show step n ≃ step n
  exact Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.positive_step
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
⊢ Positive 0 → ∃ m, step m ≃ 0
Tactic:
intro (_ : Positive (0:ℕ))
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
x✝ : Positive 0
⊢ ∃ m, step m ≃ 0
Theorem: Lean4Axiomatic.Natural.positive_step
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
x✝ : Positive 0
⊢ ∃ m, step m ≃ 0
Tactic:
apply False.elim
Proof state after:
case h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
x✝ : Positive 0
⊢ False
Theorem: Lean4Axiomatic.Natural.positive_step
Proof state before:
case h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
x✝ : Positive 0
⊢ False
Tactic:
have : (0:ℕ) ≄ 0 := Signed.positive_defn.mp ‹Positive (0:ℕ)›
Proof state after:
case h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
x✝ : Positive 0
this : 0 ≄ 0
⊢ False
Theorem: Lean4Axiomatic.Natural.positive_step
Proof state before:
case h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
x✝ : Positive 0
this : 0 ≄ 0
⊢ False
Tactic:
apply this
Proof state after:
case h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
x✝ : Positive 0
this : 0 ≄ 0
⊢ 0 ≃ 0
Theorem: Lean4Axiomatic.Natural.positive_step
Proof state before:
case h
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
x✝ : Positive 0
this : 0 ≄ 0
⊢ 0 ≃ 0
Tactic:
exact Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.positive_step
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n : ℕ
⊢ ∀ (m : ℕ), Positive (step m) → ∃ m_1, step m_1 ≃ step m
Tactic:
intro n (_ : Positive (step n))
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n✝ n : ℕ
x✝ : Positive (step n)
⊢ ∃ m, step m ≃ step n
Theorem: Lean4Axiomatic.Natural.positive_step
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n✝ n : ℕ
x✝ : Positive (step n)
⊢ ∃ m, step m ≃ step n
Tactic:
exists n
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n✝ n : ℕ
x✝ : Positive (step n)
⊢ step n ≃ step n
Theorem: Lean4Axiomatic.Natural.positive_step
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n✝ n : ℕ
x✝ : Positive (step n)
⊢ step n ≃ step n
Tactic:
exact Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.positive_add
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m : ℕ
⊢ Positive n → Positive (n + m)
Tactic:
intro (_ : Positive n)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m : ℕ
x✝ : Positive n
⊢ Positive (n + m)
Theorem: Lean4Axiomatic.Natural.positive_add
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m : ℕ
x✝ : Positive n
⊢ Positive (n + m)
Tactic:
apply cases_on (motive := λ m => Positive (n + m)) m
Proof state after:
case zero
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m : ℕ
x✝ : Positive n
⊢ Positive (n + 0)

case step
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m : ℕ
x✝ : Positive n
⊢ ∀ (m : ℕ), Positive (n + step m)
Theorem: Lean4Axiomatic.Natural.positive_add
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m : ℕ
x✝ : Positive n
⊢ Positive (n + 0)
Tactic:
case zero =>
  show Positive (n + 0)
  apply AA.substFn (Rel.symm add_zero)
  exact ‹Positive n›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.positive_add
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m : ℕ
x✝ : Positive n
⊢ ∀ (m : ℕ), Positive (n + step m)
Tactic:
case step =>
  intro m
  show Positive (n + step m)
  apply AA.substFn (Rel.symm add_step)
  show Positive (step (n + m))
  apply Signed.positive_defn.mpr
  show step (n + m) ≄ 0
  exact step_neqv_zero
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.positive_add
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m : ℕ
x✝ : Positive n
⊢ Positive (n + 0)
Tactic:
apply AA.substFn (Rel.symm add_zero)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m : ℕ
x✝ : Positive n
⊢ Positive n
Theorem: Lean4Axiomatic.Natural.positive_add
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m : ℕ
x✝ : Positive n
⊢ Positive n
Tactic:
exact ‹Positive n›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.positive_add
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m : ℕ
x✝ : Positive n
⊢ ∀ (m : ℕ), Positive (n + step m)
Tactic:
intro m
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m✝ : ℕ
x✝ : Positive n
m : ℕ
⊢ Positive (n + step m)
Theorem: Lean4Axiomatic.Natural.positive_add
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m✝ : ℕ
x✝ : Positive n
m : ℕ
⊢ Positive (n + step m)
Tactic:
apply AA.substFn (Rel.symm add_step)
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m✝ : ℕ
x✝ : Positive n
m : ℕ
⊢ Positive (step (n + m))
Theorem: Lean4Axiomatic.Natural.positive_add
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m✝ : ℕ
x✝ : Positive n
m : ℕ
⊢ Positive (step (n + m))
Tactic:
apply Signed.positive_defn.mpr
Proof state after:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m✝ : ℕ
x✝ : Positive n
m : ℕ
⊢ step (n + m) ≄ 0
Theorem: Lean4Axiomatic.Natural.positive_add
Proof state before:
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
n m✝ : ℕ
x✝ : Positive n
m : ℕ
⊢ step (n + m) ≄ 0
Tactic:
exact step_neqv_zero
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.AsRatio_subst
Proof state before:
ℕ ℤ : Type
inst✝⁷ : Natural ℕ
inst✝⁶ : Integer ℤ
ℚ : Type
inst✝⁵ : Core ℚ
inst✝⁴ : Addition ℚ
inst✝³ : Multiplication ℚ
inst✝² : Negation ℚ
inst✝¹ : Reciprocation ℚ
inst✝ : Division ℚ
a b : ℚ
⊢ a ≃ b → AsRatio a → AsRatio b
Tactic:
intro (_ : a ≃ b) (_ : AsRatio a)
Proof state after:
ℕ ℤ : Type
inst✝⁷ : Natural ℕ
inst✝⁶ : Integer ℤ
ℚ : Type
inst✝⁵ : Core ℚ
inst✝⁴ : Addition ℚ
inst✝³ : Multiplication ℚ
inst✝² : Negation ℚ
inst✝¹ : Reciprocation ℚ
inst✝ : Division ℚ
a b : ℚ
x✝¹ : a ≃ b
x✝ : AsRatio a
⊢ AsRatio b
Theorem: Lean4Axiomatic.Rational.AsRatio_subst
Proof state before:
ℕ ℤ : Type
inst✝⁷ : Natural ℕ
inst✝⁶ : Integer ℤ
ℚ : Type
inst✝⁵ : Core ℚ
inst✝⁴ : Addition ℚ
inst✝³ : Multiplication ℚ
inst✝² : Negation ℚ
inst✝¹ : Reciprocation ℚ
inst✝ : Division ℚ
a b : ℚ
x✝¹ : a ≃ b
x✝ : AsRatio a
⊢ AsRatio b
Tactic:
have (AsRatio.intro (n : ℤ) (d : ℤ) (_ : Integer.Nonzero d) eqv)
  := ‹AsRatio a›
Proof state after:
ℕ ℤ : Type
inst✝⁷ : Natural ℕ
inst✝⁶ : Integer ℤ
ℚ : Type
inst✝⁵ : Core ℚ
inst✝⁴ : Addition ℚ
inst✝³ : Multiplication ℚ
inst✝² : Negation ℚ
inst✝¹ : Reciprocation ℚ
inst✝ : Division ℚ
a b : ℚ
x✝¹ : a ≃ b
x✝ : AsRatio a
n d : ℤ
b_nonzero✝ : Integer.Nonzero d
eqv : a ≃ from_integer n / from_integer d
⊢ AsRatio b
Theorem: Lean4Axiomatic.Rational.AsRatio_subst
Proof state before:
ℕ ℤ : Type
inst✝⁷ : Natural ℕ
inst✝⁶ : Integer ℤ
ℚ : Type
inst✝⁵ : Core ℚ
inst✝⁴ : Addition ℚ
inst✝³ : Multiplication ℚ
inst✝² : Negation ℚ
inst✝¹ : Reciprocation ℚ
inst✝ : Division ℚ
a b : ℚ
x✝¹ : a ≃ b
x✝ : AsRatio a
n d : ℤ
b_nonzero✝ : Integer.Nonzero d
eqv : a ≃ from_integer n / from_integer d
⊢ AsRatio b
Tactic:
have : a ≃ n / d := eqv
Proof state after:
ℕ ℤ : Type
inst✝⁷ : Natural ℕ
inst✝⁶ : Integer ℤ
ℚ : Type
inst✝⁵ : Core ℚ
inst✝⁴ : Addition ℚ
inst✝³ : Multiplication ℚ
inst✝² : Negation ℚ
inst✝¹ : Reciprocation ℚ
inst✝ : Division ℚ
a b : ℚ
x✝¹ : a ≃ b
x✝ : AsRatio a
n d : ℤ
b_nonzero✝ : Integer.Nonzero d
eqv this : a ≃ from_integer n / from_integer d
⊢ AsRatio b
Theorem: Lean4Axiomatic.Rational.AsRatio_subst
Proof state before:
ℕ ℤ : Type
inst✝⁷ : Natural ℕ
inst✝⁶ : Integer ℤ
ℚ : Type
inst✝⁵ : Core ℚ
inst✝⁴ : Addition ℚ
inst✝³ : Multiplication ℚ
inst✝² : Negation ℚ
inst✝¹ : Reciprocation ℚ
inst✝ : Division ℚ
a b : ℚ
x✝¹ : a ≃ b
x✝ : AsRatio a
n d : ℤ
b_nonzero✝ : Integer.Nonzero d
eqv this : a ≃ from_integer n / from_integer d
⊢ AsRatio b
Tactic:
have : b ≃ n / d := calc
  _ ≃ b     := eqv_refl
  _ ≃ a     := eqv_symm ‹a ≃ b›
  _ ≃ n / d := ‹a ≃ n / d›
Proof state after:
ℕ ℤ : Type
inst✝⁷ : Natural ℕ
inst✝⁶ : Integer ℤ
ℚ : Type
inst✝⁵ : Core ℚ
inst✝⁴ : Addition ℚ
inst✝³ : Multiplication ℚ
inst✝² : Negation ℚ
inst✝¹ : Reciprocation ℚ
inst✝ : Division ℚ
a b : ℚ
x✝¹ : a ≃ b
x✝ : AsRatio a
n d : ℤ
b_nonzero✝ : Integer.Nonzero d
eqv this✝ : a ≃ from_integer n / from_integer d
this : b ≃ from_integer n / from_integer d
⊢ AsRatio b
Theorem: Lean4Axiomatic.Rational.AsRatio_subst
Proof state before:
ℕ ℤ : Type
inst✝⁷ : Natural ℕ
inst✝⁶ : Integer ℤ
ℚ : Type
inst✝⁵ : Core ℚ
inst✝⁴ : Addition ℚ
inst✝³ : Multiplication ℚ
inst✝² : Negation ℚ
inst✝¹ : Reciprocation ℚ
inst✝ : Division ℚ
a b : ℚ
x✝¹ : a ≃ b
x✝ : AsRatio a
n d : ℤ
b_nonzero✝ : Integer.Nonzero d
eqv this✝ : a ≃ from_integer n / from_integer d
this : b ≃ from_integer n / from_integer d
⊢ AsRatio b
Tactic:
exact AsRatio.intro n d ‹Integer.Nonzero d› ‹b ≃ n / d›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.as_ratio
Proof state before:
ℕ ℤ : Type
inst✝⁷ : Natural ℕ
inst✝⁶ : Integer ℤ
ℚ : Type
inst✝⁵ : Core ℚ
inst✝⁴ : Addition ℚ
inst✝³ : Multiplication ℚ
inst✝² : Negation ℚ
inst✝¹ : Reciprocation ℚ
inst✝ : Division ℚ
p : ℚ
⊢ AsRatio p
Tactic:
apply ind_fraction_on p
Proof state after:
ℕ ℤ : Type
inst✝⁷ : Natural ℕ
inst✝⁶ : Integer ℤ
ℚ : Type
inst✝⁵ : Core ℚ
inst✝⁴ : Addition ℚ
inst✝³ : Multiplication ℚ
inst✝² : Negation ℚ
inst✝¹ : Reciprocation ℚ
inst✝ : Division ℚ
p : ℚ
⊢ ∀ (a b : ℤ) [inst : Integer.Nonzero b], AsRatio (from_integer a / from_integer b)
Theorem: Lean4Axiomatic.Rational.as_ratio
Proof state before:
ℕ ℤ : Type
inst✝⁷ : Natural ℕ
inst✝⁶ : Integer ℤ
ℚ : Type
inst✝⁵ : Core ℚ
inst✝⁴ : Addition ℚ
inst✝³ : Multiplication ℚ
inst✝² : Negation ℚ
inst✝¹ : Reciprocation ℚ
inst✝ : Division ℚ
p : ℚ
⊢ ∀ (a b : ℤ) [inst : Integer.Nonzero b], AsRatio (from_integer a / from_integer b)
Tactic:
intro (a : ℤ) (b : ℤ) (_ : Integer.Nonzero b)
Proof state after:
ℕ ℤ : Type
inst✝⁷ : Natural ℕ
inst✝⁶ : Integer ℤ
ℚ : Type
inst✝⁵ : Core ℚ
inst✝⁴ : Addition ℚ
inst✝³ : Multiplication ℚ
inst✝² : Negation ℚ
inst✝¹ : Reciprocation ℚ
inst✝ : Division ℚ
p : ℚ
a b : ℤ
x✝ : Integer.Nonzero b
⊢ AsRatio (from_integer a / from_integer b)
Theorem: Lean4Axiomatic.Rational.as_ratio
Proof state before:
ℕ ℤ : Type
inst✝⁷ : Natural ℕ
inst✝⁶ : Integer ℤ
ℚ : Type
inst✝⁵ : Core ℚ
inst✝⁴ : Addition ℚ
inst✝³ : Multiplication ℚ
inst✝² : Negation ℚ
inst✝¹ : Reciprocation ℚ
inst✝ : Division ℚ
p : ℚ
a b : ℤ
x✝ : Integer.Nonzero b
⊢ AsRatio (from_integer a / from_integer b)
Tactic:
exact AsRatio.intro a b ‹Integer.Nonzero b› eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.div_substL
Proof state before:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p₁ p₂ q : ℚ
inst✝ : AP (q ≄ 0)
⊢ p₁ ≃ p₂ → p₁ / q ≃ p₂ / q
Tactic:
intro (_ : p₁ ≃ p₂)
Proof state after:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p₁ p₂ q : ℚ
inst✝ : AP (q ≄ 0)
x✝ : p₁ ≃ p₂
⊢ p₁ / q ≃ p₂ / q
Theorem: Lean4Axiomatic.Rational.div_substL
Proof state before:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p₁ p₂ q : ℚ
inst✝ : AP (q ≄ 0)
x✝ : p₁ ≃ p₂
⊢ p₁ / q ≃ p₂ / q
Tactic:
calc
  p₁ / q   ≃ _ := div_mul_recip
  p₁ * q⁻¹ ≃ _ := mul_substL ‹p₁ ≃ p₂›
  p₂ * q⁻¹ ≃ _ := eqv_symm div_mul_recip
  p₂ / q   ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.div_substR
Proof state before:
ℕ ℤ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
ℚ : Type
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
p₁ p₂ q : ℚ
inst✝¹ : AP (p₁ ≄ 0)
inst✝ : AP (p₂ ≄ 0)
⊢ p₁ ≃ p₂ → q / p₁ ≃ q / p₂
Tactic:
intro (_ : p₁ ≃ p₂)
Proof state after:
ℕ ℤ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
ℚ : Type
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
p₁ p₂ q : ℚ
inst✝¹ : AP (p₁ ≄ 0)
inst✝ : AP (p₂ ≄ 0)
x✝ : p₁ ≃ p₂
⊢ q / p₁ ≃ q / p₂
Theorem: Lean4Axiomatic.Rational.div_substR
Proof state before:
ℕ ℤ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
ℚ : Type
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
p₁ p₂ q : ℚ
inst✝¹ : AP (p₁ ≄ 0)
inst✝ : AP (p₂ ≄ 0)
x✝ : p₁ ≃ p₂
⊢ q / p₁ ≃ q / p₂
Tactic:
calc
  q / p₁   ≃ _ := div_mul_recip
  q * p₁⁻¹ ≃ _ := mul_substR (recip_subst ‹p₁ ≃ p₂›)
  q * p₂⁻¹ ≃ _ := eqv_symm div_mul_recip
  q / p₂   ≃ _ := eqv_refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.div_eqv_1
Proof state before:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
⊢ p / q ≃ 1 ↔ p ≃ q
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
⊢ p / q ≃ 1 → p ≃ q

case mpr
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
⊢ p ≃ q → p / q ≃ 1
Theorem: Lean4Axiomatic.Rational.div_eqv_1
Proof state before:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
⊢ p / q ≃ 1 → p ≃ q
Tactic:
case mp =>
  intro (_ : p/q ≃ 1)
  show p ≃ q
  calc
    _ ≃ p             := eqv_refl
    _ ≃ p * 1         := eqv_symm mul_identR
    _ ≃ p * (q⁻¹ * q) := mul_substR (eqv_symm mul_inverseL)
    _ ≃ (p * q⁻¹) * q := eqv_symm mul_assoc
    _ ≃ (p/q) * q     := mul_substL (eqv_symm div_mul_recip)
    _ ≃ 1 * q         := mul_substL ‹p/q ≃ 1›
    _ ≃ q             := mul_identL
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.div_eqv_1
Proof state before:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
⊢ p ≃ q → p / q ≃ 1
Tactic:
case mpr =>
  intro (_ : p ≃ q)
  show p/q ≃ 1
  calc
    _ ≃ p/q := eqv_refl
    _ ≃ q/q := div_substL ‹p ≃ q›
    _ ≃ 1   := div_same
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.div_eqv_1
Proof state before:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
⊢ p / q ≃ 1 → p ≃ q
Tactic:
intro (_ : p/q ≃ 1)
Proof state after:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
x✝ : p / q ≃ 1
⊢ p ≃ q
Theorem: Lean4Axiomatic.Rational.div_eqv_1
Proof state before:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
x✝ : p / q ≃ 1
⊢ p ≃ q
Tactic:
calc
  _ ≃ p             := eqv_refl
  _ ≃ p * 1         := eqv_symm mul_identR
  _ ≃ p * (q⁻¹ * q) := mul_substR (eqv_symm mul_inverseL)
  _ ≃ (p * q⁻¹) * q := eqv_symm mul_assoc
  _ ≃ (p/q) * q     := mul_substL (eqv_symm div_mul_recip)
  _ ≃ 1 * q         := mul_substL ‹p/q ≃ 1›
  _ ≃ q             := mul_identL
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.div_eqv_1
Proof state before:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
⊢ p ≃ q → p / q ≃ 1
Tactic:
intro (_ : p ≃ q)
Proof state after:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
x✝ : p ≃ q
⊢ p / q ≃ 1
Theorem: Lean4Axiomatic.Rational.div_eqv_1
Proof state before:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p q : ℚ
inst✝ : AP (q ≄ 0)
x✝ : p ≃ q
⊢ p / q ≃ 1
Tactic:
calc
  _ ≃ p/q := eqv_refl
  _ ≃ q/q := div_substL ‹p ≃ q›
  _ ≃ 1   := div_same
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.recip_preserves_nonzero
Proof state before:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
⊢ p⁻¹ ≄ 0
Tactic:
intro (_ : p⁻¹ ≃ 0)
Proof state after:
ℕ ℤ : Type
inst✝⁸ : Natural ℕ
inst✝⁷ : Integer ℤ
ℚ : Type
inst✝⁶ : Core ℚ
inst✝⁵ : Addition ℚ
inst✝⁴ : Multiplication ℚ
inst✝³ : Negation ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
x✝ : p⁻¹ ≃ 0
⊢ False