awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst : AddCommMonoid α
inst_1 : DivisionSemiring γ
inst_2 : Module γ α
h : Periodic f c
a : γ
x : α
pos : ∀ (ha : a = 0), Eq.{u_2 + 1} (α := β) ((fun (x : α) ↦ f (a • x)) (x + a⁻¹ • c)) ((fun (x : α) ↦ f (a • x)) x)
neg : ∀ (ha : ¬a = 0), Eq.{u_2 + 1} (α := β) ((fun (x : α) ↦ f (a • x)) (x + a⁻¹ • c)) ((fun (x : α) ↦ f (a • x)) x)
⊢ Eq.{u_2 + 1} (α := β) ((fun (x : α) ↦ f (a • x)) (x + a⁻¹ • c)) ((fun (x : α) ↦ f (a • x)) x)

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst : AddCommMonoid α
inst_1 : DivisionSemiring γ
inst_2 : Module γ α
h : Periodic f c
a : γ
x : α
ha : a = 0
⊢ Eq.{u_2 + 1} (α := β) ((fun (x : α) ↦ f (a • x)) (x + a⁻¹ • c)) ((fun (x : α) ↦ f (a • x)) x)

Tactic:
simp only [ha, zero_smul]

Premises used: zero_smul
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst : AddCommMonoid α
inst_1 : DivisionSemiring γ
inst_2 : Module γ α
h : Periodic f c
a : γ
x : α
ha : ¬a = 0
⊢ Eq.{u_2 + 1} (α := β) ((fun (x : α) ↦ f (a • x)) (x + a⁻¹ • c)) ((fun (x : α) ↦ f (a • x)) x)

Tactic:
simpa only [smul_add, smul_inv_smul₀ ha] using h (a • x)

Premises used: smul_inv_smul₀, HSMul.hSMul, smul_add
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : DivisionSemiring α
h : Periodic f c
a : α
⊢ Periodic.{u_1, u_2} (β := β) (fun (x : α) ↦ f (a * x)) (a⁻¹ * c)

Tactic:
Periodic.const_smul₀ h a

Premises used: Function.Periodic.const_smul₀
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst : AddCommMonoid α
inst_1 : DivisionSemiring γ
inst_2 : Module γ α
h : Periodic f c
a : γ
⊢ Periodic.{u_1, u_2} (β := β) (fun (x : α) ↦ f (a⁻¹ • x)) (a • c)

Tactic:
simpa only [inv_inv] using h.const_smul₀ a⁻¹

Premises used: Function.Periodic.const_smul₀, Inv.inv, inv_inv
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : DivisionSemiring α
h : Periodic f c
a : α
⊢ Periodic.{u_1, u_2} (β := β) (fun (x : α) ↦ f (a⁻¹ * x)) (a * c)

Tactic:
h.const_inv_smul₀ a

Premises used: Function.Periodic.const_inv_smul₀
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : DivisionSemiring α
h : Periodic f c
a : α
⊢ Periodic.{u_1, u_2} (β := β) (fun (x : α) ↦ f (x * a)) (c * a⁻¹)

Tactic:
h.const_smul₀ (MulOpposite.op a)

Premises used: Function.Periodic.const_smul₀, MulOpposite.unop, MulOpposite.op
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : DivisionSemiring α
h : Periodic f c
a : α
⊢ Periodic.{u_1, u_2} (β := β) (fun (x : α) ↦ f (x * a)) (c / a)

Tactic:
simpa only [div_eq_mul_inv] using h.mul_const a

Premises used: div_eq_mul_inv, Function.Periodic.mul_const
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : DivisionSemiring α
h : Periodic f c
a : α
⊢ Periodic.{u_1, u_2} (β := β) (fun (x : α) ↦ f (x * a⁻¹)) (c * a)

Tactic:
h.const_inv_smul₀ (MulOpposite.op a)

Premises used: MulOpposite.unop, Function.Periodic.const_inv_smul₀, MulOpposite.op
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : DivisionSemiring α
h : Periodic f c
a : α
⊢ Periodic.{u_1, u_2} (β := β) (fun (x : α) ↦ f (x / a)) (c * a)

