awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
Goal:
R : Type u_1
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : IsLocalRing R
f : R →+* K
⊢ ∃ (A : ValuationSubring K) (h : ∀ (x : R), Membership.mem (α := K) A.toSubring ((f : (a : R) → K) x : K)),
    IsLocalHom (R := R) (S := ↥A.toSubring) (F := RingHom.{u_1, u_3} R ↥A.toSubring) (f.codRestrict A.toSubring h)
have obtain : ∀ (B : ValuationSubring K) (hB : LocalSubring.range f ≤ B.toLocalSubring),
  ∃ (A : ValuationSubring K) (h : ∀ (x : R), Membership.mem (α := K) A.toSubring ((f : (a : R) → K) x : K)),
    IsLocalHom (R := R) (S := ↥A.toSubring) (F := RingHom.{u_1, u_3} R ↥A.toSubring) (f.codRestrict A.toSubring h)
Tactic: obtain ⟨B, hB⟩ := (LocalSubring.range f).exists_le_valuationSubring
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.LocalSubring (goal)
Goal:
R : Type u_1
K : Type u_3
inst : CommRing R
inst_1 : Field K
inst_2 : IsLocalRing R
f : R →+* K
B : ValuationSubring K
hB : LocalSubring.range f ≤ B.toLocalSubring
⊢ ∃ (A : ValuationSubring K) (h : ∀ (x : R), Membership.mem (α := K) A.toSubring ((f : (a : R) → K) x : K)),
    IsLocalHom (R := R) (S := ↥A.toSubring) (F := RingHom.{u_1, u_3} R ↥A.toSubring) (f.codRestrict A.toSubring h)
have refine : IsLocalHom (R := R) (S := ↥B.toSubring) (F := RingHom.{u_1, u_3} R ↥B.toSubring) (f.codRestrict B.toSubring sorry)
Tactic: refine ⟨B, fun x ↦ hB.1 ⟨x, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Minpoly (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
x : K
⊢ Eq.{u_2 + 1} (α := Γ₀)
    ((v : (a : K) → Γ₀) (coeff (minpoly.{u_1, u_3} K (B := L) ((algebraMap K L : (a : K) → L) x : L)) 0) : Γ₀)
    ((v : (a : K) → Γ₀) x : Γ₀)
have rw : Eq.{u_2 + 1} (α := Γ₀)
  ((v : (a : K) → Γ₀) ((HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])).coeff 0) : Γ₀)
  ((v : (a : K) → Γ₀) x : Γ₀)
Tactic: rw [minpoly.eq_X_sub_C, coeff_sub, coeff_X_zero, coeff_C_zero, zero_sub, Valuation.map_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Minpoly (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
x : K
rw :
  Eq.{u_2 + 1} (α := Γ₀)
    ((v : (a : K) → Γ₀) ((HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])).coeff 0) : Γ₀)
    ((v : (a : K) → Γ₀) x : Γ₀)
⊢ Eq.{u_2 + 1} (α := Γ₀)
    ((v : (a : K) → Γ₀) (coeff (minpoly.{u_1, u_3} K (B := L) ((algebraMap K L : (a : K) → L) x : L)) 0) : Γ₀)
    ((v : (a : K) → Γ₀) x : Γ₀)
have rw₁ : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (HSub.hSub (α := K) (coeff X 0) (coeff ((C : (a : K) → K[X]) x) 0)) : Γ₀)
  ((v : (a : K) → Γ₀) x : Γ₀)
Tactic: rw [minpoly.eq_X_sub_C, coeff_sub, coeff_X_zero, coeff_C_zero, zero_sub, Valuation.map_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Minpoly (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
x : K
rw :
  Eq.{u_2 + 1} (α := Γ₀)
    ((v : (a : K) → Γ₀) ((HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])).coeff 0) : Γ₀)
    ((v : (a : K) → Γ₀) x : Γ₀)
