awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
insert₂ : ((f i).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 i).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
s : Finset ι
f : ι → Submodule R M
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
have empty : ∀ {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: induction s using Finset.induction_on generalizing i with
  | empty => simp at hi
  | insert a s ha IH =>
    rcases s.eq_empty_or_nonempty with rfl | ⟨y, hy⟩
    · simp only [insert_empty_eq, mem_singleton] at hi
      simpa [hi] using hs
    simp only [inf_insert]
    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)]
    refine IsPrimary.inf (hs (by simp)) (IH hy (fun x hx ↦ hs (by simp [hx])) H) ?_
    rw [colon_finsetInf, Ideal.radical_finset_inf hy H,
      hs' (mem_insert_self _ _), hs' (mem_insert_of_mem hy)]
Cleared hypotheses: s, i, 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
s : Finset ι
f : ι → Submodule R M
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
empty :
  ∀ {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
⊢ (s.inf f).IsPrimary
have insert : ∀ (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
Tactic: induction s using Finset.induction_on generalizing i with
  | empty => simp at hi
  | insert a s ha IH =>
    rcases s.eq_empty_or_nonempty with rfl | ⟨y, hy⟩
    · simp only [insert_empty_eq, mem_singleton] at hi
      simpa [hi] using hs
    simp only [inf_insert]
    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)]
    refine IsPrimary.inf (hs (by simp)) (IH hy (fun x hx ↦ hs (by simp [hx])) H) ?_
    rw [colon_finsetInf, Ideal.radical_finset_inf hy H,
      hs' (mem_insert_self _ _), hs' (mem_insert_of_mem hy)]
Cleared hypotheses: s, i, 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
s : Finset ι
f : ι → Submodule R M
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
have empty : ∀ {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: classical
  induction s using Finset.induction_on generalizing i with
  | empty => simp at hi
  | insert a s ha IH =>
    rcases s.eq_empty_or_nonempty with rfl | ⟨y, hy⟩
    · simp only [insert_empty_eq, mem_singleton] at hi
      simpa [hi] using hs
    simp only [inf_insert]
    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)]
    refine IsPrimary.inf (hs (by simp)) (IH hy (fun x hx ↦ hs (by simp [hx])) H) ?_
    rw [colon_finsetInf, Ideal.radical_finset_inf hy H,
      hs' (mem_insert_self _ _), hs' (mem_insert_of_mem hy)]
Cleared hypotheses: s, i, 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
s : Finset ι
f : ι → Submodule R M
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
empty :
  ∀ {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
⊢ (s.inf f).IsPrimary
have insert : ∀ (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
Tactic: classical
  induction s using Finset.induction_on generalizing i with
  | empty => simp at hi
  | insert a s ha IH =>
    rcases s.eq_empty_or_nonempty with rfl | ⟨y, hy⟩
    · simp only [insert_empty_eq, mem_singleton] at hi
      simpa [hi] using hs
    simp only [inf_insert]
    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)]
    refine IsPrimary.inf (hs (by simp)) (IH hy (fun x hx ↦ hs (by simp [hx])) H) ?_
    rw [colon_finsetInf, Ideal.radical_finset_inf hy H,
      hs' (mem_insert_self _ _), hs' (mem_insert_of_mem hy)]
Cleared hypotheses: s, i, 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
S : Submodule R M
hI : S.IsPrimary
⊢ (S.colon Set.univ).radical.IsPrime
have refine : ∀ (h : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (r ^ n) ⊤ ≤ S) (x y : R),
  x * y ∈ (S.colon Set.univ).radical →
    ∀ (n : ℕ) (hn : (x * y) ^ n ∈ S.colon Set.univ), x ∈ (S.colon Set.univ).radical ∨ y ∈ (S.colon Set.univ).radical
