awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
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.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.insert a s).inf f).IsPrimary
⊢ (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)]

Premises used: Finset.mem_singleton, Submodule.colon_finsetInf, Insert.insert, Finset.inf_insert, LawfulSingleton.insert_empty_eq, 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
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
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.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.insert a s).inf f).IsPrimary
⊢ (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)]

Premises used: Finset.mem_singleton, Submodule.colon_finsetInf, Insert.insert, Finset.inf_insert, LawfulSingleton.insert_empty_eq, 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
S : Submodule R M
hI : S.IsPrimary
⊢ S ≠ ⊤ → (S.colon Set.univ).radical ≠ ⊤

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
S : Submodule R M
hI : S.IsPrimary
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
⊢ (S.colon Set.univ).radical.IsPrime

Tactic:
refine isPrime_iff.mpr <| hI.imp (by simp) fun h x y ⟨n, hn⟩ ↦ ?_

Premises used: Iff.mpr, And.imp, Ideal.isPrime_iff
-- 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
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
⊢ ∀ {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

Premises used: Submodule.mem_colon_iff_le, Ideal.mem_radical_iff
-- 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
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

Tactic:
or_iff_not_imp_left.mpr fun hx ↦ ⟨n, ?_⟩

Premises used: Iff.mpr, Classical.or_iff_not_imp_left, Exists.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 : 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
refine : ∀ (hx : x ∉ (S.colon Set.univ).radical), y ^ n ∈ S.colon Set.univ
⊢ x ∈ (S.colon Set.univ).radical ∨ y ∈ (S.colon Set.univ).radical

Tactic:
refine or_iff_not_imp_left.mpr fun hx ↦ ⟨n, ?_⟩

Premises used: Iff.mpr, Classical.or_iff_not_imp_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
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
simp : ∀ (hn : ∀ (s : M), x ^ n • y ^ n • s ∈ S) (s : M), y ^ n • s ∈ S
⊢ y ^ n ∈ S.colon Set.univ

Tactic:
simp only [mul_pow, mem_colon, Set.mem_univ, true_imp_iff, mul_smul] at hn ⊢

Premises used: true_imp_iff, Set.mem_univ, Submodule.mem_colon, mul_pow, SemigroupAction.mul_smul
-- 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
hI : S.IsPrimary
x y : R
h_1 : x * y ∈ (S.colon Set.univ).radical
n : ℕ
h : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ r ∈ (S.colon (↑⊤ : Set M)).radical
hx : x ∉ (S.colon Set.univ).radical
hn : ∀ (s : M), x ^ n • y ^ n • s ∈ S
⊢ ∀ (s : M), y ^ n • s ∈ S

Tactic:
fun p ↦ (h (hn p)).resolve_right (mt mem_radical_of_pow_mem hx)

Premises used: Set.Mem, mt, Ideal.mem_radical_of_pow_mem, Or.resolve_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 : Submodule R M
hI : S.IsPrimary
x y : R
h_1 : x * y ∈ (S.colon Set.univ).radical
n : ℕ
h : ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ r ∈ (S.colon (↑⊤ : Set M)).radical
hx : x ∉ (S.colon Set.univ).radical
hn : ∀ (s : M), x ^ n • y ^ n • s ∈ S
⊢ ∀ (s : M), y ^ n • s ∈ S

Tactic:
exact fun p ↦ (h (hn p)).resolve_right (mt mem_radical_of_pow_mem hx)

Premises used: mt, Ideal.mem_radical_of_pow_mem, Or.resolve_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 : Submodule R M
hI : S.IsPrimary
m : M
hm : m ∉ S
⊢ (S.colon {m}).radical = (S.colon Set.univ).radical

Tactic:
le_antisymm (radical_le_radical_iff.mpr fun _ hy ↦
    (hI.2 (Submodule.mem_colon_singleton.mp hy)).resolve_left hm)
    (radical_mono (Submodule.colon_mono le_rfl (Set.subset_univ {m})))

Premises used: Ideal.radical_mono, Iff.mpr, le_rfl, Set.subset_univ, Or.resolve_left, le_antisymm, And.right, Ideal.radical_le_radical_iff, Submodule.colon_mono, Iff.mp, Submodule.mem_colon_singleton, Singleton.singleton
-- 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
hS : S.IsPrimary
m : M
inst_3 : Decidable (m ∈ S)
pos : ∀ (hm : m ∈ S), (S.colon {m}).radical = ⊤
neg : ∀ (hm : m ∉ S), (S.colon {m}).radical = (S.colon Set.univ).radical
⊢ (S.colon {m}).radical = if m ∈ S then ⊤ else (S.colon Set.univ).radical

Tactic:
split_ifs with hm
-- 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
hS : S.IsPrimary
m : M
inst_3 : Decidable (m ∈ S)
hm : m ∈ S
pos : S.colon {m} = ⊤
pos₁ : {m} ⊆ (↑S : Set M)
pos₂ pos₃ pos₄ pos₅ : m ∈ (↑S : Set M)
⊢ (S.colon {m}).radical = ⊤

Tactic:
rwa [radical_eq_top, colon_eq_top_iff_subset, Set.singleton_subset_iff]

Premises used: Set.singleton_subset_iff, Submodule.colon_eq_top_iff_subset, Ideal.radical_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
hS : S.IsPrimary
m : M
inst_3 : Decidable (m ∈ S)
hm : m ∉ S
⊢ (S.colon {m}).radical = (S.colon Set.univ).radical

Tactic:
hS.radical_colon_singleton_of_notMem hm

Premises used: Submodule.IsPrimary.radical_colon_singleton_of_notMem
-- 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
hS : S.IsPrimary
m : M
inst_3 : Decidable (m ∈ S)
hm : m ∉ S
⊢ (S.colon {m}).radical = (S.colon Set.univ).radical

Tactic:
exact hS.radical_colon_singleton_of_notMem hm

Premises used: Submodule.IsPrimary.radical_colon_singleton_of_notMem
-- Module: Mathlib.RingTheory.IsPrimary
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) ⊤ = ⊥