rw₁ :
  Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (HSub.hSub (α := K) (coeff X 0) (coeff ((C : (a : K) → K[X]) x) 0)) : Γ₀)
    ((v : (a : K) → Γ₀) x : Γ₀)
⊢ Eq.{u_2 + 1} (α := Γ₀)
    ((v : (a : K) → Γ₀) (coeff (minpoly.{u_1, u_3} K (B := L) ((algebraMap K L : (a : K) → L) x : L)) 0) : Γ₀)
    ((v : (a : K) → Γ₀) x : Γ₀)
have rw₂ : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (HSub.hSub (α := K) 0 (coeff ((C : (a : K) → K[X]) x) 0)) : Γ₀)
  ((v : (a : K) → Γ₀) x : Γ₀)
Tactic: rw [minpoly.eq_X_sub_C, coeff_sub, coeff_X_zero, coeff_C_zero, zero_sub, Valuation.map_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Minpoly (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
x : K
rw :
  Eq.{u_2 + 1} (α := Γ₀)
    ((v : (a : K) → Γ₀) ((HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])).coeff 0) : Γ₀)
    ((v : (a : K) → Γ₀) x : Γ₀)
rw₁ :
  Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (HSub.hSub (α := K) (coeff X 0) (coeff ((C : (a : K) → K[X]) x) 0)) : Γ₀)
    ((v : (a : K) → Γ₀) x : Γ₀)
rw₂ :
  Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (HSub.hSub (α := K) 0 (coeff ((C : (a : K) → K[X]) x) 0)) : Γ₀)
    ((v : (a : K) → Γ₀) x : Γ₀)
⊢ Eq.{u_2 + 1} (α := Γ₀)
    ((v : (a : K) → Γ₀) (coeff (minpoly.{u_1, u_3} K (B := L) ((algebraMap K L : (a : K) → L) x : L)) 0) : Γ₀)
    ((v : (a : K) → Γ₀) x : Γ₀)
have rw₃ : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (0 - x) : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
Tactic: rw [minpoly.eq_X_sub_C, coeff_sub, coeff_X_zero, coeff_C_zero, zero_sub, Valuation.map_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Minpoly (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
x : K
rw :
  Eq.{u_2 + 1} (α := Γ₀)
    ((v : (a : K) → Γ₀) ((HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])).coeff 0) : Γ₀)
    ((v : (a : K) → Γ₀) x : Γ₀)
rw₁ :
  Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (HSub.hSub (α := K) (coeff X 0) (coeff ((C : (a : K) → K[X]) x) 0)) : Γ₀)
    ((v : (a : K) → Γ₀) x : Γ₀)
rw₂ :
  Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (HSub.hSub (α := K) 0 (coeff ((C : (a : K) → K[X]) x) 0)) : Γ₀)
    ((v : (a : K) → Γ₀) x : Γ₀)
rw₃ : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (0 - x) : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
⊢ Eq.{u_2 + 1} (α := Γ₀)
    ((v : (a : K) → Γ₀) (coeff (minpoly.{u_1, u_3} K (B := L) ((algebraMap K L : (a : K) → L) x : L)) 0) : Γ₀)
    ((v : (a : K) → Γ₀) x : Γ₀)
have rw₄ : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (-x) : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
Tactic: rw [minpoly.eq_X_sub_C, coeff_sub, coeff_X_zero, coeff_C_zero, zero_sub, Valuation.map_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Minpoly (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
x : K
rw :
  Eq.{u_2 + 1} (α := Γ₀)
    ((v : (a : K) → Γ₀) ((HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])).coeff 0) : Γ₀)
    ((v : (a : K) → Γ₀) x : Γ₀)
rw₁ :
  Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (HSub.hSub (α := K) (coeff X 0) (coeff ((C : (a : K) → K[X]) x) 0)) : Γ₀)
    ((v : (a : K) → Γ₀) x : Γ₀)
