awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
n : ℕ
f : Fin n → M
hf : Eq (α := Submodule R M) (Submodule.span R (Set.range f)) ⊤
s : Set ℕ := {m : ℕ | Ne (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m)) ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
hs : sSup s ∈ s
refine :
  Eq (α :=
    Submodule R (HasQuotient.Quotient M (B := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s))))) ⊤
    (Submodule.span R
      (singleton (α :=
        HasQuotient.Quotient M (B := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s))))
        ((Submodule.mkQ (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s))) :
              (a : M) → M ⧸ Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s)))
            (f ⟨sSup s, ⋯⟩) :
          HasQuotient.Quotient M (B := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s))))))
⊢ ∃ (N : Submodule R M), N ≠ ⊤ ∧ Submodule.IsPrincipal.{u_1, u_2} (R := R) (M := M ⧸ N) ⊤

Tactic:
refine ⟨_, hs, ⟨⟨Submodule.mkQ _ (f ⟨_, hns _ hs⟩), ?_⟩⟩⟩
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
n : ℕ
f : Fin n → M
hf : Eq (α := Submodule R M) (Submodule.span R (Set.range f)) ⊤
s : Set ℕ := {m : ℕ | Ne (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m)) ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
hs : sSup s ∈ s
⊢ Eq (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (Order.succ (sSup s)))) ⊤

Tactic:
have := not_not.mp (notMem_of_csSup_lt (Order.lt_succ _) hs₂)
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
n : ℕ
f : Fin n → M
hf : Eq (α := Submodule R M) (Submodule.span R (Set.range f)) ⊤
s : Set ℕ := {m : ℕ | Ne (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m)) ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
hs : sSup s ∈ s
this : Eq (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (Order.succ (sSup s)))) ⊤
rw :
  Eq (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' {sSup s} ∪ f '' Fin.val ⁻¹' Set.Iio (sSup s)))
    (Submodule.span R (f '' {(⟨sSup s, ⋯⟩ : Fin n)} ∪ f '' Fin.val ⁻¹' Set.Iio (sSup s)))
⊢ Eq (α :=
    Submodule R (HasQuotient.Quotient M (B := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s))))) ⊤
    (Submodule.span R
      (singleton (α :=
        HasQuotient.Quotient M (B := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s))))
        ((Submodule.mkQ (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s))) :
              (a : M) → M ⧸ Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s)))
            (f ⟨sSup s, ⋯⟩) :
          HasQuotient.Quotient M (B := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (sSup s))))))

Tactic:
rw [← Set.image_singleton, ← Submodule.map_span,
    ← (Submodule.comap_injective_of_surjective (Submodule.mkQ_surjective _)).eq_iff,
    Submodule.comap_map_eq, Submodule.ker_mkQ, Submodule.comap_top, ← this, ← Submodule.span_union,
    Order.Iio_succ_eq_insert (sSup s), ← Set.union_singleton, Set.preimage_union, Set.image_union,
    ← @Set.image_singleton _ _ f, Set.union_comm]

