awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hPQ : ∀ {R S : Type u} [inst : CommRing R] [inst_2 : CommRing S] {f : R →+* S}, P f → Q f
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
exact ⟨s, hsone, fun t ht ↦ hPQ (hs t ht)⟩
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPs : OfLocalizationSpanTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f ↔ P f

Tactic:
⟨fun ⟨s, hsone, hs⟩ ↦ hPs f s hsone (fun a ↦ hs a.val a.property), locally_of hPi f⟩

Premises used: Iff.intro, _private.0.RingHom.locally_iff_span_eq_top.match_1, RingHom.locally_of, Subtype.val, Subtype.property
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
_ :
  ∀ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Set S),
    Eq (α := Ideal S) (Ideal.span s) ⊤ →
      (∀ (r : (↑s : Type u)),
          (@fun {R S : Type u} [CommRing R] [CommRing S] ↦
              (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
            _ (Localization.Away (↑r : S)) _ _ (comp (algebraMap S (Localization.Away (↑r : S))) f)) →
        (fun {R S : Type u} [CommRing R] [CommRing S] ↦
            (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
          f
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Set S),
    Eq (α := Ideal S) (Ideal.span s) ⊤ →
      (∀ (r : (↑s : Type u)),
          (@fun {R S : Type u} [CommRing R] [CommRing S] ↦
              (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
            _ (Localization.Away (↑r : S)) _ _ (comp (algebraMap S (Localization.Away (↑r : S))) f)) →
        (fun {R S : Type u} [CommRing R] [CommRing S] ↦
            (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
          f

Tactic:
_
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
_ :
  ∀ [inst_1 : CommRing S] (f : R →+* S) (s : Set S),
    Eq (α := Ideal S) (Ideal.span s) ⊤ →
      (∀ (r : (↑s : Type u)),
          (@fun {R S : Type u} [CommRing R] [CommRing S] ↦
              (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
            _ (Localization.Away (↑r : S)) _ _ (comp (algebraMap S (Localization.Away (↑r : S))) f)) →
        (fun {R S : Type u} [CommRing R] [CommRing S] ↦
            (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
          f
⊢ ∀ [inst_1 : CommRing S] (f : R →+* S) (s : Set S),
    Eq (α := Ideal S) (Ideal.span s) ⊤ →
      (∀ (r : (↑s : Type u)),
          (@fun {R S : Type u} [CommRing R] [CommRing S] ↦
              (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
            _ (Localization.Away (↑r : S)) _ _ (comp (algebraMap S (Localization.Away (↑r : S))) f)) →
        (fun {R S : Type u} [CommRing R] [CommRing S] ↦
            (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
          f

Tactic:
_
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ (r : (↑s : Type u)),
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦
        (Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P : (f : R →+* S) → Prop))
      _ (Localization.Away (↑r : S)) _ _ (comp (algebraMap S (Localization.Away (↑r : S))) f)
choose :
  ∀ (t : (r : (↑s : Type u)) → Set (Localization.Away (↑r : S)))
    (htone : ∀ (r : (↑s : Type u)), Eq (α := Ideal (Localization.Away (↑r : S))) (Ideal.span (t r)) ⊤)
    (ht :
      ∀ (r : (↑s : Type u)),
        ∀ t_1 ∈ t r,
          (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t_1) _ _
            (@comp _ (Localization.Away (↑r : S)) _ _ Semiring.toNonAssocSemiring _
              (algebraMap (Localization.Away (↑r : S)) (Localization.Away t_1))
              (comp (algebraMap S (Localization.Away (↑r : S))) f))),
    Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f

Tactic:
choose t htone ht using hs
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
t : (r : (↑s : Type u)) → Set (Localization.Away (↑r : S))
htone : ∀ (r : (↑s : Type u)), Eq (α := Ideal (Localization.Away (↑r : S))) (Ideal.span (t r)) ⊤
ht :
  ∀ (r : (↑s : Type u)),
    ∀ t_1 ∈ t r,
      (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t_1) _ _
        (@comp _ (Localization.Away (↑r : S)) _ _ Semiring.toNonAssocSemiring _
          (algebraMap (Localization.Away (↑r : S)) (Localization.Away t_1))
          (comp (algebraMap S (Localization.Away (↑r : S))) f))
rw :
  ∃ (ι : Type u) (s : ι → S) (_ : Eq (α := Ideal S) (Ideal.span (Set.range s)) ⊤) (Sₜ : ι → Type u) (x :
    (i : ι) → CommRing (Sₜ i)) (x_1 : (i : ι) → Algebra S (Sₜ i)) (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
    ∀ (i : ι), P (S := Sₜ i) (comp (algebraMap S (Sₜ i)) f)
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f

Tactic:
rw [locally_iff_exists hP]

Premises used: RingHom.locally_iff_exists
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
t : (r : (↑s : Type u)) → Set (Localization.Away (↑r : S))
htone : ∀ (r : (↑s : Type u)), Eq (α := Ideal (Localization.Away (↑r : S))) (Ideal.span (t r)) ⊤
ht :
  ∀ (r : (↑s : Type u)),
    ∀ t_1 ∈ t r,
      (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t_1) _ _
        (@comp _ (Localization.Away (↑r : S)) _ _ Semiring.toNonAssocSemiring _
          (algebraMap (Localization.Away (↑r : S)) (Localization.Away t_1))
          (comp (algebraMap S (Localization.Away (↑r : S))) f))
⊢ ∃ (ι : Type u) (s : ι → S) (_ : Eq (α := Ideal S) (Ideal.span (Set.range s)) ⊤) (Sₜ : ι → Type u) (x :
    (i : ι) → CommRing (Sₜ i)) (x_1 : (i : ι) → Algebra S (Sₜ i)) (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
    ∀ (i : ι), P (S := Sₜ i) (comp (algebraMap S (Sₜ i)) f)

Tactic:
⟨(a : s) × t a, IsLocalization.Away.mulNumerator s t,
      IsLocalization.Away.span_range_mulNumerator_eq_top hsone htone,
      fun ⟨a, b⟩ ↦ Localization.Away b.val, inferInstance, inferInstance, fun ⟨a, b⟩ ↦ ?_, ?_⟩

Premises used: IsLocalization.Away.mulNumerator, _private.0.RingHom.locally_ofLocalizationSpanTarget.match_1, IsLocalization.Away, Localization.Away, inferInstance, Set.Elem, IsLocalization.Away.span_range_mulNumerator_eq_top, _private.0.RingHom.locally_ofLocalizationSpanTarget.match_2, Exists.intro, Subtype.val, Sigma
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
t : (r : (↑s : Type u)) → Set (Localization.Away (↑r : S))
htone : ∀ (r : (↑s : Type u)), Eq (α := Ideal (Localization.Away (↑r : S))) (Ideal.span (t r)) ⊤
ht :
  ∀ (r : (↑s : Type u)),
    ∀ t_1 ∈ t r,
      (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t_1) _ _
        (@comp _ (Localization.Away (↑r : S)) _ _ Semiring.toNonAssocSemiring _
          (algebraMap (Localization.Away (↑r : S)) (Localization.Away t_1))
          (comp (algebraMap S (Localization.Away (↑r : S))) f))
refine_1 :
  ∀ (x : (a : (↑s : Type u)) × (↑(t a) : Type u)) (a : (↑s : Type u)) (b : (↑(t a) : Type u)),
    IsLocalization.Away
      (IsLocalization.Away.mulNumerator s (Rₜ := fun (t : (↑s : Type u)) ↦ Localization.Away (↑t : S)) t
        (Sigma.mk (β := fun (a : (↑s : Type u)) ↦ (↑(t a) : Type u)) a b))
      ((fun (x : (a : (↑s : Type u)) × (↑(t a) : Type u)) ↦
          (match (motive := (a : (↑s : Type u)) × (↑(t a) : Type u) → Type u) x with
            | ⟨a, b⟩ => Localization.Away (↑b : Localization.Away (↑a : S)) :
            Type u))
        (Sigma.mk (β := fun (a : (↑s : Type u)) ↦ (↑(t a) : Type u)) a b))
refine_2 :
  ∀ (i : (a : (↑s : Type u)) × (↑(t a) : Type u)),
    P (S :=
      (fun (x : (a : (↑s : Type u)) × (↑(t a) : Type u)) ↦
          (match (motive := (a : (↑s : Type u)) × (↑(t a) : Type u) → Type u) x with
            | ⟨a, b⟩ => Localization.Away (↑b : Localization.Away (↑a : S)) :
            Type u))
        i)
      (comp
        (algebraMap S
          ((fun (x : (a : (↑s : Type u)) × (↑(t a) : Type u)) ↦
              (match (motive := (a : (↑s : Type u)) × (↑(t a) : Type u) → Type u) x with
                | ⟨a, b⟩ => Localization.Away (↑b : Localization.Away (↑a : S)) :
                Type u))
            i))
        f)
⊢ ∃ (ι : Type u) (s : ι → S) (_ : Eq (α := Ideal S) (Ideal.span (Set.range s)) ⊤) (Sₜ : ι → Type u) (x :
    (i : ι) → CommRing (Sₜ i)) (x_1 : (i : ι) → Algebra S (Sₜ i)) (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
    ∀ (i : ι), P (S := Sₜ i) (comp (algebraMap S (Sₜ i)) f)

Tactic:
refine ⟨(a : s) × t a, IsLocalization.Away.mulNumerator s t,
      IsLocalization.Away.span_range_mulNumerator_eq_top hsone htone,
      fun ⟨a, b⟩ ↦ Localization.Away b.val, inferInstance, inferInstance, fun ⟨a, b⟩ ↦ ?_, ?_⟩
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
t : (r : (↑s : Type u)) → Set (Localization.Away (↑r : S))
htone : ∀ (r : (↑s : Type u)), Eq (α := Ideal (Localization.Away (↑r : S))) (Ideal.span (t r)) ⊤
ht :
  ∀ (r : (↑s : Type u)),
    ∀ t_1 ∈ t r,
      (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t_1) _ _
        (@comp _ (Localization.Away (↑r : S)) _ _ Semiring.toNonAssocSemiring _
          (algebraMap (Localization.Away (↑r : S)) (Localization.Away t_1))
          (comp (algebraMap S (Localization.Away (↑r : S))) f))
x : (a : (↑s : Type u)) × (↑(t a) : Type u)
a : (↑s : Type u)
b : (↑(t a) : Type u)
h :
  Associated (↑b : Localization.Away (↑a : S))
    ((algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S))
      (IsLocalization.Away.sec (↑a : S) (↑b : Localization.Away (↑a : S))).1)
⊢ IsLocalization.Away (R := Localization.Away (↑a : S))
    ((algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S))
        (IsLocalization.Away.sec (↑a : S) (↑b : Localization.Away (↑a : S))).1 :
      Localization.Away (↑a : S))
    (Localization.Away (↑b : Localization.Away (↑a : S)))

Tactic:
apply IsLocalization.Away.of_associated (r := b.val)

Premises used: IsLocalization.Away.of_associated
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
t : (r : (↑s : Type u)) → Set (Localization.Away (↑r : S))
htone : ∀ (r : (↑s : Type u)), Eq (α := Ideal (Localization.Away (↑r : S))) (Ideal.span (t r)) ⊤
ht :
  ∀ (r : (↑s : Type u)),
    ∀ t_1 ∈ t r,
      (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t_1) _ _
        (@comp _ (Localization.Away (↑r : S)) _ _ Semiring.toNonAssocSemiring _
          (algebraMap (Localization.Away (↑r : S)) (Localization.Away t_1))
          (comp (algebraMap S (Localization.Away (↑r : S))) f))
x : (a : (↑s : Type u)) × (↑(t a) : Type u)
a : (↑s : Type u)
b : (↑(t a) : Type u)
h :
  Associated (↑b : Localization.Away (↑a : S))
    (HMul.hMul (β := Localization.Away (↑a : S)) (↑b : Localization.Away (↑a : S))
      ((algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S))
          ((↑a : S) ^ (IsLocalization.Away.sec (↑a : S) (↑b : Localization.Away (↑a : S))).2) :
        Localization.Away (↑a : S)))
⊢ Associated (↑b : Localization.Away (↑a : S))
    ((algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S))
      (IsLocalization.Away.sec (↑a : S) (↑b : Localization.Away (↑a : S))).1)

Tactic:
rw [← IsLocalization.Away.sec_spec]

Premises used: IsLocalization.Away.sec_spec
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
t : (r : (↑s : Type u)) → Set (Localization.Away (↑r : S))
htone : ∀ (r : (↑s : Type u)), Eq (α := Ideal (Localization.Away (↑r : S))) (Ideal.span (t r)) ⊤
ht :
  ∀ (r : (↑s : Type u)),
    ∀ t_1 ∈ t r,
      (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t_1) _ _
        (@comp _ (Localization.Away (↑r : S)) _ _ Semiring.toNonAssocSemiring _
          (algebraMap (Localization.Away (↑r : S)) (Localization.Away t_1))
          (comp (algebraMap S (Localization.Away (↑r : S))) f))
x : (a : (↑s : Type u)) × (↑(t a) : Type u)
a : (↑s : Type u)
b : (↑(t a) : Type u)
h :
  IsUnit (M := Localization.Away (↑a : S))
    ((algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S))
        ((↑a : S) ^ (IsLocalization.Away.sec (↑a : S) (↑b : Localization.Away (↑a : S))).2) :
      Localization.Away (↑a : S))
⊢ Associated (↑b : Localization.Away (↑a : S))
    (HMul.hMul (β := Localization.Away (↑a : S)) (↑b : Localization.Away (↑a : S))
      ((algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S))
          ((↑a : S) ^ (IsLocalization.Away.sec (↑a : S) (↑b : Localization.Away (↑a : S))).2) :
        Localization.Away (↑a : S)))

Tactic:
apply associated_mul_unit_right

Premises used: associated_mul_unit_right
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
t : (r : (↑s : Type u)) → Set (Localization.Away (↑r : S))
htone : ∀ (r : (↑s : Type u)), Eq (α := Ideal (Localization.Away (↑r : S))) (Ideal.span (t r)) ⊤
ht :
  ∀ (r : (↑s : Type u)),
    ∀ t_1 ∈ t r,
      (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t_1) _ _
        (@comp _ (Localization.Away (↑r : S)) _ _ Semiring.toNonAssocSemiring _
          (algebraMap (Localization.Away (↑r : S)) (Localization.Away t_1))
          (comp (algebraMap S (Localization.Away (↑r : S))) f))
x : (a : (↑s : Type u)) × (↑(t a) : Type u)
a : (↑s : Type u)
b : (↑(t a) : Type u)
h :
  IsUnit
    (HPow.hPow (α := Localization.Away (↑a : S))
      ((algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S)) (↑a : S))
      (IsLocalization.Away.sec (↑a : S) (↑b : Localization.Away (↑a : S))).2)
⊢ IsUnit (M := Localization.Away (↑a : S))
    ((algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S))
        ((↑a : S) ^ (IsLocalization.Away.sec (↑a : S) (↑b : Localization.Away (↑a : S))).2) :
      Localization.Away (↑a : S))

Tactic:
rw [map_pow _ _]

Premises used: map_pow
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
t : (r : (↑s : Type u)) → Set (Localization.Away (↑r : S))
htone : ∀ (r : (↑s : Type u)), Eq (α := Ideal (Localization.Away (↑r : S))) (Ideal.span (t r)) ⊤
ht :
  ∀ (r : (↑s : Type u)),
    ∀ t_1 ∈ t r,
      (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t_1) _ _
        (@comp _ (Localization.Away (↑r : S)) _ _ Semiring.toNonAssocSemiring _
          (algebraMap (Localization.Away (↑r : S)) (Localization.Away t_1))
          (comp (algebraMap S (Localization.Away (↑r : S))) f))
x : (a : (↑s : Type u)) × (↑(t a) : Type u)
a : (↑s : Type u)
b : (↑(t a) : Type u)
⊢ IsUnit
    (HPow.hPow (α := Localization.Away (↑a : S))
      ((algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S)) (↑a : S))
      (IsLocalization.Away.sec (↑a : S) (↑b : Localization.Away (↑a : S))).2)

Tactic:
IsUnit.pow _ (IsLocalization.Away.algebraMap_isUnit _)

Premises used: IsUnit.pow, IsLocalization.Away.algebraMap_isUnit
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
t : (r : (↑s : Type u)) → Set (Localization.Away (↑r : S))
htone : ∀ (r : (↑s : Type u)), Eq (α := Ideal (Localization.Away (↑r : S))) (Ideal.span (t r)) ⊤
ht :
  ∀ (r : (↑s : Type u)),
    ∀ t_1 ∈ t r,
      (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t_1) _ _
        (@comp _ (Localization.Away (↑r : S)) _ _ Semiring.toNonAssocSemiring _
          (algebraMap (Localization.Away (↑r : S)) (Localization.Away t_1))
          (comp (algebraMap S (Localization.Away (↑r : S))) f))
x : (a : (↑s : Type u)) × (↑(t a) : Type u)
a : (↑s : Type u)
b : (↑(t a) : Type u)
⊢ IsUnit
    (HPow.hPow (α := Localization.Away (↑a : S))
      ((algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S)) (↑a : S))
      (IsLocalization.Away.sec (↑a : S) (↑b : Localization.Away (↑a : S))).2)

Tactic:
exact IsUnit.pow _ (IsLocalization.Away.algebraMap_isUnit _)

Premises used: IsUnit.pow, IsLocalization.Away.algebraMap_isUnit
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
t : (r : (↑s : Type u)) → Set (Localization.Away (↑r : S))
htone : ∀ (r : (↑s : Type u)), Eq (α := Ideal (Localization.Away (↑r : S))) (Ideal.span (t r)) ⊤
ht :
  ∀ (r : (↑s : Type u)),
    ∀ t_1 ∈ t r,
      (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t_1) _ _
        (@comp _ (Localization.Away (↑r : S)) _ _ Semiring.toNonAssocSemiring _
          (algebraMap (Localization.Away (↑r : S)) (Localization.Away t_1))
          (comp (algebraMap S (Localization.Away (↑r : S))) f))
x : (a : (↑s : Type u)) × (↑(t a) : Type u)
a : (↑s : Type u)
b : (↑(t a) : Type u)
this :
  IsLocalization.Away (R := Localization.Away (↑a : S))
    ((algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S))
        (IsLocalization.Away.sec (↑a : S) (↑b : Localization.Away (↑a : S))).1 :
      Localization.Away (↑a : S))
    (Localization.Away (↑b : Localization.Away (↑a : S)))
⊢ IsLocalization.Away
    (IsLocalization.Away.mulNumerator s (Rₜ := fun (t : (↑s : Type u)) ↦ Localization.Away (↑t : S)) t
      (Sigma.mk (β := fun (a : (↑s : Type u)) ↦ (↑(t a) : Type u)) a b))
    ((fun (x : (a : (↑s : Type u)) × (↑(t a) : Type u)) ↦
        (match (motive := (a : (↑s : Type u)) × (↑(t a) : Type u) → Type u) x with
          | ⟨a, b⟩ => Localization.Away (↑b : Localization.Away (↑a : S)) :
          Type u))
      (Sigma.mk (β := fun (a : (↑s : Type u)) ↦ (↑(t a) : Type u)) a b))

Tactic:
apply IsLocalization.Away.mul' (Localization.Away a.val) (Localization.Away b.val)

Premises used: Localization.Away, IsLocalization.Away.mul', Subtype.val
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
t : (r : (↑s : Type u)) → Set (Localization.Away (↑r : S))
htone : ∀ (r : (↑s : Type u)), Eq (α := Ideal (Localization.Away (↑r : S))) (Ideal.span (t r)) ⊤
ht :
  ∀ (r : (↑s : Type u)),
    ∀ t_1 ∈ t r,
      (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t_1) _ _
        (@comp _ (Localization.Away (↑r : S)) _ _ Semiring.toNonAssocSemiring _
          (algebraMap (Localization.Away (↑r : S)) (Localization.Away t_1))
          (comp (algebraMap S (Localization.Away (↑r : S))) f))
a : (↑s : Type u)
b : (↑(t a) : Type u)
refine_2 :
  P (S :=
    (fun (x : (a : (↑s : Type u)) × (↑(t a) : Type u)) ↦
        (match (motive := (a : (↑s : Type u)) × (↑(t a) : Type u) → Type u) x with
          | ⟨a, b⟩ => Localization.Away (↑b : Localization.Away (↑a : S)) :
          Type u))
      (Sigma.mk (β := fun (a : (↑s : Type u)) ↦ (↑(t a) : Type u)) a b))
    (comp
      (@comp _ (Localization.Away (↑a : S)) _ _ Semiring.toNonAssocSemiring _
        (algebraMap (Localization.Away (↑a : S)) (Localization.Away (↑b : Localization.Away (↑a : S))))
        (algebraMap S (Localization.Away (↑a : S))))
      f)
⊢ P (S :=
    (fun (x : (a : (↑s : Type u)) × (↑(t a) : Type u)) ↦
        (match (motive := (a : (↑s : Type u)) × (↑(t a) : Type u) → Type u) x with
          | ⟨a, b⟩ => Localization.Away (↑b : Localization.Away (↑a : S)) :
          Type u))
      (Sigma.mk (β := fun (a : (↑s : Type u)) ↦ (↑(t a) : Type u)) a b))
    (comp
      (algebraMap S
        ((fun (x : (a : (↑s : Type u)) × (↑(t a) : Type u)) ↦
            (match (motive := (a : (↑s : Type u)) × (↑(t a) : Type u) → Type u) x with
              | ⟨a, b⟩ => Localization.Away (↑b : Localization.Away (↑a : S)) :
              Type u))
          (Sigma.mk (β := fun (a : (↑s : Type u)) ↦ (↑(t a) : Type u)) a b)))
      f)

Tactic:
rw [IsScalarTower.algebraMap_eq S (Localization.Away a.val) (Localization.Away b.val)]

Premises used: Localization.Away, IsScalarTower.algebraMap_eq, Subtype.val