internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Integer.Impl.Difference.trans
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ c₁ c₂ : ℕ
x✝¹ : a₁ + b₂ ≃ b₁ + a₂
x✝ : b₁ + c₂ ≃ c₁ + b₂
⊢ a₁——a₂ ≃ c₁——c₂
Tactic:
show a₁ + c₂ ≃ c₁ + a₂
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ c₁ c₂ : ℕ
x✝¹ : a₁ + b₂ ≃ b₁ + a₂
x✝ : b₁ + c₂ ≃ c₁ + b₂
⊢ a₁ + c₂ ≃ c₁ + a₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.trans
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ c₁ c₂ : ℕ
x✝¹ : a₁ + b₂ ≃ b₁ + a₂
x✝ : b₁ + c₂ ≃ c₁ + b₂
⊢ a₁ + c₂ ≃ c₁ + a₂
Tactic:
have : (a₁ + c₂) + (b₂ + b₁) ≃ (c₁ + a₂) + (b₂ + b₁) := calc
  (a₁ + c₂) + (b₂ + b₁) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (a₁ + b₂) + (c₂ + b₁) ≃ _ := AA.substL ‹a₁ + b₂ ≃ b₁ + a₂›
  (b₁ + a₂) + (c₂ + b₁) ≃ _ := AA.substL AA.comm
  (a₂ + b₁) + (c₂ + b₁) ≃ _ := AA.substR AA.comm
  (a₂ + b₁) + (b₁ + c₂) ≃ _ := AA.substR ‹b₁ + c₂ ≃ c₁ + b₂›
  (a₂ + b₁) + (c₁ + b₂) ≃ _ := AA.comm
  (c₁ + b₂) + (a₂ + b₁) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (c₁ + a₂) + (b₂ + b₁) ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ c₁ c₂ : ℕ
