awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
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
neg :
  ∀ (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

Tactic:
by_cases hy : y = 0
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x y : Associates α
hx : ¬x = 0
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

Tactic:
simp [hy]
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x y : Associates α
hx : ¬x = 0
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

Tactic:
simp [hx, hy]
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : Associates α
dsimp :
  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
      (({
            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

Tactic:
dsimp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
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
neg :
  ∀ (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

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
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

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x : Associates α
hx : ¬x = 0
h :
  ∀ (x : Associates α),
    ((⇑Associates.mkMonoidHom : (a : α) → Associates α) ∘
          Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
        x =
      id x
⊢ Eq.{u_1 + 1} (α := Associates α → Associates α)
    ((⇑Associates.mkMonoidHom : (a : α) → Associates α) ∘
      Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
    id

Tactic:
ext x
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x_1 : Associates α
hx : ¬x_1 = 0
x : Associates α
h : x = id x
⊢ ((⇑Associates.mkMonoidHom : (a : α) → Associates α) ∘
        Classical.choose (p := fun (x : Associates α → α) ↦ Function.RightInverse x Associates.mk) ⋯)
      x =
    id x

Tactic:
rw [Function.comp_apply, mkMonoidHom_apply,
          Classical.choose_spec mk_surjective.hasRightInverse x]

Premises used: Function.Surjective.hasRightInverse, Associates.mkMonoidHom_apply, Associates.mk_surjective, Classical.choose_spec, Function.comp_apply
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
x_1 : Associates α
hx : ¬x_1 = 0
x : Associates α
⊢ x = id x

Tactic:
rfl
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
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

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
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
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
neg : (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

Tactic:
rw [if_neg hx, ← mkMonoidHom_apply, MonoidHom.map_multiset_prod, map_map, h, map_id, ←
        associated_iff_eq]

Premises used: Multiset.map_id, Associates.mkMonoidHom_apply, associated_iff_eq, Multiset.map_map, MonoidHom.map_multiset_prod, if_neg
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
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
⊢ (normalizedFactors x).prod ~ᵤ x

Tactic:
apply prod_normalizedFactors hx

Premises used: UniqueFactorizationMonoid.prod_normalizedFactors
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : Subsingleton.{u_2 + 1} αˣ
a : α
m : Multiset α
hm : m ⊆ normalizedFactors a
⊢ normalizedFactors m.prod = m

Tactic:
normalizedFactors_prod_of_prime fun _ h ↦ prime_of_normalized_factor _ (mem_of_subset hm h)

Premises used: UniqueFactorizationMonoid.normalizedFactors_prod_of_prime, UniqueFactorizationMonoid.prime_of_normalized_factor, Multiset.mem_of_subset
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : NormalizationMonoid α
inst_3 : Nontrivial α
a : α
m : Multiset α
hm : m ⊆ normalizedFactors a
⊢ m.prod ≠ 0

Tactic:
prod_ne_zero_of_prime _ fun _ h ↦ prime_of_normalized_factor _ (mem_of_subset hm h)

Premises used: UniqueFactorizationMonoid.prime_of_normalized_factor, Multiset.prod_ne_zero_of_prime, Multiset.mem_of_subset
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq α
inst_3 : Subsingleton.{u_2 + 1} αˣ
a b : α
⊢ normalizedFactors (normalizedFactors a ∩ normalizedFactors b).prod = normalizedFactors a ∩ normalizedFactors b

Tactic:
normalizedFactors_prod_eq_self_of_subset fun _ h ↦ (mem_inter.mp h).left

Premises used: And.left, Iff.mp, UniqueFactorizationMonoid.normalizedFactors_prod_eq_self_of_subset, Multiset.mem_inter
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Goal:
α : Type u_2
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
inst_2 : DecidableEq α
inst_3 : NormalizationMonoid α
inst_4 : Nontrivial α
a b : α
⊢ (normalizedFactors a ∩ normalizedFactors b).prod ≠ 0

Tactic:
prod_ne_zero_of_subset_normalizedFactors fun _ h ↦ (mem_inter.mp h).left

Premises used: UniqueFactorizationMonoid.prod_ne_zero_of_subset_normalizedFactors, And.left, Iff.mp, Multiset.mem_inter
-- Module: Mathlib.RingTheory.Unramified.Basic
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
⊢ IsScalarTower R A B

Tactic:
haveI := IsScalarTower.of_algebraMap_eq' f₁.comp_algebraMap.symm
-- Module: Mathlib.RingTheory.Unramified.Basic
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
⊢ 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
-- Module: Mathlib.RingTheory.Unramified.Basic
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_2 : IsScalarTower R A B
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)) }
⊢ f₁ = f₂

Tactic:
Subtype.ext_iff.mp (@Subsingleton.elim _ this ⟨f₁, rfl⟩ ⟨f₂, e.symm⟩)

Premises used: Subtype.ext_iff, Subtype.mk, Iff.mp, Subsingleton.elim, Eq.symm, rfl
-- Module: Mathlib.RingTheory.Unramified.Basic
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_2 : IsScalarTower R A B
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)) }
⊢ f₁ = f₂

Tactic:
exact Subtype.ext_iff.mp (@Subsingleton.elim _ this ⟨f₁, rfl⟩ ⟨f₂, e.symm⟩)

Premises used: Subtype.ext_iff, Subtype.mk, Iff.mp, Subsingleton.elim, Eq.symm, rfl
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type v
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Algebra R A
⊢ FormallyUnramified R A ↔
    ∀ ⦃B : Type u⦄ [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B),
      HPow.hPow (β := ℕ) I 2 = ⊥ →
        Function.Injective (α := A →ₐ[R] B) (β := A →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))

Tactic:
iff_comp_injective_of_small

Premises used: Algebra.FormallyUnramified.iff_comp_injective_of_small
-- Module: Mathlib.RingTheory.Unramified.Basic
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₂)
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₂
⊢ g₁ = g₂

