awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
s₁ : Setoid α
a b : α
⊢ Eq (α := Quotient s₁) (Quotient.mk'' a) (Quotient.mk'' b) ↔ (s₁ : α → α → Prop) a b

Tactic:
Quotient.eq

Premises used: Quotient.eq
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
s₁ : Setoid α
q : Quotient s₁
⊢ Quotient.mk'' q.out = q

Tactic:
q.out_eq

Premises used: Quotient.out_eq
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
s₁ : Setoid α
a : α
⊢ (s₁ : α → α → Prop) (out (s := s₁) (Quotient.mk'' a)) a

Tactic:
Quotient.exact (Quotient.out_eq _)

Premises used: Quotient.exact, Quotient.out_eq
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
s : Setoid α
⊢ Quotient.mk'' = Quotient.mk s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
s : Setoid α
x : α
f : α → β
h : ∀ (a b : α), (s : α → α → Prop) a b → f a = f b
⊢ ⟦x⟧.liftOn' f h = f x

Tactic:
rfl

Premises used: Quotient.liftOn', rfl
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Setoid α
t : Setoid β
f : α → β → γ
h : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), (s : α → α → Prop) a₁ b₁ → (t : β → β → Prop) a₂ b₂ → f a₁ a₂ = f b₁ b₂
a : α
b : β
⊢ ⟦a⟧.liftOn₂' ⟦b⟧ f h = f a b

Tactic:
rfl

Premises used: rfl, Quotient.liftOn₂'
-- Module: Mathlib.Data.Quot
Goal:
α : Sort u_1
β : Sort u_2
s : Setoid α
t : Setoid β
f : α → β
h : ∀ (a b : α), (s : α → α → Prop) a b → (t : β → β → Prop) (f a) (f b)
x : α
⊢ Quotient.map' f h ⟦x⟧ = ⟦f x⟧

Tactic:
rfl

Premises used: Quotient.map', rfl
-- Module: Mathlib.Data.Quot
Goal:
α : Type u_3
r : α → α → Prop
h : Equivalence r
x y : α
⊢ Quot.mk r x = Quot.mk r y ↔ r x y

Tactic:
Quotient.eq (r := ⟨r, h⟩)

Premises used: Quotient, Quotient.eq
-- Module: Mathlib.Data.Rat.BigOperators
Goal:
α : Type u_2
inst : DivisionRing α
inst_1 : CharZero α
s : List ℚ
⊢ Eq.{u_2 + 1} (α := α) (↑s.sum : α) (List.sum (List.map Rat.cast s))

Tactic:
map_list_sum (Rat.castHom α) _

Premises used: map_list_sum, Rat.castHom
-- Module: Mathlib.Data.Rat.BigOperators
Goal:
α : Type u_2
inst : DivisionRing α
inst_1 : CharZero α
s : Multiset ℚ
⊢ Eq.{u_2 + 1} (α := α) (↑s.sum : α) (Multiset.sum (Multiset.map Rat.cast s))

Tactic:
map_multiset_sum (Rat.castHom α) _

Premises used: map_multiset_sum, Rat.castHom
-- Module: Mathlib.Data.Rat.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : DivisionRing α
inst_1 : CharZero α
s : Finset ι
f : ι → ℚ
⊢ Eq.{u_2 + 1} (α := α) (↑(∑ i ∈ s, f i) : α) (∑ i ∈ s, (↑(f i) : α))

Tactic:
map_sum (Rat.castHom α) _ s

Premises used: map_sum, Rat.castHom
-- Module: Mathlib.Data.Rat.BigOperators
Goal:
α : Type u_2
inst : DivisionRing α
inst_1 : CharZero α
s : List ℚ
⊢ Eq.{u_2 + 1} (α := α) (↑s.prod : α) (List.prod (List.map Rat.cast s))

Tactic:
map_list_prod (Rat.castHom α) _

Premises used: map_list_prod, Rat.castHom
-- Module: Mathlib.Data.Rat.BigOperators
Goal:
α : Type u_2
inst : Field α
inst_1 : CharZero α
s : Multiset ℚ
⊢ Eq.{u_2 + 1} (α := α) (↑s.prod : α) (Multiset.prod (Multiset.map Rat.cast s))

Tactic:
map_multiset_prod (Rat.castHom α) _

