awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
tfae_have 5 → 4 := fun h ↦ le_of_eq h.symm

Premises used: le_of_eq
-- 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)
tfae_5_to_4 :
  ∀ (a : Eq (α := Ideal R) (Ideal.comap f (maximalIdeal S)) (maximalIdeal R)),
    LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
⊢ [IsLocalHom (R := R) (S := S) f, (⇑f : (a : R) → S) '' (↑(maximalIdeal R) : Set R) ⊆ (↑(maximalIdeal S) : Set S),
      LE.le (α := Ideal S) (Ideal.map f (maximalIdeal R)) (maximalIdeal S),
      LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S)),
      Eq (α := Ideal R) (Ideal.comap f (maximalIdeal S)) (maximalIdeal R)].TFAE

Tactic:
tfae_finish
-- 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
⊢ Eq (α := Ideal R) (Ideal.comap f (maximalIdeal S)) (maximalIdeal R)

Tactic:
((local_hom_TFAE _).out 0 4).mp ‹_›

Premises used: List.TFAE.out, Iff.mp, OfNat.ofNat, IsLocalRing.local_hom_TFAE
-- 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
rw : LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
rw₁ rw₂ : LE.le (α := Ideal R) (maximalIdeal R) (maximalIdeal R)
⊢ LE.le (α := Ideal S) (Ideal.map f (maximalIdeal R)) (maximalIdeal S)

Tactic:
rw [Ideal.map_le_iff_le_comap, IsLocalRing.maximalIdeal_comap]

Premises used: Ideal.map_le_iff_le_comap, IsLocalRing.maximalIdeal_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
inst_4 : IsLocalHom (R := R) (S := S) f
⊢ LT.lt.{u_2} (α := Ideal S) (Ideal.map f (maximalIdeal R)) ⊤

Tactic:
(map_maximalIdeal_le f).trans_lt (maximalIdeal.isMaximal S).lt_top

Premises used: IsLocalRing.map_maximalIdeal_le, IsLocalRing.maximalIdeal.isMaximal, Ideal.IsMaximal.lt_top, LE.le.trans_lt
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : Semiring S
inst_3 : Nontrivial S
f : R →+* S
inst_4 : IsLocalHom (R := R) (S := S) f
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
a b : S
hab : IsUnit (a + b)
obtain :
  ∀ (a : R) (hab : IsUnit (HAdd.hAdd (α := S) ((f : (a : R) → S) a : S) b)),
    IsUnit.{u_2} (M := S) ((f : (a : R) → S) a : S) ∨ IsUnit b
⊢ IsUnit a ∨ IsUnit b

Tactic:
obtain ⟨a, rfl⟩ := hf a

Premises used: rfl
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : Semiring S
inst_3 : Nontrivial S
f : R →+* S
inst_4 : IsLocalHom (R := R) (S := S) f
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
b : S
a : R
hab : IsUnit (HAdd.hAdd (α := S) ((f : (a : R) → S) a : S) b)
obtain :
  ∀ (b : R) (hab : IsUnit (HAdd.hAdd (α := S) (β := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) b : S))),
    IsUnit.{u_2} (M := S) ((f : (a : R) → S) a : S) ∨ IsUnit.{u_2} (M := S) ((f : (a : R) → S) b : S)
⊢ IsUnit.{u_2} (M := S) ((f : (a : R) → S) a : S) ∨ IsUnit b

Tactic:
obtain ⟨b, rfl⟩ := hf b

Premises used: rfl
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : Semiring S
inst_3 : Nontrivial S
f : R →+* S
inst_4 : IsLocalHom (R := R) (S := S) f
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
a b : R
hab : IsUnit (HAdd.hAdd (α := S) (β := S) ((f : (a : R) → S) a : S) ((f : (a : R) → S) b : S))
⊢ IsUnit.{u_2} (M := S) ((f : (a : R) → S) (a + b) : S)

Tactic:
rw [← map_add] at hab

Premises used: map_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 : Semiring S
inst_3 : Nontrivial S
f : R →+* S
inst_4 : IsLocalHom (R := R) (S := S) f
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
a b : R
hab : IsUnit.{u_2} (M := S) ((f : (a : R) → S) (a + b) : S)
⊢ IsUnit.{u_2} (M := S) ((f : (a : R) → S) a : S) ∨ IsUnit.{u_2} (M := S) ((f : (a : R) → S) b : S)

Tactic:
(isUnit_or_isUnit_of_isUnit_add <| IsLocalHom.map_nonunit _ hab).imp f.isUnit_map
        f.isUnit_map

