awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_7
P : Type u_6
inst_3 : Semiring S
inst_4 : AddCommMonoid P
inst_5 : Module S P
σ : R →+* S
inst_6 : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : Function.Bijective.{u_4 + 1, u_6 + 1} (α := M) (β := P) (⇑f : (a : M) → P)
h : Module.Finite S P
rwa : f.range.FG
rwa₁ : FG.{u_7, u_6} (R := S) (M := P) ⊤
rwa₂ rwa₃ rwa₄ rwa₅ : Module.Finite S P
⊢ (map f ⊤).FG

Tactic:
rwa [Submodule.map_top, LinearMap.range_eq_top.mpr hf.surjective, ← Module.finite_def]

Premises used: Iff.mpr, Submodule.map_top, LinearMap.range_eq_top, Module.finite_def, Function.Bijective.surjective
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R_1 : Type u_1
A_1 : Type u_2
B : Type u_3
M_1 : Type u_4
N_1 : Type u_5
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid N_1
inst_4 : Module R_1 N_1
R : Type u_6
A : Type u_7
M : Type u_8
inst_5 : Semiring R
inst_6 : AddCommGroup M
inst_7 : Ring A
inst_8 : Module A M
inst_9 : Module R M
inst_10 : SMul R A
inst_11 : IsScalarTower R A M
inst_12 : Module.Finite R M
N : Submodule A M
⊢ Module.Finite.{u_6, u_8} R (M ⧸ N)

Tactic:
Module.Finite.of_surjective (N.mkQ.restrictScalars R) N.mkQ_surjective

Premises used: Module.Finite.of_surjective, LinearMap.restrictScalars, Submodule.mkQ, Submodule.mkQ_surjective
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module.Finite R M
f : M →ₗ[R] N
⊢ Module.Finite.{u_1, u_5} R ↥f.range

Tactic:
of_surjective (SemilinearMapClass.semilinearMap f).rangeRestrict
    fun ⟨_, y, hy⟩ => ⟨y, Subtype.ext hy⟩

Premises used: Module.Finite.of_surjective, Exists, LinearMap.rangeRestrict, SemilinearMapClass.semilinearMap, Exists.intro, _private.0.Module.Finite.range.match_1, Eq, DFunLike.coe, Subtype.ext
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
p : Submodule R M
inst_5 : Module.Finite.{u_1, u_4} R ↥p
f : M →ₗ[R] N
⊢ Module.Finite.{u_1, u_5} R ↥(Submodule.map f p)

Tactic:
of_surjective (f.restrict fun _ ↦ mem_map_of_mem) fun ⟨_, _, hy, hy'⟩ ↦ ⟨⟨_, hy⟩, Subtype.ext hy'⟩

Premises used: _private.0.Module.Finite.map.match_1, Module.Finite.of_surjective, Exists, LinearMap.restrict, Subtype.mk, Exists.intro, Submodule.mem_map_of_mem, Eq, DFunLike.coe, Subtype.ext
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M_1 : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M_1
inst_2 : Module R M_1
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_6
M : ι → Type u_7
inst_5 : Finite ι
inst_6 : (i : ι) → AddCommMonoid (M i)
inst_7 : (i : ι) → Module.{u_1, u_7} R (M i)
h : ∀ (i : ι), Module.Finite.{u_1, u_7} R (M i)
rw : FG (R := R) (M := (i : ι) → M i) (Submodule.pi (φ := M) univ fun (i : ι) ↦ ⊤)
rw₁ : Set ι
⊢ FG (R := R) (M := (i : ι) → M i) ⊤

Tactic:
rw [← pi_top]

Premises used: Submodule.pi_top
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M_1 : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M_1
inst_2 : Module R M_1
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_6
M : ι → Type u_7
inst_5 : Finite ι
inst_6 : (i : ι) → AddCommMonoid (M i)
inst_7 : (i : ι) → Module.{u_1, u_7} R (M i)
h : ∀ (i : ι), Module.Finite.{u_1, u_7} R (M i)
⊢ FG (R := R) (M := (i : ι) → M i) (Submodule.pi (φ := M) univ fun (i : ι) ↦ ⊤)

