awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
inst_3 : IsLocalHom (R := R) (S := T) (g.comp f)
⊢ IsLocalHom (R := R) (S := S) f

Tactic:
⟨fun _ ha => (isUnit_map_iff (g.comp f) _).mp (g.isUnit_map ha)⟩

Premises used: IsLocalHom.mk, isUnit_map_iff, RingHom.comp, Iff.mp, RingHom.isUnit_map
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_4
S : Type u_5
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : IsLocalRing S
f : R →+* S
inst_3 : IsLocalHom (R := R) (S := S) f
⊢ Nontrivial R

Tactic:
haveI : Nontrivial R := f.domain_nontrivial
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_4
S : Type u_5
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : IsLocalRing S
f : R →+* S
inst_3 : IsLocalHom (R := R) (S := S) f
this : Nontrivial R
h : ∀ (a b : R), a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits R
⊢ IsLocalRing R

Tactic:
apply IsLocalRing.of_nonunits_add

Premises used: IsLocalRing.of_nonunits_add
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_4
S : Type u_5
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : IsLocalRing S
f : R →+* S
inst_3 : IsLocalHom (R := R) (S := S) f
this : Nontrivial R
a b : R
h :
  Membership.mem (α := S) (nonunits S) ((f : (a : R) → S) a : S) →
    Membership.mem (α := S) (nonunits S) ((f : (a : R) → S) b : S) →
      HAdd.hAdd (α := S) (β := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) b : S) ∈ nonunits S
⊢ a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits R

Tactic:
simp_rw [← map_mem_nonunits_iff f, f.map_add]

Premises used: map_mem_nonunits_iff, RingHom.map_add
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_4
S : Type u_5
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : IsLocalRing S
f : R →+* S
inst_3 : IsLocalHom (R := R) (S := S) f
this : Nontrivial R
a b : R
⊢ Membership.mem (α := S) (nonunits S) ((f : (a : R) → S) a : S) →
    Membership.mem (α := S) (nonunits S) ((f : (a : R) → S) b : S) →
      HAdd.hAdd (α := S) (β := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) b : S) ∈ nonunits S

Tactic:
IsLocalRing.nonunits_add

Premises used: Set.Mem, IsLocalRing.nonunits_add
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_4
S : Type u_5
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : IsLocalRing S
f : R →+* S
inst_3 : IsLocalHom (R := R) (S := S) f
this : Nontrivial R
a b : R
⊢ Membership.mem (α := S) (nonunits S) ((f : (a : R) → S) a : S) →
    Membership.mem (α := S) (nonunits S) ((f : (a : R) → S) b : S) →
      HAdd.hAdd (α := S) (β := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) b : S) ∈ nonunits S

Tactic:
exact IsLocalRing.nonunits_add

Premises used: IsLocalRing.nonunits_add
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
inst_4 : IsLocalHom (R := R) (S := S) f
a : R
h : Membership.mem (γ := Ideal R) (maximalIdeal R) a
⊢ Membership.mem (α := S) (γ := Ideal S) (maximalIdeal S) ((f : (a : R) → S) a : S)

Tactic:
fun H => h <| isUnit_of_map_unit f a H

Premises used: Set.Mem, setOf, nonunits, isUnit_of_map_unit, Not
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
⊢ IsLocalHom (R := R) (S := S) f

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
⊢ (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
⊢ ∀ (a : IsLocalHom (R := R) (S := S) f),
    (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
⊢ ∀ (a : IsLocalHom (R := R) (S := S) f),
    (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)

Tactic:
tfae_have 1 → 2
  | _, _, ⟨a, ha, rfl⟩ => map_nonunit f a ha
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
tfae_1_to_2 :
  ∀ (a : IsLocalHom (R := R) (S := S) f),
    (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)
⊢ (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
tfae_1_to_2 :
  ∀ (a : IsLocalHom (R := R) (S := S) f),
    (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)
⊢ LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
tfae_1_to_2 :
  ∀ (a : IsLocalHom (R := R) (S := S) f),
    (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)
⊢ ∀ (a : (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)),
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))

Tactic:
2 → 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
tfae_1_to_2 :
  ∀ (a : IsLocalHom (R := R) (S := S) f),
    (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)
⊢ ∀ (a : (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)),
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))

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

Premises used: Iff.mp, Set.image_subset_iff
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
tfae_1_to_2 :
  ∀ (a : IsLocalHom (R := R) (S := S) f),
    (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)
tfae_2_to_4 :
  ∀ (a : (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)),
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
⊢ LE.le (α := Ideal S) (Ideal.map f (maximalIdeal R)) (maximalIdeal S)

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
tfae_1_to_2 :
  ∀ (a : IsLocalHom (R := R) (S := S) f),
    (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)
tfae_2_to_4 :
  ∀ (a : (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)),
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
⊢ LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
tfae_1_to_2 :
  ∀ (a : IsLocalHom (R := R) (S := S) f),
    (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)