Premises used: Set.image_singleton, Order.Iio_succ_eq_insert, Function.Injective.eq_iff, Set.union_comm, Submodule.comap_injective_of_surjective, Set.preimage_union, Submodule.span_union, Submodule.ker_mkQ, Submodule.mkQ_surjective, Submodule.map_span, Set.union_singleton, Submodule.comap_top, SupSet.sSup, Set.image_union, Submodule.comap_map_eq
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
n : ℕ
f : Fin n → M
hf : Eq (α := Submodule R M) (Submodule.span R (Set.range f)) ⊤
s : Set ℕ := {m : ℕ | Ne (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m)) ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
hs : sSup s ∈ s
this : Eq (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (Order.succ (sSup s)))) ⊤
h : Eq (α := Set (Fin n)) (Fin.val ⁻¹' {sSup s}) {(⟨sSup s, ⋯⟩ : Fin n)}
⊢ Eq (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' {sSup s} ∪ f '' Fin.val ⁻¹' Set.Iio (sSup s)))
    (Submodule.span R (f '' {(⟨sSup s, ⋯⟩ : Fin n)} ∪ f '' Fin.val ⁻¹' Set.Iio (sSup s)))

Tactic:
congr!
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
n : ℕ
f : Fin n → M
hf : Eq (α := Submodule R M) (Submodule.span R (Set.range f)) ⊤
s : Set ℕ := {m : ℕ | Ne (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m)) ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
hs : sSup s ∈ s
this : Eq (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (Order.succ (sSup s)))) ⊤
h :
  ∀ (x : Fin n),
    Membership.mem (γ := Set (Fin n)) (Fin.val ⁻¹' {sSup s}) x ↔
      Membership.mem (γ := Set (Fin n)) {(⟨sSup s, ⋯⟩ : Fin n)} x
⊢ Eq (α := Set (Fin n)) (Fin.val ⁻¹' {sSup s}) {(⟨sSup s, ⋯⟩ : Fin n)}

Tactic:
ext
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
n : ℕ
f : Fin n → M
hf : Eq (α := Submodule R M) (Submodule.span R (Set.range f)) ⊤
s : Set ℕ := {m : ℕ | Ne (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio m)) ⊤}
hns : ∀ x ∈ s, x < n
hs₁ : s.Nonempty
hs₂ : BddAbove s
hs : sSup s ∈ s
this : Eq (α := Submodule R M) (Submodule.span R (f '' Fin.val ⁻¹' Set.Iio (Order.succ (sSup s)))) ⊤
x : Fin n
⊢ Membership.mem (γ := Set (Fin n)) (Fin.val ⁻¹' {sSup s}) x ↔
    Membership.mem (γ := Set (Fin n)) {(⟨sSup s, ⋯⟩ : Fin n)} x

Tactic:
simp [Fin.ext_iff]

Premises used: Fin.ext_iff
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
obtain :
  ∀ (N : Submodule R M) (hN : N ≠ ⊤) (x : M ⧸ N) (hx : Eq (α := Submodule R (M ⧸ N)) ⊤ (R ∙ x)),
    ∃ (I : Ideal R) (f : M →ₗ[R] R ⧸ I),
      I ≠ ⊤ ∧ Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R ⧸ I) (⇑f : (a : M) → R ⧸ I)
⊢ ∃ (I : Ideal R) (f : M →ₗ[R] R ⧸ I),
    I ≠ ⊤ ∧ Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R ⧸ I) (⇑f : (a : M) → R ⧸ I)

Tactic:
obtain ⟨N, hN, ⟨x, hx⟩⟩ := Module.exists_isPrincipal_quotient_of_finite R M

Premises used: Module.exists_isPrincipal_quotient_of_finite
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
N : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : Eq (α := Submodule R (M ⧸ N)) ⊤ (R ∙ x)
rw : Eq (α := Submodule R (M ⧸ N)) (LinearMap.range (LinearMap.toSpanSingleton R (M ⧸ N) x)) ⊤
rw₁ : Eq (α := Submodule R (M ⧸ N)) (R ∙ x) ⊤
rw₂ rw₃ : Eq (α := Submodule R (M ⧸ N)) (R ∙ x) (R ∙ x)
⊢ Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := M ⧸ N) (⇑(LinearMap.toSpanSingleton R (M ⧸ N) x) : (a : R) → M ⧸ N)

Tactic:
rw [← LinearMap.range_eq_top, ← LinearMap.span_singleton_eq_range, hx]

Premises used: LinearMap.range_eq_top, LinearMap.span_singleton_eq_range
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
N : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : Eq (α := Submodule R (M ⧸ N)) ⊤ (R ∙ x)
f : LinearEquiv.{u_1, u_1, u_1, u_2} (RingHom.id R)
  (HasQuotient.Quotient R (B := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) x))) (M ⧸ N) :=
  LinearMap.quotKerEquivOfSurjective (LinearMap.toSpanSingleton R (M ⧸ N) x) ⋯
