awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
hg : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) g
⊢ ∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
    ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)

Tactic:
rw [locally_iff_finite] at hf hg

Premises used: RingHom.locally_iff_finite
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
hg : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) g
hf₁ :
  ∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
    ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
⊢ ∃ (s : Finset T) (_ : Eq (α := Ideal T) (Ideal.span (↑s : Set T)) ⊤),
    ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)

Tactic:
rw [locally_iff_finite] at hf hg

Premises used: RingHom.locally_iff_finite
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf :
  ∃ (s : Finset S) (_ : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤),
    ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
hg :
  ∃ (s : Finset T) (_ : Eq (α := Ideal T) (Ideal.span (↑s : Set T)) ⊤),
    ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
obtain :
  ∀ (sf : Finset S) (hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤)
    (hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)),
    Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (g.comp f)
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (g.comp f)

Tactic:
obtain ⟨sf, hsfone, hsf⟩ := hf
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hg :
  ∃ (s : Finset T) (_ : Eq (α := Ideal T) (Ideal.span (↑s : Set T)) ⊤),
    ∀ t ∈ s, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
obtain :
  ∀ (sg : Finset T) (hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤)
    (hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)),
    Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (g.comp f)
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (g.comp f)

Tactic:
obtain ⟨sg, hsgone, hsg⟩ := hg
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
rw :
  ∃ (ι : Type u) (s : ι → T) (_ : Eq (α := Ideal T) (Ideal.span (Set.range s)) ⊤) (Sₜ : ι → Type u) (x :
    (i : ι) → CommRing (Sₜ i)) (x_1 : (i : ι) → Algebra T (Sₜ i)) (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
    ∀ (i : ι), P (S := Sₜ i) (comp (algebraMap T (Sₜ i)) (g.comp f))
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (g.comp f)

Tactic:
rw [locally_iff_exists hPi]

Premises used: RingHom.locally_iff_exists
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
⊢ ∃ (ι : Type u) (s : ι → T) (_ : Eq (α := Ideal T) (Ideal.span (Set.range s)) ⊤) (Sₜ : ι → Type u) (x :
    (i : ι) → CommRing (Sₜ i)) (x_1 : (i : ι) → Algebra T (Sₜ i)) (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
    ∀ (i : ι), P (S := Sₜ i) (comp (algebraMap T (Sₜ i)) (g.comp f))

Tactic:
⟨sf × sg, fun (a, b) ↦ g a * b, ?_,
      fun (a, b) ↦ Localization.Away ((algebraMap T (Localization.Away b.val)) (g a.val)),
      inferInstance, inferInstance, inferInstance, ?_⟩

Premises used: HMul.hMul, Algebra.algebraMap, Localization.Away, Membership.mem, inferInstance, Subtype, Exists.intro, Prod, Subtype.val, DFunLike.coe, _private.0.RingHom.locally_stableUnderComposition.match_1
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
refine_1 :
  Eq.{u + 1} (α := Ideal T)
    (Ideal.span
      (Set.range fun (x : ↥sf × ↥sg) ↦
        match (motive := ↥sf × ↥sg → T) x with
        | (a, b) => HMul.hMul (α := T) ((g : (a : S) → T) (↑a : S) : T) (↑b : T)))
    ⊤
refine_2 :
  ∀ (i : ↥sf × ↥sg),
    P (S :=
      (fun (x : ↥sf × ↥sg) ↦
          (match (motive := ↥sf × ↥sg → Type u) x with
            | (a, b) =>
              Localization.Away (M := Localization.Away (↑b : T))
                ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T))
                    ((g : (a : S) → T) (↑a : S)) :
                  Localization.Away (↑b : T)) :
            Type u))
        i)
      (comp
        (algebraMap T
          ((fun (x : ↥sf × ↥sg) ↦
              (match (motive := ↥sf × ↥sg → Type u) x with
                | (a, b) =>
                  Localization.Away (M := Localization.Away (↑b : T))
                    ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T))
                        ((g : (a : S) → T) (↑a : S)) :
                      Localization.Away (↑b : T)) :
                Type u))
            i))
        (g.comp f))
⊢ ∃ (ι : Type u) (s : ι → T) (_ : Eq (α := Ideal T) (Ideal.span (Set.range s)) ⊤) (Sₜ : ι → Type u) (x :
    (i : ι) → CommRing (Sₜ i)) (x_1 : (i : ι) → Algebra T (Sₜ i)) (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)),
    ∀ (i : ι), P (S := Sₜ i) (comp (algebraMap T (Sₜ i)) (g.comp f))

