awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.RingHom.Basic (hypothesis)
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))
⊢ [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
have 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))
Tactic: tfae_have 3 ↔ 4 := Ideal.map_le_iff_le_comap
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.RingHom.Basic (hypothesis)
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, (⇑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
have tfae_4_to_1 : ∀ (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)⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.RingHom.Basic (goal)
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
⊢ Eq (α := Ideal R) (Ideal.comap f (maximalIdeal S)) (maximalIdeal R)
have h : ∀ (x : R),
  Membership.mem (γ := Ideal R) (Ideal.comap f (maximalIdeal S)) x ↔ Membership.mem (γ := Ideal R) (maximalIdeal R) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.RingHom.Basic (hypothesis)
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, (⇑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
have tfae_1_to_5 : ∀ (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 _)
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.RingHom.Basic (hypothesis)
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)
⊢ [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
have 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))
Tactic: tfae_have 5 → 4 := fun h ↦ le_of_eq h.symm
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.RingHom.Basic (goal)
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
⊢ LE.le (α := Ideal S) (Ideal.map f (maximalIdeal R)) (maximalIdeal S)
have rw : LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
Tactic: rw [Ideal.map_le_iff_le_comap, IsLocalRing.maximalIdeal_comap]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.RingHom.Basic (goal)
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))
⊢ LE.le (α := Ideal S) (Ideal.map f (maximalIdeal R)) (maximalIdeal S)
have rw₁ : LE.le (α := Ideal R) (maximalIdeal R) (maximalIdeal R)
Tactic: rw [Ideal.map_le_iff_le_comap, IsLocalRing.maximalIdeal_comap]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.RingHom.Basic (goal)
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)
⊢ IsUnit a ∨ IsUnit b
have 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
Tactic: obtain ⟨a, rfl⟩ := hf a
Cleared hypotheses: a, hab
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.RingHom.Basic (goal)
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)
⊢ IsUnit.{u_2} (M := S) ((f : (a : R) → S) a : S) ∨ IsUnit b
have 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)
Tactic: obtain ⟨b, rfl⟩ := hf b
Cleared hypotheses: b, hab
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.RingHom.Basic (hypothesis)
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 : S) ∨ IsUnit.{u_2} (M := S) ((f : (a : R) → S) b : S)
have hab₁ : IsUnit.{u_2} (M := S) ((f : (a : R) → S) (a + b) : S)
Tactic: rw [← map_add] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.RingHom.Basic (hypothesis)
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)
⊢ IsLocalHom (R := R) (S := S) f
have this : IsLocalRing S
Tactic: have := IsLocalRing.of_surjective' f ‹_›
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.RingHom.Basic (goal)
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
have refine : LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
Tactic: refine ((local_hom_TFAE f).out 3 0).mp ?_
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.RingHom.Basic (hypothesis)
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
⊢ LE.le (α := Ideal R) (maximalIdeal R) (Ideal.comap f (maximalIdeal S))
have this₁ : Ideal.IsMaximal (Ideal.comap f (maximalIdeal S))
Tactic: have := Ideal.comap_isMaximal_of_surjective f hf (K := maximalIdeal S)
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.RingHom.Basic (goal)
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ˣ
⊢ ∃ (a_1 : Rˣ), (Units.map (↑f : R →* S) : (a : Rˣ) → Sˣ) a_1 = a
have 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
Tactic: obtain ⟨b, hb⟩ := hf (a : S)
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.RingHom.Basic (goal)
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.{u_2} (M := S) ((f : (a : R) → S) b : S)
have rw : IsUnit (↑a : S)
Tactic: rw [hb]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.RingHom.Basic (goal)
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)
⊢ ∃ (a_1 : Rˣ), (Units.map (↑f : R →* S) : (a : Rˣ) → Sˣ) a_1 = a
have h₁ : (Units.map (↑f : R →* S) : (a : Rˣ) → Sˣ) (IsUnit.unit sorry) = a
Tactic: use (isUnit_of_map_unit f b (by rw [hb]; exact Units.isUnit _)).unit
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.RingHom.Basic (goal)
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 ⋯) = a
have h₁ : (↑((Units.map (↑f : R →* S) : (a : Rˣ) → Sˣ) (IsUnit.unit sorry)) : S) = (↑a : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.RingHom.Basic (goal)
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 := ⋯
⊢ Eq (α := Ideal S) (Ideal.map f (maximalIdeal R)) (maximalIdeal S)
have rw : Eq (α := Ideal S) (Ideal.map f (Ideal.comap f (maximalIdeal S))) (maximalIdeal S)
Tactic: rw [← maximalIdeal_comap f, Ideal.map_comap_of_surjective f hf]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.RingHom.Basic (goal)
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)
⊢ Eq (α := Ideal S) (Ideal.map f (maximalIdeal R)) (maximalIdeal S)
have rw₁ : Eq (α := Ideal S) (maximalIdeal S) (maximalIdeal S)
Tactic: rw [← maximalIdeal_comap f, Ideal.map_comap_of_surjective f hf]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Subring (hypothesis)
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
⊢ IsLocalRing R
have this : Nontrivial R
Tactic: haveI : Nontrivial R := f.domain_nontrivial
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Subring (goal)
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
have refine_1 : ∀ {a b : R} (hab : a + b = 1), IsUnit.{u_1} (M := S) ((f : (a : R) → S) a : S) → IsUnit a
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 ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Subring (goal)
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
⊢ IsLocalRing R
have refine_2 : ∀ {a b : R} (hab : a + b = 1), IsUnit.{u_1} (M := S) ((f : (a : R) → S) b : S) → IsUnit b
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 ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Algebra (goal)
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
hT : Submonoid.map g M = T
⊢ Eq (α := Ideal S) (RingHom.ker (F := S →+* Q) (map (M := M) (T := T) Q g ⋯))
    (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker g))