Tactic:
fg_pi fun i => (h i).fg_top

Premises used: Submodule.fg_pi, Module.Finite.fg_top
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_6
M : ι → Type u_7
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_1, u_7} R (M i)
inst_3 : Module.Finite R ((i : ι) → M i)
i : ι
⊢ Module.Finite.{u_1, u_7} R (M i)

Tactic:
of_surjective _ <| LinearMap.proj_surjective i

Premises used: Module.Finite.of_surjective, LinearMap.proj_surjective
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_6
M : ι → Type u_7
inst_1 : Finite ι
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_7} R (M i)
⊢ Module.Finite R ((i : ι) → M i) ↔ ∀ (i : ι), Module.Finite.{u_1, u_7} R (M i)

Tactic:
⟨fun _ i => of_pi M i, fun _ => inferInstance⟩

Premises used: inferInstance, Iff.intro, Module.Finite.of_pi
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq (α := Ideal R) (Ideal.span (↑{1} : Set R)) ⊤

Tactic:
simpa only [Finset.coe_singleton] using Ideal.span_singleton_one

Premises used: Finset.coe_singleton, Ideal.span_singleton_one
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
⊢ Module.Finite R R

Tactic:
⟨Ideal.fg_top R⟩

Premises used: Ideal.fg_top, Module.Finite.of_fg_top
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_6
A : Type u_7
M : Type u_8
inst : Semiring R
inst_1 : Semiring A
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module A M
inst_5 : SMul R A
inst_6 : IsScalarTower R A M
hM : Module.Finite R M
rw :
  ∀ (hM : ∃ (S : Set M), S.Finite ∧ Eq (α := Submodule R M) (span R S) ⊤),
    ∃ (S : Set M), S.Finite ∧ Eq (α := Submodule A M) (span A S) ⊤
⊢ Module.Finite A M

Tactic:
rw [finite_def, fg_def] at hM ⊢

Premises used: Submodule.fg_def, Module.finite_def
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_6
A : Type u_7
M : Type u_8
inst : Semiring R
inst_1 : Semiring A
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module A M
inst_5 : SMul R A
inst_6 : IsScalarTower R A M
hM : ∃ (S : Set M), S.Finite ∧ Eq (α := Submodule R M) (span R S) ⊤
obtain :
  ∀ (S : Set M) (hSfin : S.Finite) (hSgen : Eq (α := Submodule R M) (span R S) ⊤),
    ∃ (S : Set M), S.Finite ∧ Eq (α := Submodule A M) (span A S) ⊤
⊢ ∃ (S : Set M), S.Finite ∧ Eq (α := Submodule A M) (span A S) ⊤

Tactic:
obtain ⟨S, hSfin, hSgen⟩ := hM
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_6
A : Type u_7
M : Type u_8
inst : Semiring R
inst_1 : Semiring A
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module A M
inst_5 : SMul R A
inst_6 : IsScalarTower R A M
S : Set M
hSfin : S.Finite
hSgen : Eq (α := Submodule R M) (span R S) ⊤
⊢ ∃ (S : Set M), S.Finite ∧ Eq (α := Submodule A M) (span A S) ⊤

Tactic:
⟨S, hSfin, eq_top_iff.mpr ?_⟩

Premises used: Iff.mpr, eq_top_iff, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_6
A : Type u_7
M : Type u_8
inst : Semiring R
inst_1 : Semiring A
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module A M
inst_5 : SMul R A
inst_6 : IsScalarTower R A M
S : Set M
hSfin : S.Finite
hSgen : Eq (α := Submodule R M) (span R S) ⊤
refine : LE.le (α := Submodule A M) ⊤ (span A S)
⊢ ∃ (S : Set M), S.Finite ∧ Eq (α := Submodule A M) (span A S) ⊤

Tactic:
refine ⟨S, hSfin, eq_top_iff.mpr ?_⟩
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_6
A : Type u_7
M : Type u_8
inst : Semiring R
inst_1 : Semiring A
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module A M
inst_5 : SMul R A
inst_6 : IsScalarTower R A M
S : Set M
hSfin : S.Finite
hSgen : Eq (α := Submodule R M) (span R S) ⊤
⊢ LE.le (α := Submodule R M) (span R S) (restrictScalars R (span A S))

