awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
⊢ ∀ (x : M), Membership.mem (γ := Submodule S M) ⊥ x → (0 : (a : M) → M) x = x

Tactic:
simp only [mem_bot, zero_apply, forall_eq]

Premises used: LinearMap.zero_apply, Submodule.mem_bot, forall_eq
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
⊢ IsProj.{u_5, u_6, u_6} (S := S) (M := M) ⊤ (F := M →ₗ[S] M) id

Tactic:
⟨fun _ ↦ trivial, fun _ ↦ congrFun rfl⟩

Premises used: trivial, LinearMap.IsProj.mk, congrFun, rfl
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
U : Submodule S M
f : M →ₗ[S] M
hf : IsProj U f
⊢ U.subtype ∘ₗ hf.codRestrict = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
m : Submodule S M
f : M →ₗ[S] M
hf : IsProj m f
mp : m = ⊤ → f = id
mpr : f = id → m = ⊤
⊢ m = ⊤ ↔ f = id

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
f : M →ₗ[S] M
hf : IsProj.{u_5, u_6, u_6} (S := S) (M := M) ⊤ f
mp : ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((id : (a : M) → M) x : M)
⊢ f = id

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
f : M →ₗ[S] M
hf : IsProj.{u_5, u_6, u_6} (S := S) (M := M) ⊤ f
x : M
⊢ Eq (α := M) ((f : (a : M) → M) x : M) ((id : (a : M) → M) x : M)

Tactic:
simp [hf.map_id]

Premises used: LinearMap.IsProj.map_id
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
m : Submodule S M
hf : IsProj m (F := M →ₗ[S] M) id
mpr : Eq.{u_6 + 1} (α := Submodule S M) (range id) ⊤
mpr₁ mpr₂ : Eq.{u_6 + 1} (α := Submodule S M) ⊤ ⊤
⊢ m = ⊤

Tactic:
rw [← hf.range, range_id]

Premises used: LinearMap.range_id, LinearMap.IsProj.range
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
m : Submodule S M
f : M →ₗ[S] M
hf : IsProj m f
mp : m = ⊥ → f = 0
mpr : f = 0 → m = ⊥
⊢ m = ⊥ ↔ f = 0

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
f : M →ₗ[S] M
hf : IsProj.{u_5, u_6, u_6} (S := S) (M := M) ⊥ f
mp : ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((0 : (a : M) → M) x : M)
⊢ f = 0

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
f : M →ₗ[S] M
hf : IsProj.{u_5, u_6, u_6} (S := S) (M := M) ⊥ f
x : M
⊢ Eq (α := M) ((f : (a : M) → M) x : M) ((0 : (a : M) → M) x : M)

Tactic:
simpa using hf.map_mem _

Premises used: LinearMap.IsProj.map_mem
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
m : Submodule S M
hf : IsProj m (F := M →ₗ[S] M) 0
mpr : Eq.{u_6 + 1} (α := Submodule S M) (range (R := S) (M := M) (τ₁₂ := RingHom.id S) 0) ⊥
mpr₁ mpr₂ : Eq.{u_6 + 1} (α := Submodule S M) ⊥ ⊥
⊢ m = ⊥

Tactic:
rw [← hf.range, range_zero]

Premises used: LinearMap.IsProj.range, LinearMap.range_zero
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
f : E →ₗ[R] E
hf : IsIdempotentElem f
⊢ IsCompl f.range f.ker

Tactic:
hf.isProj_range.isCompl

Premises used: LinearMap.IsProj.isCompl, LinearMap.IsIdempotentElem.isProj_range
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
p : M →ₗ[S] M
hp : IsIdempotentElem p
x : M
⊢ x ∈ p.range ↔ (p : (a : M) → M) x = x

Tactic:
hp.isProj_range.mem_iff_map_id

Premises used: LinearMap.IsProj.mem_iff_map_id, LinearMap.IsIdempotentElem.isProj_range
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
T : E →ₗ[R] E
hT : IsIdempotentElem T
⊢ ofIsCompl ⋯ T.range.subtype 0 = T.range.projection T.ker ⋯

Tactic:
ofIsCompl_subtype_zero_eq hT.isCompl

Premises used: LinearMap.IsIdempotentElem.isCompl, LinearMap.ofIsCompl_subtype_zero_eq
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
T : E →ₗ[R] E
hT : IsIdempotentElem T
h : T = ofIsCompl ⋯ T.range.subtype 0
⊢ T = T.range.projection T.ker ⋯

