awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
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 ⋯
⊢ p x hx
have refine : ∀ (r : S) (n : M) (hr : Membership.mem (γ := Set S) {a} r) (hn : n ∈ N), p' (r • n) sorry
Tactic: refine Submodule.set_smul_inductionOn (motive := p') _ (N.singleton_set_smul a ▸ hx)
      (fun r n hr hn ↦ ?_) smul₁ add zero
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (hypothesis)
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
⊢ p' (r • n) ⋯
have hr₁ : r = a
Tactic: push _ ∈ _ at hr
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
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
⊢ p' (r • n) ⋯
have subst : ∀ {p : (x : M) → x ∈ r • N → Prop} (smul₀ : ∀ (s : M) (hs : s ∈ N), p (r • s) sorry) (hx : x ∈ r • N)
  (smul₁ : ∀ (r_1 : R) (m : M) (mem : m ∈ HSMul.hSMul (α := Set S) {r} N), p m sorry → p (r_1 • m) sorry)
  (add :
    ∀ (x y : M) (hx : x ∈ HSMul.hSMul (α := Set S) {r} N) (hy : y ∈ HSMul.hSMul (α := Set S) {r} N),
      p x sorry → p y sorry → p (x + y) sorry)
  (zero : p 0 sorry),
  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 sorry;
  ∀ (hr : Membership.mem (γ := Set S) {r} r), p' (r • n) sorry
Tactic: subst hr
Cleared hypotheses: a, p, smul₀, hx, smul₁, add, zero, p', hr_1, hr
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
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
⊢ Eq (α := Subgroup G) (stabilizer G S) (stabilizer G (↑S : Set M))
have h : ∀ (x : G),
  Membership.mem (γ := Subgroup G) (stabilizer G S) x ↔ Membership.mem (γ := Subgroup G) (stabilizer G (↑S : Set M)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
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
⊢ Membership.mem (γ := Subgroup G) (stabilizer G S) x ↔ Membership.mem (γ := Subgroup G) (stabilizer G (↑S : Set M)) x
have h : x • S = S ↔ Membership.mem (γ := Subgroup G) (stabilizer G (↑S : Set M)) x
Tactic: rw [mem_stabilizer_iff, SetLike.ext'_iff, coe_pointwise_smul,
    ← mem_stabilizer_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
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
⊢ Membership.mem (γ := Subgroup G) (stabilizer G S) x ↔ Membership.mem (γ := Subgroup G) (stabilizer G (↑S : Set M)) x
have h₁ : (↑(x • S) : Set M) = (↑S : Set M) ↔ Membership.mem (γ := Subgroup G) (stabilizer G (↑S : Set M)) x
Tactic: rw [mem_stabilizer_iff, SetLike.ext'_iff, coe_pointwise_smul,
    ← mem_stabilizer_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
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
⊢ Membership.mem (γ := Subgroup G) (stabilizer G S) x ↔ Membership.mem (γ := Subgroup G) (stabilizer G (↑S : Set M)) x
have h₂ : x • (↑S : Set M) = (↑S : Set M) ↔ Membership.mem (γ := Subgroup G) (stabilizer G (↑S : Set M)) x
Tactic: rw [mem_stabilizer_iff, SetLike.ext'_iff, coe_pointwise_smul,
    ← mem_stabilizer_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Pointwise (goal)
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
⊢ Membership.mem (γ := Subgroup G) (stabilizer G S) x ↔ Membership.mem (γ := Subgroup G) (stabilizer G (↑S : Set M)) x
have h₃ : Membership.mem (γ := Subgroup G) (stabilizer G (↑S : Set M)) 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]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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 = map f ⊤
have h : ∀ (x : M₂), x ∈ f.range ↔ x ∈ map f ⊤
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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 = ⊤ ↔ Surjective.{u_5 + 1, u_6 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
have rw : (↑f.range : Set M₂) = (↑⊤ : Set M₂) ↔ 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]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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₂)
⊢ f.range = ⊤ ↔ Surjective.{u_5 + 1, u_6 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
have 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₂)
Tactic: rw [SetLike.ext'_iff, coe_range, top_coe, Set.range_eq_univ]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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₂)
⊢ f.range = ⊤ ↔ Surjective.{u_5 + 1, u_6 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
have 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₂)
Tactic: rw [SetLike.ext'_iff, coe_range, top_coe, Set.range_eq_univ]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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₂)
⊢ f.range = ⊤ ↔ Surjective.{u_5 + 1, u_6 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
have 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₂)
Tactic: rw [SetLike.ext'_iff, coe_range, top_coe, Set.range_eq_univ]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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 ⊔ g.range) ((f + g : (a : M) → M₂) w : M₂)
have hs : Membership.mem (α := M₂) f.range ((f : (a : M) → M₂) w : M₂)
Tactic: apply add_mem_sup
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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₂)
⊢ Membership.mem (α := M₂) (f.range ⊔ g.range) ((f + g : (a : M) → M₂) w : M₂)
have ht : Membership.mem (α := M₂) g.range ((g : (a : M) → M₂) w : M₂)
Tactic: apply add_mem_sup
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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₂
⊢ f.range ≤ p ↔ comap f p = ⊤
have rw : map f ⊤ ≤ p ↔ comap f p = ⊤
Tactic: rw [range_eq_map, map_le_iff_le_comap, eq_top_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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 = ⊤
⊢ f.range ≤ p ↔ comap f p = ⊤
have rw₁ : ⊤ ≤ comap f p ↔ comap f p = ⊤
Tactic: rw [range_eq_map, map_le_iff_le_comap, eq_top_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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 = ⊤
⊢ f.range ≤ p ↔ comap f p = ⊤
have rw₂ : ⊤ ≤ comap f p ↔ ⊤ ≤ comap f p
Tactic: rw [range_eq_map, map_le_iff_le_comap, eq_top_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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₂
⊢ (-f).range = f.range
have change : ((-id) ∘ₛₗ f).range = f.range
Tactic: change range ((-LinearMap.id : M₂ →ₗ[R₂] M₂).comp f) = _
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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₂
⊢ ((-id) ∘ₛₗ f).range = f.range
have rw : map (-id) f.range = f.range
Tactic: rw [range_comp, Submodule.map_neg, Submodule.map_id]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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
⊢ ((-id) ∘ₛₗ f).range = f.range
have rw₁ : map id f.range = f.range
Tactic: rw [range_comp, Submodule.map_neg, Submodule.map_id]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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
⊢ ((-id) ∘ₛₗ f).range = f.range
have rw₂ : f.range = f.range
Tactic: rw [range_comp, Submodule.map_neg, Submodule.map_id]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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₂
⊢ (f.domRestrict K).range = map f K
have h : ∀ (x : M₂), x ∈ (f.domRestrict K).range ↔ x ∈ map f K
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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
⊢ map f (comap f q) = q
have rwa : f.range ⊓ q = q
Tactic: rwa [Submodule.map_comap_eq, inf_eq_right]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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 ≤ ⊥ ↔ f = 0
have rw : comap f ⊥ = ⊤ ↔ f = 0
Tactic: rw [range_le_iff_comap]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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 = ⊥ ↔ f = 0
have rw : f.range = ⊥ ↔ f.range ≤ ⊥
Tactic: rw [← range_le_bot_iff, le_bot_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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 = ⊥ ↔ f.range ≤ ⊥
⊢ f.range = ⊥ ↔ f = 0
have rw₁ : f.range = ⊥ ↔ f.range = ⊥
Tactic: rw [← range_le_bot_iff, le_bot_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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 τ₁₂
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
h : g ∘ₛₗ f = 0
x : M₂
hx : x ∈ f.range
y : M
hy : (f : (a : M) → M₂) y = x
⊢ Eq.{u_7 + 1} (α := M₃) ((g : (a : M₂) → M₃) x : M₃) (0 : M₃)
have rw : Eq.{u_7 + 1} (α := M₃) ((g : (a : M₂) → M₃) ((f : (a : M) → M₂) y : M₂) : M₃) (0 : M₃)
Tactic: rw [← hy, ← comp_apply, h, zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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 τ₁₂
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
h : g ∘ₛₗ f = 0
x : M₂
hx : x ∈ f.range
y : M
hy : (f : (a : M) → M₂) y = x
rw : Eq.{u_7 + 1} (α := M₃) ((g : (a : M₂) → M₃) ((f : (a : M) → M₂) y : M₂) : M₃) (0 : M₃)
⊢ Eq.{u_7 + 1} (α := M₃) ((g : (a : M₂) → M₃) x : M₃) (0 : M₃)
have rw₁ : Eq.{u_7 + 1} (α := M₃) ((g ∘ₛₗ f : (a : M) → M₃) y : M₃) (0 : M₃)
Tactic: rw [← hy, ← comp_apply, h, zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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 τ₁₂
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
h : g ∘ₛₗ f = 0
x : M₂
hx : x ∈ f.range
y : M
hy : (f : (a : M) → M₂) y = x
rw : Eq.{u_7 + 1} (α := M₃) ((g : (a : M₂) → M₃) ((f : (a : M) → M₂) y : M₂) : M₃) (0 : M₃)
rw₁ : Eq.{u_7 + 1} (α := M₃) ((g ∘ₛₗ f : (a : M) → M₃) y : M₃) (0 : M₃)
⊢ Eq.{u_7 + 1} (α := M₃) ((g : (a : M₂) → M₃) x : M₃) (0 : M₃)
have rw₂ : Eq.{u_7 + 1} (α := M₃) ((0 : (a : M) → M₃) y : M₃) (0 : M₃)
Tactic: rw [← hy, ← comp_apply, h, zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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 τ₁₂
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
h : g ∘ₛₗ f = 0
x : M₂
hx : x ∈ f.range
y : M
hy : (f : (a : M) → M₂) y = x
rw : Eq.{u_7 + 1} (α := M₃) ((g : (a : M₂) → M₃) ((f : (a : M) → M₂) y : M₂) : M₃) (0 : M₃)
rw₁ : Eq.{u_7 + 1} (α := M₃) ((g ∘ₛₗ f : (a : M) → M₃) y : M₃) (0 : M₃)
rw₂ : Eq.{u_7 + 1} (α := M₃) ((0 : (a : M) → M₃) y : M₃) (0 : M₃)
⊢ Eq.{u_7 + 1} (α := M₃) ((g : (a : M₂) → M₃) x : M₃) (0 : M₃)
have rw₃ : Eq.{u_7 + 1} (α := M₃) 0 0
Tactic: rw [← hy, ← comp_apply, h, zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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 : f.range = ⊤
p p' : Submodule R₂ M₂
H : comap f p ≤ comap f p'
⊢ p ≤ p'
have rwa : ∀ ⦃x : M₂⦄, x ∈ p → x ∈ p'
Tactic: rwa [SetLike.le_def, (range_eq_top.1 hf).forall]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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 : f.range = ⊤
p p' : Submodule R₂ M₂
H : comap f p ≤ comap f p'
rwa : ∀ ⦃x : M₂⦄, x ∈ p → x ∈ p'
⊢ p ≤ p'
have rwa₁ : ∀ (x : M),
  Membership.mem (α := M₂) p ((f : (a : M) → M₂) x : M₂) → Membership.mem (α := M₂) p' ((f : (a : M) → M₂) x : M₂)
Tactic: rwa [SetLike.le_def, (range_eq_top.1 hf).forall]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_10
P : Type u_11
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
g : P →ₗ[R] M
h : f ∘ₗ g = id
x : M
hx : x ∈ f.ker
⊢ HSub.hSub (β := M) x ((g : (a : P) → M) ((f : (a : M) → P) x : P) : M) = x
have rw : HSub.hSub (β := M) x ((g : (a : P) → M) 0 : M) = x
Tactic: rw [hx, map_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_10
P : Type u_11
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
g : P →ₗ[R] M
h : f ∘ₗ g = id
x : M
hx : x ∈ f.ker
rw : HSub.hSub (β := M) x ((g : (a : P) → M) 0 : M) = x
⊢ HSub.hSub (β := M) x ((g : (a : P) → M) ((f : (a : M) → P) x : P) : M) = x
have rw₁ : x - 0 = x
Tactic: rw [hx, map_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_10
P : Type u_11
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
g : P →ₗ[R] M
h : f ∘ₗ g = id
x : M
hx : x ∈ f.ker
rw : HSub.hSub (β := M) x ((g : (a : P) → M) 0 : M) = x
rw₁ : x - 0 = x
⊢ HSub.hSub (β := M) x ((g : (a : P) → M) ((f : (a : M) → P) x : P) : M) = x
have rw₂ : x = x
Tactic: rw [hx, map_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_10
P : Type u_11
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
g : P →ₗ[R] M
h : f ∘ₗ g = id
⊢ f ∘ₗ (id - g ∘ₗ f) = 0
have rw : f ∘ₗ id - f ∘ₗ g ∘ₗ f = 0
Tactic: rw [comp_sub, comp_id, ← comp_assoc, h, id_comp, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_10
P : Type u_11
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
g : P →ₗ[R] M
h : f ∘ₗ g = id
rw : f ∘ₗ id - f ∘ₗ g ∘ₗ f = 0
⊢ f ∘ₗ (id - g ∘ₗ f) = 0
have rw₁ : f - f ∘ₗ g ∘ₗ f = 0
Tactic: rw [comp_sub, comp_id, ← comp_assoc, h, id_comp, sub_self]