Premises used: map_multiset_prod, Rat.castHom
-- Module: Mathlib.Data.Rat.BigOperators
Goal:
ι : Type u_1
α : Type u_2
inst : Field α
inst_1 : CharZero α
s : Finset ι
f : ι → ℚ
⊢ Eq.{u_2 + 1} (α := α) (↑(∏ i ∈ s, f i) : α) (∏ i ∈ s, (↑(f i) : α))

Tactic:
map_prod (Rat.castHom α) _ _

Premises used: map_prod, Rat.castHom
-- Module: Mathlib.Data.Rat.Cardinal
Goal:
⊢ #ℚ = ℵ₀

Tactic:
mk_eq_aleph0 ℚ

Premises used: Rat, Cardinal.mk_eq_aleph0
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionRing α
inst_1 : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
h :
  Eq.{u_3 + 1} (α := α) (↑{ num := n₁, den := d₁, den_nz := d₁0, reduced := c₁ } : α)
    (↑{ num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ } : α)
⊢ Ne.{u_3 + 1} (α := α) (↑d₁ : α) 0

Tactic:
have d₁a : (d₁ : α) ≠ 0 := Nat.cast_ne_zero.2 d₁0
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionRing α
inst_1 : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
h :
  Eq.{u_3 + 1} (α := α) (↑{ num := n₁, den := d₁, den_nz := d₁0, reduced := c₁ } : α)
    (↑{ num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ } : α)
d₁a : Ne.{u_3 + 1} (α := α) (↑d₁ : α) 0
⊢ Ne.{u_3 + 1} (α := α) (↑d₂ : α) 0

Tactic:
have d₂a : (d₂ : α) ≠ 0 := Nat.cast_ne_zero.2 d₂0
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionRing α
inst_1 : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
h :
  Eq.{u_3 + 1} (α := α) (↑{ num := n₁, den := d₁, den_nz := d₁0, reduced := c₁ } : α)
    (↑{ num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ } : α)
d₁a : Ne.{u_3 + 1} (α := α) (↑d₁ : α) 0
d₂a : Ne.{u_3 + 1} (α := α) (↑d₂ : α) 0
rw :
  ∀ (h : Eq.{u_3 + 1} (α := α) (↑(n₁ /. (↑d₁ : ℤ)) : α) (↑(n₂ /. (↑d₂ : ℤ)) : α))
    (d₁a : Ne.{u_3 + 1} (α := α) (↑d₁ : α) 0) (d₂a : Ne.{u_3 + 1} (α := α) (↑d₂ : α) 0),
    n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
⊢ { num := n₁, den := d₁, den_nz := d₁0, reduced := c₁ : ℚ } = { num := n₂, den := d₂, den_nz := d₂0, reduced := c₂ }

Tactic:
rw [mk_eq_divInt, mk_eq_divInt] at h ⊢

Premises used: Rat.mk_eq_divInt
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionRing α
inst_1 : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
h : Eq.{u_3 + 1} (α := α) (↑(n₁ /. (↑d₁ : ℤ)) : α) (↑(n₂ /. (↑d₂ : ℤ)) : α)
d₁a : Ne.{u_3 + 1} (α := α) (↑d₁ : α) 0
d₂a : Ne.{u_3 + 1} (α := α) (↑d₂ : α) 0
⊢ Ne.{u_3 + 1} (α := α) (↑(↑d₁ : ℤ) : α) 0

Tactic:
simpa
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionRing α
inst_1 : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
h : HDiv.hDiv (α := α) (↑n₁ : α) (↑(↑d₁ : ℤ) : α) = (↑(n₂ /. (↑d₂ : ℤ)) : α)
d₁a : Ne.{u_3 + 1} (α := α) (↑d₁ : α) 0
d₂a : Ne.{u_3 + 1} (α := α) (↑d₂ : α) 0
⊢ Ne.{u_3 + 1} (α := α) (↑(↑d₂ : ℤ) : α) 0

Tactic:
simpa
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionRing α
inst_1 : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
h : Eq.{u_3 + 1} (α := α) (↑(n₁ /. (↑d₁ : ℤ)) : α) (↑(n₂ /. (↑d₂ : ℤ)) : α)
d₁a : Ne.{u_3 + 1} (α := α) (↑d₁ : α) 0
d₂a : Ne.{u_3 + 1} (α := α) (↑d₂ : α) 0
⊢ HDiv.hDiv (α := α) (↑n₁ : α) (↑(↑d₁ : ℤ) : α) = HDiv.hDiv (α := α) (↑n₂ : α) (↑(↑d₂ : ℤ) : α)

