awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (hypothesis)
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
h : H
i : I
⊢ (e₁ : (a : H) → I) h = i ↔ (e₂ : (a : I) → H) i = h
have he₃ : ∀ (x : H × I), x ∈ f.range ↔ x.2 = (e₁ : (a : H) → I) x.1
Tactic: simp only [SetLike.ext_iff, LinearMap.mem_graph_iff] at he₁ he₂
Cleared hypotheses: he₁, he₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (hypothesis)
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
h : H
i : I
he₃ : ∀ (x : H × I), x ∈ f.range ↔ x.2 = (e₁ : (a : H) → I) x.1
⊢ (e₁ : (a : H) → I) h = i ↔ (e₂ : (a : I) → H) i = h
have he₄ : ∀ (x : I × H), x ∈ ((↑(LinearEquiv.prodComm S H I) : H × I →ₗ[S] I × H) ∘ₛₗ f).range ↔ x.2 = (e₂ : (a : I) → H) x.1
Tactic: simp only [SetLike.ext_iff, LinearMap.mem_graph_iff] at he₁ he₂
Cleared hypotheses: he₁, he₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
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
e₂ : I →ₗ[S] H
h : H
i : I
he₁ : ∀ (x : H × I), x ∈ f.range ↔ x.2 = (e₁ : (a : H) → I) x.1
he₂ :
  ∀ (x : I × H), x ∈ ((↑(LinearEquiv.prodComm S H I) : H × I →ₗ[S] I × H) ∘ₛₗ f).range ↔ x.2 = (e₂ : (a : I) → H) x.1