Tactic:
refine ⟨sf × sg, fun (a, b) ↦ g a * b, ?_,
      fun (a, b) ↦ Localization.Away ((algebraMap T (Localization.Away b.val)) (g a.val)),
      inferInstance, inferInstance, inferInstance, ?_⟩
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
refine_1 :
  (↑sg : Set T) ⊆
    (↑(Ideal.span
          (Set.range fun (x : ↥sf × ↥sg) ↦
            match (motive := ↥sf × ↥sg → T) x with
            | (a, b) => HMul.hMul (α := T) ((g : (a : S) → T) (↑a : S) : T) (↑b : T))) :
      Set T)
⊢ Eq.{u + 1} (α := Ideal T)
    (Ideal.span
      (Set.range fun (x : ↥sf × ↥sg) ↦
        match (motive := ↥sf × ↥sg → T) x with
        | (a, b) => HMul.hMul (α := T) ((g : (a : S) → T) (↑a : S) : T) (↑b : T)))
    ⊤

Tactic:
rw [eq_top_iff, ← hsgone, Ideal.span_le]

Premises used: Ideal.span_le, eq_top_iff
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
t : T
ht : t ∈ (↑sg : Set T)
⊢ Membership.mem (γ := Ideal S) (Ideal.span (Set.range fun (a : ↥sf) ↦ (↑a : S))) 1

Tactic:
simp [hsfone]
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
t : T
ht : t ∈ (↑sg : Set T)
⊢ Membership.mem (γ := Ideal S) (Ideal.span (Set.range fun (a : ↥sf) ↦ (↑a : S))) 1

Tactic:
have : 1 ∈ Ideal.span (Set.range <| fun a : sf ↦ a.val) := by simp [hsfone]
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
t : T
ht : t ∈ (↑sg : Set T)
this : Membership.mem (γ := Ideal S) (Ideal.span (Set.range fun (a : ↥sf) ↦ (↑a : S))) 1
refine_1 :
  ∀ (this : ∃ (c : ↥sf → S), Eq.{u + 1} (α := S) (∑ i : ↥sf, c i * (↑i : S)) 1),
    ∃ (c : ↥sf × ↥sg → T), ∑ i : ↥sf × ↥sg, c i * HMul.hMul (α := T) ((g : (a : S) → T) (↑i.1 : S) : T) (↑i.2 : T) = t
⊢ t ∈
    (↑(Ideal.span
          (Set.range fun (x : ↥sf × ↥sg) ↦
            match (motive := ↥sf × ↥sg → T) x with
            | (a, b) => HMul.hMul (α := T) ((g : (a : S) → T) (↑a : S) : T) (↑b : T))) :
      Set T)

Tactic:
simp only [Ideal.mem_span_range_iff_exists_fun, SetLike.mem_coe] at this ⊢

Premises used: Ideal.mem_span_range_iff_exists_fun, SetLike.mem_coe
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
t : T
ht : t ∈ (↑sg : Set T)
this : ∃ (c : ↥sf → S), Eq.{u + 1} (α := S) (∑ i : ↥sf, c i * (↑i : S)) 1
refine_1 :
  ∀ (cf : ↥sf → S) (hcf : Eq.{u + 1} (α := S) (∑ i : ↥sf, cf i * (↑i : S)) 1),
    ∃ (c : ↥sf × ↥sg → T), ∑ i : ↥sf × ↥sg, c i * HMul.hMul (α := T) ((g : (a : S) → T) (↑i.1 : S) : T) (↑i.2 : T) = t
⊢ ∃ (c : ↥sf × ↥sg → T), ∑ i : ↥sf × ↥sg, c i * HMul.hMul (α := T) ((g : (a : S) → T) (↑i.1 : S) : T) (↑i.2 : T) = t

Tactic:
obtain ⟨cf, hcf⟩ := this
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
t : T
ht : t ∈ (↑sg : Set T)
cf : ↥sf → S
hcf : Eq.{u + 1} (α := S) (∑ i : ↥sf, cf i * (↑i : S)) 1
cg : ↥sg → T := Pi.single (M := fun (a : ↥sg) ↦ T) (Subtype.mk (p := fun (x : T) ↦ x ∈ sg) t ht) 1
h :
  ∑ i : ↥sf × ↥sg,
      (fun (x : ↥sf × ↥sg) ↦
            (match (motive := ↥sf × ↥sg → T) x with
              | (a, b) => HMul.hMul (α := T) ((g : (a : S) → T) (cf a) : T) (cg b) :
              T))
          i *
        HMul.hMul (α := T) ((g : (a : S) → T) (↑i.1 : S) : T) (↑i.2 : T) =
    t
⊢ ∃ (c : ↥sf × ↥sg → T), ∑ i : ↥sf × ↥sg, c i * HMul.hMul (α := T) ((g : (a : S) → T) (↑i.1 : S) : T) (↑i.2 : T) = t