tfae_2_to_4 :
  ∀ (a : (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)),
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
⊢ LE.le (α := Ideal S) (Ideal.map f (maximalIdeal R)) (maximalIdeal S) ↔
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))

Tactic:
3 ↔ 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
tfae_1_to_2 :
  ∀ (a : IsLocalHom (R := R) (S := S) f),
    (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)
tfae_2_to_4 :
  ∀ (a : (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)),
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
⊢ LE.le (α := Ideal S) (Ideal.map f (maximalIdeal R)) (maximalIdeal S) ↔
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))

Tactic:
tfae_have 3 ↔ 4 := Ideal.map_le_iff_le_comap

Premises used: Ideal.map_le_iff_le_comap
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
tfae_1_to_2 :
  ∀ (a : IsLocalHom (R := R) (S := S) f),
    (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)
tfae_2_to_4 :
  ∀ (a : (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)),
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
tfae_3_iff_4 :
  LE.le (α := Ideal S) (Ideal.map f (maximalIdeal R)) (maximalIdeal S) ↔
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
⊢ LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
tfae_1_to_2 :
  ∀ (a : IsLocalHom (R := R) (S := S) f),
    (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)
tfae_2_to_4 :
  ∀ (a : (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)),
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
tfae_3_iff_4 :
  LE.le (α := Ideal S) (Ideal.map f (maximalIdeal R)) (maximalIdeal S) ↔
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
⊢ IsLocalHom (R := R) (S := S) f

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
tfae_1_to_2 :
  ∀ (a : IsLocalHom (R := R) (S := S) f),
    (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)
tfae_2_to_4 :
  ∀ (a : (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)),
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
tfae_3_iff_4 :
  LE.le (α := Ideal S) (Ideal.map f (maximalIdeal R)) (maximalIdeal S) ↔
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
⊢ ∀ (a : LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))), IsLocalHom (R := R) (S := S) f

Tactic:
4 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
tfae_1_to_2 :
  ∀ (a : IsLocalHom (R := R) (S := S) f),
    (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)
tfae_2_to_4 :
  ∀ (a : (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)),
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
tfae_3_iff_4 :
  LE.le (α := Ideal S) (Ideal.map f (maximalIdeal R)) (maximalIdeal S) ↔
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
⊢ ∀ (a : LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))), IsLocalHom (R := R) (S := S) f

Tactic:
tfae_have 4 → 1 := fun h ↦ ⟨fun x => not_imp_not.1 (@h x)⟩
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
tfae_1_to_2 :
  ∀ (a : IsLocalHom (R := R) (S := S) f),
    (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)
tfae_2_to_4 :
  ∀ (a : (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)),
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
tfae_3_iff_4 :
  LE.le (α := Ideal S) (Ideal.map f (maximalIdeal R)) (maximalIdeal S) ↔
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
tfae_4_to_1 :
  ∀ (a : LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))), IsLocalHom (R := R) (S := S) f
⊢ IsLocalHom (R := R) (S := S) f

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
tfae_1_to_2 :
  ∀ (a : IsLocalHom (R := R) (S := S) f),
    (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)
tfae_2_to_4 :
  ∀ (a : (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)),
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
tfae_3_iff_4 :
  LE.le (α := Ideal S) (Ideal.map f (maximalIdeal R)) (maximalIdeal S) ↔
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
tfae_4_to_1 :
  ∀ (a : LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))), IsLocalHom (R := R) (S := S) f
⊢ Eq (α := Ideal R) (Ideal.comap f (maximalIdeal S)) (maximalIdeal R)

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
tfae_1_to_2 :
  ∀ (a : IsLocalHom (R := R) (S := S) f),
    (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)
tfae_2_to_4 :
  ∀ (a : (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)),
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
tfae_3_iff_4 :
  LE.le (α := Ideal S) (Ideal.map f (maximalIdeal R)) (maximalIdeal S) ↔
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
tfae_4_to_1 :
  ∀ (a : LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))), IsLocalHom (R := R) (S := S) f
⊢ ∀ (a : IsLocalHom (R := R) (S := S) f), Eq (α := Ideal R) (Ideal.comap f (maximalIdeal S)) (maximalIdeal R)

Tactic:
1 → 5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
tfae_1_to_2 :
  ∀ (a : IsLocalHom (R := R) (S := S) f),
    (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)
tfae_2_to_4 :
  ∀ (a : (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)),
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
tfae_3_iff_4 :
  LE.le (α := Ideal S) (Ideal.map f (maximalIdeal R)) (maximalIdeal S) ↔
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
tfae_4_to_1 :
  ∀ (a : LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))), IsLocalHom (R := R) (S := S) f
h_1 : IsLocalHom (R := R) (S := S) f
h :
  ∀ (x : R),
    Membership.mem (γ := Ideal R) (Ideal.comap f (maximalIdeal S)) x ↔ Membership.mem (γ := Ideal R) (maximalIdeal R) x