Tactic:
rw [cast_divInt_of_ne_zero _ (by simpa), cast_divInt_of_ne_zero _ (by simpa)] at h

Premises used: Rat.cast_divInt_of_ne_zero
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionRing α
inst_1 : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
h : Eq.{u_3 + 1} (α := α) (↑(n₁ /. (↑d₁ : ℤ)) : α) (↑(n₂ /. (↑d₂ : ℤ)) : α)
d₁a : Ne.{u_3 + 1} (α := α) (↑d₁ : α) 0
d₂a : Ne.{u_3 + 1} (α := α) (↑d₂ : α) 0
h₁ : HDiv.hDiv (α := α) (↑n₁ : α) (↑(↑d₁ : ℤ) : α) = HDiv.hDiv (α := α) (↑n₂ : α) (↑(↑d₂ : ℤ) : α)
⊢ Ne.{u_3 + 1} (α := α) (↑d₁ : α) 0

Tactic:
rw [cast_divInt_of_ne_zero _ (by simpa), cast_divInt_of_ne_zero _ (by simpa)] at h

Premises used: Rat.cast_divInt_of_ne_zero
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionRing α
inst_1 : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
h : Eq.{u_3 + 1} (α := α) (↑(n₁ /. (↑d₁ : ℤ)) : α) (↑(n₂ /. (↑d₂ : ℤ)) : α)
d₁a : Ne.{u_3 + 1} (α := α) (↑d₁ : α) 0
d₂a : Ne.{u_3 + 1} (α := α) (↑d₂ : α) 0
h₁ : HDiv.hDiv (α := α) (↑n₁ : α) (↑(↑d₁ : ℤ) : α) = HDiv.hDiv (α := α) (↑n₂ : α) (↑(↑d₂ : ℤ) : α)
d₁a₁ : Ne.{u_3 + 1} (α := α) (↑d₁ : α) 0
⊢ Ne.{u_3 + 1} (α := α) (↑d₂ : α) 0

Tactic:
rw [cast_divInt_of_ne_zero _ (by simpa), cast_divInt_of_ne_zero _ (by simpa)] at h

Premises used: Rat.cast_divInt_of_ne_zero
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionRing α
inst_1 : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
h : HDiv.hDiv (α := α) (↑n₁ : α) (↑(↑d₁ : ℤ) : α) = HDiv.hDiv (α := α) (↑n₂ : α) (↑(↑d₂ : ℤ) : α)
d₁a : Ne.{u_3 + 1} (α := α) (↑d₁ : α) 0
d₂a : Ne.{u_3 + 1} (α := α) (↑d₂ : α) 0
⊢ HDiv.hDiv (α := α) (↑n₁ : α) (↑d₁ : α) = HDiv.hDiv (α := α) (↑n₂ : α) (↑d₂ : α)

Tactic:
norm_cast at h
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionRing α
inst_1 : CharZero α
n₁ : ℤ
d₁ : ℕ
d₁0 : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
n₂ : ℤ
d₂ : ℕ
d₂0 : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
d₁a : Ne.{u_3 + 1} (α := α) (↑d₁ : α) 0
d₂a : Ne.{u_3 + 1} (α := α) (↑d₂ : α) 0
h : HDiv.hDiv (α := α) (↑n₁ : α) (↑d₁ : α) = HDiv.hDiv (α := α) (↑n₂ : α) (↑d₂ : α)
rwa : ∀ (h : HDiv.hDiv (α := α) (↑n₁ : α) (↑d₁ : α) * (↑d₂ : α) = (↑n₂ : α)), n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
rwa₁ : ∀ (h : HMul.hMul (α := α) (↑n₁ : α) (↑d₁ : α)⁻¹ * (↑d₂ : α) = (↑n₂ : α)), n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
rwa₂ : ∀ (h : (↑n₁ : α) * HMul.hMul (α := α) (↑d₁ : α)⁻¹ (↑d₂ : α) = (↑n₂ : α)), n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
rwa₃ : ∀ (h : (↑n₁ : α) * HMul.hMul (α := α) (↑d₂ : α) (↑d₁ : α)⁻¹ = (↑n₂ : α)), n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
rwa₄ : ∀ (h : HMul.hMul (α := α) (↑n₁ : α) (↑d₂ : α) * (↑d₁ : α)⁻¹ = (↑n₂ : α)), n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
rwa₅ : ∀ (h : HMul.hMul (α := α) (↑n₁ : α) (↑d₂ : α) / (↑d₁ : α) = (↑n₂ : α)), n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
rwa₆ : ∀ (h : (↑n₂ : α) = HMul.hMul (α := α) (↑n₁ : α) (↑d₂ : α) / (↑d₁ : α)), n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
rwa₇ :
  ∀ (h : HMul.hMul (α := α) (↑n₂ : α) (↑d₁ : α) = HMul.hMul (α := α) (↑n₁ : α) (↑d₂ : α)),
    n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
