awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ExtendToLocalization (goal)
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
f : Submonoid.LocalizationMap.{u_1, u_3} (M := A) S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit.{u_2} (M := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (↑s : A) : Γ) := ⋯
a b : A
s : ↥S
⊢ (↑(f.lift h) : OneHom B Γ).toFun (f.mk' a s + f.mk' b s) ≤
    max ((↑(f.lift h) : OneHom B Γ).toFun (f.mk' a s)) ((↑(f.lift h) : OneHom B Γ).toFun (f.mk' b s))
have h₁ : (↑(f.lift h) : OneHom B Γ).toFun (f.mk' a s + f.mk' b s) = (f.lift h : (a : B) → Γ) (f.mk' (a + b) s)
Tactic: convert_to f.lift h (f.mk' (a + b) s) ≤ max (f.lift h _) (f.lift h _)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ExtendToLocalization (goal)
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
f : Submonoid.LocalizationMap.{u_1, u_3} (M := A) S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit.{u_2} (M := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (↑s : A) : Γ) := ⋯
a b : A
s : ↥S
h₁ : (↑(f.lift h) : OneHom B Γ).toFun (f.mk' a s + f.mk' b s) = (f.lift h : (a : B) → Γ) (f.mk' (a + b) s)
⊢ (↑(f.lift h) : OneHom B Γ).toFun (f.mk' a s + f.mk' b s) ≤
    max ((↑(f.lift h) : OneHom B Γ).toFun (f.mk' a s)) ((↑(f.lift h) : OneHom B Γ).toFun (f.mk' b s))
have convert_3 : LE.le.{u_2} (α := Γ) ((f.lift h : (a : B) → Γ) (f.mk' (a + b) s) : Γ)
  (max ((f.lift h : (a : B) → Γ) (f.mk' a s)) ((f.lift h : (a : B) → Γ) (f.mk' b s)) : Γ)
Tactic: convert_to f.lift h (f.mk' (a + b) s) ≤ max (f.lift h _) (f.lift h _)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ExtendToLocalization (goal)
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
f : Submonoid.LocalizationMap.{u_1, u_3} (M := A) S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit.{u_2} (M := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (↑s : A) : Γ) := ⋯
a b : A
s : ↥S
⊢ (↑(f.lift h) : OneHom B Γ).toFun (f.mk' a s + f.mk' b s) = (f.lift h : (a : B) → Γ) (f.mk' (a + b) s)
have h₁ : HMul.hMul (β := B) (f.mk' a s + f.mk' b s) ((algebraMap A B : (a : A) → B) (↑s : A) : B) =
  (algebraMap A B : (a : A) → B) (a + b)
Tactic: refine congr_arg (f.lift h) (IsLocalization.eq_mk'_iff_mul_eq.2 ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ExtendToLocalization (goal)
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
f : Submonoid.LocalizationMap.{u_1, u_3} (M := A) S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit.{u_2} (M := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (↑s : A) : Γ) := ⋯
a b : A
s : ↥S
⊢ HMul.hMul (β := B) (f.mk' a s + f.mk' b s) ((algebraMap A B : (a : A) → B) (↑s : A) : B) =
    (algebraMap A B : (a : A) → B) (a + b)
have h₁ : HMul.hMul (β := B) (f.mk' a s) ((algebraMap A B : (a : A) → B) (↑s : A) : B) +
    HMul.hMul (β := B) (f.mk' b s) ((algebraMap A B : (a : A) → B) (↑s : A) : B) =
  HAdd.hAdd (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B)
Tactic: rw [add_mul, map_add]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ExtendToLocalization (goal)
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
f : Submonoid.LocalizationMap.{u_1, u_3} (M := A) S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit.{u_2} (M := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (↑s : A) : Γ) := ⋯
a b : A
s : ↥S
⊢ HMul.hMul (β := B) (f.mk' a s) ((algebraMap A B : (a : A) → B) (↑s : A) : B) +
      HMul.hMul (β := B) (f.mk' b s) ((algebraMap A B : (a : A) → B) (↑s : A) : B) =
    HAdd.hAdd (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B)
have h₁ : HMul.hMul (β := B) (f.mk' a s) ((IsLocalization.toLocalizationMap S B : (a : A) → B) (↑s : A) : B) +
    HMul.hMul (β := B) (f.mk' b s) ((IsLocalization.toLocalizationMap S B : (a : A) → B) (↑s : A) : B) =
  HAdd.hAdd (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B)
Tactic: rw [← IsLocalization.toLocalizationMap_apply S B, f.mk'_spec, f.mk'_spec,
          IsLocalization.toLocalizationMap_apply,
          IsLocalization.toLocalizationMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ExtendToLocalization (goal)
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
f : Submonoid.LocalizationMap.{u_1, u_3} (M := A) S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit.{u_2} (M := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (↑s : A) : Γ) := ⋯
a b : A
s : ↥S
h₁ :
  HMul.hMul (β := B) (f.mk' a s) ((IsLocalization.toLocalizationMap S B : (a : A) → B) (↑s : A) : B) +
      HMul.hMul (β := B) (f.mk' b s) ((IsLocalization.toLocalizationMap S B : (a : A) → B) (↑s : A) : B) =
    HAdd.hAdd (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B)
⊢ HMul.hMul (β := B) (f.mk' a s) ((algebraMap A B : (a : A) → B) (↑s : A) : B) +
      HMul.hMul (β := B) (f.mk' b s) ((algebraMap A B : (a : A) → B) (↑s : A) : B) =
    HAdd.hAdd (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B)
have h₂ : HAdd.hAdd (α := B) ((f : (a : A) → B) a : B)
    (HMul.hMul (β := B) (f.mk' b s) ((IsLocalization.toLocalizationMap S B : (a : A) → B) (↑s : A) : B)) =
  HAdd.hAdd (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B)
Tactic: rw [← IsLocalization.toLocalizationMap_apply S B, f.mk'_spec, f.mk'_spec,
          IsLocalization.toLocalizationMap_apply,
          IsLocalization.toLocalizationMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ExtendToLocalization (goal)
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
f : Submonoid.LocalizationMap.{u_1, u_3} (M := A) S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit.{u_2} (M := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (↑s : A) : Γ) := ⋯
a b : A
s : ↥S
h₁ :
  HMul.hMul (β := B) (f.mk' a s) ((IsLocalization.toLocalizationMap S B : (a : A) → B) (↑s : A) : B) +
      HMul.hMul (β := B) (f.mk' b s) ((IsLocalization.toLocalizationMap S B : (a : A) → B) (↑s : A) : B) =
    HAdd.hAdd (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B)
h₂ :
  HAdd.hAdd (α := B) ((f : (a : A) → B) a : B)
      (HMul.hMul (β := B) (f.mk' b s) ((IsLocalization.toLocalizationMap S B : (a : A) → B) (↑s : A) : B)) =
    HAdd.hAdd (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B)
⊢ HMul.hMul (β := B) (f.mk' a s) ((algebraMap A B : (a : A) → B) (↑s : A) : B) +
      HMul.hMul (β := B) (f.mk' b s) ((algebraMap A B : (a : A) → B) (↑s : A) : B) =
    HAdd.hAdd (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B)
have h₃ : HAdd.hAdd (α := B) (β := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B) =
  HAdd.hAdd (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B)
Tactic: rw [← IsLocalization.toLocalizationMap_apply S B, f.mk'_spec, f.mk'_spec,
          IsLocalization.toLocalizationMap_apply,
          IsLocalization.toLocalizationMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ExtendToLocalization (goal)
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
f : Submonoid.LocalizationMap.{u_1, u_3} (M := A) S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit.{u_2} (M := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (↑s : A) : Γ) := ⋯
a b : A
s : ↥S
h₁ :
  HMul.hMul (β := B) (f.mk' a s) ((IsLocalization.toLocalizationMap S B : (a : A) → B) (↑s : A) : B) +
      HMul.hMul (β := B) (f.mk' b s) ((IsLocalization.toLocalizationMap S B : (a : A) → B) (↑s : A) : B) =
    HAdd.hAdd (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B)
h₂ :
  HAdd.hAdd (α := B) ((f : (a : A) → B) a : B)
      (HMul.hMul (β := B) (f.mk' b s) ((IsLocalization.toLocalizationMap S B : (a : A) → B) (↑s : A) : B)) =
    HAdd.hAdd (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B)
h₃ :
  HAdd.hAdd (α := B) (β := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B) =
    HAdd.hAdd (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B)
⊢ HMul.hMul (β := B) (f.mk' a s) ((algebraMap A B : (a : A) → B) (↑s : A) : B) +
      HMul.hMul (β := B) (f.mk' b s) ((algebraMap A B : (a : A) → B) (↑s : A) : B) =
    HAdd.hAdd (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B)
have h₄ : HAdd.hAdd (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((f : (a : A) → B) b : B) =
  HAdd.hAdd (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B)
Tactic: rw [← IsLocalization.toLocalizationMap_apply S B, f.mk'_spec, f.mk'_spec,
          IsLocalization.toLocalizationMap_apply,
          IsLocalization.toLocalizationMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ExtendToLocalization (goal)
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
f : Submonoid.LocalizationMap.{u_1, u_3} (M := A) S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit.{u_2} (M := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (↑s : A) : Γ) := ⋯
a b : A
s : ↥S
h₁ :
  HMul.hMul (β := B) (f.mk' a s) ((IsLocalization.toLocalizationMap S B : (a : A) → B) (↑s : A) : B) +
      HMul.hMul (β := B) (f.mk' b s) ((IsLocalization.toLocalizationMap S B : (a : A) → B) (↑s : A) : B) =
    HAdd.hAdd (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B)
h₂ :
  HAdd.hAdd (α := B) ((f : (a : A) → B) a : B)
      (HMul.hMul (β := B) (f.mk' b s) ((IsLocalization.toLocalizationMap S B : (a : A) → B) (↑s : A) : B)) =
    HAdd.hAdd (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B)
h₃ :
  HAdd.hAdd (α := B) (β := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B) =
    HAdd.hAdd (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B)
h₄ :
  HAdd.hAdd (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((f : (a : A) → B) b : B) =
    HAdd.hAdd (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B)
⊢ HMul.hMul (β := B) (f.mk' a s) ((algebraMap A B : (a : A) → B) (↑s : A) : B) +
      HMul.hMul (β := B) (f.mk' b s) ((algebraMap A B : (a : A) → B) (↑s : A) : B) =
    HAdd.hAdd (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B)
have h₅ : HAdd.hAdd (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B) =
  HAdd.hAdd (α := B) (β := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B)
Tactic: rw [← IsLocalization.toLocalizationMap_apply S B, f.mk'_spec, f.mk'_spec,
          IsLocalization.toLocalizationMap_apply,
          IsLocalization.toLocalizationMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ExtendToLocalization (goal)
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
f : Submonoid.LocalizationMap.{u_1, u_3} (M := A) S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit.{u_2} (M := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (↑s : A) : Γ) := ⋯
a b : A
s : ↥S
⊢ LE.le.{u_2} (α := Γ) ((f.lift h : (a : B) → Γ) (f.mk' (a + b) s) : Γ)
    (max ((f.lift h : (a : B) → Γ) (f.mk' a s)) ((f.lift h : (a : B) → Γ) (f.mk' b s)) : Γ)
have convert_3 : HMul.hMul (α := Γ) (β := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (a + b) : Γ)
    ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ) ≤
  max ((f.lift h : (a : B) → Γ) (f.mk' a s)) ((f.lift h : (a : B) → Γ) (f.mk' b s))
Tactic: rw [f.lift_mk']
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ExtendToLocalization (goal)
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
f : Submonoid.LocalizationMap.{u_1, u_3} (M := A) S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit.{u_2} (M := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (↑s : A) : Γ) := ⋯
a b : A
s : ↥S
⊢ HMul.hMul (α := Γ) (β := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (a + b) : Γ)
      ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ) ≤
    max ((f.lift h : (a : B) → Γ) (f.mk' a s)) ((f.lift h : (a : B) → Γ) (f.mk' b s))
have convert_3 : HMul.hMul (α := Γ) (β := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (a + b) : Γ)
    ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ) ≤
  max
    (HMul.hMul (α := Γ) (β := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) a : Γ)
      ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ))
    ((f.lift h : (a : B) → Γ) (f.mk' b s))
Tactic: rw [f.lift_mk']
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ExtendToLocalization (goal)
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
f : Submonoid.LocalizationMap.{u_1, u_3} (M := A) S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit.{u_2} (M := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (↑s : A) : Γ) := ⋯
a b : A
s : ↥S
⊢ HMul.hMul (α := Γ) (β := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (a + b) : Γ)
      ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ) ≤
    max
      (HMul.hMul (α := Γ) (β := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) a : Γ)
        ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ))
      ((f.lift h : (a : B) → Γ) (f.mk' b s))
have convert_3 : HMul.hMul (α := Γ) (β := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (a + b) : Γ)
    ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ) ≤
  max
    (HMul.hMul (α := Γ) (β := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) a : Γ)
      ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ))
    (HMul.hMul (α := Γ) (β := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) b : Γ)
      ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ))
Tactic: rw [f.lift_mk']
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ExtendToLocalization (goal)
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
f : Submonoid.LocalizationMap.{u_1, u_3} (M := A) S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit.{u_2} (M := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (↑s : A) : Γ) := ⋯
a b : A
s : ↥S
⊢ LE.le.{u_2} (α := Γ) ((f.lift h : (a : B) → Γ) (f.mk' (a + b) s) : Γ)
    (max ((f.lift h : (a : B) → Γ) (f.mk' a s)) ((f.lift h : (a : B) → Γ) (f.mk' b s)) : Γ)
have convert_3 : HMul.hMul (α := Γ) (β := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (a + b) : Γ)
    ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ) ≤
  max
    (HMul.hMul (α := Γ) (β := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) a : Γ)
      ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ))
    (HMul.hMul (α := Γ) (β := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) b : Γ)
      ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ))
Tactic: iterate 3 rw [f.lift_mk']
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ExtendToLocalization (goal)
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
f : Submonoid.LocalizationMap.{u_1, u_3} (M := A) S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit.{u_2} (M := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (↑s : A) : Γ) := ⋯
a b : A
s : ↥S
⊢ HMul.hMul (α := Γ) (β := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (a + b) : Γ)
      ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ) ≤
    max
      (HMul.hMul (α := Γ) (β := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) a : Γ)
        ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ))
      (HMul.hMul (α := Γ) (β := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) b : Γ)
        ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ))
have convert_3 : HMul.hMul (α := Γ) (β := Γ) ((v : (a : A) → Γ) (a + b) : Γ)
    ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ) ≤
  max
    (HMul.hMul (α := Γ) (β := Γ) ((v : (a : A) → Γ) a : Γ)
      ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ))
    (HMul.hMul (α := Γ) (β := Γ) ((v : (a : A) → Γ) b : Γ)
      ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ExtendToLocalization (goal)
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
f : Submonoid.LocalizationMap.{u_1, u_3} (M := A) S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit.{u_2} (M := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (↑s : A) : Γ) := ⋯
a b : A
s : ↥S
⊢ HMul.hMul (α := Γ) (β := Γ) ((v : (a : A) → Γ) (a + b) : Γ)
      ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ) ≤
    max
      (HMul.hMul (α := Γ) (β := Γ) ((v : (a : A) → Γ) a : Γ)
        ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ))
      (HMul.hMul (α := Γ) (β := Γ) ((v : (a : A) → Γ) b : Γ)
        ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ))
have convert_3 : HMul.hMul (α := Γ) (β := Γ) ((v : (a : A) → Γ) (a + b) : Γ)
    ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ) ≤
  HMul.hMul (α := Γ) (β := Γ) (max ((v : (a : A) → Γ) a) ((v : (a : A) → Γ) b) : Γ)
    ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ)
Tactic: grw [max_mul_mul_right, v.map_add a b]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ExtendToLocalization (goal)
Goal:
A : Type u_1
inst : CommRing A
Γ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsLocalization S B
f : Submonoid.LocalizationMap.{u_1, u_3} (M := A) S B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit.{u_2} (M := Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) (↑s : A) : Γ) := ⋯
a b : A
s : ↥S
convert_3 :
  HMul.hMul (α := Γ) (β := Γ) ((v : (a : A) → Γ) (a + b) : Γ)
      ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ) ≤
    HMul.hMul (α := Γ) (β := Γ) (max ((v : (a : A) → Γ) a) ((v : (a : A) → Γ) b) : Γ)
      ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ)
⊢ HMul.hMul (α := Γ) (β := Γ) ((v : (a : A) → Γ) (a + b) : Γ)
      ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ) ≤
    max
      (HMul.hMul (α := Γ) (β := Γ) ((v : (a : A) → Γ) a : Γ)
        ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ))
      (HMul.hMul (α := Γ) (β := Γ) ((v : (a : A) → Γ) b : Γ)
        ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ))
have convert_3₁ : HMul.hMul (α := Γ) (β := Γ) (max ((v : (a : A) → Γ) a) ((v : (a : A) → Γ) b) : Γ)
    ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ) ≤
  HMul.hMul (α := Γ) (β := Γ) (max ((v : (a : A) → Γ) a) ((v : (a : A) → Γ) b) : Γ)
    ((↑((IsUnit.liftRight ((↑v.toMonoidWithZeroHom : A →* Γ).restrict S) h : (a : ↥S) → Γˣ) s)⁻¹ : Γ) : Γ)
Tactic: grw [max_mul_mul_right, v.map_add a b]
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.CancelIso (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x y : C
f : x ⟶ y
inst_1 : IsIso f
g : y ⟶ x
h : inv f = g
⊢ f ≫ g = 𝟙 x
have rw : f ≫ inv f = 𝟙 x
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.CancelIso (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
x y : C
f : x ⟶ y
inst_1 : IsIso f
g : y ⟶ x
h : inv f = g
z : C
k : x ⟶ z
⊢ f ≫ g ≫ k = k
have rw : f ≫ inv f ≫ k = k
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Tactic.Positivity.Basic (goal)
Goal:
α : Type u_1
inst : Zero α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LT α
ha : 0 < a
hb : 0 < b
⊢ 0 < if p then a else b
have pos : p → 0 < if p then a else b
Tactic: by_cases p
-- Lean 4 proof step from Mathlib.Tactic.Positivity.Basic (goal)
Goal:
α : Type u_1
inst : Zero α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LT α
ha : 0 < a
hb : 0 < b
pos : p → 0 < if p then a else b
⊢ 0 < if p then a else b
have neg : ¬p → 0 < if p then a else b
Tactic: by_cases p
-- Lean 4 proof step from Mathlib.Tactic.Positivity.Basic (goal)
Goal:
α : Type u_1
inst : Zero α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LE α
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ if p then a else b
have pos : p → 0 ≤ if p then a else b
Tactic: by_cases p