Tactic:
have := span_le_restrictScalars R A S
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_6
A : Type u_7
M : Type u_8
inst : Semiring R
inst_1 : Semiring A
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module A M
inst_5 : SMul R A
inst_6 : IsScalarTower R A M
S : Set M
hSfin : S.Finite
hSgen : Eq (α := Submodule R M) (span R S) ⊤
this : LE.le (α := Submodule R M) (span R S) (restrictScalars R (span A S))
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : LE.le (α := Submodule R M) ⊤ (restrictScalars R (span A S))), LE.le (α := Submodule A M) ⊤ (span A S)
⊢ LE.le (α := Submodule A M) ⊤ (span A S)

Tactic:
rwa [hSgen] at this
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module.Finite R M
e : M ≃ₗ[R] N
⊢ Module.Finite R N

Tactic:
of_surjective (e : M →ₗ[R] N) e.surjective

Premises used: Module.Finite.of_surjective, LinearEquiv.surjective, LinearEquiv.toLinearMap
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
e : M ≃ₗ[R] N
⊢ Module.Finite R M ↔ Module.Finite R N

Tactic:
⟨fun _ ↦ equiv e, fun _ ↦ equiv e.symm⟩

Premises used: LinearEquiv.symm, Iff.intro, Module.Finite.equiv
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module.Finite R M
⊢ Module.Finite.{u_1, u_4} R Mᵐᵒᵖ

Tactic:
equiv (MulOpposite.opLinearEquiv R)

Premises used: MulOpposite.opLinearEquiv, Module.Finite.equiv
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module.Finite R M
⊢ Module.Finite R (ULift.{u_6, u_4} M)

Tactic:
equiv ULift.moduleEquiv.symm

Premises used: LinearEquiv.symm, ULift.moduleEquiv, Module.Finite.equiv
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module.Finite R M
inst_6 : Small.{u, u_4} M
⊢ Module.Finite.{u_1, u} R (Shrink.{u, u_4} M)

Tactic:
Module.Finite.equiv (Shrink.linearEquiv R M).symm

Premises used: LinearEquiv.symm, Shrink.linearEquiv, Module.Finite.equiv
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
⊢ Module.Finite.{u_1, u_4} R ↥N ↔ N.FG

Tactic:
finite_def.trans N.fg_top

Premises used: Module.finite_def, Submodule.fg_top, Iff.trans
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
inst_3 : Module.Finite.{u_1, u_4} R ↥N
⊢ N.FG

Tactic:
iff_fg.mp ‹_›

Premises used: Iff.mp, Module.Finite.iff_fg
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
⊢ Module.Finite.{u_1, u_4} R ↥⊥

Tactic:
.of_fg fg_bot

Premises used: Module.Finite.of_fg, Submodule.fg_bot
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module.Finite R M
⊢ Module.Finite.{u_1, u_4} R ↥⊤

Tactic:
.of_fg fg_top

Premises used: Module.Finite.fg_top, Module.Finite.of_fg
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module.Finite R M
⊢ Module.Finite.{u_1, u_4} (↥⊤) M

Tactic:
have : RingHomSurjective (Subsemiring.topEquiv (R := R)).symm.toRingHom :=
    RingHomSurjective.instToRingHomRingEquiv Subsemiring.topEquiv.symm
  of_surjective (σ := (Subsemiring.topEquiv (R := R)).symm.toRingHom)
      ⟨⟨id, fun _ _ ↦ rfl⟩, fun _ _ ↦ rfl⟩ Function.surjective_id

Premises used: Module.Finite.of_surjective, RingHomSurjective.instToRingHomRingEquiv, id, Subsemiring.topEquiv, Function.surjective_id, LinearMap.mk, AddHom.mk, RingEquiv.symm, rfl
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Set M
hA : A.Finite
⊢ Module.Finite.{u_1, u_4} R ↥(span R A)

Tactic:
of_fg ⟨hA.toFinset, hA.coe_toFinset.symm ▸ rfl⟩