⊢ Eq (α := Ideal R) (Ideal.comap f (maximalIdeal S)) (maximalIdeal R)

Tactic:
ext
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
tfae_1_to_2 :
  ∀ (a : IsLocalHom (R := R) (S := S) f),
    (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)
tfae_2_to_4 :
  ∀ (a : (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)),
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
tfae_3_iff_4 :
  LE.le (α := Ideal S) (Ideal.map f (maximalIdeal R)) (maximalIdeal S) ↔
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
tfae_4_to_1 :
  ∀ (a : LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))), IsLocalHom (R := R) (S := S) f
h : IsLocalHom (R := R) (S := S) f
x : R
⊢ Membership.mem (γ := Ideal R) (Ideal.comap f (maximalIdeal S)) x ↔ Membership.mem (γ := Ideal R) (maximalIdeal R) x

Tactic:
not_iff_not.2 (isUnit_map_iff f _)

Premises used: not_iff_not, Iff.mpr, Set.Mem, setOf, nonunits, isUnit_map_iff, Set.preimage, Not
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
tfae_1_to_2 :
  ∀ (a : IsLocalHom (R := R) (S := S) f),
    (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)
tfae_2_to_4 :
  ∀ (a : (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)),
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
tfae_3_iff_4 :
  LE.le (α := Ideal S) (Ideal.map f (maximalIdeal R)) (maximalIdeal S) ↔
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
tfae_4_to_1 :
  ∀ (a : LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))), IsLocalHom (R := R) (S := S) f
h : IsLocalHom (R := R) (S := S) f
x : R
⊢ Membership.mem (γ := Ideal R) (Ideal.comap f (maximalIdeal S)) x ↔ Membership.mem (γ := Ideal R) (maximalIdeal R) x

Tactic:
exact not_iff_not.2 (isUnit_map_iff f _)

Premises used: not_iff_not, Iff.mpr, isUnit_map_iff
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
tfae_1_to_2 :
  ∀ (a : IsLocalHom (R := R) (S := S) f),
    (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)
tfae_2_to_4 :
  ∀ (a : (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)),
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
tfae_3_iff_4 :
  LE.le (α := Ideal S) (Ideal.map f (maximalIdeal R)) (maximalIdeal S) ↔
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
tfae_4_to_1 :
  ∀ (a : LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))), IsLocalHom (R := R) (S := S) f
⊢ ∀ (a : IsLocalHom (R := R) (S := S) f), Eq (α := Ideal R) (Ideal.comap f (maximalIdeal S)) (maximalIdeal R)

Tactic:
tfae_have 1 → 5
  | _ => by ext; exact not_iff_not.2 (isUnit_map_iff f _)
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
tfae_1_to_2 :
  ∀ (a : IsLocalHom (R := R) (S := S) f),
    (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)
tfae_2_to_4 :
  ∀ (a : (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)),
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
tfae_3_iff_4 :
  LE.le (α := Ideal S) (Ideal.map f (maximalIdeal R)) (maximalIdeal S) ↔
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
tfae_4_to_1 :
  ∀ (a : LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))), IsLocalHom (R := R) (S := S) f
tfae_1_to_5 :
  ∀ (a : IsLocalHom (R := R) (S := S) f), Eq (α := Ideal R) (Ideal.comap f (maximalIdeal S)) (maximalIdeal R)
⊢ Eq (α := Ideal R) (Ideal.comap f (maximalIdeal S)) (maximalIdeal R)

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
tfae_1_to_2 :
  ∀ (a : IsLocalHom (R := R) (S := S) f),
    (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)
tfae_2_to_4 :
  ∀ (a : (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)),
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
tfae_3_iff_4 :
  LE.le (α := Ideal S) (Ideal.map f (maximalIdeal R)) (maximalIdeal S) ↔
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
tfae_4_to_1 :
  ∀ (a : LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))), IsLocalHom (R := R) (S := S) f
tfae_1_to_5 :
  ∀ (a : IsLocalHom (R := R) (S := S) f), Eq (α := Ideal R) (Ideal.comap f (maximalIdeal S)) (maximalIdeal R)
⊢ LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : CommSemiring S
inst_3 : IsLocalRing S
f : R →+* S
tfae_1_to_2 :
  ∀ (a : IsLocalHom (R := R) (S := S) f),
    (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)
tfae_2_to_4 :
  ∀ (a : (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S)),
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
tfae_3_iff_4 :
  LE.le (α := Ideal S) (Ideal.map f (maximalIdeal R)) (maximalIdeal S) ↔
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
tfae_4_to_1 :
  ∀ (a : LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))), IsLocalHom (R := R) (S := S) f
tfae_1_to_5 :
  ∀ (a : IsLocalHom (R := R) (S := S) f), Eq (α := Ideal R) (Ideal.comap f (maximalIdeal S)) (maximalIdeal R)
⊢ ∀ (a : Eq (α := Ideal R) (Ideal.comap f (maximalIdeal S)) (maximalIdeal R)),
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))

Tactic:
5 → 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false