awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw₁ : f - 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]
-- 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
rw₁ : f - f ∘ₗ g ∘ₗ f = 0
rw₂ : f - (f ∘ₗ g) ∘ₗ f = 0
⊢ f ∘ₗ (id - g ∘ₗ f) = 0
have rw₃ : f - id ∘ₗ 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
rw₁ : f - f ∘ₗ g ∘ₗ f = 0
rw₂ : f - (f ∘ₗ g) ∘ₗ f = 0
rw₃ : f - id ∘ₗ f = 0
⊢ f ∘ₗ (id - g ∘ₗ f) = 0
have rw₄ : f - 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
rw₁ : f - f ∘ₗ g ∘ₗ f = 0
rw₂ : f - (f ∘ₗ g) ∘ₗ f = 0
rw₃ : f - id ∘ₗ f = 0
rw₄ : f - f = 0
⊢ f ∘ₗ (id - g ∘ₗ f) = 0
have rw₅ : Eq (α := M →ₗ[R] P) 0 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
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst_6 : RingHomSurjective τ₁₂
p : Submodule R M
⊢ f.ker ≤ p ↔ ∃ y ∈ f.range, Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M)
have mp : f.ker ≤ p → ∃ y ∈ f.range, Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M)
Tactic: constructor
-- 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 : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst_6 : RingHomSurjective τ₁₂
p : Submodule R M
mp : f.ker ≤ p → ∃ y ∈ f.range, Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M)
⊢ f.ker ≤ p ↔ ∃ y ∈ f.range, Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M)
have mpr : (∃ y ∈ f.range, Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M)) → f.ker ≤ p
Tactic: constructor
-- 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 : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst_6 : RingHomSurjective τ₁₂
p : Submodule R M
h : f.ker ≤ p
⊢ ∃ y ∈ f.range, Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M)
have h₁ : 0 ∈ f.range ∧ Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {0} ⊆ (↑p : Set M)
Tactic: use 0
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (hypothesis)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst_6 : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₁ : y ∈ f.range
h₂ : Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M)
z : M
hz : z ∈ f.ker
⊢ z ∈ p
have hz₁ : Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) z : M₂) (0 : M₂)
Tactic: simp only [mem_ker] at hz
Cleared hypotheses: hz
-- 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 : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst_6 : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₁ : y ∈ f.range
h₂ : Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M)
z : M
hz : Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) z : M₂) (0 : M₂)
⊢ z ∈ p
have mpr : ∀ (h₁ : ∃ (y_1 : M), (f : (a : M) → M₂) y_1 = y) (h₂ : Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M))
  ⦃z : M⦄ (hz : Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) z : M₂) (0 : M₂)), z ∈ p
Tactic: rw [← SetLike.mem_coe, coe_range, Set.mem_range] at h₁
Cleared hypotheses: h₁, h₂, z, hz
-- 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 : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst_6 : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₁ : ∃ (y_1 : M), (f : (a : M) → M₂) y_1 = y
h₂ : Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M)
z : M
hz : Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) z : M₂) (0 : M₂)
⊢ z ∈ p
have mpr : ∀ (x : M) (hx : (f : (a : M) → M₂) x = y), z ∈ p
Tactic: obtain ⟨x, hx⟩ := h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (hypothesis)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst_6 : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M)
z : M
hz : Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) z : M₂) (0 : M₂)
x : M
hx : (f : (a : M) → M₂) x = y
⊢ z ∈ p
have hx' : x ∈ p
Tactic: have hx' : x ∈ p := h₂ hx
-- 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 : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst_6 : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M)
z : M
hz : Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) z : M₂) (0 : M₂)
x : M
hx : (f : (a : M) → M₂) x = y
hx' : x ∈ p
⊢ z + x ∈ p
have a : Membership.mem (γ := Set M) (Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y}) (z + x)
Tactic: apply h₂
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (hypothesis)
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst_6 : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M)
z : M
hz : Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) z : M₂) (0 : M₂)
x : M
hx : (f : (a : M) → M₂) x = y
hx' : x ∈ p
⊢ z ∈ p
have hxz : z + x ∈ p
Tactic: have hxz : z + x ∈ p := by
      apply h₂
      simp [hx, hz]