Tactic:
simpa only [div_eq_mul_inv] using h.mul_const_inv a

Premises used: div_eq_mul_inv, Function.Periodic.mul_const_inv
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
h : Periodic f c
hc : 0 < c
x : α
⊢ ∃ y ∈ Ico 0 c, f x = f y

Tactic:
let ⟨n, H, _⟩ := existsUnique_zsmul_near_of_pos' hc x
  ⟨x - n • c, H, (h.sub_zsmul_eq n).symm⟩

Premises used: existsUnique_zsmul_near_of_pos', HSub.hSub, Membership.mem, Exists, Function.Periodic.sub_zsmul_eq, Set.Ico, And, And.intro, Exists.intro, HSMul.hSMul, _private.0.Function.Periodic.exists_mem_Ico₀.match_1, OfNat.ofNat, Eq.symm, Eq
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
h : Periodic f c
hc : 0 < c
x a : α
⊢ ∃ y ∈ Ico a (a + c), f x = f y

Tactic:
let ⟨n, H, _⟩ := existsUnique_add_zsmul_mem_Ico hc x a
  ⟨x + n • c, H, (h.zsmul n x).symm⟩

Premises used: Membership.mem, Exists, _private.0.Function.Periodic.exists_mem_Ico.match_1, existsUnique_add_zsmul_mem_Ico, Set.Ico, And, HAdd.hAdd, And.intro, Exists.intro, HSMul.hSMul, Function.Periodic.zsmul, Eq.symm, Eq
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
h : Periodic f c
hc : 0 < c
x a : α
⊢ ∃ y ∈ Ioc a (a + c), f x = f y

Tactic:
let ⟨n, H, _⟩ := existsUnique_add_zsmul_mem_Ioc hc x a
  ⟨x + n • c, H, (h.zsmul n x).symm⟩

Premises used: Set.Ioc, existsUnique_add_zsmul_mem_Ioc, Membership.mem, Exists, And, HAdd.hAdd, And.intro, Exists.intro, HSMul.hSMul, Function.Periodic.zsmul, Eq.symm, Eq, _private.0.Function.Periodic.exists_mem_Ioc.match_1
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
h : Periodic f c
hc : 0 < c
a : α
⊢ f '' Ioc a (a + c) = range f

Tactic:
(image_subset_range _ _).antisymm <| range_subset_iff.2 fun x =>
    let ⟨y, hy, hyx⟩ := h.exists_mem_Ioc hc x a
    ⟨y, hy, hyx.symm⟩

Premises used: Iff.mpr, Set.Ioc, Membership.mem, Set.image_subset_range, HAdd.hAdd, HasSubset.Subset.antisymm, And.intro, Exists.intro, Set.image, Function.Periodic.exists_mem_Ioc, Set.range_subset_iff, Eq.symm, _private.0.Function.Periodic.image_Ioc.match_1
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
h : Periodic f c
hc : 0 < c
a : α
⊢ f '' Icc a (a + c) = range f

Tactic:
(image_subset_range _ _).antisymm <| h.image_Ioc hc a ▸ image_mono Ioc_subset_Icc_self

Premises used: Set.image_mono, Set.Ioc_subset_Icc_self, Eq.rec, Set.image_subset_range, Function.Periodic.image_Ioc, HasSubset.Subset.antisymm
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
h : Periodic f c
hc_1 : c ≠ 0
a : α
hc : c < 0
inl : f '' Icc (a + c) a = range f
inl₁ : f '' Icc (a + c) a = f '' Icc (a + c) (a + c + -c)
inl₂ inl₃ : f '' Icc (a + c) a = f '' Icc (a + c) a
⊢ f '' uIcc a (a + c) = range f

Tactic:
rw [uIcc_of_ge (add_le_of_nonpos_right hc.le), ← h.neg.image_Icc (neg_pos.2 hc) (a + c),
      add_neg_cancel_right]

