awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f_1 : R[X]
h_1 : IsAdjoinRootMonic S f_1
inst_3 : Module.Finite R S
inst_4 : Free R S
α : S
hα : Eq (α := Subalgebra R S) R[α] ⊤
f : R[X] := minpoly R α
hf : Monic (minpoly R α)
φ : AdjoinRoot f →ₐ[R] S := AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α ⋯
hφ : Function.Surjective.{u + 1, v + 1} (α := AdjoinRoot f) (β := S) (⇑φ : (a : AdjoinRoot f) → S)
this_1 : Free R (AdjoinRoot (minpoly R α))
this : Module.Finite R (AdjoinRoot (minpoly R α))
h : Nontrivial R
e : AdjoinRoot f ≃ₗ[R] S := LinearEquiv.ofFinrankEq (AdjoinRoot f) S ⋯
⊢ Function.Bijective.{u + 1, v + 1} (α := AdjoinRoot (minpoly R α)) (β := S) (⇑φ : (a : AdjoinRoot (minpoly R α)) → S)

Tactic:
OrzechProperty.bijective_of_surjective_of_injective
          e.toLinearMap φ e.injective hφ

Premises used: AdjoinRoot, Quotient.liftOn', Set.Mem, AddCon.liftOn, SemilinearMapClass.semilinearMap, LinearEquiv.toLinearMap, Submodule.quotientRel, AddAction.orbitRel, LinearEquiv.injective, AddCon.Quotient, OrzechProperty.bijective_of_surjective_of_injective
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f_1 : R[X]
h_1 : IsAdjoinRootMonic S f_1
inst_3 : Module.Finite R S
inst_4 : Free R S
α : S
hα : Eq (α := Subalgebra R S) R[α] ⊤
f : R[X] := minpoly R α
hf : Monic (minpoly R α)
φ : AdjoinRoot f →ₐ[R] S := AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α ⋯
hφ : Function.Surjective.{u + 1, v + 1} (α := AdjoinRoot f) (β := S) (⇑φ : (a : AdjoinRoot f) → S)
this_1 : Free R (AdjoinRoot (minpoly R α))
this : Module.Finite R (AdjoinRoot (minpoly R α))
h : Nontrivial R
e : AdjoinRoot f ≃ₗ[R] S := LinearEquiv.ofFinrankEq (AdjoinRoot f) S ⋯
⊢ Function.Bijective.{u + 1, v + 1} (α := AdjoinRoot (minpoly R α)) (β := S) (⇑φ : (a : AdjoinRoot (minpoly R α)) → S)

Tactic:
exact OrzechProperty.bijective_of_surjective_of_injective
          e.toLinearMap φ e.injective hφ

Premises used: SemilinearMapClass.semilinearMap, LinearEquiv.toLinearMap, LinearEquiv.injective, OrzechProperty.bijective_of_surjective_of_injective
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f_1 : R[X]
h_1 : IsAdjoinRootMonic S f_1
inst_3 : Module.Finite R S
inst_4 : Free R S
α : S
hα : Eq (α := Subalgebra R S) R[α] ⊤
f : R[X] := minpoly R α
hf : Monic (minpoly R α)
φ : AdjoinRoot f →ₐ[R] S := AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α ⋯
hφ : Function.Surjective.{u + 1, v + 1} (α := AdjoinRoot f) (β := S) (⇑φ : (a : AdjoinRoot f) → S)
this_1 : Free R (AdjoinRoot (minpoly R α))
this : Module.Finite R (AdjoinRoot (minpoly R α))
h : ¬Nontrivial R
⊢ Subsingleton R

Tactic:
apply not_nontrivial_iff_subsingleton.mp at h

Premises used: not_nontrivial_iff_subsingleton, Iff.mp
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f_1 : R[X]
h_1 : IsAdjoinRootMonic S f_1
inst_3 : Module.Finite R S
inst_4 : Free R S
α : S
hα : Eq (α := Subalgebra R S) R[α] ⊤
f : R[X] := minpoly R α
hf : Monic (minpoly R α)
φ : AdjoinRoot f →ₐ[R] S := AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α ⋯
hφ : Function.Surjective.{u + 1, v + 1} (α := AdjoinRoot f) (β := S) (⇑φ : (a : AdjoinRoot f) → S)
this_1 : Free R (AdjoinRoot (minpoly R α))
this : Module.Finite R (AdjoinRoot (minpoly R α))
h : Subsingleton R
⊢ Subsingleton.{u + 1} (AdjoinRoot f)