⊢ (e₁ : (a : H) → I) h = i ↔ (e₂ : (a : I) → H) i = h
have rw : (h, i) ∈ f.range ↔ (i, h) ∈ ((↑(LinearEquiv.prodComm S H I) : H × I →ₗ[S] I × H) ∘ₛₗ f).range
Tactic: rw [Eq.comm, ← he₁ (h, i), Eq.comm, ← he₂ (i, h)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (hypothesis)
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
⊢ ∃ (e : H ≃ₗ[S] I), f.range = (↑e : H →ₗ[S] I).graph
have he₁₂ : ∀ (h : H) (i : I), (e₁ : (a : H) → I) h = i ↔ (e₂ : (a : I) → H) i = h
Tactic: have he₁₂ h i : e₁ h = i ↔ e₂ i = h := by
    simp only [SetLike.ext_iff, LinearMap.mem_graph_iff] at he₁ he₂
    rw [Eq.comm, ← he₁ (h, i), Eq.comm, ← he₂ (i, h)]
    simp only [mem_range, coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
      LinearEquiv.prodComm_apply, Prod.swap_eq_iff_eq_swap, Prod.swap_prod_mk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
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
h : H
⊢ (e₂ : (a : I) → H) ((e₁ : (a : H) → I) h : I) = h
have rw : Eq.{u_7 + 1} (α := I) ((e₁ : (a : H) → I) h : I) ((e₁ : (a : H) → I) h : I)
Tactic: rw [← he₁₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Prod (goal)
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
i : I
⊢ (e₁ : (a : H) → I) ((e₂ : (a : I) → H) i : H) = i
have rw : Eq.{u_6 + 1} (α := H) ((e₂ : (a : I) → H) i : H) ((e₂ : (a : I) → H) i : H)
Tactic: rw [he₁₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
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
⊢ (id - p.subtype ∘ₗ f).ker = p
have h : ∀ (x : E), x ∈ (id - p.subtype ∘ₗ f).ker ↔ x ∈ p
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
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 ∈ (id - p.subtype ∘ₗ f).ker ↔ x ∈ p
have h : x = (↑((f : (a : E) → ↥p) x) : E) ↔ x ∈ p
Tactic: simp only [comp_apply, mem_ker, subtype_apply, sub_apply, id_apply, sub_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
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
⊢ x = (↑((f : (a : E) → ↥p) x) : E)
have rw : x = (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ p) x hx) : E)
Tactic: rw [hf ⟨x, hx⟩, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
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)
⊢ x = (↑((f : (a : E) → ↥p) x) : E)
have rw₁ : x = x
Tactic: rw [hf ⟨x, hx⟩, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
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
⊢ IsCompl p f.ker
have disjoint : Disjoint p f.ker
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
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
⊢ IsCompl p f.ker
have codisjoint : Codisjoint p f.ker
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
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
have disjoint : p ⊓ f.ker ≤ ⊥
Tactic: rw [disjoint_iff_inf_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (hypothesis)
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)
⊢ Membership.mem (γ := Submodule R E) ⊥ x
have hfx₁ : x = 0
Tactic: rw [SetLike.mem_coe, mem_ker, hf ⟨x, hpx⟩, mk_eq_zero] at hfx
Cleared hypotheses: hfx
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
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
have codisjoint : ⊤ ≤ p ⊔ f.ker
Tactic: rw [codisjoint_iff_le_sup]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
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
⊢ x ∈ p ⊔ f.ker
have codisjoint : ∃ (y : ↥p) (z : ↥f.ker), (↑y : E) + (↑z : E) = x
Tactic: rw [mem_sup']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
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
have codisjoint : x - (↑((f : (a : E) → ↥p) x) : E) ∈ f.ker
Tactic: refine ⟨f x, ⟨x - f x, ?_⟩, add_sub_cancel _ _⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
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
⊢ x - (↑((f : (a : E) → ↥p) x) : E) ∈ f.ker
have codisjoint : Eq (α := ↥p) ((f : (a : E) → ↥p) (x - (↑((f : (a : E) → ↥p) x) : E)) : ↥p) (0 : ↥p)
Tactic: rw [mem_ker, map_sub, hf, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
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)
⊢ x - (↑((f : (a : E) → ↥p) x) : E) ∈ f.ker
have codisjoint₁ : HSub.hSub (α := ↥p) (β := ↥p) ((f : (a : E) → ↥p) x : ↥p) ((f : (a : E) → ↥p) (↑((f : (a : E) → ↥p) x) : E) : ↥p) = 0
Tactic: rw [mem_ker, map_sub, hf, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
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
⊢ x - (↑((f : (a : E) → ↥p) x) : E) ∈ f.ker
have codisjoint₂ : HSub.hSub (α := ↥p) (β := ↥p) ((f : (a : E) → ↥p) x : ↥p) ((f : (a : E) → ↥p) x : ↥p) = 0
Tactic: rw [mem_ker, map_sub, hf, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
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
⊢ x - (↑((f : (a : E) → ↥p) x) : E) ∈ f.ker
have codisjoint₃ : Eq.{u_2 + 1} (α := ↥p) 0 0
Tactic: rw [mem_ker, map_sub, hf, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
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
⊢ (↥p × ↥q) ≃ₗ[R] E
have apply : Function.Bijective (α := ↥p × ↥q) (β := E) (⇑(p.subtype.coprod q.subtype) : (a : ↥p × ↥q) → E)
Tactic: apply LinearEquiv.ofBijective (p.subtype.coprod q.subtype)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
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
⊢ Function.Bijective (α := ↥p × ↥q) (β := E) (⇑(p.subtype.coprod q.subtype) : (a : ↥p × ↥q) → E)
have left : Function.Injective (α := ↥p × ↥q) (β := E) (⇑(p.subtype.coprod q.subtype) : (a : ↥p × ↥q) → E)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
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)
⊢ Function.Bijective (α := ↥p × ↥q) (β := E) (⇑(p.subtype.coprod q.subtype) : (a : ↥p × ↥q) → E)
have right : Function.Surjective (α := ↥p × ↥q) (β := E) (⇑(p.subtype.coprod q.subtype) : (a : ↥p × ↥q) → E)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
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
⊢ Function.Injective (α := ↥p × ↥q) (β := E) (⇑(p.subtype.coprod q.subtype) : (a : ↥p × ↥q) → E)
have left : Disjoint p.subtype.range q.subtype.range
Tactic: rw [← ker_eq_bot, ker_coprod_of_disjoint_range, ker_subtype, ker_subtype, prod_bot]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
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.subtype.range q.subtype.range
have left : Disjoint p q
Tactic: rw [range_subtype, range_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
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
⊢ Function.Surjective (α := ↥p × ↥q) (β := E) (⇑(p.subtype.coprod q.subtype) : (a : ↥p × ↥q) → E)
have right : (p.subtype.coprod q.subtype).range = ⊤
Tactic: rw [← range_eq_top, ← sup_eq_range, h.sup_eq_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
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 = ⊤
⊢ Function.Surjective (α := ↥p × ↥q) (β := E) (⇑(p.subtype.coprod q.subtype) : (a : ↥p × ↥q) → E)
have right₁ : p ⊔ q = ⊤
Tactic: rw [← range_eq_top, ← sup_eq_range, h.sup_eq_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
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 = ⊤
⊢ Function.Surjective (α := ↥p × ↥q) (β := E) (⇑(p.subtype.coprod q.subtype) : (a : ↥p × ↥q) → E)
have right₂ : Eq.{u_2 + 1} (α := Submodule R E) ⊤ ⊤
Tactic: rw [← range_eq_top, ← sup_eq_range, h.sup_eq_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
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
| x ∈ q
have 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)
Tactic: rw [← (prodEquivOfIsCompl p q h).apply_symm_apply x]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
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.{u_2 + 1} (α := ↥p) (((p.prodEquivOfIsCompl q h).symm : (a : E) → ↥p × ↥q) x).1 0 ↔ x ∈ q
have 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)
Tactic: conv_rhs => rw [← (prodEquivOfIsCompl p q h).apply_symm_apply x]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
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.{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)
have 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
Tactic: rw [coe_prodEquivOfIsCompl', Submodule.add_mem_iff_left _ (Submodule.coe_mem _),
    mem_right_iff_eq_zero_of_disjoint h.disjoint]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
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
⊢ 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)
have 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
Tactic: rw [coe_prodEquivOfIsCompl', Submodule.add_mem_iff_left _ (Submodule.coe_mem _),
    mem_right_iff_eq_zero_of_disjoint h.disjoint]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
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
⊢ 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)
have 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
Tactic: rw [coe_prodEquivOfIsCompl', Submodule.add_mem_iff_left _ (Submodule.coe_mem _),
    mem_right_iff_eq_zero_of_disjoint h.disjoint]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Projection (goal)
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
| x ∈ p
have 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)
Tactic: rw [← (prodEquivOfIsCompl p q h).apply_symm_apply x]