awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : RingHomSurjective σ
inst_3 : AddCommMonoid G
inst_4 : Module R G
inst_5 : AddCommMonoid H
inst_6 : Module S H
inst_7 : AddCommMonoid I
inst_8 : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective.{u_5 + 1, u_6 + 1} (α := G) (β := H) (Function.comp (β := H × I) Prod.fst (⇑f : (a : G) → H × I))
hf₂ : Surjective.{u_5 + 1, u_7 + 1} (α := G) (β := I) (Function.comp (β := H × I) Prod.snd (⇑f : (a : G) → H × I))
hf :
  ∀ (g₁ g₂ : G),
    Eq.{u_6 + 1} (α := H) ((f : (a : G) → H × I) g₁).1 ((f : (a : G) → H × I) g₂).1 ↔
      Eq.{u_7 + 1} (α := I) ((f : (a : G) → H × I) g₁).2 ((f : (a : G) → H × I) g₂).2
e₁ : H →ₗ[S] I
he₁ : f.range = e₁.graph
e₂ : I →ₗ[S] H
he₂ : ((↑(LinearEquiv.prodComm S H I) : H × I →ₗ[S] I × H) ∘ₛₗ f).range = e₂.graph
he₁₂ : ∀ (h : H) (i : I), (e₁ : (a : H) → I) h = i ↔ (e₂ : (a : I) → H) i = h
⊢ ∃ (e : H ≃ₗ[S] I), f.range = (↑e : H →ₗ[S] I).graph

Tactic:
exact ⟨
  { toFun := e₁
    map_smul' := e₁.map_smul'
    map_add' := e₁.map_add'
    invFun := e₂
    left_inv := fun h ↦ by rw [← he₁₂]
    right_inv := fun i ↦ by rw [he₁₂] }, he₁⟩
-- Module: Mathlib.LinearAlgebra.Prod
Goal:
S : Type u_4
H : Type u_6
I : Type u_7
inst : Semiring S
inst_1 : AddCommMonoid H
inst_2 : Module S H
inst_3 : AddCommMonoid I
inst_4 : Module S I
G : Submodule S (H × I)
hG₁ : Bijective (α := ↥G) (β := H) (comp (β := H × I) Prod.fst (⇑G.subtype : (a : ↥G) → H × I))
hG₂ : Bijective (α := ↥G) (β := I) (comp (β := H × I) Prod.snd (⇑G.subtype : (a : ↥G) → H × I))
⊢ ∃ (e : H ≃ₗ[S] I), G = (↑e : H →ₗ[S] I).graph

Tactic:
simpa only [range_subtype] using LinearMap.exists_linearEquiv_eq_graph
    hG₁.surjective hG₂.surjective fun _ _ ↦ hG₁.injective.eq_iff.trans hG₂.injective.eq_iff.symm

Premises used: LinearMap.exists_linearEquiv_eq_graph, Function.Injective.eq_iff, Function.Bijective.injective, Function.Bijective.surjective, Iff.trans, Submodule.range_subtype, Iff.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 : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), (f : (a : E) → ↥p) (↑x : E) = x
h : ∀ (x : E), x ∈ (id - p.subtype ∘ₗ f).ker ↔ x ∈ p
⊢ (id - p.subtype ∘ₗ f).ker = p

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 : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), (f : (a : E) → ↥p) (↑x : E) = x
x : E
h : x = (↑((f : (a : E) → ↥p) x) : E) ↔ x ∈ p
⊢ x ∈ (id - p.subtype ∘ₗ f).ker ↔ x ∈ p

Tactic:
simp only [comp_apply, mem_ker, subtype_apply, sub_apply, id_apply, sub_eq_zero]

Premises used: LinearMap.id_apply, sub_eq_zero, Submodule.subtype_apply, LinearMap.comp_apply, LinearMap.mem_ker, LinearMap.sub_apply
-- 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 : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), (f : (a : E) → ↥p) (↑x : E) = x
x : E
hx : x ∈ p
rw : x = (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ p) x hx) : E)
rw₁ rw₂ : x = x
⊢ x = (↑((f : (a : E) → ↥p) x) : E)

Tactic:
rw [hf ⟨x, hx⟩, Subtype.coe_mk]

