-- Mathlib/LinearAlgebra/BilinearMap.lean
theorem compl₁₂_inj {f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ} {g : Qₗ →ₗ[R] Mₗ} {g' : Qₗ' →ₗ[R] Nₗ}
    (hₗ : Function.Surjective g) (hᵣ : Function.Surjective g') :
    f₁.compl₁₂ g g' = f₂.compl₁₂ g g' ↔ f₁ = f₂

Proof state:
case mp.h.h.intro.intro
R : Type u_1
inst✝¹⁰ : CommSemiring R
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝⁹ : AddCommMonoid Mₗ
inst✝⁸ : AddCommMonoid Nₗ
inst✝⁷ : AddCommMonoid Pₗ
inst✝⁶ : AddCommMonoid Qₗ
inst✝⁵ : AddCommMonoid Qₗ'
inst✝⁴ : Module R Mₗ
inst✝³ : Module R Nₗ
inst✝² : Module R Pₗ
inst✝¹ : Module R Qₗ
inst✝ : Module R Qₗ'
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Surjective ⇑g
hᵣ : Surjective ⇑g'
h : f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
x' : Qₗ
y' : Qₗ'
⊢ (f₁ (g x')) (g' y') = (f₂ (g x')) (g' y')

Tactic:
convert LinearMap.congr_fun₂ h x' y' using 0

Result:
no goals

Proof state:
case mp
R : Type u_1
inst✝¹⁰ : CommSemiring R
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝⁹ : AddCommMonoid Mₗ
inst✝⁸ : AddCommMonoid Nₗ
inst✝⁷ : AddCommMonoid Pₗ
inst✝⁶ : AddCommMonoid Qₗ
inst✝⁵ : AddCommMonoid Qₗ'
inst✝⁴ : Module R Mₗ
inst✝³ : Module R Nₗ
inst✝² : Module R Pₗ
inst✝¹ : Module R Qₗ
inst✝ : Module R Qₗ'
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Surjective ⇑g
hᵣ : Surjective ⇑g'
h : f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
⊢ f₁ = f₂

Tactic:
ext x y

Result:
case mp.h.h
R : Type u_1
inst✝¹⁰ : CommSemiring R
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝⁹ : AddCommMonoid Mₗ
inst✝⁸ : AddCommMonoid Nₗ
inst✝⁷ : AddCommMonoid Pₗ
inst✝⁶ : AddCommMonoid Qₗ
inst✝⁵ : AddCommMonoid Qₗ'
inst✝⁴ : Module R Mₗ
inst✝³ : Module R Nₗ
inst✝² : Module R Pₗ
inst✝¹ : Module R Qₗ
inst✝ : Module R Qₗ'
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Surjective ⇑g
hᵣ : Surjective ⇑g'
h : f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
x : Mₗ
y : Nₗ
⊢ (f₁ x) y = (f₂ x) y

Proof state:
case mp.h.h.intro.intro
R : Type u_1
inst✝¹⁰ : CommSemiring R
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝⁹ : AddCommMonoid Mₗ
inst✝⁸ : AddCommMonoid Nₗ
inst✝⁷ : AddCommMonoid Pₗ
inst✝⁶ : AddCommMonoid Qₗ
inst✝⁵ : AddCommMonoid Qₗ'
inst✝⁴ : Module R Mₗ
inst✝³ : Module R Nₗ
inst✝² : Module R Pₗ
inst✝¹ : Module R Qₗ
inst✝ : Module R Qₗ'
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Surjective ⇑g
hᵣ : Surjective ⇑g'
h : f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
y : Nₗ
x' : Qₗ
y' : Qₗ'
hy : g' y' = y
⊢ (f₁ (g x')) y = (f₂ (g x')) y

Tactic:
subst hy

Result:
case mp.h.h.intro.intro
R : Type u_1
inst✝¹⁰ : CommSemiring R
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝⁹ : AddCommMonoid Mₗ
inst✝⁸ : AddCommMonoid Nₗ
inst✝⁷ : AddCommMonoid Pₗ
inst✝⁶ : AddCommMonoid Qₗ
inst✝⁵ : AddCommMonoid Qₗ'
inst✝⁴ : Module R Mₗ
inst✝³ : Module R Nₗ
inst✝² : Module R Pₗ
inst✝¹ : Module R Qₗ
inst✝ : Module R Qₗ'
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Surjective ⇑g
hᵣ : Surjective ⇑g'
h : f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
x' : Qₗ
y' : Qₗ'
⊢ (f₁ (g x')) (g' y') = (f₂ (g x')) (g' y')

Proof state:
case mp.h.h.intro
R : Type u_1
inst✝¹⁰ : CommSemiring R
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝⁹ : AddCommMonoid Mₗ
inst✝⁸ : AddCommMonoid Nₗ
inst✝⁷ : AddCommMonoid Pₗ
inst✝⁶ : AddCommMonoid Qₗ
inst✝⁵ : AddCommMonoid Qₗ'
inst✝⁴ : Module R Mₗ
inst✝³ : Module R Nₗ
inst✝² : Module R Pₗ
inst✝¹ : Module R Qₗ
inst✝ : Module R Qₗ'
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Surjective ⇑g
hᵣ : Surjective ⇑g'
h : f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
x : Mₗ
y : Nₗ
x' : Qₗ
hx : g x' = x
⊢ (f₁ x) y = (f₂ x) y

Tactic:
subst hx

Result:
case mp.h.h.intro
R : Type u_1
inst✝¹⁰ : CommSemiring R
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝⁹ : AddCommMonoid Mₗ
inst✝⁸ : AddCommMonoid Nₗ
inst✝⁷ : AddCommMonoid Pₗ
inst✝⁶ : AddCommMonoid Qₗ
inst✝⁵ : AddCommMonoid Qₗ'
inst✝⁴ : Module R Mₗ
inst✝³ : Module R Nₗ
inst✝² : Module R Pₗ
inst✝¹ : Module R Qₗ
inst✝ : Module R Qₗ'
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Surjective ⇑g
hᵣ : Surjective ⇑g'
h : f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
y : Nₗ
x' : Qₗ
⊢ (f₁ (g x')) y = (f₂ (g x')) y

Proof state:
R : Type u_1
inst✝¹⁰ : CommSemiring R
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝⁹ : AddCommMonoid Mₗ
inst✝⁸ : AddCommMonoid Nₗ
inst✝⁷ : AddCommMonoid Pₗ
inst✝⁶ : AddCommMonoid Qₗ
inst✝⁵ : AddCommMonoid Qₗ'
inst✝⁴ : Module R Mₗ
inst✝³ : Module R Nₗ
inst✝² : Module R Pₗ
inst✝¹ : Module R Qₗ
inst✝ : Module R Qₗ'
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Surjective ⇑g
hᵣ : Surjective ⇑g'
⊢ f₁.compl₁₂ g g' = f₂.compl₁₂ g g' ↔ f₁ = f₂

Tactic:
constructor <;> intro h

Result:
case mp
R : Type u_1
inst✝¹⁰ : CommSemiring R
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝⁹ : AddCommMonoid Mₗ
inst✝⁸ : AddCommMonoid Nₗ
inst✝⁷ : AddCommMonoid Pₗ
inst✝⁶ : AddCommMonoid Qₗ
inst✝⁵ : AddCommMonoid Qₗ'
inst✝⁴ : Module R Mₗ
inst✝³ : Module R Nₗ
inst✝² : Module R Pₗ
inst✝¹ : Module R Qₗ
inst✝ : Module R Qₗ'
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Surjective ⇑g
hᵣ : Surjective ⇑g'
h : f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
⊢ f₁ = f₂

case mpr
R : Type u_1
inst✝¹⁰ : CommSemiring R
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝⁹ : AddCommMonoid Mₗ
inst✝⁸ : AddCommMonoid Nₗ
inst✝⁷ : AddCommMonoid Pₗ
inst✝⁶ : AddCommMonoid Qₗ
inst✝⁵ : AddCommMonoid Qₗ'
inst✝⁴ : Module R Mₗ
inst✝³ : Module R Nₗ
inst✝² : Module R Pₗ
inst✝¹ : Module R Qₗ
inst✝ : Module R Qₗ'
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Surjective ⇑g
hᵣ : Surjective ⇑g'
h : f₁ = f₂
⊢ f₁.compl₁₂ g g' = f₂.compl₁₂ g g'

Proof state:
case mp.h.h.intro
R : Type u_1
inst✝¹⁰ : CommSemiring R
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝⁹ : AddCommMonoid Mₗ
inst✝⁸ : AddCommMonoid Nₗ
inst✝⁷ : AddCommMonoid Pₗ
inst✝⁶ : AddCommMonoid Qₗ
inst✝⁵ : AddCommMonoid Qₗ'
inst✝⁴ : Module R Mₗ
inst✝³ : Module R Nₗ
inst✝² : Module R Pₗ
inst✝¹ : Module R Qₗ
inst✝ : Module R Qₗ'
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Surjective ⇑g
hᵣ : Surjective ⇑g'
h : f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
y : Nₗ
x' : Qₗ
⊢ (f₁ (g x')) y = (f₂ (g x')) y

Tactic:
obtain ⟨y', hy⟩ := hᵣ y

Result:
case mp.h.h.intro.intro
R : Type u_1
inst✝¹⁰ : CommSemiring R
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝⁹ : AddCommMonoid Mₗ
inst✝⁸ : AddCommMonoid Nₗ
inst✝⁷ : AddCommMonoid Pₗ
inst✝⁶ : AddCommMonoid Qₗ
inst✝⁵ : AddCommMonoid Qₗ'
inst✝⁴ : Module R Mₗ
inst✝³ : Module R Nₗ
inst✝² : Module R Pₗ
inst✝¹ : Module R Qₗ
inst✝ : Module R Qₗ'
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Surjective ⇑g
hᵣ : Surjective ⇑g'
h : f₁.compl₁₂ g g' = f₂.compl₁₂ g g'
y : Nₗ
x' : Qₗ
y' : Qₗ'
hy : g' y' = y
⊢ (f₁ (g x')) y = (f₂ (g x')) y

Proof state:
case mpr
R : Type u_1
inst✝¹⁰ : CommSemiring R
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝⁹ : AddCommMonoid Mₗ
inst✝⁸ : AddCommMonoid Nₗ
inst✝⁷ : AddCommMonoid Pₗ
inst✝⁶ : AddCommMonoid Qₗ
inst✝⁵ : AddCommMonoid Qₗ'
inst✝⁴ : Module R Mₗ
inst✝³ : Module R Nₗ
inst✝² : Module R Pₗ
inst✝¹ : Module R Qₗ
inst✝ : Module R Qₗ'
f₁ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Surjective ⇑g
hᵣ : Surjective ⇑g'
⊢ f₁.compl₁₂ g g' = f₁.compl₁₂ g g'

Tactic:
rfl

Result:
no goals