⊢ ∃ (I : Ideal R) (f : M →ₗ[R] R ⧸ I),
    I ≠ ⊤ ∧ Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R ⧸ I) (⇑f : (a : M) → R ⧸ I)

Tactic:
⟨_, f.symm.toLinearMap.comp N.mkQ, fun e ↦ ?_, f.symm.surjective.comp N.mkQ_surjective⟩

Premises used: LinearEquiv.symm, LinearEquiv.surjective, LinearMap.comp, LinearEquiv.toLinearMap, And.intro, Exists.intro, Function.Surjective.comp, Submodule.mkQ, Submodule.mkQ_surjective
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
N : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : Eq (α := Submodule R (M ⧸ N)) ⊤ (R ∙ x)
f : LinearEquiv.{u_1, u_1, u_1, u_2} (RingHom.id R)
  (HasQuotient.Quotient R (B := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) x))) (M ⧸ N) :=
  LinearMap.quotKerEquivOfSurjective (LinearMap.toSpanSingleton R (M ⧸ N) x) ⋯
refine : ∀ (e : Eq (α := Ideal R) (LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) x)) ⊤), False
⊢ ∃ (I : Ideal R) (f : M →ₗ[R] R ⧸ I),
    I ≠ ⊤ ∧ Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R ⧸ I) (⇑f : (a : M) → R ⧸ I)

Tactic:
refine ⟨_, f.symm.toLinearMap.comp N.mkQ, fun e ↦ ?_, f.symm.surjective.comp N.mkQ_surjective⟩
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
N : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : Eq (α := Submodule R (M ⧸ N)) ⊤ (R ∙ x)
f : LinearEquiv.{u_1, u_1, u_1, u_2} (RingHom.id R)
  (HasQuotient.Quotient R (B := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) x))) (M ⧸ N) :=
  LinearMap.quotKerEquivOfSurjective (LinearMap.toSpanSingleton R (M ⧸ N) x) ⋯
e : Eq (α := Ideal R) (LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) x)) ⊤
⊢ x = 0

Tactic:
simpa using LinearMap.congr_fun (LinearMap.ker_eq_top.mp e) 1

Premises used: LinearMap.ker_eq_top, LinearMap.congr_fun, Iff.mp, OfNat.ofNat
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
N : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : Eq (α := Submodule R (M ⧸ N)) ⊤ (R ∙ x)
f : LinearEquiv.{u_1, u_1, u_1, u_2} (RingHom.id R)
  (HasQuotient.Quotient R (B := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) x))) (M ⧸ N) :=
  LinearMap.quotKerEquivOfSurjective (LinearMap.toSpanSingleton R (M ⧸ N) x) ⋯
e : Eq (α := Ideal R) (LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) x)) ⊤
⊢ Eq (α := Submodule R (M ⧸ N)) ⊤ (R ∙ 0)

Tactic:
obtain rfl : x = 0 := by simpa using LinearMap.congr_fun (LinearMap.ker_eq_top.mp e) 1

Premises used: rfl
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
N : Submodule R M
hN : N ≠ ⊤
x : M ⧸ N
hx : Eq (α := Submodule R (M ⧸ N)) ⊤ (R ∙ x)
f : LinearEquiv.{u_1, u_1, u_1, u_2} (RingHom.id R)
  (HasQuotient.Quotient R (B := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) x))) (M ⧸ N) :=
  LinearMap.quotKerEquivOfSurjective (LinearMap.toSpanSingleton R (M ⧸ N) x) ⋯
e : Eq (α := Ideal R) (LinearMap.ker (LinearMap.toSpanSingleton R (M ⧸ N) x)) ⊤
hx₁ : Eq (α := Submodule R (M ⧸ N)) ⊤ (R ∙ 0)
⊢ Eq (α := Ideal R) (LinearMap.ker.{u_1, u_1, u_1, u_2} (M₂ := M ⧸ N) (LinearMap.toSpanSingleton R (M ⧸ N) 0)) ⊤

