awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
K : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
V₂ : Type u_9
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
p : Submodule R M
τ₁₂ : R →+* R₂
x : { p' : Submodule R M // p' ≤ p }
q : Submodule R M
hq : q ≤ p
⊢ (↑((fun (p' : Submodule R ↥p) ↦
            (Subtype.mk (p := fun (p' : Submodule R M) ↦ p' ≤ p) (map p.subtype p') ⋯ :
              { p' : Submodule R M // p' ≤ p }))
          ((fun (q : { p' : Submodule R M // p' ≤ p }) ↦ comap p.subtype (↑q : Submodule R M))
            (Subtype.mk (p := fun (p' : Submodule R M) ↦ p' ≤ p) q hq))) :
      Submodule R M) =
    (↑(Subtype.mk (p := fun (p' : Submodule R M) ↦ p' ≤ p) q hq) : Submodule R M)

Tactic:
simp [map_comap_subtype p, inf_of_le_right hq]

Premises used: inf_of_le_right, Submodule.map_comap_subtype
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
K : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
V₂ : Type u_9
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
p : Submodule R M
τ₁₂ : R →+* R₂
p₁ p₂ : Submodule R ↥p
rw : p₁ ≤ comap p.subtype (map p.subtype p₂) ↔ p₁ ≤ p₂
rw₁ rw₂ : p₁ ≤ p₂ ↔ p₁ ≤ p₂
⊢ map p.subtype p₁ ≤ map p.subtype p₂ ↔ p₁ ≤ p₂

Tactic:
rw [map_le_iff_le_comap,
      comap_map_eq_of_injective (show Injective p.subtype from Subtype.coe_injective) p₂]

Premises used: Submodule.comap_map_eq_of_injective, Subtype.coe_injective, Submodule.map_le_iff_le_comap
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
p' : Submodule R ↥p
⊢ (MapSubtype.orderEmbedding p : (a : Submodule R ↥p) → Submodule R M) p' = map p.subtype p'

Tactic:
rfl

Premises used: Submodule.map, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
q : Submodule R ↥p
⊢ (↑((p.mapIic : (a : Submodule R ↥p) → (↑(Set.Iic p) : Type u_5)) q) : Submodule R M) = map p.subtype q

Tactic:
rfl

Premises used: Submodule.map, rfl
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
hf : Surjective.{u_5 + 1, u_6 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R M
hpq : Codisjoint p q
rw : map f p ⊔ map f q = ⊤
rw₁ : map f (p ⊔ q) = ⊤
rw₂ : map f ⊤ = ⊤
rw₃ : f.range = ⊤
rw₄ rw₅ : Eq.{u_6 + 1} (α := Submodule R₂ M₂) ⊤ ⊤
⊢ Codisjoint (map f p) (map f q)

Tactic:
rw [codisjoint_iff, ← Submodule.map_sup, codisjoint_iff.mp hpq, map_top,
    LinearMap.range_eq_top_of_surjective f hf]

Premises used: LinearMap.range_eq_top_of_surjective, Submodule.map_top, codisjoint_iff, Submodule.map_sup, Iff.mp
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : ↥f.ker →ₗ[R] M), f ∘ₛₗ u = f ∘ₛₗ v → u = v
⊢ Eq (α := LinearMap.{u_1, u_2, u_5, u_6} τ₁₂ (↥f.ker) M₂) (f.comp (σ₁₂ := RingHom.id R) 0) 0

Tactic:
have h₁ : f.comp (0 : ker f →ₗ[R] M) = 0 := comp_zero _
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : ↥f.ker →ₗ[R] M), f ∘ₛₗ u = f ∘ₛₗ v → u = v
h₁ : Eq (α := LinearMap.{u_1, u_2, u_5, u_6} τ₁₂ (↥f.ker) M₂) (f.comp (σ₁₂ := RingHom.id R) 0) 0
rw : Eq.{u_5 + 1} (α := Submodule R M) (range (R := R) (M := ↥f.ker) (τ₁₂ := RingHom.id R) 0) ⊥
⊢ f.ker = ⊥

Tactic:
rw [← Submodule.range_subtype (ker f),
    ← h 0 (ker f).subtype (Eq.trans h₁ (comp_ker_subtype f).symm)]

Premises used: LinearMap.ker, Submodule.subtype, OfNat.ofNat, Eq.symm, Submodule.range_subtype, LinearMap.comp_ker_subtype, Eq.trans
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : ↥f.ker →ₗ[R] M), f ∘ₛₗ u = f ∘ₛₗ v → u = v
h₁ : Eq (α := LinearMap.{u_1, u_2, u_5, u_6} τ₁₂ (↥f.ker) M₂) (f.comp (σ₁₂ := RingHom.id R) 0) 0
⊢ Eq.{u_5 + 1} (α := Submodule R M) (range (R := R) (M := ↥f.ker) (τ₁₂ := RingHom.id R) 0) ⊥

Tactic:
range_zero

Premises used: LinearMap.range_zero
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : ↥f.ker →ₗ[R] M), f ∘ₛₗ u = f ∘ₛₗ v → u = v
h₁ : Eq (α := LinearMap.{u_1, u_2, u_5, u_6} τ₁₂ (↥f.ker) M₂) (f.comp (σ₁₂ := RingHom.id R) 0) 0
⊢ Eq.{u_5 + 1} (α := Submodule R M) (range (R := R) (M := ↥f.ker) (τ₁₂ := RingHom.id R) 0) ⊥

Tactic:
exact range_zero

Premises used: LinearMap.range_zero
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R M
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst_9 : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
inst_10 : RingHomSurjective τ₁₂
inst_11 : RingHomSurjective τ₂₃
inst_12 : RingHomSurjective τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
hf : f.range = ⊤
rw : Submodule.map g f.range = g.range
rw₁ : Submodule.map g ⊤ = g.range
rw₂ rw₃ : g.range = g.range
⊢ (g ∘ₛₗ f).range = g.range

Tactic:
rw [range_comp, hf, Submodule.map_top]

Premises used: Submodule.map_top, LinearMap.range_comp
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_10
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
O : Submodule R M
ϕ : LinearMap.{u_1, u_1, u_5, u_10} (RingHom.id R) (↥O) M'
N : Submodule R M
x : M'
⊢ x ∈ ϕ.submoduleImage N ↔
    ∃ (y : M) (yO : y ∈ O), y ∈ N ∧ (ϕ : (a : ↥O) → M') (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y yO) = x

Tactic:
Submodule.mem_map.trans ⟨?_, ?_⟩

Premises used: Set.Mem, Submodule.mem_map, Iff.intro, Iff.trans
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_10
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
O : Submodule R M
ϕ : LinearMap.{u_1, u_1, u_5, u_10} (RingHom.id R) (↥O) M'
N : Submodule R M
x : M'
refine_1 :
  (∃ y ∈ Submodule.comap O.subtype N, (ϕ : (a : ↥O) → M') y = x) →
    ∃ (y : M) (yO : y ∈ O), y ∈ N ∧ (ϕ : (a : ↥O) → M') (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y yO) = x
refine_2 :
  (∃ (y : M) (yO : y ∈ O), y ∈ N ∧ (ϕ : (a : ↥O) → M') (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y yO) = x) →
    ∃ y ∈ Submodule.comap O.subtype N, (ϕ : (a : ↥O) → M') y = x
⊢ x ∈ ϕ.submoduleImage N ↔
    ∃ (y : M) (yO : y ∈ O), y ∈ N ∧ (ϕ : (a : ↥O) → M') (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y yO) = x

Tactic:
refine Submodule.mem_map.trans ⟨?_, ?_⟩

Premises used: Submodule.mem_map, Iff.intro, Iff.trans
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_10
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
O : Submodule R M
ϕ : LinearMap.{u_1, u_1, u_5, u_10} (RingHom.id R) (↥O) M'
N : Submodule R M
x : M'
refine_1 :
  (∃ (y : ↥O), Membership.mem (α := M) N ((O.subtype : (a : ↥O) → M) y : M) ∧ (ϕ : (a : ↥O) → M') y = x) →
    ∃ (y : M) (yO : y ∈ O), y ∈ N ∧ (ϕ : (a : ↥O) → M') (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y yO) = x
⊢ (∃ y ∈ Submodule.comap O.subtype N, (ϕ : (a : ↥O) → M') y = x) →
    ∃ (y : M) (yO : y ∈ O), y ∈ N ∧ (ϕ : (a : ↥O) → M') (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y yO) = x

Tactic:
simp_rw [Submodule.mem_comap]

Premises used: Submodule.mem_comap
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_10
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
O : Submodule R M
ϕ : LinearMap.{u_1, u_1, u_5, u_10} (RingHom.id R) (↥O) M'
N : Submodule R M
x : M'
refine_2 :
  (∃ (y : M) (yO : y ∈ O), y ∈ N ∧ (ϕ : (a : ↥O) → M') (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y yO) = x) →
    ∃ (y : ↥O), Membership.mem (α := M) N ((O.subtype : (a : ↥O) → M) y : M) ∧ (ϕ : (a : ↥O) → M') y = x
⊢ (∃ (y : M) (yO : y ∈ O), y ∈ N ∧ (ϕ : (a : ↥O) → M') (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y yO) = x) →
    ∃ y ∈ Submodule.comap O.subtype N, (ϕ : (a : ↥O) → M') y = x

Tactic:
simp_rw [Submodule.mem_comap]

Premises used: Submodule.mem_comap
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_10
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
O : Submodule R M
ϕ : LinearMap.{u_1, u_1, u_5, u_10} (RingHom.id R) (↥O) M'
N : Submodule R M
x : M'
y : M
yO : y ∈ O
yN : y ∈ N
h : (ϕ : (a : ↥O) → M') (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y yO) = x
⊢ ∃ (y : M) (yO : y ∈ O), y ∈ N ∧ (ϕ : (a : ↥O) → M') (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y yO) = x

Tactic:
⟨y, yO, yN, h⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_10
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
O : Submodule R M
ϕ : LinearMap.{u_1, u_1, u_5, u_10} (RingHom.id R) (↥O) M'
N : Submodule R M
x : M'
y : M
yO : y ∈ O
yN : y ∈ N
h : (ϕ : (a : ↥O) → M') (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y yO) = x
⊢ ∃ (y : M) (yO : y ∈ O), y ∈ N ∧ (ϕ : (a : ↥O) → M') (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y yO) = x

Tactic:
exact ⟨y, yO, yN, h⟩
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_10
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
O : Submodule R M
ϕ : LinearMap.{u_1, u_1, u_5, u_10} (RingHom.id R) (↥O) M'
N : Submodule R M
x : M'
y : M
yO : y ∈ O
yN : y ∈ N
h : (ϕ : (a : ↥O) → M') (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y yO) = x
⊢ ∃ (y : ↥O), Membership.mem (α := M) N ((O.subtype : (a : ↥O) → M) y : M) ∧ (ϕ : (a : ↥O) → M') y = x

Tactic:
⟨⟨y, yO⟩, yN, h⟩

Premises used: Subtype.mk, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_10
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
O : Submodule R M
ϕ : LinearMap.{u_1, u_1, u_5, u_10} (RingHom.id R) (↥O) M'
N : Submodule R M
x : M'
y : M
yO : y ∈ O
yN : y ∈ N
h : (ϕ : (a : ↥O) → M') (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y yO) = x
⊢ ∃ (y : ↥O), Membership.mem (α := M) N ((O.subtype : (a : ↥O) → M) y : M) ∧ (ϕ : (a : ↥O) → M') y = x

Tactic:
exact ⟨⟨y, yO⟩, yN, h⟩
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_10
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
O : Submodule R M
ϕ : LinearMap.{u_1, u_1, u_5, u_10} (RingHom.id R) (↥O) M'
N : Submodule R M
hNO : N ≤ O
x : M'
⊢ x ∈ ϕ.submoduleImage N ↔ ∃ (y : M) (yN : y ∈ N), (ϕ : (a : ↥O) → M') (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = x

Tactic:
grind [mem_submoduleImage]

Premises used: LinearMap.mem_submoduleImage
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_10
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
O : Submodule R M
ϕ : LinearMap.{u_1, u_1, u_5, u_10} (RingHom.id R) (↥O) M'
N : Submodule R M
hNO : N ≤ O
rw : Submodule.map ϕ (Submodule.comap O.subtype N) = (ϕ ∘ₗ Submodule.inclusion hNO).range
rw₁ : Submodule.map ϕ (Submodule.comap O.subtype N) = Submodule.map ϕ (Submodule.inclusion hNO).range
rw₂ rw₃ : Submodule.map ϕ (Submodule.comap O.subtype N) = Submodule.map ϕ (Submodule.comap O.subtype N)
⊢ ϕ.submoduleImage N = (ϕ ∘ₗ Submodule.inclusion hNO).range

Tactic:
rw [submoduleImage, range_comp, Submodule.range_inclusion]

Premises used: LinearMap.range_comp, Submodule.range_inclusion, LinearMap.submoduleImage
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ Eq (α := Submodule R₂ ↥f.range) (range f.rangeRestrict) ⊤

Tactic:
simp [f.range_codRestrict _]

Premises used: LinearMap.range_codRestrict
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
rw : Eq (α := Submodule R₂ ↥f.range) (range f.rangeRestrict) ⊤
rw₁ rw₂ : Eq.{u_6 + 1} (α := Submodule R₂ ↥f.range) ⊤ ⊤
⊢ Surjective.{u_5 + 1, u_6 + 1} (α := M) (β := ↥f.range) (⇑f.rangeRestrict : (a : M) → ↥f.range)

Tactic:
rw [← range_eq_top, range_rangeRestrict]

Premises used: LinearMap.range_rangeRestrict, LinearMap.range_eq_top
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ ker (M₂ := ↥f.range) f.rangeRestrict = f.ker

Tactic:
LinearMap.ker_codRestrict _ _ _

Premises used: LinearMap.ker_codRestrict
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ Injective.{u_5 + 1, u_6 + 1} (α := M) (β := ↥f.range) (⇑f.rangeRestrict : (a : M) → ↥f.range) ↔
    Injective.{u_5 + 1, u_6 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)

Tactic:
Set.injective_codRestrict _

Premises used: Set.injective_codRestrict, Set.codRestrict
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
q : Submodule R₂ M₂
h : ∀ x ∈ p, Membership.mem (α := M₂) q ((f : (a : M) → M₂) x : M₂)
rw : map (f.restrict h) ⊤ = comap q.subtype (map f p)
rw₁ : comap q.subtype (map f (map p.subtype ⊤)) = comap q.subtype (map f p)
rw₂ : comap q.subtype (map f p.subtype.range) = comap q.subtype (map f p)
rw₃ rw₄ : comap q.subtype (map f p) = comap q.subtype (map f p)
⊢ (f.restrict h).range = comap q.subtype (map f p)

Tactic:
rw [← Submodule.map_top, map_restrict, Submodule.map_top, p.range_subtype]

Premises used: LinearMap.map_restrict, Submodule.map_top, Submodule.range_subtype
-- Module: Mathlib.Algebra.Module.Submodule.RestrictScalars
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
V : Submodule R M
⊢ (↑(restrictScalars S V) : Set M) = (↑V : Set M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.RestrictScalars
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
V : Submodule R M
⊢ toAddSubmonoid (restrictScalars S V) = V.toAddSubmonoid

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Submodule.RestrictScalars
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
V : Submodule R M
m : M
⊢ Membership.mem (γ := Submodule S M) (restrictScalars S V) m ↔ m ∈ V

Tactic:
Iff.refl _

Premises used: Set.Mem, Iff.refl
-- Module: Mathlib.Algebra.Module.Submodule.RestrictScalars
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
V : Submodule R M
⊢ restrictScalars R V = V

Tactic:
SetLike.coe_injective rfl

Premises used: SetLike.coe_injective, rfl
-- Module: Mathlib.Algebra.Module.Submodule.RestrictScalars
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
T : Type u_4
inst_7 : Semiring T
inst_8 : SMul T R
inst_9 : SMul S T
inst_10 : IsScalarTower S T R
inst_11 : Module T M
inst_12 : IsScalarTower S T M
inst_13 : IsScalarTower T R M
V : Submodule R M
⊢ Eq (α := Submodule S M) (restrictScalars S (restrictScalars T V)) (restrictScalars S V)

Tactic:
rfl

Premises used: Submodule.restrictScalars, rfl
-- Module: Mathlib.Algebra.Module.Submodule.RestrictScalars
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
⊢ Function.Injective.{u_3 + 1, u_3 + 1} (α := Submodule R M) (β := Submodule S M) (restrictScalars S)

Tactic:
fun _ _ h =>
  ext <| Set.ext_iff.1 (SetLike.ext'_iff.1 h :)

Premises used: Iff.mp, SetLike.ext'_iff, Set.ext_iff, Function.Injective, Submodule.ext
-- Module: Mathlib.Algebra.Module.Submodule.RestrictScalars
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
V₁ V₂ : Submodule R M
⊢ Eq (α := Submodule S M) (restrictScalars S V₁) (restrictScalars S V₂) ↔ V₁ = V₂

Tactic:
(restrictScalars_injective S _ _).eq_iff

Premises used: Function.Injective.eq_iff, Submodule.restrictScalars_injective
-- Module: Mathlib.Algebra.Module.Submodule.RestrictScalars
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
s t : Submodule R M
⊢ LE.le (α := Submodule S M) (restrictScalars S s) (restrictScalars S t) ↔ s ≤ t

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Module.Submodule.RestrictScalars
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
s t : Submodule R M
⊢ LT.lt (α := Submodule S M) (restrictScalars S s) (restrictScalars S t) ↔ s < t

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Module.Submodule.RestrictScalars
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
⊢ Monotone.{u_3, u_3} (α := Submodule R M) (β := Submodule S M) (restrictScalars S)

Tactic:
(restrictScalarsEmbedding S R M).monotone

Premises used: OrderEmbedding.monotone, Submodule.restrictScalars, Submodule.restrictScalarsEmbedding
-- Module: Mathlib.Algebra.Module.Submodule.RestrictScalars
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
s t : Submodule R M
hst : s ≤ t
⊢ LE.le (α := Submodule S M) (restrictScalars S s) (restrictScalars S t)

Tactic:
restrictScalars_monotone S R M hst

Premises used: Submodule.restrictScalars_monotone
-- Module: Mathlib.Algebra.Module.Submodule.RestrictScalars
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
⊢ Eq.{u_3 + 1} (α := Submodule S M) (restrictScalars.{u_1, u_2, u_3} S (R := R) ⊥) ⊥

Tactic:
rfl

Premises used: Submodule.restrictScalars, setOf, Set.singleton, rfl
-- Module: Mathlib.Algebra.Module.Submodule.RestrictScalars
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
p : Submodule R M
⊢ Eq (α := Submodule S M) (restrictScalars S p) ⊥ ↔ p = ⊥

Tactic:
simp [SetLike.ext_iff]

Premises used: SetLike.ext_iff
-- Module: Mathlib.Algebra.Module.Submodule.RestrictScalars
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
⊢ Eq.{u_3 + 1} (α := Submodule S M) (restrictScalars.{u_1, u_2, u_3} S (R := R) ⊤) ⊤

Tactic:
rfl

Premises used: Set.univ, Submodule.restrictScalars, setOf, rfl
-- Module: Mathlib.Algebra.Module.Submodule.RestrictScalars
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
p : Submodule R M
⊢ Eq (α := Submodule S M) (restrictScalars S p) ⊤ ↔ p = ⊤

Tactic:
simp [SetLike.ext_iff]

Premises used: SetLike.ext_iff
-- Module: Mathlib.Algebra.Module.Submodule.RestrictScalars
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
s : Set (Submodule R M)
h :
  ∀ (x : M),
    Membership.mem (γ := Submodule S M) (restrictScalars S (sInf s)) x ↔
      Membership.mem (γ := Submodule S M) (sInf (restrictScalars S '' s)) x
⊢ Eq (α := Submodule S M) (restrictScalars S (sInf s)) (sInf (restrictScalars S '' s))

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Submodule.RestrictScalars
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
s : Set (Submodule R M)
x : M
⊢ Membership.mem (γ := Submodule S M) (restrictScalars S (sInf s)) x ↔
    Membership.mem (γ := Submodule S M) (sInf (restrictScalars S '' s)) x

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.RestrictScalars
Goal:
S : Type u_1
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Semiring S
inst_3 : Module S M
inst_4 : Module R M
inst_5 : SMul S R
inst_6 : IsScalarTower S R M
s : Set (Submodule R M)
⊢ Eq (α := Submodule S M) (restrictScalars S (sSup s)) (sSup (restrictScalars S '' s))

Tactic:
simp [← toAddSubmonoid_inj, toAddSubmonoid_sSup, ← Set.image_comp]

Premises used: Submodule.toAddSubmonoid_sSup, Submodule.toAddSubmonoid_inj, Set.image_comp