awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TensorProduct.Free
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι : Type u_4
ι₂ : Type u_5
A : Type u_6
inst : Fintype ι
inst_1 : Finite ι₂
inst_2 : DecidableEq ι
inst_3 : CommSemiring R
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : AddCommMonoid M₁
inst_7 : Module R M₁
inst_8 : AddCommMonoid M₂
inst_9 : Module R M₂
f : M₁ →ₗ[R] M₂
b₁ : Basis ι R M₁
b₂ : Basis ι₂ R M₂
a :
  ∀ (i : ι₂) (j : ι),
    Eq.{u_6 + 1} (α := A)
      ((toMatrix (basis A b₁) (basis A b₂) : (a : A ⊗[R] M₁ →ₗ[A] A ⊗[R] M₂) → Matrix ι₂ ι A) (baseChange A f) i j : A)
      (Matrix.map.{u_1, u_6, u_5, u_4} (α := R) ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι R) f)
          (⇑(algebraMap R A) : (a : R) → A) i j :
        A)
⊢ Eq (α := Matrix ι₂ ι A)
    ((toMatrix (basis A b₁) (basis A b₂) : (a : A ⊗[R] M₁ →ₗ[A] A ⊗[R] M₂) → Matrix ι₂ ι A) (baseChange A f) :
      Matrix ι₂ ι A)
    (Matrix.map.{u_1, u_6, u_5, u_4} (α := R) ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι R) f)
        (⇑(algebraMap R A) : (a : R) → A) :
      Matrix ι₂ ι A)

Tactic:
ext
-- Module: Mathlib.RingTheory.TensorProduct.Free
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι : Type u_4
ι₂ : Type u_5
A : Type u_6
inst : Fintype ι
inst_1 : Finite ι₂
inst_2 : DecidableEq ι
inst_3 : CommSemiring R
inst_4 : CommSemiring A
inst_5 : Algebra R A
inst_6 : AddCommMonoid M₁
inst_7 : Module R M₁
inst_8 : AddCommMonoid M₂
inst_9 : Module R M₂
f : M₁ →ₗ[R] M₂
b₁ : Basis ι R M₁
b₂ : Basis ι₂ R M₂
i : ι₂
j : ι
⊢ Eq.{u_6 + 1} (α := A)
    ((toMatrix (basis A b₁) (basis A b₂) : (a : A ⊗[R] M₁ →ₗ[A] A ⊗[R] M₂) → Matrix ι₂ ι A) (baseChange A f) i j : A)
    (Matrix.map.{u_1, u_6, u_5, u_4} (α := R) ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι R) f)
        (⇑(algebraMap R A) : (a : R) → A) i j :
      A)

Tactic:
simp [toMatrix_apply]

Premises used: LinearMap.toMatrix_apply
-- Module: Mathlib.RingTheory.Valuation.ExtendToLocalization
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) : Γ) := ⋯
⊢ Eq.{u_2 + 1} (α := Γ) ((f.lift h : (a : B) → Γ) ((f : (a : A) → B) 0 : B) : Γ)
    (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) 0 : Γ)

Tactic:
f.lift_eq (P := Γ) _ 0

Premises used: Submonoid.LocalizationMap.lift_eq, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.ExtendToLocalization
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) : Γ) := ⋯
h₁ : Eq.{u_3 + 1} (α := B) (0 : B) ((f : (a : A) → B) 0 : B)
h₂ : Eq.{u_2 + 1} (α := Γ) (0 : Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) 0 : Γ)
⊢ (↑(f.lift h) : OneHom B Γ).toFun 0 = 0

Tactic:
convert! f.lift_eq (P := Γ) _ 0

Premises used: Submonoid.LocalizationMap.lift_eq, OfNat.ofNat
-- Module: Mathlib.RingTheory.Valuation.ExtendToLocalization
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) : Γ) := ⋯
⊢ Eq.{u_3 + 1} (α := B) (0 : B) ((f : (a : A) → B) 0 : B)

