awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
s : Multiset α
hs : 0 ∉ s
h : Subsingleton α
⊢ normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum
have inl : ∀ (hs : 0 ∉ 0),
  Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors (Multiset.prod 0)) (Multiset.sum (Multiset.map normalizedFactors 0))
Tactic: obtain rfl : s = 0 := by
      apply Multiset.eq_zero_of_forall_notMem
      intro _
      convert! hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
h : Nontrivial α
a : α
s : Multiset α
IH : ∀ (hs : 0 ∉ s), normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum
hs : 0 ∉ a ::ₘ s
⊢ normalizedFactors (a ::ₘ s).prod = (Multiset.map normalizedFactors (a ::ₘ s)).sum
have inr : 0 ∉ s
Tactic: rw [Multiset.prod_cons, Multiset.map_cons, Multiset.sum_cons, normalizedFactors_mul, IH]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
h : Nontrivial α
a : α
s : Multiset α
IH : ∀ (hs : 0 ∉ s), normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum
hs : 0 ∉ a ::ₘ s
inr : 0 ∉ s
⊢ normalizedFactors (a ::ₘ s).prod = (Multiset.map normalizedFactors (a ::ₘ s)).sum
have inr₁ : a ≠ 0
Tactic: rw [Multiset.prod_cons, Multiset.map_cons, Multiset.sum_cons, normalizedFactors_mul, IH]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
h : Nontrivial α
a : α
s : Multiset α
IH : ∀ (hs : 0 ∉ s), normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum
hs : 0 ∉ a ::ₘ s
inr : 0 ∉ s
inr₁ : a ≠ 0
⊢ normalizedFactors (a ::ₘ s).prod = (Multiset.map normalizedFactors (a ::ₘ s)).sum
have inr₂ : s.prod ≠ 0
Tactic: rw [Multiset.prod_cons, Multiset.map_cons, Multiset.sum_cons, normalizedFactors_mul, IH]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
h : Nontrivial α
a : α
s : Multiset α
IH : ∀ (hs : 0 ∉ s), normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum
hs : 0 ∉ a ::ₘ s
⊢ s.prod ≠ 0
have inr : 0 ∉ s
Tactic: apply Multiset.prod_ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
s : Multiset α
hs : 0 ∉ s
h : Nontrivial α
⊢ normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum
have inr : ∀ (hs : 0 ∉ 0),
  Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors (Multiset.prod 0)) (Multiset.sum (Multiset.map normalizedFactors 0))
Tactic: induction s using Multiset.induction with
  | empty => simp
  | cons _ _ IH =>
    rw [Multiset.prod_cons, Multiset.map_cons, Multiset.sum_cons, normalizedFactors_mul, IH]
    · exact fun h ↦ hs (Multiset.mem_cons_of_mem h)
    · exact fun h ↦ hs (h ▸ Multiset.mem_cons_self _ _)
    · apply Multiset.prod_ne_zero
      exact fun h ↦ hs (Multiset.mem_cons_of_mem h)
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
s : Multiset α
hs : 0 ∉ s
h : Nontrivial α
inr :
  ∀ (hs : 0 ∉ 0),
    Eq.{u_1 + 1} (α := Multiset α) (normalizedFactors (Multiset.prod 0))
      (Multiset.sum (Multiset.map normalizedFactors 0))
⊢ normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum
have inr₁ : ∀ (a : α) (s : Multiset α) (IH : ∀ (hs : 0 ∉ s), normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum)
  (hs : 0 ∉ a ::ₘ s), normalizedFactors (a ::ₘ s).prod = (Multiset.map normalizedFactors (a ::ₘ s)).sum
Tactic: induction s using Multiset.induction with
  | empty => simp
  | cons _ _ IH =>
    rw [Multiset.prod_cons, Multiset.map_cons, Multiset.sum_cons, normalizedFactors_mul, IH]
    · exact fun h ↦ hs (Multiset.mem_cons_of_mem h)
    · exact fun h ↦ hs (h ▸ Multiset.mem_cons_self _ _)
    · apply Multiset.prod_ne_zero
      exact fun h ↦ hs (Multiset.mem_cons_of_mem h)
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
β : Type u_2
inst_3 : CommMonoidWithZero β
inst_4 : NormalizationMonoid β
inst_5 : UniqueFactorizationMonoid β
F : Type u_3
inst_6 : EquivLike F α β
inst_7 : MulEquivClass F α β
f : F
he :
  ∀ (x : α),
    Eq (α := β) ((normalize : (a : β) → β) ((f : (a : α) → β) x : β) : β)
      ((f : (a : α) → β) ((normalize : (a : α) → α) x : α) : β)