-- 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 : Ring R
inst_1 : Ring R₂
inst_2 : AddCommGroup M
inst_3 : AddCommGroup M₂
inst_4 : Module R M
inst_5 : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst_6 : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : Set.preimage (β := M₂) (⇑f : (a : M) → M₂) {y} ⊆ (↑p : Set M)
z : M
hz : Eq.{u_6 + 1} (α := M₂) ((f : (a : M) → M₂) z : M₂) (0 : M₂)
x : M
hx : (f : (a : M) → M₂) x = y
hx' : x ∈ p
hxz : z + x ∈ p
⊢ z ∈ p
have mpr : z + x - x ∈ p
Tactic: suffices z + x - x ∈ p by simpa only [this, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p p' : Submodule R M
⊢ map p.subtype ⊤ ≤ p' ↔ p ≤ p'
have rw : p ≤ p' ↔ p ≤ p'
Tactic: rw [map_subtype_top]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N₁ N₂ N : Submodule R M
h₁ : N₁ ≤ N
h₂ : N₂ ≤ N
⊢ (N₁ ⊔ N₂).submoduleOf N = N₁.submoduleOf N ⊔ N₂.submoduleOf N
have a : map N.subtype ((N₁ ⊔ N₂).submoduleOf N) = map N.subtype (N₁.submoduleOf N ⊔ N₂.submoduleOf N)
Tactic: apply Submodule.map_injective_of_injective N.subtype_injective
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N₁ N₂ N : Submodule R M
h₁ : N₁ ≤ N
h₂ : N₂ ≤ N
⊢ map N.subtype ((N₁ ⊔ N₂).submoduleOf N) = map N.subtype (N₁.submoduleOf N ⊔ N₂.submoduleOf N)
have a : N.subtype.range ⊓ (N₁ ⊔ N₂) = map N.subtype (comap N.subtype N₁ ⊔ comap N.subtype N₂)
Tactic: simp only [submoduleOf, map_comap_eq]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p q : Submodule R M
h : p ≤ q
⊢ (inclusion h).range = comap q.subtype p
have rw : map (inclusion h) ⊤ = comap q.subtype p
Tactic: rw [← map_top, inclusion, LinearMap.map_codRestrict, map_top, range_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p q : Submodule R M
h : p ≤ q
rw : map (inclusion h) ⊤ = comap q.subtype p
⊢ (inclusion h).range = comap q.subtype p
have rw₁ : map (codRestrict q p.subtype sorry) ⊤ = comap q.subtype p
Tactic: rw [← map_top, inclusion, LinearMap.map_codRestrict, map_top, range_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p q : Submodule R M
h : p ≤ q
rw : map (inclusion h) ⊤ = comap q.subtype p
rw₁ : map (codRestrict q p.subtype ⋯) ⊤ = comap q.subtype p
⊢ (inclusion h).range = comap q.subtype p
have rw₂ : comap q.subtype (map p.subtype ⊤) = comap q.subtype p
Tactic: rw [← map_top, inclusion, LinearMap.map_codRestrict, map_top, range_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p q : Submodule R M
h : p ≤ q
rw : map (inclusion h) ⊤ = comap q.subtype p
rw₁ : map (codRestrict q p.subtype ⋯) ⊤ = comap q.subtype p
rw₂ : comap q.subtype (map p.subtype ⊤) = comap q.subtype p
⊢ (inclusion h).range = comap q.subtype p
have rw₃ : comap q.subtype p.subtype.range = comap q.subtype p
Tactic: rw [← map_top, inclusion, LinearMap.map_codRestrict, map_top, range_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p q : Submodule R M
h : p ≤ q
rw : map (inclusion h) ⊤ = comap q.subtype p
rw₁ : map (codRestrict q p.subtype ⋯) ⊤ = comap q.subtype p
rw₂ : comap q.subtype (map p.subtype ⊤) = comap q.subtype p
rw₃ : comap q.subtype p.subtype.range = comap q.subtype p
⊢ (inclusion h).range = comap q.subtype p
have rw₄ : comap q.subtype p = comap q.subtype p
Tactic: rw [← map_top, inclusion, LinearMap.map_codRestrict, map_top, range_subtype]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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
⊢ map p.subtype p₁ ≤ map p.subtype p₂ ↔ p₁ ≤ p₂
have rw : p₁ ≤ comap p.subtype (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₂]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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₂
⊢ map p.subtype p₁ ≤ map p.subtype p₂ ↔ p₁ ≤ p₂
have rw₁ : p₁ ≤ p₂ ↔ p₁ ≤ p₂
Tactic: rw [map_le_iff_le_comap,
      comap_map_eq_of_injective (show Injective p.subtype from Subtype.coe_injective) p₂]
-- 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 : Surjective.{u_5 + 1, u_6 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R M
hpq : Codisjoint p q
⊢ Codisjoint (map f p) (map f q)
have rw : 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]
-- 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 : 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 = ⊤
⊢ Codisjoint (map f p) (map f q)
have rw₁ : map f (p ⊔ q) = ⊤
Tactic: rw [codisjoint_iff, ← Submodule.map_sup, codisjoint_iff.mp hpq, map_top,
    LinearMap.range_eq_top_of_surjective f hf]
-- 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 : 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) = ⊤
⊢ Codisjoint (map f p) (map f q)
have rw₂ : map f ⊤ = ⊤
Tactic: rw [codisjoint_iff, ← Submodule.map_sup, codisjoint_iff.mp hpq, map_top,
    LinearMap.range_eq_top_of_surjective f hf]
-- 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 : 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 ⊤ = ⊤
⊢ Codisjoint (map f p) (map f q)
have rw₃ : f.range = ⊤
Tactic: rw [codisjoint_iff, ← Submodule.map_sup, codisjoint_iff.mp hpq, map_top,
    LinearMap.range_eq_top_of_surjective f hf]
-- 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 : 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 = ⊤
⊢ Codisjoint (map f p) (map f q)
have rw₄ : Eq.{u_6 + 1} (α := Submodule R₂ M₂) ⊤ ⊤
Tactic: rw [codisjoint_iff, ← Submodule.map_sup, codisjoint_iff.mp hpq, map_top,
    LinearMap.range_eq_top_of_surjective f hf]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (hypothesis)
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
⊢ f.ker = ⊥
have h₁ : 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 _
-- 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₂
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
⊢ f.ker = ⊥
have rw : Eq.{u_5 + 1} (α := Submodule R M) (range (R := R) (M := ↥f.ker) (τ₁₂ := RingHom.id R) 0) ⊥
Tactic: rw [← Submodule.range_subtype (ker f),
    ← h 0 (ker f).subtype (Eq.trans h₁ (comp_ker_subtype f).symm)]
-- 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 τ₁₂
inst_11 : RingHomSurjective τ₂₃
inst_12 : RingHomSurjective τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
hf : f.range = ⊤
⊢ (g ∘ₛₗ f).range = g.range
have rw : Submodule.map g f.range = g.range
Tactic: rw [range_comp, hf, Submodule.map_top]
-- 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 τ₁₂
inst_11 : RingHomSurjective τ₂₃
inst_12 : RingHomSurjective τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
hf : f.range = ⊤
rw : Submodule.map g f.range = g.range
⊢ (g ∘ₛₗ f).range = g.range
have rw₁ : Submodule.map g ⊤ = g.range
Tactic: rw [range_comp, hf, Submodule.map_top]
-- 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 τ₁₂
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
⊢ (g ∘ₛₗ f).range = g.range
have rw₂ : g.range = g.range
Tactic: rw [range_comp, hf, Submodule.map_top]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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
have 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
Tactic: refine Submodule.mem_map.trans ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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
⊢ x ∈ ϕ.submoduleImage N ↔
    ∃ (y : M) (yO : y ∈ O), y ∈ N ∧ (ϕ : (a : ↥O) → M') (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y yO) = x
have 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
Tactic: refine Submodule.mem_map.trans ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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 ∈ 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
have 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
Tactic: simp_rw [Submodule.mem_comap]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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), 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
have 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
Tactic: simp_rw [Submodule.mem_comap]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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
⊢ ϕ.submoduleImage N = (ϕ ∘ₗ Submodule.inclusion hNO).range
have rw : Submodule.map ϕ (Submodule.comap O.subtype N) = (ϕ ∘ₗ Submodule.inclusion hNO).range
Tactic: rw [submoduleImage, range_comp, Submodule.range_inclusion]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Range (goal)
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
⊢ ϕ.submoduleImage N = (ϕ ∘ₗ Submodule.inclusion hNO).range
have rw₁ : Submodule.map ϕ (Submodule.comap O.subtype N) = Submodule.map ϕ (Submodule.inclusion hNO).range
Tactic: rw [submoduleImage, range_comp, Submodule.range_inclusion]