have h : ∀ (x : S),
  Membership.mem (γ := Ideal S) (RingHom.ker (F := S →+* Q) (map (M := M) (T := T) Q g sorry)) x ↔
    Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker g)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Algebra (goal)
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
hT : Submonoid.map g M = T
x : S
⊢ Membership.mem (γ := Ideal S) (RingHom.ker (F := S →+* Q) (map (M := M) (T := T) Q g ⋯)) x ↔
    Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker g)) x
have h : ∀ (x : R) (s : ↥M),
  Membership.mem (γ := Ideal S) (RingHom.ker (F := S →+* Q) (map (M := M) (T := T) Q g sorry)) (mk' S x s) ↔
    Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker g)) (mk' S x s)
Tactic: obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq M x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Algebra (goal)
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
hT : Submonoid.map g M = T
e : ↥(Ideal.map (F := R →+* S) (algebraMap R S) (ker g)) ≃ₛₗ[id S]
  ↥(ker (F := S →+* Q) (IsLocalization.map (M := M) (T := T) Q g ⋯)) :=
  LinearEquiv.ofEq (Ideal.map (F := R →+* S) (algebraMap R S) (ker g))
    (ker (F := S →+* Q) (IsLocalization.map (M := M) (T := T) Q g ⋯)) ⋯
⊢ IsLocalizedModule (M' := ↥(ker (F := S →+* Q) (IsLocalization.map (M := M) (T := T) Q g ⋯))) M
    (toKerIsLocalization S Q g ⋯)
have convert_to : IsLocalizedModule M
  ((↑(LinearEquiv.restrictScalars R e) :
      ↥(Ideal.map (algebraMap R S) (ker g)) →ₛₗ[id R] ↥(ker (IsLocalization.map Q g sorry))) ∘ₗ
    Algebra.idealMap S (ker g))
Tactic: convert_to IsLocalizedModule M ((e.restrictScalars R).toLinearMap ∘ₗ
    Algebra.idealMap S (RingHom.ker g))
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Algebra (goal)
Goal:
R_1 : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S
inst_2 : CommSemiring P
inst_3 : CommSemiring Q
M_1 : Submonoid R_1
T : Submonoid P
inst_4 : Algebra R_1 S
inst_5 : Algebra P Q
inst_6 : IsLocalization M_1 S
inst_7 : IsLocalization T Q
g : R_1 →+* P
R : Type u_5
inst_8 : CommSemiring R
M : Submonoid R
A : Type u_6
inst_9 : CommSemiring A
inst_10 : Algebra R A
B : Type u_7
inst_11 : CommSemiring B
inst_12 : Algebra R B
Rₚ : Type u_8
inst_13 : CommSemiring Rₚ
inst_14 : Algebra R Rₚ
inst_15 : IsLocalization M Rₚ
Aₚ : Type u_9
inst_16 : CommSemiring Aₚ
inst_17 : Algebra R Aₚ
inst_18 : Algebra A Aₚ
inst_19 : IsScalarTower R A Aₚ
inst_20 : IsLocalization (algebraMapSubmonoid A M) Aₚ
Bₚ : Type u_10
inst_21 : CommSemiring Bₚ
inst_22 : Algebra R Bₚ
inst_23 : Algebra B Bₚ
inst_24 : IsScalarTower R B Bₚ
inst_25 : IsLocalization (algebraMapSubmonoid B M) Bₚ
inst_26 : Algebra Rₚ Aₚ
inst_27 : Algebra Rₚ Bₚ
inst_28 : IsScalarTower R Rₚ Aₚ
inst_29 : IsScalarTower R Rₚ Bₚ
f : A →ₐ[R] B
r : Rₚ
⊢ OneHom.toFun.{u_9, u_10} (M := Aₚ) ((↑(↑(map Bₚ f.toRingHom ⋯) : Aₚ →* Bₚ) : OneHom Aₚ Bₚ) : OneHom Aₚ Bₚ)
      ((algebraMap Rₚ Aₚ : (a : Rₚ) → Aₚ) r : Aₚ) =
    (algebraMap Rₚ Bₚ : (a : Rₚ) → Bₚ) r
have obtain : ∀ (a : R) (m : ↥M),
  OneHom.toFun.{u_9, u_10} (M := Aₚ) ((↑(↑(map Bₚ f.toRingHom sorry) : Aₚ →* Bₚ) : OneHom Aₚ Bₚ) : OneHom Aₚ Bₚ)
      ((algebraMap Rₚ Aₚ : (a : Rₚ) → Aₚ) (mk' Rₚ a m) : Aₚ) =
    (algebraMap Rₚ Bₚ : (a : Rₚ) → Bₚ) (mk' Rₚ a m)
Tactic: obtain ⟨a, m, rfl⟩ := IsLocalization.exists_mk'_eq M r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Algebra (goal)
Goal:
R : Type u_5
inst : CommSemiring R
M : Submonoid R
A : Type u_6
inst_1 : CommSemiring A
inst_2 : Algebra R A
B : Type u_7
inst_3 : CommSemiring B
inst_4 : Algebra R B
Rₚ : Type u_8
inst_5 : CommSemiring Rₚ
inst_6 : Algebra R Rₚ
inst_7 : IsLocalization M Rₚ
Aₚ : Type u_9
inst_8 : CommSemiring Aₚ
inst_9 : Algebra R Aₚ
inst_10 : Algebra A Aₚ
inst_11 : IsScalarTower R A Aₚ
inst_12 : IsLocalization (algebraMapSubmonoid A M) Aₚ
Bₚ : Type u_10
inst_13 : CommSemiring Bₚ
inst_14 : Algebra R Bₚ
inst_15 : Algebra B Bₚ
inst_16 : IsScalarTower R B Bₚ
inst_17 : IsLocalization (algebraMapSubmonoid B M) Bₚ
inst_18 : Algebra Rₚ Aₚ
inst_19 : Algebra Rₚ Bₚ
inst_20 : IsScalarTower R Rₚ Aₚ
inst_21 : IsScalarTower R Rₚ Bₚ
f : A →ₐ[R] B
⊢ Eq (α := Aₚ →ₗ[Rₚ] Bₚ)
    (((IsLocalizedModule.mapExtendScalars M (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₚ))
              (AlgHom.toLinearMap (IsScalarTower.toAlgHom R B Bₚ)) Rₚ :
            (A →ₗ[R] B) →ₗ[R] Aₚ →ₗ[Rₚ] Bₚ) :
          (a : A →ₗ[R] B) → Aₚ →ₗ[Rₚ] Bₚ)
        f.toLinearMap :
      Aₚ →ₗ[Rₚ] Bₚ)
    (AlgHom.toLinearMap (mapₐ M Rₚ Aₚ Bₚ f) : Aₚ →ₗ[Rₚ] Bₚ)
have refine : Eq (α := Aₚ →ₗ[R] Bₚ)
  ((↑R :
      {S : Type u_8} →
        {M : Type u_9} →
          {M₂ : Type u_10} →
            [inst : Semiring R] →
              [inst_22 : Semiring S] →
                [inst_23 : AddCommMonoid M] →
                  [inst_24 : AddCommMonoid M₂] →
                    [inst_25 : Module R M] →
                      [inst_26 : Module R M₂] →
                        [inst_27 : Module S M] →
                          [inst_28 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    (S := Rₚ)
    (((IsLocalizedModule.mapExtendScalars M (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₚ))
            (AlgHom.toLinearMap (IsScalarTower.toAlgHom R B Bₚ)) Rₚ :
          (A →ₗ[R] B) →ₗ[R] Aₚ →ₗ[Rₚ] Bₚ) :
        (a : A →ₗ[R] B) → Aₚ →ₗ[Rₚ] Bₚ)
      f.toLinearMap))
  ((↑R :
      {S : Type u_8} →
        {M : Type u_9} →
          {M₂ : Type u_10} →
            [inst : Semiring R] →
              [inst_22 : Semiring S] →
                [inst_23 : AddCommMonoid M] →
                  [inst_24 : AddCommMonoid M₂] →
                    [inst_25 : Module R M] →
                      [inst_26 : Module R M₂] →
                        [inst_27 : Module S M] →
                          [inst_28 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
    (AlgHom.toLinearMap (mapₐ M Rₚ Aₚ Bₚ f)))
Tactic: refine LinearMap.restrictScalars_injective R ?_