Premises used: Iff.mpr, Function.Periodic.image_Icc, neg_pos, add_neg_cancel_right, Set.uIcc_of_ge, LT.lt.le, Function.Periodic.neg, HAdd.hAdd, add_le_of_nonpos_right
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
h : Periodic f c
hc_1 : c ≠ 0
a : α
hc : 0 < c
inr : f '' Icc a (a + c) = range f
inr₁ inr₂ : range f = range f
⊢ f '' uIcc a (a + c) = range f

Tactic:
rw [uIcc_of_le (le_add_of_nonneg_right hc.le), h.image_Icc hc]

Premises used: Function.Periodic.image_Icc, Set.uIcc_of_le, LT.lt.le, le_add_of_nonneg_right
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : Archimedean α
h : Periodic f c
hc : c ≠ 0
a : α
⊢ c < 0 ∨ 0 < c

Tactic:
cases hc.lt_or_gt with
  | inl hc =>
    rw [uIcc_of_ge (add_le_of_nonpos_right hc.le), ← h.neg.image_Icc (neg_pos.2 hc) (a + c),
      add_neg_cancel_right]
  | inr hc => rw [uIcc_of_le (le_add_of_nonneg_right hc.le), h.image_Icc hc]

Premises used: add_neg_cancel_right, Ne.lt_or_gt
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : NonAssocSemiring α
inst_1 : Ring β
h : Antiperiodic f c
n : ℕ
⊢ f (x + (↑n : α) * c) = HPow.hPow (α := β) (-1) n * f x

Tactic:
simpa only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow, Int.cast_neg,
    Int.cast_one] using h.add_nsmul_eq n

Premises used: Int.cast_neg, zsmul_eq_mul, Int.cast_pow, nsmul_eq_mul, Function.Antiperiodic.add_nsmul_eq, Int.cast_one
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : NonAssocRing α
inst_1 : Ring β
h : Antiperiodic f c
n : ℕ
⊢ f (x - (↑n : α) * c) = HPow.hPow (α := β) (-1) n * f x

Tactic:
simpa only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow, Int.cast_neg,
    Int.cast_one] using h.sub_nsmul_eq n

Premises used: Int.cast_neg, zsmul_eq_mul, Int.cast_pow, nsmul_eq_mul, Int.cast_one, Function.Antiperiodic.sub_nsmul_eq
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst : NonAssocRing α
inst_1 : Ring β
h : Antiperiodic f c
n : ℕ
⊢ f ((↑n : α) * c - x) = HPow.hPow (α := β) (-1) n * f (-x)

Tactic:
simpa only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow, Int.cast_neg,
    Int.cast_one] using h.nsmul_sub_eq n

Premises used: Int.cast_neg, zsmul_eq_mul, Int.cast_pow, Function.Antiperiodic.nsmul_sub_eq, nsmul_eq_mul, Int.cast_one
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst : AddMonoid α
inst_1 : Neg β
inst_2 : GroupWithZero γ
inst_3 : DistribMulAction γ α
h : Antiperiodic f c
a : γ
ha : a ≠ 0
x : α
⊢ Eq.{u_2 + 1} (α := β) ((fun (x : α) ↦ f (a • x)) (x + a⁻¹ • c)) (-(fun (x : α) ↦ f (a • x)) x)

Tactic:
simpa only [smul_add, smul_inv_smul₀ ha] using h (a • x)

Premises used: smul_inv_smul₀, HSMul.hSMul, smul_add
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : DivisionSemiring α
inst_1 : Neg β
h : Antiperiodic f c
a : α
ha : a ≠ 0
⊢ Antiperiodic.{u_1, u_2} (β := β) (fun (x : α) ↦ f (a * x)) (a⁻¹ * c)

Tactic:
h.const_smul₀ ha

Premises used: Function.Antiperiodic.const_smul₀
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst : AddMonoid α
inst_1 : Neg β
inst_2 : GroupWithZero γ
inst_3 : DistribMulAction γ α
h : Antiperiodic f c
a : γ
ha : a ≠ 0
⊢ Antiperiodic.{u_1, u_2} (β := β) (fun (x : α) ↦ f (a⁻¹ • x)) (a • c)