Tactic:
haveI := Module.subsingleton R (AdjoinRoot f)
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f_1 : R[X]
h_1 : IsAdjoinRootMonic S f_1
inst_3 : Module.Finite R S
inst_4 : Free R S
α : S
hα : Eq (α := Subalgebra R S) R[α] ⊤
f : R[X] := minpoly R α
hf : Monic (minpoly R α)
φ : AdjoinRoot f →ₐ[R] S := AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α ⋯
hφ : Function.Surjective.{u + 1, v + 1} (α := AdjoinRoot f) (β := S) (⇑φ : (a : AdjoinRoot f) → S)
this_1 : Free R (AdjoinRoot (minpoly R α))
this_2 : Module.Finite R (AdjoinRoot (minpoly R α))
h : Subsingleton R
this : Subsingleton.{u + 1} (AdjoinRoot f)
⊢ Function.Bijective.{u + 1, v + 1} (α := AdjoinRoot (minpoly R α)) (β := S) (⇑φ : (a : AdjoinRoot (minpoly R α)) → S)

Tactic:
⟨Function.injective_of_subsingleton φ, hφ⟩

Premises used: Function.injective_of_subsingleton, And.intro, Function.Bijective, DFunLike.coe
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
f_1 : R[X]
h_1 : IsAdjoinRootMonic S f_1
inst_3 : Module.Finite R S
inst_4 : Free R S
α : S
hα : Eq (α := Subalgebra R S) R[α] ⊤
f : R[X] := minpoly R α
hf : Monic (minpoly R α)
φ : AdjoinRoot f →ₐ[R] S := AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α ⋯
hφ : Function.Surjective.{u + 1, v + 1} (α := AdjoinRoot f) (β := S) (⇑φ : (a : AdjoinRoot f) → S)
this_1 : Free R (AdjoinRoot (minpoly R α))
this_2 : Module.Finite R (AdjoinRoot (minpoly R α))
h : Subsingleton R
this : Subsingleton.{u + 1} (AdjoinRoot f)
⊢ Function.Bijective.{u + 1, v + 1} (α := AdjoinRoot (minpoly R α)) (β := S) (⇑φ : (a : AdjoinRoot (minpoly R α)) → S)

Tactic:
exact ⟨Function.injective_of_subsingleton φ, hφ⟩
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
inst_4 : Free R S
α : S
hα : Eq (α := Subalgebra R S) R[α] ⊤
⊢ (mkOfAdjoinEqTop' hα).root = α

Tactic:
simp [IsAdjoinRoot.root]

Premises used: IsAdjoinRoot.root
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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
⊢ IsDomain.{u} (AdjoinRoot (minpoly R x))

Tactic:
have := isDomain_of_prime (prime_of_isIntegrallyClosed hx')
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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))
⊢ IsTorsionFree R (AdjoinRoot (minpoly R x))

Tactic:
have :=
    noZeroSMulDivisors_of_prime_of_degree_ne_zero (prime_of_isIntegrallyClosed hx')
      (degree_pos hx').ne'
-- Module: Mathlib.RingTheory.IsAdjoinRoot
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)
rw₇ rw₈ : Eq (α := R[X]) (minpoly R x) (minpoly R x)
⊢ Eq (α := R[X]) (minpoly R x) (minpoly R (powerBasis' hx').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')]

Premises used: AdjoinRoot.isAdjoinRoot_root_eq_root, minpoly.monic, AdjoinRoot.powerBasis'_gen, AdjoinRoot.isAdjoinRootMonic, AdjoinRoot.isAdjoinRootMonic_toAdjoinRoot, PowerBasis.minpolyGen_map, PowerBasis.minpolyGen_eq, Algebra.adjoin.powerBasis', minpoly.irreducible, IsAdjoinRootMonic.minpoly_eq
-- Module: Mathlib.RingTheory.IsAdjoinRoot
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
f : F[X]
h : IsAdjoinRoot E f
⊢ Eq (α := IntermediateField F E) F⟮h.root⟯ ⊤

Tactic:
IntermediateField.adjoin_eq_top_of_algebra F {h.root} (adjoin_root_eq_top h)

Premises used: IsAdjoinRoot.root, IntermediateField.adjoin_eq_top_of_algebra, Singleton.singleton, IsAdjoinRoot.adjoin_root_eq_top
-- Module: Mathlib.RingTheory.IsPrimary
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Submodule R M
h : S.IsPrimary
⊢ S ≠ ⊤

Tactic:
h.left

Premises used: And.left
-- Module: Mathlib.RingTheory.IsPrimary
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Submodule R M
h : S.IsPrimary
r : R
m : M
hrm : r • m ∈ S
⊢ m ∈ S ∨ r ∈ (S.colon Set.univ).radical

Tactic:
h.right hrm

Premises used: Set.Mem, Set.univ, setOf, Set.Subset, And.right
-- Module: Mathlib.RingTheory.IsPrimary
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 ≠ ⊤

Tactic:
obtain ⟨_, hS⟩ := hS
-- Module: Mathlib.RingTheory.IsPrimary
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 ≠ ⊤
⊢ ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (r ^ n) ⊤ ≤ S

Tactic:
obtain ⟨_, hS⟩ := hS
-- Module: Mathlib.RingTheory.IsPrimary
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
⊢ T ≠ ⊤

Tactic:
obtain ⟨_, hT⟩ := hT
-- Module: Mathlib.RingTheory.IsPrimary
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 ≠ ⊤
⊢ ∀ {r : R} {x : M}, r • x ∈ T → x ∈ T ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (r ^ n) ⊤ ≤ T

Tactic:
obtain ⟨_, hT⟩ := hT
-- Module: Mathlib.RingTheory.IsPrimary
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 ≠ ⊤

Tactic:
grind
-- Module: Mathlib.RingTheory.IsPrimary
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
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
⊢ (S ⊓ T).IsPrimary

Tactic:
refine ⟨by grind, fun ⟨hS', hT'⟩ ↦ ?_⟩
-- Module: Mathlib.RingTheory.IsPrimary
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)
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)
⊢ x ∈ S ⊓ T ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (r ^ n) ⊤ ≤ S ⊓ T

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 ⊢