Tactic:
convert! ofIsCompl_subtype_zero_eq hT.isCompl

Premises used: LinearMap.IsIdempotentElem.isCompl, LinearMap.ofIsCompl_subtype_zero_eq
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
T : E →ₗ[R] E
hT : IsIdempotentElem T
⊢ ∀ (u : ↥T.range), Eq (α := E) ((T.range.subtype : (a : ↥T.range) → E) u : E) ((T : (a : E) → E) (↑u : E) : E)

Tactic:
simp [hT.isProj_range.map_id]

Premises used: LinearMap.IsProj.map_id, LinearMap.IsIdempotentElem.isProj_range
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
T : E →ₗ[R] E
hT : IsIdempotentElem T
⊢ ∀ (u : ↥T.ker), Eq (α := E) ((0 : (a : ↥T.ker) → E) u : E) ((T : (a : E) → E) (↑u : E) : E)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
T : E →ₗ[R] E
hT : IsIdempotentElem T
⊢ T = ofIsCompl ⋯ T.range.subtype 0

Tactic:
exact ofIsCompl_eq _ (by simp [hT.isProj_range.map_id]) (by simp) |>.symm

Premises used: LinearMap.ofIsCompl_eq, Eq.symm
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
T : E →ₗ[R] E
⊢ IsIdempotentElem T ↔ ∃ (h : IsCompl T.range T.ker), T = T.range.projection T.ker h

Tactic:
⟨fun hT => ⟨hT.isProj_range.isCompl, hT.eq_projection⟩,
   fun ⟨hT, h⟩ => h.symm ▸ isIdempotentElem_projection hT⟩

Premises used: LinearMap.IsProj.isCompl, Eq.rec, LinearMap.IsIdempotentElem.eq_projection, IsIdempotentElem, Iff.intro, LinearMap.IsIdempotentElem.isProj_range, Exists.intro, _private.0.LinearMap.isIdempotentElem_iff_eq_projection_range_ker.match_1, Eq.symm, Submodule.isIdempotentElem_projection
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
S : Type u_5
inst : Semiring S
M : Type u_6
inst_1 : AddCommMonoid M
inst_2 : Module S M
q : M →ₗ[S] M
hq : IsIdempotentElem q
E : Type u_7
inst_3 : AddCommMonoid E
inst_4 : Module S E
p : E →ₗ[S] M
simp_rw :
  (∀ (x : E), Eq.{u_6 + 1} (α := M) ((q ∘ₗ p : (a : E) → M) x : M) ((p : (a : E) → M) x : M)) ↔ p.range ≤ q.range
simp_rw₁ :
  (∀ (x : E), Eq (α := M) ((q : (a : M) → M) ((p : (a : E) → M) x : M) : M) ((p : (a : E) → M) x : M)) ↔
    p.range ≤ q.range
simp_rw₂ : (∀ (x : E), Membership.mem (α := M) q.range ((p : (a : E) → M) x : M)) ↔ p.range ≤ q.range
simp_rw₃ : (∀ (x : E), Membership.mem (α := M) q.range ((p : (a : E) → M) x : M)) ↔ ∀ ⦃x : M⦄, x ∈ p.range → x ∈ q.range
simp_rw₄ :
  (∀ (x : E), ∃ (y : M), Eq (α := M) ((q : (a : M) → M) y : M) ((p : (a : E) → M) x : M)) ↔
    ∀ ⦃x : M⦄, (∃ (y : E), (p : (a : E) → M) y = x) → ∃ (y : M), (q : (a : M) → M) y = x
simp_rw₅ :
  (∀ (x : E), ∃ (y : M), Eq (α := M) ((q : (a : M) → M) y : M) ((p : (a : E) → M) x : M)) ↔
    ∀ ⦃x : M⦄ (x_1 : E) (h : (p : (a : E) → M) x_1 = x), ∃ (y : M), (q : (a : M) → M) y = x
⊢ q ∘ₗ p = p ↔ p.range ≤ q.range

Tactic:
simp_rw [LinearMap.ext_iff, comp_apply, ← hq.mem_range_iff,
    SetLike.le_def, mem_range, forall_exists_index, forall_apply_eq_imp_iff]

