-- Mathlib/RingTheory/LocalRing/RingHom/Basic.lean
theorem local_hom_TFAE (f : R →+* S) :
    List.TFAE
      [IsLocalHom f, f '' (maximalIdeal R).1 ⊆ maximalIdeal S,
        (maximalIdeal R).map f ≤ maximalIdeal S, maximalIdeal R ≤ (maximalIdeal S).comap f,
        (maximalIdeal S).comap f = maximalIdeal R]

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalHom f → ⇑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ⇑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
⊢ [IsLocalHom f, ⇑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S),
      Ideal.map f (maximalIdeal R) ≤ maximalIdeal S, maximalIdeal R ≤ Ideal.comap f (maximalIdeal S),
      Ideal.comap f (maximalIdeal S) = maximalIdeal R].TFAE

Tactic:
tfae_have 3 ↔ 4 := Ideal.map_le_iff_le_comap

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalHom f → ⇑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ⇑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
⊢ [IsLocalHom f, ⇑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S),
      Ideal.map f (maximalIdeal R) ≤ maximalIdeal S, maximalIdeal R ≤ Ideal.comap f (maximalIdeal S),
      Ideal.comap f (maximalIdeal S) = maximalIdeal R].TFAE

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
⊢ [IsLocalHom f, ⇑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S),
      Ideal.map f (maximalIdeal R) ≤ maximalIdeal S, maximalIdeal R ≤ Ideal.comap f (maximalIdeal S),
      Ideal.comap f (maximalIdeal S) = maximalIdeal R].TFAE

Tactic:
tfae_have 1 → 2
| _, _, ⟨a, ha, rfl⟩ => map_nonunit f a ha

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalHom f → ⇑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
⊢ [IsLocalHom f, ⇑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S),
      Ideal.map f (maximalIdeal R) ≤ maximalIdeal S, maximalIdeal R ≤ Ideal.comap f (maximalIdeal S),
      Ideal.comap f (maximalIdeal S) = maximalIdeal R].TFAE

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalHom f → ⇑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
⊢ [IsLocalHom f, ⇑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S),
      Ideal.map f (maximalIdeal R) ≤ maximalIdeal S, maximalIdeal R ≤ Ideal.comap f (maximalIdeal S),
      Ideal.comap f (maximalIdeal S) = maximalIdeal R].TFAE

Tactic:
tfae_have 2 → 4 := Set.image_subset_iff.1

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalHom f → ⇑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ⇑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
⊢ [IsLocalHom f, ⇑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S),
      Ideal.map f (maximalIdeal R) ≤ maximalIdeal S, maximalIdeal R ≤ Ideal.comap f (maximalIdeal S),
      Ideal.comap f (maximalIdeal S) = maximalIdeal R].TFAE

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalHom f → ⇑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ⇑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
⊢ [IsLocalHom f, ⇑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S),
      Ideal.map f (maximalIdeal R) ≤ maximalIdeal S, maximalIdeal R ≤ Ideal.comap f (maximalIdeal S),
      Ideal.comap f (maximalIdeal S) = maximalIdeal R].TFAE

Tactic:
tfae_have 4 → 1 := fun h ↦ ⟨fun x => not_imp_not.1 (@h x)⟩

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalHom f → ⇑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ⇑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_4_to_1 : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S) → IsLocalHom f
⊢ [IsLocalHom f, ⇑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S),
      Ideal.map f (maximalIdeal R) ≤ maximalIdeal S, maximalIdeal R ≤ Ideal.comap f (maximalIdeal S),
      Ideal.comap f (maximalIdeal S) = maximalIdeal R].TFAE

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalHom f → ⇑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ⇑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_4_to_1 : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S) → IsLocalHom f
tfae_1_to_5 : IsLocalHom f → Ideal.comap f (maximalIdeal S) = maximalIdeal R
tfae_5_to_4 : Ideal.comap f (maximalIdeal S) = maximalIdeal R → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
⊢ [IsLocalHom f, ⇑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S),
      Ideal.map f (maximalIdeal R) ≤ maximalIdeal S, maximalIdeal R ≤ Ideal.comap f (maximalIdeal S),
      Ideal.comap f (maximalIdeal S) = maximalIdeal R].TFAE

Tactic:
tfae_finish

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalHom f → ⇑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ⇑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_4_to_1 : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S) → IsLocalHom f
x✝ : IsLocalHom f
⊢ Ideal.comap f (maximalIdeal S) = maximalIdeal R

Tactic:
ext

Result:
case h
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsLocalRing R
inst✝¹ : CommSemiring S
inst✝ : IsLocalRing S
f : R →+* S
tfae_1_to_2 : IsLocalHom f → ⇑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S)
tfae_2_to_4 :
  ⇑f '' ↑(maximalIdeal R).toAddSubmonoid ⊆ ↑(maximalIdeal S) → maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_3_iff_4 : Ideal.map f (maximalIdeal R) ≤ maximalIdeal S ↔ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
tfae_4_to_1 : maximalIdeal R ≤ Ideal.comap f (maximalIdeal S) → IsLocalHom f
x✝¹ : IsLocalHom f
x✝ : R
⊢ x✝ ∈ Ideal.comap f (maximalIdeal S) ↔ x✝ ∈ maximalIdeal R