awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass S R M
a : S
p : (x : M) → x ∈ a • N → Prop
smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) ⋯
x : M
hx : x ∈ a • N
smul₁ : ∀ (r : R) (m : M) (mem : m ∈ HSMul.hSMul (α := Set S) {a} N), p m ⋯ → p (r • m) ⋯
add :
  ∀ (x y : M) (hx : x ∈ HSMul.hSMul (α := Set S) {a} N) (hy : y ∈ HSMul.hSMul (α := Set S) {a} N),
    p x ⋯ → p y ⋯ → p (x + y) ⋯
zero : p 0 ⋯
p' : (x : M) → (hx : x ∈ HSMul.hSMul (α := Set S) {a} N) → Prop :=
  fun (x : M) (hx : x ∈ HSMul.hSMul (α := Set S) {a} N) ↦ p x ⋯
r : S
n : M
hr : Membership.mem (γ := Set S) {a} r
hn : n ∈ N
⊢ r = a

Tactic:
push _ ∈ _ at hr
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass S R M
a : S
p : (x : M) → x ∈ a • N → Prop
smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) ⋯
x : M
hx : x ∈ a • N
smul₁ : ∀ (r : R) (m : M) (mem : m ∈ HSMul.hSMul (α := Set S) {a} N), p m ⋯ → p (r • m) ⋯
add :
  ∀ (x y : M) (hx : x ∈ HSMul.hSMul (α := Set S) {a} N) (hy : y ∈ HSMul.hSMul (α := Set S) {a} N),
    p x ⋯ → p y ⋯ → p (x + y) ⋯
zero : p 0 ⋯
p' : (x : M) → (hx : x ∈ HSMul.hSMul (α := Set S) {a} N) → Prop :=
  fun (x : M) (hx : x ∈ HSMul.hSMul (α := Set S) {a} N) ↦ p x ⋯
r : S
n : M
hr_1 : Membership.mem (γ := Set S) {a} r
hn : n ∈ N
hr : r = a
subst :
  ∀ {p : (x : M) → x ∈ r • N → Prop} (smul₀ : ∀ (s : M) (hs : s ∈ N), p (r • s) ⋯) (hx : x ∈ r • N)
    (smul₁ : ∀ (r_1 : R) (m : M) (mem : m ∈ HSMul.hSMul (α := Set S) {r} N), p m ⋯ → p (r_1 • m) ⋯)
    (add :
      ∀ (x y : M) (hx : x ∈ HSMul.hSMul (α := Set S) {r} N) (hy : y ∈ HSMul.hSMul (α := Set S) {r} N),
        p x ⋯ → p y ⋯ → p (x + y) ⋯)
    (zero : p 0 ⋯),
    let p' : (x : M) → (hx : x ∈ HSMul.hSMul (α := Set S) {r} N) → Prop :=
      fun (x : M) (hx : x ∈ HSMul.hSMul (α := Set S) {r} N) ↦ p x ⋯;
    ∀ (hr : Membership.mem (γ := Set S) {r} r), p' (r • n) ⋯
⊢ p' (r • n) ⋯

Tactic:
subst hr
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass S R M
x : M
r : S
n : M
hn : n ∈ N
p : (x : M) → x ∈ r • N → Prop
smul₀ : ∀ (s : M) (hs : s ∈ N), p (r • s) ⋯
hx : x ∈ r • N
smul₁ : ∀ (r_1 : R) (m : M) (mem : m ∈ HSMul.hSMul (α := Set S) {r} N), p m ⋯ → p (r_1 • m) ⋯
add :
  ∀ (x y : M) (hx : x ∈ HSMul.hSMul (α := Set S) {r} N) (hy : y ∈ HSMul.hSMul (α := Set S) {r} N),
    p x ⋯ → p y ⋯ → p (x + y) ⋯
zero : p 0 ⋯
p' : (x : M) → (hx : x ∈ HSMul.hSMul (α := Set S) {r} N) → Prop :=
  fun (x : M) (hx : x ∈ HSMul.hSMul (α := Set S) {r} N) ↦ p x ⋯