Tactic:
obtain rfl : x = 0 := by simpa using LinearMap.congr_fun (LinearMap.ker_eq_top.mp e) 1

Premises used: rfl
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
N : Submodule R M
hN : N ≠ ⊤
hx : Eq (α := Submodule R (M ⧸ N)) ⊤ (R ∙ 0)
f : LinearEquiv.{u_1, u_1, u_1, u_2} (RingHom.id R)
  (HasQuotient.Quotient R (B := Submodule R R)
    (LinearMap.ker.{u_1, u_1, u_1, u_2} (M₂ := M ⧸ N) (LinearMap.toSpanSingleton R (M ⧸ N) 0)))
  (M ⧸ N) :=
  LinearMap.quotKerEquivOfSurjective (LinearMap.toSpanSingleton R (M ⧸ N) 0) ⋯
e : Eq (α := Ideal R) (LinearMap.ker.{u_1, u_1, u_1, u_2} (M₂ := M ⧸ N) (LinearMap.toSpanSingleton R (M ⧸ N) 0)) ⊤
rwa rwa₁ rwa₂ rwa₃ : N ≠ ⊤
⊢ Nontrivial.{u_2} (M ⧸ N)

Tactic:
rwa [Submodule.Quotient.nontrivial_iff]

Premises used: Submodule.Quotient.nontrivial_iff
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
N : Submodule R M
hN : N ≠ ⊤
hx : Eq (α := Submodule R (M ⧸ N)) ⊤ (R ∙ 0)
f : LinearEquiv.{u_1, u_1, u_1, u_2} (RingHom.id R)
  (HasQuotient.Quotient R (B := Submodule R R)
    (LinearMap.ker.{u_1, u_1, u_1, u_2} (M₂ := M ⧸ N) (LinearMap.toSpanSingleton R (M ⧸ N) 0)))
  (M ⧸ N) :=
  LinearMap.quotKerEquivOfSurjective (LinearMap.toSpanSingleton R (M ⧸ N) 0) ⋯
e : Eq (α := Ideal R) (LinearMap.ker.{u_1, u_1, u_1, u_2} (M₂ := M ⧸ N) (LinearMap.toSpanSingleton R (M ⧸ N) 0)) ⊤
⊢ Nontrivial.{u_2} (M ⧸ N)

Tactic:
have : Nontrivial (M ⧸ N) := by rwa [Submodule.Quotient.nontrivial_iff]
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
N : Submodule R M
hN : N ≠ ⊤
hx : Eq (α := Submodule R (M ⧸ N)) ⊤ (R ∙ 0)
f : LinearEquiv.{u_1, u_1, u_1, u_2} (RingHom.id R)
  (HasQuotient.Quotient R (B := Submodule R R)
    (LinearMap.ker.{u_1, u_1, u_1, u_2} (M₂ := M ⧸ N) (LinearMap.toSpanSingleton R (M ⧸ N) 0)))
  (M ⧸ N) :=
  LinearMap.quotKerEquivOfSurjective (LinearMap.toSpanSingleton R (M ⧸ N) 0) ⋯
e : Eq (α := Ideal R) (LinearMap.ker.{u_1, u_1, u_1, u_2} (M₂ := M ⧸ N) (LinearMap.toSpanSingleton R (M ⧸ N) 0)) ⊤
this : Nontrivial.{u_2} (M ⧸ N)
⊢ False

Tactic:
simp at hx
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
obtain :
  ∀ (I : Ideal R) (ϕ : M →ₗ[R] R ⧸ I) (hI : I ≠ ⊤)
    (hϕ : Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R ⧸ I) (⇑ϕ : (a : M) → R ⧸ I)), Nontrivial.{u_2} (M ⊗[R] M)
⊢ Nontrivial.{u_2} (M ⊗[R] M)

Tactic:
obtain ⟨I, ϕ, hI, hϕ⟩ := Module.exists_surjective_quotient_of_finite R M