rw₂ :
  Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (HSub.hSub (α := K) 0 (coeff ((C : (a : K) → K[X]) x) 0)) : Γ₀)
    ((v : (a : K) → Γ₀) x : Γ₀)
rw₃ : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (0 - x) : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
rw₄ : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (-x) : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
⊢ Eq.{u_2 + 1} (α := Γ₀)
    ((v : (a : K) → Γ₀) (coeff (minpoly.{u_1, u_3} K (B := L) ((algebraMap K L : (a : K) → L) x : L)) 0) : Γ₀)
    ((v : (a : K) → Γ₀) x : Γ₀)
have rw₅ : Eq.{u_2 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
Tactic: rw [minpoly.eq_X_sub_C, coeff_sub, coeff_X_zero, coeff_C_zero, zero_sub, Valuation.map_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Minpoly (hypothesis)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : FiniteDimensional K L
x : L
hx : IsUnit x
⊢ HPow.hPow (α := Γ₀) ((v : (a : K) → Γ₀) (coeff (minpoly K x) 0) : Γ₀) (finrank K L / natDegree (minpoly K x)) ≠ 0
have h_alg : Algebra.IsAlgebraic K L
Tactic: have h_alg : Algebra.IsAlgebraic K L := Algebra.IsAlgebraic.of_finite K L
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Minpoly (hypothesis)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : FiniteDimensional K L
x : L
hx : IsUnit x
h_alg : Algebra.IsAlgebraic K L
⊢ HPow.hPow (α := Γ₀) ((v : (a : K) → Γ₀) (coeff (minpoly K x) 0) : Γ₀) (finrank K L / natDegree (minpoly K x)) ≠ 0
have hx₀ : IsIntegral K x
Tactic: have hx₀ : IsIntegral K x := (Algebra.IsAlgebraic.isAlgebraic x).isIntegral
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Minpoly (hypothesis)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : FiniteDimensional K L
x : L
hx : IsUnit x
h_alg : Algebra.IsAlgebraic K L
hx₀ : IsIntegral K x
⊢ HPow.hPow (α := Γ₀) ((v : (a : K) → Γ₀) (coeff (minpoly K x) 0) : Γ₀) (finrank K L / natDegree (minpoly K x)) ≠ 0
have hdeg : 0 < finrank K L / natDegree (minpoly K x)
Tactic: have hdeg := Nat.div_pos (natDegree_le x) (natDegree_pos hx₀)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Minpoly (goal)
Goal:
K : Type u_1
inst : Field K
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : FiniteDimensional K L
x : L
hx : IsUnit x
h_alg : Algebra.IsAlgebraic K L
hx₀ : IsIntegral K x
hdeg : 0 < finrank K L / natDegree (minpoly K x)
⊢ HPow.hPow (α := Γ₀) ((v : (a : K) → Γ₀) (coeff (minpoly K x) 0) : Γ₀) (finrank K L / natDegree (minpoly K x)) ≠ 0
have rw : ¬coeff (minpoly K x) 0 = 0
Tactic: rw [ne_eq, pow_eq_zero_iff hdeg.ne.symm, Valuation.zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Quotient (goal)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
J : Ideal R
v : Valuation.{u_1, u_2} (R ⧸ J) Γ₀
⊢ J ≤ (comap (Ideal.Quotient.mk J) v).supp
have rw : Ideal.map (F := R →+* R ⧸ J) (Ideal.Quotient.mk J) J ≤ v.supp
Tactic: rw [comap_supp, ← Ideal.map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Quotient (goal)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
⊢ (v.onQuot hJ).supp = Ideal.map (F := R →+* R ⧸ J) (Ideal.Quotient.mk J) v.supp
have a : (v.onQuot hJ).supp ≤ Ideal.map (F := R →+* R ⧸ J) (Ideal.Quotient.mk J) v.supp
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Quotient (goal)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
a : (v.onQuot hJ).supp ≤ Ideal.map (F := R →+* R ⧸ J) (Ideal.Quotient.mk J) v.supp
⊢ (v.onQuot hJ).supp = Ideal.map (F := R →+* R ⧸ J) (Ideal.Quotient.mk J) v.supp
have a₁ : Ideal.map (F := R →+* R ⧸ J) (Ideal.Quotient.mk J) v.supp ≤ (v.onQuot hJ).supp
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Quotient (goal)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
x_1 : R ⧸ J
x : R
hx : Quot.mk (⇑(Submodule.quotientRel J) : R → R → Prop) x ∈ (v.onQuot hJ).supp
⊢ Membership.mem (γ := Submodule (R ⧸ J) (R ⧸ J)) (Ideal.map (F := R →+* R ⧸ J) (Ideal.Quotient.mk J) v.supp)
    (Quot.mk (⇑(Submodule.quotientRel J) : R → R → Prop) x)
have a : Membership.mem (γ := Set (R ⧸ J)) ((⇑(Ideal.Quotient.mk J) : (a : R) → R ⧸ J) '' (↑v.supp : Set R))
  (Quot.mk (⇑(Submodule.quotientRel J) : R → R → Prop) x)
Tactic: apply Ideal.subset_span
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Quotient (goal)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
⊢ Ideal.map (F := R →+* R ⧸ J) (Ideal.Quotient.mk J) v.supp ≤ (v.onQuot hJ).supp
have a : v.supp ≤ Ideal.comap (F := R →+* R ⧸ J) (Ideal.Quotient.mk J) (v.onQuot hJ).supp
Tactic: rw [Ideal.map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Quotient (goal)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ (v.onQuot ⋯).supp = 0
have rw : Eq (α := Ideal (R ⧸ v.supp)) (Ideal.map (F := R →+* R ⧸ v.supp) (Ideal.Quotient.mk v.supp) v.supp) 0
Tactic: rw [supp_quot]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
⊢ Nonempty.{u_2 + 1} v.RankOne ↔ MulArchimedean.{u_2} (ValueGroup₀ v)
have mp : Nonempty.{u_2 + 1} v.RankOne → MulArchimedean.{u_2} (ValueGroup₀ v)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
mp : Nonempty.{u_2 + 1} v.RankOne → MulArchimedean.{u_2} (ValueGroup₀ v)
⊢ Nonempty.{u_2 + 1} v.RankOne ↔ MulArchimedean.{u_2} (ValueGroup₀ v)
have mpr : MulArchimedean.{u_2} (ValueGroup₀ v) → Nonempty.{u_2 + 1} v.RankOne
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
h : Nonempty.{u_2 + 1} v.RankOne
⊢ MulArchimedean.{u_2} (ValueGroup₀ v)
have mp : ∀ (hv : v.RankOne), MulArchimedean.{u_2} (ValueGroup₀ v)
Tactic: obtain hv := Nonempty.some h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
h : MulArchimedean.{u_2} (ValueGroup₀ v)
⊢ Nonempty.{u_2 + 1} v.RankOne
have mpr : ∀ (f : Additive (ValueGroup₀ v)ˣ →+o ℝ)
  (hf : Injective (α := Additive (ValueGroup₀ v)ˣ) (β := ℝ) (⇑f : (a : Additive (ValueGroup₀ v)ˣ) → ℝ)),
  Nonempty.{u_2 + 1} v.RankOne
Tactic: obtain ⟨f, hf⟩ :=
      Archimedean.exists_orderAddMonoidHom_real_injective (Additive (ValueGroup₀ v)ˣ)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
h : MulArchimedean.{u_2} (ValueGroup₀ v)
f : Additive (ValueGroup₀ v)ˣ →+o ℝ
hf : Injective (α := Additive (ValueGroup₀ v)ˣ) (β := ℝ) (⇑f : (a : Additive (ValueGroup₀ v)ˣ) → ℝ)
e : (ValueGroup₀ v)ˣ →* Multiplicative ℝ :=
  (AddMonoidHom.toMultiplicativeRight : (a : Additive (ValueGroup₀ v)ˣ →+ ℝ) → (ValueGroup₀ v)ˣ →* Multiplicative ℝ)
    (↑f : Additive (ValueGroup₀ v)ˣ →+ ℝ)
⊢ StrictMono (α := (ValueGroup₀ v)ˣ) (β := Multiplicative ℝ) (⇑e : (a : (ValueGroup₀ v)ˣ) → Multiplicative ℝ)
have simp : StrictMono (α := (ValueGroup₀ v)ˣ) (β := Multiplicative ℝ)
  (Function.comp (β := ℝ) (⇑ofAdd : (a : ℝ) → Multiplicative ℝ)
    (Function.comp (β := Additive (ValueGroup₀ v)ˣ) (⇑f : (a : Additive (ValueGroup₀ v)ˣ) → ℝ)
      (⇑Additive.ofMul : (a : (ValueGroup₀ v)ˣ) → Additive (ValueGroup₀ v)ˣ)))
Tactic: simp only [AddMonoidHom.coe_toMultiplicativeRight, AddMonoidHom.coe_coe, e]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (hypothesis)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
h : MulArchimedean.{u_2} (ValueGroup₀ v)
f : Additive (ValueGroup₀ v)ˣ →+o ℝ
hf : Injective (α := Additive (ValueGroup₀ v)ˣ) (β := ℝ) (⇑f : (a : Additive (ValueGroup₀ v)ˣ) → ℝ)
e : (ValueGroup₀ v)ˣ →* Multiplicative ℝ :=
  (AddMonoidHom.toMultiplicativeRight : (a : Additive (ValueGroup₀ v)ˣ →+ ℝ) → (ValueGroup₀ v)ˣ →* Multiplicative ℝ)
    (↑f : Additive (ValueGroup₀ v)ˣ →+ ℝ)
⊢ Nonempty.{u_2 + 1} v.RankOne
have he : StrictMono (α := (ValueGroup₀ v)ˣ) (β := Multiplicative ℝ) (⇑e : (a : (ValueGroup₀ v)ˣ) → Multiplicative ℝ)
Tactic: have he : StrictMono e := by
      simp only [AddMonoidHom.coe_toMultiplicativeRight, AddMonoidHom.coe_coe, e]
      -- toAdd_strictMono is already in an applied form, do defeq abuse instead
      exact StrictMono.comp strictMono_id (f.monotone'.strictMono_of_injective hf)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
h : MulArchimedean.{u_2} (ValueGroup₀ v)
f : Additive (ValueGroup₀ v)ˣ →+o ℝ
hf : Injective (α := Additive (ValueGroup₀ v)ˣ) (β := ℝ) (⇑f : (a : Additive (ValueGroup₀ v)ˣ) → ℝ)
e : (ValueGroup₀ v)ˣ →* Multiplicative ℝ :=
  (AddMonoidHom.toMultiplicativeRight : (a : Additive (ValueGroup₀ v)ˣ →+ ℝ) → (ValueGroup₀ v)ˣ →* Multiplicative ℝ)
    (↑f : Additive (ValueGroup₀ v)ˣ →+ ℝ)
he : StrictMono (α := (ValueGroup₀ v)ˣ) (β := Multiplicative ℝ) (⇑e : (a : (ValueGroup₀ v)ˣ) → Multiplicative ℝ)
x : Multiplicative ℝ
⊢ NNReal.mk (HPow.hPow (α := ℝ) 2 (↑x : WithZero (Multiplicative ℝ)).log) ⋯ ≠ 0
have rw : ¬(↑(NNReal.mk (HPow.hPow (α := ℝ) 2 (↑x : WithZero (Multiplicative ℝ)).log) sorry) : ℝ) = (↑0 : ℝ)
Tactic: rw [ne_eq, Subtype.ext_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
h : MulArchimedean.{u_2} (ValueGroup₀ v)
f : Additive (ValueGroup₀ v)ˣ →+o ℝ
hf : Injective (α := Additive (ValueGroup₀ v)ˣ) (β := ℝ) (⇑f : (a : Additive (ValueGroup₀ v)ˣ) → ℝ)
e : (ValueGroup₀ v)ˣ →* Multiplicative ℝ :=
  (AddMonoidHom.toMultiplicativeRight : (a : Additive (ValueGroup₀ v)ˣ →+ ℝ) → (ValueGroup₀ v)ˣ →* Multiplicative ℝ)
    (↑f : Additive (ValueGroup₀ v)ˣ →+ ℝ)
he : StrictMono (α := (ValueGroup₀ v)ˣ) (β := Multiplicative ℝ) (⇑e : (a : (ValueGroup₀ v)ˣ) → Multiplicative ℝ)
x x_1 : Multiplicative ℝ
⊢ Units.mk0 (NNReal.mk (HPow.hPow (α := ℝ) 2 (↑(x * x_1) : WithZero (Multiplicative ℝ)).log) ⋯) ⋯ =
    Units.mk0 (NNReal.mk (HPow.hPow (α := ℝ) 2 (↑x : WithZero (Multiplicative ℝ)).log) ⋯) ⋯ *
      Units.mk0 (NNReal.mk (HPow.hPow (α := ℝ) 2 (↑x_1 : WithZero (Multiplicative ℝ)).log) ⋯) ⋯
have rw : (↑(↑(Units.mk0 (NNReal.mk (HPow.hPow (α := ℝ) 2 (↑(x * x_1) : WithZero (Multiplicative ℝ)).log) sorry) sorry) : ℝ≥0) : ℝ) =
  (↑(↑(Units.mk0 (NNReal.mk (HPow.hPow (α := ℝ) 2 (↑x : WithZero (Multiplicative ℝ)).log) sorry) sorry *
            Units.mk0 (NNReal.mk (HPow.hPow (α := ℝ) 2 (↑x_1 : WithZero (Multiplicative ℝ)).log) sorry) sorry) :
        ℝ≥0) :
    ℝ)
Tactic: rw [Units.ext_iff, Subtype.ext_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
h : MulArchimedean.{u_2} (ValueGroup₀ v)
f : Additive (ValueGroup₀ v)ˣ →+o ℝ
hf : Injective (α := Additive (ValueGroup₀ v)ˣ) (β := ℝ) (⇑f : (a : Additive (ValueGroup₀ v)ˣ) → ℝ)
e : (ValueGroup₀ v)ˣ →* Multiplicative ℝ :=
  (AddMonoidHom.toMultiplicativeRight : (a : Additive (ValueGroup₀ v)ˣ →+ ℝ) → (ValueGroup₀ v)ˣ →* Multiplicative ℝ)
    (↑f : Additive (ValueGroup₀ v)ˣ →+ ℝ)
he : StrictMono (α := (ValueGroup₀ v)ˣ) (β := Multiplicative ℝ) (⇑e : (a : (ValueGroup₀ v)ˣ) → Multiplicative ℝ)
rf : Multiplicative ℝ →* ℝ≥0ˣ :=
  {
    toFun := fun (x : Multiplicative ℝ) ↦
      Units.mk0 (NNReal.mk (HPow.hPow (α := ℝ) 2 (↑x : WithZero (Multiplicative ℝ)).log) ⋯) ⋯,
    map_one' := ⋯, map_mul' := ⋯ }
⊢ StrictMono (α := WithZero (ValueGroup₀ v)ˣ) (β := WithZero ℝ≥0ˣ)
    (⇑(map' (rf.comp e)) : (a : WithZero (ValueGroup₀ v)ˣ) → WithZero ℝ≥0ˣ)
have refine : StrictMono (α := (ValueGroup₀ v)ˣ) (β := ℝ≥0ˣ) (⇑(rf.comp e) : (a : (ValueGroup₀ v)ˣ) → ℝ≥0ˣ)
Tactic: refine map'_strictMono ?_
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (hypothesis)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
inst_2 : v.IsNontrivial
h : MulArchimedean.{u_2} (ValueGroup₀ v)
f : Additive (ValueGroup₀ v)ˣ →+o ℝ
hf : Injective (α := Additive (ValueGroup₀ v)ˣ) (β := ℝ) (⇑f : (a : Additive (ValueGroup₀ v)ˣ) → ℝ)
e : (ValueGroup₀ v)ˣ →* Multiplicative ℝ :=
  (AddMonoidHom.toMultiplicativeRight : (a : Additive (ValueGroup₀ v)ˣ →+ ℝ) → (ValueGroup₀ v)ˣ →* Multiplicative ℝ)
    (↑f : Additive (ValueGroup₀ v)ˣ →+ ℝ)
he : StrictMono (α := (ValueGroup₀ v)ˣ) (β := Multiplicative ℝ) (⇑e : (a : (ValueGroup₀ v)ˣ) → Multiplicative ℝ)
rf : Multiplicative ℝ →* ℝ≥0ˣ :=
  {
    toFun := fun (x : Multiplicative ℝ) ↦
      Units.mk0 (NNReal.mk (HPow.hPow (α := ℝ) 2 (↑x : WithZero (Multiplicative ℝ)).log) ⋯) ⋯,
    map_one' := ⋯, map_mul' := ⋯ }
⊢ Nonempty.{u_2 + 1} v.RankOne
have H : StrictMono (α := WithZero (ValueGroup₀ v)ˣ) (β := WithZero ℝ≥0ˣ)
  (⇑(map' (rf.comp e)) : (a : WithZero (ValueGroup₀ v)ˣ) → WithZero ℝ≥0ˣ)
Tactic: have H : StrictMono (map' (rf.comp e)) := by
      refine map'_strictMono ?_
      intro a b h
      simpa [← Units.val_lt_val, ← NNReal.coe_lt_coe, rf] using he h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
x : ValueGroup₀ v
hx : Eq (α := ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
⊢ x = 0
have refine : ∀ (h_lt : 0 < x), False
Tactic: refine (eq_of_le_of_not_lt (zero_le' (a := x)) fun h_lt ↦ ?_).symm
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (hypothesis)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
x : ValueGroup₀ v
hx : Eq (α := ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
h_lt : 0 < x
⊢ False
have hs : LT.lt (α := ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) 0 : ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) x : ℝ≥0)
Tactic: have hs := strictMono v h_lt
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (hypothesis)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
x : ValueGroup₀ v
hx : Eq (α := ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
h_lt : 0 < x
hs : LT.lt (α := ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) 0 : ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) x : ℝ≥0)
⊢ False
have hs₁ : LT.lt (α := ℝ≥0) 0 0
Tactic: rw [map_zero, hx] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
x : ValueGroup₀ v
h : x = 0
⊢ Eq (α := ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
have rw : Eq (α := ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) 0 : ℝ≥0) (0 : ℝ≥0)
Tactic: rw [h, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
x : ValueGroup₀ v
h : x = 0
rw : Eq (α := ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) 0 : ℝ≥0) (0 : ℝ≥0)
⊢ Eq (α := ℝ≥0) ((hom v : (a : ValueGroup₀ v) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
have rw₁ : Eq (α := ℝ≥0) 0 0
Tactic: rw [h, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.RankOne (goal)
Goal:
R : Type u_1
Γ₀ : Type u_2
inst : Ring R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
hv : v.RankOne
⊢ unit v ≠ 1
have rw : ¬(↑(unit v) : Γ₀) = 1
Tactic: rw [Ne, ← Units.val_inj, Units.val_one]