x✝¹ : a₁ + b₂ ≃ b₁ + a₂
x✝ : b₁ + c₂ ≃ c₁ + b₂
this : a₁ + c₂ + (b₂ + b₁) ≃ c₁ + a₂ + (b₂ + b₁)
⊢ a₁ + c₂ ≃ c₁ + a₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.trans
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
a₁ a₂ b₁ b₂ c₁ c₂ : ℕ
x✝¹ : a₁ + b₂ ≃ b₁ + a₂
x✝ : b₁ + c₂ ≃ c₁ + b₂
this : a₁ + c₂ + (b₂ + b₁) ≃ c₁ + a₂ + (b₂ + b₁)
⊢ a₁ + c₂ ≃ c₁ + a₂
Tactic:
exact AA.cancelR ‹(a₁ + c₂) + (b₂ + b₁) ≃ (c₁ + a₂) + (b₂ + b₁)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.diff_substL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ m : ℕ
⊢ n₁ ≃ n₂ → n₁——m ≃ n₂——m
Tactic:
intro (_ : n₁ ≃ n₂)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ m : ℕ
x✝ : n₁ ≃ n₂
⊢ n₁——m ≃ n₂——m
Theorem: Lean4Axiomatic.Integer.Impl.Difference.diff_substL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ m : ℕ
x✝ : n₁ ≃ n₂
⊢ n₁——m ≃ n₂——m
Tactic:
have : n₁ + m ≃ n₂ + m := AA.substL ‹n₁ ≃ n₂›
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ m : ℕ
x✝ : n₁ ≃ n₂
this : n₁ + m ≃ n₂ + m
⊢ n₁——m ≃ n₂——m
Theorem: Lean4Axiomatic.Integer.Impl.Difference.diff_substL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ m : ℕ
x✝ : n₁ ≃ n₂
this : n₁ + m ≃ n₂ + m
⊢ n₁——m ≃ n₂——m
Tactic:
have : n₁——m ≃ n₂——m := this
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ m : ℕ
x✝ : n₁ ≃ n₂
this✝ : n₁ + m ≃ n₂ + m
this : n₁——m ≃ n₂——m
⊢ n₁——m ≃ n₂——m
Theorem: Lean4Axiomatic.Integer.Impl.Difference.diff_substL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ m : ℕ
x✝ : n₁ ≃ n₂
this✝ : n₁ + m ≃ n₂ + m
this : n₁——m ≃ n₂——m
⊢ n₁——m ≃ n₂——m
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.diff_substR
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m₁ m₂ : ℕ
⊢ m₁ ≃ m₂ → n——m₁ ≃ n——m₂
Tactic:
intro (_ : m₁ ≃ m₂)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m₁ m₂ : ℕ
x✝ : m₁ ≃ m₂
⊢ n——m₁ ≃ n——m₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.diff_substR
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m₁ m₂ : ℕ
x✝ : m₁ ≃ m₂
⊢ n——m₁ ≃ n——m₂
Tactic:
have : n + m₂ ≃ n + m₁ := AA.substR (Rel.symm ‹m₁ ≃ m₂›)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m₁ m₂ : ℕ
x✝ : m₁ ≃ m₂
this : n + m₂ ≃ n + m₁
⊢ n——m₁ ≃ n——m₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.diff_substR
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m₁ m₂ : ℕ
x✝ : m₁ ≃ m₂
this : n + m₂ ≃ n + m₁
⊢ n——m₁ ≃ n——m₂
Tactic:
have : n——m₁ ≃ n——m₂ := this
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m₁ m₂ : ℕ
x✝ : m₁ ≃ m₂
this✝ : n + m₂ ≃ n + m₁
this : n——m₁ ≃ n——m₂
⊢ n——m₁ ≃ n——m₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.diff_substR
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m₁ m₂ : ℕ
x✝ : m₁ ≃ m₂
this✝ : n + m₂ ≃ n + m₁
this : n——m₁ ≃ n——m₂
⊢ n——m₁ ≃ n——m₂
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.from_ℕ_subst
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ : ℕ
⊢ n₁ ≃ n₂ → n₁——0 ≃ n₂——0
Tactic:
intro (_ : n₁ ≃ n₂)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ : ℕ
x✝ : n₁ ≃ n₂
⊢ n₁——0 ≃ n₂——0
Theorem: Lean4Axiomatic.Integer.Impl.Difference.from_ℕ_subst
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ : ℕ
x✝ : n₁ ≃ n₂
⊢ n₁——0 ≃ n₂——0
Tactic:
show from_prod (n₁, 0) ≃ from_prod (n₂, 0)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ : ℕ
x✝ : n₁ ≃ n₂
⊢ from_prod (n₁, 0) ≃ from_prod (n₂, 0)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.from_ℕ_subst
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ : ℕ
x✝ : n₁ ≃ n₂
⊢ from_prod (n₁, 0) ≃ from_prod (n₂, 0)
Tactic:
apply AA.subst₁
Proof state after:
case a
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ : ℕ
x✝ : n₁ ≃ n₂
⊢ (n₁, 0) ≃ (n₂, 0)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.from_ℕ_subst
Proof state before:
case a
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ : ℕ
x✝ : n₁ ≃ n₂
⊢ (n₁, 0) ≃ (n₂, 0)
Tactic:
exact AA.substL ‹n₁ ≃ n₂›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.from_ℕ_inject
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ : ℕ
⊢ n₁——0 ≃ n₂——0 → n₁ ≃ n₂
Tactic:
intro (_ : n₁——0 ≃ n₂——0)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ : ℕ
x✝ : n₁——0 ≃ n₂——0
⊢ n₁ ≃ n₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.from_ℕ_inject
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ : ℕ
x✝ : n₁——0 ≃ n₂——0
⊢ n₁ ≃ n₂
Tactic:
have : n₁ + 0 ≃ n₂ + 0 := ‹n₁——0 ≃ n₂——0›
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ : ℕ
x✝ : n₁——0 ≃ n₂——0
this : n₁ + 0 ≃ n₂ + 0
⊢ n₁ ≃ n₂
Theorem: Lean4Axiomatic.Integer.Impl.Difference.from_ℕ_inject
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n₁ n₂ : ℕ
x✝ : n₁——0 ≃ n₂——0
this : n₁ + 0 ≃ n₂ + 0
⊢ n₁ ≃ n₂
Tactic:
calc
  n₁     ≃ _ := Rel.symm AA.identR
  n₁ + 0 ≃ _ := ‹n₁ + 0 ≃ n₂ + 0›
  n₂ + 0 ≃ _ := AA.identR
  n₂     ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.substN