Premises used: Module.exists_surjective_quotient_of_finite
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
I : Ideal R
ϕ : M →ₗ[R] R ⧸ I
hI : I ≠ ⊤
hϕ : Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R ⧸ I) (⇑ϕ : (a : M) → R ⧸ I)
ψ : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (M ⊗[R] M) (R ⧸ I) := LinearMap.mul' R (R ⧸ I) ∘ₗ map ϕ ϕ
rwa rwa₁ rwa₂ rwa₃ : I ≠ ⊤
⊢ Nontrivial.{u_1} (R ⧸ I)

Tactic:
rwa [Submodule.Quotient.nontrivial_iff]

Premises used: Submodule.Quotient.nontrivial_iff
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
I : Ideal R
ϕ : M →ₗ[R] R ⧸ I
hI : I ≠ ⊤
hϕ : Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R ⧸ I) (⇑ϕ : (a : M) → R ⧸ I)
ψ : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (M ⊗[R] M) (R ⧸ I) := LinearMap.mul' R (R ⧸ I) ∘ₗ map ϕ ϕ
⊢ Nontrivial.{u_1} (R ⧸ I)

Tactic:
have : Nontrivial (R ⧸ I) := by rwa [Submodule.Quotient.nontrivial_iff]
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
I : Ideal R
ϕ : M →ₗ[R] R ⧸ I
hI : I ≠ ⊤
hϕ : Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R ⧸ I) (⇑ϕ : (a : M) → R ⧸ I)
ψ : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (M ⊗[R] M) (R ⧸ I) := LinearMap.mul' R (R ⧸ I) ∘ₗ map ϕ ϕ
this : Nontrivial.{u_1} (R ⧸ I)
x : R ⧸ I
obtain :
  ∀ (x : M),
    ∃ (a : M ⊗[R] M),
      Eq.{u_1 + 1} (α := R ⧸ I) ((ψ : (a : M ⊗[R] M) → R ⧸ I) a : R ⧸ I) ((ϕ : (a : M) → R ⧸ I) x : R ⧸ I)
⊢ ∃ (a : M ⊗[R] M), (ψ : (a : M ⊗[R] M) → R ⧸ I) a = x

Tactic:
obtain ⟨x, rfl⟩ := hϕ x

Premises used: rfl
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
I : Ideal R
ϕ : M →ₗ[R] R ⧸ I
hI : I ≠ ⊤
hϕ : Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R ⧸ I) (⇑ϕ : (a : M) → R ⧸ I)
ψ : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (M ⊗[R] M) (R ⧸ I) := LinearMap.mul' R (R ⧸ I) ∘ₗ map ϕ ϕ
this : Nontrivial.{u_1} (R ⧸ I)
x : M
obtain :
  ∀ (y : M) (hy : Eq.{u_1 + 1} (α := R ⧸ I) ((ϕ : (a : M) → R ⧸ I) y : R ⧸ I) (1 : R ⧸ I)),
    ∃ (a : M ⊗[R] M),
      Eq.{u_1 + 1} (α := R ⧸ I) ((ψ : (a : M ⊗[R] M) → R ⧸ I) a : R ⧸ I) ((ϕ : (a : M) → R ⧸ I) x : R ⧸ I)
⊢ ∃ (a : M ⊗[R] M), Eq.{u_1 + 1} (α := R ⧸ I) ((ψ : (a : M ⊗[R] M) → R ⧸ I) a : R ⧸ I) ((ϕ : (a : M) → R ⧸ I) x : R ⧸ I)

Tactic:
obtain ⟨y, hy⟩ := hϕ 1