Premises used: IsLocalHom.map_nonunit, IsLocalRing.isUnit_or_isUnit_of_isUnit_add, RingHom.isUnit_map, Or.imp
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : IsLocalRing R
inst_2 : Semiring S
inst_3 : Nontrivial S
f : R →+* S
inst_4 : IsLocalHom (R := R) (S := S) f
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
a b : R
hab : IsUnit.{u_2} (M := S) ((f : (a : R) → S) (a + b) : S)
⊢ IsUnit.{u_2} (M := S) ((f : (a : R) → S) a : S) ∨ IsUnit.{u_2} (M := S) ((f : (a : R) → S) b : S)

Tactic:
exact
      (isUnit_or_isUnit_of_isUnit_add <| IsLocalHom.map_nonunit _ hab).imp f.isUnit_map
        f.isUnit_map

Premises used: IsLocalHom.map_nonunit, IsLocalRing.isUnit_or_isUnit_of_isUnit_add, RingHom.isUnit_map, Or.imp
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Nontrivial S
inst_3 : IsLocalRing R
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ IsLocalRing S

Tactic:
have := IsLocalRing.of_surjective' f ‹_›
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Nontrivial S
inst_3 : IsLocalRing R
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
this : IsLocalRing S
⊢ IsLocalHom (R := R) (S := S) f

Tactic:
((local_hom_TFAE f).out 3 0).mp ?_

Premises used: List.TFAE.out, Iff.mp, OfNat.ofNat, IsLocalRing.local_hom_TFAE
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Nontrivial S
inst_3 : IsLocalRing R
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
this : IsLocalRing S
refine : LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
⊢ IsLocalHom (R := R) (S := S) f

Tactic:
refine ((local_hom_TFAE f).out 3 0).mp ?_

Premises used: List.TFAE.out, Iff.mp, OfNat.ofNat, IsLocalRing.local_hom_TFAE
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Nontrivial S
inst_3 : IsLocalRing R
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
this : IsLocalRing S
⊢ Ideal.IsMaximal (Ideal.comap f (maximalIdeal S))

Tactic:
have := Ideal.comap_isMaximal_of_surjective f hf (K := maximalIdeal S)
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Nontrivial S
inst_3 : IsLocalRing R
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
this_1 : IsLocalRing S
this : Ideal.IsMaximal (Ideal.comap f (maximalIdeal S))
⊢ LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))

Tactic:
((maximal_ideal_unique R).unique (inferInstanceAs (maximalIdeal R).IsMaximal) this).le

Premises used: IsLocalRing.maximal_ideal_unique, Set.Mem, Eq.le, ExistsUnique.unique
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Nontrivial S
inst_3 : IsLocalRing R
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
this_1 : IsLocalRing S
this : Ideal.IsMaximal (Ideal.comap f (maximalIdeal S))
⊢ LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))

Tactic:
exact ((maximal_ideal_unique R).unique (inferInstanceAs (maximalIdeal R).IsMaximal) this).le

Premises used: IsLocalRing.maximal_ideal_unique, Eq.le, ExistsUnique.unique
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : IsLocalHom (R := R) (S := S) f
a : Sˣ
obtain :
  ∀ (b : R) (hb : (f : (a : R) → S) b = (↑a : S)), ∃ (a_1 : Rˣ), (Units.map (↑f : R →* S) : (a : Rˣ) → Sˣ) a_1 = a
⊢ ∃ (a_1 : Rˣ), (Units.map (↑f : R →* S) : (a : Rˣ) → Sˣ) a_1 = a

Tactic:
obtain ⟨b, hb⟩ := hf (a : S)

Premises used: Units.val
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : IsLocalHom (R := R) (S := S) f
a : Sˣ
b : R
hb : (f : (a : R) → S) b = (↑a : S)
rw : IsUnit (↑a : S)
⊢ IsUnit.{u_2} (M := S) ((f : (a : R) → S) b : S)

Tactic:
rw [hb]
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : IsLocalHom (R := R) (S := S) f
a : Sˣ
b : R
hb : (f : (a : R) → S) b = (↑a : S)
⊢ IsUnit (↑a : S)

Tactic:
Units.isUnit _

Premises used: Units.isUnit
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : IsLocalHom (R := R) (S := S) f
a : Sˣ
b : R
hb : (f : (a : R) → S) b = (↑a : S)
⊢ IsUnit (↑a : S)

Tactic:
exact Units.isUnit _

Premises used: Units.isUnit
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : IsLocalHom (R := R) (S := S) f
a : Sˣ
b : R
hb : (f : (a : R) → S) b = (↑a : S)
h₁ : (Units.map (↑f : R →* S) : (a : Rˣ) → Sˣ) (IsUnit.unit ⋯) = a
⊢ ∃ (a_1 : Rˣ), (Units.map (↑f : R →* S) : (a : Rˣ) → Sˣ) a_1 = a