Premises used: Subtype.coe_mk, Subtype.mk
-- 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 : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), (f : (a : E) → ↥p) (↑x : E) = x
x : E
⊢ x = (↑((f : (a : E) → ↥p) x) : E) ↔ x ∈ p

Tactic:
exact ⟨fun h => h.symm ▸ Submodule.coe_mem _, fun hx => by rw [hf ⟨x, hx⟩, Subtype.coe_mk]⟩
-- 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 : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), (f : (a : E) → ↥p) (↑x : E) = x
⊢ f.range = ⊤

Tactic:
range_eq_top.2 fun x => ⟨x, hf x⟩

Premises used: Iff.mpr, LinearMap.range_eq_top, Exists.intro, Subtype.val
-- 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 : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), (f : (a : E) → ↥p) (↑x : E) = x
disjoint : Disjoint p f.ker
codisjoint : Codisjoint p f.ker
⊢ IsCompl p f.ker

Tactic:
constructor
-- 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 : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), (f : (a : E) → ↥p) (↑x : E) = x
disjoint : p ⊓ f.ker ≤ ⊥
⊢ Disjoint p f.ker

Tactic:
rw [disjoint_iff_inf_le]

Premises used: disjoint_iff_inf_le
-- 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 : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), (f : (a : E) → ↥p) (↑x : E) = x
x : E
hpx : x ∈ (↑p : Set E)
hfx : x ∈ (↑f.ker : Set E)
⊢ x = 0

Tactic:
rw [SetLike.mem_coe, mem_ker, hf ⟨x, hpx⟩, mk_eq_zero] at hfx

Premises used: LinearMap.mem_ker, Subtype.mk, SetLike.mem_coe, Submodule.mk_eq_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
p : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), (f : (a : E) → ↥p) (↑x : E) = x
x : E
hpx : x ∈ (↑p : Set E)
hfx : x = 0
⊢ Membership.mem (γ := Submodule R E) ⊥ x

Tactic:
simp only [hfx, zero_mem]

Premises used: ZeroMemClass.zero_mem
-- 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 : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), (f : (a : E) → ↥p) (↑x : E) = x
codisjoint : ⊤ ≤ p ⊔ f.ker
⊢ Codisjoint p f.ker

Tactic:
rw [codisjoint_iff_le_sup]

Premises used: codisjoint_iff_le_sup
-- 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 : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), (f : (a : E) → ↥p) (↑x : E) = x
x : E
codisjoint : Membership.mem (γ := Submodule R E) ⊤ x → x ∈ p ⊔ f.ker
⊢ Membership.mem (γ := Submodule R E) ⊤ x → x ∈ p ⊔ f.ker

Tactic:
_
-- 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 : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), (f : (a : E) → ↥p) (↑x : E) = x
x : E
h : Membership.mem (γ := Submodule R E) ⊤ x
codisjoint : ∃ (y : ↥p) (z : ↥f.ker), (↑y : E) + (↑z : E) = x
⊢ x ∈ p ⊔ f.ker

Tactic:
rw [mem_sup']

Premises used: Submodule.mem_sup'
-- 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 : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), (f : (a : E) → ↥p) (↑x : E) = x
x : E
h : Membership.mem (γ := Submodule R E) ⊤ x
⊢ ∃ (y : ↥p) (z : ↥f.ker), (↑y : E) + (↑z : E) = x

Tactic:
⟨f x, ⟨x - f x, ?_⟩, add_sub_cancel _ _⟩

Premises used: HSub.hSub, Subtype.mk, add_sub_cancel, Exists.intro, Subtype.val, DFunLike.coe
-- 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 : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), (f : (a : E) → ↥p) (↑x : E) = x
x : E
h : Membership.mem (γ := Submodule R E) ⊤ x
codisjoint : x - (↑((f : (a : E) → ↥p) x) : E) ∈ f.ker
⊢ ∃ (y : ↥p) (z : ↥f.ker), (↑y : E) + (↑z : E) = x