rwa₈ :
  ∀ (h : HMul.hMul (α := α) (↑n₁ : α) (↑d₂ : α) = HMul.hMul (α := α) (↑n₂ : α) (↑d₁ : α)),
    n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
rwa₉ :
  ∀ (h : HMul.hMul (α := α) (↑n₁ : α) (↑d₂ : α) = HMul.hMul (α := α) (↑n₂ : α) (↑(↑d₁ : ℤ) : α)),
    n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
rwa₁₀ : ∀ (h : HMul.hMul (α := α) (↑n₁ : α) (↑d₂ : α) = (↑(n₂ * (↑d₁ : ℤ)) : α)), n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
rwa₁₁ :
  ∀ (h : HMul.hMul (α := α) (↑n₁ : α) (↑(↑d₂ : ℤ) : α) = (↑(n₂ * (↑d₁ : ℤ)) : α)), n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
rwa₁₂ : ∀ (h : Eq.{u_3 + 1} (α := α) (↑(n₁ * (↑d₂ : ℤ)) : α) (↑(n₂ * (↑d₁ : ℤ)) : α)), n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
rwa₁₃ : ∀ (h : n₁ * (↑d₂ : ℤ) = n₂ * (↑d₁ : ℤ)), n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
rwa₁₄ rwa₁₅ rwa₁₆ rwa₁₇ : ∀ (h : mkRat n₁ d₁ = mkRat n₂ d₂), n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)
⊢ n₁ /. (↑d₁ : ℤ) = n₂ /. (↑d₂ : ℤ)

Tactic:
rwa [eq_div_iff_mul_eq d₂a, division_def, mul_assoc, (d₁.cast_commute (d₂ : α)).inv_left₀.eq,
      ← mul_assoc, ← division_def, eq_comm, eq_div_iff_mul_eq d₁a, eq_comm, ← Int.cast_natCast d₁,
      ← Int.cast_mul, ← Int.cast_natCast d₂, ← Int.cast_mul, Int.cast_inj, ← mkRat_eq_iff d₁0 d₂0]
      at h

Premises used: Int.cast_natCast, Int.cast_inj, mul_assoc, Rat.mkRat_eq_iff, division_def, eq_comm, Nat.cast, Int.cast_mul, eq_div_iff_mul_eq, Commute.eq, Commute.inv_left₀, Nat.cast_commute
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionRing α
inst_1 : CharZero α
p q : ℚ
⊢ Eq.{u_3 + 1} (α := α) (↑p : α) (↑q : α) ↔ p = q

Tactic:
cast_injective.eq_iff

Premises used: Function.Injective.eq_iff, Rat.cast_injective
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionRing α
inst_1 : CharZero α
p : ℚ
⊢ Eq.{u_3 + 1} (α := α) (↑p : α) 0 ↔ p = 0

Tactic:
cast_injective.eq_iff' cast_zero

Premises used: Function.Injective.eq_iff', Rat.cast_zero, Rat.cast_injective
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionRing α
inst_1 : CharZero α
p : ℚ
⊢ Ne.{u_3 + 1} (α := α) (↑p : α) 0 ↔ p ≠ 0

Tactic:
cast_eq_zero.ne

Premises used: Iff.ne, Rat.cast_eq_zero
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionRing α
inst_1 : CharZero α
p q : ℚ
⊢ (↑(p + q) : α) = HAdd.hAdd (α := α) (↑p : α) (↑q : α)

