awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsTorsionFree R S
inst_6 : IsIntegrallyClosed R
x : S
hx' : IsIntegral R x
this : IsDomain.{u} (AdjoinRoot (minpoly R x))
⊢ Eq (α := R[X]) (minpoly R x) (minpoly R (powerBasis' hx').gen)
have this₁ : IsTorsionFree R (AdjoinRoot (minpoly R x))
Tactic: have :=
    noZeroSMulDivisors_of_prime_of_degree_ne_zero (prime_of_isIntegrallyClosed hx')
      (degree_pos hx').ne'
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsTorsionFree R S
inst_6 : IsIntegrallyClosed R
x : S
hx' : IsIntegral R x
this_1 : IsDomain.{u} (AdjoinRoot (minpoly R x))
this : IsTorsionFree R (AdjoinRoot (minpoly R x))
⊢ Eq (α := R[X]) (minpoly R x) (minpoly R (powerBasis' hx').gen)
have rw : minpoly R x = (powerBasis' hx').minpolyGen
Tactic: rw [← minpolyGen_eq, adjoin.powerBasis', minpolyGen_map, minpolyGen_eq,
    AdjoinRoot.powerBasis'_gen, ← isAdjoinRoot_root_eq_root _,
    ← isAdjoinRootMonic_toAdjoinRoot _ (monic hx'),
    minpoly_eq (AdjoinRoot.isAdjoinRootMonic _ (monic hx')) (irreducible hx')]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsTorsionFree R S
inst_6 : IsIntegrallyClosed R
x : S
hx' : IsIntegral R x
this_1 : IsDomain.{u} (AdjoinRoot (minpoly R x))
this : IsTorsionFree R (AdjoinRoot (minpoly R x))
rw : minpoly R x = (powerBasis' hx').minpolyGen
⊢ Eq (α := R[X]) (minpoly R x) (minpoly R (powerBasis' hx').gen)
have rw₁ : minpoly R x = ((AdjoinRoot.powerBasis' sorry).map (equivAdjoin hx')).minpolyGen
Tactic: rw [← minpolyGen_eq, adjoin.powerBasis', minpolyGen_map, minpolyGen_eq,
    AdjoinRoot.powerBasis'_gen, ← isAdjoinRoot_root_eq_root _,
    ← isAdjoinRootMonic_toAdjoinRoot _ (monic hx'),
    minpoly_eq (AdjoinRoot.isAdjoinRootMonic _ (monic hx')) (irreducible hx')]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsTorsionFree R S
inst_6 : IsIntegrallyClosed R
x : S
hx' : IsIntegral R x
this_1 : IsDomain.{u} (AdjoinRoot (minpoly R x))
this : IsTorsionFree R (AdjoinRoot (minpoly R x))
rw : minpoly R x = (powerBasis' hx').minpolyGen
rw₁ : minpoly R x = ((AdjoinRoot.powerBasis' ⋯).map (equivAdjoin hx')).minpolyGen
⊢ Eq (α := R[X]) (minpoly R x) (minpoly R (powerBasis' hx').gen)
have rw₂ : minpoly R x = (AdjoinRoot.powerBasis' sorry).minpolyGen
Tactic: rw [← minpolyGen_eq, adjoin.powerBasis', minpolyGen_map, minpolyGen_eq,
    AdjoinRoot.powerBasis'_gen, ← isAdjoinRoot_root_eq_root _,
    ← isAdjoinRootMonic_toAdjoinRoot _ (monic hx'),
    minpoly_eq (AdjoinRoot.isAdjoinRootMonic _ (monic hx')) (irreducible hx')]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsTorsionFree R S
inst_6 : IsIntegrallyClosed R
x : S
hx' : IsIntegral R x
this_1 : IsDomain.{u} (AdjoinRoot (minpoly R x))
this : IsTorsionFree R (AdjoinRoot (minpoly R x))
rw : minpoly R x = (powerBasis' hx').minpolyGen
rw₁ : minpoly R x = ((AdjoinRoot.powerBasis' ⋯).map (equivAdjoin hx')).minpolyGen
rw₂ : minpoly R x = (AdjoinRoot.powerBasis' ⋯).minpolyGen
⊢ Eq (α := R[X]) (minpoly R x) (minpoly R (powerBasis' hx').gen)
have rw₃ : Eq (α := R[X]) (minpoly R x) (minpoly R (AdjoinRoot.powerBasis' sorry).gen)
Tactic: rw [← minpolyGen_eq, adjoin.powerBasis', minpolyGen_map, minpolyGen_eq,
    AdjoinRoot.powerBasis'_gen, ← isAdjoinRoot_root_eq_root _,
    ← isAdjoinRootMonic_toAdjoinRoot _ (monic hx'),
    minpoly_eq (AdjoinRoot.isAdjoinRootMonic _ (monic hx')) (irreducible hx')]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsTorsionFree R S
inst_6 : IsIntegrallyClosed R
x : S
hx' : IsIntegral R x
this_1 : IsDomain.{u} (AdjoinRoot (minpoly R x))
this : IsTorsionFree R (AdjoinRoot (minpoly R x))
rw : minpoly R x = (powerBasis' hx').minpolyGen
rw₁ : minpoly R x = ((AdjoinRoot.powerBasis' ⋯).map (equivAdjoin hx')).minpolyGen
rw₂ : minpoly R x = (AdjoinRoot.powerBasis' ⋯).minpolyGen
rw₃ : Eq (α := R[X]) (minpoly R x) (minpoly R (AdjoinRoot.powerBasis' ⋯).gen)
⊢ Eq (α := R[X]) (minpoly R x) (minpoly R (powerBasis' hx').gen)
have rw₄ : Eq (α := R[X]) (minpoly R x) (minpoly R (B := AdjoinRoot (minpoly R x)) (AdjoinRoot.root (minpoly R x)))
Tactic: rw [← minpolyGen_eq, adjoin.powerBasis', minpolyGen_map, minpolyGen_eq,
    AdjoinRoot.powerBasis'_gen, ← isAdjoinRoot_root_eq_root _,
    ← isAdjoinRootMonic_toAdjoinRoot _ (monic hx'),
    minpoly_eq (AdjoinRoot.isAdjoinRootMonic _ (monic hx')) (irreducible hx')]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsTorsionFree R S
inst_6 : IsIntegrallyClosed R
x : S
hx' : IsIntegral R x
this_1 : IsDomain.{u} (AdjoinRoot (minpoly R x))
this : IsTorsionFree R (AdjoinRoot (minpoly R x))
rw : minpoly R x = (powerBasis' hx').minpolyGen
rw₁ : minpoly R x = ((AdjoinRoot.powerBasis' ⋯).map (equivAdjoin hx')).minpolyGen
rw₂ : minpoly R x = (AdjoinRoot.powerBasis' ⋯).minpolyGen
rw₃ : Eq (α := R[X]) (minpoly R x) (minpoly R (AdjoinRoot.powerBasis' ⋯).gen)
rw₄ : Eq (α := R[X]) (minpoly R x) (minpoly R (B := AdjoinRoot (minpoly R x)) (AdjoinRoot.root (minpoly R x)))
⊢ Eq (α := R[X]) (minpoly R x) (minpoly R (powerBasis' hx').gen)
have rw₅ : Eq (α := R[X]) (minpoly R x)
  (minpoly R (B := AdjoinRoot (minpoly R x)) (IsAdjoinRoot.root (AdjoinRoot.isAdjoinRoot (minpoly R x))))
Tactic: rw [← minpolyGen_eq, adjoin.powerBasis', minpolyGen_map, minpolyGen_eq,
    AdjoinRoot.powerBasis'_gen, ← isAdjoinRoot_root_eq_root _,
    ← isAdjoinRootMonic_toAdjoinRoot _ (monic hx'),
    minpoly_eq (AdjoinRoot.isAdjoinRootMonic _ (monic hx')) (irreducible hx')]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsTorsionFree R S
inst_6 : IsIntegrallyClosed R
x : S
hx' : IsIntegral R x
this_1 : IsDomain.{u} (AdjoinRoot (minpoly R x))
this : IsTorsionFree R (AdjoinRoot (minpoly R x))
rw : minpoly R x = (powerBasis' hx').minpolyGen
rw₁ : minpoly R x = ((AdjoinRoot.powerBasis' ⋯).map (equivAdjoin hx')).minpolyGen
rw₂ : minpoly R x = (AdjoinRoot.powerBasis' ⋯).minpolyGen
rw₃ : Eq (α := R[X]) (minpoly R x) (minpoly R (AdjoinRoot.powerBasis' ⋯).gen)
rw₄ : Eq (α := R[X]) (minpoly R x) (minpoly R (B := AdjoinRoot (minpoly R x)) (AdjoinRoot.root (minpoly R x)))
rw₅ :
  Eq (α := R[X]) (minpoly R x)
    (minpoly R (B := AdjoinRoot (minpoly R x)) (IsAdjoinRoot.root (AdjoinRoot.isAdjoinRoot (minpoly R x))))
⊢ Eq (α := R[X]) (minpoly R x) (minpoly R (powerBasis' hx').gen)
have rw₆ : Eq (α := R[X]) (minpoly R x) (minpoly R (AdjoinRoot.isAdjoinRootMonic (minpoly R x) sorry).root)
Tactic: rw [← minpolyGen_eq, adjoin.powerBasis', minpolyGen_map, minpolyGen_eq,
    AdjoinRoot.powerBasis'_gen, ← isAdjoinRoot_root_eq_root _,
    ← isAdjoinRootMonic_toAdjoinRoot _ (monic hx'),
    minpoly_eq (AdjoinRoot.isAdjoinRootMonic _ (monic hx')) (irreducible hx')]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : IsTorsionFree R S
inst_6 : IsIntegrallyClosed R
x : S
hx' : IsIntegral R x
this_1 : IsDomain.{u} (AdjoinRoot (minpoly R x))
this : IsTorsionFree R (AdjoinRoot (minpoly R x))
rw : minpoly R x = (powerBasis' hx').minpolyGen
rw₁ : minpoly R x = ((AdjoinRoot.powerBasis' ⋯).map (equivAdjoin hx')).minpolyGen
rw₂ : minpoly R x = (AdjoinRoot.powerBasis' ⋯).minpolyGen
rw₃ : Eq (α := R[X]) (minpoly R x) (minpoly R (AdjoinRoot.powerBasis' ⋯).gen)
rw₄ : Eq (α := R[X]) (minpoly R x) (minpoly R (B := AdjoinRoot (minpoly R x)) (AdjoinRoot.root (minpoly R x)))
rw₅ :
  Eq (α := R[X]) (minpoly R x)
    (minpoly R (B := AdjoinRoot (minpoly R x)) (IsAdjoinRoot.root (AdjoinRoot.isAdjoinRoot (minpoly R x))))
rw₆ : Eq (α := R[X]) (minpoly R x) (minpoly R (AdjoinRoot.isAdjoinRootMonic (minpoly R x) ⋯).root)
⊢ Eq (α := R[X]) (minpoly R x) (minpoly R (powerBasis' hx').gen)
have rw₇ : Eq (α := R[X]) (minpoly R x) (minpoly R x)
Tactic: rw [← minpolyGen_eq, adjoin.powerBasis', minpolyGen_map, minpolyGen_eq,
    AdjoinRoot.powerBasis'_gen, ← isAdjoinRoot_root_eq_root _,
    ← isAdjoinRootMonic_toAdjoinRoot _ (monic hx'),
    minpoly_eq (AdjoinRoot.isAdjoinRootMonic _ (monic hx')) (irreducible hx')]
-- Lean 4 proof step from Mathlib.RingTheory.IsPrimary (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S T : Submodule R M
hS : S.IsPrimary
hT : T.IsPrimary
h : (S.colon Set.univ).radical = (T.colon Set.univ).radical
⊢ (S ⊓ T).IsPrimary
have left : S ≠ ⊤
Tactic: obtain ⟨_, hS⟩ := hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.RingTheory.IsPrimary (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S T : Submodule R M
hS : S.IsPrimary
hT : T.IsPrimary
h : (S.colon Set.univ).radical = (T.colon Set.univ).radical
left : S ≠ ⊤
⊢ (S ⊓ T).IsPrimary
have hS₁ : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (r ^ n) ⊤ ≤ S
Tactic: obtain ⟨_, hS⟩ := hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.RingTheory.IsPrimary (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S T : Submodule R M
hT : T.IsPrimary
h : (S.colon Set.univ).radical = (T.colon Set.univ).radical
left : S ≠ ⊤
hS : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (r ^ n) ⊤ ≤ S
⊢ (S ⊓ T).IsPrimary
have left : T ≠ ⊤
Tactic: obtain ⟨_, hT⟩ := hT
Cleared hypotheses: hT
-- Lean 4 proof step from Mathlib.RingTheory.IsPrimary (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S T : Submodule R M
hT : T.IsPrimary
h : (S.colon Set.univ).radical = (T.colon Set.univ).radical
left_1 : S ≠ ⊤
hS : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (r ^ n) ⊤ ≤ S
left : T ≠ ⊤
⊢ (S ⊓ T).IsPrimary
have hT₁ : ∀ {r : R} {x : M}, r • x ∈ T → x ∈ T ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (r ^ n) ⊤ ≤ T
Tactic: obtain ⟨_, hT⟩ := hT
Cleared hypotheses: hT
-- Lean 4 proof step from Mathlib.RingTheory.IsPrimary (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S T : Submodule R M
h : (S.colon Set.univ).radical = (T.colon Set.univ).radical
left : S ≠ ⊤
hS : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (r ^ n) ⊤ ≤ S
left_1 : T ≠ ⊤
hT : ∀ {r : R} {x : M}, r • x ∈ T → x ∈ T ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (r ^ n) ⊤ ≤ T
⊢ (S ⊓ T).IsPrimary
have refine : ∀ {r : R} {x : M},
  r • x ∈ S ⊓ T →
    ∀ (hS' : r • x ∈ (↑S : Set M)) (hT' : r • x ∈ (↑T : Set M)),
      x ∈ S ⊓ T ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (r ^ n) ⊤ ≤ S ⊓ T
Tactic: refine ⟨by grind, fun ⟨hS', hT'⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.IsPrimary (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S T : Submodule R M
h : (S.colon Set.univ).radical = (T.colon Set.univ).radical
left : S ≠ ⊤
hS : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (r ^ n) ⊤ ≤ S
left_1 : T ≠ ⊤
hT : ∀ {r : R} {x : M}, r • x ∈ T → x ∈ T ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (r ^ n) ⊤ ≤ T
r : R
x : M
h_1 : r • x ∈ S ⊓ T
hS' : r • x ∈ (↑S : Set M)
hT' : r • x ∈ (↑T : Set M)
⊢ x ∈ S ⊓ T ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (r ^ n) ⊤ ≤ S ⊓ T
have simp_rw : ∀ (hT : ∀ {r : R} {x : M}, r • x ∈ T → x ∈ T ∨ r ∈ (T.colon Set.univ).radical)
  (hS : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ r ∈ (T.colon Set.univ).radical),
  (x ∈ S ∨ r ∈ (T.colon Set.univ).radical) ∧ (x ∈ T ∨ r ∈ (T.colon Set.univ).radical)
Tactic: simp_rw [← mem_colon_iff_le, ← Ideal.mem_radical_iff, inf_colon, Ideal.radical_inf,
    top_coe, h, inf_idem, mem_inf, and_or_right] at hS hT ⊢
Cleared hypotheses: hS, hT
-- Lean 4 proof step from Mathlib.RingTheory.IsPrimary (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
f : ι → Submodule R M
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι} (hi : i ∈ s) (hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary)
    (hs' : ∀ ⦃y : ι⦄, y ∈ s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical), (s.inf f).IsPrimary
i : ι
hi : i ∈ insert a s
hs : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical
⊢ ((insert a s).inf f).IsPrimary
have insert : ∀ (ha : a ∉ ∅)
  (IH :
    ∀ {i : ι} (hi : Membership.mem (γ := Finset ι) ∅ i)
      (hs : ∀ ⦃y : ι⦄, Membership.mem (γ := Finset ι) ∅ y → (f y).IsPrimary)
      (hs' :
        ∀ ⦃y : ι⦄,
          Membership.mem (γ := Finset ι) ∅ y → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical),
      (inf ∅ f).IsPrimary)
  (hi : Membership.mem (γ := Finset ι) (insert a ∅) i)
  (hs : ∀ ⦃y : ι⦄, Membership.mem (γ := Finset ι) (insert a ∅) y → (f y).IsPrimary)
  (hs' :
    ∀ ⦃y : ι⦄,
      Membership.mem (γ := Finset ι) (insert a ∅) y → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical),
  (inf (insert a ∅) f).IsPrimary
Tactic: rcases s.eq_empty_or_nonempty with rfl | ⟨y, hy⟩
Cleared hypotheses: s, ha, IH, hi, hs, hs'
-- Lean 4 proof step from Mathlib.RingTheory.IsPrimary (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
f : ι → Submodule R M
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι} (hi : i ∈ s) (hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary)
    (hs' : ∀ ⦃y : ι⦄, y ∈ s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical), (s.inf f).IsPrimary
i : ι
hi : i ∈ Insert.insert a s
hs : ∀ ⦃y : ι⦄, y ∈ Insert.insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ Insert.insert a s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical
insert :
  ∀ (ha : a ∉ ∅)
    (IH :
      ∀ {i : ι} (hi : Membership.mem (γ := Finset ι) ∅ i)
        (hs : ∀ ⦃y : ι⦄, Membership.mem (γ := Finset ι) ∅ y → (f y).IsPrimary)
        (hs' :
          ∀ ⦃y : ι⦄,
            Membership.mem (γ := Finset ι) ∅ y → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical),
        (inf ∅ f).IsPrimary)
    (hi : Membership.mem (γ := Finset ι) (Insert.insert a ∅) i)
    (hs : ∀ ⦃y : ι⦄, Membership.mem (γ := Finset ι) (Insert.insert a ∅) y → (f y).IsPrimary)
    (hs' :
      ∀ ⦃y : ι⦄,
        Membership.mem (γ := Finset ι) (Insert.insert a ∅) y →
          ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical),
    (inf (Insert.insert a ∅) f).IsPrimary
⊢ ((Insert.insert a s).inf f).IsPrimary
have insert₁ : ∀ (y : ι) (hy : y ∈ s), ((Insert.insert a s).inf f).IsPrimary
Tactic: rcases s.eq_empty_or_nonempty with rfl | ⟨y, hy⟩
-- Lean 4 proof step from Mathlib.RingTheory.IsPrimary (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
f : ι → Submodule R M
a i : ι
ha : a ∉ ∅
IH :
  ∀ {i : ι} (hi : Membership.mem (γ := Finset ι) ∅ i)
    (hs : ∀ ⦃y : ι⦄, Membership.mem (γ := Finset ι) ∅ y → (f y).IsPrimary)
    (hs' :
      ∀ ⦃y : ι⦄, Membership.mem (γ := Finset ι) ∅ y → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical),
    (inf ∅ f).IsPrimary
hi : Membership.mem (γ := Finset ι) (insert a ∅) i
hs : ∀ ⦃y : ι⦄, Membership.mem (γ := Finset ι) (insert a ∅) y → (f y).IsPrimary
hs' :
  ∀ ⦃y : ι⦄,
    Membership.mem (γ := Finset ι) (insert a ∅) y → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical
⊢ (inf (insert a ∅) f).IsPrimary
have hi₁ : i = a
Tactic: simp only [insert_empty_eq, mem_singleton] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.IsPrimary (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
f : ι → Submodule R M
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι} (hi : i ∈ s) (hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary)
    (hs' : ∀ ⦃y : ι⦄, y ∈ s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical), (s.inf f).IsPrimary
i : ι
hi : i ∈ insert a s
hs : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical
y : ι
hy : y ∈ s
⊢ ((insert a s).inf f).IsPrimary
have insert : (f a ⊓ s.inf f).IsPrimary
Tactic: simp only [inf_insert]
-- Lean 4 proof step from Mathlib.RingTheory.IsPrimary (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
f : ι → Submodule R M
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι} (hi : i ∈ s) (hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary)
    (hs' : ∀ ⦃y : ι⦄, y ∈ s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical), (s.inf f).IsPrimary
i : ι
hi : i ∈ insert a s
hs : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical
y : ι
hy : y ∈ s
x : ι
hx : x ∈ s
⊢ ((f x).colon Set.univ).radical = ((f y).colon Set.univ).radical
have rw : ((f i).colon Set.univ).radical = ((f y).colon Set.univ).radical
Tactic: rw [hs' (mem_insert_of_mem hx), hs' (mem_insert_of_mem hy)]
-- Lean 4 proof step from Mathlib.RingTheory.IsPrimary (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
f : ι → Submodule R M
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι} (hi : i ∈ s) (hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary)
    (hs' : ∀ ⦃y : ι⦄, y ∈ s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical), (s.inf f).IsPrimary
i : ι
hi : i ∈ insert a s
hs : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical
y : ι
hy : y ∈ s
x : ι
hx : x ∈ s
rw : ((f i).colon Set.univ).radical = ((f y).colon Set.univ).radical
⊢ ((f x).colon Set.univ).radical = ((f y).colon Set.univ).radical
have rw₁ : ((f i).colon Set.univ).radical = ((f i).colon Set.univ).radical
Tactic: rw [hs' (mem_insert_of_mem hx), hs' (mem_insert_of_mem hy)]
-- Lean 4 proof step from Mathlib.RingTheory.IsPrimary (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
f : ι → Submodule R M
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι} (hi : i ∈ s) (hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary)
    (hs' : ∀ ⦃y : ι⦄, y ∈ s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical), (s.inf f).IsPrimary
i : ι
hi : i ∈ insert a s
hs : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical
y : ι
hy : y ∈ s
⊢ (f a ⊓ s.inf f).IsPrimary
have H : ∀ ⦃x : ι⦄ (hx : x ∈ s), ((f x).colon Set.univ).radical = ((f y).colon Set.univ).radical
Tactic: have H ⦃x⦄ (hx : x ∈ s) : ((f x).colon Set.univ).radical = ((f y).colon Set.univ).radical := by
      rw [hs' (mem_insert_of_mem hx), hs' (mem_insert_of_mem hy)]
-- Lean 4 proof step from Mathlib.RingTheory.IsPrimary (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
f : ι → Submodule R M
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι} (hi : i ∈ s) (hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary)
    (hs' : ∀ ⦃y : ι⦄, y ∈ s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical), (s.inf f).IsPrimary
i : ι
hi : i ∈ insert a s
hs : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical
y : ι
hy : y ∈ s
H : ∀ ⦃x : ι⦄ (hx : x ∈ s), ((f x).colon Set.univ).radical = ((f y).colon Set.univ).radical
⊢ (f a ⊓ s.inf f).IsPrimary
have insert : ((f a).colon Set.univ).radical = ((s.inf f).colon Set.univ).radical
Tactic: refine IsPrimary.inf (hs (by simp)) (IH hy (fun x hx ↦ hs (by simp [hx])) H) ?_
-- Lean 4 proof step from Mathlib.RingTheory.IsPrimary (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
f : ι → Submodule R M
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι} (hi : i ∈ s) (hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary)
    (hs' : ∀ ⦃y : ι⦄, y ∈ s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical), (s.inf f).IsPrimary
i : ι
hi : i ∈ insert a s
hs : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical
y : ι
hy : y ∈ s
H : ∀ ⦃x : ι⦄ (hx : x ∈ s), ((f x).colon Set.univ).radical = ((f y).colon Set.univ).radical
⊢ ((f a).colon Set.univ).radical = ((s.inf f).colon Set.univ).radical
have insert : ((f a).colon Set.univ).radical = radical (s.inf fun (i : ι) ↦ (f i).colon Set.univ)
Tactic: rw [colon_finsetInf, Ideal.radical_finset_inf hy H,
      hs' (mem_insert_self _ _), hs' (mem_insert_of_mem hy)]
-- Lean 4 proof step from Mathlib.RingTheory.IsPrimary (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
f : ι → Submodule R M
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι} (hi : i ∈ s) (hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary)
    (hs' : ∀ ⦃y : ι⦄, y ∈ s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical), (s.inf f).IsPrimary
i : ι
hi : i ∈ Insert.insert a s
hs : ∀ ⦃y : ι⦄, y ∈ Insert.insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ Insert.insert a s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical
y : ι
hy : y ∈ s
H : ∀ ⦃x : ι⦄ (hx : x ∈ s), ((f x).colon Set.univ).radical = ((f y).colon Set.univ).radical
insert : ((f a).colon Set.univ).radical = radical (s.inf fun (i : ι) ↦ (f i).colon Set.univ)
⊢ ((f a).colon Set.univ).radical = ((s.inf f).colon Set.univ).radical
have insert₁ : ((f a).colon Set.univ).radical = ((f y).colon Set.univ).radical
Tactic: rw [colon_finsetInf, Ideal.radical_finset_inf hy H,
      hs' (mem_insert_self _ _), hs' (mem_insert_of_mem hy)]
-- Lean 4 proof step from Mathlib.RingTheory.IsPrimary (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_3
f : ι → Submodule R M
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι} (hi : i ∈ s) (hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary)
    (hs' : ∀ ⦃y : ι⦄, y ∈ s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical), (s.inf f).IsPrimary
i : ι
hi : i ∈ Insert.insert a s
hs : ∀ ⦃y : ι⦄, y ∈ Insert.insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ Insert.insert a s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical
y : ι
hy : y ∈ s
H : ∀ ⦃x : ι⦄ (hx : x ∈ s), ((f x).colon Set.univ).radical = ((f y).colon Set.univ).radical
insert : ((f a).colon Set.univ).radical = radical (s.inf fun (i : ι) ↦ (f i).colon Set.univ)
insert₁ : ((f a).colon Set.univ).radical = ((f y).colon Set.univ).radical
⊢ ((f a).colon Set.univ).radical = ((s.inf f).colon Set.univ).radical
have insert₂ : ((f i).colon Set.univ).radical = ((f y).colon Set.univ).radical
Tactic: rw [colon_finsetInf, Ideal.radical_finset_inf hy H,
      hs' (mem_insert_self _ _), hs' (mem_insert_of_mem hy)]