awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Field.Opposite (goal)
Goal:
α : Type u_1
inst : DivisionSemiring α
q : ℚ≥0
rw : (↑q : α) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
rw₁ : (↑q : α) = HDiv.hDiv (α := α) (unop (↑q.num : αᵃᵒᵖ)) (unop (↑q.den : αᵃᵒᵖ))
rw₂ : (↑q : α) = HDiv.hDiv (α := α) (↑q.num : α) (unop (↑q.den : αᵃᵒᵖ))
⊢ unop (↑q : αᵃᵒᵖ) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
have rw₃ : (↑q : α) = HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)
Tactic: rw [unop_nnratCast, unop_div, unop_natCast, unop_natCast,
    NNRat.cast_def, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Field.Opposite (goal)
Goal:
α : Type u_1
inst : DivisionSemiring α
q : ℚ≥0
rw : (↑q : α) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
rw₁ : (↑q : α) = HDiv.hDiv (α := α) (unop (↑q.num : αᵃᵒᵖ)) (unop (↑q.den : αᵃᵒᵖ))
rw₂ : (↑q : α) = HDiv.hDiv (α := α) (↑q.num : α) (unop (↑q.den : αᵃᵒᵖ))
rw₃ : (↑q : α) = HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)
⊢ unop (↑q : αᵃᵒᵖ) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
have rw₄ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)
Tactic: rw [unop_nnratCast, unop_div, unop_natCast, unop_natCast,
    NNRat.cast_def, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Field.Opposite (goal)
Goal:
α : Type u_1
inst : DivisionSemiring α
q : ℚ≥0
rw : (↑q : α) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
rw₁ : (↑q : α) = HDiv.hDiv (α := α) (unop (↑q.num : αᵃᵒᵖ)) (unop (↑q.den : αᵃᵒᵖ))
rw₂ : (↑q : α) = HDiv.hDiv (α := α) (↑q.num : α) (unop (↑q.den : αᵃᵒᵖ))
rw₃ : (↑q : α) = HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)
rw₄ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)
⊢ unop (↑q : αᵃᵒᵖ) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
have rw₅ : HMul.hMul (α := α) (↑q.num : α) (↑q.den : α)⁻¹ = HMul.hMul (α := α) (↑q.num : α) (↑q.den : α)⁻¹
Tactic: rw [unop_nnratCast, unop_div, unop_natCast, unop_natCast,
    NNRat.cast_def, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Field.Opposite (goal)
Goal:
α : Type u_1
inst : DivisionRing α
q : ℚ
⊢ unop (↑q : αᵃᵒᵖ) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
have rw : (↑q : α) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
Tactic: rw [unop_ratCast, Rat.cast_def, unop_div, unop_natCast,
    unop_intCast, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Field.Opposite (goal)
Goal:
α : Type u_1
inst : DivisionRing α
q : ℚ
rw : (↑q : α) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
⊢ unop (↑q : αᵃᵒᵖ) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
have rw₁ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
Tactic: rw [unop_ratCast, Rat.cast_def, unop_div, unop_natCast,
    unop_intCast, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Field.Opposite (goal)
Goal:
α : Type u_1
inst : DivisionRing α
q : ℚ
rw : (↑q : α) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
rw₁ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
⊢ unop (↑q : αᵃᵒᵖ) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
have rw₂ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HDiv.hDiv (α := α) (unop (↑q.num : αᵃᵒᵖ)) (unop (↑q.den : αᵃᵒᵖ))
Tactic: rw [unop_ratCast, Rat.cast_def, unop_div, unop_natCast,
    unop_intCast, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Field.Opposite (goal)
Goal:
α : Type u_1
inst : DivisionRing α
q : ℚ
rw : (↑q : α) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
rw₁ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
rw₂ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HDiv.hDiv (α := α) (unop (↑q.num : αᵃᵒᵖ)) (unop (↑q.den : αᵃᵒᵖ))
⊢ unop (↑q : αᵃᵒᵖ) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
have rw₃ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HDiv.hDiv (α := α) (unop (↑q.num : αᵃᵒᵖ)) (↑q.den : α)
Tactic: rw [unop_ratCast, Rat.cast_def, unop_div, unop_natCast,
    unop_intCast, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Field.Opposite (goal)
Goal:
α : Type u_1
inst : DivisionRing α
q : ℚ
rw : (↑q : α) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
rw₁ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
rw₂ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HDiv.hDiv (α := α) (unop (↑q.num : αᵃᵒᵖ)) (unop (↑q.den : αᵃᵒᵖ))
rw₃ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HDiv.hDiv (α := α) (unop (↑q.num : αᵃᵒᵖ)) (↑q.den : α)
⊢ unop (↑q : αᵃᵒᵖ) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
have rw₄ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)
Tactic: rw [unop_ratCast, Rat.cast_def, unop_div, unop_natCast,
    unop_intCast, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Field.Opposite (goal)
Goal:
α : Type u_1
inst : DivisionRing α
q : ℚ
rw : (↑q : α) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
rw₁ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
rw₂ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HDiv.hDiv (α := α) (unop (↑q.num : αᵃᵒᵖ)) (unop (↑q.den : αᵃᵒᵖ))
rw₃ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HDiv.hDiv (α := α) (unop (↑q.num : αᵃᵒᵖ)) (↑q.den : α)
rw₄ : HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α) = HDiv.hDiv (α := α) (↑q.num : α) (↑q.den : α)
⊢ unop (↑q : αᵃᵒᵖ) = unop (HDiv.hDiv (α := αᵃᵒᵖ) (↑q.num : αᵃᵒᵖ) (↑q.den : αᵃᵒᵖ))
have rw₅ : HMul.hMul (α := α) (↑q.num : α) (↑q.den : α)⁻¹ = HMul.hMul (α := α) (↑q.num : α) (↑q.den : α)⁻¹
Tactic: rw [unop_ratCast, Rat.cast_def, unop_div, unop_natCast,
    unop_intCast, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Algebra.Field.Periodic (goal)
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 : α
⊢ Eq.{u_2 + 1} (α := β) ((fun (x : α) ↦ f (a • x)) (x + a⁻¹ • c)) ((fun (x : α) ↦ f (a • x)) x)
have pos : ∀ (ha : a = 0), Eq.{u_2 + 1} (α := β) ((fun (x : α) ↦ f (a • x)) (x + a⁻¹ • c)) ((fun (x : α) ↦ f (a • x)) x)
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Field.Periodic (goal)
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)
⊢ Eq.{u_2 + 1} (α := β) ((fun (x : α) ↦ f (a • x)) (x + a⁻¹ • c)) ((fun (x : α) ↦ f (a • x)) x)
have neg : ∀ (ha : ¬a = 0), Eq.{u_2 + 1} (α := β) ((fun (x : α) ↦ f (a • x)) (x + a⁻¹ • c)) ((fun (x : α) ↦ f (a • x)) x)
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Field.Periodic (goal)
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
⊢ f '' uIcc a (a + c) = range f
have inl : f '' Icc (a + c) a = 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]
-- Lean 4 proof step from Mathlib.Algebra.Field.Periodic (goal)
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
⊢ f '' uIcc a (a + c) = range f
have inl₁ : f '' Icc (a + c) a = f '' Icc (a + c) (a + c + -c)
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]
-- Lean 4 proof step from Mathlib.Algebra.Field.Periodic (goal)
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)
⊢ f '' uIcc a (a + c) = range f
have inl₂ : f '' Icc (a + c) a = f '' Icc (a + c) a
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]
-- Lean 4 proof step from Mathlib.Algebra.Field.Periodic (goal)
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
⊢ f '' uIcc a (a + c) = range f
have inr : f '' Icc a (a + c) = range f
Tactic: rw [uIcc_of_le (le_add_of_nonneg_right hc.le), h.image_Icc hc]
-- Lean 4 proof step from Mathlib.Algebra.Field.Periodic (goal)
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
⊢ f '' uIcc a (a + c) = range f
have inr₁ : range f = range f
Tactic: rw [uIcc_of_le (le_add_of_nonneg_right hc.le), h.image_Icc hc]
-- Lean 4 proof step from Mathlib.Algebra.Field.Periodic (hypothesis)
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 : α
⊢ f '' uIcc a (a + c) = range f
have x : 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]
-- Lean 4 proof step from Mathlib.Algebra.Field.Rat (goal)
Goal:
q : ℚ≥0
⊢ (↑q : ℚ) = HDiv.hDiv (α := ℚ) (↑q.num : ℚ) (↑q.den : ℚ)
have rw : (↑q : ℚ) = HDiv.hDiv (α := ℚ) (↑(num (↑q : ℚ)) : ℚ) (↑(den (↑q : ℚ)) : ℚ)
Tactic: rw [← NNRat.den_coe, ← Int.cast_natCast q.num, ← NNRat.num_coe]
-- Lean 4 proof step from Mathlib.Algebra.Field.Rat (goal)
Goal:
a : ℚ
ha : 0 ≤ a
⊢ 0 ≤ a⁻¹
have rw : 0 ≤ (↑a.den : ℤ) /. a.num
Tactic: rw [inv_def]
-- Lean 4 proof step from Mathlib.Algebra.Field.Rat (goal)
Goal:
q : ℚ≥0
⊢ q⁻¹ = divNat q.den q.num
have a : Eq (α := ℚ) (↑q⁻¹ : ℚ) (↑(divNat q.den q.num) : ℚ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Field.Rat (goal)
Goal:
p q : ℚ≥0
⊢ p / q = divNat (p.num * q.den) (p.den * q.num)
have a : Eq (α := ℚ) (↑(p / q) : ℚ) (↑(divNat (p.num * q.den) (p.den * q.num)) : ℚ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Field.Rat (goal)
Goal:
q : ℚ≥0
hq : q ≠ 0
⊢ q⁻¹.num = q.den
have rw : (Int.natAbs (↑q.den : ℤ)).Coprime q.num
Tactic: rw [inv_def, divNat, num, coe_mk, Rat.divInt_ofNat, ← Rat.mk_eq_mkRat _ _ (num_ne_zero.mpr hq),
    Int.natAbs_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Field.Rat (goal)
Goal:
q : ℚ≥0
hq : q ≠ 0
⊢ q⁻¹.den = q.num
have rw : (Int.natAbs (↑q.den : ℤ)).Coprime q.num
Tactic: rw [inv_def, divNat, den, coe_mk, Rat.divInt_ofNat, ← Rat.mk_eq_mkRat _ _ (num_ne_zero.mpr hq)]
-- Lean 4 proof step from Mathlib.Algebra.Field.Rat (goal)
Goal:
q : ℚ≥0
⊢ HDiv.hDiv (α := ℚ≥0) (↑q.num : ℚ≥0) (↑q.den : ℚ≥0) = q
have a : Eq (α := ℚ) (↑(HDiv.hDiv (α := ℚ≥0) (↑q.num : ℚ≥0) (↑q.den : ℚ≥0)) : ℚ) (↑q : ℚ)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Field.Rat (goal)
Goal:
a : ℚ≥0
⊢ HPow.hPow (β := ℤ) a 0 = 1
have a₁ : Eq (α := ℚ) (↑(HPow.hPow (β := ℤ) a 0) : ℚ) (↑1 : ℚ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Field.Rat (goal)
Goal:
n : ℕ
a : ℚ≥0
⊢ HPow.hPow (β := ℤ) a (↑n.succ : ℤ) = HPow.hPow (β := ℤ) a (↑n : ℤ) * a
have a₁ : Eq (α := ℚ) (↑(HPow.hPow (β := ℤ) a (↑n.succ : ℤ)) : ℚ) (↑(HPow.hPow (β := ℤ) a (↑n : ℤ) * a) : ℚ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Field.Rat (goal)
Goal:
n : ℕ
a : ℚ≥0
⊢ a ^ Int.negSucc n = (HPow.hPow (β := ℤ) a (↑n.succ : ℤ))⁻¹
have a₁ : Eq (α := ℚ) (↑(a ^ Int.negSucc n) : ℚ) (↑(HPow.hPow (β := ℤ) a (↑n.succ : ℤ))⁻¹ : ℚ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Field.Rat (goal)
Goal:
⊢ Eq (α := ℚ≥0) 0⁻¹ 0
have a : Eq (α := ℚ) (↑0⁻¹ : ℚ) (↑0 : ℚ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Field.Rat (goal)
Goal:
q : ℚ≥0
h : q ≠ 0
⊢ q * q⁻¹ = 1
have a : Eq (α := ℚ) (↑(q * q⁻¹) : ℚ) (↑1 : ℚ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Field.Subfield.Basic (goal)
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)
have rw : Membership.mem (α := L) s (((f : (a : K) → L) x)⁻¹ : L)
Tactic: rw [map_inv₀ f]
-- Lean 4 proof step from Mathlib.Algebra.Field.Subfield.Basic (goal)
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
f : K →+* L
⊢ f.fieldRange = Subfield.map f ⊤
have h : ∀ (x : L), x ∈ f.fieldRange ↔ x ∈ Subfield.map f ⊤
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Field.Subfield.Basic (goal)
Goal:
K : Type u
L : Type v
M : Type w
inst : DivisionRing K
inst_1 : DivisionRing L
inst_2 : DivisionRing M
S : Set (Subfield K)
x : K
hx : x ∈ (sInf (toSubring '' S)).carrier
⊢ x⁻¹ ∈ (sInf (toSubring '' S)).carrier
have apply : ∀ p ∈ toSubring '' S, x⁻¹ ∈ p
Tactic: apply Subring.mem_sInf.mpr
-- Lean 4 proof step from Mathlib.Algebra.Field.Subfield.Basic (goal)
Goal:
K : Type u
inst : DivisionRing K
s : Set (Subfield K)
⊢ (sInf s).toSubring = ⨅ t ∈ s, t.toSubring
have h : ∀ (x : K), x ∈ (sInf s).toSubring ↔ Membership.mem (γ := Subring K) (⨅ t ∈ s, t.toSubring) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Field.Subfield.Basic (hypothesis)
Goal:
K : Type u
inst : DivisionRing K
S : Set (Subfield K)
⊢ IsGLB S (sInf S)
have this : ∀ {s t : Subfield K}, (↑s : Set K) ≤ (↑t : Set K) ↔ s ≤ t
Tactic: have : ∀ {s t : Subfield K}, (s : Set K) ≤ t ↔ s ≤ t := by simp [SetLike.coe_subset_coe]
-- Lean 4 proof step from Mathlib.Algebra.Field.Subfield.Basic (goal)
Goal:
K : Type u
inst : DivisionRing K
S : Set (Subfield K)
this : ∀ {s t : Subfield K}, (↑s : Set K) ≤ (↑t : Set K) ↔ s ≤ t
⊢ IsGLB S (sInf S)
have refine : IsGLB ((fun {x : Subfield K} ↦ (↑x : Set K)) '' S) (↑(sInf S) : Set K)
Tactic: refine IsGLB.of_image this ?_
-- Lean 4 proof step from Mathlib.Algebra.Field.Subfield.Basic (goal)
Goal:
K : Type u
inst : DivisionRing K
S : Set (Subfield K)
this : ∀ {s t : Subfield K}, (↑s : Set K) ≤ (↑t : Set K) ↔ s ≤ t
⊢ IsGLB ((fun {x : Subfield K} ↦ (↑x : Set K)) '' S) (↑(sInf S) : Set K)
have h : (↑(sInf S) : Set K) = ⨅ x ∈ S, (↑x : Set K)
Tactic: convert! isGLB_biInf (s := S) (f := SetLike.coe)
-- Lean 4 proof step from Mathlib.Algebra.Field.Subfield.Basic (goal)
Goal:
K : Type u
inst : DivisionRing K
s : Set K
p : (x : K) → Membership.mem (γ := Subfield K) (closure s) x → Prop
mem : ∀ (x : K) (hx : x ∈ s), p x ⋯
one : p 1 ⋯
add :
  ∀ (x y : K) (hx : Membership.mem (γ := Subfield K) (closure s) x)
    (hy : Membership.mem (γ := Subfield K) (closure s) y), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : K) (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx → p (-x) ⋯
inv : ∀ (x : K) (hx : Membership.mem (γ := Subfield K) (closure s) x), p x hx → p x⁻¹ ⋯
mul :
  ∀ (x y : K) (hx : Membership.mem (γ := Subfield K) (closure s) x)
    (hy : Membership.mem (γ := Subfield K) (closure s) y), p x hx → p y hy → p (x * y) ⋯
x : K
h : Membership.mem (γ := Subfield K) (closure s) x
⊢ p 0 ⋯
have simp_rw : p (HAdd.hAdd (α := K) 1 (-1)) sorry
Tactic: simp_rw [← @add_neg_cancel K _ 1]
-- Lean 4 proof step from Mathlib.Algebra.Field.Subfield.Basic (goal)
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
ι : Sort u_1
inst_2 : Nonempty ι
f : K →+* L
s : ι → Subfield K
⊢ map f (iInf s) = ⨅ (i : ι), map f (s i)
have a : (↑(map f (iInf s)) : Set L) = (↑(⨅ (i : ι), map f (s i)) : Set L)
Tactic: apply SetLike.coe_injective
-- Lean 4 proof step from Mathlib.Algebra.Field.Subfield.Basic (hypothesis)
Goal:
K : Type u
inst : DivisionRing K
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun (x1 x2 : Subfield K) ↦ x1 ≤ x2) S
x : K
s : Subfield K :=
  let __spread.0 := Subring.copy (⨆ (i : ι), (S i).toSubring) (⋃ (i : ι), (↑(S i).toSubring : Set K)) ⋯;
  { toSubring := __spread.0, inv_mem' := ⋯ }
⊢ Membership.mem (γ := Subfield K) (⨆ (i : ι), S i) x ↔ ∃ (i : ι), x ∈ S i
have this : iSup S = s
Tactic: have : iSup S = s := le_antisymm
    (iSup_le fun i ↦ le_iSup (fun i ↦ (S i : Set K)) i) (Set.iUnion_subset fun _ ↦ le_iSup S _)
-- Lean 4 proof step from Mathlib.Algebra.Field.Subfield.Basic (hypothesis)
Goal:
K : Type u
inst : DivisionRing K
S : Set (Subfield K)
Sne : S.Nonempty
hS : DirectedOn (fun (x1 x2 : Subfield K) ↦ x1 ≤ x2) S
x : K
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
have this : Nonempty.{u + 1} (↑S : Type u)
Tactic: haveI : Nonempty S := Sne.to_subtype
-- Lean 4 proof step from Mathlib.Algebra.Field.Subfield.Basic (goal)
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
f : K →+* L
x : ↥f.fieldRange
⊢ (f : (a : K) → L) ((f.rangeRestrictFieldEquiv.symm : (a : ↥f.fieldRange) → K) x : K) = (↑x : L)
have rw : (↑((f.rangeRestrictFieldEquiv : (a : K) → ↥f.fieldRange)
        ((f.rangeRestrictFieldEquiv.symm : (a : ↥f.fieldRange) → K) x)) :
    L) =
  (↑x : L)
Tactic: rw [← rangeRestrictFieldEquiv_apply_coe, RingEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Field.Subfield.Basic (goal)
Goal:
K : Type u
L : Type v
inst : DivisionRing K
inst_1 : DivisionRing L
f : K →+* L
x : ↥f.fieldRange
rw :
  (↑((f.rangeRestrictFieldEquiv : (a : K) → ↥f.fieldRange)
          ((f.rangeRestrictFieldEquiv.symm : (a : ↥f.fieldRange) → K) x)) :
      L) =
    (↑x : L)
⊢ (f : (a : K) → L) ((f.rangeRestrictFieldEquiv.symm : (a : ↥f.fieldRange) → K) x : K) = (↑x : L)
have rw₁ : (↑x : L) = (↑x : L)
Tactic: rw [← rangeRestrictFieldEquiv_apply_coe, RingEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Field.Subfield.Basic (goal)
Goal:
K_1 : Type u
L : Type v
M : Type w
inst : DivisionRing K_1
inst_1 : DivisionRing L
inst_2 : DivisionRing M
s_1 : Set K_1
K : Type u
inst_3 : Field K
s_2 : Subfield K
s : Set K
a b : K
x_mem :
  Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    a
y_mem :
  Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    b
⊢ Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (a + b)
have obtain : ∀ (nx : K) (hnx : Membership.mem (γ := Subring K) (Subring.closure s) nx) (dx : K)
  (hdx : Membership.mem (γ := Subring K) (Subring.closure s) dx)
  (x_mem :
    Membership.mem (γ := Set K)
      {z : K |
        ∃ (x : K),
          Membership.mem (γ := Subring K) (Subring.closure s) x ∧
            ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
      (nx / dx)),
  Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (nx / dx + b)
Tactic: obtain ⟨nx, hnx, dx, hdx, rfl⟩ := id x_mem
Cleared hypotheses: a, x_mem
-- Lean 4 proof step from Mathlib.Algebra.Field.Subfield.Basic (goal)
Goal:
K_1 : Type u
L : Type v
M : Type w
inst : DivisionRing K_1
inst_1 : DivisionRing L
inst_2 : DivisionRing M
s_1 : Set K_1
K : Type u
inst_3 : Field K
s_2 : Subfield K
s : Set K
b : K
y_mem :
  Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    b
nx : K
hnx : Membership.mem (γ := Subring K) (Subring.closure s) nx
dx : K
hdx : Membership.mem (γ := Subring K) (Subring.closure s) dx
x_mem :
  Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (nx / dx)
⊢ Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (nx / dx + b)
have obtain : ∀ (ny : K) (hny : Membership.mem (γ := Subring K) (Subring.closure s) ny) (dy : K)
  (hdy : Membership.mem (γ := Subring K) (Subring.closure s) dy)
  (y_mem :
    Membership.mem (γ := Set K)
      {z : K |
        ∃ (x : K),
          Membership.mem (γ := Subring K) (Subring.closure s) x ∧
            ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
      (ny / dy)),
  Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (nx / dx + ny / dy)
Tactic: obtain ⟨ny, hny, dy, hdy, rfl⟩ := id y_mem
Cleared hypotheses: b, y_mem
-- Lean 4 proof step from Mathlib.Algebra.Field.Subfield.Basic (goal)
Goal:
K_1 : Type u
L : Type v
M : Type w
inst : DivisionRing K_1
inst_1 : DivisionRing L
inst_2 : DivisionRing M
s_1 : Set K_1
K : Type u
inst_3 : Field K
s_2 : Subfield K
s : Set K
nx : K
hnx : Membership.mem (γ := Subring K) (Subring.closure s) nx
dx : K
hdx : Membership.mem (γ := Subring K) (Subring.closure s) dx
x_mem :
  Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (nx / dx)
ny : K
hny : Membership.mem (γ := Subring K) (Subring.closure s) ny
dy : K
hdy : Membership.mem (γ := Subring K) (Subring.closure s) dy
y_mem :
  Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (ny / dy)
⊢ Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (nx / dx + ny / dy)
have pos : ∀ (hx0 : dx = 0),
  Membership.mem (γ := Set K)
    {z : K |
      ∃ (x : K),
        Membership.mem (γ := Subring K) (Subring.closure s) x ∧
          ∃ (y : K), Membership.mem (γ := Subring K) (Subring.closure s) y ∧ x / y = z}
    (nx / dx + ny / dy)
Tactic: by_cases hx0 : dx = 0