Tactic:
cast_add_of_ne_zero (Nat.cast_ne_zero.2 p.pos.ne') (Nat.cast_ne_zero.2 q.pos.ne')

Premises used: Iff.mpr, Rat.pos, Rat.cast_add_of_ne_zero, LT.lt.ne', Nat.cast_ne_zero
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionRing α
inst_1 : CharZero α
p q : ℚ
⊢ (↑(p - q) : α) = HSub.hSub (α := α) (↑p : α) (↑q : α)

Tactic:
cast_sub_of_ne_zero (Nat.cast_ne_zero.2 p.pos.ne') (Nat.cast_ne_zero.2 q.pos.ne')

Premises used: Iff.mpr, Rat.pos, LT.lt.ne', Rat.cast_sub_of_ne_zero, Nat.cast_ne_zero
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionRing α
inst_1 : CharZero α
p q : ℚ
⊢ (↑(p * q) : α) = HMul.hMul (α := α) (↑p : α) (↑q : α)

Tactic:
cast_mul_of_ne_zero (Nat.cast_ne_zero.2 p.pos.ne') (Nat.cast_ne_zero.2 q.pos.ne')

Premises used: Iff.mpr, Rat.pos, LT.lt.ne', Rat.cast_mul_of_ne_zero, Nat.cast_ne_zero
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionRing α
inst_1 : CharZero α
⊢ Eq (α := (a : ℚ) → α) (⇑(castHom α) : (a : ℚ) → α) Rat.cast

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionRing α
inst_1 : CharZero α
p : ℚ
⊢ Eq.{u_3 + 1} (α := α) (↑p⁻¹ : α) (↑p : α)⁻¹

Tactic:
map_inv₀ (castHom α) _

Premises used: map_inv₀, Rat.castHom
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionRing α
inst_1 : CharZero α
p q : ℚ
⊢ (↑(p / q) : α) = HDiv.hDiv (α := α) (↑p : α) (↑q : α)

Tactic:
map_div₀ (castHom α) ..

Premises used: map_div₀, Rat.castHom
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionRing α
inst_1 : CharZero α
p : ℚ
n : ℤ
⊢ (↑(p ^ n) : α) = HPow.hPow (α := α) (↑p : α) n

Tactic:
map_zpow₀ (castHom α) ..

Premises used: Rat.castHom, map_zpow₀
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionRing α
inst_1 : CharZero α
a b : ℤ
⊢ (↑(a /. b) : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)

Tactic:
simp only [divInt_eq_div, cast_div, cast_intCast]

Premises used: Rat.cast_intCast, Rat.divInt_eq_div, Rat.cast_div
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : Eq.{u_3 + 1} (α := α) (↑p : α) (↑q : α)
rw : ∀ (hpq : HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.num : α) (↑p.den : α)), p = q
hbd :
  ∀ (hpq : HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) = HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)),
    Commute.{u_3} (S := α) (↑p.den : α) (↑q.den : α)
hb :
  ∀ (hpq : HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) = HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)),
    Ne.{u_3 + 1} (α := α) (↑p.den : α) 0
hd :
  ∀ (hpq : HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) = HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)),
    Ne.{u_3 + 1} (α := α) (↑q.den : α) 0
⊢ p = q

Tactic:
rw [NNRat.cast_def, NNRat.cast_def, Commute.div_eq_div_iff] at hpq

Premises used: NNRat.cast_def, Commute.div_eq_div_iff
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.num : α) (↑p.den : α)
rw : HMul.hMul (α := ℚ≥0) (↑p.num : ℚ≥0) (↑q.den : ℚ≥0) = HMul.hMul (α := ℚ≥0) (↑q.num : ℚ≥0) (↑p.den : ℚ≥0)
hb : Ne (α := ℚ≥0) (↑p.den : ℚ≥0) 0
hd : Ne (α := ℚ≥0) (↑q.den : ℚ≥0) 0
⊢ p = q

Tactic:
rw [← p.num_div_den, ← q.num_div_den, div_eq_div_iff]

Premises used: div_eq_div_iff, NNRat.num_div_den
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.num : α) (↑p.den : α)
on_goal : HMul.hMul (α := ℚ≥0) (↑p.num : ℚ≥0) (↑q.den : ℚ≥0) = HMul.hMul (α := ℚ≥0) (↑q.num : ℚ≥0) (↑p.den : ℚ≥0)
hb : Ne (α := ℚ≥0) (↑p.den : ℚ≥0) 0
hd : Ne (α := ℚ≥0) (↑q.den : ℚ≥0) 0
⊢ p = q