Premises used: SetLike.le_def, LinearMap.comp_apply, forall_exists_index, LinearMap.ext_iff, LinearMap.mem_range, LinearMap.IsIdempotentElem.mem_range_iff, forall_apply_eq_imp_iff
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
p q : E →ₗ[R] E
hp : IsIdempotentElem p
hq : IsIdempotentElem q
⊢ p = q ↔ p.range = q.range ∧ p.ker = q.ker

Tactic:
⟨fun h => ⟨congrArg range h, congrArg ker h⟩, fun ⟨hr, hk⟩ => ?_⟩

Premises used: congrArg, LinearMap.ker, _private.0.LinearMap.IsIdempotentElem.ext_iff.match_1, LinearMap.range, And.intro, Iff.intro, Eq
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
p q : E →ₗ[R] E
hp : IsIdempotentElem p
hq : IsIdempotentElem q
refine : p.range = q.range ∧ p.ker = q.ker → ∀ (hr : p.range = q.range) (hk : p.ker = q.ker), p = q
⊢ p = q ↔ p.range = q.range ∧ p.ker = q.ker

Tactic:
refine ⟨fun h => ⟨congrArg range h, congrArg ker h⟩, fun ⟨hr, hk⟩ => ?_⟩
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
p q : E →ₗ[R] E
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h_1 : p.range = q.range ∧ p.ker = q.ker
hr : p.range = q.range
hk : p.ker = q.ker
h : ∀ (x : E), Eq (α := E) ((p : (a : E) → E) x : E) ((q : (a : E) → E) x : E)
⊢ p = q

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
p q : E →ₗ[R] E
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h_1 : p.range = q.range ∧ p.ker = q.ker
hr : p.range = q.range
hk : p.ker = q.ker
x : E
h :
  ∀ (v : E) (hv : v ∈ p.ker) (w : E) (hw : w ∈ p.range),
    (∀ (r : ↥p.ker) (s : ↥p.range),
        (↑r : E) + (↑s : E) =
            (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ p.ker) v hv) : E) +
              (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ p.range) w hw) : E) →
          r = Subtype.mk (p := fun (x : E) ↦ x ∈ p.ker) v hv ∧ s = Subtype.mk (p := fun (x : E) ↦ x ∈ p.range) w hw) →
      Eq (α := E)
        ((p : (a : E) → E)
            ((↑(Subtype.mk (p := fun (x : E) ↦ x ∈ p.ker) v hv) : E) +
              (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ p.range) w hw) : E)) :
          E)
        ((q : (a : E) → E)
            ((↑(Subtype.mk (p := fun (x : E) ↦ x ∈ p.ker) v hv) : E) +
              (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ p.range) w hw) : E)) :
          E)
⊢ Eq (α := E) ((p : (a : E) → E) x : E) ((q : (a : E) → E) x : E)

Tactic:
obtain ⟨⟨v, hv⟩, ⟨w, hw⟩, rfl, _⟩ :=
    (ker p).existsUnique_add_of_isCompl hp.isCompl.symm x

Premises used: LinearMap.IsIdempotentElem.isCompl, Submodule.existsUnique_add_of_isCompl, rfl, IsCompl.symm
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
p q : E →ₗ[R] E
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p.range = q.range ∧ p.ker = q.ker
hr : p.range = q.range
hk : p.ker = q.ker
v : E
hv : v ∈ p.ker
w : E
hw : w ∈ p.range
right :
  ∀ (r : ↥p.ker) (s : ↥p.range),
    (↑r : E) + (↑s : E) =
        (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ p.ker) v hv) : E) +
          (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ p.range) w hw) : E) →
      r = Subtype.mk (p := fun (x : E) ↦ x ∈ p.ker) v hv ∧ s = Subtype.mk (p := fun (x : E) ↦ x ∈ p.range) w hw
⊢ Eq (α := E)
    ((p : (a : E) → E)
        ((↑(Subtype.mk (p := fun (x : E) ↦ x ∈ p.ker) v hv) : E) +
          (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ p.range) w hw) : E)) :
      E)
    ((q : (a : E) → E)
        ((↑(Subtype.mk (p := fun (x : E) ↦ x ∈ p.ker) v hv) : E) +
          (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ p.range) w hw) : E)) :
      E)

Tactic:
simp [mem_ker.mp, hv, (hk ▸ hv), (mem_range_iff hp).mp, hw, (mem_range_iff hq).mp, (hr ▸ hw)]