a x : α
⊢ x ∈ normalizedFactors a ↔
    Membership.mem.{u_2, u_2} (α := β) (γ := Multiset β) (normalizedFactors ((f : (a : α) → β) a) : Multiset β)
      (((↑f : α ≃ β) : (a : α) → β) x : β)
have inl : Membership.mem (γ := Multiset α) (normalizedFactors 0) x ↔
  Membership.mem.{u_2, u_2} (α := β) (γ := Multiset β) (normalizedFactors ((f : (a : α) → β) 0) : Multiset β)
    (((↑f : α ≃ β) : (a : α) → β) x : β)
Tactic: rcases eq_or_ne a 0 with rfl | ha
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : NormalizationMonoid α
inst_2 : UniqueFactorizationMonoid α
β : Type u_2
inst_3 : CommMonoidWithZero β
inst_4 : NormalizationMonoid β
inst_5 : UniqueFactorizationMonoid β
F : Type u_3
inst_6 : EquivLike F α β
inst_7 : MulEquivClass F α β
f : F
he :
  ∀ (x : α),
    Eq (α := β) ((normalize : (a : β) → β) ((f : (a : α) → β) x : β) : β)
      ((f : (a : α) → β) ((normalize : (a : α) → α) x : α) : β)
a x : α
inl :
  Membership.mem (γ := Multiset α) (normalizedFactors 0) x ↔
    Membership.mem.{u_2, u_2} (α := β) (γ := Multiset β) (normalizedFactors ((f : (a : α) → β) 0) : Multiset β)
      (((↑f : α ≃ β) : (a : α) → β) x : β)
⊢ x ∈ normalizedFactors a ↔
    Membership.mem.{u_2, u_2} (α := β) (γ := Multiset β) (normalizedFactors ((f : (a : α) → β) a) : Multiset β)
      (((↑f : α ≃ β) : (a : α) → β) x : β)
have inr : ∀ (ha : a ≠ 0),
  x ∈ normalizedFactors a ↔
    Membership.mem.{u_2, u_2} (α := β) (γ := Multiset β) (normalizedFactors ((f : (a : α) → β) a) : Multiset β)
      (((↑f : α ≃ β) : (a : α) → β) x : β)
Tactic: rcases eq_or_ne a 0 with rfl | ha
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
⊢ Eq.{u_1 + 1} (α := α)
    (if Eq.{u_1 + 1} (α := Associates α) 1 0 then 0
    else
      prod
        (map (α := Associates α)
          (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
          (normalizedFactors 1)))
    1
have a : Nontrivial α
Tactic: nontriviality α
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x y : Associates α
⊢ (if x * y = 0 then 0
    else
      (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
          (normalizedFactors (x * y))).prod) =
    (if x = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
            (normalizedFactors x)).prod) *
      if y = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
            (normalizedFactors y)).prod
have pos : ∀ (hx : x = 0),
  (if x * y = 0 then 0
    else
      (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) sorry)
          (normalizedFactors (x * y))).prod) =
    (if x = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) sorry)
            (normalizedFactors x)).prod) *
      if y = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) sorry)
            (normalizedFactors y)).prod
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x y : Associates α
pos :
  ∀ (hx : x = 0),
    (if x * y = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
            (normalizedFactors (x * y))).prod) =
      (if x = 0 then 0
        else
          (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
              (normalizedFactors x)).prod) *
        if y = 0 then 0
        else
          (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
              (normalizedFactors y)).prod
⊢ (if x * y = 0 then 0
    else
      (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
          (normalizedFactors (x * y))).prod) =
    (if x = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
            (normalizedFactors x)).prod) *
      if y = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
            (normalizedFactors y)).prod