Tactic:
on_goal 1 => rw [← p.num_div_den, ← q.num_div_den, div_eq_div_iff]

Premises used: div_eq_div_iff, NNRat.num_div_den
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.num : α) (↑p.den : α)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ∀ (hpq : p.num * q.den = q.num * p.den), p.num * q.den = q.num * p.den
⊢ HMul.hMul (α := ℚ≥0) (↑p.num : ℚ≥0) (↑q.den : ℚ≥0) = HMul.hMul (α := ℚ≥0) (↑q.num : ℚ≥0) (↑p.den : ℚ≥0)

Tactic:
norm_cast at hpq ⊢
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.num : α) (↑p.den : α)
hb : ¬p.den = 0
⊢ Ne (α := ℚ≥0) (↑p.den : ℚ≥0) 0

Tactic:
norm_cast
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.num : α) (↑p.den : α)
hd : ¬q.den = 0
⊢ Ne (α := ℚ≥0) (↑q.den : ℚ≥0) 0

Tactic:
norm_cast
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) = HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)
hb : ¬p.den = 0
⊢ Ne.{u_3 + 1} (α := α) (↑p.den : α) 0

Tactic:
norm_cast
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) = HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)
hd : ¬q.den = 0
⊢ Ne.{u_3 + 1} (α := α) (↑q.den : α) 0

Tactic:
norm_cast
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.num : α) (↑p.den : α)
⊢ ¬p.den = 0

Tactic:
apply den_ne_zero

Premises used: NNRat.den_ne_zero
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : HMul.hMul (α := α) (↑p.num : α) (↑q.den : α) = HMul.hMul (α := α) (↑q.num : α) (↑p.den : α)
⊢ ¬q.den = 0

Tactic:
apply den_ne_zero

Premises used: NNRat.den_ne_zero
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) = HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)
⊢ ¬p.den = 0

Tactic:
apply den_ne_zero

Premises used: NNRat.den_ne_zero
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) = HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)
⊢ ¬q.den = 0

Tactic:
apply den_ne_zero

Premises used: NNRat.den_ne_zero
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) = HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)
⊢ Commute.{u_3} (S := α) (↑p.den : α) (↑q.den : α)

Tactic:
Nat.cast_commute ..

Premises used: Nat.cast_commute
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
hpq : HDiv.hDiv (α := α) (↑p.num : α) (↑p.den : α) = HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)
⊢ Commute.{u_3} (S := α) (↑p.den : α) (↑q.den : α)

Tactic:
exact Nat.cast_commute ..

Premises used: Nat.cast_commute
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
⊢ Eq.{u_3 + 1} (α := α) (↑p : α) (↑q : α) ↔ p = q

Tactic:
cast_injective.eq_iff

Premises used: Function.Injective.eq_iff, NNRat.cast_injective
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
q : ℚ≥0
rw : Eq.{u_3 + 1} (α := α) (↑q : α) (↑0 : α) ↔ q = 0
rw₁ rw₂ : q = 0 ↔ q = 0
⊢ Eq.{u_3 + 1} (α := α) (↑q : α) 0 ↔ q = 0

Tactic:
rw [← cast_zero, cast_inj]

Premises used: NNRat.cast_inj, NNRat.cast_zero
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
q : ℚ≥0
⊢ Ne.{u_3 + 1} (α := α) (↑q : α) 0 ↔ q ≠ 0

Tactic:
cast_eq_zero.not

Premises used: NNRat.cast_eq_zero, Iff.not
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
⊢ (↑(p + q) : α) = HAdd.hAdd (α := α) (↑p : α) (↑q : α)

Tactic:
cast_add_of_ne_zero (Nat.cast_ne_zero.2 p.den_pos.ne') (Nat.cast_ne_zero.2 q.den_pos.ne')

Premises used: Iff.mpr, NNRat.cast_add_of_ne_zero, LT.lt.ne', NNRat.den_pos, Nat.cast_ne_zero
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
⊢ (↑(p * q) : α) = HMul.hMul (α := α) (↑p : α) (↑q : α)

Tactic:
cast_mul_of_ne_zero (Nat.cast_ne_zero.2 p.den_pos.ne') (Nat.cast_ne_zero.2 q.den_pos.ne')