hr : Membership.mem (γ := Set S) {r} r
⊢ p' (r • n) ⋯

Tactic:
smul₀ n hn
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
inst_5 : SMulCommClass S R M
x : M
r : S
n : M
hn : n ∈ N
p : (x : M) → x ∈ r • N → Prop
smul₀ : ∀ (s : M) (hs : s ∈ N), p (r • s) ⋯
hx : x ∈ r • N
smul₁ : ∀ (r_1 : R) (m : M) (mem : m ∈ HSMul.hSMul (α := Set S) {r} N), p m ⋯ → p (r_1 • m) ⋯
add :
  ∀ (x y : M) (hx : x ∈ HSMul.hSMul (α := Set S) {r} N) (hy : y ∈ HSMul.hSMul (α := Set S) {r} N),
    p x ⋯ → p y ⋯ → p (x + y) ⋯
zero : p 0 ⋯
p' : (x : M) → (hx : x ∈ HSMul.hSMul (α := Set S) {r} N) → Prop :=
  fun (x : M) (hx : x ∈ HSMul.hSMul (α := Set S) {r} N) ↦ p x ⋯
hr : Membership.mem (γ := Set S) {r} r
⊢ p' (r • n) ⋯

Tactic:
exact smul₀ n hn
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
s t : Set S
r : S
n : M
hr : r ∈ s
hn : n ∈ N
⊢ r • n ∈ s • N ⊔ t • N

Tactic:
Submodule.mem_sup_left (mem_set_smul_of_mem_mem hr hn)

Premises used: Submodule.mem_set_smul_of_mem_mem, Submodule.mem_sup_left
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
s t : Set S
r : S
n : M
hr : r ∈ s
hn : n ∈ N
⊢ r • n ∈ s • N ⊔ t • N

Tactic:
exact Submodule.mem_sup_left (mem_set_smul_of_mem_mem hr hn)

Premises used: Submodule.mem_set_smul_of_mem_mem, Submodule.mem_sup_left
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
s t : Set S
r : S
n : M
hr : r ∈ t
hn : n ∈ N
⊢ r • n ∈ s • N ⊔ t • N

Tactic:
Submodule.mem_sup_right (mem_set_smul_of_mem_mem hr hn)

Premises used: Submodule.mem_set_smul_of_mem_mem, Submodule.mem_sup_right
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_4
inst_3 : Monoid S
inst_4 : DistribMulAction S M
N : Submodule R M
s t : Set S
r : S
n : M
hr : r ∈ t
hn : n ∈ N
⊢ r • n ∈ s • N ⊔ t • N

Tactic:
exact Submodule.mem_sup_right (mem_set_smul_of_mem_mem hr hn)

Premises used: Submodule.mem_set_smul_of_mem_mem, Submodule.mem_sup_right
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_4
G : Type u_5
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Group G
inst_4 : DistribMulAction G M
inst_5 : SMulCommClass G R M
S : Submodule R M
h :
  ∀ (x : G),
    Membership.mem (γ := Subgroup G) (stabilizer G S) x ↔ Membership.mem (γ := Subgroup G) (stabilizer G (↑S : Set M)) x
⊢ Eq (α := Subgroup G) (stabilizer G S) (stabilizer G (↑S : Set M))

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_4
G : Type u_5
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Group G
inst_4 : DistribMulAction G M
inst_5 : SMulCommClass G R M
S : Submodule R M
x : G
h : x • S = S ↔ Membership.mem (γ := Subgroup G) (stabilizer G (↑S : Set M)) x
h₁ : (↑(x • S) : Set M) = (↑S : Set M) ↔ Membership.mem (γ := Subgroup G) (stabilizer G (↑S : Set M)) x
h₂ : x • (↑S : Set M) = (↑S : Set M) ↔ Membership.mem (γ := Subgroup G) (stabilizer G (↑S : Set M)) x
h₃ h₄ :
  Membership.mem (γ := Subgroup G) (stabilizer G (↑S : Set M)) x ↔
    Membership.mem (γ := Subgroup G) (stabilizer G (↑S : Set M)) x