Premises used: LinearMap.mem_ker, LinearMap.IsIdempotentElem.mem_range_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
S : Type u_5
inst : Semiring S
E : Type u_7
inst_1 : AddCommGroup E
inst_2 : Module S E
p : E →ₗ[S] E
hp : IsIdempotentElem p
x : E
hx : x ∈ (id - p).ker
⊢ (p : (a : E) → E) x = x

Tactic:
simpa [sub_eq_zero, eq_comm (a := x)] using hx

Premises used: sub_eq_zero, eq_comm
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
S : Type u_5
inst : Semiring S
E : Type u_7
inst_1 : AddCommGroup E
inst_2 : Module S E
p : E →ₗ[S] E
hp : IsIdempotentElem p
⊢ p.range = (1 - p).ker

Tactic:
range_eq_ker hp

Premises used: LinearMap.IsIdempotentElem.range_eq_ker
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
S : Type u_5
inst : Semiring S
E : Type u_7
inst_1 : AddCommGroup E
inst_2 : Module S E
p : E →ₗ[S] E
hp : IsIdempotentElem p
⊢ p.ker = (id - p).range

Tactic:
simpa using hp.one_sub.range_eq_ker_one_sub.symm

Premises used: IsIdempotentElem.one_sub, LinearMap.IsIdempotentElem.range_eq_ker_one_sub, Eq.symm
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
S : Type u_5
inst : Semiring S
E : Type u_7
inst_1 : AddCommGroup E
inst_2 : Module S E
p : E →ₗ[S] E
hp : IsIdempotentElem p
⊢ p.ker = (1 - p).range

Tactic:
ker_eq_range hp

Premises used: LinearMap.IsIdempotentElem.ker_eq_range
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
S : Type u_5
inst : Semiring S
M : Type u_7
inst_1 : AddCommGroup M
inst_2 : Module S M
q : M →ₗ[S] M
hq : IsIdempotentElem q
E : Type u_8
inst_3 : AddCommGroup E
inst_4 : Module S E
p : M →ₗ[S] E
⊢ p ∘ₗ q = p ↔ q.ker ≤ p.ker

Tactic:
simp [hq.ker_eq_range, range_le_ker_iff, comp_sub, sub_eq_zero, eq_comm]

Premises used: sub_eq_zero, LinearMap.IsIdempotentElem.ker_eq_range, eq_comm, LinearMap.comp_sub, LinearMap.range_le_ker_iff
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
R : Type u_1
inst : CommRing R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
rw :
  f =
    ((↑(p.prodEquivOfIsCompl f.ker ⋯) : ↥p × ↥f.ker →ₗ[R] E) ∘ₗ prodMap id 0) ∘ₗ
      (↑(p.prodEquivOfIsCompl f.ker ⋯).symm : E →ₗ[R] ↥p × ↥f.ker)
⊢ f =
    ((LinearEquiv.conj.{u_1, u_1, u_2, u_2} (R₁' := R) (R₂' := R) (M₁' := ↥p × ↥f.ker) (M₂' := E) (σ₁'₂' :=
            RingHom.id R) (σ₂'₁' := RingHom.id R) (p.prodEquivOfIsCompl f.ker ⋯) :
          Module.End R (↥p × ↥f.ker) ≃ₗ[R] Module.End R E) :
        (a : Module.End R (↥p × ↥f.ker)) → Module.End R E)
      (prodMap id 0)

Tactic:
rw [LinearEquiv.conj_apply]

Premises used: LinearEquiv.conj_apply
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
R : Type u_1
inst : CommRing R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ f =
    ((↑(p.prodEquivOfIsCompl f.ker ⋯) : ↥p × ↥f.ker →ₗ[R] E) ∘ₗ prodMap id 0) ∘ₗ
      (↑(p.prodEquivOfIsCompl f.ker ⋯).symm : E →ₗ[R] ↥p × ↥f.ker)

Tactic:
h.eq_conj_prod_map'

Premises used: Set.Mem, LinearMap.IsProj.eq_conj_prod_map'
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
R : Type u_1
inst : CommRing R
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ f =
    ((↑(p.prodEquivOfIsCompl f.ker ⋯) : ↥p × ↥f.ker →ₗ[R] E) ∘ₗ prodMap id 0) ∘ₗ
      (↑(p.prodEquivOfIsCompl f.ker ⋯).symm : E →ₗ[R] ↥p × ↥f.ker)

Tactic:
exact h.eq_conj_prod_map'