Tactic:
simp [f]
-- Module: Mathlib.RingTheory.Valuation.ExtendToLocalization
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) : Γ) := ⋯
⊢ Eq.{u_2 + 1} (α := Γ) (0 : Γ) (((↑v.toMonoidWithZeroHom : A →* Γ) : (a : A) → Γ) 0 : Γ)

Tactic:
simp [f]
-- Module: Mathlib.RingTheory.Valuation.ExtendToLocalization
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) : Γ) := ⋯
x y : B
obtain : ∀ (a : A) (s : ↥S), ∃ (a_1 : A) (b : A) (s_1 : ↥S), f.mk' a_1 s_1 = f.mk' a s ∧ f.mk' b s_1 = y
⊢ ∃ (a : A) (b : A) (s : ↥S), f.mk' a s = x ∧ f.mk' b s = y

Tactic:
obtain ⟨a, s, rfl⟩ := f.mk'_surjective x

Premises used: Submonoid.LocalizationMap.mk'_surjective, rfl
-- Module: Mathlib.RingTheory.Valuation.ExtendToLocalization
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) : Γ) := ⋯
y : B
a : A
s : ↥S
obtain : ∀ (b : A) (t : ↥S), ∃ (a_1 : A) (b_1 : A) (s_1 : ↥S), f.mk' a_1 s_1 = f.mk' a s ∧ f.mk' b_1 s_1 = f.mk' b t
⊢ ∃ (a_1 : A) (b : A) (s_1 : ↥S), f.mk' a_1 s_1 = f.mk' a s ∧ f.mk' b s_1 = y

Tactic:
obtain ⟨b, t, rfl⟩ := f.mk'_surjective y

Premises used: Submonoid.LocalizationMap.mk'_surjective, rfl
-- Module: Mathlib.RingTheory.Valuation.ExtendToLocalization
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 : A
s : ↥S
b : A
t : ↥S
h₁ : f.mk' (a * (↑t : A)) (s * t) = f.mk' a s ∧ f.mk' (b * (↑s : A)) (s * t) = f.mk' b t
⊢ ∃ (a_1 : A) (b_1 : A) (s_1 : ↥S), f.mk' a_1 s_1 = f.mk' a s ∧ f.mk' b_1 s_1 = f.mk' b t

Tactic:
use a * t, b * s, s * t
-- Module: Mathlib.RingTheory.Valuation.ExtendToLocalization
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 : A
s : ↥S
b : A
t : ↥S
h₁ : f.mk' (a * (↑t : A)) (s * t) = f.mk' a s
h₂ : f.mk' (b * (↑s : A)) (s * t) = f.mk' b t
⊢ f.mk' (a * (↑t : A)) (s * t) = f.mk' a s ∧ f.mk' (b * (↑s : A)) (s * t) = f.mk' b t

Tactic:
constructor
-- Module: Mathlib.RingTheory.Valuation.ExtendToLocalization
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 : A
s : ↥S
b : A
t : ↥S
h₁ :
  Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) ((↑s : A) * (a * (↑t : A))) : B)
    ((f : (a : A) → B) ((↑s : A) * (↑t : A) * a) : B)
⊢ f.mk' (a * (↑t : A)) (s * t) = f.mk' a s

Tactic:
rw [f.mk'_eq_iff_eq, Submonoid.coe_mul]

Premises used: Submonoid.LocalizationMap.mk'_eq_iff_eq, Submonoid.coe_mul
-- Module: Mathlib.RingTheory.Valuation.ExtendToLocalization
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 : A
s : ↥S
b : A
t : ↥S
⊢ Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) ((↑s : A) * (a * (↑t : A))) : B)
    ((f : (a : A) → B) ((↑s : A) * (↑t : A) * a) : B)

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Valuation.ExtendToLocalization
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 : A
s : ↥S
b : A
t : ↥S
h₁ :
  Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) ((↑t : A) * (b * (↑s : A))) : B)
    ((f : (a : A) → B) ((↑s : A) * (↑t : A) * b) : B)
⊢ f.mk' (b * (↑s : A)) (s * t) = f.mk' b t

