-- Mathlib/RingTheory/LocalProperties/Basic.lean
theorem RingHom.ofLocalizationSpanTarget_iff_finite :
    RingHom.OfLocalizationSpanTarget @P ↔ RingHom.OfLocalizationFiniteSpanTarget @P

Proof state:
case h.mpr.intro.intro
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a✝ b✝ : Type u
c✝ : CommRing a✝
d✝ : CommRing b✝
e✝ : a✝ →+* b✝
h :
  ∀ (s : Finset b✝),
    Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝
s : Set b✝
hs : Ideal.span s = ⊤
hs' : ∀ (r : ↑s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)
s' : Finset b✝
h₁ : ↑s' ⊆ s
h₂ : Ideal.span ↑s' = ⊤
⊢ P e✝

Tactic:
exact h s' h₂ fun x => hs' ⟨_, h₁ x.prop⟩

Result:
no goals

Proof state:
case h.mpr
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a✝ b✝ : Type u
c✝ : CommRing a✝
d✝ : CommRing b✝
e✝ : a✝ →+* b✝
h :
  ∀ (s : Finset b✝),
    Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝
s : Set b✝
hs : Ideal.span s = ⊤
hs' : ∀ (r : ↑s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)
⊢ P e✝

Tactic:
obtain ⟨s', h₁, h₂⟩ := (Ideal.span_eq_top_iff_finite s).mp hs

Result:
case h.mpr.intro.intro
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a✝ b✝ : Type u
c✝ : CommRing a✝
d✝ : CommRing b✝
e✝ : a✝ →+* b✝
h :
  ∀ (s : Finset b✝),
    Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝
s : Set b✝
hs : Ideal.span s = ⊤
hs' : ∀ (r : ↑s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)
s' : Finset b✝
h₁ : ↑s' ⊆ s
h₂ : Ideal.span ↑s' = ⊤
⊢ P e✝

Proof state:
case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a✝ b✝ : Type u
c✝ : CommRing a✝
d✝ : CommRing b✝
e✝ : a✝ →+* b✝
⊢ (∀ (s : Set b✝), Ideal.span s = ⊤ → (∀ (r : ↑s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝) ↔
    ∀ (s : Finset b✝),
      Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝

Tactic:
constructor

Result:
case h.mp
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a✝ b✝ : Type u
c✝ : CommRing a✝
d✝ : CommRing b✝
e✝ : a✝ →+* b✝
⊢ (∀ (s : Set b✝), Ideal.span s = ⊤ → (∀ (r : ↑s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝) →
    ∀ (s : Finset b✝),
      Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝

case h.mpr
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a✝ b✝ : Type u
c✝ : CommRing a✝
d✝ : CommRing b✝
e✝ : a✝ →+* b✝
⊢ (∀ (s : Finset b✝),
      Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝) →
    ∀ (s : Set b✝), Ideal.span s = ⊤ → (∀ (r : ↑s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
⊢ OfLocalizationSpanTarget P ↔ OfLocalizationFiniteSpanTarget P

Tactic:
delta RingHom.OfLocalizationSpanTarget RingHom.OfLocalizationFiniteSpanTarget

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
⊢ (∀ ⦃R S : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Set S),
      Ideal.span s = ⊤ → (∀ (r : ↑s), P ((algebraMap S (Localization.Away ↑r)).comp f)) → P f) ↔
    ∀ ⦃R S : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset S),
      Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P ((algebraMap S (Localization.Away ↑r)).comp f)) → P f

Proof state:
case h.mpr
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a✝ b✝ : Type u
c✝ : CommRing a✝
d✝ : CommRing b✝
e✝ : a✝ →+* b✝
⊢ (∀ (s : Finset b✝),
      Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝) →
    ∀ (s : Set b✝), Ideal.span s = ⊤ → (∀ (r : ↑s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝

Tactic:
intro h s hs hs'

Result:
case h.mpr
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a✝ b✝ : Type u
c✝ : CommRing a✝
d✝ : CommRing b✝
e✝ : a✝ →+* b✝
h :
  ∀ (s : Finset b✝),
    Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝
s : Set b✝
hs : Ideal.span s = ⊤
hs' : ∀ (r : ↑s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)
⊢ P e✝

Proof state:
case h.mp
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a✝ b✝ : Type u
c✝ : CommRing a✝
d✝ : CommRing b✝
e✝ : a✝ →+* b✝
⊢ (∀ (s : Set b✝), Ideal.span s = ⊤ → (∀ (r : ↑s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝) →
    ∀ (s : Finset b✝),
      Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝

Tactic:
intro h s

Result:
case h.mp
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a✝ b✝ : Type u
c✝ : CommRing a✝
d✝ : CommRing b✝
e✝ : a✝ →+* b✝
h : ∀ (s : Set b✝), Ideal.span s = ⊤ → (∀ (r : ↑s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝
s : Finset b✝
⊢ Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝

Proof state:
case h.mp
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a✝ b✝ : Type u
c✝ : CommRing a✝
d✝ : CommRing b✝
e✝ : a✝ →+* b✝
h : ∀ (s : Set b✝), Ideal.span s = ⊤ → (∀ (r : ↑s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝
s : Finset b✝
⊢ Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝

Tactic:
exact h s

Result:
no goals

Proof state:
case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
⊢ ∀ (a b : Type u) (c : CommRing a) (d : CommRing b) (e : a →+* b),
    (∀ (s : Set b), Ideal.span s = ⊤ → (∀ (r : ↑s), P ((algebraMap b (Localization.Away ↑r)).comp e)) → P e) ↔
      ∀ (s : Finset b),
        Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P ((algebraMap b (Localization.Away ↑r)).comp e)) → P e

Tactic:
intros

Result:
case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a✝ b✝ : Type u
c✝ : CommRing a✝
d✝ : CommRing b✝
e✝ : a✝ →+* b✝
⊢ (∀ (s : Set b✝), Ideal.span s = ⊤ → (∀ (r : ↑s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝) ↔
    ∀ (s : Finset b✝),
      Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
⊢ (∀ ⦃R S : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Set S),
      Ideal.span s = ⊤ → (∀ (r : ↑s), P ((algebraMap S (Localization.Away ↑r)).comp f)) → P f) ↔
    ∀ ⦃R S : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset S),
      Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P ((algebraMap S (Localization.Away ↑r)).comp f)) → P f

Tactic:
apply forall₅_congr

Result:
case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
⊢ ∀ (a b : Type u) (c : CommRing a) (d : CommRing b) (e : a →+* b),
    (∀ (s : Set b), Ideal.span s = ⊤ → (∀ (r : ↑s), P ((algebraMap b (Localization.Away ↑r)).comp e)) → P e) ↔
      ∀ (s : Finset b),
        Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P ((algebraMap b (Localization.Away ↑r)).comp e)) → P e