Premises used: Eq.rec, Set.Finite.coe_toFinset, Set.Finite.toFinset, Exists.intro, Module.Finite.of_fg, Eq.symm, rfl
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
x : M
⊢ Module.Finite.{u_1, u_4} R ↥(R ∙ x)

Tactic:
span_of_finite R <| Set.finite_singleton _

Premises used: Module.Finite.span_of_finite, Set.finite_singleton
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
s : Finset M
⊢ Module.Finite.{u_1, u_4} R ↥(span R (↑s : Set M))

Tactic:
of_fg ⟨s, rfl⟩

Premises used: Exists.intro, Module.Finite.of_fg, rfl
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_6
A : Type u_7
M : Type u_8
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
s : Finset A
hs : Eq (α := Submodule R A) (span R (↑s : Set A)) ⊤
t : Finset M
ht : Eq (α := Submodule A M) (span A (↑t : Set M)) ⊤
rw : Eq (α := Submodule R M) (span R ((↑s : Set A) • (↑t : Set M))) ⊤
rw₁ : Eq (α := Submodule R M) (restrictScalars R (span A (↑t : Set M))) ⊤
rw₂ : Eq.{u_8 + 1} (α := Submodule R M) (restrictScalars.{u_6, u_7, u_8} R (R := A) ⊤) ⊤
rw₃ rw₄ : Eq.{u_8 + 1} (α := Submodule R M) ⊤ ⊤
⊢ Eq (α := Submodule R M) (span R (image2 (fun (x1 : A) (x2 : M) ↦ x1 • x2) (↑s : Set A) (↑t : Set M))) ⊤

Tactic:
rw [image2_smul, span_smul_of_span_eq_top hs (↑t : Set M), ht, restrictScalars_top]

Premises used: Submodule.restrictScalars_top, Set.image2_smul, SetLike.coe, Submodule.span_smul_of_span_eq_top
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
A₁ : Type u_6
B₁ : Type u_7
A₂ : Type u_8
B₂ : Type u_9
inst : CommSemiring A₁
inst_1 : CommSemiring B₁
inst_2 : CommSemiring A₂
inst_3 : Semiring B₂
inst_4 : Algebra A₁ B₁
inst_5 : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he :
  Eq (α := A₁ →+* B₂) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A₂ B₂) (↑e₁ : A₁ →+* A₂))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁))
inst_6 : Module.Finite A₁ B₁
this_1 : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra
this : Algebra A₂ B₁ := RingHom.toAlgebra (RingHom.comp (algebraMap A₁ B₁) e₁.symm.toRingHom)
x : A₁
⊢ Eq.{u_7 + 1} (α := B₁) ((algebraMap A₁ B₁ : (a : A₁) → B₁) x : B₁)
    ((algebraMap A₂ B₁ : (a : A₂) → B₁) ((algebraMap A₁ A₂ : (a : A₁) → A₂) x : A₂) : B₁)

Tactic:
simp [RingHom.algebraMap_toAlgebra]

Premises used: RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
A₁ : Type u_6
B₁ : Type u_7
A₂ : Type u_8
B₂ : Type u_9
inst : CommSemiring A₁
inst_1 : CommSemiring B₁
inst_2 : CommSemiring A₂
inst_3 : Semiring B₂
inst_4 : Algebra A₁ B₁
inst_5 : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he :
  Eq (α := A₁ →+* B₂) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A₂ B₂) (↑e₁ : A₁ →+* A₂))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁))
inst_6 : Module.Finite A₁ B₁
this_1 : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra
this : Algebra A₂ B₁ := RingHom.toAlgebra (RingHom.comp (algebraMap A₁ B₁) e₁.symm.toRingHom)
⊢ IsScalarTower A₁ A₂ B₁

Tactic:
haveI : IsScalarTower A₁ A₂ B₁ := IsScalarTower.of_algebraMap_eq
    (fun x ↦ by simp [RingHom.algebraMap_toAlgebra])
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
A₁ : Type u_6
B₁ : Type u_7
A₂ : Type u_8
B₂ : Type u_9
inst : CommSemiring A₁
inst_1 : CommSemiring B₁
inst_2 : CommSemiring A₂
inst_3 : Semiring B₂
inst_4 : Algebra A₁ B₁
inst_5 : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he :
  Eq (α := A₁ →+* B₂) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A₂ B₂) (↑e₁ : A₁ →+* A₂))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁))