Premises used: LinearMap.IsProj.eq_conj_prod_map'
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
E : Type u_1
R : Type u_2
inst : Ring R
inst_1 : AddCommGroup E
inst_2 : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
rw : f.range ∈ Module.End.invtSubmodule T ↔ (T ∘ₗ f).range ≤ f.range
rw₁ : f.range ∈ Module.End.invtSubmodule T ↔ map T f.range ≤ f.range
rw₂ rw₃ : map T f.range ≤ f.range ↔ map T f.range ≤ f.range
⊢ f.range ∈ Module.End.invtSubmodule T ↔ f ∘ₗ T ∘ₗ f = T ∘ₗ f

Tactic:
rw [hf.comp_eq_right_iff, range_comp, Module.End.mem_invtSubmodule_iff_map_le]

Premises used: LinearMap.IsIdempotentElem.comp_eq_right_iff, LinearMap.range_comp, Module.End.mem_invtSubmodule_iff_map_le
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
E : Type u_1
R : Type u_2
inst : Ring R
inst_1 : AddCommGroup E
inst_2 : Module R E
T f : E →ₗ[R] E
U : Submodule R E
hf : IsProj U f
⊢ U ∈ Module.End.invtSubmodule T ↔ f ∘ₗ T ∘ₗ f = T ∘ₗ f

Tactic:
hf.range ▸ hf.isIdempotentElem.range_mem_invtSubmodule_iff

Premises used: LinearMap.IsProj.range, Eq.rec, LinearMap.IsProj.isIdempotentElem, LinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
E : Type u_1
R : Type u_2
inst : Ring R
inst_1 : AddCommGroup E
inst_2 : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
rw : f.ker ∈ Module.End.invtSubmodule T ↔ (f ∘ₗ T) ∘ₗ f = f ∘ₗ T
rw₁ : f.ker ∈ Module.End.invtSubmodule T ↔ f.ker ≤ (f ∘ₗ T).ker
rw₂ : f.ker ∈ Module.End.invtSubmodule T ↔ f.ker ≤ comap T f.ker
rw₃ rw₄ : f.ker ≤ comap T f.ker ↔ f.ker ≤ comap T f.ker
⊢ f.ker ∈ Module.End.invtSubmodule T ↔ f ∘ₗ T ∘ₗ f = f ∘ₗ T

Tactic:
rw [← comp_assoc, hf.comp_eq_left_iff, ker_comp, Module.End.mem_invtSubmodule]

Premises used: Module.End.mem_invtSubmodule, LinearMap.comp_assoc, LinearMap.ker_comp, LinearMap.IsIdempotentElem.comp_eq_left_iff
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
E : Type u_1
R : Type u_2
inst : Ring R
inst_1 : AddCommGroup E
inst_2 : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
simp_rw : Commute f T ↔ f * (T * f) = T * f ∧ f * (T * f) = f * T
⊢ Commute f T ↔ f.range ∈ Module.End.invtSubmodule T ∧ f.ker ∈ Module.End.invtSubmodule T

Tactic:
simp_rw [hf.range_mem_invtSubmodule_iff, hf.ker_mem_invtSubmodule_iff, ← Module.End.mul_eq_comp]

Premises used: Module.End.mul_eq_comp, LinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff, LinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
E : Type u_1
R : Type u_2
inst : Ring R
inst_1 : AddCommGroup E
inst_2 : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
h : Commute f T
⊢ f * (T * f) = T * f ∧ f * (T * f) = f * T

Tactic:
simp [← h.eq, ← mul_assoc, hf.eq]

Premises used: mul_assoc, IsIdempotentElem.eq, Commute.eq
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
E : Type u_1
R : Type u_2
inst : Ring R
inst_1 : AddCommGroup E
inst_2 : Module R E
T f : E →ₗ[R] E
hf : IsIdempotentElem f
⊢ Commute f T ↔ f * (T * f) = T * f ∧ f * (T * f) = f * T

Tactic:
exact ⟨fun h => (by simp [← h.eq, ← mul_assoc, hf.eq]), fun ⟨h1, h2⟩ => h2.symm.trans h1⟩
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
E : Type u_1
R : Type u_2
inst : Ring R
inst_1 : AddCommGroup E
inst_2 : Module R E
T f : E →ₗ[R] E
hT : IsUnit T
hf : IsIdempotentElem f
⊢ IsUnit T