Tactic:
revert g₁ g₂
-- Module: Mathlib.RingTheory.Unramified.Basic
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
change : Function.Injective (α := A →ₐ[R] B) (β := AlgHom.{v, u, w} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R 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₂

Tactic:
change Function.Injective (Ideal.Quotient.mkₐ R I).comp

Premises used: Function.Injective, AlgHom.comp, Ideal.Quotient.mkₐ
-- Module: Mathlib.RingTheory.Unramified.Basic
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
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))
⊢ 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›

Premises used: Algebra
-- Module: Mathlib.RingTheory.Unramified.Basic
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
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))
h₂ :
  ∀ ⦃S : Type w⦄ [inst_5 : CommRing S] (I J : Ideal S),
    I ≤ J →
      (∀ [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))) →
        (∀ [inst_6 : Algebra.{v, w} R (S ⧸ I)],
            Function.Injective (α := AlgHom.{v, u, w} R A (S ⧸ I)) (β :=
              AlgHom.{v, u, w} R A
                (HasQuotient.Quotient (S ⧸ I) (B := Ideal (S ⧸ I))
                  (Ideal.map (F := S →+* S ⧸ I) (Ideal.Quotient.mk I) J)))
              (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := S →+* S ⧸ I) (Ideal.Quotient.mk I) J)))) →
          ∀ [inst_6 : Algebra R S],
            Function.Injective (α := A →ₐ[R] S) (β := AlgHom.{v, u, w} R A (S ⧸ J))
              (AlgHom.comp (Ideal.Quotient.mkₐ R J))
⊢ ∀ [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))

Tactic:
apply Ideal.IsNilpotent.induction_on (S := B) I hI

Premises used: Ideal.IsNilpotent.induction_on
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type v
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Algebra R A
B_1 : Type w
inst_3 : CommRing B_1
inst_4 : FormallyUnramified R A
I : Ideal B_1
hI : IsNilpotent I
B : Type w
h₁ :
  ∀ [inst_5 : CommRing B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      ∀ [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))
