-- Mathlib/RingTheory/LocalProperties/Basic.lean
theorem RingHom.ofLocalizationSpan_iff_finite :
    RingHom.OfLocalizationSpan @P ↔ RingHom.OfLocalizationFiniteSpan @P

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

Tactic:
delta RingHom.OfLocalizationSpan RingHom.OfLocalizationFiniteSpan

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 R),
      Ideal.span s = ⊤ → (∀ (r : ↑s), P (Localization.awayMap f ↑r)) → P f) ↔
    ∀ ⦃R S : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset R),
      Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P (Localization.awayMap f ↑r)) → 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 a✝), Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P (Localization.awayMap e✝ ↑r)) → P e✝) →
    ∀ (s : Set a✝), Ideal.span s = ⊤ → (∀ (r : ↑s), P (Localization.awayMap e✝ ↑r)) → 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 a✝), Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P (Localization.awayMap e✝ ↑r)) → P e✝
s : Set a✝
hs : Ideal.span s = ⊤
hs' : ∀ (r : ↑s), P (Localization.awayMap e✝ ↑r)
⊢ 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 R),
      Ideal.span s = ⊤ → (∀ (r : ↑s), P (Localization.awayMap f ↑r)) → P f) ↔
    ∀ ⦃R S : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Finset R),
      Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P (Localization.awayMap f ↑r)) → 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 a), Ideal.span s = ⊤ → (∀ (r : ↑s), P (Localization.awayMap e ↑r)) → P e) ↔
      ∀ (s : Finset a), Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P (Localization.awayMap e ↑r)) → 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 a✝), Ideal.span s = ⊤ → (∀ (r : ↑s), P (Localization.awayMap e✝ ↑r)) → P e✝
s : Finset a✝
⊢ Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P (Localization.awayMap e✝ ↑r)) → 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 a), Ideal.span s = ⊤ → (∀ (r : ↑s), P (Localization.awayMap e ↑r)) → P e) ↔
      ∀ (s : Finset a), Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P (Localization.awayMap e ↑r)) → 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 a✝), Ideal.span s = ⊤ → (∀ (r : ↑s), P (Localization.awayMap e✝ ↑r)) → P e✝) ↔
    ∀ (s : Finset a✝), Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P (Localization.awayMap e✝ ↑r)) → 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 a✝), Ideal.span s = ⊤ → (∀ (r : ↑s), P (Localization.awayMap e✝ ↑r)) → P e✝) →
    ∀ (s : Finset a✝), Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P (Localization.awayMap e✝ ↑r)) → 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 a✝), Ideal.span s = ⊤ → (∀ (r : ↑s), P (Localization.awayMap e✝ ↑r)) → P e✝
s : Finset a✝
⊢ Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P (Localization.awayMap e✝ ↑r)) → P e✝

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 a✝), Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P (Localization.awayMap e✝ ↑r)) → P e✝
s : Set a✝
hs : Ideal.span s = ⊤
hs' : ∀ (r : ↑s), P (Localization.awayMap e✝ ↑r)
⊢ 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 a✝), Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P (Localization.awayMap e✝ ↑r)) → P e✝
s : Set a✝
hs : Ideal.span s = ⊤
hs' : ∀ (r : ↑s), P (Localization.awayMap e✝ ↑r)
s' : Finset a✝
h₁ : ↑s' ⊆ s
h₂ : Ideal.span ↑s' = ⊤
⊢ P e✝

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 a✝), Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P (Localization.awayMap e✝ ↑r)) → P e✝
s : Set a✝
hs : Ideal.span s = ⊤
hs' : ∀ (r : ↑s), P (Localization.awayMap e✝ ↑r)
s' : Finset a✝
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
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 a✝), Ideal.span s = ⊤ → (∀ (r : ↑s), P (Localization.awayMap e✝ ↑r)) → P e✝) ↔
    ∀ (s : Finset a✝), Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P (Localization.awayMap e✝ ↑r)) → 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 a✝), Ideal.span s = ⊤ → (∀ (r : ↑s), P (Localization.awayMap e✝ ↑r)) → P e✝) →
    ∀ (s : Finset a✝), Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P (Localization.awayMap e✝ ↑r)) → 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 a✝), Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P (Localization.awayMap e✝ ↑r)) → P e✝) →
    ∀ (s : Set a✝), Ideal.span s = ⊤ → (∀ (r : ↑s), P (Localization.awayMap e✝ ↑r)) → P e✝