Premises used: Iff.mpr, LT.lt.ne', NNRat.den_pos, Nat.cast_ne_zero, NNRat.cast_mul_of_ne_zero
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
⊢ Eq (α := (a : ℚ≥0) → α) (⇑(castHom α) : (a : ℚ≥0) → α) NNRat.cast

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p : ℚ≥0
⊢ Eq.{u_3 + 1} (α := α) (↑p⁻¹ : α) (↑p : α)⁻¹

Tactic:
map_inv₀ (castHom α) _

Premises used: map_inv₀, NNRat.castHom
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
p q : ℚ≥0
⊢ (↑(p / q) : α) = HDiv.hDiv (α := α) (↑p : α) (↑q : α)

Tactic:
map_div₀ (castHom α) ..

Premises used: NNRat.castHom, map_div₀
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
q : ℚ≥0
p : ℤ
⊢ (↑(q ^ p) : α) = HPow.hPow (α := α) (↑q : α) p

Tactic:
map_zpow₀ (castHom α) ..

Premises used: NNRat.castHom, map_zpow₀
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
a b : ℕ
rw : Eq.{u_3 + 1} (α := α) (↑(divNat a b) : α) (↑(HDiv.hDiv (α := ℚ≥0) (↑a : ℚ≥0) (↑b : ℚ≥0)) : α)
⊢ (↑(divNat a b) : α) = HDiv.hDiv (α := α) (↑a : α) (↑b : α)

Tactic:
rw [← cast_natCast, ← cast_natCast b, ← cast_div]

Premises used: NNRat.cast_div, NNRat.cast_natCast
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
a b : ℕ
e_a : divNat a b = HDiv.hDiv (α := ℚ≥0) (↑a : ℚ≥0) (↑b : ℚ≥0)
⊢ Eq.{u_3 + 1} (α := α) (↑(divNat a b) : α) (↑(HDiv.hDiv (α := ℚ≥0) (↑a : ℚ≥0) (↑b : ℚ≥0)) : α)

Tactic:
congr
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
a b : ℕ
e_a : Eq (α := ℚ) (↑(divNat a b) : ℚ) (↑(HDiv.hDiv (α := ℚ≥0) (↑a : ℚ≥0) (↑b : ℚ≥0)) : ℚ)
⊢ divNat a b = HDiv.hDiv (α := ℚ≥0) (↑a : ℚ≥0) (↑b : ℚ≥0)

Tactic:
ext
-- Module: Mathlib.Data.Rat.Cast.CharZero
Goal:
α : Type u_3
inst : DivisionSemiring α
inst_1 : CharZero α
a b : ℕ
⊢ Eq (α := ℚ) (↑(divNat a b) : ℚ) (↑(HDiv.hDiv (α := ℚ≥0) (↑a : ℚ≥0) (↑b : ℚ≥0)) : ℚ)

Tactic:
apply Rat.mkRat_eq_div

Premises used: Rat.mkRat_eq_div
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
n : ℕ
⊢ Eq.{u_3 + 1} (α := α) (↑(↑n : ℚ≥0) : α) (↑n : α)

Tactic:
simp [cast_def]

Premises used: NNRat.cast_def
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u_3 + 1} (α := α) (↑(OfNat.ofNat n) : α) (OfNat.ofNat n)

Tactic:
cast_natCast _

Premises used: NNRat.cast_natCast
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
⊢ Eq.{u_3 + 1} (α := α) (↑0 : α) 0

Tactic:
(cast_natCast _).trans Nat.cast_zero

Premises used: Nat.cast_zero, NNRat.cast_natCast, Eq.trans
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
⊢ Eq.{u_3 + 1} (α := α) (↑1 : α) 1

Tactic:
(cast_natCast _).trans Nat.cast_one

Premises used: NNRat.cast_natCast, Nat.cast_one, Eq.trans
-- Module: Mathlib.Data.Rat.Cast.Defs
Goal:
α : Type u_3
inst : DivisionSemiring α
q : ℚ≥0
a : α
⊢ Commute (↑q : α) a

Tactic:
simpa only [cast_def] using (q.num.cast_commute a).div_left (q.den.cast_commute a)

Premises used: NNRat.cast_def, Commute.div_left, NNRat.num, NNRat.den, Nat.cast_commute