⊢ ∀ [inst_5 : CommRing B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      ∀ [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:
_
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type v
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Algebra R A
B_1 : Type w
inst_3 : CommRing B_1
inst_4 : FormallyUnramified R A
I_1 : Ideal B_1
hI_1 : IsNilpotent I_1
B : Type w
inst_5 : CommRing B
I : Ideal B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
h₁ :
  ∀ [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))
⊢ ∀ [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:
_
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type v
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Algebra R A
B_1 : Type w
inst_3 : CommRing B_1
inst_4 : FormallyUnramified R A
I_1 : Ideal B_1
hI_1 : IsNilpotent I_1
B : Type w
inst_5 : CommRing B
I : Ideal B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
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:
FormallyUnramified.comp_injective I hI

Premises used: Algebra.FormallyUnramified.comp_injective
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type v
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Algebra R A
B_1 : Type w
inst_3 : CommRing B_1
inst_4 : FormallyUnramified R A
I_1 : Ideal B_1
hI_1 : IsNilpotent I_1
B : Type w
inst_5 : CommRing B
I : Ideal B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
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:
exact FormallyUnramified.comp_injective I hI

Premises used: Algebra.FormallyUnramified.comp_injective
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type v
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Algebra R A
B_1 : Type w
inst_3 : CommRing B_1
inst_4 : FormallyUnramified R A
I : Ideal B_1
hI : IsNilpotent I
B : Type w
h₂ :
  ∀ [inst_5 : CommRing B] (I J : Ideal B),
    I ≤ J →
      (∀ [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))) →
        (∀ [inst_6 : Algebra.{v, w} R (B ⧸ I)],
            Function.Injective (α := AlgHom.{v, u, w} R A (B ⧸ I)) (β :=
              AlgHom.{v, u, w} R A
                (HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I))
                  (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
              (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))) →
          ∀ [inst_6 : Algebra R B],
            Function.Injective (α := A →ₐ[R] B) (β := AlgHom.{v, u, w} R A (B ⧸ J))
              (AlgHom.comp (Ideal.Quotient.mkₐ R J))
⊢ ∀ [inst_5 : CommRing B] (I J : Ideal B),
    I ≤ J →
      (∀ [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))) →
        (∀ [inst_6 : Algebra.{v, w} R (B ⧸ I)],
            Function.Injective (α := AlgHom.{v, u, w} R A (B ⧸ I)) (β :=
              AlgHom.{v, u, w} R A
                (HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I))
                  (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
              (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))) →
          ∀ [inst_6 : Algebra R B],
            Function.Injective (α := A →ₐ[R] B) (β := AlgHom.{v, u, w} R A (B ⧸ J))
              (AlgHom.comp (Ideal.Quotient.mkₐ R J))

Tactic:
_
-- Module: Mathlib.RingTheory.Unramified.Basic
Goal:
R : Type v
inst : CommRing R
A : Type u
inst_1 : CommRing A
inst_2 : Algebra R A
B_1 : Type w
inst_3 : CommRing B_1
inst_4 : FormallyUnramified R A
I_1 : Ideal B_1
hI : IsNilpotent I_1
B : Type w
inst_5 : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ :
  ∀ [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))
h₂ :
  ∀ [inst_6 : Algebra.{v, w} R (B ⧸ I)],
    Function.Injective (α := AlgHom.{v, u, w} R A (B ⧸ I)) (β :=
      AlgHom.{v, u, w} R A
        (HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
      (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
h₃ :
  ∀ [inst_6 : Algebra R B],
    Function.Injective (α := A →ₐ[R] B) (β := AlgHom.{v, u, w} R A (B ⧸ J)) (AlgHom.comp (Ideal.Quotient.mkₐ R J))
⊢ ∀ [inst_6 : Algebra R B],
    Function.Injective (α := A →ₐ[R] B) (β := AlgHom.{v, u, w} R A (B ⧸ J)) (AlgHom.comp (Ideal.Quotient.mkₐ R J))

Tactic:
_