Premises used: OfNat.ofNat
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
I : Ideal R
ϕ : M →ₗ[R] R ⧸ I
hI : I ≠ ⊤
hϕ : Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R ⧸ I) (⇑ϕ : (a : M) → R ⧸ I)
ψ : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (M ⊗[R] M) (R ⧸ I) := LinearMap.mul' R (R ⧸ I) ∘ₗ map ϕ ϕ
this : Nontrivial.{u_1} (R ⧸ I)
x y : M
hy : Eq.{u_1 + 1} (α := R ⧸ I) ((ϕ : (a : M) → R ⧸ I) y : R ⧸ I) (1 : R ⧸ I)
⊢ Eq.{u_1 + 1} (α := R ⧸ I) ((ψ : (a : M ⊗[R] M) → R ⧸ I) (x ⊗ₜ[R] y) : R ⧸ I) ((ϕ : (a : M) → R ⧸ I) x : R ⧸ I)

Tactic:
simp [ψ, hy]
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
I : Ideal R
ϕ : M →ₗ[R] R ⧸ I
hI : I ≠ ⊤
hϕ : Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R ⧸ I) (⇑ϕ : (a : M) → R ⧸ I)
ψ : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (M ⊗[R] M) (R ⧸ I) := LinearMap.mul' R (R ⧸ I) ∘ₗ map ϕ ϕ
this : Nontrivial.{u_1} (R ⧸ I)
x y : M
hy : Eq.{u_1 + 1} (α := R ⧸ I) ((ϕ : (a : M) → R ⧸ I) y : R ⧸ I) (1 : R ⧸ I)
⊢ ∃ (a : M ⊗[R] M), Eq.{u_1 + 1} (α := R ⧸ I) ((ψ : (a : M ⊗[R] M) → R ⧸ I) a : R ⧸ I) ((ϕ : (a : M) → R ⧸ I) x : R ⧸ I)

Tactic:
exact ⟨x ⊗ₜ y, by simp [ψ, hy]⟩
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
I : Ideal R
ϕ : M →ₗ[R] R ⧸ I
hI : I ≠ ⊤
hϕ : Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R ⧸ I) (⇑ϕ : (a : M) → R ⧸ I)
ψ : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (M ⊗[R] M) (R ⧸ I) := LinearMap.mul' R (R ⧸ I) ∘ₗ map ϕ ϕ
this : Nontrivial.{u_1} (R ⧸ I)
⊢ Surjective.{u_2 + 1, u_1 + 1} (α := M ⊗[R] M) (β := R ⧸ I) (⇑ψ : (a : M ⊗[R] M) → R ⧸ I)

Tactic:
have : Function.Surjective ψ := by
    intro x; obtain ⟨x, rfl⟩ := hϕ x; obtain ⟨y, hy⟩ := hϕ 1; exact ⟨x ⊗ₜ y, by simp [ψ, hy]⟩
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
I : Ideal R
ϕ : M →ₗ[R] R ⧸ I
hI : I ≠ ⊤
hϕ : Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R ⧸ I) (⇑ϕ : (a : M) → R ⧸ I)
ψ : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (M ⊗[R] M) (R ⧸ I) := LinearMap.mul' R (R ⧸ I) ∘ₗ map ϕ ϕ
this_1 : Nontrivial.{u_1} (R ⧸ I)
this : Surjective.{u_2 + 1, u_1 + 1} (α := M ⊗[R] M) (β := R ⧸ I) (⇑ψ : (a : M ⊗[R] M) → R ⧸ I)
⊢ Nontrivial.{u_2} (M ⊗[R] M)

Tactic:
this.nontrivial

Premises used: Function.Surjective.nontrivial
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Nontrivial M
I : Ideal R
ϕ : M →ₗ[R] R ⧸ I
hI : I ≠ ⊤
hϕ : Surjective.{u_2 + 1, u_1 + 1} (α := M) (β := R ⧸ I) (⇑ϕ : (a : M) → R ⧸ I)
ψ : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (M ⊗[R] M) (R ⧸ I) := LinearMap.mul' R (R ⧸ I) ∘ₗ map ϕ ϕ
this_1 : Nontrivial.{u_1} (R ⧸ I)
this : Surjective.{u_2 + 1, u_1 + 1} (α := M ⊗[R] M) (β := R ⧸ I) (⇑ψ : (a : M ⊗[R] M) → R ⧸ I)
⊢ Nontrivial.{u_2} (M ⊗[R] M)