⊢ Membership.mem (γ := Subgroup G) (stabilizer G S) x ↔ Membership.mem (γ := Subgroup G) (stabilizer G (↑S : Set M)) x

Tactic:
rw [mem_stabilizer_iff, SetLike.ext'_iff, coe_pointwise_smul,
    ← mem_stabilizer_iff]

Premises used: Submodule.coe_pointwise_smul, SetLike.ext'_iff, MulAction.mem_stabilizer_iff
-- Module: Mathlib.Algebra.Module.Submodule.Pointwise
Goal:
R : Type u_4
G : Type u_5
M : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Group G
inst_4 : DistribMulAction G M
inst_5 : SMulCommClass G R M
S : Submodule R M
e : G
⊢ Membership.mem (γ := Subgroup G) (stabilizer G S) e ↔ map (DistribSMul.toLinearMap R M e) S = S

Tactic:
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₂
⊢ (↑f.range : Set M₂) = Set.range.{u_6, u_5 + 1} (ι := M) (⇑f : (a : M) → M₂)

Tactic:
rfl

Premises used: setOf, Set.range, 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₂
⊢ f.range.toAddSubmonoid = AddMonoidHom.mrange f

Tactic:
rfl

Premises used: AddSubmonoid.copy, AddMonoidHom.mrange, 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₂
x : M₂
⊢ x ∈ f.range ↔ ∃ (y : M), (f : (a : M) → M₂) y = x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range
-- 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₂
h : ∀ (x : M₂), x ∈ f.range ↔ x ∈ map f ⊤
⊢ f.range = map f ⊤

Tactic:
ext
-- 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₂
x : M₂
⊢ x ∈ f.range ↔ x ∈ map f ⊤

Tactic:
simp
-- 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₂
x : M
⊢ Membership.mem (α := M₂) f.range ((f : (a : M) → M₂) x : M₂)

Tactic:
⟨x, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, 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
⊢ Eq.{u_5 + 1} (α := Submodule R M) (range id) ⊤

Tactic:
SetLike.coe_injective Set.range_id

Premises used: SetLike.coe_injective, Set.range_id
-- 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₃
⊢ (g ∘ₛₗ f).range = map g f.range

Tactic:
SetLike.coe_injective (Set.range_comp g f)

Premises used: Set.range_comp, SetLike.coe_injective, DFunLike.coe
-- 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 τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
⊢ (g ∘ₛₗ f).range ≤ g.range

Tactic:
SetLike.coe_mono (Set.range_comp_subset_range f g)