Tactic:
rw [f.mk'_eq_iff_eq, Submonoid.coe_mul]

Premises used: Submonoid.LocalizationMap.mk'_eq_iff_eq, Submonoid.coe_mul
-- Module: Mathlib.RingTheory.Valuation.ExtendToLocalization
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 : A
s : ↥S
b : A
t : ↥S
⊢ Eq.{u_3 + 1} (α := B) ((f : (a : A) → B) ((↑t : A) * (b * (↑s : A))) : B)
    ((f : (a : A) → B) ((↑s : A) * (↑t : A) * b) : B)

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Valuation.ExtendToLocalization
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) : Γ) := ⋯
x y : B
obtain :
  ∀ (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))
⊢ (↑(f.lift h) : OneHom B Γ).toFun (x + y) ≤
    max ((↑(f.lift h) : OneHom B Γ).toFun x) ((↑(f.lift h) : OneHom B Γ).toFun y)

Tactic:
obtain ⟨a, b, s, rfl, rfl⟩ : ∃ (a b : A) (s : S), f.mk' a s = x ∧ f.mk' b s = y := by
        obtain ⟨a, s, rfl⟩ := f.mk'_surjective x
        obtain ⟨b, t, rfl⟩ := f.mk'_surjective y
        use a * t, b * s, s * t
        constructor <;>
          · rw [f.mk'_eq_iff_eq, Submonoid.coe_mul]
            ring_nf

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.ExtendToLocalization
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)
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)) : Γ)
⊢ (↑(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))

Tactic:
convert_to f.lift h (f.mk' (a + b) s) ≤ max (f.lift h _) (f.lift h _)

Premises used: Submonoid.LocalizationMap.lift, Submonoid.LocalizationMap.mk', HAdd.hAdd, Max.max, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.ExtendToLocalization
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)

Tactic:
congr_arg (f.lift h) (IsLocalization.eq_mk'_iff_mul_eq.2 ?_)

Premises used: Iff.mpr, Submonoid.LocalizationMap.lift, congr_arg, IsLocalization.eq_mk'_iff_mul_eq, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.ExtendToLocalization
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 + f.mk' b s) ((algebraMap A B : (a : A) → B) (↑s : A) : B) =
    (algebraMap A B : (a : A) → B) (a + b)
⊢ (↑(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:
refine congr_arg (f.lift h) (IsLocalization.eq_mk'_iff_mul_eq.2 ?_)

Premises used: Iff.mpr, Submonoid.LocalizationMap.lift, congr_arg, IsLocalization.eq_mk'_iff_mul_eq, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.ExtendToLocalization
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) ((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)
⊢ 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:
rw [add_mul, map_add]

Premises used: add_mul, map_add
-- Module: Mathlib.RingTheory.Valuation.ExtendToLocalization
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)
h₅ 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)
⊢ 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 [← IsLocalization.toLocalizationMap_apply S B, f.mk'_spec, f.mk'_spec,
          IsLocalization.toLocalizationMap_apply,
          IsLocalization.toLocalizationMap_apply]

Premises used: IsLocalization.toLocalizationMap_apply, Submonoid.LocalizationMap.mk'_spec
-- Module: Mathlib.RingTheory.Valuation.ExtendToLocalization
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.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))
⊢ 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:
rw [f.lift_mk']

Premises used: Submonoid.LocalizationMap.lift_mk'
-- Module: Mathlib.RingTheory.Valuation.ExtendToLocalization
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.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))
⊢ 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']

Premises used: Submonoid.LocalizationMap.lift_mk'
-- Module: Mathlib.RingTheory.Valuation.ExtendToLocalization
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.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)⁻¹ : Γ) : Γ))
⊢ 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']

Premises used: Submonoid.LocalizationMap.lift_mk'
-- Module: Mathlib.RingTheory.Valuation.ExtendToLocalization
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.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)⁻¹ : Γ) : Γ))
⊢ 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:
iterate 3 rw [f.lift_mk']

Premises used: Submonoid.LocalizationMap.lift_mk'