Tactic:
simpa only [inv_inv] using h.const_smul₀ (inv_ne_zero ha)

Premises used: Function.Antiperiodic.const_smul₀, inv_inv, inv_ne_zero
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : DivisionSemiring α
inst_1 : Neg β
h : Antiperiodic f c
a : α
ha : a ≠ 0
⊢ Antiperiodic.{u_1, u_2} (β := β) (fun (x : α) ↦ f (a⁻¹ * x)) (a * c)

Tactic:
h.const_inv_smul₀ ha

Premises used: Function.Antiperiodic.const_inv_smul₀
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : DivisionSemiring α
inst_1 : Neg β
h : Antiperiodic f c
a : α
ha : a ≠ 0
⊢ Antiperiodic.{u_1, u_2} (β := β) (fun (x : α) ↦ f (x * a)) (c * a⁻¹)

Tactic:
h.const_smul₀ <| (MulOpposite.op_ne_zero_iff a).mpr ha

Premises used: Iff.mpr, MulOpposite.op_ne_zero_iff, Function.Antiperiodic.const_smul₀, MulOpposite.unop
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : DivisionSemiring α
inst_1 : Neg β
h : Antiperiodic f c
a : α
ha : a ≠ 0
⊢ Antiperiodic.{u_1, u_2} (β := β) (fun (x : α) ↦ f (x * a)) (c / a)

Tactic:
simpa only [div_eq_mul_inv] using h.mul_const ha

Premises used: div_eq_mul_inv, Function.Antiperiodic.mul_const
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : DivisionSemiring α
inst_1 : Neg β
h : Antiperiodic f c
a : α
ha : a ≠ 0
⊢ Antiperiodic.{u_1, u_2} (β := β) (fun (x : α) ↦ f (x * a⁻¹)) (c * a)

Tactic:
h.const_inv_smul₀ <| (MulOpposite.op_ne_zero_iff a).mpr ha

Premises used: Iff.mpr, MulOpposite.op_ne_zero_iff, Function.Antiperiodic.const_inv_smul₀, MulOpposite.unop
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst : DivisionSemiring α
inst_1 : Neg β
h : Antiperiodic f c
a : α
ha : a ≠ 0
⊢ Antiperiodic.{u_1, u_2} (β := β) (fun (x : α) ↦ f (x / a)) (c * a)

Tactic:
simpa only [div_eq_mul_inv] using h.mul_const_inv ha

Premises used: div_eq_mul_inv, Function.Antiperiodic.mul_const_inv
-- Module: Mathlib.Algebra.Field.Periodic
Goal:
α : Type u_4
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorRing α
⊢ Function.Periodic.{u_4, u_4} (α := α) fract 1

Tactic:
fun a => mod_cast Int.fract_add_intCast a 1

Premises used: Int.cast, congrArg, Int.fract, cast, HAdd.hAdd, Int.fract_add_intCast, Function.Periodic, congrFun', OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Int.cast_one, Eq.trans
-- Module: Mathlib.Algebra.Field.Rat
Goal:
q : ℚ≥0
rw : (↑q : ℚ) = HDiv.hDiv (α := ℚ) (↑(num (↑q : ℚ)) : ℚ) (↑(den (↑q : ℚ)) : ℚ)
⊢ (↑q : ℚ) = HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)

Tactic:
rw [← NNRat.den_coe, ← Int.cast_natCast q.num, ← NNRat.num_coe]

Premises used: Int.cast_natCast, NNRat.den_coe, NNRat.num, NNRat.num_coe
-- Module: Mathlib.Algebra.Field.Rat
Goal:
q : ℚ≥0
⊢ (↑q : ℚ) = HDiv.hDiv (α := ℚ) (↑(num (↑q : ℚ)) : ℚ) (↑(den (↑q : ℚ)) : ℚ)

Tactic:
(num_div_den _).symm