Tactic:
use (isUnit_of_map_unit f b (by rw [hb]; exact Units.isUnit _)).unit

Premises used: isUnit_of_map_unit, IsUnit.unit
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : IsLocalHom (R := R) (S := S) f
a : Sˣ
b : R
hb : (f : (a : R) → S) b = (↑a : S)
h₁ : (↑((Units.map (↑f : R →* S) : (a : Rˣ) → Sˣ) (IsUnit.unit ⋯)) : S) = (↑a : S)
⊢ (Units.map (↑f : R →* S) : (a : Rˣ) → Sˣ) (IsUnit.unit ⋯) = a

Tactic:
ext
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : IsLocalHom (R := R) (S := S) f
a : Sˣ
b : R
hb : (f : (a : R) → S) b = (↑a : S)
⊢ (↑((Units.map (↑f : R →* S) : (a : Rˣ) → Sˣ) (IsUnit.unit ⋯)) : S) = (↑a : S)

Tactic:
hb
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : IsLocalHom (R := R) (S := S) f
a : Sˣ
b : R
hb : (f : (a : R) → S) b = (↑a : S)
⊢ (↑((Units.map (↑f : R →* S) : (a : Rˣ) → Sˣ) (IsUnit.unit ⋯)) : S) = (↑a : S)

Tactic:
exact hb
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R_1 : Type u_1
S : Type u_2
T : Type u_3
K : Type u_4
R : Type u_5
inst : DivisionRing K
inst_1 : CommRing R
inst_2 : Nontrivial R
f : K →+* R
r : K
hr : IsUnit.{u_5} (M := R) ((f : (a : K) → R) r : R)
⊢ IsUnit r

Tactic:
simpa only [isUnit_iff_ne_zero, ne_eq, map_eq_zero] using hr.ne_zero

Premises used: map_eq_zero, isUnit_iff_ne_zero, ne_eq, IsUnit.ne_zero
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsLocalRing R
inst_3 : IsLocalRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
this : IsLocalHom (R := R) (S := S) f := ⋯
rw : Eq (α := Ideal S) (Ideal.map f (Ideal.comap f (maximalIdeal S))) (maximalIdeal S)
rw₁ rw₂ : Eq (α := Ideal S) (maximalIdeal S) (maximalIdeal S)
⊢ Eq (α := Ideal S) (Ideal.map f (maximalIdeal R)) (maximalIdeal S)

Tactic:
rw [← maximalIdeal_comap f, Ideal.map_comap_of_surjective f hf]

Premises used: IsLocalRing.maximalIdeal_comap, Ideal.map_comap_of_surjective
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsLocalRing R
inst_3 : IsLocalRing S
e : R ≃+* S
⊢ Eq (α := Ideal S) (Ideal.map e (maximalIdeal R)) (maximalIdeal S)

Tactic:
map_maximalIdeal_of_surjective (e : R →+* S) e.surjective

Premises used: RingEquiv.surjective, Ideal.map, RingHomClass.toRingHom, IsLocalRing.map_maximalIdeal_of_surjective
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
A : Type u_4
B : Type u_5
inst : CommSemiring A
inst_1 : IsLocalRing A
inst_2 : Semiring B
e : A ≃+* B
⊢ IsLocalRing B

Tactic:
haveI := e.symm.toEquiv.nontrivial
  IsLocalRing.of_surjective (e : A →+* B) e.surjective

Premises used: RingEquiv.surjective, IsLocalRing.of_surjective, RingHomClass.toRingHom
-- Module: Mathlib.RingTheory.LocalRing.RingHom.Basic
Goal:
R_1 : Type u_1
S : Type u_2
T : Type u_3
R : Type u_4
inst : CommRing R
inst_1 : IsLocalRing R
n : ℕ
inst_2 : Nontrivial (ZMod n)
f : R →+* ZMod n
⊢ IsLocalHom (R := R) (S := ZMod n) f

Tactic:
(ZMod.ringHom_surjective f).isLocalHom