Proof state before:
ℕ : Type
inst✝² : Natural ℕ
ℤ : Type
inst✝¹ : Integer ℤ
a₁ a₂ b : ℤ
inst✝ : AP (Positive b)
⊢ a₁ ≃ a₂ → a₁//b ≃ a₂//b
Tactic:
intro (_ : a₁ ≃ a₂)
Proof state after:
ℕ : Type
inst✝² : Natural ℕ
ℤ : Type
inst✝¹ : Integer ℤ
a₁ a₂ b : ℤ
inst✝ : AP (Positive b)
x✝ : a₁ ≃ a₂
⊢ a₁//b ≃ a₂//b
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.substN
Proof state before:
ℕ : Type
inst✝² : Natural ℕ
ℤ : Type
inst✝¹ : Integer ℤ
a₁ a₂ b : ℤ
inst✝ : AP (Positive b)
x✝ : a₁ ≃ a₂
⊢ a₁//b ≃ a₂//b
Tactic:
show a₁ * b ≃ a₂ * b
Proof state after:
ℕ : Type
inst✝² : Natural ℕ
ℤ : Type
inst✝¹ : Integer ℤ
a₁ a₂ b : ℤ
inst✝ : AP (Positive b)
x✝ : a₁ ≃ a₂
⊢ a₁ * b ≃ a₂ * b
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.substN
Proof state before:
ℕ : Type
inst✝² : Natural ℕ
ℤ : Type
inst✝¹ : Integer ℤ
a₁ a₂ b : ℤ
inst✝ : AP (Positive b)
x✝ : a₁ ≃ a₂
⊢ a₁ * b ≃ a₂ * b
Tactic:
exact AA.substL ‹a₁ ≃ a₂›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.substD
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b₁ b₂ : ℤ
pb₁ : AP (Positive b₁)
pb₂ : AP (Positive b₂)
⊢ b₁ ≃ b₂ → a//b₁ ≃ a//b₂
Tactic:
intro (_ : b₁ ≃ b₂)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b₁ b₂ : ℤ
pb₁ : AP (Positive b₁)
pb₂ : AP (Positive b₂)
x✝ : b₁ ≃ b₂
⊢ a//b₁ ≃ a//b₂
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.substD
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b₁ b₂ : ℤ
pb₁ : AP (Positive b₁)
pb₂ : AP (Positive b₂)
x✝ : b₁ ≃ b₂
⊢ a//b₁ ≃ a//b₂
Tactic:
show a * b₂ ≃ a * b₁
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b₁ b₂ : ℤ
pb₁ : AP (Positive b₁)
pb₂ : AP (Positive b₂)
x✝ : b₁ ≃ b₂
⊢ a * b₂ ≃ a * b₁
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.substD
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b₁ b₂ : ℤ
pb₁ : AP (Positive b₁)
pb₂ : AP (Positive b₂)
x✝ : b₁ ≃ b₂
⊢ a * b₂ ≃ a * b₁
Tactic:
exact AA.substR (Rel.symm ‹b₁ ≃ b₂›)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.from_integer_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a₁ a₂ : ℤ
⊢ a₁ ≃ a₂ → from_integer a₁ ≃ from_integer a₂
Tactic:
intro (_ : a₁ ≃ a₂)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
⊢ from_integer a₁ ≃ from_integer a₂
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.from_integer_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
⊢ from_integer a₁ ≃ from_integer a₂
Tactic:
show a₁//1 ≃ a₂//1
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
⊢ a₁//1 ≃ a₂//1
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.from_integer_subst
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a₁ a₂ : ℤ
x✝ : a₁ ≃ a₂
⊢ a₁//1 ≃ a₂//1
Tactic:
exact substN ‹a₁ ≃ a₂›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.from_integer_inject
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a₁ a₂ : ℤ
⊢ from_integer a₁ ≃ from_integer a₂ → a₁ ≃ a₂
Tactic:
intro (_ : from_integer a₁ ≃ from_integer a₂)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a₁ a₂ : ℤ
x✝ : from_integer a₁ ≃ from_integer a₂
⊢ a₁ ≃ a₂
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.from_integer_inject
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a₁ a₂ : ℤ
x✝ : from_integer a₁ ≃ from_integer a₂
⊢ a₁ ≃ a₂
Tactic:
have : a₁//1 ≃ a₂//1 := ‹from_integer a₁ ≃ from_integer a₂›
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a₁ a₂ : ℤ
x✝ : from_integer a₁ ≃ from_integer a₂
this : a₁//1 ≃ a₂//1
⊢ a₁ ≃ a₂
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.from_integer_inject
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a₁ a₂ : ℤ
x✝ : from_integer a₁ ≃ from_integer a₂
this : a₁//1 ≃ a₂//1
⊢ a₁ ≃ a₂
Tactic:
have : a₁ * 1 ≃ a₂ * 1 := this
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a₁ a₂ : ℤ
x✝ : from_integer a₁ ≃ from_integer a₂
this✝ : a₁//1 ≃ a₂//1
this : a₁ * 1 ≃ a₂ * 1
⊢ a₁ ≃ a₂
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.from_integer_inject
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a₁ a₂ : ℤ
x✝ : from_integer a₁ ≃ from_integer a₂
this✝¹ : a₁//1 ≃ a₂//1
this✝ : a₁ * 1 ≃ a₂ * 1
this : a₁ ≃ a₂
⊢ a₁ ≃ a₂
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.eqv_zero_iff_numerator_eqv_zero
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
⊢ p ≃ 0 ↔ p.numerator ≃ 0
Tactic:
revert p
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ∀ {p : Fraction ℤ}, p ≃ 0 ↔ p.numerator ≃ 0
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.eqv_zero_iff_numerator_eqv_zero
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ∀ {p : Fraction ℤ}, p ≃ 0 ↔ p.numerator ≃ 0
Tactic:
intro (pn//pd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ pn//pd ≃ 0 ↔ (pn//pd).numerator ≃ 0
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.eqv_zero_iff_numerator_eqv_zero
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ pn//pd ≃ 0 ↔ (pn//pd).numerator ≃ 0
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ pn//pd ≃ 0 → (pn//pd).numerator ≃ 0

case mpr
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ (pn//pd).numerator ≃ 0 → pn//pd ≃ 0
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.eqv_zero_iff_numerator_eqv_zero
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ pn//pd ≃ 0 → (pn//pd).numerator ≃ 0
Tactic:
case mp =>
  intro (_ : pn//pd ≃ 0)
  show pn ≃ 0
  have : pn//pd ≃ 0//1 := ‹pn//pd ≃ 0›
  have : pn * 1 ≃ 0 * pd := ‹pn//pd ≃ 0//1›
  calc
    pn     ≃ _ := Rel.symm AA.identR
    pn * 1 ≃ _ := ‹pn * 1 ≃ 0 * pd›
    0 * pd ≃ _ := AA.absorbL
    0      ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.eqv_zero_iff_numerator_eqv_zero
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ (pn//pd).numerator ≃ 0 → pn//pd ≃ 0
Tactic:
case mpr =>
  intro (_ : pn ≃ 0)
  show pn//pd ≃ 0
  show pn//pd ≃ 0//1
  show pn * 1 ≃ 0 * pd
  calc
    pn * 1 ≃ _ := AA.identR
    pn     ≃ _ := ‹pn ≃ 0›
    0      ≃ _ := Rel.symm AA.absorbL
    0 * pd ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.eqv_zero_iff_numerator_eqv_zero
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ pn//pd ≃ 0 → (pn//pd).numerator ≃ 0
Tactic:
intro (_ : pn//pd ≃ 0)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn//pd ≃ 0
⊢ (pn//pd).numerator ≃ 0
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.eqv_zero_iff_numerator_eqv_zero
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn//pd ≃ 0
⊢ (pn//pd).numerator ≃ 0
Tactic:
show pn ≃ 0
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn//pd ≃ 0
⊢ pn ≃ 0
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.eqv_zero_iff_numerator_eqv_zero
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn//pd ≃ 0
⊢ pn ≃ 0
Tactic:
have : pn//pd ≃ 0//1 := ‹pn//pd ≃ 0›
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn//pd ≃ 0
this : pn//pd ≃ 0//1
⊢ pn ≃ 0
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.eqv_zero_iff_numerator_eqv_zero
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn//pd ≃ 0
this : pn//pd ≃ 0//1
⊢ pn ≃ 0
Tactic:
have : pn * 1 ≃ 0 * pd := ‹pn//pd ≃ 0//1›
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn//pd ≃ 0
this✝ : pn//pd ≃ 0//1
this : pn * 1 ≃ 0 * pd
⊢ pn ≃ 0
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.eqv_zero_iff_numerator_eqv_zero
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn//pd ≃ 0
this✝ : pn//pd ≃ 0//1
this : pn * 1 ≃ 0 * pd
⊢ pn ≃ 0
Tactic:
calc
  pn     ≃ _ := Rel.symm AA.identR
  pn * 1 ≃ _ := ‹pn * 1 ≃ 0 * pd›
  0 * pd ≃ _ := AA.absorbL
  0      ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.eqv_zero_iff_numerator_eqv_zero
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ (pn//pd).numerator ≃ 0 → pn//pd ≃ 0
Tactic:
intro (_ : pn ≃ 0)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn ≃ 0
⊢ pn//pd ≃ 0
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.eqv_zero_iff_numerator_eqv_zero
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn ≃ 0
⊢ pn//pd ≃ 0
Tactic:
show pn//pd ≃ 0//1
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn ≃ 0
⊢ pn//pd ≃ 0//1
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.eqv_zero_iff_numerator_eqv_zero
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn ≃ 0
⊢ pn//pd ≃ 0//1
Tactic:
show pn * 1 ≃ 0 * pd
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn ≃ 0
⊢ pn * 1 ≃ 0 * pd
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.eqv_zero_iff_numerator_eqv_zero
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn ≃ 0
⊢ pn * 1 ≃ 0 * pd
Tactic:
calc
  pn * 1 ≃ _ := AA.identR
  pn     ≃ _ := ‹pn ≃ 0›
  0      ≃ _ := Rel.symm AA.absorbL
  0 * pd ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.nonzero_numerator
Proof state before:
ℕ : Type
inst✝² : Natural ℕ
ℤ : Type
inst✝¹ : Integer ℤ
p : Fraction ℤ
inst✝ : AP (p ≄ 0)
⊢ Integer.Nonzero p.numerator
Tactic:
revert p
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ∀ (p : Fraction ℤ) [inst : AP (p ≄ 0)], Integer.Nonzero p.numerator
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.nonzero_numerator
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ∀ (p : Fraction ℤ) [inst : AP (p ≄ 0)], Integer.Nonzero p.numerator
Tactic:
intro (a//b) (_ : AP (a//b ≄ 0))
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
x✝ : AP (a//b ≄ 0)
⊢ Integer.Nonzero (a//b).numerator
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.nonzero_numerator
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
x✝ : AP (a//b ≄ 0)
⊢ Integer.Nonzero (a//b).numerator
Tactic:
have : a ≃ 0 → a//b ≃ 0 := (eqv_zero_iff_numerator_eqv_zero (p := a//b)).mpr
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
x✝ : AP (a//b ≄ 0)
this : a ≃ 0 → a//b ≃ 0
⊢ Integer.Nonzero (a//b).numerator
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.nonzero_numerator
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
x✝ : AP (a//b ≄ 0)
this : a ≃ 0 → a//b ≃ 0
⊢ Integer.Nonzero (a//b).numerator
Tactic:
have : a ≄ 0 := mt this ‹AP (a//b ≄ 0)›.ev
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
x✝ : AP (a//b ≄ 0)
this✝ : a ≃ 0 → a//b ≃ 0
this : a ≄ 0
⊢ Integer.Nonzero (a//b).numerator
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.nonzero_numerator
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
x✝ : AP (a//b ≄ 0)
this✝ : a ≃ 0 → a//b ≃ 0
this : a ≄ 0
⊢ Integer.Nonzero (a//b).numerator
Tactic:
have : Integer.Nonzero a := Integer.nonzero_iff_neqv_zero.mpr this
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
x✝ : AP (a//b ≄ 0)
this✝¹ : a ≃ 0 → a//b ≃ 0
this✝ : a ≄ 0
this : Integer.Nonzero a
⊢ Integer.Nonzero (a//b).numerator
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.nonzero_numerator
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
x✝ : AP (a//b ≄ 0)
this✝¹ : a ≃ 0 → a//b ≃ 0
this✝ : a ≄ 0
this : Integer.Nonzero a
⊢ Integer.Nonzero (a//b).numerator
Tactic:
exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.eqv_one_iff_numer_eqv_denom
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
⊢ p ≃ 1 ↔ p.numerator ≃ p.denominator
Tactic:
revert p
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ∀ {p : Fraction ℤ}, p ≃ 1 ↔ p.numerator ≃ p.denominator
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.eqv_one_iff_numer_eqv_denom
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
⊢ ∀ {p : Fraction ℤ}, p ≃ 1 ↔ p.numerator ≃ p.denominator
Tactic:
intro (pn//pd)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ pn//pd ≃ 1 ↔ (pn//pd).numerator ≃ (pn//pd).denominator
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.eqv_one_iff_numer_eqv_denom
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ pn//pd ≃ 1 ↔ (pn//pd).numerator ≃ (pn//pd).denominator
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ pn//pd ≃ 1 → (pn//pd).numerator ≃ (pn//pd).denominator

case mpr
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ (pn//pd).numerator ≃ (pn//pd).denominator → pn//pd ≃ 1
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.eqv_one_iff_numer_eqv_denom
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ pn//pd ≃ 1 → (pn//pd).numerator ≃ (pn//pd).denominator
Tactic:
case mp =>
  intro (_ : pn//pd ≃ 1)
  show pn ≃ pd
  have : pn//pd ≃ 1//1 := ‹pn//pd ≃ 1//1›
  have : pn * 1 ≃ 1 * pd := ‹pn//pd ≃ 1//1›
  calc
    pn     ≃ _ := Rel.symm AA.identR
    pn * 1 ≃ _ := ‹pn * 1 ≃ 1 * pd›
    1 * pd ≃ _ := AA.identL
    pd     ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.eqv_one_iff_numer_eqv_denom
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ (pn//pd).numerator ≃ (pn//pd).denominator → pn//pd ≃ 1
Tactic:
case mpr =>
  intro (_ : pn ≃ pd)
  show pn//pd ≃ 1
  show pn//pd ≃ 1//1
  show pn * 1 ≃ 1 * pd
  calc
    pn * 1 ≃ _ := AA.substL ‹pn ≃ pd›
    pd * 1 ≃ _ := AA.comm
    1 * pd ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.eqv_one_iff_numer_eqv_denom
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
⊢ pn//pd ≃ 1 → (pn//pd).numerator ≃ (pn//pd).denominator
Tactic:
intro (_ : pn//pd ≃ 1)
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn//pd ≃ 1
⊢ (pn//pd).numerator ≃ (pn//pd).denominator
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.eqv_one_iff_numer_eqv_denom
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn//pd ≃ 1
⊢ (pn//pd).numerator ≃ (pn//pd).denominator
Tactic:
show pn ≃ pd
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn//pd ≃ 1
⊢ pn ≃ pd
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.eqv_one_iff_numer_eqv_denom
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn//pd ≃ 1
⊢ pn ≃ pd
Tactic:
have : pn//pd ≃ 1//1 := ‹pn//pd ≃ 1//1›
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn//pd ≃ 1
this : pn//pd ≃ 1//1
⊢ pn ≃ pd
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.eqv_one_iff_numer_eqv_denom
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn//pd ≃ 1
this : pn//pd ≃ 1//1
⊢ pn ≃ pd
Tactic:
have : pn * 1 ≃ 1 * pd := ‹pn//pd ≃ 1//1›
Proof state after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn//pd ≃ 1
this✝ : pn//pd ≃ 1//1
this : pn * 1 ≃ 1 * pd
⊢ pn ≃ pd
Theorem: Lean4Axiomatic.Rational.Impl.Fraction.eqv_one_iff_numer_eqv_denom
Proof state before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : AP (Positive pd)
x✝ : pn//pd ≃ 1
this✝ : pn//pd ≃ 1//1
this : pn * 1 ≃ 1 * pd
⊢ pn ≃ pd
Tactic:
calc
  pn     ≃ _ := Rel.symm AA.identR
  pn * 1 ≃ _ := ‹pn * 1 ≃ 1 * pd›
  1 * pd ≃ _ := AA.identL
  pd     ≃ _ := Rel.refl
Proof state after:
no goals