Premises used: Rat.num_div_den, Eq.symm
-- Module: Mathlib.Algebra.Field.Rat
Goal:
q : ℚ≥0
⊢ (↑q : ℚ) = HDiv.hDiv (α := ℚ) (↑(num (↑q : ℚ)) : ℚ) (↑(den (↑q : ℚ)) : ℚ)

Tactic:
exact (num_div_den _).symm

Premises used: Rat.num_div_den, Eq.symm
-- Module: Mathlib.Algebra.Field.Rat
Goal:
a : ℚ
ha : 0 ≤ a
rw : 0 ≤ (↑a.den : ℤ) /. a.num
⊢ 0 ≤ a⁻¹

Tactic:
rw [inv_def]

Premises used: Rat.inv_def
-- Module: Mathlib.Algebra.Field.Rat
Goal:
a : ℚ
ha : 0 ≤ a
⊢ 0 ≤ (↑a.den : ℤ) /. a.num

Tactic:
divInt_nonneg (Int.natCast_nonneg a.den) (num_nonneg.mpr ha)

Premises used: Iff.mpr, Rat.divInt_nonneg, Rat.den, Rat.num_nonneg, Int.natCast_nonneg
-- Module: Mathlib.Algebra.Field.Rat
Goal:
a : ℚ
ha : 0 ≤ a
⊢ 0 ≤ (↑a.den : ℤ) /. a.num

Tactic:
exact divInt_nonneg (Int.natCast_nonneg a.den) (num_nonneg.mpr ha)

Premises used: Iff.mpr, Rat.divInt_nonneg, Rat.den, Rat.num_nonneg, Int.natCast_nonneg
-- Module: Mathlib.Algebra.Field.Rat
Goal:
a b : ℚ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a / b

Tactic:
mul_nonneg ha (Rat.inv_nonneg hb)

Premises used: mul_nonneg, Rat.inv_nonneg, Rat.div
-- Module: Mathlib.Algebra.Field.Rat
Goal:
q : ℚ≥0
⊢ Eq (α := ℚ) (↑q⁻¹ : ℚ) (↑q : ℚ)⁻¹

Tactic:
rfl