Tactic:
refine ⟨f x, ⟨x - f x, ?_⟩, add_sub_cancel _ _⟩
-- 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 : Submodule R E
f : E →ₗ[R] ↥p
hf : ∀ (x : ↥p), (f : (a : E) → ↥p) (↑x : E) = x
x : E
h : Membership.mem (γ := Submodule R E) ⊤ x
codisjoint : Eq (α := ↥p) ((f : (a : E) → ↥p) (x - (↑((f : (a : E) → ↥p) x) : E)) : ↥p) (0 : ↥p)
codisjoint₁ :
  HSub.hSub (α := ↥p) (β := ↥p) ((f : (a : E) → ↥p) x : ↥p) ((f : (a : E) → ↥p) (↑((f : (a : E) → ↥p) x) : E) : ↥p) = 0
codisjoint₂ : HSub.hSub (α := ↥p) (β := ↥p) ((f : (a : E) → ↥p) x : ↥p) ((f : (a : E) → ↥p) x : ↥p) = 0
codisjoint₃ codisjoint₄ : Eq.{u_2 + 1} (α := ↥p) 0 0
⊢ x - (↑((f : (a : E) → ↥p) x) : E) ∈ f.ker

Tactic:
rw [mem_ker, map_sub, hf, sub_self]

Premises used: map_sub, sub_self, LinearMap.mem_ker
-- 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 : Type u_3
inst_3 : AddCommGroup F
inst_4 : Module R F
G : Type u_4
inst_5 : AddCommGroup G
inst_6 : Module R G
p q : Submodule R E
S : Type u_5
inst_7 : Semiring S
M : Type u_6
inst_8 : AddCommMonoid M
inst_9 : Module S M
m : Submodule S M
h : IsCompl p q
apply : Function.Bijective (α := ↥p × ↥q) (β := E) (⇑(p.subtype.coprod q.subtype) : (a : ↥p × ↥q) → E)
⊢ (↥p × ↥q) ≃ₗ[R] E

Tactic:
apply LinearEquiv.ofBijective (p.subtype.coprod q.subtype)

Premises used: LinearMap.coprod, Submodule.subtype, LinearEquiv.ofBijective
-- 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 : Type u_3
inst_3 : AddCommGroup F
inst_4 : Module R F
G : Type u_4
inst_5 : AddCommGroup G
inst_6 : Module R G
p q : Submodule R E
S : Type u_5
inst_7 : Semiring S
M : Type u_6
inst_8 : AddCommMonoid M
inst_9 : Module S M
m : Submodule S M
h : IsCompl p q
left : Function.Injective (α := ↥p × ↥q) (β := E) (⇑(p.subtype.coprod q.subtype) : (a : ↥p × ↥q) → E)
right : Function.Surjective (α := ↥p × ↥q) (β := E) (⇑(p.subtype.coprod q.subtype) : (a : ↥p × ↥q) → E)
⊢ Function.Bijective (α := ↥p × ↥q) (β := E) (⇑(p.subtype.coprod q.subtype) : (a : ↥p × ↥q) → E)

Tactic:
constructor
-- 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 : Type u_3
inst_3 : AddCommGroup F
inst_4 : Module R F
G : Type u_4
inst_5 : AddCommGroup G
inst_6 : Module R G
p q : Submodule R E
S : Type u_5
inst_7 : Semiring S
M : Type u_6
inst_8 : AddCommMonoid M
inst_9 : Module S M
m : Submodule S M
h : IsCompl p q
left : Disjoint p.subtype.range q.subtype.range
⊢ Function.Injective (α := ↥p × ↥q) (β := E) (⇑(p.subtype.coprod q.subtype) : (a : ↥p × ↥q) → E)

Tactic:
rw [← ker_eq_bot, ker_coprod_of_disjoint_range, ker_subtype, ker_subtype, prod_bot]

Premises used: LinearMap.ker_coprod_of_disjoint_range, Submodule.ker_subtype, LinearMap.ker_eq_bot, Submodule.prod_bot
-- 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 : Type u_3
inst_3 : AddCommGroup F
inst_4 : Module R F
G : Type u_4
inst_5 : AddCommGroup G
inst_6 : Module R G
p q : Submodule R E
S : Type u_5
inst_7 : Semiring S
M : Type u_6
inst_8 : AddCommMonoid M
inst_9 : Module S M
m : Submodule S M
h : IsCompl p q
left : Disjoint p q
⊢ Disjoint p.subtype.range q.subtype.range

Tactic:
rw [range_subtype, range_subtype]