Tactic: refine isPrime_iff.mpr <| hI.imp (by simp) fun h x y ⟨n, hn⟩ ↦ ?_
-- 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 : Submodule R M
hI : S.IsPrimary
h : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (r ^ n) ⊤ ≤ S
x y : R
h_1 : x * y ∈ (S.colon Set.univ).radical
n : ℕ
hn : (x * y) ^ n ∈ S.colon Set.univ
⊢ x ∈ (S.colon Set.univ).radical ∨ y ∈ (S.colon Set.univ).radical
have h₁ : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ r ∈ (S.colon (↑⊤ : Set M)).radical
Tactic: simp_rw [← mem_colon_iff_le, ← mem_radical_iff] at h
Cleared hypotheses: 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
S : Submodule R M
hI : S.IsPrimary
x y : R
h_1 : x * y ∈ (S.colon Set.univ).radical
n : ℕ
hn : (x * y) ^ n ∈ S.colon Set.univ
h : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ r ∈ (S.colon (↑⊤ : Set M)).radical
⊢ x ∈ (S.colon Set.univ).radical ∨ y ∈ (S.colon Set.univ).radical
have refine : ∀ (hx : x ∉ (S.colon Set.univ).radical), y ^ n ∈ S.colon Set.univ
Tactic: refine or_iff_not_imp_left.mpr fun hx ↦ ⟨n, ?_⟩
-- 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 : Submodule R M
hI : S.IsPrimary
x y : R
h_1 : x * y ∈ (S.colon Set.univ).radical
n : ℕ
hn : (x * y) ^ n ∈ S.colon Set.univ
h : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ r ∈ (S.colon (↑⊤ : Set M)).radical
hx : x ∉ (S.colon Set.univ).radical
⊢ y ^ n ∈ S.colon Set.univ
have simp : ∀ (hn : ∀ (s : M), x ^ n • y ^ n • s ∈ S) (s : M), y ^ n • s ∈ S
Tactic: simp only [mul_pow, mem_colon, Set.mem_univ, true_imp_iff, mul_smul] at hn ⊢
Cleared hypotheses: hn
-- 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 : Submodule R M
hS : S.IsPrimary
m : M
inst_3 : Decidable (m ∈ S)
⊢ (S.colon {m}).radical = if m ∈ S then ⊤ else (S.colon Set.univ).radical
have pos : ∀ (hm : m ∈ S), (S.colon {m}).radical = ⊤
Tactic: split_ifs with hm
-- 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 : Submodule R M
hS : S.IsPrimary
m : M
inst_3 : Decidable (m ∈ S)
pos : ∀ (hm : m ∈ S), (S.colon {m}).radical = ⊤
⊢ (S.colon {m}).radical = if m ∈ S then ⊤ else (S.colon Set.univ).radical
have neg : ∀ (hm : m ∉ S), (S.colon {m}).radical = (S.colon Set.univ).radical
Tactic: split_ifs with hm
-- 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 : Submodule R M
hS : S.IsPrimary
m : M
inst_3 : Decidable (m ∈ S)
hm : m ∈ S
⊢ (S.colon {m}).radical = ⊤
have pos : S.colon {m} = ⊤
Tactic: rwa [radical_eq_top, colon_eq_top_iff_subset, Set.singleton_subset_iff]
-- 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 : Submodule R M
hS : S.IsPrimary
m : M
inst_3 : Decidable (m ∈ S)
hm : m ∈ S
pos : S.colon {m} = ⊤
⊢ (S.colon {m}).radical = ⊤
have pos₁ : {m} ⊆ (↑S : Set M)
Tactic: rwa [radical_eq_top, colon_eq_top_iff_subset, Set.singleton_subset_iff]
-- 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 : Submodule R M
hS : S.IsPrimary
m : M
inst_3 : Decidable (m ∈ S)
hm : m ∈ S
pos : S.colon {m} = ⊤
pos₁ : {m} ⊆ (↑S : Set M)
⊢ (S.colon {m}).radical = ⊤
have pos₂ : m ∈ (↑S : Set M)
Tactic: rwa [radical_eq_top, colon_eq_top_iff_subset, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.IsPrimary (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submodule R M
⊢ S.IsPrimary ↔
    S ≠ ⊤ ∧ ∀ (r : R) (x : M ⧸ S), x ≠ 0 → r • x = 0 → ∃ (n : ℕ), HSMul.hSMul (β := Submodule R (M ⧸ S)) (r ^ n) ⊤ = ⊥
have refine : S ≠ ⊤ →
  ((∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (r ^ n) ⊤ ≤ S) ↔
    ∀ (r : R) (x : M ⧸ S), x ≠ 0 → r • x = 0 → ∃ (n : ℕ), HSMul.hSMul (β := Submodule R (M ⧸ S)) (r ^ n) ⊤ = ⊥)
Tactic: refine (and_congr_right fun _ ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.IsPrimary (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submodule R M
h : S ≠ ⊤
⊢ (∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (r ^ n) ⊤ ≤ S) ↔
    ∀ (r : R) (x : M ⧸ S), x ≠ 0 → r • x = 0 → ∃ (n : ℕ), HSMul.hSMul (β := Submodule R (M ⧸ S)) (r ^ n) ⊤ = ⊥
have simp_rw : (∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (r ^ n) ⊤ ≤ S) ↔
  ∀ (r : R), ∀ x ∉ S, r • x ∈ S → ∃ (n : ℕ), HSMul.hSMul (β := Submodule R (M ⧸ S)) (r ^ n) ⊤ = ⊥
Tactic: simp_rw [S.mkQ_surjective.forall, ← map_smul, ne_eq, ← LinearMap.mem_ker, ker_mkQ]
-- Lean 4 proof step from Mathlib.RingTheory.IsPrimary (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submodule R M
h : S ≠ ⊤
⊢ (∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (r ^ n) ⊤ ≤ S) ↔
    ∀ (r : R), ∀ x ∉ S, r • x ∈ S → ∃ (n : ℕ), HSMul.hSMul (β := Submodule R (M ⧸ S)) (r ^ n) ⊤ = ⊥
have a : ∀ (a : R) (a_1 : M),
  (a • a_1 ∈ S → a_1 ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ S) ↔
    a_1 ∉ S → a • a_1 ∈ S → ∃ (n : ℕ), HSMul.hSMul (β := Submodule R (M ⧸ S)) (a ^ n) ⊤ = ⊥
Tactic: congr! 2
-- Lean 4 proof step from Mathlib.RingTheory.IsPrimary (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submodule R M
h : S ≠ ⊤
a : R
a_1 : M
⊢ (a • a_1 ∈ S → a_1 ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ S) ↔
    a_1 ∉ S → a • a_1 ∈ S → ∃ (n : ℕ), HSMul.hSMul (β := Submodule R (M ⧸ S)) (a ^ n) ⊤ = ⊥
have a : (a • a_1 ∈ S → a_1 ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ S) ↔
  ∀ (b : a • a_1 ∈ S), a_1 ∈ S ∨ ∃ (n : ℕ), a ^ n • map S.mkQ ⊤ = ⊥
Tactic: rw [forall_comm, ← or_iff_not_imp_left,
    ← LinearMap.range_eq_top.mpr S.mkQ_surjective, ← map_top]
-- Lean 4 proof step from Mathlib.RingTheory.IsPrimary (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submodule R M
h : S ≠ ⊤
a : R
a_1 : M
⊢ (a • a_1 ∈ S → a_1 ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ S) ↔
    ∀ (b : a • a_1 ∈ S), a_1 ∈ S ∨ ∃ (n : ℕ), a ^ n • map S.mkQ ⊤ = ⊥
have a : (a • a_1 ∈ S → a_1 ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a ^ n) ⊤ ≤ S) ↔
  ∀ (b : a • a_1 ∈ S), a_1 ∈ S ∨ ∃ (n : ℕ), a ^ n • map S.mkQ ⊤ ≤ ⊥
Tactic: simp_rw [eq_bot_iff, ← map_pointwise_smul, map_le_iff_le_comap, comap_bot, ker_mkQ]
-- Lean 4 proof step from Mathlib.RingTheory.IsPrimary (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submodule R M
h : S ≠ ⊤
a_1 : R
a_2 : M
a :
  (a_1 • a_2 ∈ S → a_2 ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a_1 ^ n) ⊤ ≤ S) ↔
    ∀ (b : a_1 • a_2 ∈ S), a_2 ∈ S ∨ ∃ (n : ℕ), a_1 ^ n • map S.mkQ ⊤ ≤ ⊥
⊢ (a_1 • a_2 ∈ S → a_2 ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a_1 ^ n) ⊤ ≤ S) ↔
    ∀ (b : a_1 • a_2 ∈ S), a_2 ∈ S ∨ ∃ (n : ℕ), a_1 ^ n • map S.mkQ ⊤ = ⊥
have a₁ : (a_1 • a_2 ∈ S → a_2 ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a_1 ^ n) ⊤ ≤ S) ↔
  ∀ (b : a_1 • a_2 ∈ S), a_2 ∈ S ∨ ∃ (n : ℕ), map S.mkQ (HSMul.hSMul (β := Submodule R M) (a_1 ^ n) ⊤) ≤ ⊥
Tactic: simp_rw [eq_bot_iff, ← map_pointwise_smul, map_le_iff_le_comap, comap_bot, ker_mkQ]
-- Lean 4 proof step from Mathlib.RingTheory.IsPrimary (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submodule R M
h : S ≠ ⊤
a_1 : R
a_2 : M
a :
  (a_1 • a_2 ∈ S → a_2 ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a_1 ^ n) ⊤ ≤ S) ↔
    ∀ (b : a_1 • a_2 ∈ S), a_2 ∈ S ∨ ∃ (n : ℕ), a_1 ^ n • map S.mkQ ⊤ ≤ ⊥
a₁ :
  (a_1 • a_2 ∈ S → a_2 ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a_1 ^ n) ⊤ ≤ S) ↔
    ∀ (b : a_1 • a_2 ∈ S), a_2 ∈ S ∨ ∃ (n : ℕ), map S.mkQ (HSMul.hSMul (β := Submodule R M) (a_1 ^ n) ⊤) ≤ ⊥
⊢ (a_1 • a_2 ∈ S → a_2 ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a_1 ^ n) ⊤ ≤ S) ↔
    ∀ (b : a_1 • a_2 ∈ S), a_2 ∈ S ∨ ∃ (n : ℕ), a_1 ^ n • map S.mkQ ⊤ = ⊥
have a₂ : (a_1 • a_2 ∈ S → a_2 ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a_1 ^ n) ⊤ ≤ S) ↔
  ∀ (b : a_1 • a_2 ∈ S), a_2 ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a_1 ^ n) ⊤ ≤ comap S.mkQ ⊥