inst_6 : Module.Finite A₁ B₁
this_1 : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra
this_2 : Algebra A₂ B₁ := RingHom.toAlgebra (RingHom.comp (algebraMap A₁ B₁) e₁.symm.toRingHom)
this : IsScalarTower A₁ A₂ B₁
r : A₂
⊢ e₂.toFun ((algebraMap A₂ B₁ : (a : A₂) → B₁) r) = (algebraMap A₂ B₂ : (a : A₂) → B₂) r

Tactic:
simpa [RingHom.algebraMap_toAlgebra] using DFunLike.congr_fun he.symm (e₁.symm r)

Premises used: DFunLike.congr_fun, RingHom.algebraMap_toAlgebra, Eq.symm, DFunLike.coe, RingEquiv.symm
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
A₁ : Type u_6
B₁ : Type u_7
A₂ : Type u_8
B₂ : Type u_9
inst : CommSemiring A₁
inst_1 : CommSemiring B₁
inst_2 : CommSemiring A₂
inst_3 : Semiring B₂
inst_4 : Algebra A₁ B₁
inst_5 : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he :
  Eq (α := A₁ →+* B₂) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A₂ B₂) (↑e₁ : A₁ →+* A₂))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁))
inst_6 : Module.Finite A₁ B₁
this_1 : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra
this_2 : Algebra A₂ B₁ := RingHom.toAlgebra (RingHom.comp (algebraMap A₁ B₁) e₁.symm.toRingHom)
this : IsScalarTower A₁ A₂ B₁
e : B₁ ≃ₐ[A₂] B₂ := { toEquiv := e₂.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ Module.Finite A₂ B₁

Tactic:
haveI := of_restrictScalars_finite A₁ A₂ B₁
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
A₁ : Type u_6
B₁ : Type u_7
A₂ : Type u_8
B₂ : Type u_9
inst : CommSemiring A₁
inst_1 : CommSemiring B₁
inst_2 : CommSemiring A₂
inst_3 : Semiring B₂
inst_4 : Algebra A₁ B₁
inst_5 : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he :
  Eq (α := A₁ →+* B₂) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A₂ B₂) (↑e₁ : A₁ →+* A₂))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁))
inst_6 : Module.Finite A₁ B₁
this_1 : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra
this_2 : Algebra A₂ B₁ := RingHom.toAlgebra (RingHom.comp (algebraMap A₁ B₁) e₁.symm.toRingHom)
this_3 : IsScalarTower A₁ A₂ B₁
e : B₁ ≃ₐ[A₂] B₂ := { toEquiv := e₂.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
this : Module.Finite A₂ B₁
⊢ Module.Finite A₂ B₂

Tactic:
equiv e.toLinearEquiv

Premises used: AlgEquiv.toLinearEquiv, Module.Finite.equiv
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
A₁ : Type u_6
B₁ : Type u_7
A₂ : Type u_8
B₂ : Type u_9
inst : CommSemiring A₁
inst_1 : CommSemiring B₁
inst_2 : CommSemiring A₂
inst_3 : Semiring B₂
inst_4 : Algebra A₁ B₁
inst_5 : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he :
  Eq (α := A₁ →+* B₂) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A₂ B₂) (↑e₁ : A₁ →+* A₂))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁))