Premises used: Submodule.range_subtype
-- 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 : Type u_3
inst_3 : AddCommGroup F
inst_4 : Module R F
G : Type u_4
inst_5 : AddCommGroup G
inst_6 : Module R G
p q : Submodule R E
S : Type u_5
inst_7 : Semiring S
M : Type u_6
inst_8 : AddCommMonoid M
inst_9 : Module S M
m : Submodule S M
h : IsCompl p q
⊢ Disjoint p q

Tactic:
h.1

Premises used: IsCompl.disjoint
-- 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 : Type u_3
inst_3 : AddCommGroup F
inst_4 : Module R F
G : Type u_4
inst_5 : AddCommGroup G
inst_6 : Module R G
p q : Submodule R E
S : Type u_5
inst_7 : Semiring S
M : Type u_6
inst_8 : AddCommMonoid M
inst_9 : Module S M
m : Submodule S M
h : IsCompl p q
⊢ Disjoint p q

Tactic:
exact h.1

Premises used: IsCompl.disjoint
-- 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 : Type u_3
inst_3 : AddCommGroup F
inst_4 : Module R F
G : Type u_4
inst_5 : AddCommGroup G
inst_6 : Module R G
p q : Submodule R E
S : Type u_5
inst_7 : Semiring S
M : Type u_6
inst_8 : AddCommMonoid M
inst_9 : Module S M
m : Submodule S M
h : IsCompl p q
right : (p.subtype.coprod q.subtype).range = ⊤
right₁ : p ⊔ q = ⊤
right₂ right₃ : Eq.{u_2 + 1} (α := Submodule R E) ⊤ ⊤
⊢ Function.Surjective (α := ↥p × ↥q) (β := E) (⇑(p.subtype.coprod q.subtype) : (a : ↥p × ↥q) → E)

Tactic:
rw [← range_eq_top, ← sup_eq_range, h.sup_eq_top]

Premises used: IsCompl.sup_eq_top, Submodule.sup_eq_range, LinearMap.range_eq_top
-- 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 : Submodule R E
h : IsCompl p q
⊢ (↑(p.prodEquivOfIsCompl q h) : ↥p × ↥q →ₗ[R] E) = p.subtype.coprod q.subtype

Tactic:
rfl

Premises used: LinearMap.coprod, rfl
-- 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 : Submodule R E
h : IsCompl p q
x : ↥p × ↥q
⊢ (p.prodEquivOfIsCompl q h : (a : ↥p × ↥q) → E) x = (↑x.1 : E) + (↑x.2 : E)

Tactic:
rfl

Premises used: rfl
-- 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 : Submodule R E
h : IsCompl p q
x : ↥p
⊢ (↑x : E) = (p.prodEquivOfIsCompl q h : (a : ↥p × ↥q) → E) (x, 0)

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
p q : Submodule R E
h : IsCompl p q
x : ↥q
⊢ (↑x : E) = (p.prodEquivOfIsCompl q h : (a : ↥p × ↥q) → E) (0, x)

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
p q : Submodule R E
h : IsCompl p q
x : E
rw :
  Membership.mem (α := E) q
    ((p.prodEquivOfIsCompl q h : (a : ↥p × ↥q) → E)
        (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x : ↥p × ↥q) :
      E)
| x ∈ q

Tactic:
rw [← (prodEquivOfIsCompl p q h).apply_symm_apply x]

Premises used: Submodule.prodEquivOfIsCompl, LinearEquiv.apply_symm_apply
-- 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 : Submodule R E
h : IsCompl p q
x : E
conv_rhs :
  Eq.{u_2 + 1} (α := ↥p) (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).1 0 ↔
    Membership.mem (α := E) q
      ((p.prodEquivOfIsCompl q h : (a : ↥p × ↥q) → E)
          (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x : ↥p × ↥q) :
        E)
⊢ Eq.{u_2 + 1} (α := ↥p) (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).1 0 ↔ x ∈ q

Tactic:
conv_rhs => rw [← (prodEquivOfIsCompl p q h).apply_symm_apply x]