Tactic:
use fun (a, b) ↦ g (cf a) * cg b
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
t : T
ht : t ∈ (↑sg : Set T)
cf : ↥sf → S
hcf : Eq.{u + 1} (α := S) (∑ i : ↥sf, cf i * (↑i : S)) 1
cg : ↥sg → T := Pi.single (M := fun (a : ↥sg) ↦ T) (Subtype.mk (p := fun (x : T) ↦ x ∈ sg) t ht) 1
⊢ ∑ i : ↥sf × ↥sg,
      (fun (x : ↥sf × ↥sg) ↦
            (match (motive := ↥sf × ↥sg → T) x with
              | (a, b) => HMul.hMul (α := T) ((g : (a : S) → T) (cf a) : T) (cg b) :
              T))
          i *
        HMul.hMul (α := T) ((g : (a : S) → T) (↑i.1 : S) : T) (↑i.2 : T) =
    t

Tactic:
simp [cg, Pi.single_apply, Fintype.sum_prod_type, ← mul_assoc, ← Finset.sum_mul, ← map_mul,
      ← map_sum, hcf] at hcf ⊢

Premises used: Pi.single_apply, mul_assoc, map_sum, map_mul, Fintype.sum_prod_type, Finset.sum_mul
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
a : ↥sf
b : ↥sg
g' : S →+* Localization.Away (↑b : T) := comp (algebraMap T (Localization.Away (↑b : T))) g
a' : Localization.Away (↑b : T) :=
  (algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T)) ((g : (a : S) → T) (↑a : S))
a₁ :
  ∀ (x : R),
    Eq (α := Localization.Away a')
      ((comp (algebraMap T (Localization.Away a')) (g.comp f) : (a : R) → Localization.Away a') x :
        Localization.Away a')
      ((comp (Localization.awayMap g' (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) :
            (a : R) → Localization.Away a')
          x :
        Localization.Away a')
⊢ Eq (α := R →+* Localization.Away a') (comp (algebraMap T (Localization.Away a')) (g.comp f))
    (comp (Localization.awayMap g' (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f))

Tactic:
ext x
-- Module: Mathlib.RingTheory.RingHom.Locally
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Eq (α := Ideal S) (Ideal.span (↑sf : Set S)) ⊤
hsf : ∀ t ∈ sf, P (S := Localization.Away t) (comp (algebraMap S (Localization.Away t)) f)
sg : Finset T
hsgone : Eq (α := Ideal T) (Ideal.span (↑sg : Set T)) ⊤
hsg : ∀ t ∈ sg, P (S := Localization.Away t) (comp (algebraMap T (Localization.Away t)) g)
a : ↥sf
b : ↥sg
g' : S →+* Localization.Away (↑b : T) := comp (algebraMap T (Localization.Away (↑b : T))) g
a' : Localization.Away (↑b : T) :=
  (algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T)) ((g : (a : S) → T) (↑a : S))
x : R
a₁ :
  Eq (α :=
    Localization.Away (M := Localization.Away (↑b : T))
      ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T)) ((g : (a : S) → T) (↑a : S)) :
        Localization.Away (↑b : T)))
    ((algebraMap T
            (Localization.Away (M := Localization.Away (↑b : T))
              ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T))
                  ((g : (a : S) → T) (↑a : S)) :
                Localization.Away (↑b : T))) :
          (a_1 : T) →
            Localization.Away
              ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T))
                ((g : (a : S) → T) (↑a : S))))
        ((g : (a : S) → T) ((f : (a : R) → S) x : S)) :
      Localization.Away (M := Localization.Away (↑b : T))
        ((algebraMap T (Localization.Away (↑b : T)) : (a : T) → Localization.Away (↑b : T))
            ((g : (a : S) → T) (↑a : S)) :
          Localization.Away (↑b : T)))
    ((Localization.awayMap g' (↑a : S) :
          (a_1 : Localization.Away (↑a : S)) → Localization.Away ((g' : (a : S) → Localization.Away (↑b : T)) (↑a : S)))
        ((algebraMap S (Localization.Away (↑a : S)) : (a_1 : S) → Localization.Away (↑a : S)) ((f : (a : R) → S) x)) :
      Localization.Away (M := Localization.Away (↑b : T))
        ((g' : (a : S) → Localization.Away (↑b : T)) (↑a : S) : Localization.Away (↑b : T)))
⊢ Eq (α := Localization.Away a')
    ((comp (algebraMap T (Localization.Away a')) (g.comp f) : (a : R) → Localization.Away a') x : Localization.Away a')
    ((comp (Localization.awayMap g' (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) :
          (a : R) → Localization.Away a')
        x :
      Localization.Away a')

Tactic:
simp only [coe_comp, Function.comp_apply, a']

Premises used: RingHom.coe_comp, Function.comp_apply