inst_6 : Module.Finite A₁ B₁
this_1 : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra
this_2 : Algebra A₂ B₁ := RingHom.toAlgebra (RingHom.comp (algebraMap A₁ B₁) e₁.symm.toRingHom)
this_3 : IsScalarTower A₁ A₂ B₁
e : B₁ ≃ₐ[A₂] B₂ := { toEquiv := e₂.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
this : Module.Finite A₂ B₁
⊢ Module.Finite A₂ B₂

Tactic:
exact equiv e.toLinearEquiv

Premises used: AlgEquiv.toLinearEquiv, Module.Finite.equiv
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
S₁ S₂ : Submodule R V
h₁ : Module.Finite.{u_1, u_2} R ↥S₁
h₂ : Module.Finite.{u_1, u_2} R ↥S₂
rw : ∀ (h₁ : S₁.FG) (h₂ : S₂.FG), (S₁ ⊔ S₂).FG
⊢ Module.Finite.{u_1, u_2} R ↥(S₁ ⊔ S₂)

Tactic:
rw [Finite.iff_fg] at *

Premises used: Module.Finite.iff_fg
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
S₁ S₂ : Submodule R V
h₁ : S₁.FG
h₂ : S₂.FG
⊢ (S₁ ⊔ S₂).FG

Tactic:
.sup h₁ h₂

Premises used: Submodule.FG.sup
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
S₁ S₂ : Submodule R V
h₁ : S₁.FG
h₂ : S₂.FG
⊢ (S₁ ⊔ S₂).FG

Tactic:
exact .sup h₁ h₂
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_2
V : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
ι : Type u_1
s : Finset ι
S : ι → Submodule R V
inst_3 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(S i)
⊢ Module.Finite.{u_2, u_3} R ↥(s.sup S)

Tactic:
s.sup_induction (f := S) (p := fun i => Module.Finite R ↑i) (Module.Finite.bot R V) ?_
    inferInstance

Premises used: Finset.sup_induction, inferInstance, Module.Finite.bot
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_2
V : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
ι : Type u_1
s : Finset ι
S : ι → Submodule R V
inst_3 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(S i)
refine :
  ∀ (a₁ : Submodule R V),
    (fun (i : Submodule R V) ↦ Module.Finite.{u_2, u_3} R ↥i) a₁ →
      ∀ (a₂ : Submodule R V),
        (fun (i : Submodule R V) ↦ Module.Finite.{u_2, u_3} R ↥i) a₂ →
          (fun (i : Submodule R V) ↦ Module.Finite.{u_2, u_3} R ↥i) (a₁ ⊔ a₂)
⊢ Module.Finite.{u_2, u_3} R ↥(s.sup S)

Tactic:
refine s.sup_induction (f := S) (p := fun i => Module.Finite R ↑i) (Module.Finite.bot R V) ?_
    inferInstance

Premises used: Finset.sup_induction, inferInstance, Module.Finite.bot
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_2
V : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
ι : Type u_1
s : Finset ι
S : ι → Submodule R V
inst_3 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(S i)
S₁ : Submodule R V
hS₁ : Module.Finite.{u_2, u_3} R ↥S₁
S₂ : Submodule R V
hS₂ : Module.Finite.{u_2, u_3} R ↥S₂
⊢ Module.Finite.{u_2, u_3} R ↥(S₁ ⊔ S₂)

Tactic:
finite_sup S₁ S₂

Premises used: Submodule.finite_sup
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_2
V : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
ι : Type u_1
s : Finset ι
S : ι → Submodule R V
inst_3 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(S i)
S₁ : Submodule R V
hS₁ : Module.Finite.{u_2, u_3} R ↥S₁
S₂ : Submodule R V
hS₂ : Module.Finite.{u_2, u_3} R ↥S₂
⊢ Module.Finite.{u_2, u_3} R ↥(S₁ ⊔ S₂)

Tactic:
exact finite_sup S₁ S₂

Premises used: Submodule.finite_sup
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Module R A
inst_5 : Module A M
inst_6 : IsScalarTower R A M
S : Submodule A M
inst_7 : Module.Finite R A
hS : S.FG
rw : ∀ (hS : Module.Finite.{u_3, u_2} A ↥S), Module.Finite.{u_1, u_2} R ↥(Submodule.restrictScalars R S)
⊢ FG (Submodule.restrictScalars R S)

Tactic:
rw [← Module.Finite.iff_fg] at *

Premises used: Module.Finite.iff_fg
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Module R A
inst_5 : Module A M
inst_6 : IsScalarTower R A M
S : Submodule A M
inst_7 : Module.Finite R A
hS : Module.Finite.{u_3, u_2} A ↥S
⊢ Module.Finite.{u_1, u_2} R ↥(Submodule.restrictScalars R S)

Tactic:
Module.Finite.trans A S

Premises used: Set.Mem, Submodule.restrictScalars, Membership.mem, Subtype, Module.Finite.trans