Tactic:
(and_congr_right fun _ ↦ ?_)

Premises used: Submodule.IsPrimary, and_congr_right
-- Module: Mathlib.RingTheory.IsPrimary
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
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) ⊤ = ⊥)
⊢ S.IsPrimary ↔
    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 _ ↦ ?_)

Premises used: and_congr_right
-- Module: Mathlib.RingTheory.IsPrimary
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 ≠ ⊤
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) ⊤ = ⊥
⊢ (∀ {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:
simp_rw [S.mkQ_surjective.forall, ← map_smul, ne_eq, ← LinearMap.mem_ker, ker_mkQ]

Premises used: Function.Surjective.forall, ne_eq, LinearMap.mem_ker, Submodule.ker_mkQ, Submodule.mkQ_surjective, map_smul
-- Module: Mathlib.RingTheory.IsPrimary
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 :
  ∀ (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) ⊤ = ⊥
⊢ (∀ {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:
congr! 2
-- Module: Mathlib.RingTheory.IsPrimary
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) ↔
    a_2 ∉ S → a_1 • a_2 ∈ S → ∃ (n : ℕ), HSMul.hSMul (β := Submodule R (M ⧸ S)) (a_1 ^ n) ⊤ = ⊥

Tactic:
rw [forall_comm, ← or_iff_not_imp_left,
    ← LinearMap.range_eq_top.mpr S.mkQ_surjective, ← map_top]

Premises used: Iff.mpr, Submodule.map_top, forall_comm, LinearMap.range_eq_top, Classical.or_iff_not_imp_left, Submodule.mkQ_surjective
-- Module: Mathlib.RingTheory.IsPrimary
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₃ :
  (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
⊢ (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 ⊤ = ⊥

Tactic:
simp_rw [eq_bot_iff, ← map_pointwise_smul, map_le_iff_le_comap, comap_bot, ker_mkQ]

Premises used: Submodule.map_pointwise_smul, Submodule.ker_mkQ, Submodule.map_le_iff_le_comap, eq_bot_iff, Submodule.comap_bot
-- Module: Mathlib.RingTheory.IsTensorProduct
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
convert_to : Function.Bijective (α := M ⊗[R] N) (β := M ⊗[R] N) (⇑LinearMap.id : (a : M ⊗[R] N) → M ⊗[R] N)
⊢ Function.Bijective (α := M ⊗[R] N) (β := M ⊗[R] N) (⇑(lift (mk R M N)) : (a : M ⊗[R] N) → M ⊗[R] N)

Tactic:
convert_to Function.Bijective (LinearMap.id : M ⊗[R] N →ₗ[R] M ⊗[R] N) using 2

Premises used: LinearMap.id, Function.Bijective, DFunLike.coe
-- Module: Mathlib.RingTheory.IsTensorProduct
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 :
  ∀ (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)
⊢ Eq (α := M ⊗[R] N →ₗ[R] M ⊗[R] N) (lift (mk R M N)) LinearMap.id

Tactic:
apply TensorProduct.ext'

Premises used: TensorProduct.ext'
-- Module: Mathlib.RingTheory.IsTensorProduct
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
⊢ ∀ (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:
simp
-- Module: Mathlib.RingTheory.IsTensorProduct
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) (⇑LinearMap.id : (a : M ⊗[R] N) → M ⊗[R] N)

Tactic:
Function.bijective_id

Premises used: Function.bijective_id
-- Module: Mathlib.RingTheory.IsTensorProduct
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) (⇑LinearMap.id : (a : M ⊗[R] N) → M ⊗[R] N)

Tactic:
exact Function.bijective_id

Premises used: Function.bijective_id
-- Module: Mathlib.RingTheory.IsTensorProduct
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
⊢ (↑h.equiv : M₁ ⊗[R] M₂ →ₗ[R] M) = lift f

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, TensorProduct.lift, rfl
-- Module: Mathlib.RingTheory.IsTensorProduct
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₂
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)
⊢ 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₂)

Tactic:
apply h.equiv.injective

Premises used: IsTensorProduct.equiv, LinearEquiv.injective
-- Module: Mathlib.RingTheory.IsTensorProduct
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)

Tactic:
(h.equiv.apply_symm_apply _).trans ?_

Premises used: IsTensorProduct.equiv, LinearEquiv.apply_symm_apply, Eq.trans
-- Module: Mathlib.RingTheory.IsTensorProduct
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₂
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)
⊢ 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:
refine (h.equiv.apply_symm_apply _).trans ?_