Premises used: dite, rfl
-- Module: Mathlib.Algebra.Field.Rat
Goal:
p q : ℚ≥0
⊢ (↑(p / q) : ℚ) = HDiv.hDiv (α := ℚ) (↑p : ℚ) (↑q : ℚ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.Rat
Goal:
p : ℚ≥0
n : ℤ
⊢ (↑(p ^ n) : ℚ) = HPow.hPow (α := ℚ) (↑p : ℚ) n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Field.Rat
Goal:
q : ℚ≥0
a : Eq (α := ℚ) (↑q⁻¹ : ℚ) (↑(divNat q.den q.num) : ℚ)
⊢ q⁻¹ = divNat q.den q.num

Tactic:
ext
-- Module: Mathlib.Algebra.Field.Rat
Goal:
q : ℚ≥0
⊢ Eq (α := ℚ) (↑q⁻¹ : ℚ) (↑(divNat q.den q.num) : ℚ)

Tactic:
simp [Rat.inv_def, num_coe, den_coe]

Premises used: NNRat.den_coe, Rat.inv_def, NNRat.num_coe
-- Module: Mathlib.Algebra.Field.Rat
Goal:
p q : ℚ≥0
a : Eq (α := ℚ) (↑(p / q) : ℚ) (↑(divNat (p.num * q.den) (p.den * q.num)) : ℚ)
⊢ p / q = divNat (p.num * q.den) (p.den * q.num)

Tactic:
ext
-- Module: Mathlib.Algebra.Field.Rat
Goal:
p q : ℚ≥0
⊢ Eq (α := ℚ) (↑(p / q) : ℚ) (↑(divNat (p.num * q.den) (p.den * q.num)) : ℚ)

Tactic:
simp [Rat.div_def', num_coe, den_coe]

Premises used: NNRat.den_coe, Rat.div_def', NNRat.num_coe
-- Module: Mathlib.Algebra.Field.Rat
Goal:
q : ℚ≥0
hq : q ≠ 0
rw : (Int.natAbs (↑q.den : ℤ)).Coprime q.num
⊢ q⁻¹.num = q.den

Tactic:
rw [inv_def, divNat, num, coe_mk, Rat.divInt_ofNat, ← Rat.mk_eq_mkRat _ _ (num_ne_zero.mpr hq),
    Int.natAbs_natCast]

Premises used: Iff.mpr, NNRat.divNat, NNRat.coe_mk, NNRat.num, Rat.divInt_ofNat, NNRat.inv_def, NNRat.num_ne_zero, Int.natAbs_natCast, Rat.mk_eq_mkRat
-- Module: Mathlib.Algebra.Field.Rat
Goal:
q : ℚ≥0
hq : q ≠ 0
⊢ (Int.natAbs (↑q.den : ℤ)).Coprime q.num

Tactic:
simpa using q.coprime_num_den.symm

Premises used: Nat.Coprime.symm, NNRat.coprime_num_den
-- Module: Mathlib.Algebra.Field.Rat
Goal:
q : ℚ≥0
hq : q ≠ 0
rw : (Int.natAbs (↑q.den : ℤ)).Coprime q.num
⊢ q⁻¹.den = q.num

Tactic:
rw [inv_def, divNat, den, coe_mk, Rat.divInt_ofNat, ← Rat.mk_eq_mkRat _ _ (num_ne_zero.mpr hq)]

Premises used: Iff.mpr, NNRat.divNat, NNRat.coe_mk, Rat.divInt_ofNat, NNRat.den, NNRat.inv_def, NNRat.num_ne_zero, Rat.mk_eq_mkRat
-- Module: Mathlib.Algebra.Field.Rat
Goal:
q : ℚ≥0
a : Eq (α := ℚ) (↑(HDiv.hDiv (α := ℚ≥0) (↑q.num : ℚ≥0) (↑q.den : ℚ≥0)) : ℚ) (↑q : ℚ)
⊢ HDiv.hDiv (α := ℚ≥0) (↑q.num : ℚ≥0) (↑q.den : ℚ≥0) = q

Tactic:
ext1
-- Module: Mathlib.Algebra.Field.Rat
Goal:
q : ℚ≥0
⊢ HDiv.hDiv (α := ℚ) (↑(↑(Rat.num (↑q : ℚ)).natAbs : ℤ) : ℚ) (↑q.den : ℚ) = (↑q : ℚ)

Tactic:
(cast_def _).symm

Premises used: NNRat.cast_def, NNRat.num, Eq.symm
-- Module: Mathlib.Algebra.Field.Rat
Goal:
q : ℚ≥0
⊢ HDiv.hDiv (α := ℚ) (↑(↑(Rat.num (↑q : ℚ)).natAbs : ℤ) : ℚ) (↑q.den : ℚ) = (↑q : ℚ)

Tactic:
exact (cast_def _).symm

Premises used: NNRat.cast_def, Eq.symm
-- Module: Mathlib.Algebra.Field.Rat
Goal:
a : ℚ≥0
a₁ : Eq (α := ℚ) (↑(HPow.hPow (β := ℤ) a 0) : ℚ) (↑1 : ℚ)
⊢ HPow.hPow (β := ℤ) a 0 = 1

Tactic:
ext
-- Module: Mathlib.Algebra.Field.Rat
Goal:
a : ℚ≥0
⊢ Eq (α := ℚ) (↑(HPow.hPow (β := ℤ) a 0) : ℚ) (↑1 : ℚ)

Tactic:
apply Field.zpow_zero'

Premises used: Field.zpow_zero'
-- Module: Mathlib.Algebra.Field.Rat
Goal:
n : ℕ
a : ℚ≥0
a₁ : Eq (α := ℚ) (↑(HPow.hPow (β := ℤ) a (↑n.succ : ℤ)) : ℚ) (↑(HPow.hPow (β := ℤ) a (↑n : ℤ) * a) : ℚ)
⊢ HPow.hPow (β := ℤ) a (↑n.succ : ℤ) = HPow.hPow (β := ℤ) a (↑n : ℤ) * a

Tactic:
ext
-- Module: Mathlib.Algebra.Field.Rat
Goal:
n : ℕ
a : ℚ≥0
⊢ Eq (α := ℚ) (↑(HPow.hPow (β := ℤ) a (↑n.succ : ℤ)) : ℚ) (↑(HPow.hPow (β := ℤ) a (↑n : ℤ) * a) : ℚ)

Tactic:
apply Field.zpow_succ'

Premises used: Field.zpow_succ'
-- Module: Mathlib.Algebra.Field.Rat
Goal:
n : ℕ
a : ℚ≥0
a₁ : Eq (α := ℚ) (↑(a ^ Int.negSucc n) : ℚ) (↑(HPow.hPow (β := ℤ) a (↑n.succ : ℤ))⁻¹ : ℚ)
⊢ a ^ Int.negSucc n = (HPow.hPow (β := ℤ) a (↑n.succ : ℤ))⁻¹

Tactic:
ext
-- Module: Mathlib.Algebra.Field.Rat
Goal:
n : ℕ
a : ℚ≥0
⊢ Eq (α := ℚ) (↑(a ^ Int.negSucc n) : ℚ) (↑(HPow.hPow (β := ℤ) a (↑n.succ : ℤ))⁻¹ : ℚ)

Tactic:
apply Field.zpow_neg'

Premises used: Field.zpow_neg'
-- Module: Mathlib.Algebra.Field.Rat
Goal:
a : Eq (α := ℚ) (↑0⁻¹ : ℚ) (↑0 : ℚ)
⊢ Eq (α := ℚ≥0) 0⁻¹ 0

Tactic:
ext
-- Module: Mathlib.Algebra.Field.Rat
Goal:
⊢ Eq (α := ℚ) (↑0⁻¹ : ℚ) (↑0 : ℚ)

Tactic:
simp
-- Module: Mathlib.Algebra.Field.Rat
Goal:
q : ℚ≥0
h : q ≠ 0
a : Eq (α := ℚ) (↑(q * q⁻¹) : ℚ) (↑1 : ℚ)
⊢ q * q⁻¹ = 1

Tactic:
ext
-- Module: Mathlib.Algebra.Field.Rat
Goal:
q : ℚ≥0
h : q ≠ 0
⊢ Eq (α := ℚ) (↑(q * q⁻¹) : ℚ) (↑1 : ℚ)

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
l : List K
⊢ (∀ x ∈ l, x ∈ s) → l.prod ∈ s

Tactic:
list_prod_mem

Premises used: list_prod_mem, Set.Mem
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
l : List K
⊢ (∀ x ∈ l, x ∈ s) → l.sum ∈ s

Tactic:
list_sum_mem

Premises used: Set.Mem, list_sum_mem
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
m : Multiset K
⊢ (∀ a ∈ m, a ∈ s) → m.sum ∈ s

Tactic:
multiset_sum_mem m

Premises used: multiset_sum_mem
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
s : Subfield K
ι : Type u_1
t : Finset ι
f : ι → K
h : ∀ c ∈ t, f c ∈ s
⊢ ∑ i ∈ t, f i ∈ s

Tactic:
sum_mem h

Premises used: sum_mem
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
x : K
⊢ Membership.mem (γ := Subfield K) ⊤ x

Tactic:
Set.mem_univ x

Premises used: Set.Mem, Set.univ, setOf, Set.mem_univ
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
inst : DivisionRing K
⊢ (↑⊤ : Set K) = Set.univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
M : Type w
inst : DivisionRing K
inst_1 : DivisionRing L
inst_2 : DivisionRing M
s_1 t : Subfield K
f : K →+* L
s : Subfield L
x : K
hx :
  Membership.mem (γ := Set K)
    (Subsemigroup.carrier
      (Submonoid.toSubsemigroup (Subsemiring.toSubmonoid (Subring.toSubsemiring (Subring.comap f s.toSubring)))))
    x
rw : Membership.mem (α := L) s (((f : (a : K) → L) x)⁻¹ : L)
⊢ Membership.mem (α := L) s ((f : (a : K) → L) x⁻¹ : L)

Tactic:
rw [map_inv₀ f]

Premises used: map_inv₀
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
M : Type w
inst : DivisionRing K
inst_1 : DivisionRing L
inst_2 : DivisionRing M
s_1 t : Subfield K
f : K →+* L
s : Subfield L
x : K
hx :
  Membership.mem (γ := Set K)
    (Subsemigroup.carrier
      (Submonoid.toSubsemigroup (Subsemiring.toSubmonoid (Subring.toSubsemiring (Subring.comap f s.toSubring)))))
    x
⊢ Membership.mem (α := L) s (((f : (a : K) → L) x)⁻¹ : L)

Tactic:
s.inv_mem hx

Premises used: Subfield.inv_mem
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
M : Type w
inst : DivisionRing K
inst_1 : DivisionRing L
inst_2 : DivisionRing M
s_1 t : Subfield K
f : K →+* L
s : Subfield L
x : K
hx :
  Membership.mem (γ := Set K)
    (Subsemigroup.carrier
      (Submonoid.toSubsemigroup (Subsemiring.toSubmonoid (Subring.toSubsemiring (Subring.comap f s.toSubring)))))
    x
⊢ Membership.mem (α := L) s (((f : (a : K) → L) x)⁻¹ : L)

Tactic:
exact s.inv_mem hx

Premises used: Subfield.inv_mem
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
f : K →+* L
s : Subfield L
⊢ (↑(comap f s) : Set K) = (⇑f : (a : K) → L) ⁻¹' (↑s : Set L)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
s : Subfield L
f : K →+* L
x : K
⊢ x ∈ comap f s ↔ Membership.mem (α := L) s ((f : (a : K) → L) x : L)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
M : Type w
inst : DivisionRing K
inst_1 : DivisionRing L
inst_2 : DivisionRing M
s : Subfield M
g : L →+* M
f : K →+* L
⊢ comap f (comap g s) = comap (g.comp f) s

Tactic:
rfl

Premises used: Set.Mem, setOf, Subfield.comap, Set.preimage, Subring.comap, rfl
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
M : Type w
inst : DivisionRing K
inst_1 : DivisionRing L
inst_2 : DivisionRing M
s_1 t : Subfield K
f : K →+* L
s : Subfield K
x : K
hx : x ∈ s.carrier
⊢ Membership.mem.{v, v} (α := L) (γ := Set L)
    (Subsemigroup.carrier
      (Submonoid.toSubsemigroup (Subsemiring.toSubmonoid (Subring.toSubsemiring (Subring.map f s.toSubring)))))
    (((f : (a : K) → L) x)⁻¹ : L)

Tactic:
⟨x⁻¹, s.inv_mem hx, map_inv₀ f x⟩

Premises used: Set.Mem, setOf, map_inv₀, Subfield.inv_mem, Inv.inv, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
M : Type w
inst : DivisionRing K
inst_1 : DivisionRing L
inst_2 : DivisionRing M
s_1 t : Subfield K
f : K →+* L
s : Subfield K
x : K
hx : x ∈ s.carrier
⊢ Membership.mem.{v, v} (α := L) (γ := Set L)
    (Subsemigroup.carrier
      (Submonoid.toSubsemigroup (Subsemiring.toSubmonoid (Subring.toSubsemiring (Subring.map f s.toSubring)))))
    (((f : (a : K) → L) x)⁻¹ : L)

Tactic:
exact ⟨x⁻¹, s.inv_mem hx, map_inv₀ f x⟩
-- Module: Mathlib.Algebra.Field.Subfield.Basic
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
s : Subfield K
f : K →+* L
⊢ (↑(map f s) : Set L) = (⇑f : (a : K) → L) '' (↑s : Set K)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.image, rfl