Premises used: ZMod.ringHom_surjective, Function.Surjective.isLocalHom
-- Module: Mathlib.RingTheory.LocalRing.Subring
Goal:
R : Type u_2
S : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : IsLocalRing S
f : R →+* S
hf : Function.Injective.{u_2 + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : ∀ (a : R), Membership.mem (γ := Submonoid R) R⁰ a → IsUnit a
⊢ Nontrivial R

Tactic:
haveI : Nontrivial R := f.domain_nontrivial
-- Module: Mathlib.RingTheory.LocalRing.Subring
Goal:
R : Type u_2
S : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : IsLocalRing S
f : R →+* S
hf : Function.Injective.{u_2 + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : ∀ (a : R), Membership.mem (γ := Submonoid R) R⁰ a → IsUnit a
this : Nontrivial R
⊢ IsLocalRing R

Tactic:
.of_is_unit_or_is_unit_of_add_one fun {a b} hab ↦
    (IsLocalRing.isUnit_or_isUnit_of_add_one (map_add f .. ▸ map_one f ▸ congrArg f hab)).imp ?_ ?_

Premises used: IsLocalRing.isUnit_or_isUnit_of_add_one, IsLocalRing.of_is_unit_or_is_unit_of_add_one, Or.imp
-- Module: Mathlib.RingTheory.LocalRing.Subring
Goal:
R : Type u_2
S : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : IsLocalRing S
f : R →+* S
hf : Function.Injective.{u_2 + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : ∀ (a : R), Membership.mem (γ := Submonoid R) R⁰ a → IsUnit a
this : Nontrivial R
refine_1 : ∀ {a b : R} (hab : a + b = 1), IsUnit.{u_1} (M := S) ((f : (a : R) → S) a : S) → IsUnit a
refine_2 : ∀ {a b : R} (hab : a + b = 1), IsUnit.{u_1} (M := S) ((f : (a : R) → S) b : S) → IsUnit b
⊢ IsLocalRing R

Tactic:
refine .of_is_unit_or_is_unit_of_add_one fun {a b} hab ↦
    (IsLocalRing.isUnit_or_isUnit_of_add_one (map_add f .. ▸ map_one f ▸ congrArg f hab)).imp ?_ ?_
-- Module: Mathlib.RingTheory.LocalRing.Subring
Goal:
R : Type u_2
S : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : IsLocalRing S
f : R →+* S
hf : Function.Injective.{u_2 + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : ∀ (a : R), Membership.mem (γ := Submonoid R) R⁰ a → IsUnit a
this : Nontrivial R
a b : R
hab : a + b = 1
⊢ IsUnit.{u_1} (M := S) ((f : (a : R) → S) a : S) → IsUnit a

Tactic:
h _ ∘ mem_nonZeroDivisors_of_injective hf ∘ IsUnit.mem_nonZeroDivisors

Premises used: Function.comp, IsUnit.mem_nonZeroDivisors, mem_nonZeroDivisors_of_injective
-- Module: Mathlib.RingTheory.LocalRing.Subring
Goal:
R : Type u_2
S : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : IsLocalRing S
f : R →+* S
hf : Function.Injective.{u_2 + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : ∀ (a : R), Membership.mem (γ := Submonoid R) R⁰ a → IsUnit a
this : Nontrivial R
a b : R
hab : a + b = 1
⊢ IsUnit.{u_1} (M := S) ((f : (a : R) → S) a : S) → IsUnit a

Tactic:
exact h _ ∘ mem_nonZeroDivisors_of_injective hf ∘ IsUnit.mem_nonZeroDivisors

Premises used: IsUnit.mem_nonZeroDivisors, mem_nonZeroDivisors_of_injective
-- Module: Mathlib.RingTheory.LocalRing.Subring
Goal:
R : Type u_2
S : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : IsLocalRing S
f : R →+* S
hf : Function.Injective.{u_2 + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : ∀ (a : R), Membership.mem (γ := Submonoid R) R⁰ a → IsUnit a
this : Nontrivial R
a b : R
hab : a + b = 1
⊢ IsUnit.{u_1} (M := S) ((f : (a : R) → S) b : S) → IsUnit b

Tactic:
h _ ∘ mem_nonZeroDivisors_of_injective hf ∘ IsUnit.mem_nonZeroDivisors

Premises used: Function.comp, IsUnit.mem_nonZeroDivisors, mem_nonZeroDivisors_of_injective
-- Module: Mathlib.RingTheory.LocalRing.Subring
Goal:
R : Type u_2
S : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : IsLocalRing S
f : R →+* S
hf : Function.Injective.{u_2 + 1, u_1 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
h : ∀ (a : R), Membership.mem (γ := Submonoid R) R⁰ a → IsUnit a
this : Nontrivial R
a b : R
hab : a + b = 1
⊢ IsUnit.{u_1} (M := S) ((f : (a : R) → S) b : S) → IsUnit b

Tactic:
exact h _ ∘ mem_nonZeroDivisors_of_injective hf ∘ IsUnit.mem_nonZeroDivisors

Premises used: IsUnit.mem_nonZeroDivisors, mem_nonZeroDivisors_of_injective
-- Module: Mathlib.RingTheory.LocalRing.Subring
Goal:
S : Type u_1
inst : Semiring S
inst_1 : IsLocalRing S
R : Subsemiring S
h : ∀ (a : ↥R), Membership.mem (γ := Submonoid ↥R) (↥R)⁰ a → IsUnit a
⊢ IsLocalRing.{u_1} ↥R

Tactic:
of_injective R.subtype_injective h

Premises used: IsLocalRing.of_injective, Subsemiring.subtype_injective
-- Module: Mathlib.RingTheory.LocalRing.Subring
Goal:
S : Type u_1
inst : Semiring S
R R' : Subsemiring S
inst_1 : IsLocalRing.{u_1} ↥R'
inc : R ≤ R'
h : ∀ (a : ↥R), Membership.mem (γ := Submonoid ↥R) (↥R)⁰ a → IsUnit a
⊢ IsLocalRing.{u_1} ↥R

Tactic:
of_injective (Subsemiring.inclusion_injective inc) h

Premises used: Subsemiring.inclusion_injective, IsLocalRing.of_injective
-- Module: Mathlib.RingTheory.Localization.Algebra
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring P
inst_3 : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst_4 : Algebra R S
inst_5 : Algebra P Q
inst_6 : IsLocalization M S
inst_7 : IsLocalization T Q
g : R →+* P
I : Ideal R
x : ↥M
a b : ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)
e :
  Eq (α := ↥(Ideal.map (F := R →+* S) (algebraMap R S) I))
    ((((algebraMap R (Module.End R ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)) :
                (a : R) → Module.End R ↥(Ideal.map (algebraMap R S) I))
              (↑x : R) :
            Module.End R ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)) :
          (a : ↥(Ideal.map (algebraMap R S) I)) → ↥(Ideal.map (algebraMap R S) I))
        a :
      ↥(Ideal.map (F := R →+* S) (algebraMap R S) I))
    ((((algebraMap R (Module.End R ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)) :
                (a : R) → Module.End R ↥(Ideal.map (algebraMap R S) I))
              (↑x : R) :
            Module.End R ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)) :
          (a : ↥(Ideal.map (algebraMap R S) I)) → ↥(Ideal.map (algebraMap R S) I))
        b :
      ↥(Ideal.map (F := R →+* S) (algebraMap R S) I))
⊢ Eq.{u_2 + 1} (α := S)
    ((fun (x_1 : S) ↦ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑x : R) : S) x_1) (↑a : S))
    ((fun (x_1 : S) ↦ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑x : R) : S) x_1) (↑b : S))

