-- Mathlib/LinearAlgebra/Prod.lean
theorem isCompl_range_inl_inr : IsCompl (range <| inl R M M₂) (range <| inr R M M₂)

Proof state:
case codisjoint.mk
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M
y : M₂
⊢ (x, y) ∈ range (inl R M M₂) ⊔ range (inr R M M₂)

Tactic:
simp only [mem_sup, mem_range, exists_prop]

Result:
case codisjoint.mk
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M
y : M₂
⊢ ∃ y_1, (∃ y, (inl R M M₂) y = y_1) ∧ ∃ z, (∃ y, (inr R M M₂) y = z) ∧ y_1 + z = (x, y)

Proof state:
case disjoint.mk.intro.intro
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
fst✝ : M
snd✝ : M₂
x : M
hx : (inl R M M₂) x = (fst✝, snd✝)
y : M₂
hy : (inr R M M₂) y = (fst✝, snd✝)
⊢ (fst✝, snd✝) = 0

Tactic:
simp only [Prod.ext_iff, inl_apply, inr_apply, mem_bot] at hx hy ⊢

Result:
case disjoint.mk.intro.intro
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
fst✝ : M
snd✝ : M₂
x : M
y : M₂
hx : x = fst✝ ∧ 0 = snd✝
hy : 0 = fst✝ ∧ y = snd✝
⊢ fst✝ = 0.1 ∧ snd✝ = 0.2

Proof state:
case disjoint
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ ∀ x ∈ range (inl R M M₂), x ∈ range (inr R M M₂) → x = 0

Tactic:
rintro ⟨_, _⟩ ⟨x, hx⟩ ⟨y, hy⟩

Result:
case disjoint.mk.intro.intro
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
fst✝ : M
snd✝ : M₂
x : M
hx : (inl R M M₂) x = (fst✝, snd✝)
y : M₂
hy : (inr R M M₂) y = (fst✝, snd✝)
⊢ (fst✝, snd✝) = 0

Proof state:
case codisjoint
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ Codisjoint (range (inl R M M₂)) (range (inr R M M₂))

Tactic:
rw [codisjoint_iff_le_sup]

Result:
case codisjoint
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ ⊤ ≤ range (inl R M M₂) ⊔ range (inr R M M₂)

Proof state:
case codisjoint.mk
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M
y : M₂
⊢ (x, 0) + (0, y) = (x, y)

Tactic:
simp

Result:
no goals

Proof state:
case disjoint.mk.intro.intro
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
fst✝ : M
snd✝ : M₂
x : M
y : M₂
hx : x = fst✝ ∧ 0 = snd✝
hy : 0 = fst✝ ∧ y = snd✝
⊢ fst✝ = 0.1 ∧ snd✝ = 0.2

Tactic:
exact ⟨hy.1.symm, hx.2.symm⟩

Result:
no goals

Proof state:
case disjoint
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ Disjoint (range (inl R M M₂)) (range (inr R M M₂))

Tactic:
rw [disjoint_def]

Result:
case disjoint
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ ∀ x ∈ range (inl R M M₂), x ∈ range (inr R M M₂) → x = 0

Proof state:
case codisjoint
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ ⊤ ≤ range (inl R M M₂) ⊔ range (inr R M M₂)

Tactic:
rintro ⟨x, y⟩ -

Result:
case codisjoint.mk
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M
y : M₂
⊢ (x, y) ∈ range (inl R M M₂) ⊔ range (inr R M M₂)

Proof state:
case codisjoint.mk
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M
y : M₂
⊢ ∃ y_1, (∃ y, (inl R M M₂) y = y_1) ∧ ∃ z, (∃ y, (inr R M M₂) y = z) ∧ y_1 + z = (x, y)

Tactic:
refine ⟨(x, 0), ⟨x, rfl⟩, (0, y), ⟨y, rfl⟩, ?_⟩

Result:
case codisjoint.mk
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M
y : M₂
⊢ (x, 0) + (0, y) = (x, y)

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ IsCompl (range (inl R M M₂)) (range (inr R M M₂))

Tactic:
constructor

Result:
case disjoint
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ Disjoint (range (inl R M M₂)) (range (inr R M M₂))

case codisjoint
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ Codisjoint (range (inl R M M₂)) (range (inr R M M₂))