Tactic:
hT
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
E : Type u_1
R : Type u_2
inst : Ring R
inst_1 : AddCommGroup E
inst_2 : Module R E
T f : E →ₗ[R] E
hT : IsUnit T
hf : IsIdempotentElem f
lift :
  ∀ (T : (E →ₗ[R] E)ˣ),
    Commute f (↑T : E →ₗ[R] E) ↔ map (↑T : E →ₗ[R] E) f.range = f.range ∧ map (↑T : E →ₗ[R] E) f.ker = f.ker
⊢ Commute f T ↔ map T f.range = f.range ∧ map T f.ker = f.ker

Tactic:
lift T to GeneralLinearGroup R E using hT

Premises used: LinearMap.GeneralLinearGroup
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
E : Type u_1
R : Type u_2
inst : Ring R
inst_1 : AddCommGroup E
inst_2 : Module R E
f : E →ₗ[R] E
hf : IsIdempotentElem f
T : (E →ₗ[R] E)ˣ
simp_rw :
  Commute f (↑T : E →ₗ[R] E) →
    Commute f
      (↑(LinearEquiv.symm ((GeneralLinearGroup.generalLinearEquiv R E : (a : GeneralLinearGroup R E) → E ≃ₗ[R] E) T)) :
        E →ₗ[R] E)
⊢ Commute f (↑T : E →ₗ[R] E) ↔ map (↑T : E →ₗ[R] E) f.range = f.range ∧ map (↑T : E →ₗ[R] E) f.ker = f.ker

Tactic:
simp_rw [← GeneralLinearGroup.generalLinearEquiv_to_linearMap, le_antisymm_iff,
    ← Module.End.mem_invtSubmodule_iff_map_le, ← Module.End.mem_invtSubmodule_symm_iff_le_map,
    and_and_and_comm (c := (ker f ∈ _)), ← hf.commute_iff,
    GeneralLinearGroup.generalLinearEquiv_to_linearMap, iff_self_and]

Premises used: LinearMap.IsIdempotentElem.commute_iff, LinearMap.GeneralLinearGroup.generalLinearEquiv_to_linearMap, iff_self_and, and_and_and_comm, le_antisymm_iff, Module.End.mem_invtSubmodule_symm_iff_le_map, Module.End.mem_invtSubmodule_iff_map_le
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
E : Type u_1
R : Type u_2
inst : Ring R
inst_1 : AddCommGroup E
inst_2 : Module R E
f : E →ₗ[R] E
hf : IsIdempotentElem f
T : (E →ₗ[R] E)ˣ
⊢ Commute f (↑T : E →ₗ[R] E) →
    Commute f
      (↑(LinearEquiv.symm ((GeneralLinearGroup.generalLinearEquiv R E : (a : GeneralLinearGroup R E) → E ≃ₗ[R] E) T)) :
        E →ₗ[R] E)

Tactic:
Commute.units_inv_right

Premises used: Commute.units_inv_right
-- Module: Mathlib.LinearAlgebra.Projection
Goal:
E : Type u_1
R : Type u_2
inst : Ring R
inst_1 : AddCommGroup E
inst_2 : Module R E
f : E →ₗ[R] E
hf : IsIdempotentElem f
T : (E →ₗ[R] E)ˣ
⊢ Commute f (↑T : E →ₗ[R] E) →
    Commute f
      (↑(LinearEquiv.symm ((GeneralLinearGroup.generalLinearEquiv R E : (a : GeneralLinearGroup R E) → E ≃ₗ[R] E) T)) :
        E →ₗ[R] E)

Tactic:
exact Commute.units_inv_right

Premises used: Commute.units_inv_right
-- Module: Mathlib.LinearAlgebra.Projectivization.Action
Goal:
G : Type u_1
K : Type u_2
V : Type u_3
inst : AddCommGroup V
inst_1 : DivisionRing K
inst_2 : Module K V
inst_3 : Group G
inst_4 : DistribMulAction G V
inst_5 : SMulCommClass G K V
g g' : G
x : ℙ K V
simp_rw :
  map
      ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g ∘ₗ
        (DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g')
      ⋯ x =
    map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g) ⋯
      (map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g') ⋯ x)
⊢ map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) (g * g')) ⋯ x =
    map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g) ⋯
      (map ((DistribMulAction.toModuleEnd K V : (a : G) → Module.End K V) g') ⋯ x)

Tactic:
simp_rw [map_mul, Module.End.mul_eq_comp]

Premises used: Module.End.mul_eq_comp, map_mul