Tactic:
simpa [Algebra.smul_def] using congr(($e).1)

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.Localization.Algebra
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring P
inst_3 : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst_4 : Algebra R S
inst_5 : Algebra P Q
inst_6 : IsLocalization M S
inst_7 : IsLocalization T Q
g : R →+* P
I : Ideal R
x : ↥M
a : ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)
⊢ (↑((((algebraMap R (Module.End R ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)) :
                  (a : R) → Module.End R ↥(Ideal.map (algebraMap R S) I))
                (↑x : R) :
              Module.End R ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)) :
            (a : ↥(Ideal.map (algebraMap R S) I)) → ↥(Ideal.map (algebraMap R S) I))
          (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) x)
            ((↑(IsUnit.unit (a := (algebraMap R S : (a : R) → S) (↑x : R)) ⋯)⁻¹ : S) * (↑a : S)) ⋯)) :
      S) =
    (↑a : S)

Tactic:
simp [Algebra.smul_def, ← mul_assoc]

Premises used: mul_assoc, Algebra.smul_def
-- Module: Mathlib.RingTheory.Localization.Algebra
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring P
inst_3 : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst_4 : Algebra R S
inst_5 : Algebra P Q
inst_6 : IsLocalization M S
inst_7 : IsLocalization T Q
g : R →+* P
I : Ideal R
y : ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)
x : ↥I × ↥M
hx :
  HMul.hMul (β := S) (↑y : S) ((algebraMap R S : (a : R) → S) (↑x.2 : R) : S) =
    (algebraMap R S : (a : R) → S) (↑x.1 : R)
⊢ (↑(x.2 • y) : S) =
    (↑(((idealMap S I :
              LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id R) ↥I ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)) :
            (a : ↥I) → ↥(Ideal.map (algebraMap R S) I))
          x.1) :
      S)

Tactic:
simp [Submonoid.smul_def, Algebra.smul_def, mul_comm, hx]

Premises used: Submonoid.smul_def, mul_comm, Algebra.smul_def