Premises used: Set.range_comp_subset_range, Set.Subset, DFunLike.coe, SetLike.coe_mono
-- 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 : (↑f.range : Set M₂) = (↑⊤ : Set M₂) ↔ Surjective.{u_5 + 1, u_6 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
rw₁ :
  Set.range.{u_6, u_5 + 1} (ι := M) (⇑f : (a : M) → M₂) = (↑⊤ : Set M₂) ↔
    Surjective.{u_5 + 1, u_6 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
rw₂ :
  Eq.{u_6 + 1} (α := Set M₂) (Set.range.{u_6, u_5 + 1} (ι := M) (⇑f : (a : M) → M₂)) Set.univ ↔
    Surjective.{u_5 + 1, u_6 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
rw₃ rw₄ :
  Surjective.{u_5 + 1, u_6 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂) ↔
    Surjective.{u_5 + 1, u_6 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
⊢ f.range = ⊤ ↔ Surjective.{u_5 + 1, u_6 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)

Tactic:
rw [SetLike.ext'_iff, coe_range, top_coe, Set.range_eq_univ]

Premises used: Set.range_eq_univ, LinearMap.coe_range, SetLike.ext'_iff, Submodule.top_coe
-- 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₂)
⊢ f.range = ⊤

Tactic:
range_eq_top.2 hf

Premises used: Iff.mpr, 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 g : M →ₛₗ[τ₁₂] M₂
w : M
hs : Membership.mem (α := M₂) f.range ((f : (a : M) → M₂) w : M₂)
ht : Membership.mem (α := M₂) g.range ((g : (a : M) → M₂) w : M₂)
⊢ Membership.mem (α := M₂) (f.range ⊔ g.range) ((f + g : (a : M) → M₂) w : M₂)

Tactic:
apply add_mem_sup

Premises used: Submodule.add_mem_sup
-- 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 g : M →ₛₗ[τ₁₂] M₂
w : M
⊢ Membership.mem (α := M₂) f.range ((f : (a : M) → M₂) w : M₂)

Tactic:
simp only [mem_range, exists_apply_eq_apply]

Premises used: LinearMap.mem_range, exists_apply_eq_apply
-- 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 g : M →ₛₗ[τ₁₂] M₂
w : M
⊢ Membership.mem (α := M₂) g.range ((g : (a : M) → M₂) w : M₂)

Tactic:
simp only [mem_range, exists_apply_eq_apply]

Premises used: LinearMap.mem_range, exists_apply_eq_apply
-- 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₂
rw : map f ⊤ ≤ p ↔ comap f p = ⊤
rw₁ : ⊤ ≤ comap f p ↔ comap f p = ⊤
rw₂ rw₃ : ⊤ ≤ comap f p ↔ ⊤ ≤ comap f p
⊢ f.range ≤ p ↔ comap f p = ⊤

Tactic:
rw [range_eq_map, map_le_iff_le_comap, eq_top_iff]

Premises used: eq_top_iff, LinearMap.range_eq_map, Submodule.map_le_iff_le_comap
-- 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
⊢ map f p ≤ f.range

Tactic:
SetLike.coe_mono (Set.image_subset_range f p)

Premises used: Set.image_subset_range, Set.Subset, SetLike.coe, DFunLike.coe, SetLike.coe_mono
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_10
R₂ : Type u_11
M : Type u_12
M₂ : Type u_13
inst : Semiring R
inst_1 : Ring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
change : ((-id) ∘ₛₗ f).range = f.range
⊢ (-f).range = f.range

Tactic:
change range ((-LinearMap.id : M₂ →ₗ[R₂] M₂).comp f) = _

Premises used: LinearMap.id, LinearMap.range, LinearMap.comp, Neg.neg
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_10
R₂ : Type u_11
M : Type u_12
M₂ : Type u_13
inst : Semiring R
inst_1 : Ring R₂
inst_2 : AddCommMonoid M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
inst_6 : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
rw : map (-id) f.range = f.range
rw₁ : map id f.range = f.range
rw₂ rw₃ : f.range = f.range
⊢ ((-id) ∘ₛₗ f).range = f.range

Tactic:
rw [range_comp, Submodule.map_neg, Submodule.map_id]

Premises used: Submodule.map_id, LinearMap.range_comp, Submodule.map_neg
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
M : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
K : Submodule R M
f : M →ₗ[R] M₂
h : ∀ (x : M₂), x ∈ (f.domRestrict K).range ↔ x ∈ map f K
⊢ (f.domRestrict K).range = map f K

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
R : Type u_1
M : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
K : Submodule R M
f : M →ₗ[R] M₂
x : M₂
⊢ x ∈ (f.domRestrict K).range ↔ x ∈ map f K

Tactic:
simp
-- 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₂
S : Submodule R M
y : M
hy : y ∈ S
⊢ Membership.mem (α := M₂) f.range ((f.domRestrict S : (a : ↥S) → M₂) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) y hy) : M₂)

Tactic:
LinearMap.mem_range_self f y

Premises used: Set.Mem, LinearMap.mem_range_self
-- 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₂
S : Submodule R M
y : M
hy : y ∈ S
⊢ Membership.mem (α := M₂) f.range ((f.domRestrict S : (a : ↥S) → M₂) (Subtype.mk (p := fun (x : M) ↦ x ∈ S) y hy) : M₂)

Tactic:
exact LinearMap.mem_range_self f y

Premises used: LinearMap.mem_range_self
-- Module: Mathlib.Algebra.Module.Submodule.Range
Goal:
M : Type u_10
M₂ : Type u_11
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
f : M →+ M₂
⊢ f.toIntLinearMap.range = (AddSubgroup.toIntSubmodule : (a : AddSubgroup M₂) → Submodule ℤ M₂) f.range

Tactic:
rfl

Premises used: LinearMap.range, rfl, Submodule.copy
-- 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₂
h : p ≤ f.range
⊢ map f (comap f p) = p

Tactic:
SetLike.coe_injective <| Set.image_preimage_eq_of_subset h

Premises used: SetLike.coe_injective, Set.image_preimage_eq_of_subset
-- 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₂
inst_6 : SMul R R₂
inst_7 : Module R₂ M
inst_8 : Module R M₂
inst_9 : CompatibleSMul M M₂ R R₂
inst_10 : IsScalarTower R R₂ M₂
f : M →ₗ[R₂] M₂
⊢ Eq (α := Submodule R M₂)
    (range
      ((↑R :
          {S : Type u_2} →
            {M : Type u_5} →
              {M₂ : Type u_6} →
                [inst : Semiring R] →
                  [inst_11 : Semiring S] →
                    [inst_12 : AddCommMonoid M] →
                      [inst_13 : AddCommMonoid M₂] →
                        [inst_14 : Module R M] →
                          [inst_15 : Module R M₂] →
                            [inst_16 : Module S M] →
                              [inst_17 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        f))
    (Submodule.restrictScalars R f.range)

Tactic:
rfl

Premises used: Submodule.restrictScalars, setOf, LinearMap.range, Set.range, rfl, Submodule.copy
-- 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
f : M →ₗ[R] M
n : ℕ
⊢ (f.iterateRange : (a : ℕ) → (Submodule R M)ᵒᵈ) (n + 1) = map f ((f.iterateRange : (a : ℕ) → (Submodule R M)ᵒᵈ) n)

Tactic:
simp only [iterateRange_coe, range_eq_map, ← map_comp, Module.End.iterate_succ']

Premises used: Module.End.iterate_succ', Submodule.map_comp, LinearMap.iterateRange_coe, LinearMap.range_eq_map
-- 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 τ₂₁
p : Submodule R M
f : M₂ →ₛₗ[τ₂₁] M
hf : ∀ (c : M₂), Membership.mem (α := M) p ((f : (a : M₂) → M) c : M)
⊢ (codRestrict p f hf).range = comap p.subtype f.range

Tactic:
simpa only [range_eq_map] using map_codRestrict _ _ _ _

Premises used: LinearMap.map_codRestrict, LinearMap.range_eq_map
-- 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₂
q : Submodule R₂ M₂
x : M
hx : Membership.mem (α := M₂) (↑q : Set M₂) ((f : (a : M) → M₂) x : M₂)
⊢ Membership.mem (α := M₂) (map f (comap f q)) ((f : (a : M) → M₂) x : M₂)

Tactic:
⟨x, hx, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, 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₂
q : Submodule R₂ M₂
x : M
hx : Membership.mem (α := M₂) (↑q : Set M₂) ((f : (a : M) → M₂) x : M₂)
⊢ Membership.mem (α := M₂) (map f (comap f q)) ((f : (a : M) → M₂) x : M₂)

Tactic:
exact ⟨x, hx, 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₂
q : Submodule R₂ M₂
h : q ≤ f.range
rwa : f.range ⊓ q = q
rwa₁ rwa₂ rwa₃ rwa₄ : q ≤ f.range
⊢ map f (comap f q) = q

Tactic:
rwa [Submodule.map_comap_eq, inf_eq_right]

Premises used: Submodule.map_comap_eq, inf_eq_right
-- 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 τ₁₂
⊢ Eq.{u_6 + 1} (α := Submodule R₂ M₂) (range.{u_1, u_2, u_5, u_6} (R := R) (M := M) (τ₁₂ := τ₁₂) 0) ⊥

Tactic:
simpa only [range_eq_map] using Submodule.map_zero _

Premises used: Submodule.map_zero, LinearMap.range_eq_map
-- 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 : comap f ⊥ = ⊤ ↔ f = 0
⊢ f.range ≤ ⊥ ↔ f = 0

Tactic:
rw [range_le_iff_comap]

Premises used: LinearMap.range_le_iff_comap