Tactic: simp_rw [eq_bot_iff, ← map_pointwise_smul, map_le_iff_le_comap, comap_bot, ker_mkQ]
-- Lean 4 proof step from Mathlib.RingTheory.IsPrimary (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
S : Submodule R M
h : S ≠ ⊤
a_1 : R
a_2 : M
a :
  (a_1 • a_2 ∈ S → a_2 ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a_1 ^ n) ⊤ ≤ S) ↔
    ∀ (b : a_1 • a_2 ∈ S), a_2 ∈ S ∨ ∃ (n : ℕ), a_1 ^ n • map S.mkQ ⊤ ≤ ⊥
a₁ :
  (a_1 • a_2 ∈ S → a_2 ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a_1 ^ n) ⊤ ≤ S) ↔
    ∀ (b : a_1 • a_2 ∈ S), a_2 ∈ S ∨ ∃ (n : ℕ), map S.mkQ (HSMul.hSMul (β := Submodule R M) (a_1 ^ n) ⊤) ≤ ⊥
a₂ :
  (a_1 • a_2 ∈ S → a_2 ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a_1 ^ n) ⊤ ≤ S) ↔
    ∀ (b : a_1 • a_2 ∈ S), a_2 ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a_1 ^ n) ⊤ ≤ comap S.mkQ ⊥