Premises used: Ideal.radical_inf, and_or_right, Submodule.mem_colon_iff_le, Submodule.mem_inf, Ideal.mem_radical_iff, Submodule.top_coe, Submodule.inf_colon, inf_idem
-- Module: Mathlib.RingTheory.IsPrimary
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 ≠ ⊤
left_1 : T ≠ ⊤
r : R
x : M
h_1 : r • x ∈ S ⊓ T
hS' : r • x ∈ (↑S : Set M)
hT' : r • x ∈ (↑T : Set M)
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:
⟨hS hS', hT hT'⟩

Premises used: And.intro
-- Module: Mathlib.RingTheory.IsPrimary
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 ≠ ⊤
left_1 : T ≠ ⊤
r : R
x : M
h_1 : r • x ∈ S ⊓ T
hS' : r • x ∈ (↑S : Set M)
hT' : r • x ∈ (↑T : Set M)
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:
exact ⟨hS hS', hT hT'⟩
-- Module: Mathlib.RingTheory.IsPrimary
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
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

Tactic:
simp at hi
-- Module: Mathlib.RingTheory.IsPrimary
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₁ : ∀ (y : ι) (hy : y ∈ s), ((Insert.insert a s).inf f).IsPrimary
⊢ ((Insert.insert a s).inf f).IsPrimary

Tactic:
rcases s.eq_empty_or_nonempty with rfl | ⟨y, hy⟩

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.RingTheory.IsPrimary
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
⊢ i = a

Tactic:
simp only [insert_empty_eq, mem_singleton] at hi

Premises used: Finset.mem_singleton, LawfulSingleton.insert_empty_eq
-- Module: Mathlib.RingTheory.IsPrimary
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
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
hi : i = a
⊢ (inf (insert a ∅) f).IsPrimary

Tactic:
simpa [hi] using hs
-- Module: Mathlib.RingTheory.IsPrimary
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
insert : (f a ⊓ s.inf f).IsPrimary
⊢ ((Insert.insert a s).inf f).IsPrimary

Tactic:
simp only [inf_insert]

Premises used: Finset.inf_insert
-- Module: Mathlib.RingTheory.IsPrimary
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
rw₁ rw₂ : ((f i).colon Set.univ).radical = ((f i).colon Set.univ).radical
⊢ ((f x).colon Set.univ).radical = ((f y).colon Set.univ).radical

Tactic:
rw [hs' (mem_insert_of_mem hx), hs' (mem_insert_of_mem hy)]

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.RingTheory.IsPrimary
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

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)]
-- Module: Mathlib.RingTheory.IsPrimary
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
⊢ a ∈ insert a s

Tactic:
simp
-- Module: Mathlib.RingTheory.IsPrimary
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
x : ι
hx : x ∈ s
⊢ x ∈ insert a s

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.IsPrimary
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 = ((s.inf f).colon Set.univ).radical
⊢ (f a ⊓ s.inf f).IsPrimary

Tactic:
refine IsPrimary.inf (hs (by simp)) (IH hy (fun x hx ↦ hs (by simp [hx])) H) ?_

Premises used: Submodule.IsPrimary.inf
-- Module: Mathlib.RingTheory.IsPrimary
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
insert₂ : ((f i).colon Set.univ).radical = ((f y).colon Set.univ).radical
insert₃ insert₄ : ((f i).colon Set.univ).radical = ((f i).colon Set.univ).radical
⊢ ((f a).colon Set.univ).radical = ((s.inf f).colon Set.univ).radical

Tactic:
rw [colon_finsetInf, Ideal.radical_finset_inf hy H,
      hs' (mem_insert_self _ _), hs' (mem_insert_of_mem hy)]

Premises used: Finset.mem_insert_self, Submodule.colon_finsetInf, Finset.mem_insert_of_mem, Ideal.radical_finset_inf