awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
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₂
σ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
i : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p : Submodule R M
x : ↥(map f p)
⊢ (f : (a : M) → M₂)
      (↑(((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
              (a : ↥(map f p)) → ↥p)
            x) :
        M) =
    (↑x : M₂)
have rw : Eq.{u_7 + 1} (α := M₂)
  ((f : (a : M) → M₂)
      (↑(((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
              (a : ↥(map f p)) → ↥p)
            (((equivMapOfInjective f i p : LinearEquiv.{u_1, u_3, u_5, u_7} σ₁₂ ↥p ↥(map f p)) : (a : ↥p) → ↥(map f p))
              (((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
                  (a : ↥(map f p)) → ↥p)
                x))) :
        M) :
    M₂)
  ((↑(((equivMapOfInjective f i p : LinearEquiv.{u_1, u_3, u_5, u_7} σ₁₂ ↥p ↥(map f p)) : (a : ↥p) → ↥(map f p))
          (((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
              (a : ↥(map f p)) → ↥p)
            x)) :
      M₂) :
    M₂)
Tactic: rw [← LinearEquiv.apply_symm_apply (equivMapOfInjective f i p) x, coe_equivMapOfInjective_apply,
    i.eq_iff, LinearEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
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₂
σ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
i : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p : Submodule R M
x : ↥(map f p)
rw :
  Eq.{u_7 + 1} (α := M₂)
    ((f : (a : M) → M₂)
        (↑(((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
                (a : ↥(map f p)) → ↥p)
              (((equivMapOfInjective f i p : LinearEquiv.{u_1, u_3, u_5, u_7} σ₁₂ ↥p ↥(map f p)) :
                  (a : ↥p) → ↥(map f p))
                (((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
                    (a : ↥(map f p)) → ↥p)
                  x))) :
          M) :
      M₂)
    ((↑(((equivMapOfInjective f i p : LinearEquiv.{u_1, u_3, u_5, u_7} σ₁₂ ↥p ↥(map f p)) : (a : ↥p) → ↥(map f p))
            (((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
                (a : ↥(map f p)) → ↥p)
              x)) :
        M₂) :
      M₂)
⊢ (f : (a : M) → M₂)
      (↑(((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
              (a : ↥(map f p)) → ↥p)
            x) :
        M) =
    (↑x : M₂)
have rw₁ : Eq.{u_7 + 1} (α := M₂)
  ((f : (a : M) → M₂)
      (↑(((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
              (a : ↥(map f p)) → ↥p)
            (((equivMapOfInjective f i p : LinearEquiv.{u_1, u_3, u_5, u_7} σ₁₂ ↥p ↥(map f p)) : (a : ↥p) → ↥(map f p))
              (((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
                  (a : ↥(map f p)) → ↥p)
                x))) :
        M) :
    M₂)
  ((f : (a : M) → M₂)
      (↑(((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
              (a : ↥(map f p)) → ↥p)
            x) :
        M) :
    M₂)
Tactic: rw [← LinearEquiv.apply_symm_apply (equivMapOfInjective f i p) x, coe_equivMapOfInjective_apply,
    i.eq_iff, LinearEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
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₂
σ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
i : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p : Submodule R M
x : ↥(map f p)
rw :
  Eq.{u_7 + 1} (α := M₂)
    ((f : (a : M) → M₂)
        (↑(((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
                (a : ↥(map f p)) → ↥p)
              (((equivMapOfInjective f i p : LinearEquiv.{u_1, u_3, u_5, u_7} σ₁₂ ↥p ↥(map f p)) :
                  (a : ↥p) → ↥(map f p))
                (((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
                    (a : ↥(map f p)) → ↥p)
                  x))) :
          M) :
      M₂)
    ((↑(((equivMapOfInjective f i p : LinearEquiv.{u_1, u_3, u_5, u_7} σ₁₂ ↥p ↥(map f p)) : (a : ↥p) → ↥(map f p))
            (((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
                (a : ↥(map f p)) → ↥p)
              x)) :
        M₂) :
      M₂)
rw₁ :
  Eq.{u_7 + 1} (α := M₂)
    ((f : (a : M) → M₂)
        (↑(((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
                (a : ↥(map f p)) → ↥p)
              (((equivMapOfInjective f i p : LinearEquiv.{u_1, u_3, u_5, u_7} σ₁₂ ↥p ↥(map f p)) :
                  (a : ↥p) → ↥(map f p))
                (((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
                    (a : ↥(map f p)) → ↥p)
                  x))) :
          M) :
      M₂)
    ((f : (a : M) → M₂)
        (↑(((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
                (a : ↥(map f p)) → ↥p)
              x) :
          M) :
      M₂)
⊢ (f : (a : M) → M₂)
      (↑(((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
              (a : ↥(map f p)) → ↥p)
            x) :
        M) =
    (↑x : M₂)
have rw₂ : Eq.{u_5 + 1} (α := M)
  (↑(((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
          (a : ↥(map f p)) → ↥p)
        (((equivMapOfInjective f i p : LinearEquiv.{u_1, u_3, u_5, u_7} σ₁₂ ↥p ↥(map f p)) : (a : ↥p) → ↥(map f p))
          (((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
              (a : ↥(map f p)) → ↥p)
            x))) :
    M)
  (↑(((LinearEquiv.symm (equivMapOfInjective f i p) : LinearEquiv.{u_3, u_1, u_7, u_5} σ₂₁ ↥(map f p) ↥p) :
          (a : ↥(map f p)) → ↥p)
        x) :
    M)
Tactic: rw [← LinearEquiv.apply_symm_apply (equivMapOfInjective f i p) x, coe_equivMapOfInjective_apply,
    i.eq_iff, LinearEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
⊢ p ≤ comap (f ^ k) p
have zero : p ≤ comap (HPow.hPow (β := ℕ) f 0) p
Tactic: induction k with
  | zero => simp [Module.End.one_eq_id]
  | succ k ih => simp [Module.End.iterate_succ, comap_comp, h.trans (comap_mono ih)]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
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
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
zero : p ≤ comap (HPow.hPow (β := ℕ) f 0) p
⊢ p ≤ comap (f ^ k) p
have succ : ∀ (k : ℕ) (ih : p ≤ comap (f ^ k) p), p ≤ comap (f ^ (k + 1)) p
Tactic: induction k with
  | zero => simp [Module.End.one_eq_id]
  | succ k ih => simp [Module.End.iterate_succ, comap_comp, h.trans (comap_mono ih)]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
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 : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R M
hpq : Disjoint p q
⊢ Disjoint (map f p) (map f q)
have rw : map f p ⊓ map f q = ⊥
Tactic: rw [disjoint_iff, ← map_inf f hf, disjoint_iff.mp hpq, map_bot]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
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 : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R M
hpq : Disjoint p q
rw : map f p ⊓ map f q = ⊥
⊢ Disjoint (map f p) (map f q)
have rw₁ : map f (p ⊓ q) = ⊥
Tactic: rw [disjoint_iff, ← map_inf f hf, disjoint_iff.mp hpq, map_bot]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
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 : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R M
hpq : Disjoint p q
rw : map f p ⊓ map f q = ⊥
rw₁ : map f (p ⊓ q) = ⊥
⊢ Disjoint (map f p) (map f q)
have rw₂ : map f ⊥ = ⊥
Tactic: rw [disjoint_iff, ← map_inf f hf, disjoint_iff.mp hpq, map_bot]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
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 : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R M
hpq : Disjoint p q
rw : map f p ⊓ map f q = ⊥
rw₁ : map f (p ⊓ q) = ⊥
rw₂ : map f ⊥ = ⊥
⊢ Disjoint (map f p) (map f q)
have rw₃ : Eq.{u_7 + 1} (α := Submodule R₂ M₂) ⊥ ⊥
Tactic: rw [disjoint_iff, ← map_inf f hf, disjoint_iff.mp hpq, map_bot]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
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 σ₁₂ σ₂₃ σ₁₃
p p' : Submodule R M
q q' : Submodule R₂ M₂
x_1 : M
σ₂₁ : R₂ →+* R
inst_10 : RingHomInvPair σ₁₂ σ₂₁
inst_11 : RingHomInvPair σ₂₁ σ₁₂
inst_12 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
S : Submodule R₂ M₂
x : M₂
hx : x ∈ S
⊢ x ∈ map f (comap f S)
have rcases : ∀ (y : M) (hx : Membership.mem (α := M₂) S ((f : (a : M) → M₂) y : M₂)),
  Membership.mem (α := M₂) (map f (comap f S)) ((f : (a : M) → M₂) y : M₂)
Tactic: rcases hf x with ⟨y, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
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 σ₁₂ σ₂₃ σ₁₃
p p' : Submodule R M
q q' : Submodule R₂ M₂
x : M
σ₂₁ : R₂ →+* R
inst_10 : RingHomInvPair σ₁₂ σ₂₁
inst_11 : RingHomInvPair σ₂₁ σ₁₂
inst_12 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
S : Submodule R₂ M₂
y : M
hx : Membership.mem (α := M₂) S ((f : (a : M) → M₂) y : M₂)
⊢ Membership.mem (α := M₂) (map f (comap f S)) ((f : (a : M) → M₂) y : M₂)
have simp : ∃ (y_1 : M),
  Membership.mem (α := M₂) S ((f : (a : M) → M₂) y_1 : M₂) ∧
    Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) y_1 : M₂) ((f : (a : M) → M₂) y : M₂)
Tactic: simp only [mem_map, mem_comap]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
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_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R₂ M₂
⊢ comap f p < comap f q ↔ p < q
have H : comap f q ≤ comap f p ↔ q ≤ p
Tactic: apply lt_iff_lt_of_le_iff_le'
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
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_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R₂ M₂
H : comap f q ≤ comap f p ↔ q ≤ p
⊢ comap f p < comap f q ↔ p < q
have H' : comap f p ≤ comap f q ↔ p ≤ q
Tactic: apply lt_iff_lt_of_le_iff_le'
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (hypothesis)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
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₂
p : Submodule R M
q : Submodule R₂ M₂
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
h : comap f q < p
⊢ q < map f p
have h₁ : comap f q ≤ p ∧ ¬p ≤ comap f q
Tactic: rw [lt_iff_le_not_ge] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
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₂
p : Submodule R M
q : Submodule R₂ M₂
inst_6 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Surjective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
h : comap f q ≤ p ∧ ¬p ≤ comap f q
⊢ q ≤ map f p ∧ ¬map f p ≤ q
have rw : q ≤ map f p ∧ ¬p ≤ comap f q
Tactic: rw [map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
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 σ₁₂ σ₂₃ σ₁₃
p p' : Submodule R M
q q' : Submodule R₂ M₂
x_1 : M
σ₂₁ : R₂ →+* R
inst_10 : RingHomInvPair σ₁₂ σ₂₁
inst_11 : RingHomInvPair σ₂₁ σ₁₂
inst_12 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
S : Submodule R M
x : M
⊢ x ∈ comap f (map f S) → x ∈ S
have simp : ∀ x_2 ∈ S, Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) x_2 : M₂) ((f : (a : M) → M₂) x : M₂) → x ∈ S
Tactic: simp only [mem_comap, mem_map, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (hypothesis)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
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 σ₁₂ σ₂₃ σ₁₃
p p' : Submodule R M
q q' : Submodule R₂ M₂
x_1 : M
σ₂₁ : R₂ →+* R
inst_10 : RingHomInvPair σ₁₂ σ₂₁
inst_11 : RingHomInvPair σ₂₁ σ₁₂
inst_12 : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
S : Submodule R M
x y : M
hy : y ∈ S
hxy : Eq.{u_7 + 1} (α := M₂) ((f : (a : M) → M₂) y : M₂) ((f : (a : M) → M₂) x : M₂)
⊢ x ∈ S
have hxy₁ : y = x
Tactic: rw [hf.eq_iff] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
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 : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R M
⊢ map f p < map f q ↔ p < q
have rw : map f p ≤ map f q ∧ map f p ≠ map f q ↔ p < q
Tactic: rw [lt_iff_le_and_ne, lt_iff_le_and_ne, map_le_map_iff_of_injective hf,
    (map_injective_of_injective hf).ne_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
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 : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R M
rw : map f p ≤ map f q ∧ map f p ≠ map f q ↔ p < q
⊢ map f p < map f q ↔ p < q
have rw₁ : map f p ≤ map f q ∧ map f p ≠ map f q ↔ p ≤ q ∧ p ≠ q
Tactic: rw [lt_iff_le_and_ne, lt_iff_le_and_ne, map_le_map_iff_of_injective hf,
    (map_injective_of_injective hf).ne_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
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 : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R M
rw : map f p ≤ map f q ∧ map f p ≠ map f q ↔ p < q
rw₁ : map f p ≤ map f q ∧ map f p ≠ map f q ↔ p ≤ q ∧ p ≠ q
⊢ map f p < map f q ↔ p < q
have rw₂ : p ≤ q ∧ map f p ≠ map f q ↔ p ≤ q ∧ p ≠ q
Tactic: rw [lt_iff_le_and_ne, lt_iff_le_and_ne, map_le_map_iff_of_injective hf,
    (map_injective_of_injective hf).ne_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
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 : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R M
rw : map f p ≤ map f q ∧ map f p ≠ map f q ↔ p < q
rw₁ : map f p ≤ map f q ∧ map f p ≠ map f q ↔ p ≤ q ∧ p ≠ q
rw₂ : p ≤ q ∧ map f p ≠ map f q ↔ p ≤ q ∧ p ≠ q
⊢ map f p < map f q ↔ p < q
have rw₃ : p ≤ q ∧ p ≠ q ↔ p ≤ q ∧ p ≠ q
Tactic: rw [lt_iff_le_and_ne, lt_iff_le_and_ne, map_le_map_iff_of_injective hf,
    (map_injective_of_injective hf).ne_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
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 : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p : Submodule R M
q : Submodule R₂ M₂
h : q < map f p
⊢ comap f q < p
have rw : map f (comap f q) < map f p
Tactic: rw [← map_lt_map_iff_of_injective hf]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
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 : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R M
h : p ⋖ q
⊢ map f p ⋖ map f q
have refine : ∀ ⦃c : Submodule R₂ M₂⦄, map f p < c → ¬c < map f q
Tactic: refine ⟨lt_of_le_of_ne (map_mono h.1.le) ((map_injective_of_injective hf).ne h.1.ne), ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
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 : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R M
h : p ⋖ q
P : Submodule R₂ M₂
h₁ : map f p < P
h₂ : P < map f q
⊢ False
have refine : p < comap f P
Tactic: refine h.2 ?_ (Submodule.comap_lt_of_lt_map_of_injective hf h₂)
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
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 : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R M
h : p ⋖ q
P : Submodule R₂ M₂
h₁ : map f p < P
h₂ : P < map f q
⊢ p < comap f P
have rw : map f p < map f (comap f P)
Tactic: rw [← Submodule.map_lt_map_iff_of_injective hf]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
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 : Injective.{u_5 + 1, u_7 + 1} (α := M) (β := M₂) (⇑f : (a : M) → M₂)
p q : Submodule R M
h : p ⋖ q
P : Submodule R₂ M₂
h₁ : map f p < P
h₂ : P < map f q
⊢ map f p < map f (comap f P)
have refine : P ≤ map f (comap f P)
Tactic: refine h₁.trans_le ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (goal)
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
σ : R →+* R
ι : Sort u_9
f : M →ₛₗ[σ] M
p : ι → Submodule R M
hf : ∀ (i : ι), ∀ v ∈ p i, Membership.mem (α := M) (p i) ((f : (a : M) → M) v : M)
⊢ ∀ v ∈ iInf p, Membership.mem (α := M) (iInf p) ((f : (a : M) → M) v : M)
have simp : ∀ (v : M), (∀ (i : ι), v ∈ p i) → ∀ (i : ι), Membership.mem (α := M) (p i) ((f : (a : M) → M) v : M)
Tactic: simp only [mem_iInf]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (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
⊢ Disjoint p q ↔ comap p.subtype q = ⊥
have rw : Disjoint p q ↔ map p.subtype (comap p.subtype q) = map p.subtype ⊥
Tactic: rw [← (map_injective_of_injective (show Injective p.subtype from Subtype.coe_injective)).eq_iff,
    map_comap_subtype, map_bot, disjoint_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Map (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
rw : Disjoint p q ↔ map p.subtype (comap p.subtype q) = map p.subtype ⊥
⊢ Disjoint p q ↔ comap p.subtype q = ⊥
have rw₁ : Disjoint p q ↔ p ⊓ q = map p.subtype ⊥
Tactic: rw [← (map_injective_of_injective (show Injective p.subtype from Subtype.coe_injective)).eq_iff,
    map_comap_subtype, map_bot, disjoint_iff]