⊢ (a_1 • a_2 ∈ S → a_2 ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a_1 ^ n) ⊤ ≤ S) ↔
    ∀ (b : a_1 • a_2 ∈ S), a_2 ∈ S ∨ ∃ (n : ℕ), a_1 ^ n • map S.mkQ ⊤ = ⊥
have a₃ : (a_1 • a_2 ∈ S → a_2 ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a_1 ^ n) ⊤ ≤ S) ↔
  ∀ (b : a_1 • a_2 ∈ S), a_2 ∈ S ∨ ∃ (n : ℕ), HSMul.hSMul (β := Submodule R M) (a_1 ^ n) ⊤ ≤ S.mkQ.ker
Tactic: simp_rw [eq_bot_iff, ← map_pointwise_smul, map_le_iff_le_comap, comap_bot, ker_mkQ]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_4
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_8
inst_3 : AddCommMonoid N
inst_4 : Module R N
⊢ Function.Bijective (α := M ⊗[R] N) (β := M ⊗[R] N) (⇑(lift (mk R M N)) : (a : M ⊗[R] N) → M ⊗[R] N)
have h : Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N) (lift (mk R M N)) LinearMap.id
Tactic: convert_to Function.Bijective (LinearMap.id : M ⊗[R] N →ₗ[R] M ⊗[R] N) using 2
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_4
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_8
inst_3 : AddCommMonoid N
inst_4 : Module R N
h : Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N) (lift (mk R M N)) LinearMap.id
⊢ Function.Bijective (α := M ⊗[R] N) (β := M ⊗[R] N) (⇑(lift (mk R M N)) : (a : M ⊗[R] N) → M ⊗[R] N)
have convert_to : Function.Bijective (α := M ⊗[R] N) (β := M ⊗[R] N) (⇑LinearMap.id : (a : M ⊗[R] N) → M ⊗[R] N)
Tactic: convert_to Function.Bijective (LinearMap.id : M ⊗[R] N →ₗ[R] M ⊗[R] N) using 2
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_4
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_8
inst_3 : AddCommMonoid N
inst_4 : Module R N
⊢ Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N) (lift (mk R M N)) LinearMap.id
have h : ∀ (x : M) (y : N),
  Eq (α := M ⊗[R] N) ((lift (mk R M N) : (a : M ⊗[R] N) → M ⊗[R] N) (x ⊗ₜ[R] y) : M ⊗[R] N)
    ((LinearMap.id : (a : M ⊗[R] N) → M ⊗[R] N) (x ⊗ₜ[R] y) : M ⊗[R] N)