Premises used: Submodule.prodEquivOfIsCompl, LinearEquiv.apply_symm_apply
-- 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 : Submodule R E
h : IsCompl p q
x : E
rw :
  Eq.{u_2 + 1} (α := ↥p) (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).1 0 ↔
    HAdd.hAdd (α := E) (↑(((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).1 : E)
        (↑(((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).2 : E) ∈
      q
rw₁ :
  Eq.{u_2 + 1} (α := ↥p) (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).1 0 ↔
    (↑(((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).1 : E) ∈ q
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := ↥p) (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).1 0 ↔
    Eq.{u_2 + 1} (α := ↥p) (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).1 0
⊢ Eq.{u_2 + 1} (α := ↥p) (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).1 0 ↔
    Membership.mem (α := E) q
      ((p.prodEquivOfIsCompl q h : (a : ↥p × ↥q) → E)
          (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x : ↥p × ↥q) :
        E)

Tactic:
rw [coe_prodEquivOfIsCompl', Submodule.add_mem_iff_left _ (Submodule.coe_mem _),
    mem_right_iff_eq_zero_of_disjoint h.disjoint]

Premises used: Submodule.coe_prodEquivOfIsCompl', Submodule.coe_mem, Submodule.mem_right_iff_eq_zero_of_disjoint, Submodule.add_mem_iff_left, IsCompl.disjoint
-- 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 : Submodule R E
h : IsCompl p q
x : E
rw :
  Membership.mem (α := E) p
    ((p.prodEquivOfIsCompl q h : (a : ↥p × ↥q) → E)
        (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x : ↥p × ↥q) :
      E)
| x ∈ p

Tactic:
rw [← (prodEquivOfIsCompl p q h).apply_symm_apply x]

Premises used: Submodule.prodEquivOfIsCompl, LinearEquiv.apply_symm_apply
-- 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 : Submodule R E
h : IsCompl p q
x : E
conv_rhs :
  Eq.{u_2 + 1} (α := ↥q) (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).2 0 ↔
    Membership.mem (α := E) p
      ((p.prodEquivOfIsCompl q h : (a : ↥p × ↥q) → E)
          (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x : ↥p × ↥q) :
        E)
⊢ Eq.{u_2 + 1} (α := ↥q) (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).2 0 ↔ x ∈ p

Tactic:
conv_rhs => rw [← (prodEquivOfIsCompl p q h).apply_symm_apply x]

Premises used: Submodule.prodEquivOfIsCompl, LinearEquiv.apply_symm_apply
-- 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 : Submodule R E
h : IsCompl p q
x : E
rw :
  Eq.{u_2 + 1} (α := ↥q) (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).2 0 ↔
    HAdd.hAdd (α := E) (↑(((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).1 : E)
        (↑(((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).2 : E) ∈
      p
rw₁ :
  Eq.{u_2 + 1} (α := ↥q) (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).2 0 ↔
    (↑(((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).2 : E) ∈ p
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := ↥q) (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).2 0 ↔
    Eq.{u_2 + 1} (α := ↥q) (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).2 0
⊢ Eq.{u_2 + 1} (α := ↥q) (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).2 0 ↔
    Membership.mem (α := E) p
      ((p.prodEquivOfIsCompl q h : (a : ↥p × ↥q) → E)
          (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x : ↥p × ↥q) :
        E)

Tactic:
rw [coe_prodEquivOfIsCompl', Submodule.add_mem_iff_right _ (Submodule.coe_mem _),
    mem_left_iff_eq_zero_of_disjoint h.disjoint]

Premises used: Submodule.coe_prodEquivOfIsCompl', Submodule.mem_left_iff_eq_zero_of_disjoint, Submodule.coe_mem, Submodule.add_mem_iff_right, IsCompl.disjoint
-- 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 : Submodule R E
h : IsCompl p q
⊢ LinearEquiv.prodComm R ↥q ↥p ≪≫ₗ p.prodEquivOfIsCompl q h = q.prodEquivOfIsCompl p ⋯

Tactic:
LinearEquiv.ext fun _ => add_comm _ _

Premises used: LinearMap.fst, LinearMap.snd, Membership.mem, LinearEquiv.ext, Subtype, add_comm, LinearEquiv.prodComm, LinearMap.comp, LinearEquiv.toLinearMap, Submodule.subtype, DFunLike.coe
-- 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 : Submodule R E
hpq : IsCompl p q
x : E
⊢ Eq (α := E) ((p.projection q hpq : (a : E) → E) x : E) ((↑((p.projectionOnto q hpq : (a : E) → ↥p) x) : E) : E)

Tactic:
rfl

Premises used: rfl
-- 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 : Submodule R E
hpq : IsCompl p q
x : E
⊢ Eq (α := E) ((↑((p.projectionOnto q hpq : (a : E) → ↥p) x) : E) : E) ((p.projection q hpq : (a : E) → E) x : E)

Tactic:
rfl

Premises used: rfl
-- 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 : Submodule R E
hpq : IsCompl p q
x : E
⊢ Membership.mem (α := E) p ((p.projection q hpq : (a : E) → E) x : E)

Tactic:
SetLike.coe_mem _

Premises used: SetLike.coe_mem, Set.Mem
-- 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 : Submodule R E
h : IsCompl p q
x : ↥p
⊢ (p.projectionOnto q h : (a : E) → ↥p) (↑x : E) = x

Tactic:
simp [projectionOnto, prodEquivOfIsCompl_symm_apply_left]

Premises used: Submodule.prodEquivOfIsCompl_symm_apply_left, Submodule.projectionOnto
-- 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 : Submodule R E
hpq : IsCompl p q
x : ↥p
⊢ (p.projection q hpq : (a : E) → E) (↑x : E) = (↑x : E)

Tactic:
simp [projection]

Premises used: Submodule.projection
-- 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 : Submodule R E
h : IsCompl p q
⊢ (p.projectionOnto q h).range = ⊤

Tactic:
range_eq_of_proj (projectionOnto_apply_left h)

Premises used: Submodule.projectionOnto_apply_left, LinearMap.range_eq_of_proj
-- 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 : Submodule R E
hpq : IsCompl p q
⊢ (p.projection q hpq).range = p

Tactic:
simp [projection, range_comp]

Premises used: Submodule.projection, LinearMap.range_comp
-- 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 : Submodule R E
h : IsCompl p q
⊢ Function.Surjective (α := E) (β := ↥p) (⇑(p.projectionOnto q h) : (a : E) → ↥p)

Tactic:
range_eq_top.mp (range_projectionOnto h)

Premises used: Submodule.range_projectionOnto, LinearMap.range_eq_top, Iff.mp
-- 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 : Submodule R E
h : IsCompl p q
x : E
⊢ Eq (α := ↥p) ((p.projectionOnto q h : (a : E) → ↥p) x : ↥p) (0 : ↥p) ↔ x ∈ q

Tactic:
simp [projectionOnto, prodEquivOfIsCompl_symm_apply_fst_eq_zero]

Premises used: Submodule.prodEquivOfIsCompl_symm_apply_fst_eq_zero, Submodule.projectionOnto
-- 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 : Submodule R E
hpq : IsCompl p q
x : E
⊢ Eq (α := E) ((p.projection q hpq : (a : E) → E) x : E) (0 : E) ↔ x ∈ q

Tactic:
simp [projection, -coe_projectionOnto_apply]

Premises used: Submodule.projection, Submodule.coe_projectionOnto_apply
-- 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 : Submodule R E
h : IsCompl p q
x : ↥q
⊢ Eq (α := ↥p) ((p.projectionOnto q h : (a : E) → ↥p) (↑x : E) : ↥p) (0 : ↥p)

Tactic:
projectionOnto_apply_of_mem_right h x.2

Premises used: Submodule.projectionOnto_apply_of_mem_right, Subtype.property
-- 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 : Submodule R E
h : IsCompl p q
x : ↥q
⊢ Eq (α := E) ((p.projection q h : (a : E) → E) (↑x : E) : E) (0 : E)

Tactic:
projection_apply_of_mem_right h x.2

Premises used: Submodule.projection_apply_of_mem_right, Subtype.property
-- 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 : Submodule R E
h : IsCompl p q
⊢ (p.projectionOnto q h).ker = q

Tactic:
ext fun _ => mem_ker.trans (projectionOnto_apply_eq_zero_iff h)

Premises used: Submodule.projectionOnto_apply_eq_zero_iff, LinearMap.mem_ker, Iff.trans, Submodule.ext
-- 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 : Submodule R E
hpq : IsCompl p q
⊢ (p.projection q hpq).ker = q

Tactic:
simp [projection, ker_comp]

Premises used: Submodule.projection, LinearMap.ker_comp