have neg : ∀ (hx : ¬x = 0),
  (if x * y = 0 then 0
    else
      (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) sorry)
          (normalizedFactors (x * y))).prod) =
    (if x = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) sorry)
            (normalizedFactors x)).prod) *
      if y = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) sorry)
            (normalizedFactors y)).prod
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x y : Associates α
hx : ¬x = 0
⊢ (if x * y = 0 then 0
    else
      (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
          (normalizedFactors (x * y))).prod) =
    (if x = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
            (normalizedFactors x)).prod) *
      if y = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
            (normalizedFactors y)).prod
have pos : ∀ (hy : y = 0),
  (if x * y = 0 then 0
    else
      (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) sorry)
          (normalizedFactors (x * y))).prod) =
    (if x = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) sorry)
            (normalizedFactors x)).prod) *
      if y = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) sorry)
            (normalizedFactors y)).prod
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x y : Associates α
hx : ¬x = 0
pos :
  ∀ (hy : y = 0),
    (if x * y = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
            (normalizedFactors (x * y))).prod) =
      (if x = 0 then 0
        else
          (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
              (normalizedFactors x)).prod) *
        if y = 0 then 0
        else
          (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
              (normalizedFactors y)).prod
⊢ (if x * y = 0 then 0
    else
      (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
          (normalizedFactors (x * y))).prod) =
    (if x = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
            (normalizedFactors x)).prod) *
      if y = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
            (normalizedFactors y)).prod
have neg : ∀ (hy : ¬y = 0),
  (if x * y = 0 then 0
    else
      (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) sorry)
          (normalizedFactors (x * y))).prod) =
    (if x = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) sorry)
            (normalizedFactors x)).prod) *
      if y = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) sorry)
            (normalizedFactors y)).prod
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : Associates α
⊢ Associates.mk
      (({
            toFun := fun (a : Associates α) ↦
              if a = 0 then 0
              else
                (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
                    (normalizedFactors a)).prod,
            map_one' := ⋯, map_mul' := ⋯ } :
          (a : Associates α) → α)
        x) =
    x
have dsimp : Associates.mk
    (if x = 0 then 0
    else
      (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) sorry)
          (normalizedFactors x)).prod) =
  x
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : Associates α
⊢ Associates.mk
      (if x = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
            (normalizedFactors x)).prod) =
    x
have pos : ∀ (hx : x = 0),
  Associates.mk
      (if x = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) sorry)
            (normalizedFactors x)).prod) =
    x
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : Associates α
pos :
  ∀ (hx : x = 0),
    Associates.mk
        (if x = 0 then 0
        else
          (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
              (normalizedFactors x)).prod) =
      x
⊢ Associates.mk
      (if x = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
            (normalizedFactors x)).prod) =
    x
have neg : ∀ (hx : ¬x = 0),
  Associates.mk
      (if x = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) sorry)
            (normalizedFactors x)).prod) =
    x
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : Associates α
hx : ¬x = 0
⊢ Eq.{u_1 + 1} (α := Associates α → Associates α)
    ((⇑Associates.mkMonoidHom : (a : α) → Associates α) ∘
      Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
    id
have h : ∀ (x : Associates α),
  ((⇑Associates.mkMonoidHom : (a : α) → Associates α) ∘
        Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) sorry)
      x =
    id x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x_1 : Associates α
hx : ¬x_1 = 0
x : Associates α
⊢ ((⇑Associates.mkMonoidHom : (a : α) → Associates α) ∘
        Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
      x =
    id x
have h : x = id x
Tactic: rw [Function.comp_apply, mkMonoidHom_apply,
          Classical.choose_spec mk_surjective.hasRightInverse x]
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : Associates α
hx : ¬x = 0
⊢ Associates.mk
      (if x = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
            (normalizedFactors x)).prod) =
    x
have h : Eq.{u_1 + 1} (α := Associates α → Associates α)
  ((⇑Associates.mkMonoidHom : (a : α) → Associates α) ∘
    Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) sorry)
  id
Tactic: have h : Associates.mkMonoidHom ∘ Classical.choose mk_surjective.hasRightInverse =
          (id : Associates α → Associates α) := by
        ext x
        rw [Function.comp_apply, mkMonoidHom_apply,
          Classical.choose_spec mk_surjective.hasRightInverse x]
        rfl