Tactic: apply TensorProduct.ext'
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
x₁ : M₁
x₂ : M₂
⊢ Eq (α := M₁ ⊗[R] M₂)
    ((h.equiv.symm : (a : M) → M₁ ⊗[R] M₂) ((((f : (a : M₁) → M₂ →ₗ[R] M) x₁ : M₂ →ₗ[R] M) : (a : M₂) → M) x₂) :
      M₁ ⊗[R] M₂)
    (x₁ ⊗ₜ[R] x₂ : M₁ ⊗[R] M₂)
have a : Eq.{u_4 + 1} (α := M)
  ((h.equiv : (a : M₁ ⊗[R] M₂) → M)
      ((h.equiv.symm : (a : M) → M₁ ⊗[R] M₂) ((((f : (a : M₁) → M₂ →ₗ[R] M) x₁ : M₂ →ₗ[R] M) : (a : M₂) → M) x₂) :
        M₁ ⊗[R] M₂) :
    M)
  ((h.equiv : (a : M₁ ⊗[R] M₂) → M) (x₁ ⊗ₜ[R] x₂) : M)
Tactic: apply h.equiv.injective
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
x₁ : M₁
x₂ : M₂
⊢ Eq.{u_4 + 1} (α := M)
    ((h.equiv : (a : M₁ ⊗[R] M₂) → M)
        ((h.equiv.symm : (a : M) → M₁ ⊗[R] M₂) ((((f : (a : M₁) → M₂ →ₗ[R] M) x₁ : M₂ →ₗ[R] M) : (a : M₂) → M) x₂) :
          M₁ ⊗[R] M₂) :
      M)
    ((h.equiv : (a : M₁ ⊗[R] M₂) → M) (x₁ ⊗ₜ[R] x₂) : M)
have a : Eq.{u_4 + 1} (α := M) ((((f : (a : M₁) → M₂ →ₗ[R] M) x₁ : M₂ →ₗ[R] M) : (a : M₂) → M) x₂ : M)
  ((h.equiv : (a : M₁ ⊗[R] M₂) → M) (x₁ ⊗ₜ[R] x₂) : M)
Tactic: refine (h.equiv.apply_symm_apply _).trans ?_
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
⊢ motive m
have rw : motive ((↑h.equiv : M₁ ⊗[R] M₂ →ₗ[R] M).toFun (h.equiv.invFun m))
Tactic: rw [← h.equiv.right_inv m]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
⊢ motive ((↑h.equiv : M₁ ⊗[R] M₂ →ₗ[R] M).toFun (h.equiv.invFun m))
have generalize : ∀ (y : M₁ ⊗[R] M₂), motive ((↑h.equiv : M₁ ⊗[R] M₂ →ₗ[R] M).toFun y)
Tactic: generalize h.equiv.invFun m = y
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
y : M₁ ⊗[R] M₂
⊢ motive ((↑h.equiv : M₁ ⊗[R] M₂ →ₗ[R] M).toFun y)
have change : motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) y)
Tactic: change motive (TensorProduct.lift f y)
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
x : M₁
y : M₂
⊢ motive ((TensorProduct.lift f : (a : M₁ ⊗[R] M₂) → M) (x ⊗ₜ[R] y))
have tmul₁ : motive ((((f : (a : M₁) → M₂ →ₗ[R] M) x : M₂ →ₗ[R] M) : (a : M₂) → M) y)
Tactic: rw [TensorProduct.lift.tmul]