Premises used: IsTensorProduct.equiv, LinearEquiv.apply_symm_apply, Eq.trans
-- Module: Mathlib.RingTheory.IsTensorProduct
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) ((((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:
simp
-- Module: Mathlib.RingTheory.IsTensorProduct
Goal:
R : Type u_1
inst : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
M' : Type u_5
inst_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R M₁
inst_6 : Module R M₂
inst_7 : Module R M
inst_8 : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
f' : M₁ →ₗ[R] M₂ →ₗ[R] M'
x₁ : M₁
x₂ : M₂
⊢ Eq.{u_5 + 1} (α := M')
    ((h.lift f' : (a : M) → M') ((((f : (a : M₁) → M₂ →ₗ[R] M) x₁ : M₂ →ₗ[R] M) : (a : M₂) → M) x₂ : M) : M')
    ((((f' : (a : M₁) → M₂ →ₗ[R] M') x₁ : M₂ →ₗ[R] M') : (a : M₂) → M') x₂ : M')

Tactic:
simp [lift]

Premises used: IsTensorProduct.lift
-- Module: Mathlib.RingTheory.IsTensorProduct
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
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst_7 : AddCommMonoid N₁
inst_8 : AddCommMonoid N₂
inst_9 : AddCommMonoid N
inst_10 : Module R N₁
inst_11 : Module R N₂
inst_12 : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
hf : IsTensorProduct f
hg : IsTensorProduct g
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
x₁ : M₁
x₂ : M₂
⊢ Eq.{u_8 + 1} (α := N)
    ((hf.map hg i₁ i₂ : (a : M) → N) ((((f : (a : M₁) → M₂ →ₗ[R] M) x₁ : M₂ →ₗ[R] M) : (a : M₂) → M) x₂ : M) : N)
    ((((g : (a : N₁) → N₂ →ₗ[R] N) ((i₁ : (a : M₁) → N₁) x₁) : N₂ →ₗ[R] N) : (a : N₂) → N)
        ((i₂ : (a : M₂) → N₂) x₂ : N₂) :
      N)

Tactic:
simp [map]

Premises used: IsTensorProduct.map
-- Module: Mathlib.RingTheory.IsTensorProduct
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)
rw : motive ((↑h.equiv : M₁ ⊗[R] M₂ →ₗ[R] M).toFun (h.equiv.invFun m))
⊢ motive m

Tactic:
rw [← h.equiv.right_inv m]

Premises used: LinearEquiv.right_inv, IsTensorProduct.equiv
-- Module: Mathlib.RingTheory.IsTensorProduct
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)
generalize : ∀ (y : M₁ ⊗[R] M₂), motive ((↑h.equiv : M₁ ⊗[R] M₂ →ₗ[R] M).toFun y)
⊢ motive ((↑h.equiv : M₁ ⊗[R] M₂ →ₗ[R] M).toFun (h.equiv.invFun m))

Tactic:
generalize h.equiv.invFun m = y

Premises used: IsTensorProduct.equiv, LinearEquiv.invFun