-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : Associates α
hx : ¬x = 0
h :
  Eq.{u_1 + 1} (α := Associates α → Associates α)
    ((⇑Associates.mkMonoidHom : (a : α) → Associates α) ∘
      Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
    id
⊢ Associates.mk
      (if x = 0 then 0
      else
        (map (Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
            (normalizedFactors x)).prod) =
    x
have neg : (normalizedFactors x).prod ~ᵤ x
Tactic: rw [if_neg hx, ← mkMonoidHom_apply, MonoidHom.map_multiset_prod, map_map, h, map_id, ←
        associated_iff_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (hypothesis)
Goal:
R : Type v
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w
inst_3 : CommRing B
inst_4 : Algebra R B
I : Ideal B
inst_5 : FormallyUnramified R A
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : A →ₐ[R] B
e :
  Eq (α := AlgHom.{v, u, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁)
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂)
this : Algebra A B := f₁.toAlgebra
⊢ f₁ = f₂
have this₁ : IsScalarTower R A B
Tactic: haveI := IsScalarTower.of_algebraMap_eq' f₁.comp_algebraMap.symm
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (hypothesis)
Goal:
R : Type v
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w
inst_3 : CommRing B
inst_4 : Algebra R B
I : Ideal B
inst_5 : FormallyUnramified R A
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f₁ f₂ : A →ₐ[R] B
e :
  Eq (α := AlgHom.{v, u, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₁)
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) f₂)
this_1 : Algebra A B := f₁.toAlgebra
this : IsScalarTower R A B
⊢ f₁ = f₂
have this₁ : Subsingleton
  { f : A →ₐ[R] B //
    Eq (α := AlgHom.{v, u, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)
      (IsScalarTower.toAlgHom R A (B ⧸ I)) }
Tactic: have :=
    ((KaehlerDifferential.linearMapEquivDerivation R A).toEquiv.trans
          (derivationToSquareZeroEquivLift I hI)).surjective.subsingleton
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type v
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
I : Ideal B
hI : IsNilpotent I
g₁ g₂ : A →ₐ[R] B
h :
  Eq (α := AlgHom.{v, u, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) g₁)
    (AlgHom.comp (Ideal.Quotient.mkₐ R I) g₂)
⊢ g₁ = g₂
have revert : ∀ (g₁ g₂ : A →ₐ[R] B)
  (h :
    Eq (α := AlgHom.{v, u, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) g₁)
      (AlgHom.comp (Ideal.Quotient.mkₐ R I) g₂)),
  g₁ = g₂
Tactic: revert g₁ g₂
Cleared hypotheses: g₁, g₂, h
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type v
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
I : Ideal B
hI : IsNilpotent I
⊢ ∀ (g₁ g₂ : A →ₐ[R] B)
    (h :
      Eq (α := AlgHom.{v, u, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I) g₁)
        (AlgHom.comp (Ideal.Quotient.mkₐ R I) g₂)),
    g₁ = g₂
have change : Function.Injective (α := A →ₐ[R] B) (β := AlgHom.{v, u, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
Tactic: change Function.Injective (Ideal.Quotient.mkₐ R I).comp
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type v
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallyUnramified R A
I : Ideal B
hI : IsNilpotent I
⊢ Function.Injective (α := A →ₐ[R] B) (β := AlgHom.{v, u, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
have revert : ∀ [inst_6 : Algebra R B],
  Function.Injective (α := A →ₐ[R] B) (β := AlgHom.{v, u, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
Tactic: revert ‹Algebra R B›
Cleared hypotheses: inst_4
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Basic (goal)
Goal:
R : Type v
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w
inst_3 : CommRing B
inst_4 : FormallyUnramified R A
I : Ideal B
hI : IsNilpotent I
⊢ ∀ [inst_5 : Algebra R B],
    Function.Injective (α := A →ₐ[R] B) (β := AlgHom.{v, u, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
have h₁ : ∀ ⦃S : Type w⦄ [inst_5 : CommRing S] (I : Ideal S),
  HPow.hPow (β := ℕ) I 2 = ⊥ →
    ∀ [inst_6 : Algebra R S],
      Function.Injective (α := A →ₐ[R] S) (β := AlgHom.{v, u, w} R A (S ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
Tactic: apply Ideal.IsNilpotent.induction_on (S := B) I hI