Tactic:
exact this.nontrivial

Premises used: Function.Surjective.nontrivial
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
inst_2 : Algebra K L
E1 E2 : Subalgebra K L
inst_3 : Module.Finite.{u_1, u_2} K ↥E1
inst_4 : Module.Finite.{u_1, u_2} K ↥E2
rw : Module.Finite.{u_1, u_2} K ↥(Algebra.TensorProduct.productMap E1.val E2.val).range
⊢ Module.Finite.{u_1, u_2} K ↥(E1 ⊔ E2)

Tactic:
rw [← E1.range_val, ← E2.range_val, ← Algebra.TensorProduct.productMap_range]

Premises used: Subalgebra.range_val, Algebra.TensorProduct.productMap_range
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
inst_2 : Algebra K L
E1 E2 : Subalgebra K L
inst_3 : Module.Finite.{u_1, u_2} K ↥E1
inst_4 : Module.Finite.{u_1, u_2} K ↥E2
⊢ Module.Finite.{u_1, u_2} K ↥(Algebra.TensorProduct.productMap E1.val E2.val).range

Tactic:
Module.Finite.range (Algebra.TensorProduct.productMap E1.val E2.val).toLinearMap

Premises used: AlgHom.toLinearMap, Quotient.liftOn', Set.Mem, AddCon.liftOn, Subalgebra.val, LinearMap.range, Module.Finite.range, Algebra.TensorProduct.productMap, TensorProduct, Subsemiring.copy, AlgHom.range, Submodule.copy, RingHom.rangeS
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
K : Type u_1
L : Type u_2
inst : CommSemiring K
inst_1 : CommSemiring L
inst_2 : Algebra K L
E1 E2 : Subalgebra K L
inst_3 : Module.Finite.{u_1, u_2} K ↥E1
inst_4 : Module.Finite.{u_1, u_2} K ↥E2
⊢ Module.Finite.{u_1, u_2} K ↥(Algebra.TensorProduct.productMap E1.val E2.val).range

Tactic:
exact Module.Finite.range (Algebra.TensorProduct.productMap E1.val E2.val).toLinearMap

Premises used: AlgHom.toLinearMap, Subalgebra.val, Module.Finite.range, Algebra.TensorProduct.productMap
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R S'
f : S →ₐ[R] S'
Hf : f.Finite
this : Algebra S S' := f.toAlgebra
⊢ IsScalarTower R S S'

Tactic:
have := IsScalarTower.of_algebraMap_eq' f.comp_algebraMap.symm
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R S'
f : S →ₐ[R] S'
Hf : f.Finite
this_1 : Algebra S S' := f.toAlgebra
this : IsScalarTower R S S'
⊢ Module.Finite S S'

Tactic:
have : Module.Finite S S' := finite_algebraMap.mp Hf
-- Module: Mathlib.RingTheory.TensorProduct.Finite
Goal:
R : Type u_1
S : Type u_2
S' : Type u_3
T : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R T
inst_6 : Algebra R S'
f : S →ₐ[R] S'
Hf : f.Finite
this_1 : Algebra S S' := f.toAlgebra
this_2 : IsScalarTower R S S'
this : Module.Finite S S'
change :
  AlgHom.Finite (R := S) (A := TensorProduct R S T) (B := TensorProduct R S' T)
    (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T))
⊢ Finite (A := TensorProduct R S T) (B := TensorProduct R S' T)
    (AlgHom.toRingHom (Algebra.TensorProduct.map f (AlgHom.id R T) : TensorProduct R S T →ₐ[R] TensorProduct R S' T))

Tactic:
change (Algebra.TensorProduct.map (Algebra.ofId S S') (AlgHom.id R T)).Finite

Premises used: AlgHom.Finite, Algebra.TensorProduct.map, AlgHom.id, Algebra.ofId